Categorical Completeness Results for the Simply-typed Lambda-calculus

Alex Simpson

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


We investigate, in a categorical setting, some completeness properties of beta-eta conversion between closed terms of the simplytyped lambda calculus. A cartesian-closed category is said to be complete if, for any two unconvertible terms, there is some interpretation of the calculus in the category that distinguishes them. It is said to have a complete interpretation if there is some interpretation that equates only interconvertible terms. We give simple necessary and sufficient conditions on the category for each of the two forms of completeness to hold. The classic completeness results of, e.g., Friedman and Plotkin are immediate consequences. As another application, we derive a syntactic theorem of Statman characterizing beta-eta conversion as a maximum consistent congruence relation satisfying a property known as typical ambiguity.
Original languageEnglish
Title of host publicationProceedings of the Second International Conference on Typed Lambda Calculi and Applications
Place of PublicationLondon, UK, UK
PublisherSpringer-Verlag GmbH
Number of pages14
Publication statusPublished - 1995

Publication series

NameTLCA '95


Dive into the research topics of 'Categorical Completeness Results for the Simply-typed Lambda-calculus'. Together they form a unique fingerprint.

Cite this