is a domain-theoretic recipe for constructing a model of the untyped lambda calculus given a complete partial order with at least two elements.
Please expand.
models induce an equational theory in the standard way, by defining
where is the interpretation of a term in . This theory is sometimes called the local structure of .
Hyland and Wadsworth proved that if we begin the construction from a cpo with a least element , and a canonical embedding-projection pair, this theory is independent of . Moreover, it relates to solvability.
Theorem (Hyland and Wadsworth). Constructing from the embedding-projection pair
we have that
A textbook proof of this theorem may be found in [Barendregt 1984, Theorem 19.2.9].
Barendregt, Henk. 1984. Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland. [link]
@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}
}