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