TY - GEN

T1 - Categorical Completeness Results for the Simply-typed Lambda-calculus

AU - Simpson, Alex

PY - 1995

Y1 - 1995

N2 - 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.

AB - 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.

U2 - 10.1007/BFb0014068

DO - 10.1007/BFb0014068

M3 - Conference contribution

T3 - TLCA '95

SP - 414

EP - 427

BT - Proceedings of the Second International Conference on Typed Lambda Calculi and Applications

PB - Springer-Verlag GmbH

CY - London, UK, UK

ER -