D_\infty

D_\infty is a domain-theoretic recipe for constructing a model of the untyped lambda calculus given a complete partial order (D, \sqsubseteq) with at least two elements.

Description of the construction

Please expand.

Induced theory

D_\infty models induce an equational theory in the standard way, by defining

D_\infty \vDash M = N
\quad\triangleq\quad
\llbracket M \rrbracket = \llbracket N \rrbracket

where \llbracket M \rrbracket is the interpretation of a term in D_\infty. This theory is sometimes called the local structure of D_\infty.

Hyland and Wadsworth proved that if we begin the construction from a cpo D with a least element \bot, and a canonical embedding-projection pair, this theory is independent of D. Moreover, it relates to solvability.

Theorem (Hyland and Wadsworth). Constructing D_\infty from the embedding-projection pair

\begin{array}{cccccc}
  e &:& D &\to     & [D \to D] \\
  e &\triangleq& d &\mapsto & (\_ \mapsto d)
\end{array}
\qquad
\begin{array}{cccccc}
  p &:& [D \to D] &\to     & D \\
  p &\triangleq& f & \to & f(\bot)
\end{array}

we have that

  D_\infty \vDash M = N
    \quad\Longleftrightarrow\quad
  \forall C[-].\ (C[M] \text{ solvable} \Leftrightarrow C[N] \text{ solvable})

A textbook proof of this theorem may be found in Barendregt 1984, Theorem 19.2.9.

References

• A textbook presentation of D_\infty as well as many theorems relating to it may be found in the classic textbook

@book{barendregt_1984,
	address = {Amsterdam},
	title = {Lambda {Calculus}: {Its} {Syntax} and {Semantics}},
	isbn = {978-0-444-87508-2},
	publisher = {North-Holland},
	author = {Barendregt, Henk},
	year = {1984}
}