2026-07-22T12:47:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18008 2024-03-06T11:00:51Z ddc:004 open_access

Combinatory Logic and Lambda Calculus Are Equal, Algebraically Altenkirch, Thorsten Kaposi, Ambrus Šinkarovs, Artjoms Végh, Tamás Combinatory logic lambda calculus quotient inductive types Cubical Agda 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thorsten Altenkirch and Ambrus Kaposi and Artjoms Šinkarovs and Tamás Végh 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.24 urn:nbn:de:0030-drops-180086 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.24 eng https://creativecommons.org/licenses/by/4.0/legalcode