Document Open Access Logo

Abstract Clones for Abstract Syntax

Authors Nathanael Arkor , Dylan McDermott

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2021.30.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Higher order logic
  • Theory of computation → Proof theory
Keywords
  • simple type theories
  • abstract clones
  • second-order abstract syntax
  • substitution
  • variable binding
  • presentations
  • free algebras
  • induction
  • logical relations

Metrics

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

Abstract

We give a formal treatment of simple type theories, such as the simply-typed λ-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed λ-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β- and η-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.

Cite As Get BibTex

Nathanael Arkor and Dylan McDermott. Abstract Clones for Abstract Syntax. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.30

Author Details

Nathanael Arkor
  • University of Cambridge, UK
Dylan McDermott
  • Reykjavik University, Iceland

Funding

  • McDermott, Dylan: Icelandic Research Fund project grant numero 196323-053.

References

  1. Peter Aczel. A general Church-Rosser theorem. Unpublished manuscript, 1978. Google Scholar
  2. Benedikt Ahrens. Modules over relative monads for syntax and semantics. Mathematical Structures in Computer Science, 26(1):3-37, 2016. URL: https://doi.org/10.1017/S0960129514000103.
  3. 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), volume 131, pages 1-16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.6.
  4. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. In Foundations of Software Science and Computational Structures, pages 297-311. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_21.
  5. Nathanael Arkor and Marcelo Fiore. Algebraic models of simple type theories: a polynomial approach. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, page 88–101. Association for Computing Machinery, 2020. URL: https://doi.org/10.1145/3373718.3394771.
  6. Nathanael Arkor and Dylan McDermott. Higher-order algebraic theories. Preprint, 2020. URL: https://www.cl.cam.ac.uk/~na412/Higher-order%20algebraic%20theories.pdf.
  7. Michael Barr. Exact categories. In Exact categories and categories of sheaves, pages 1-120. Springer, 1971. Google Scholar
  8. Garrett Birkhoff. On the structure of abstract algebras. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 31, pages 433-454. Cambridge University Press, 1935. URL: https://doi.org/10.1017/S0305004100013463.
  9. Garrett Birkhoff and John D Lipson. Heterogeneous algebras. Journal of Combinatorial Theory, 8(1):115-133, 1970. URL: https://doi.org/10.1016/S0021-9800(70)80014-X.
  10. Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 26-37. Association for Computing Machinery, 2002. URL: https://doi.org/10.1145/571157.571161.
  11. Marcelo Fiore. Second-order and dependently-sorted abstract syntax. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, pages 57-68. IEEE, 2008. URL: https://doi.org/10.1109/LICS.2008.38.
  12. Marcelo Fiore and Makoto Hamana. Multiversal polymorphic algebraic theories: syntax, semantics, translations, and equational logic. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 520-529. IEEE, 2013. URL: https://doi.org/10.1109/LICS.2013.59.
  13. Marcelo Fiore and Chung-Kil Hur. Second-order equational logic. In Computer Science Logic, pages 320-335. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_26.
  14. Marcelo Fiore and Ola Mahmoud. Second-order algebraic theories. In Mathematical Foundations of Computer Science, pages 368-380. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15155-2_33.
  15. Marcelo Fiore and Ola Mahmoud. Functorial semantics of second-order algebraic theories, 2014. URL: http://arxiv.org/abs/1401.4697.
  16. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 193-202. IEEE, 1999. URL: https://doi.org/10.1109/LICS.1999.782615.
  17. Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307-334, 1985. Google Scholar
  18. Makoto Hamana. Free σ-monoids: A higher-order syntax with metavariables. In Asian Symposium on Programming Languages and Systems, pages 348-363. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30477-7_23.
  19. André Hirschowitz, Tom Hirschowitz, and Ambroise Lafont. Modules over monads and operational semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167, pages 12-1. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.12.
  20. André Hirschowitz and Marco Maggesi. Modules over monads and linearity. In Logic, Language, Information, and Computation, pages 218-237. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73445-1_16.
  21. André Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Information and Computation, 208(5):545-564, 2010. URL: https://doi.org/10.1016/j.ic.2009.07.003.
  22. Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 204-213. IEEE, 1999. URL: https://doi.org/10.1109/LICS.1999.782616.
  23. Mathieu Huot. Operads with algebraic structure. MPRI Internship Report, 2016. URL: http://users.ox.ac.uk/~scro3639/M1_Report.pdf.
  24. J.M.E. Hyland. Classical lambda calculus in modern dress. Mathematical Structures in Computer Science, 27(5):762–781, 2017. URL: https://doi.org/10.1017/S0960129515000377.
  25. J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 88, pages 205-232. Cambridge University Press, 1980. URL: https://doi.org/10.1017/S0305004100057534.
  26. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, 1999. Google Scholar
  27. Achim Jung and Jerzy Tiuryn. A new characterization of lambda definability. In Typed Lambda Calculi and Applications, pages 245-257. Springer, 1993. URL: https://doi.org/10.1007/BFb0037110.
  28. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1988. Google Scholar
  29. F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(5):869-872, 1963. URL: https://doi.org/10.1073/pnas.50.5.869.
  30. Daniel J. Lehmann and Michael B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical systems theory, 14(1):97-139, 1981. URL: https://doi.org/10.1007/BF01752392.
  31. F.E.J. Linton. An outline of functorial semantics. In Seminar on Triples and Categorical Homology Theory, pages 7-52. Springer, 1969. URL: https://doi.org/10.1007/BFb0083080.
  32. Ola Mahmoud. Second-order algebraic theories. Technical Report UCAM-CL-TR-807, University of Cambridge, Computer Laboratory, 2011. URL: https://doi.org/10.48456/tr-807.
  33. Claudio Pisani. Sequential multicategories. Theory and Applications of Categories, 29(19):496-541, 2014. URL: http://www.tac.mta.ca/tac/volumes/29/19/29-19abs.html.
  34. Andrew M. Pitts. Tripos theory in retrospect. Mathematical structures in computer science, 12(3):265-279, 2002. URL: https://doi.org/10.1017/S096012950200364X.
  35. Miki Tanaka. Abstract syntax and variable binding for linear binders. In Mathematical Foundations of Computer Science, pages 670-679. Springer, 2000. URL: https://doi.org/10.1007/3-540-44612-5_62.
  36. Walter Taylor. Abstract clone theory. In Algebras and orders, volume 389 of NATO ASI Series C, pages 507-530. Springer, 1993. URL: https://doi.org/10.1007/978-94-017-0697-1_11.
  37. Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-matching. PhD thesis, Carnegie Mellon University, 2009. Google Scholar
  38. Julianna Zsidó. Typed abstract syntax. PhD thesis, Université Nice Sophia Antipolis, 2010. Google Scholar
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