Scott-Engeler models are a class of models for the untyped -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 law fails. However, an 'inequational variant' holds.
Let be a set of constants. We inductively define a set by the following rules:
In other words, the set is the least solution to . Because we use \emph{finite} powersets, this is an inductive definition and no domain theory is required.
Then the set is a model of the untyped -calculus.
Define an applicative structure on as follows:
This can then be turned into a reflexive cpo by defining
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},
}
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},
}
@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, 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}
}
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}
}
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}
}