Skip to main content
SpringerLink
Log in

Dependently-Typed Formalisation of Relation-Algebraic Abstractions

  • Conference paper
Relational and Algebraic Methods in Computer Science (RAMICS 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6663))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anand, C.K., Kahl, W.: An optimized Cell BE special function library generated by Coconut. IEEE Transactions on Computers 58(8), 1126–1138 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  2. Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261–293 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  3. Berghammer, R., Jaoua, A.M., Möller, B. (eds.): RelMiCS 2009. LNCS, vol. 5827. Springer, Heidelberg (2009)

    MATH  Google Scholar 

  4. Bird, R.S., de Moor, O.: Algebra of Programming. International Series in Computer Science, vol. 100. Prentice-Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Desharnais, J., Jipsen, P., Struth, G.: Domain and antidomain semigroups. In: Berghammer et al. [3], pp. 73–87

    Google Scholar 

  8. Desharnais, J., Möller, B.: Characterizing determinacy in Kleene algebras. Information Sciences 139, 253–273 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  9. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic 7(4), 798–833 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Freyd, P.J., Scedrov, A.: Categories, Allegories. North-Holland Mathematical Library, vol. 39. North-Holland, Amsterdam (1990)

    MATH  Google Scholar 

  11. 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)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic 1(1), 77–111 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. Han, J.: Proofs of Relational Semigroupoids in Isabelle/Isar. M.Sc. thesis, McMaster University, Department of Computing and Software (2008)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Ph.D. thesis, Cornell University (1995)

    Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Kahl, W.: Relational semigroupoids: Abstract relation-algebraic interfaces for finite relations between infinite types. J. Logic and Algebraic Programming 76(1), 60–89 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  20. Kahl, W.: Collagories for relational adhesive rewriting. In: Berghammer et al [3], pp. 211–226

    Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Kahl, W.: Determinisation of relational substitutions in ordered categories with domain. J. Logic and Algebraic Programming 79, 812–829 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. McCune, W.: Prover9 and Mace4, version LADR-2009-11A (2009), http://www.prover9.org/

  25. 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)

    Chapter  Google Scholar 

  26. 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)

    Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. Schmidt, G., Ströhlein, T.: Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoret. Comput. Sci. Springer, Heidelberg (1993)

    Google Scholar 

  29. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. McMaster University, Hamilton, Ontario, Canada

    Wolfram Kahl

Authors
  1. Wolfram Kahl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000, Tilburg, LE, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation