Document Open Access Logo

High-Level Signatures and Initial Semantics

Authors Benedikt Ahrens , André Hirschowitz , Ambroise Lafont , Marco Maggesi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.4.pdf
  • Filesize: 0.57 MB
  • 22 pages

Document Identifiers

Author Details

Benedikt Ahrens
  • University of Birmingham, UK
André Hirschowitz
  • Université Nice Sophia Antipolis, France
Ambroise Lafont
  • IMT Atlantique , Inria, LS2N CNRS, France
Marco Maggesi
  • Università degli Studi di Firenze, Italy

Funding

This work has partly been funded by the CoqHoTT ERC Grant 637339. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-17-1-0363.
  • Maggesi, Marco: Supported by GNSAGA-INdAM and MIUR.

Cite AsGet BibTex

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-Level Signatures and Initial Semantics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.4

Abstract

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we consider a general notion of "signature" for specifying syntactic constructions. Our signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object - if it exists - in a suitable category of models. Our notions of signature and syntax are suited for compositionality and provide, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles. Our signatures are "general" in the sense that the existence of an associated syntax is not automatically guaranteed. In this work, we identify a large and simple class of signatures which do generate a syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic language theory
Keywords
  • initial semantics
  • signatures
  • syntax
  • monadic substitution
  • computer-checked proofs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Benedikt Ahrens. Modules over relative monads for syntax and semantics. Mathematical Structures in Computer Science, 26:3-37, 2016. URL: http://dx.doi.org/10.1017/S0960129514000103.
  2. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, volume 84 of Leibniz International Proceedings in Informatics, pages 5:1-5:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.5.
  3. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. Logical Methods in Computer Science, 11(1), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(1:3)2015.
  4. Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453-468. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-48168-0_32.
  5. Richard S. Bird and Oege de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997. Google Scholar
  6. Richard S. Bird and Ross Paterson. Generalised folds for nested datatypes. Formal Asp. Comput., 11(2):200-222, 1999. URL: http://dx.doi.org/10.1007/s001650050047.
  7. Marcelo P. Fiore. Second-order and dependently-sorted abstract syntax. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 57-68. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.38.
  8. Marcelo P. Fiore and Chung-Kil Hur. Second-order equational logic (extended abstract). In Anuj Dawar and Helmut Veith, editors, CSL, volume 6247 of Lecture Notes in Computer Science, pages 320-335. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15205-4_26.
  9. Marcelo P. Fiore and Ola Mahmoud. Second-order algebraic theories - (extended abstract). In Petr Hlinený and Antonín Kucera, editors, MFCS, volume 6281 of Lecture Notes in Computer Science, pages 368-380. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15155-2_33.
  10. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 193-202, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782615.
  11. Murdoch J. Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax Involving Binders. In 14th Annual Symposium on Logic in Computer Science, pages 214-224, Washington, DC, USA, 1999. IEEE Computer Society Press. URL: http://dx.doi.org/10.1109/LICS.1999.782617.
  12. Neil Ghani and Tarmo Uustalu. Explicit substitutions and higher-order syntax. In MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, pages 1-7, New York, NY, USA, 2003. ACM Press. Google Scholar
  13. Neil Ghani, Tarmo Uustalu, and Makoto Hamana. Explicit substitutions and higher-order syntax. Higher-Order and Symbolic Computation, 19(2-3):263-282, 2006. URL: http://dx.doi.org/10.1007/s10990-006-8748-4.
  14. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50(1):1-102, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  15. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, jan 1993. URL: http://dx.doi.org/10.1145/138027.138060.
  16. André Hirschowitz and Marco Maggesi. Modules over monads and linearity. In D. Leivant and R. J. G. B. de Queiroz, editors, WoLLIC, volume 4576 of Lecture Notes in Computer Science, pages 218-237. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73445-1_16.
  17. André Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Information and Computation, 208(5):545-564, May 2010. Special Issue: 14th Workshop on Logic, Language, Information and Computation (WoLLIC 2007). URL: http://dx.doi.org/10.1016/j.ic.2009.07.003.
  18. André Hirschowitz and Marco Maggesi. Initial semantics for strengthened signatures. In Dale Miller and Ésik Zoltán, editors, Proceedings of the 8th Workshop on Fixed Points in Computer Science, pages 31-38, 2012. URL: http://dx.doi.org/10.4204/EPTCS.77.
  19. Tom Hirschowitz. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science, 9(3):10, 2013. 19 pages. URL: http://dx.doi.org/10.2168/LMCS-9(3:10)2013.
  20. Martin Hyland and John Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science, 172:437-458, April 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.019.
  21. J.W. Thatcher J.A. Goguen and E.G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R. Yeh, editor, Current Trends in Programming Methodology, IV: Data Structuring, pages 80-144. Prentice-Hall, 1978. Google Scholar
  22. Patricia Johann and Neil Ghani. Initial algebra semantics is enough! In Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, pages 207-222, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73228-0_16.
  23. Saunders Mac Lane. Categories for the working mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1998. Google Scholar
  24. Ralph Matthes and Tarmo Uustalu. Substitution in non-wellfounded syntax with variable binding. Theor. Comput. Sci., 327(1-2):155-174, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.07.025.
  25. The Coq development team. The Coq Proof Assistant, version 8.8.0, 2018. Version 8.8. URL: http://coq.inria.fr.
  26. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at URL: https://github.com/UniMath/UniMath.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact