The Coq mailing list

[Tobias Tebbi <t.tebbi AT googlemail.com>]

It even badly interferes with extraction:

Definition ignore (x:nat) := 0.

Fixpoint foo (x : nat) : nat := ignore (foo x).

Extraction foo.

produces the Ocaml code

let rec foo x =

  ignore (foo x)

that obviously does not terminate.

I guess this really should be considered a bug.

(At least it cannot happen if you extract to Haskell :D )

Best,

Tobias

2012/6/15 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.