How to construct an array inductively?

Stream: new members

[Jakub Nowak]

I want to construct an array of size n, by calculating elements one by one, but also using already computed values of an array. As an example, I want to have a function fib (upto : Nat) : Array Nat the returns an array of first upto Fibonacci numbers.

I would want something like Array.ofFn, but with the following signature:

def Array.ofFnInduct (f : Fin n → Array α → α) : Array α

I can implement it like this:

def Array.ofFnInduct (f : Fin n → Array α → α) : Array α :=
  if _ : n = 0 then
    Array.emptyWithCapacity 0
  else
    re ⟨0, by cutsat⟩ (Array.emptyWithCapacity n)
where
  re (k : Fin n) arr :=
    let arr := arr.push (f k arr)
    if _ : k+1 = n then
      arr
    else
      re ⟨k+1, by cutsat⟩ arr
  termination_by n-k

But is it possible to implement this easier, possibly without recursion?

[Jakub Nowak]

More likely, to be able to use the array without unsafe get, I would probably want something with this signature:

def Array.ofFnInduct (f : (k : Fin n) → (arr : Array α) → (arr.size = k) → α) : Array α

[Jakub Nowak]

def Array.ofFnInduct (f : (k : Fin n) → (arr : Array α) → (arr.size = k) → α) : Array α :=
  if _ : n = 0 then
    Array.emptyWithCapacity 0
  else
    re ⟨0, by cutsat⟩ (Array.emptyWithCapacity n) (by grind)
where
  re (k : Fin n) arr h :=
    let arr := arr.push (f k arr h)
    if _ : k+1 = n then
      arr
    else
      re ⟨k+1, by cutsat⟩ arr (by grind)
  termination_by n-k

[Aaron Liu]

Like this? Maybe this implementation would be better for List though, since I didn't use Vector.emptyWithCapacity.

def Vector.ofFnInduct {α : Type u} {n : Nat} (f : (k : Fin n) → Vector α k → α) : Vector α n :=
  match n with
  | 0 => #v[]
  | n + 1 =>
    letI ih := Vector.ofFnInduct fun k ih => f k.castSucc ih
    ih.push (f (Fin.last n) ih)

[Jakub Nowak]

I do want constant-time access though. That's why I'm ussing Array. Does Lean's List have constant-time access?

[Aaron Liu]

for lists accessing the nth element is O(n)

[Jakub Nowak]

So that's a no. I want fib (upto : Nat) : Array Nat to be linear.

[Aaron Liu]

then try modifying what I have to use Vector.emptyWithCapacity instead of #v[]

[Jakub Nowak]

Isn't Vector just a List?

[Aaron Liu]

oh and you can also try making it tail recursive

[Aaron Liu]

Jakub Nowak said:

Isn't Vector just a List?

no, docs#Vector wraps a docs#Array with known length, and docs#List.Vector wraps a docs#List with known length

[Jakub Nowak]

Oh. :O
I didn't knew there are two different Vector.

[Jakub Nowak]

Aaron Liu said:

then try modifying what I have to use Vector.emptyWithCapacity instead of #v[]

Is it strictly needed though? Isn't push amortized constant-time?

[Aaron Liu]

sure

[Aaron Liu]

but it's better to do emptyWithCapacity right

[Jakub Nowak]

Aaron Liu said:

oh and you can also try making it tail recursive

I think the tail recursive version is what I wrote, just for Vector?

[Jakub Nowak]

Hmm, wait, I'm not sure if your implementation is linear? This is because in your implementation the call to e.g. f 100 .. would need to get through 100 nested calls.

[Jakub Nowak]

No, it's the other way around. If n is 100, then the call to f 0 would have to go through 100 nested calls.

[Aaron Liu]

Jakub Nowak said:

Hmm, wait, I'm not sure if your implementation is linear? This is because in your implementation the call to e.g. f 100 .. would need to get through 100 nested calls.

after checking the ir with set_option trace.compiler.ir.result true, I can confirm that it is linear

[Aaron Liu]

but if f modifies the vector taken as input it will have to be copied

[Robin Arnez]

Well it recursively allocates a closure though doesn't it?

[Aaron Liu]

it's not tail recursive

[Aaron Liu]

the stack will be O(log n)

[Aaron Liu]

but the array is used linearly

[Robin Arnez]

Oh I thought we were talking about running time, which would be quadratic here due to suboptimal compilation

[Aaron Liu]

Robin Arnez said:

Oh I thought we were talking about running time, which would be quadratic here due to suboptimal compilation

wait why is it quadratic

[Jakub Nowak]

@Aaron Liu
Look at the printed trace here.

set_option trace.compiler.ir.result true

