A characterization of F-complete type assignments (Q1089331)

In some preceding works of the first author, an extension of the classical polymorphic type discipline for terms of the (untyped) \(\lambda\)-calculus is proposed. This is done by adding a constant type (\(\omega\)- the ''universal'' type) to the set of type variables, and a new operator (\(\Lambda\)- ''intersection'') for type formation. If D is the domain of a \(\lambda\)-model, then there exists a subset F of D whose elements are ''canonical'' representatives of functions. In the F-semantics of types, \(\sigma\to \tau\) is interpreted as a subset of F and \(\sigma\to \tau\) has then the intuitive meaning of ''the type of functions with domain \(\sigma\) and range \(\tau\) ''. This paper investigates the soundness and completeness of the intersection type discipline with respect to the F-semantics. The main theorem states that a type assignment is F-complete iff equal terms get equal types and, whenever M has a type \(\phi \Lambda \omega^ n\to \omega\) (\(\phi\) a type variable), the term \(\lambda z_ 1...z_ n.Mz_ 1...z_ n\) \((z_ i\), \(i=1...n\), do not occur free in M) has the type \(\phi\).