zbMATH — the first resource for mathematics

Polymorphism is not set-theoretic. (English) Zbl 0554.03012
Semantics of data types, Proc. int. Symp., Sophia-Antipolis/France 1984, Lect. Notes Comput. Sci. 173, 145-156 (1984).
[For the entire collection see Zbl 0534.00019.]
The polymorphic or second order typed lambda calculus is an extension of the typed lambda calculus, involving abstraction over typed variables, in which polymorphic (i.e. multityped) functions can be defined. The author had conjectured that the standard set theoretic model of the ordinary typed lambda calculus might be extended to a model of the polymorphic system by restricting polymorphic functions to ”parametric polymorphism” in the sense of Strachy. He shows in this paper that, independently of the particular definition of ”parametric”, the existence of a set theoretic model leads to the isomorphism of sets P and \((P\to B)\to B.\) Because of the differing cardinalities of these sets, this is impossible, so no such model exists. The paper contains a clear outline of the syntax of the polymorphic typed, lambda calculus as well as a clear list of conditions any such set theoretic model is assumed to satisfy.
Reviewer: M.W.Bunder

03B40 Combinatory logic and lambda calculus
03C55 Set-theoretic model theory
03C65 Models of other mathematical theories