The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

My bad.  There is something else going on in the recursive function.
It passes the recursive call as a continuation, which is being called
more often than I thought, and is running until out of fuel in some
cases even though the outer recursion doesn't.

I wish there was an easy way to debug Gallina code.

Thanks anyway to Jason and Clément for the suggestions.

On Wed, 16 Dec 2020 21:41:36 -0500
Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

> On 12/16/20 8:31 PM, 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).  
> 
> What if you pass much larger fuel values, like 10000?
> 
> > 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.  
> 
> The 30x factor is surprising, but a small difference wouldn't be
> entirely unexpected for large constants, since they have to be
> constructed.  Try replacing 100 with (Nat.of_uint 100%uint), or
> passing 10000 as the fuel (which will automatically get interpreted
> as (Nat.of_uint 10000%uint)):
> 
> Fixpoint collatz (fuel: nat) (start: positive) :=
>   match fuel with
>   | O => false
>   | S fuel =>
>     match start with
>     | xO x => collatz fuel x
>     | xI _ => collatz fuel (start * 3 + 1)
>     | xH => true
>     end
>   end.
> 
> Require Import Decimal.
> 
> Time Compute (collatz 50 150).    0s
> Time Compute (collatz 2000 150).  0.006s
> Time Compute (collatz 5000 150).  0.021s
> Time Compute (collatz 10000 150). 0s (w/ warning)
> 
> 
>