THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
Combinatory logic and lambda calculus are equal, algebraically
Altenkirch, Thorsten; Kaposi, Ambrus; Šinkarovs, Artjoms; Végh, Tamás
Authors
Ambrus Kaposi
Artjoms Šinkarovs
Tamás Végh
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/ |
Files
LIPIcs-FSCD-2023-24
(704 Kb)
PDF
Publisher Licence URL
https://creativecommons.org/licenses/by/4.0/
You might also like
Monads need not be endofunctors
(2015)
Journal Article
Type theory in type theory using quotient inductive types
(2016)
Presentation / Conference Contribution
Normalisation by evaluation for dependent types
(2016)
Presentation / Conference Contribution
Notions of anonymous existence in Martin-Löf type theory
(2017)
Journal Article
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
(2017)
Presentation / Conference Contribution
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search