Performant code + recursion

Stream: lean4

[Wrenna Robson]

(deleted)

[Henrik Böving]

I'm assumign you posted too early? Otherwise there is a bug and i can't see it

[Wrenna Robson]

I have the following code:

import Mathlib

def foo (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => ![0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
    8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16] i
| (n + 1) => (foo n) (foo n i)

#eval foo 2 1

I can't get this eval to actually resolve - it seems there's some kind of issue with my recursion I guess - but this really doesn't look unreasonable to me. Any tips on how to fix this?

[Wrenna Robson]

@Henrik Böving ah! Yes I must have hit enter?

[Wrenna Robson]

Posted the message now :)

[Henrik Böving]

Perm doesn't resolve for me, what namespaces do you have open?

[Wrenna Robson]

Ah, Equiv I think

[Henrik Böving]

image.png

that's not enough^^

[Henrik Böving]

You can try out your MWEs on live.lean-lang.org to see if they work in a bare environment

[Wrenna Robson]

I have adjusted my MWE :)

[Wrenna Robson]

I am not sure how to minimise the imports but that isn't so important.

[Wrenna Robson]

Basically, given some function f : A -> A, I want to calculate doublings of f. And f is concretely defined and this is on a nice finite type and so forth.

[Henrik Böving]

Right, I'm assuming that ![] is a mathlib type? I would not be surprised if it is not at all made for evaluation and suffers from very poor performance characteristics tbh

[Yaël Dillies]

file#Data/Fin/VecNotation

[Wrenna Robson]

It's notation for Fin n -> A tuples.

[Wrenna Robson]

Ah thanks! Couldn't remember the file it was defined in.

[Markus Himmel]

This doesn't seem to be related to the recursion, #eval ![0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24, 8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16] 31 is already slow

[Henrik Böving]

import Mathlib

def foo (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => #[0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
    8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16][i]
| (n + 1) => (foo n) (foo n i)

 #eval foo 2 1

so if I use an array here (If i understand correctly this is the proper translation? This computation basically runs instantly

[Wrenna Robson]

import Mathlib.Data.Fin.VecNotation

#eval (![0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
    8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16])
    (![0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
    8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16] (0 : Fin 32))

And this doesn't evaluate I think.

[Henrik Böving]

So if you want to do this I would suggest either use a proper data structure like array or figure out how to make this vecnotation yield performant code

[Mario Carneiro]

I don't think the iterated call is the issue:

set_option profiler true
#eval foo 0 0
#eval foo 0 1
#eval foo 0 2
#eval foo 0 3
#eval foo 0 4
#eval foo 0 5
#eval foo 0 6
#eval foo 0 7
#eval foo 0 8
#eval foo 0 9
#eval foo 0 10
#eval foo 0 11
#eval foo 0 12
#eval foo 0 13
#eval foo 0 14
#eval foo 0 15
#eval foo 0 16
#eval foo 0 17
#eval foo 0 18
#eval foo 0 19 -- 118ms
#eval foo 0 20 -- 268ms
#eval foo 0 21 -- 619ms
#eval foo 0 22 -- 1.05s
#eval foo 0 23 -- 1.91s
#eval foo 0 24 -- 2.57s
#eval foo 0 25 -- 7.52s
#eval foo 0 26 -- 9.98s
#eval foo 0 27 -- 20.1s
#eval foo 0 28 -- ...
#eval foo 0 29
#eval foo 0 30
#eval foo 0 31

[Wrenna Robson]

Henrik Böving said:

import Mathlib

def foo (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => #[0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
    8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16][i]
| (n + 1) => (foo n) (foo n i)

 #eval foo 2 1

so if I use an array here (If i understand correctly this is the proper translation? This computation basically runs instantly

This doesn't surprise me! Is an array of fixed size?

[Henrik Böving]

You can grow arrays as you want. They are what Rust or C++ would call a Vec

[Wrenna Robson]

Right. Essentially I'm concerned with, if you like, arrays of fixed size, analogous to Fin n -> A. The latter is easy to work with, but as I am finding, extremely not perfomant.

[Wrenna Robson]

Naively I thought it would be :)

[Henrik Böving]

You can define a subtype { xs : Array a // xs.size = n} if you want. Iirc some batteries people are working on bulding some API around this notion but you can live without that if you just want to index into it

[Wrenna Robson]

It is just a little embarassing as nominally I have implemented a "faster" version of another function, but in fact it is not faster in practice because of this.

[Henrik Böving]

I have a feeling that you won't be able to convince mathlib of designing their abstractions such that they are performant for evaluation :P

[Wrenna Robson]

In a sense what I want to do is "load" the values of a "f : Fin n -> A" into an array and work with that.

[Henrik Böving]

docs#Array.ofFn this exists!

[Wrenna Robson]

Henrik Böving said:

I have a feeling that you won't be able to convince mathlib of designing their abstractions such that they are performant for evaluation :P

This is for a personal project (for my thesis...) rather than anything that will be in mathlib.

[Wrenna Robson]

Ah very nice.

[Wrenna Robson]

Difficult to go the other way ofc

[Wrenna Robson]

but that might be fine.

[Henrik Böving]

Why? You can just partially apply docs#Array.get and get a Fin array.size -> a

[Mario Carneiro]

It's actually quite difficult to get lean to compute a closure instead of eta-expanding

[Wrenna Robson]

Henrik Böving said:

Why? You can just partially apply docs#Array.get and get a Fin array.size -> a

That is true.

[Wrenna Robson]

Difficult if I need to iterate a permutation into a permutation but I can avoid that here.

[Mario Carneiro]

This does seem to compile as desired:

def myArray := #[0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
    8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16]
