Lambda Galore

In the present paper we solve two open problems in the theory of λ-calculus and intersection type theories. In particular we prove that there exist models which equate all unsolvable terms, but nonetheless separate fixed point combinators, i.e. terms which have the same Böhm tree. Moreover we show how the results concerning recursive types in second-order λ-calculus for strong normalisation change significantly when head normalisation in untyped λ-calculus endowed with type assignment systems is considered. We achieve this by generalising intersection type theory to an algebraic framework of meet-semilattices, thereby assigning an algebraic notion to each applicative structure. In the style of algebraic topology we establish transfer results between the theories of the models capitalising on the morphisms between the corresponding meet-semilattices. This machinery permits also to yield a thorough analysis of the potential and the limitations of computability arguments.