Combinatory Logic and Lambda Calculus Are Equal, Algebraically

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

29 Downloads (Pure)

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.

Original languageEnglish
Title of host publication8th International Conference on Formal Structures for Computation and Deduction 2023
EditorsMarco Gaboardi, Femke van Raamsdonk
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
ISBN (Electronic)9783959772778
DOIs
Publication statusPublished - 28 Jun 2023
Event8th International Conference on Formal Structures for Computation and Deduction 2023 - Rome, Italy
Duration: 3 Jul 20236 Jul 2023

Publication series

NameLeibniz International Proceedings in Informatics
Volume260
ISSN (Print)1868-8969

Conference

Conference8th International Conference on Formal Structures for Computation and Deduction 2023
Abbreviated titleFSCD 2023
Country/TerritoryItaly
CityRome
Period3/07/236/07/23

Keywords

  • Combinatory logic
  • Cubical Agda
  • lambda calculus
  • quotient inductive types

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Combinatory Logic and Lambda Calculus Are Equal, Algebraically'. Together they form a unique fingerprint.

Cite this