Abstract
We present a formalisation in the dependently-typed programming language Agda2 of basic category and allegory theory, and of generalised algebras where function symbols are interpreted in a parameter category. We use this nestable algebra construction as the basis for nestable category and allegory constructions, ultimately aiming at a formalised foundation of the algebraic approach to graph transformation, which uses constructions in categories of graph structures considered as unary algebras.
The features of Agda permit strongly-typed programming with these nested algebras and with relational homomorphisms between them in a natural mathematical style and with remarkable ease, far beyond what can be achieved even in Haskell.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Anand, C.K., Kahl, W.: An optimized Cell BE special function library generated by Coconut. IEEE Transactions on Computers 58(8), 1126–1138 (2009)
Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261–293 (2003)
Berghammer, R., Jaoua, A.M., Möller, B. (eds.): RelMiCS 2009. LNCS, vol. 5827. Springer, Heidelberg (2009)
Bird, R.S., de Moor, O.: Algebra of Programming. International Series in Computer Science, vol. 100. Prentice-Hall, Englewood Cliffs (1997)
Capretta, V.: Universal algebra in type theory. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 131–148. Springer, Heidelberg (1999)
Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation, part I: Basic concepts and double pushout approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Foundations, vol. 1, ch. 3, pp. 163–245. World Scientific, Singapore (1997)
Desharnais, J., Jipsen, P., Struth, G.: Domain and antidomain semigroups. In: Berghammer et al. [3], pp. 73–87
Desharnais, J., Möller, B.: Characterizing determinacy in Kleene algebras. Information Sciences 139, 253–273 (2001)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic 7(4), 798–833 (2006)
Freyd, P.J., Scedrov, A.: Categories, Allegories. North-Holland Mathematical Library, vol. 39. North-Holland, Amsterdam (1990)
Furusawa, H., Kahl, W.: A study on symmetric quotients. Tech. Rep. 1998-06, Fakultät für Informatik, Universität der Bundeswehr München (December 1998)
Gonzalía, C.: Relations in Dependent Type Theory. Ph.D. thesis, also as Technical Report No. 14D, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg University (2006)
Gurevich, Y.: Evolving Algebras: An attempt to discover semantics. In: Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science, pp. 266–292. World Scientific, Singapore (1993)
Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic 1(1), 77–111 (2000)
Han, J.: Proofs of Relational Semigroupoids in Isabelle/Isar. M.Sc. thesis, McMaster University, Department of Computing and Software (2008)
Huet, G., Saïbi, A.: Constructive category theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, language, and interaction: Essays in honour of Robin Milner. Foundations of Computing Series, pp. 239–275. MIT Press, Cambridge (2000)
Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Ph.D. thesis, Cornell University (1995)
Kahl, W.: Calculational relation-algebraic proofs in Isabelle/Isar. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 178–190. Springer, Heidelberg (2004)
Kahl, W.: Relational semigroupoids: Abstract relation-algebraic interfaces for finite relations between infinite types. J. Logic and Algebraic Programming 76(1), 60–89 (2008)
Kahl, W.: Collagories for relational adhesive rewriting. In: Berghammer et al [3], pp. 211–226
Kahl, W.: Amalgamating pushout and pullback graph transformation in collagories. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 362–378. Springer, Heidelberg (2010)
Kahl, W.: Determinisation of relational substitutions in ordered categories with domain. J. Logic and Algebraic Programming 79, 812–829 (2010)
Kanda, A.: Constructive category theory (no. 1). In: Gruska, J., Chytil, M.P. (eds.) MFCS 1981. LNCS, vol. 118, pp. 563–577. Springer, Heidelberg (1981)
McCune, W.: Prover9 and Mace4, version LADR-2009-11A (2009), http://www.prover9.org/
Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming using dependent types. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 268–283. Springer, Heidelberg (2008)
Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (September 2007)
Schmidt, G., Hattensperger, C., Winter, M.: Heterogeneous relation algebra. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science. Advances in Computing Science, ch. 3, pp. 39–53. Springer, Wien (1997)
Schmidt, G., Ströhlein, T.: Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoret. Comput. Sci. Springer, Heidelberg (1993)
West, S., Kahl, W.: A generic graph transformation, visualisation, and editing framework in Haskell. In: Boronat, A., Heckel, R. (eds.) Proceedings of the Eighth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2009). Electronic Communications of the EASST, vol. 18, pp. 12.1–12.18 (September 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kahl, W. (2011). Dependently-Typed Formalisation of Relation-Algebraic Abstractions. In: de Swart, H. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2011. Lecture Notes in Computer Science, vol 6663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21070-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-21070-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21069-3
Online ISBN: 978-3-642-21070-9
eBook Packages: Computer ScienceComputer Science (R0)