The Coq mailing list

["Luo, Zhaohui" <Zhaohui.Luo AT rhul.ac.uk>]

Dear all,

In his PhD thesis in 1994, Goguen has studied the meta-theory of UTT (SN, CR, SR, ...) which is essentially CoC + inductive types + universes (ie, a subset of the current Coq system pCIC after its universe Set became predicative.) 

Best regards,

Zhaohui

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of roux cody <cody.roux AT gmail.com>
Sent: 28 February 2016 20:57
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is Coq SN ?

 

The SN of CIC + universes is something of a nasty open question at the moment. With recursors instead of fixpoint and no co-induction, it's believed to be indeed strongly normalizing, with Benjamin Werner's PhD serving as reference for the CIC without universes and Luo's thesis for CoC with universes.

There is no "smoking gun" that seems to jeopardize consistency, but a complete write up would be nice.

Size types seem to be a tempting solution to fix the weak normalization problem mentioned above, with the main obstruction to implementation being lack of manpower and reverse compatibility, I believe. Also Sacchini's proof only covers a small subset of inductives (just nat I think) and a single universe, so it would be reassuring to have a full proof.

I think part of the issue is that the theory for strong normalization proofs are really not streamlined, which means each individual proof has to do a lot of setup work, which is really discouraging. In particular, there seems to be some resilience to using the "usual" realizability semantics interpretation. There's some work by Hyland, Ong and Ritter on how to fix this, but it hasn't been pushed all the way through, as far as I know.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.6979&rep=rep1&type=pdf

Co-recursion is tough. Up to recently there has been no clean formulation of size-typed based criteria for co-inductives. A strong move in this direction has been pursued in the last couple of years by Abel et al, see eg these nice slides:

http://www.cse.chalmers.se/~abela/talkIHP14.pdf

There's an experimental implementation in Agda:

https://gist.github.com/puffnfresh/8960574

It still seems a ways away in Coq.

Best,

Cody

This email has been sent from a virus-free computer protected by Avast.
www.avast.com

On Sun, Feb 28, 2016 at 1:43 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

However, Coq's implementation (if no bugs) should be weakly normalizing,
which is usually enough for consistency.

I thought that for consistency we also need type preservation (along with strong/weak normalization). 

Coq seems to not have type preservation, as shown in the last 2 slides (25 and 26) of 

https://coq.inria.fr/files/coq5-slides-sacchini.pdf

I just reproduced the above described problem using Coq 8.5:

Set Implicit Arguments.

CoInductive Inf :=

S : Inf -> Inf.

CoFixpoint infinity : Inf :=S ( infinity).

(** This innocuous looking function 

    actually causes an unfolding of cofix *)

Definition unfold (x : Inf) : Inf :=

match x with

| S y => S y

end.

Definition unfoldEq (x:Inf) : x = unfold x.

Proof.

  intros.

  destruct x as [x'].

  simpl. exact eq_refl.

Defined.

(** We make a dummy goal to use the "type of" function *)

Goal False.

(** [unfoldEq infinity] is of type [infinity = S infinity] *)

match type of (unfoldEq infinity) with

| ?T => let T' := eval simpl in T in idtac T "," T'

end.

(**

    when we compute on [eqq infinity] as shown above, we

    get [eq_refl] which cannot be of the type

    [infinity = S infinity] because [S infinity] is not definitionally equal to [infinity]. *)

Eval compute in (unfoldEq infinity).

(** This is  a voilation of type preservation*)