Zulip Chat Archive

Stream: general

Topic: Complexity of Fibonacci sequence evaluation


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 02 2021 at 19:05):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 02 2021 at 19:07):

you can view the definition with #print nat.brec_on

view this post on Zulip Eric Wieser (Jan 02 2021 at 19:08):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 02 2021 at 19:10):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jan 02 2021 at 19:33):

#print prefix foo should list them all.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Jeremy Avigad (Jan 04 2021 at 01:34):

I'll update TPIL.

view this post on Zulip 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 @@.)

view this post on Zulip 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.


Last updated: May 13 2021 at 05:21 UTC