The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

         Hi Hendrik,

> 
> 
> Deep within the coq reference manual (Section 4.2, Typed Terms),
> I find the rule.
> 
> Prod: 
> 
>         E[G] |- T : Type(i)     E[G::(x:T)] |- U : Type(j)   i <= k   j <= k
>        -------------------------------------------------------------------
>                           E[G] |- (x:T)U : Type(k)
> 
> THe dependency of k on i surprised me.
> I had thought that coq would be based on the calculus of constructions
> (even the name coq = coc - coquand?) suggests that.
> But here I find a constraint that hearkens back to Martin-Lof's
> Intuitionistic Theory of Types.
> 
> Is this an error in the manual?
> Is this a historical accident?
> Or, as I fear, is there some deepseated reason why this impredicativity is
> forbidden?  Do we encounter inconsistency if we confront impredicativity
> with these lovely induction laws?  Or has no one happened to prove 
> consistency yet (of the CoC with all the inductions)?

Let me try to make a long story short.

The formalism implemented in Coq is an extension of the original
CoC. This extension is generaly called CIC (calculus of Inductive
Constructions) and is the fruit of a evolution parallel with the
successive implementations.

In CoC you have two sorts, say Set and Type. You have Set : Type, and
Set is impredicative.

additional features of Coq's formalism are:

* Prop, which is a twin sort of Set, also impredicative and also of
type Type.

* A hierarchy of predicative sorts Type is replaced by Type(1) :
Type(2) : Types(3) ...

these sorts have to be predicative since they live ABOVE an
impredicative sort. They are closely related to Martin-Lof's
universes. So Coq can be viewed as pasting together ML and CoC.


* primitive inductive types (in CoC you have to encode these through
Church numerals' style encoding).


* primitive co-inductive types.


* a cumulativity between the universes (if A:Type(i), then A :
Type(i+1))



Since the expressive power of the formalism is very strong, the known
models generaly require inaccessible ordinals. There are not too many
papers on the topic, since these consistency proofs are very
tedious. You can have, among others, a look at my TACS'97 paper (LNCS
1281, simple model for a large fragment of Coq), at Alexandre
Miquel's paper accepted to the forthcoming LICS as well as at work of
Healf Goguen and Thorsten Altenkirch.


Cheers,


Benjamin