Thunks

Stream: lean4

[Jonas Bayer]

I just found out that Lean 4 supports Thunks which are described on the documentation page Lean 4 Docs: Thunks. This made me curious and I tried out the code given there which should supposedly calculate the Fibonacci numbers. Code from the documentation page linked above:

def fib : Nat → Nat
  | 0   => 0
  | 1   => 1
  | x+2 => fib (x+1) + fib x

def f (c : Bool) (x : Thunk Nat) : Nat :=
  if c then
    x.get
  else
    0

def g (c : Bool) (x : Nat) : Nat :=
  f c (Thunk.mk (fun _ => fib x))

#eval g false 1000

However, I only get the value zero as a result, which makes sense from how g is defined. But I see very little benefit in such behavior.

What I wished for the example to do was to calculate the value of the 1000th Fibonacci number but with caching of all previous Fibonacci numbers. Using a cache the computation then is no longer exponential and should therefore be much faster although the original fib definition is very computationally inefficient.

Is it possible that there is a mistake in the example? If not, could you give me an explanation where I'm wrong?

[Sebastian Ullrich]

I'm afraid I don't understand your code at all or how it should lead to caching. There recently was a thread on memoization of functions like fib: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/memoziation.20of.20strong.20recursion.20on.20nat

[Jonas Bayer]

It is not actually my code, I just copied it from the documentation page linked above. (I also just changed the original post to make that clearer).

[Sebastian Ullrich]

Oops, I see! It's merely supposed to illustrate that the thunk is not run when its value is not actually needed. It does not attempt to speed up fib itself.

[Mario Carneiro]

The example seems to be demonstrating that x is not evaluated because c is false (fib 1000 being used as a stand-in for something that takes long enough to be noticeable), but that would also be true if you replaced Thunk Nat with Unit -> Nat

[Jonas Bayer]

This is also what I found out when playing around with it. But what is the added value of a Thunk then? Edit: I just saw that this is described in the second example