The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 21/12/2020 à 14:14, Xavier Leroy a écrit :

> On Mon, Dec 21, 2020 at 8:10 AM Guillaume Melquiond wrote:
> 
>     Fixpoint foo (n:nat) x :=
>       match n with
>       | S n => foo n (foo n x)
>       | O => bar x
>       end.
> 
>     With n = 64, it will already run past the end of the solar system.
> 
> This is a nice trick when it applies, i.e. not that often in my
> experience.

Actually, this trick always works! Indeed, in the worst case, if you
cannot adapt your recursive function to look like "foo", then you just
use "foo" itself as fuel for your function. Here is what it looks like:

Inductive fuel :=
  | FO : fuel
  | FS : (unit -> fuel) -> fuel.

(* the dummy "unit" argument is only there in case you intend to
evaluate your code using a cbv strategy, e.g., vm_compute. *)

Fixpoint foo (n:nat) x :=
  match n with
  | S n => FS (fun _ => foo n (foo n x))
  | O => x
  end.

Fixpoint bar f x :=
  match f with
  | FO => not_enough_fuel
  | FS f => do_something x (bar (f tt) (do_some_other_thing x))
  end.

Definition forever_bar x := bar (foo 64 FO) x.

Best regards,

Guillaume