def foo (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => myArray.get i
| (n + 1) => foo n (foo n i)

#eval foo 0 31

[Wrenna Robson]

Aye. But I do need to start with a function for my context, and this doesn't.

def myArray : Array (Fin 32) :=
    Array.ofFn ![0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
      8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16]

def foo (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => myArray.get i
| (n + 1) => (foo n) (foo n i)

#eval foo 0 31

[Wrenna Robson]

In a sense it feels like I want to - I want it to, I guess this is what you mean by compute the closure - I want it to fully compute that array, rather than be lazy about it

[Wrenna Robson]

Incidentally, this starts getting slow again:

def myArray : Array (Fin 32) :=
   #[0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
      8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16]

def foo (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => myArray.get i
| (n + 1) => (foo n) (foo n i)

#eval foo 6 31

[Wrenna Robson]

And I think this is the recursion this time.

[Wrenna Robson]

Oh except now it works on recompile. Shrug!

[Mario Carneiro]

import Mathlib

open Equiv
def Perm.fromArray {n} (a : Array (Fin n)) (b : Array (Fin n))
    (ha : a.size = n := by rfl)
    (hb : b.size = n := by rfl)
    (ab : ∀ i : Fin n, b.get ((a.get (i.cast ha.symm)).cast hb.symm) = i := by decide) :
    Perm (Fin n) where
  toFun i := a.get (i.cast ha.symm)
  invFun i := b.get (i.cast hb.symm)
  left_inv := ab
  right_inv := Function.LeftInverse.rightInverse_of_card_le
    (f := fun i => b.get (i.cast hb.symm)) (g := fun i => a.get (i.cast ha.symm)) (ab ·) le_rfl

def controlBits4_perm : Perm (Fin 32) :=
  Perm.fromArray
    #[0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
      8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16]
    #[0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26,
      28, 30, 31, 29, 27, 25, 23, 21, 19, 17, 15, 13, 11, 9, 7, 5, 3, 1]

def controlBits4_perm_powers (n : ℕ) (i : Fin 32) : Fin 32 :=
match n with
| 0 => controlBits4_perm i
| (n + 1) => (controlBits4_perm_powers n) (controlBits4_perm_powers n i)

#eval controlBits4_perm_powers 6 31

[Wrenna Robson]

Very nice.

[Wrenna Robson]

Somewhat more simply, I had luck with this:

def myArray : Array (Fin 32) :=
   #[0, 31, 1, 30, 2, 29, 3, 28, 4, 27, 5, 26, 6, 25, 7, 24,
      8, 23, 9, 22, 10, 21, 11, 20, 12, 19, 13, 18, 14, 17, 15, 16]

def myInvArray : Array (Fin 32) :=
   #[0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26,
    28, 30, 31, 29, 27, 25, 23, 21, 19, 17, 15, 13, 11, 9, 7, 5, 3, 1]

def controlBits4_perm : Perm (Fin 32) where
  toFun := myArray.get
  invFun := myInvArray.get
  left_inv s := by fin_cases s <;> rfl
  right_inv s := by fin_cases s <;> rfl

[Wrenna Robson]

So it does seem the key is: start it as an Array!

[Mario Carneiro]

you can use by decide instead of fin_cases

[Wrenna Robson]

ah thanks

[Mario Carneiro]

(my version saves on checking one of the two conditions because of the pigeonhole principle)

[Wrenna Robson]

by decide doesn't work for me because of the free variable.

[Mario Carneiro]

don't introduce it

[Wrenna Robson]

Oh I see

[Wrenna Robson]

Very nice :)

[Wrenna Robson]

I wonder if you could generalise beyond the fins.

[Wrenna Robson]

Anyway: may I use this code? It's a nice efficient implementation.

[Mario Carneiro]

yes please, that's why I wrote it

[Wrenna Robson]

It seemed polite to double check.

[Wrenna Robson]

I am glad I asked about this!

[Mario Carneiro]

You can't generalize beyond the fins, because that's how arrays work. If you want to use another type you should just pre/postcompose with an equiv

[Wrenna Robson]

Right! As it happens I don't need that so it's all good.

[Wrenna Robson]

@Mario Carneiro I have another function (I won't get into the details) that I am struggling to evaluate successfully for larger inputs. Is there a way to see where a function is bottlenecking? It would be good to understand what the slow parts of my code actually are.

[Henrik Böving]

You can compile them to a binary and use a profiler like perf + hotspot to check where you are spending most time in

[Wrenna Robson]

Aha