[Prev][Next][Index][Thread]
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
interested.
UNIVERSE MODELS AND INITIAL MODEL SEMANTICS FOR THE
SECOND ORDER POLYMORPHIC LAMBDA CALCULUS
J. Meseguer
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]
satisfies it.
REMARK. Realizability topos models are an instance of universe models.