Type theories, normal forms, and D∞-lambda-models

A (non-standard) inverse-limit λ-model D∞ ∗ is constructed which has a non Hilbert-Post complete theory. Moreover, in D∞ ∗, a simple semantic characterization of normalizable terms is given. These results are proved using the properties of a generalized type assignment system which yields a filter model (Barendregt, Coppo, and Dezani-Ciancaglini, 1983, J. Symbolic. Logic, 48, 931–940; Coppo, Dezani-Ciancaglini, Honsell, and Longo, 1983, pp. 241–262, “Logic Colloquium '82, ” North-Holland, Amsterdam), isomorphic to D∞ ∗. The type assignment system is also proved complete with respect to an interpretation of types (in the term model of β-equality) based only on normalization properties. As an application a class of maximal monoids of normalizable terms is characterized.

Authors

• M. Coppo
• M. Dezani-Ciancaglini
• M. Zacchi

Keywords

No keywords are indexed for this paper.