There is a simple set-theoretic model of simply-typed -calculus.
The model is given by the following translation:
The semantic function needs to take the entire typing derivation 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.
Assume we have one base type in the formal theory.
Furthermore, assume this is interpreted by some set .
The interpretation is usually defined by
Please expand.
Please expand.
Theorem. If then .
The set-theoretic model of the simply-typed -calculus seems to have first appeared in [Friedman 1975].
The construction of this model corresponds precisely to the fact that the category of sets and functions is cartesian closed.
The standard interpretation of simply-typed -calculus into cartesian closed categories then induces the above set-theoretic model.
When seen categorically, the set-theoretic model of the simply-typed -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 is interpreted by a set :
Then, suppose we have two terms and . When interpreted into the model, these become functions
(Contrary to good practice, we elide writing the entire judgement.)
We then have that whenever
it is the case that . Thus, equality 'on points' suffices to induce equality of interpretations.
The model given above can be varied by changing the set 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 equational theory of the calculus.
Theorem For any two , if in the set-theoretic model based on for all sets , then .
The following authors have given completeness theorems:
The above models cannot cover the case where is empty. For those more complicated types of models are needed.
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.
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},
}
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}
}
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}
}