Wadsworth's theorem

In the context of the untyped \lambda-calculus, Wadsworth's theorem connects a certain kind of denotational model, namely the D_\infty model, with a certain kind of reduction, namely head reduction. It is an early form of an adequacy result.

Statement

Consider the D_\infty model of the untyped \lambda-calculus.

Consider the notion of head reduction.

Wadsworth's theorem. An untyped term M has a head normal form iff \llbracket M \rrbracket \neq \bot.

Intuition

For simplicity, costruct D_\infty by taking the base domain D to be the Sierpinski domain \Sigma = \{ \bot \sqsubseteq \top \}. Intuitively, this domain is a flat cpo which only models termination: \bot stands for a term that loops forever, while \top stands for a computation that somehow observably terminates.

Then, the theorem says that head reduction terminates iff the term is interpreted by \top in \Sigma_\infty.

References

• Wadsworth's theorem appears in Barendregt's textbook as Theorem 19.2.4:

@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}
}