Scott-Engeler models

Scott-Engeler models are a class of models for the untyped \lambda-calculus. They were introduced in Scott 1980, and then later generalised by Engeler 1981 and others.

Scott 1980, §5 and Plotkin 1993, §4 give a technical argument that in all Scott-Engeler models the the \eta law fails. However, an 'inequational variant' M \subseteq \lambda x. M(x) holds.

Definition

Let A be a set of constants. We inductively define a set D_A by the following rules:

\frac{
  a \in A
}{
  c \in D
}
\qquad
\frac{
  S \in \mathcal{P}_\text{fin}(D_A)
  \quad
  x \in D_A
}{
  (\beta, x) \in D_A
}

In other words, the set D_A is the least solution to D_A \cong A + \mathcal{P}_\text{fin}(D_A). Because we use \emph powersets, this is an inductive definition and no domain theory is required.

Then the set \mathcal{P}(D_A) is a model of the untyped \lambda-calculus.

Define an applicative structure on D_A as follows:

x \cdot y \triangleq
  \{ b \in B \mid \exists \beta \subseteq y.\ (\beta, b) \in x \}

This can then be turned into a reflexive cpo by defining

\begin{array}{lcl}
  F    & : &D_A \to [D_A \to D_A] \\
  F(x) & = &y \mapsto x \cdot y \\
  & & \\
  G    & : &[D_A \to D_A] \to D_A \\
  G(f) & = & \{ (\beta, b) \mid \beta \subseteq_\text{fin} B \land b \in f(\beta) \}
\end{array}

References

The very first Scott-Engeler model was developed in a very chatty and interesting paper by Dana Scott:

Scott, Dana. ‘Lambda Calculus: Some Models, Some Philosophy’. In The Kleene Symposium, 223–65. Studies in Logic and the Foundations of Mathematics 101. Elsevier, 1980. https://doi.org/10.1016/S0049-237X(08)71262-X. pdf

@incollection{scott_1980,
	title = {Lambda Calculus: Some Models, Some Philosophy},
	series = {Studies in Logic and the Foundations of Mathematics},
	pages = {223--265},
	number = {101},
	booktitle = {The Kleene Symposium},
	publisher = {Elsevier},
	author = {Scott, Dana},
	date = {1980},
	doi = {10.1016/S0049-237X(08)71262-X},
}

A review article on webbed models, which contains significant intuitions on Scott-Engeler models is

Berline, Chantal. ‘From Computation to Foundations via Functions and Application: The λ-Calculus and Its Webbed Models’. Theoretical Computer Science 249, no. 1 (2000): 81–161. https://doi.org/10.1016/S0304-3975(00)00057-8.

@article{berline_computation_2000,
	title = {From computation to foundations via functions and application: The λ-calculus and its webbed models},
	volume = {249},
	doi = {10.1016/S0304-3975(00)00057-8},
	pages = {81--161},
	number = {1},
	journaltitle = {Theoretical Computer Science},
	author = {Berline, Chantal},
	date = {2000},
	file = {Berline - 2000 - From computation to foundations via functions and .pdf:C\:\\Users\\Alex\\Zotero\\storage\\C37KG97R\\Berline - 2000 - From computation to foundations via functions and .pdf:application/pdf},
}

A review article whose second part contains a wealth of information and references to Scott-Engeler models is

@article{plotkin_1993,
	title = {Set-theoretical and other elementary models of the λ-calculus},
	volume = {121},
	doi = {10.1016/0304-3975(93)90094-A},
	pages = {351--409},
	number = {1},
	journaltitle = {Theoretical Computer Science},
	author = {Plotkin, Gordon D.},
	date = {1993},
}

Engeler models were introduced in

Engeler, Erwin. 1981. ‘Algebras and Combinators’. Algebra Universalis 13 (1): 389–92. https://doi.org/10.1007/BF02483849.

@article{engeler_1981,
	title = {Algebras and combinators},
	volume = {13},
	doi = {10.1007/BF02483849},
	number = {1},
	journal = {Algebra Universalis},
	author = {Engeler, Erwin},
	year = {1981},
	pages = {389--392}
}

Another article is

Longo, Giuseppe. 1983. ‘Set-Theoretical Models of λ-Calculus: Theories, Expansions, Isomorphisms’. Annals of Pure and Applied Logic 24 (2): 153–88. https://doi.org/10.1016/0168-0072(83)90030-1.

@article{longo_1983,
	title = {Set-theoretical models of λ-calculus: theories, expansions, isomorphisms},
	volume = {24},
	doi = {10.1016/0168-0072(83)90030-1},
	number = {2},
	journal = {Annals of Pure and Applied Logic},
	author = {Longo, Giuseppe},
	year = {1983},
	pages = {153--188}
}

A very short account of an Engeler model for the untyped \lambda-calculus appears on pp. 106-107 of

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