Graph models of untyped \lambda-calculus

The untyped \lambda-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 \eta rule Plotkin 1993, Berline 2000.

Definition

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 D and a function

i : \mathcal{P}_\text{fin}(D) \times D \to D

An SE algebra is extensional just if i is an injection.

The map i allows us to uniquely encode a finite subset S \subseteq_\text{fin} D of D and an element x \in D as a single element i(D, x) of D. The idea is that seeing the finite amount of information in S in our input suffices to issue x as an output.

The \lambda-calculus will then be interpreted in the structure

(P(D), \subseteq)

Each function will be mapped to the set of its 'finite approximants' of the form i(S, x). We can then define an applicative structure \cdot : \mathcal{P}(D) \times \mathcal{P}(D) \to \mathcal{P}(D) by

f \cdot x \triangleq
  \{ y \mid \exists S \subseteq_\text{fin} x.\ i(S, y) \in f \}

Examples

• \mathcal{P}\omega
• Scott-Engeler models are essentially graph models where i is an inclusion.

References

• A review article:

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

• A review article on webbed models of untyped \lambda-calculus, which include graph models, is

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