addendum to models of CIC

Thomas Streicher <streicher@mathematik.tu-darmstadt.de> · Tue, 28 Oct 2003 12:06:03 +0100 (CET)

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

concerning the question of models for ECC with inductive types I think the
following addenda to Thorsten's answer are in place:

In my Thesis I didn't deal with inductive types at all. Nevertheless it was
clear to me -- and, actually, a lot of other people working on semantics of 
type theory in that time -- that it is not a problem to give meaning to
inductive types in assemblies (as \omega-sets or D-sets are called nowadays).
The reason is quite easy. In assemblies one works as in Set up to the proviso
that one has to restrict to realizable elements. So the receipe is to construct
inductive types as usual but restrict to the realizable elements. E.g. for
W-types, whose elements are infinite tree or terms, the elements in Asm(K_1)
are just those trees which are effective (K_1 being numbers with Kleene 
application). 

I don't know of any systematic treatment of semantics of inductive types in
realizability models up to the following citations

(1) if I remember correctly in Thorsten's Thesis itself at least a few
    particular cases were dealt with

(2) there is the These of Benjamin Werner (presumably obtainable from his
    home page) devoted to CIC

(3) thre is a paper by Christian-Emil Ore (a student of D.Norman)

    Zbl 0784.03009 Ore, Christian-Emil
    The extended calculus of constructions (ECC) with inductive types. 
    Inf. Comput. 99, No.2, 231-264 (1992).

To my opinion the problem rather is to *fix* a syntactic notion of inductive 
type (which always will be incomplete) rather than to provide it with a 
semantics in assemblies. 

There is a general non-syntactic notion of inductive type as given by 
realizable endo-functors on PER(AA) that preserve coercion maps (those
realizable by identity). These induce monotone endomaps on the complete
poset (PER(AA),\subseteq) which by Knaster-Tarski do have a fixpoint. There
is a general argument showing that these guys coincide with the initial 
algebras of the functors (I have a little note on that which I can provide on
request). However, alas, from this general treatment it doesn't follow that 
these fixpoints are initial in the category of assemblies though in all 
interesting cases they are!

Best, Thomas