The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

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
>