Type theories, normal forms, and \(D_{\infty}\)-lambda-models (Q1102936)

The study of a special filter model for the \(\lambda\)-calculus (in the sense of H. Barendregt), denoted \({\mathcal F}^*\), is the main objective of this paper. The type assignement system, on which the definition of \({\mathcal F}^*\) is based, is the classical Curry's type assignement to which \(\omega\) (the universal type), the operator \(\Lambda\) (intersection) - for type formation, and an ``inclusion'' relation on types are added. Much more, the initial set of atomic types is a two- element set. It is proved that \({\mathcal F}^*\) is isomorphic with an inverse limit space \(D^*_{\infty}\) constructed from a (three point) lattice with a nonstandard initial projection, which is not (Hilbert- Post) complete. A nice characterization (the first purely semantic one?) for a term to be normalizable is also given.