fibonacci function in scientific-computing-lean

Stream: general

[Asei Inoue]

The following code is proposed in https://lecopivo.github.io/scientific-computing-lean/working-with-arrays.html :

def fibonacci (n : Nat) : Array Nat := Id.run do
    let mut fib : Array Nat := Array.mkEmpty n
    fib := fib.push 0
    fib := fib.push 1
    for i in [2:n] do
        fib := fib.push (fib[i-1]! + fib[i-2]!)
    return fib

The text says that fib.push actually mutates the array:

The great thing about Lean is that the above code actually mutates the array fib. Each call of fib.push in the Fibonacci function modifies the array directly.

I wanted to make sure that the array was actually being changed in a destructive way. So I wrote the following code.

def fibonacci (n : Nat) : Array Nat := Id.run do
    let mut fib : Array Nat := Array.mkEmpty n
    fib := fib.push 0
    fib := fib.push 1
    for i in [2:n] do
        fib := (dbgTraceIfShared "share" fib).push (fib[i-1]! + fib[i-2]!)
    return fib

#eval fibonacci 32

My guess is that the share message should only be displayed once．In actuality, however, as many share messages as there are for statements are displayed.
What is wrong with my testing method?

[Tomas Skrivan]

Haha I never tested if the claim is actually true :)

The usual issue with testing this is that you hit compiler optimization which decides to turn something into a global variable. Not sure if this is happening here though but definitely have a look at previous Zulip questions getting confused by dbgTraceIfShared not working as naively expected.

[Siddhartha Gadgil]

It is possible that the presence of the trace blocked the optimizations of Functional but in place and so the Array was not mutated. Maybe a good check is the generated C code.

[Marc Huisinga]

Tomas Skrivan said:

Haha I never tested if the claim is actually true :)

The usual issue with testing this is that you hit compiler optimization which decides to turn something into a global variable. Not sure if this is happening here though but definitely have a look at previous Zulip questions getting confused by dbgTraceIfShared not working as naively expected.

Global variables wouldn't need to be copied every iteration.

Some evidence that the presence of dbgTraceIfShared is probably messing things up and that the code is at least morally linear (though compiler optimizations may still get in the way in the original code):

@[noinline]
def checkedPush (fib : Array Nat) (x : Nat) : Array Nat :=
  (dbgTraceIfShared "share" fib).push x

def fibonacci (n : Nat) : Array Nat := Id.run do
    let mut fib : Array Nat := Array.mkEmpty n
    fib := fib.push 0
    fib := fib.push 1
    for i in [2:n] do
        fib := checkedPush fib (fib[i-1]! + fib[i-2]!)
    return fib

#eval fibonacci 32 -- no "share"

[Marc Huisinga]

The IR shows that it's indeed dbgTraceIfShared messing things up. The dbgTraceIfShared call is executed first and only then it executes fib[i-1]! and fib[i-2]!. So it becomes shared with the dbgTraceIfShared call and then again referentially unique just before the push. This is why it's typically a good idea to put dbgTraceIfShared calls on their own line, though the compiler may still decide to re-order things and break linearity (see this post for an example).

This works as expected:

def fibonacci (n : Nat) : Array Nat := Id.run do
    let mut fib : Array Nat := Array.mkEmpty n
    fib := fib.push 0
    fib := fib.push 1
    for i in [2:n] do
        fib := dbgTraceIfShared "share" fib
        fib := fib.push (fib[i-1]! + fib[i-2]!)
    return fib

#eval fibonacci 32

[Asei Inoue]

Thank you all!!

[Asei Inoue]

By the way, is it not possible to check which memory address the value of a variable is stored at in Lean?

[Mario Carneiro]

It is possible, with one of two methods:

• ptrAddrUnsafe (a : α) : USize. This directly returns the address of a lean object. This is unsafe because it violates referenital transparency - the same (up to equality) object can result in different outputs depending on where it was allocated and how many other versions of the object exist in memory
• withPtrAddr (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β: this is a safe function which gives access to the pointer value. The catch is that you can't actually use the value you get in any way which changes the final result - this is needed to avoid the possibility of defining non-functional functions caused by the raw getter above. This can still be used if you use the equality only for caching purposes and only the time taken to calculate the result changes depending on what address you get.

[Asei Inoue]

@Tomas Skrivan

Haha I never tested if the claim is actually true :)

That's actually true!!

/-- calculate fibonacci sequence  -/
unsafe def fibonacci (n : Nat) : Array Nat := Id.run do
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    -- display memory address of `fib`
    dbg_trace ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

-- same address!
#eval fibonacci 15