Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification


Chronological Thread 
  • From: raffaello.giulietti AT supsi.ch
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification
  • Date: Thu, 8 Jun 2017 14:52:47 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=raffaello.giulietti AT supsi.ch; spf=Pass smtp.mailfrom=raffaello.giulietti AT supsi.ch; spf=Pass smtp.helo=postmaster AT ti-edu.ch
  • Ironport-phdr: 9a23:cK+NFROwY0y8VvtPrtEl6mtUPXoX/o7sNwtQ0KIMzox0LPv5rarrMEGX3/hxlliBBdydsKMbzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzYHPbYGJN/dzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cBJ/xXr4fzp1QUsxS+AQ2sBOT1xj9Hh3/2wKk60+U/HgHawAwgHskDsG/JrNXtL6cSUPq5w7XIzTjFcvhY2i/95ZDVfh0lofyAR698fMjQxEU1Cg/IjFSdpZb4Mz6Xy+gAtXWQ4fB6WuK1kWEnrhl8ojixyccojYnEnp4VylHd+Spn3Yk1OMe0R1J7YdK8EZtQsT+VN5duT88/R2xluDw2xqAEtJO6ZiQG1ZYqyh/FZ/CacYWE/wrvVOOLLjd5gHJldqi/hxG38UW40O3zTMe00FhQoSVbltnMsncN2wbc6siGV/t9+kah1iiT1wDP6+FJOls0lbfDK546w748jIYcsUTbEi/shEr2lLOWdlkj+uWw9+vnZazmqoaAOI9wlwHxKb8jmte/AOQ9KggBRXKX+eW61L35/E32Wq9GjvMskvqRjJePLsMC46W9HgV904A56h/5AS31/s4fmCwdJVxLcR+Di4+vNFDTJPH1Eeu+q0+xiCxqgfvGbe6pOYnEMnWWyOSpRr168UMJkAc=
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


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
>


Archive powered by MHonArc 2.6.18.

Top of Page