Zulip Chat Archive

Stream: general

Topic: Complexity of Fibonacci sequence evaluation


Gihan Marasingha (Jan 02 2021 at 18:17):

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 (Jan 02 2021 at 19:05):

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

Mario Carneiro (Jan 02 2021 at 19:05):

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

Mario Carneiro (Jan 02 2021 at 19:06):

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 (Jan 02 2021 at 19:07):

you can view the definition with #print nat.brec_on

Eric Wieser (Jan 02 2021 at 19:08):

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

Mario Carneiro (Jan 02 2021 at 19:09):

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 (Jan 02 2021 at 19:10):

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

Mario Carneiro (Jan 02 2021 at 19:11):

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

Mario Carneiro (Jan 02 2021 at 19:12):

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 (Jan 02 2021 at 19:32):

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 (Jan 02 2021 at 19:33):

#print prefix foo should list them all.

Mario Carneiro (Jan 02 2021 at 19:34):

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 (Jan 02 2021 at 19:35):

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

Kevin Buzzard (Jan 02 2021 at 23:27):

@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 (Jan 02 2021 at 23:29):

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 (Jan 04 2021 at 01:34):

I'll update TPIL.

Jeremy Avigad (Jan 22 2021 at 01:07):

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

Kevin Buzzard (Jan 22 2021 at 08:16):

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 (Nov 15 2022 at 18:36):

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.


Last updated: Dec 20 2023 at 11:08 UTC