The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

On 15/06/2012 08:29, Gert Smolka wrote:
> One of our students discovered that Coq 8.3 accepts
>
> Fixpoint foo (x : nat) : nat := (fun _ =>  O) (foo x).
>
> although foo diverges under cbv.
>
> Is this considered a bug or a feature?
> (foo terminates under call by name)
>
> Gert
This is definitely not a feature ! This is not really a bug either 
because if strong normalization is broken, weak is not. As a result, 
consistency remains.

In any case, it's a known but not that popular fact. (Each time I show 
that to someone, he can't believe its eyes, then he trys for half a day 
to get a closed proof of false thanks to that. None has succeed yet).

It is also one of the purpose of my proposal for a new implementation of 
guard condition that I formally describe and badly try to explain the 
motivations here : 
http://hal.archives-ouvertes.fr/docs/00/65/17/80/PDF/boutillier.pdf

The main purpose is to exhibit how an abstract machine that computes 
subterm_values instead of lambda terms could at the same time ensure 
strong normalization and allow to interleave "fix" and "injection" 
tactics (which means in CIC term accepting

fix f x := match x with |C y => fun f' => f' y end f.

)

The patch that implements this is in the proof reading queue of the 
kernel guardian for a month...

Pierre.