The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

To add to Thomas' argumentation, sometimes you don't even have a
choice since the integer bound is not computable (typically for
lexicographic orders) and neither is the well-foundedness proof (if it
is classical for instance, as in Guillaume Melquiond's original post).

Stéphane

On Thu, Sep 24, 2009 at 8:34 PM, Thomas Braibant
<thomas.braibant AT gmail.com>
 wrote:
>>> A nice trick by B. Barras & G. Gonthier some time ago on this list was
>>> to use a "guard"  to the well_foundedness argument, which hides it.
>>>
>> I'm not sure to understand the interest of this trick.
>> The only way to really prove the termination of the function is to be able 
>> to give an upper bound of the number of recursive steps done in guard. In 
>> that case, why > not use the {measure ....} construction.
>
> But, sometime, the upper bound can be very big, and using measure (or
> wf), wouldn't you start by evaluating this upper bound, by computing
> the witness of termination, in order to exhibit all the constructors
> needed for the recursion? In our case, the function was the
> determinisation of NFA, and the bound was 2 to the power of the number
> of states of the original automata. Which is quite big.
>
> Here, using this guard, you still need to prove the well-foundedness
> of the recursive calls, but you are given 2^n recursion steps, before
> trying to compute the witness...
>
> Here is the original post on this list from where this is originated :
> http://logical.saclay.inria.fr/coq-puma/messages/7d5a3493009fd0e2
>
> Thomas
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06