TY - GEN
T1 - Combinatory Logic and Lambda Calculus Are Equal, Algebraically
AU - Altenkirch, Thorsten
AU - Kaposi, Ambrus
AU - Šinkarovs, Artjoms
AU - Végh, Tamás
N1 - Funding Information:
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. Artjoms Šinkarovs: Supported by the Engineering and Physical Sciences Research Council through the grant EP/N028201/1.
Publisher Copyright:
© Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh.
PY - 2023/6/28
Y1 - 2023/6/28
N2 - 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.
AB - 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.
KW - Combinatory logic
KW - Cubical Agda
KW - lambda calculus
KW - quotient inductive types
UR - http://www.scopus.com/inward/record.url?scp=85166014566&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2023.24
DO - 10.4230/LIPIcs.FSCD.2023.24
M3 - Conference contribution
AN - SCOPUS:85166014566
T3 - Leibniz International Proceedings in Informatics
BT - 8th International Conference on Formal Structures for Computation and Deduction 2023
A2 - Gaboardi, Marco
A2 - van Raamsdonk, Femke
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
T2 - 8th International Conference on Formal Structures for Computation and Deduction 2023
Y2 - 3 July 2023 through 6 July 2023
ER -