Combinatory logic and lambda calculus are equal, algebraically

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

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.

Citation

Altenkirch, T., Kaposi, A., Šinkarovs, A., & Végh, T. (2023). Combinatory logic and lambda calculus are equal, algebraically. LIPIcs, Article 24

• Presentation Conference Type: Conference Paper (published)
• Conference Name: FSCD
• Acceptance Date: Apr 13, 2023
• Online Publication Date: Jun 28, 2023
• Publication Date: 2023
• Deposit Date: Jun 8, 2023
• Publicly Available Date: Jun 29, 2023
• Journal: LIPIcs
• Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
• Peer Reviewed: Peer Reviewed
• Article Number: 24
• Public URL: https://nottingham-repository.worktribe.com/output/21641221
• Publisher URL: https://drops.dagstuhl.de/opus/volltexte/2023/18008/
• Related Public URLs: https://easyconferences.eu/fscd2023/