[Prev][Next][Index][Thread]
query: models of CIC
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
Hi Milad,
> Is there a realizability semantics or set theoretical model known for
> CIC (i.e. Calculus of Inductive Contrsuctions, the underlying type
> theory of Coq proof assistant)? In CIC we have two impredicative
> universes,Prop and Set and a cumulative hierarchy of Type_0, Type_1, ...
> on top of them. Moreover we have (dependent) inductive types both on the
> predicative and the impredicative level and we have dependent
> elimination on Set (which is stronger than the one for Prop).
I am not sure what you mean by a "set theoretic model": there is an
old result by Reynolds which shows that there are no non-trivial
set-theoritic models of impredicativity (in classical set theory).
As far as realizability goes: omega-sets (and related models called
D-sets by Thomas Streicher) provide models for CIC and similar
calculi. Basically the idea is that a Type is modelled by an omega-set
(X,||-_X) where X is a set and ||-_X a relation between the natural
numbers (hence omega) and X s.t. forall x in X there is a number i
s.t. i ||-_X x. i is called the realizer of x. Given omega-sets
(X,||-_X) and (Y,||-_Y) the omega-set of functions is given by those
set-theoretic functions which are tracked by a recursive function
(which again can be encoded as a number) giving rise to a new relation
||-_X->Y. To be precise
({f : X-> Y | Ex m. m ||-X->Y f,
m ||-_X->Y f iff Forall i,x.i||- x -> {m}i ||- f(x))
This can be extended to dependent function spaces (Pi-type), Sigma
types and it is easy to see that omega-sets support inductive types
such as Natural Numbers and W-types. To construct an impredicative
universe one observes that the subcategory of modest omega-sets
(where the ||- relation is injective) provide a good interpretation
fro Prop.
To model the hierarchy of Type-universes one seems to need
inaccessible cardinals.
There are a lot of (old) references to this, w-sets (or D-sets) are
the main topic of Thomas Streichers PhD and book (Semantics of Type
Theory, Birkhaeuser, 1991). Zhaohui Luo extended this in his PhD to
ECC. I used a variant - lambda sets - in my own PhD to show strong
normalisation also covering inductive types. There is much more...
Provaktive question: why does one need an impredicative universe?
Cheers,
Thorsten
Follow-Ups: