Document Open Access Logo

Combinatory Logic and Lambda Calculus Are Equal, Algebraically

Authors Thorsten Altenkirch , Ambrus Kaposi , Artjoms Šinkarovs , Tamás Végh

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.24.pdf
  • Filesize: 0.67 MB
  • 19 pages

Document Identifiers

Author Details

Thorsten Altenkirch
  • School of Computer Science, University of Nottingham, UK
Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
Artjoms Šinkarovs
  • Heriot-Watt University, Edinburgh, UK
Tamás Végh
  • Eötvös Loránd University, Budapest, Hungary

Funding

The first two authors were supported by the "Application Domain Specific Highly Reliable IT Solutions" project which has been implemented with support from the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme.
  • Šinkarovs, Artjoms: Supported by the Engineering and Physical Sciences Research Council through the grant EP/N028201/1.

Cite AsGet BibTex

Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. Combinatory Logic and Lambda Calculus Are Equal, Algebraically. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 24:1-24:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.24

Abstract

It is well-known that extensional lambda calculus is equivalent to extensional combinatory logic. In this paper we describe a formalisation of this fact in Cubical Agda. The distinguishing features of our formalisation are the following: (i) Both languages are defined as generalised algebraic theories, the syntaxes are intrinsically typed and quotiented by conversion; we never mention preterms or break the quotients in our construction. (ii) Typing is a parameter, thus the un(i)typed and simply typed variants are special cases of the same proof. (iii) We define syntaxes as quotient inductive-inductive types (QIITs) in Cubical Agda; we prove the equivalence and (via univalence) the equality of these QIITs; we do not rely on any axioms, the conversion functions all compute and can be experimented with.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Combinatory logic
  • lambda calculus
  • quotient inductive types
  • Cubical Agda

Metrics

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

Supplementary Materials

References

  1. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by evaluation for dependent types. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 6:1-6:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.6.
  2. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  3. Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. The Münchhausen method and combinatory type theory. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes, 2022. URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_8.pdf.
  4. Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 56-65. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  5. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  6. Katalin Bimbó. Combinatory Logic: Pure, Applied and Typed. Taylor & Francis, 2011. Google Scholar
  7. Martin W. Bunder, J. Roger Hindley, and Jonathan P. Seldin. On adding ξ to weak equality in combinatory logic. J. Symb. Log., 54(2):590-607, 1989. URL: https://doi.org/10.2307/2274872.
  8. John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Log., 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  9. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. CoRR, abs/1904.00827, 2019. URL: https://arxiv.org/abs/1904.00827.
  10. Haskell B. Curry, Robert Feys, and William Craig. Combinatory logic, volume i. Philosophical Review, 68(4):548-550, 1959. URL: https://doi.org/10.2307/2182503.
  11. J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, USA, 2 edition, 2008. Google Scholar
  12. J. M. E. Hyland. Classical lambda calculus in modern dress. Math. Struct. Comput. Sci., 27(5):762-781, 2017. URL: https://doi.org/10.1017/S0960129515000377.
  13. Ambrus Kaposi. Formalisation of type checking into algebraic syntax. https://bitbucket.org/akaposi/tt-in-tt/src/master/Typecheck.agda, 2018.
  14. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, 2019. URL: https://doi.org/10.1145/3290315.
  15. András Kovács. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. PhD thesis, Eötvös Loránd University, Hungary, 2022. URL: https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf.
  16. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, USA, 1986. Google Scholar
  17. Conor McBride. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Bruno C. d. S. Oliveira and Marcin Zalewski, editors, Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2010, Baltimore, MD, USA, September 27-29, 2010, pages 1-12. ACM, 2010. URL: https://doi.org/10.1145/1863495.1863497.
  18. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
  19. Jonathan P. Seldin. The search for a reduction in combinatory logic equivalent to λβ-reduction. Theor. Comput. Sci., 412(37):4905-4918, 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.002.
  20. Jonathan P. Seldin. The search for a reduction in combinatory logic equivalent to λβ-reduction, part II. Theor. Comput. Sci., 663:34-58, 2017. URL: https://doi.org/10.1016/j.tcs.2016.12.016.
  21. Peter Selinger. The lambda calculus is algebraic. J. Funct. Program., 12(6):549-566, 2002. URL: https://doi.org/10.1017/S0956796801004294.
  22. Wouter Swierstra. A correct-by-construction conversion to combinators, 2021. https://webspace.science.uu.nl/ swier004/publications/2021-jfp-submission-2.pdf. URL: https://webspace.science.uu.nl/~swier004/publications/2021-jfp-submission-2.pdf.
  23. William W Tait. Variable-free formalization of the Curry-Howard Theory. In Twenty Five Years of Constructive Type Theory. Oxford University Press, October 1998. URL: https://doi.org/10.1093/oso/9780198501275.003.0016.
  24. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program., 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  25. Philip Wadler, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. August 2022. URL: https://plfa.inf.ed.ac.uk/22.08/.
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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact