The Coq mailing list

[Morrisett <morrisett AT gmail.com>]

But it breaks extraction to CBV languages such as Ocaml. Consider this more insidious example:

Fixpoint f(x:nat):nat:= 

  let x := f x in 0.

This extracts to:

letrec f x = let z = f x in 0

Which diverges. 

-Greg

On Jun 8, 2017, at 8:56 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:

On Thu, Jun 8, 2017 at 9:52 AM, <raffaello.giulietti AT supsi.ch> wrote:

I agree on both your observation about evaluation strategies as well as
your (and my) surprise that Coq tries to be smart.

I think Coq should reject the definition.


Greetings
Raffaello

The problem is that it should then reject many good definitions (take division, for instance).

 

On 08/06/17 14:41, Gaetan Gilbert wrote:
> Some evaluation strategies terminate. eg
>
>
> Fixpoint z (n: nat): nat := 0 * z n.
>
> Lemma foo n : z n = 0.
> unfold z. cbn.
> (* (fix z (n0 : nat) : nat := 0) n = 0 *)
>
>
> I don't know why Coq tries to be smart with this though.
>
> Gaëtan Gilbert
>
> On 08/06/2017 14:38, raffaello.giulietti AT supsi.ch wrote:
>> Hello,
>>
>> consider the following z function
>>
>> Fixpoint z (n: nat): nat := 0 * z n.
>>
>> which Coq accepts with the usual notification "decreasing on 1st
>> argument".
>>
>> Well, I don't see that this recursive definition is "decreasing on 1st
>> argument". Indeed, an invocation results in an infinite recursion, as
>> witnessed by the Out of memory message:
>>
>> Compute z 0.
>> Out of memory.
>>
>> I'd expect Coq to reject the definition (even if the smallest
>> mathematical fixpoint is the unary function 0).
>>
>> What is really happening? Any clarification would help.
>>
>> Greetings
>> Raffaello
>