The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Le 29/02/2016 12:17, Thorsten Altenkirch a écrit :

Healfdene Goguen’s thesis in particular included \eta-reduction which was a non-trivial issue.

I don’t think Benjamin Werner did this.

Yes, he did. But he considered only 1 or 2 universes.

Frédéric.

Neither did I, in my ’93 PhD

http://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf

but I still think this is the simplest (and first) proof of SN for CoC with large eliminations – hence I would be grateful if it doesn’t get completely ignored.

A short summary is given in 

http://www.cs.nott.ac.uk/~psztxa/publ/types94.pdf

Cheers,

Thorsten

From: <coq-club-request AT inria.fr> on behalf of "Luo, Zhaohui" <Zhaohui.Luo AT rhul.ac.uk>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Monday, 29 February 2016 02:21
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Cc: "Luo, Zhaohui" <Zhaohui.Luo AT rhul.ac.uk>
Subject: Re: [Coq-Club] Is Coq SN ?

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*)

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.