The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello,

this is a known problem of the termination checker.

What happens is that Coq reduces the body of the fixpoint, and then 
checks whether all recursive calls are guarded. In your example, after 
reduction, the body no longer contains any recursive calls (and in 
particular the non-terminating call), so Coq accepts your definition.

See also:

* http://foundations.cs.ru.nl/chitchat/slides/chit-barras.pdf
  A talk by Bruno Barras on the implementation of the guard condition. 
Slide 22 shows about the same example as below.

* http://cs.ioc.ee/~tarmo/papers/mscs04.pdf
  Page 2 (last paragraph) - 4 explain the problems of the guard condition.

* http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1843

Robbert

On 06/15/2012 08:29 AM, 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