Intersection types and domain operators

We use intersection types as a tool for obtaining lambda-models. Relying on the notion of easy intersection type theory, we successfully build a lambda-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the lambda-theory where the lambda-term (lambdax.xx)(lambdax.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of lambda-theories. The second result is that for any simple easy term, there is a lambda-model, where the interpretation of the term is the minimal fixed point operator. (C) 2004 Elsevier B.V. All rights reserved.