Recall the untyped \lambda calculus:

DefinitionUntyped \lambda -calculus [dt-004K]

• Liam O'Connor

Untyped \lambda -calculus consists only of untyped (higher-order) functions: e \; \Coloneqq \; x \mid \lambda x. e \mid e_1\ e_2

We mentioned before that the semantic domain of this language must be a cpo D such that D \simeq D\twoheadrightarrow D In other words, solutions to this equation are fixed points of \mathcal {F}(X) = X\twoheadrightarrow X. The least such fixed point can expressed, by Theorem [dt-005B], as the colimit of the \omega -chain:

But, the least solution to this equation is trivial: D_\infty \simeq \mathbf {1}, because \mathbf {1} \simeq \mathbf {1}\twoheadrightarrow \mathbf {1}. A non-trivial solution is obtained by starting the chain at \mathbf {2}, the cpo containing just \{\top ,\bot \}, rather than \mathbf {1}.

We will now sketch a proof of the retraction pair between D_\infty and D_\infty \twoheadrightarrow D_\infty , by providing two functions, \textbf {\textsf {up}} : D_\infty \rightarrow (D_\infty \twoheadrightarrow D_\infty ) and its inverse \textbf {\textsf {down}} : (D_\infty \twoheadrightarrow D_\infty ) \rightarrow D_\infty .

Observe that each element of D_i (for i > 0) is a function D_{i-1} \twoheadrightarrow D_{i-1}. Therefore, an element of the colimit D_\infty is an \omega -tuple of such functions. To define \textbf {\textsf {up}}(d)(x), we must essentially "apply" each function in the element d \in D_\infty (viewed as an \omega -tuple of functions) to the element x \in D_\infty (viewed as an \omega -tuple of values). More specifically, we say that \textbf {\textsf {up}}(d)(x) is an \omega -tuple (y_m \mid y \in \mathbb {N}), as follows: y_m = \bigsqcup _{k \in \mathbb {N}} \theta _{m+k,m}(d_{m+k+1}(x_{m+k})) To define \textbf {\textsf {down}}(f), we are given a (continuous) function f : D_\infty \twoheadrightarrow D_\infty and must construct the \omega -tuple of approximations at every D_n. We do this by projecting the action of f down to D_n. We say that \textbf {\textsf {down}}(f) is an \omega -tuple (v_n \mid n \in \mathbb {N}) where: \begin {array}{lcl} v_0 & \triangleq & \theta _{\infty ,0}(f(\theta _{0,\infty }(\bot _{D_0})))\\ v_{n+1} & \triangleq & \theta _{\infty ,n} \circ f \circ \theta _{n,\infty } \end {array}

DefinitionDenotations for untyped \lambda -calculus

• Liam O'Connor

Using the new functions \textbf {\textsf {up}} and \textbf {\textsf {down}}, it is now straightforward to define a semantics for untyped \lambda -calculus, where \sigma is an environment \mathsf {Var} \rightarrow D_\infty : \llbracket \cdot \rrbracket : (\mathsf {Var} \rightarrow D_\infty )\twoheadrightarrow D_\infty \begin {array}{lcl} \llbracket x \rrbracket \sigma & = & \sigma (x) \\ \llbracket e_0\ e_1 \rrbracket \sigma & = & \textbf {\textsf {up}}(\llbracket e_0 \rrbracket \sigma ) (\llbracket e_1 \rrbracket \sigma )\\ \llbracket \lambda x.\ e \rrbracket \sigma & = & \textbf {\textsf {down}}(\boldsymbol {\lambda } v \in D_{\infty }.\ \llbracket e \rrbracket \ \sigma (x \mapsto v) ) \end {array} This semantics does not distinguish non-terminating computations from terminating ones. To model call-by-value more faithfully, we could use the equation D \simeq D\twoheadrightarrow D_\bot instead, and for call-by-name we could use D \simeq D_\bot \twoheadrightarrow D_\bot . The constructions are very similar.