Intersection types and domain operators (Q1434348)

Intersection types are a very powerful type language which allows us to describe interesting computational properties of \(\lambda\)-terms. For instance, they have been used to give type characterizations of strongly normalising terms and (persistently) normalising terms. The models of lambda calculus built out of intersection types, the so-called filter models of lambda calculus, are also useful to provide semantic proofs of consistency of lambda theories. In this paper, the authors deal with the issue of easiness proofs of \(\lambda\)-terms from the semantic point of view (we recall that a closed term \(e\) is easy if, for any other closed term \(t\), the lambda theory generated by the equation \(e = t\) is consistent). The main tool used by the authors is the notion of simple easiness, which turns out to be stronger than easiness and allows the authors to prove consistency results via construction of suitable filter models. In the main result of the paper, the authors show that, for every simple easy term \(e\) and continuous predicate \(P\), there is a filter model, where the simple easy term \(e\) is interpreted as the filter induced by \(P\). The authors provide the following two applications of the main theorem: For any simple easy term, there is a filter model, where the interpretation of the term is the join operator. For any simple easy term, there is a filter model, where the interpretation of the term is the minimal fixed point operator. The first result has been used by \textit{S. Lusin} and \textit{A. Salibra} [``The lattice of lambda theories'', J. Log. Comput. 14, No. 3, 373--394 (2004; Zbl 1057.03011)] to show that there exists a sublattice of the lattice of lambda theories satisfying interesting algebraic properties.