def BaseIO.println [ToString α] (s : α) : BaseIO Unit :=
  EIO.catchExceptions (IO.println s) (fun _ ↦ return ())

unsafe def Vector.ofFnInduct {α : Type u} {n : Nat} (f : (k : Fin n) → Vector α k → α) : Vector α n :=
  match n with
  | 0 => #v[]
  | n + 1 =>
    letI ih := Vector.ofFnInduct fun k ih => f (unsafeBaseIO do BaseIO.println k; return k.castSucc) ih
    ih.push (f (Fin.last n) ih)

#eval! Vector.ofFnInduct (n := 20) (fun k v ↦ k)

[Robin Arnez]

If you look at the compilation output you'll see that it passes fun k ih => f k.castSucc ih as a new allocated closure instead of just using f. That way we get deeply nested closures that take longer and longer to reach the actual f.

[Jakub Nowak]

If we assume that initial f is constant-time, then we want Array.ofFnInduct to work in O(n). You're "building-up" f through each recursive call. After 10 steps, the call to the modified f has to go through 10 anonymous lambdas, before it calls the original f. After 100 steps, the call to the modified f has to go through 100 anonymous lambdas, before it calls the original f.

[Robin Arnez]

Anyways, this should work better as a tail-recursive (and probably linear time) variant:

def Vector.ofFnInduct {α : Type u} {n : Nat} (f : (k : Fin n) → Vector α k → α) : Vector α n :=
  go 0 (Nat.zero_le _) (Vector.emptyWithCapacity n)
where
  go (k : Nat) (hk : k ≤ n) (v : Vector α k) : Vector α n :=
    if h : k < n then
      go (k + 1) h (v.push (f ⟨k, h⟩ v))
    else
      v.cast (by lia)

[Aaron Liu]

oh yeah that happens

[Aaron Liu]

I didn't notice

[Aaron Liu]

ok it has quadratically many closures

[Aaron Liu]

but if you feed it a function f then f only gets called linearly many times

[Jakub Nowak]

Yes. But if we assume that initial f is constant-time, then we want Array.ofFnInduct to work in O(n), not O(n^2).

[Aaron Liu]

well of course

[Aaron Liu]

then make it tail recursive and all the problems are solved

[Aaron Liu]

but the version I had would probably be better for List.Vector

[Aaron Liu]

it has better defeqs

[Jakub Nowak]

Hmm, for proofs you probably want to use Array.ofFn for a recursively defined function f, specifically defined by a structural induction on Nat. And you can write unsafe implementation of Array.ofFn that replaces recursive calls with array access.

[Aaron Liu]

oh yeah

[Jakub Nowak]

Aaron Liu said:

then make it tail recursive and all the problems are solved

It's not about tail recursiveness though. Tail recursiveness is an optimization that doesn't even change complexity class.
What would have to happen to ensure that this compiles down to O(n) implementation is, compiler would have to realize that fun k ih => f k.castSucc ih is equal to f after Prop erasure, and pass it explicitly, without creating a lambda abstraction. In fact, maybe Lean's compiler is smart enough to do that? I don't know who we could ask to answer that?

[Robin Arnez]

Robin Arnez schrieb:

Anyways, this should work better as a tail-recursive (and probably linear time) variant:

def Vector.ofFnInduct {α : Type u} {n : Nat} (f : (k : Fin n) → Vector α k → α) : Vector α n :=
  go 0 (Nat.zero_le _) (Vector.emptyWithCapacity n)
where
  go (k : Nat) (hk : k ≤ n) (v : Vector α k) : Vector α n :=
    if h : k < n then
      go (k + 1) h (v.push (f ⟨k, h⟩ v))
    else
      v.cast (by lia)

Well this tail-recursive implementation also avoids this problem

[Jakub Nowak]

Robin Arnez said:

Anyways, this should work better as a tail-recursive (and probably linear time) variant:

def Vector.ofFnInduct {α : Type u} {n : Nat} (f : (k : Fin n) → Vector α k → α) : Vector α n :=
  go 0 (Nat.zero_le _) (Vector.emptyWithCapacity n)
where
  go (k : Nat) (hk : k ≤ n) (v : Vector α k) : Vector α n :=
    if h : k < n then
      go (k + 1) h (v.push (f ⟨k, h⟩ v))
    else
      v.cast (by lia)

That's nice! This implementation is very similar to what I wrote, if you ignore the fact that it uses Vector instead of an Array. But thanks to a different assumption in the recursive function it ended up being much simpler and not requiring special case for 0.

[Jakub Nowak]

Ah, it's also simpler because the proof that v.push (f ⟨k, h⟩ v) has length k + 1 passes by just defeq on types.