D∞ models and intersection types
Roberto M. Amadio, Pierre-Louis Curien · Cambridge University Press eBooks · 1998
In this chapter we address the fundamental domain equation D = D → D which serves to define models of the untyped λ-calculus. By ‘equation’, we actually mean that we seek a D together with an order-isomorphism D ≅ D → D . Taking D = {⊥} certainly yields a solution, since there is exactly one function f : {⊥} → {⊥}. But we are interested in a non-trivial solution, that is a D of cardinality at least 2, so that not all λ-terms will be identified! Domain equations will be treated in a general setting in chapter 7. In section 3.1, we construct Scott's D ∞ models as order theoretical limit constructions. In section 3.2, we first define a general notion of λ-model, and then discuss some specific properties of the D ∞ models: Curry's fixpoint combinator is interpreted as the least fixpoint operator, and the theory induced by a D ∞ model can be characterized syntactically, using Böhm trees. In section 3.3, we present a class of λ-models based on the idea that the meaning of a term should be the collection of properties it satisfies in a suitable ‘logic’. This point of view will be developed in more generality in chapter 10. In section 3.4, we relate the constructions of sections 3.1 and 3.3, following [CDHL82]. Finally, in section 3.5, we use intersection types as a tool for the syntactic theory of the λ-calculus [Kri91, RdR93].