new results on polymorphism
What follows is an abstract that I sent to the Americal Mathematical Society
in March and that will appear in the August 1988 issue of "Abstracts of the
Americal Mathematical Society". It summarizes some new results that I have
found on the second order polymorphic lambda calculus. I hope to have an
extended abstract ready in a few weeks and would be glad to send it to those
UNIVERSE MODELS AND INITIAL MODEL SEMANTICS FOR THE
SECOND ORDER POLYMORPHIC LAMBDA CALCULUS
SRI and CSLI
We propose a general notion of model of a second order polymorphic lambda
calculus (lambda-2) theory that provides a direct correspondence with semantic
intuitions lacking in R. Seely's PL categories (JSL, 52, 969-989).
DEFINITION. A universe is a pair (C,U) with C a locally cartesian closed
category (lccc) and U an internal full subcategory that is cartesian closed
and closed under (greek) PI; a universe model for a lambda-2 theory T is an
interpretation of the syntax of T in a universe such that the axioms of T are
satisfied; this generalizes the topos models of A. Pitts (in Proc. Conf. on
Category Theory and Computer Science, Edinburgh, 1987).
THEOREM. For any lccc C there is an elementary topos T[C] and a full and
faithful lccc universal map C -> T[C]; also, the Yoneda embedding
C -> Set^(C^op) is s a lccc map.
THEOREM. For any lambda-2 theory T there is a universe model I[T] that is
initial in the category of T models. I[T] has a full and faithful universal
homomorphism into an initial elementary topos universe model, and a full and
faithful (Yoneda) homomorphism into a presheaf universe model. A simple
direct construction of I[T] can be given as the term model of a Martin-Loef
theory extended with adequate reflection rules.
COMPLETENESS THEOREM. T proves an equation in lambda-2 logic iff I[T]
REMARK. Realizability topos models are an instance of universe models.