Document Open Access Logo

Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories

Authors Ralph Matthes , Kobe Wullaert , Benedikt Ahrens

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.25.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

Ralph Matthes
  • IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, France
Kobe Wullaert
  • Delft University of Technology, The Netherlands
Benedikt Ahrens
  • Delft University of Technology, The Netherlands
  • University of Birmingham, United Kingdom

Acknowledgements

We thank Henning Basold for pointing us to the work on completely iterative algebras, leading to a simpler proof of Theorem 4. We also thank Thomas Lamiaux for valuable comments on a draft of this paper. We gratefully acknowledge the work by the Coq development team in providing the Coq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Coq. Not least, we thank the anonymous FSCD reviewers for their thoughtful feedback on our submission.

Cite AsGet BibTex

Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.25

Abstract

We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multi-sorted binding signature, say Σ. First, we provide sufficient criteria for Σ to generate a language of possibly infinite terms, through ω-continuity. Second, we construct a monadic substitution operation for the language generated by Σ. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution. The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • Non-wellfounded syntax
  • Substitution
  • Monoidal categories
  • Actegories
  • Tensorial strength
  • Proof assistant Coq
  • UniMath library

Metrics

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

Related Versions

References

  1. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in homotopy type theory. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland, volume 38 of LIPIcs, pages 17-30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.17.
  2. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular specification of monads through higher-order presentations. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 6:1-6:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.6.
  3. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Reduction monads and their signatures. Proc. ACM Program. Lang., 4(POPL):31:1-31:29, 2020. URL: https://doi.org/10.1145/3371099.
  4. Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg. From signatures to monads in UniMath. J. Autom. Reason., 63(2):285-318, 2019. URL: https://doi.org/10.1007/s10817-018-9474-4.
  5. Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg. Implementing a category-theoretic framework for typed abstract syntax. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 307-323. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503678.
  6. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program., 31:e22, 2021. URL: https://doi.org/10.1017/S0956796820000076.
  7. 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: https://doi.org/10.1007/3-540-48168-0_32.
  8. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. URL: http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types.
  9. Henning Basold. Mixed Inductive-Coinductive Reasoning - Types, Programs and Logic. PhD thesis, Radboud University, Nijmegen, The Netherlands, 2018. URL: https://repository.ubn.ru.nl/handle/2066/190323.
  10. Richard Bird and Lambert Meertens. Nested Datatypes. In Johan Jeuring, editor, Mathematics of Program Construction, MPC'98, Proceedings, volume 1422 of Lecture Notes in Computer Science, pages 52-67. Springer, 1998. Google Scholar
  11. Richard S. Bird and Ross Paterson. De Bruijn Notation as a Nested Datatype. J. Funct. Program., 9(1):77-91, 1999. URL: http://journals.cambridge.org/action/displayAbstract?aid=44239, URL: https://doi.org/10.1017/S0956796899003366.
  12. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as bounded natural functors. Proc. ACM Program. Lang., 3(POPL):22:1-22:34, 2019. URL: https://doi.org/10.1145/3290335.
  13. Peio Borthelle, Tom Hirschowitz, and Ambroise Lafont. A cellular Howe theorem. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 273-286. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394738.
  14. Matteo Capucci and Bruno Gavranović. Actegories for the working amthematician, 2022. URL: https://doi.org/10.48550/arXiv.2203.16351.
  15. Marcelo Fiore and Dmitrij Szamozvancev. Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang., 6(POPL):1-29, 2022. URL: https://doi.org/10.1145/3498715.
  16. 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: https://doi.org/10.1109/LICS.2008.38.
  17. 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. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782615.
  18. André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, and Marco Maggesi. Variable binding and substitution for (nameless) dummies. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 389-408. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_20.
  19. Chung-Kil Hur. Categorical equational systems : algebraic models and equational reasoning. PhD thesis, University of Cambridge, UK, 2010. URL: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.608664.
  20. Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Nominal coalgebraic data types with applications to lambda calculus. Log. Methods Comput. Sci., 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:20)2013.
  21. Thomas Lamiaux and Benedikt Ahrens. An introduction to different approaches to initial semantics, 2024. URL: https://arxiv.org/abs/2401.09366.
  22. Ralph Matthes and Tarmo Uustalu. Substitution in non-wellfounded syntax with variable binding. Theoretical Computer Science, 327(1-2):155-174, 2004. URL: https://doi.org/10.1016/j.tcs.2004.07.025.
  23. Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for non-wellfounded syntax with binders through monoidal categories. CoRR, abs/2308.05485, 2023. https://doi.org/10.48550/arXiv.2308.05485, minimally version 3.
  24. Paul-André Melliès. Higher-order parity automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005077.
  25. Stefan Milius. Completely iterative algebras and completely iterative monads. Inf. Comput., 196(1):1-41, 2005. URL: https://doi.org/10.1016/j.ic.2004.05.003.
  26. Andrei Popescu. Nominal recursors as epi-recursors. Proc. ACM Program. Lang., 8(POPL):425-456, 2024. URL: https://doi.org/10.1145/3632857.
  27. José Espírito Santo, Ralph Matthes, and Luís Pinto. A coinductive approach to proof search through typed lambda-calculi. Ann. Pure Appl. Log., 172(10):103026, 2021. URL: https://doi.org/10.1016/j.apal.2021.103026.
  28. The Coq Development Team. The Coq proof assistant, version 8.17, 2023. URL: https://zenodo.org/record/8161141.
  29. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at http://unimath.github.io/UniMath/ , 2021.
  30. Julianna Zsidó. Typed Abstract Syntax. PhD thesis, University of Nice Sophia Antipolis, 2010. URL: http://tel.archives-ouvertes.fr/tel-00535944/.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact