Document Open Access Logo

Modular Specification of Monads Through Higher-Order Presentations

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.6.pdf
  • Filesize: 0.63 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic language theory
Keywords
  • free monads
  • presentation of monads
  • 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

Abstract

In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of "models", and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair.
In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating ("higher-order") operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to beta- and eta-equalities. Such a 2-signature is hence a pair (Sigma,E) of a binding signature Sigma and a family E of equations for Sigma. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. 
We associate, to each 2-signature (Sigma,E), a category of "models of (Sigma,E)"; and we say that a 2-signature is "effective" if this category has an initial object; the monad underlying this (essentially unique) object is the "monad specified by the 2-signature". Not every 2-signature is effective; we identify a class of 2-signatures, which we call "algebraic", that are effective.
Importantly, our 2-signatures together with their models enjoy "modularity": when we glue (algebraic) 2-signatures together, their initial models are glued accordingly.
We provide a computer formalization for our main results.

Cite As Get BibTex

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular Specification of Monads Through Higher-Order Presentations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.6

Author Details

Benedikt Ahrens
  • University of Birmingham, United Kingdom
André Hirschowitz
  • Université Côte d'Azur, CNRS, LJAD, Nice, France
Ambroise Lafont
  • IMT Atlantique, Inria, LS2N CNRS, Nantes, 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.
  • Ahrens, Benedikt: Ahrens acknowledges the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the 2018/19 academic year.
  • Maggesi, Marco: Supported by GNSAGA-INdAM and MIUR.

Acknowledgements

We thank Paige R. North for a valuable hint regarding preservation of epimorphisms. We also thank the referees for their careful reading and thoughtful and constructive criticism.

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, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-Level Signatures and Initial Semantics. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:22, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2018.4.
  3. Michael Barr. Coequalizers and free triples. Mathematische Zeitschrift, 116(4):307-322, December 1970. URL: http://dx.doi.org/10.1007/BF01111838.
  4. Ranald Clouston. Binding in Nominal Equational Logic. Electr. Notes Theor. Comput. Sci., 265:259-276, 2010. URL: http://dx.doi.org/10.1016/j.entcs.2010.08.016.
  5. Maribel Fernández and Murdoch J. Gabbay. Closed nominal rewriting and efficiently computable nominal algebra equality. In Karl Crary and Marino Miculan, editors, Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., volume 34 of EPTCS, pages 37-51, 2010. URL: http://dx.doi.org/10.4204/EPTCS.34.5.
  6. Marcelo P. Fiore and Makoto Hamana. Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 520-529. IEEE Computer Society, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.59.
  7. Marcelo P. Fiore and Chung-Kil Hur. On the construction of free algebras for equational systems. Theor. Comput. Sci., 410(18):1704-1729, 2009. URL: http://dx.doi.org/10.1016/j.tcs.2008.12.052.
  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. Marcelo P. Fiore and Philip Saville. List Objects with Algebraic Structure. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:18, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.16.
  12. 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.
  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. Bernhard Gramlich. Modularity in term rewriting revisited. Theoretical Computer Science, 464:3-19, 2012. New Directions in Rewriting (Honoring the 60th Birthday of Yoshihito Toyama). URL: http://dx.doi.org/10.1016/j.tcs.2012.09.008.
  15. Makoto Hamana. Term Rewriting with Variable Binding: An Initial Algebra Approach. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, PPDP '03, pages 148-159, New York, NY, USA, 2003. ACM. URL: http://dx.doi.org/10.1145/888251.888266.
  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. Martin Hofmann. Semantical Analysis of Higher-Order Abstract Syntax. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 204-213. IEEE Computer Society, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782616.
  19. G. Maxwell Kelly and A. John Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89(1):163-179, 1993. URL: http://dx.doi.org/10.1016/0022-4049(93)90092-8.
  20. Alexander Kurz and Daniela Petrisan. On universal algebra over nominal sets. Mathematical Structures in Computer Science, 20(2):285-318, 2010. URL: http://dx.doi.org/10.1017/S0960129509990399.
  21. Christoph Lüth and Neil Ghani. Monads and Modular Term Rewriting. In Eugenio Moggi and Giuseppe Rosolini, editors, Category Theory and Computer Science, 7th International Conference, CTCS '97, volume 1290 of Lecture Notes in Computer Science, pages 69-86. Springer, 1997. URL: http://dx.doi.org/10.1007/BFb0026982.
  22. Ernest Manes. Algebraic Theories, volume 26 of Graduate Texts in Mathematics. Springer, 1976. Google Scholar
  23. The Coq development team. The Coq Proof Assistant, version 8.9, 2019. Version 8.9. URL: http://coq.inria.fr.
  24. A. John Power. Abstract Syntax: Substitution and Binders: Invited Address. Electr. Notes Theor. Comput. Sci., 173:3-16, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.024.
  25. Sam Staton. An Algebraic Presentation of Predicate Logic (Extended Abstract). In Frank Pfenning, editor, Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, volume 7794 of Lecture Notes in Computer Science, pages 401-417. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37075-5_26.
  26. Jiří Velebil and Alexander Kurz. Equational presentations of functors and monads. Mathematical Structures in Computer Science, 21(2):363-381, 2011. URL: http://dx.doi.org/10.1017/S0960129510000575.
  27. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at URL: https://github.com/UniMath/UniMath.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact