The untyped -calculus admits a class of models known as graph models. This refers not to the combinatorial notion of graph, but to the graph of a function, i.e. the set of input-output pairs. They are more general than Scott-Engeler models.
Graph models never satisfy the rule [Plotkin 1993, Berline 2000].
A general definition of what a graph model is can be given through Scott-Engeler algebras (SE algebras). An SE algebra consists of a set and a function
An SE algebra is extensional just if is an injection.
The map allows us to uniquely encode a finite subset of and an element as a single element of . The idea is that seeing the finite amount of information in in our input suffices to issue as an output.
The -calculus will then be interpreted in the structure
Each function will be mapped to the set of its 'finite approximants' of the form . We can then define an applicative structure by
Plotkin, Gordon D. ‘Set-Theoretical and Other Elementary Models of the λ-Calculus’. Theoretical Computer Science 121, no. 1–2 (1993): 351–409. https://doi.org/10.1016/0304-3975(93)90094-A. [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},
}
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_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},
}