Suppose we have a language with recursive data types, such as this \mathit {List} type in Haskell-style syntax: \textbf {data}\ \mathit {List} = \mathsf {Nil} \mid \mathsf {Cons}\ (\mathit {Int} \times \mathit {List}) As in PCF, the denotation of a type \tau is the domain which contains all the denotations of all closed expressions of type \tau . What, then, is the domain that corresponds to \mathit {List}\ a? We need a cpo L that satisfies the below equation (where \mathbf {1} is the cpo containing just one element \bot ): L \simeq \mathbf {1} + (\mathbb {Z}_\bot \times L)

If we take PCF, discard the type system, \textbf {fix}, natural number primitives and any other superfluous features, and just boil our language down to a minimal, Turing-complete subset, we end up with the untyped \lambda -calculus — a language consisting only of untyped functions.

Trying to give a semantics to the untyped \lambda calculus poses an issue: we can no longer rely on the type of an expression to select an appropriate semantic domain. Instead, we we must pick a single domain D which, since functions can be applied to themselves, must apparently include the set of functions D \twoheadrightarrow D: D \simeq D\twoheadrightarrow D

This recursive equation for lists: L \simeq \mathbf {1} + (\mathbb {Z}_\bot \times L) Can be expressed as the least fixed point of this mapping (specifically an endofunctor) \mathcal {F} on cpos: \mathcal {F}(A) \triangleq \mathbf {1} + (\mathbb {Z}_\bot \times A)