Models and theories of lambda calculus
Giulio Manzonetto (INRIA Rocquencourt)
TL;DR
This paper summarizes Manzonetto's PhD thesis on denotational semantics and equational theories of untyped lambda calculus, introducing new models, representation theorems, and limitations of effective lambda-models.
Contribution
It presents a general construction of lambda-models from reflexive objects, a Stone-style representation theorem, and proves limitations on effective lambda-models' equational theories.
Findings
Constructed lambda-models from reflexive objects in categories
Proved a Stone-style representation theorem for combinatory algebras
Showed no effective lambda-model can have lambda-beta or lambda-beta-eta as its equational theory
Abstract
In this paper we briefly summarize the contents of Manzonetto's PhD thesis which concerns denotational semantics and equational/order theories of the pure untyped lambda-calculus. The main research achievements include: (i) a general construction of lambda-models from reflexive objects in (possibly non-well-pointed) categories; (ii) a Stone-style representation theorem for combinatory algebras; (iii) a proof that no effective lambda-model can have lambda-beta or lambda-beta-eta as its equational theory (this can be seen as a partial answer to an open problem introduced by Honsell-Ronchi Della Rocca in 1984).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.