The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

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)