Complexity of Fibonacci sequence evaluation

Stream: general

[Gihan Marasingha]

Chapter 8 of #tpil has the following definition.

def fib : nat → nat
| 0     := 1
| 1     := 1
| (n+2) := fib (n+1) + fib n

It is claimed that, by using course-of-values recursion to interpret this definition, exponential blowup is avoided. However, using set_option profiler true to time the evaluation, I get the following results (times in milliseconds)

fib 29   550
fib 30   970
fib 31  1536
fib 32  2470

Am I missing something?

Additional question: does Lean translate every function defined using nat.brec_on into a function defined using nat.rec_on? If so, how can I view this translation?

[Mario Carneiro]

This used to be true in an older version of lean. It was later "fixed" to have the expected exponential behavior

[Mario Carneiro]

@Jeremy Avigad has been hunting down and removing references to this older behavior in TPIL

[Mario Carneiro]

Additional question: does Lean translate every function defined using nat.brec_on into a function defined using nat.rec_on? If so, how can I view this translation?

No, nat.brec_on is a function which is defined in terms of nat.rec_on, there is no translation involved, just one function calling another

[Mario Carneiro]

you can view the definition with #print nat.brec_on

[Eric Wieser]

Is there any discussion about the motivation behind this "fix"?

[Mario Carneiro]

The reason you get exponential behavior here is that the VM doesn't actually use the brec_on definition, it compiles using "naive recursion", i.e. what you would do in a C like language. You called the function twice so that's what you will get

[Mario Carneiro]

If you want alternate evaluation behavior you have to write it explicitly

[Mario Carneiro]

I think this is a good thing in general, because directly executing a brec_on is time and memory wasteful

[Mario Carneiro]

because you have to build up a tuple of all previous values, even though the compilation strategy can only use the first n of them for some fixed n (here 2)

[Gihan Marasingha]

Thanks @Mario Carneiro ! Follow up questions: for every inductive type foo, is every recursor on foo defined in terms of foo.rec? Is there a list of the recursors that are created automatically? I know of rec, rec_on, cases_on and (for inductive types in Prop), foo.dcases_on.

[Bryan Gin-ge Chen]

#print prefix foo should list them all.

[Mario Carneiro]

for every inductive type foo, is every recursor on foo defined in terms of foo.rec?

Yes.

Is there a list of the recursors that are created automatically? I know of rec, rec_on, cases_on and (for inductive types in Prop), foo.dcases_on.

You can use #print prefix foo on a newly declared inductive type to see all the autogenerated functions. The only one that can be called a recursor that is not on your list is brec_on.

[Gihan Marasingha]

Thanks Bryan and Mario. Silly of me to miss brec_on when I'd been asking about it!

[Kevin Buzzard]

@Gihan Marasingha when you make a new inductive type lean adds new axioms/constants to its system! One for the type, one for each constructor, and then this rec function, the eliminator. You can #print definitions and see that the rec function has no definition, but all the other useful stuff which is auto-generated does (and a lot of it uses rec).

[Kevin Buzzard]

For example when you define nat lean adds four new constants to the system -- nat, nat.zero, nat.succ and nat.rec. everything else is made from that. I have a blog post called something like no confusion over no_confusion where Chris and I went through some of the stuff defined by the system and figured out how to define it ourselves

[Jeremy Avigad]

I'll update TPIL.

[Jeremy Avigad]

TPIL updated: https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html. (Also with Johan's correction regarding @@.)

[Kevin Buzzard]

Thank you as ever Jeremy! I'm still avidly recommending this text to all the computationally minded people who show up on the Discord.

[Reid Barton]

If VM evaluation doesn't have the memoizing behavior of brec_on, is there any point to the equation compiler using it?
Even in Lean 4, the equation compiler still generates Nat.brecOn.