Proofs of Relational Semigroupoids in Isabelle/Isar

Abstract

The concept of relations is useful for applications in mathematics, logics and computer science. Once an application structure is identified as a model of a particular relation-algebraic theory, that theory becomes the preferred reasoning environment in this application area. Examples of applications in computer science are database, graph and games. In [Kah03], Kahl proposed using the proof assistant Isabelle/Isar to provide a collection of theories for abstract relation-algebraic reasoning. In [DG04], De Guzman improved and populated the theories introduced by Kahl in [Kah03]. Finite maps or finite relations between infinite sets do not form a category since the necessary identities are infinite. In [Kah08], Kahl presented relation-algebraic extensions of semigroupoids where the operations that would produce infinite results in category have been replaced with their variants that preserve finiteness, but still satisfy useful algebraic laws. In this thesis, we will build a framework by building a hierarchy of Isabelle/Isar theories to implement relational semigroupoid theories which are presented by Kahl in [Kah08], focusing on the following: Since the difference between semigroupoids and categories are that no identities are assumed in semigroupoids, category theories in [DG04] will be transferred into our semigroupoid theories by modifying definitions, reformulating theorems, adding theorems to help reprove theorems involving identities in their proofs. New theorems and new theories will be added to implement subidentity and range and their properties. Then new theorems and new theories about restricted residual and standard residual and their properties will be developed. In [Kah08], Kahl proposed that in ordered semigroupoids with domain and range, if standard residuals exist, then restricted residuals exist too and can be calculated via standard residuals. A new theory will be built to prove this.