Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] about 'function' definition clause

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] about 'function' definition clause


Chronological Thread 
  • From: Pascal Manoury <pascal.manoury AT pps.univ-paris-diderot.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] about 'function' definition clause
  • Date: Tue, 10 Feb 2015 18:46:26 +0100



> Hello. Why not taking a pair as argument, ordered lexicographically?
> Frédéric.
Because I am interested in using ordinal measure, not in proving Ackermann's
termination :)

We already use a pair as argument and the nested recursion in refused.

Pascal Manoury.

>
> Le 10/02/2015 18:25, Pascal Manoury a écrit :
>> Hello dear coqists,
>>
>> I am trying with students to experiment the use of the 'function'
>> definition clause and ordinal measure for proving
>> termination of recursive functions.
>>
>> Unfortunately, we are stuck with the example of Ackermann's function
>> because the 'function' clause does not
>> allow nested recursion.
>>
>> Is there any way to relax this restriction, for instance, by generalizing
>> the nested recursive call when generating
>> the proof obligation ?
>>
>> Pascal Manoury.
>>
>




Archive powered by MHonArc 2.6.18.

Top of Page