The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

On Sat, Aug 9, 2014 at 2:26 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

When trying to define it the "usual" way, the clause for dependent function (PI) types is problematic.

In what sense?

Firstly, "the usual" was a poor choice of words on my part.

Dependent type theories are often presented directly as rules in a sequent calculus with contexts and typehood judgements.

I don't know if my comment is relevant for that style of definition.

My comment is relevant for a more semantic style along the lines of Stuart Allen.

He first assigns meanings to types and derives the rules from that meaning.

I'll first sketch an informal explanation of the problem when defining a core fragment of Nuprl

and then show some self-contained 

Coq code to more precisely show exactly 

where the strict positivity requirement of Coq's inductive types gets violated.

To define Nuprl, he first defined its terms and its computation system.

Intuitively, the type system can then be understood as two mutually inductive definitions. 

The first  one (type equality) defines

which terms denote equal types and the second one (term equality) defines which terms are equal members of a given type.

The problem in this approach is that the definition of type equality for PI types mentions  term equality at a non-strictly-positive position.

The terms (v1:A1 -> B1)  and (v2:A2 -> B2) denote equal PI types in Nuprl iff 

A1 and A2 are equal types 

and  

forall terms a1 and a2 such that a1 and a2 are equal members of A1, B1[v1\a1] and B2[v2\a2] are equal types.

(the part in underlined italics is problematic)

The definition of term equality in PI types has a similar problem.

Here is some Coq code that can perhaps make the above explanation more concrete.

(if the code below is not rendered properly, please see Nuprl.v (attached))

----------------------

Definition Var : Set := nat.

Inductive Term : Set :=

| app : Term -> Term -> Term (* term denoting application *)

| lam : Var -> Term -> Term (* curry style; type of variable is not specified *)

| num : nat -> Term (* terms denoting numbers *)

| NAT : Term (* term denoting the type of numbers *)

| PI : Var -> Term -> Term -> Term (* term denoting PI types *).

(* substitute u for v in t *)

Definition subst (u: Term) (v: Var) (t : Term) : Term .

Admitted.

(* (reducesTo u v) denotes that computation on the term u converges to the value v. *)

Definition reducesTo : Term -> Term -> Prop.

Admitted.

Inductive equalTypes : Term -> Term -> Prop :=

| TEQ_NAT : forall (T1 T2 : Term), 

     reducesTo T1 NAT

     -> reducesTo T2 NAT

     -> equalTypes T1 T2

| TEQ_PI :  forall (A1 B1 A2 B2 T1 T2 : Term) 

     (v1 v2 : Var),

     (reducesTo T1 (PI v1 A1 B1) )

     -> (reducesTo T2 (PI v2 A2 B2))

     -> equalTypes A1 A2

     -> (forall (a1 a2 : Term),

           equalTermsInType a1 a2 A1 (* NON STRICTLY-POSITIVE OCCURRENCE *)

           -> equalTypes (subst a1 v1 B1) (subst a2 v2 B2))

     -> equalTypes T1 T2

with equalTermsInType : Term -> Term -> Term -> Prop :=

| EQ_NAT : forall (t1 t2 T: Term) (n: nat),

         reducesTo T NAT

         -> reducesTo t1 (num n)

         -> reducesTo t2 (num n)

         -> equalTermsInType t1 t2 T

| EQ_PI : forall (T A B f1 f2 : Term ) (v : Var),

        reducesTo T (PI v A B)

        -> equalTypes (PI v A B) (PI v A B) (*(PI v A B) has to be a type *)

        -> (forall (a1 a2 : Term),

             equalTermsInType a1 a2 A (* NON STRICTLY-POSITIVE OCCURRENCE *)

             -> equalTermsInType (app f1 a1) (app f2 a2) (subst a1 v B))

        -> equalTermsInType f1 f2 T.

-------------------------

The same problem would occur if one tries to define a similar fragment of Coq in the above style.

For Coq, perhaps one would define using mutual induction the following:

- which terms denote types

- which terms are members of a given type.

The attached file Coq.v shows where strict positivity is violated in this case.

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/ 

Attachment: Nuprl.v
Description: Binary data

Attachment: Coq.v
Description: Binary data