Set-theoretic Model of Simple Types

There is a simple set-theoretic model of simply-typed \lambda-calculus.

The model is given by the following translation:

every type A is mapped to a set \llbracket A \rrbracket
every context \Gamma is mapped to a set \llbracket \Gamma \rrbracket
every term \Gamma \vdash M : A is mapped to a function

  \llbracket \Gamma \vdash M : A \rrbracket
  : \llbracket \Gamma \rrbracket \to \llbracket A \rrbracket

The semantic function \llbracket - \rrbracket needs to take the entire typing derivation \Gamma \vdash M : A as an argument in order to uniquely define the meaning of a term. In other words, we only assign semantics to what is variably called typed terms, or terms-in-context. When we do not do this, we run into a coherence problem.

Description of the model

Type interpretation

Assume we have one base type b in the formal theory.

Furthermore, assume this is interpreted by some set X_b.

The interpretation is usually defined by

\begin{aligned}
  \llbracket b \rrbracket &= X_b \\
  \llbracket A \to B \rrbracket &= B^A = \{ f \mid f : \llbracket A \rrbracket \to \llbracket B \rrbracket \}
\end{aligned}

Context interpretation

Please expand.

Term interpretation

Please expand.

Soundness

Theorem. If \Gamma \vdash M = N : A then \llbracket \Gamma \vdash M : A \rrbracket = \llbracket \Gamma \vdash N : A \rrbracket.

History

The set-theoretic model of the simply-typed lambda-calculus seems to have first appeared in Friedman 1975.

Categorically

The construction of this model corresponds precisely to the fact that the category \textbf{Set} of sets and functions is cartesian closed.

The standard interpretation of simply-typed \lambda-calculus into cartesian closed categories then induces the above set-theoretic model.

Well-pointedness

When seen categorically, the set-theoretic model of the simply-typed \lambda-calculus has a somewhat desirable property, which is that it is well-pointed.

To explain what that means, suppose that a context consisting of one variable of type A is interpreted by a set S:

  \llbracket x : A \rrbracket = S

Then, suppose we have two terms x : A \vdash M : B and x : A \vdash N : B. When interpreted into the model, these become functions

\llbracket M \rrbracket, \llbracket N \rrbracket : S \to \llbracket B \rrbracket

(Contrary to good practice, we elide writing the entire judgement.)
We then have that whenever

\forall s \in S.\ \llbracket M \rrbracket(s) = \llbracket N \rrbracket(s)

it is the case that \llbracket M \rrbracket = \llbracket N \rrbracket. Thus, equality 'on points' suffices to induce equality of interpretations.

Completeness results

The model given above can be varied by changing the set X_b that interprets the base type. This generates an entire class of set-theoretic models.

This class of models is complete complete, in the sense that it precisely mirrors the \beta\eta equational theory of the calculus.

Theorem For any two \Gamma \vdash M, N : A, if \llbracket M \rrbracket = \llbracket N \rrbracket in the set-theoretic model based on X_b for all sets X_b, then \Gamma \vdash M = N : A.

The following authors have given completeness theorems:

Henkin 1950
If the base set X_b is infinite, then the class of models is complete Friedman 1975
Statman 1985

The above models cannot cover the case where X_b is empty. For those more complicated types of models are needed.

As a semantics of programming languages

In programming language terms, this model gives a simple set-theoretic denotational semantics for a programming language without recursion.

This basic model is very useful, and rather extensible. It can be extended to a denotational semantics of the language with recursion and/or recursive types using domain theory. Alternatively, it can be extended into a denotational semantics of effectful languages.

References

The first completeness proof for simply-typed \lambda-calculus seems to have appeared in

Henkin, Leon. 1950. ‘Completeness in the Theory of Types’. Journal of Symbolic Logic 15 (2): 81–91. https://doi.org/10.2307/2266967.

@article{henkin_1950,
	title = {Completeness in the theory of types},
	volume = {15},
	doi = {10.2307/2266967},
	number = {2},
	journal = {Journal of Symbolic Logic},
	author = {Henkin, Leon},
	year = {1950},
	pages = {81--91},
}

The first set-theoretic model of the simply-typed \lambda-calculus seems to have appeared in

Friedman, Harvey. 1975. ‘Equality between Functionals’. In Logic Colloquium, edited by Rohit Parikh, 453:22–37. Lecture Notes in Mathematics. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0064870.

@inproceedings{friedman_1975,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Mathematics}},
	title = {Equality between functionals},
	volume = {453},
	doi = {10.1007/BFb0064870},
	booktitle = {Logic {Colloquium}},
	publisher = {Springer Berlin Heidelberg},
	author = {Friedman, Harvey},
	editor = {Dold, A. and Eckmann, B. and Parikh, Rohit},
	year = {1975},
	pages = {22--37}
}

A 'revisited' version of Friedman's completeness theorem appears in

Statman, R. 1985. ‘Equality between Functionals Revisited’. In Harvey Friedman’s Research on the Foundations of Mathematics, edited by L. A. Harrington, M. D. Morley, A. Scedrov, and S. G. Simpson, 117:331–38. Studies in Logic and the Foundations of Mathematics. Elsevier. https://doi.org/10.1016/S0049-237X(09)70166-1.

@incollection{statman_1985,
	series = {Studies in {Logic} and the {Foundations} of {Mathematics}},
	title = {Equality between {Functionals} {Revisited}},
	volume = {117},
	booktitle = {Harvey {Friedman}'s {Research} on the {Foundations} of {Mathematics}},
	publisher = {Elsevier},
	author = {Statman, R.},
	editor = {Harrington, L. A. and Morley, M. D. and Scedrov, A. and Simpson, S. G.},
	year = {1985},
	doi = {10.1016/S0049-237X(09)70166-1},
	pages = {331--338}
}