The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Does anything change if you don't pass the fuel as a literal, but instead pass it as 10*10?  What if you use a "thunked nat" type for recursion where the successor argument is of type "(unit -> tnat) -> tnat", so the fuel isn't computed eagerly, define addition and multiplication for these, and then use 10*10 as thunked nat fuel?

On Wed, Dec 16, 2020, 20:31 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

I have a recursive Gallina function that uses a nat-typed fuel arg to
guarantee termination.  In cases where the function terminates prior to
running out of fuel, I've found that larger than necessary fuel args
are very costly. For example, with a fuel value of 100, the function
takes 30 times longer than if the fuel value is 10 (neither runs out of
fuel, all other args are the same). In both cases, the computation was
done with vm_cast_no_check. Nothing is done with the fuel arg other
than the usual "match fuel with 0 => done | S n => loop n"
recursion idiom.

I guess this is probably due to the overhead of nats in Gallina.  But
it is still surprising to me, considering that if I wrote a function to
traverse the first 8 links in a list, I wouldn't expect it to take 30
times longer with a 100-element list than a 10-element list.

Is there a way around this?  I'd like to use a constant fuel value
that is plenty large enough, without having to compute one from the
function's arguments that is just barely large enough.