Float.floor

Stream: lean4

[Marcus Rossel]

Is there some kind of flooring function for Float (preferably returning a Nat)?
I'm trying and struggling to express the inverse to Cantor's pairing function.

[Kevin Buzzard]

Whatever does Float have to do with Cantor's pairing function? You know that there are infinitely many naturals but only finitely many floats, right?

[Marcus Rossel]

The inverse to Cantor's pairing function requires a square root and a floor. So I was just looking for something in Lean 4 that allows me to take a square root.
I'm not trying to prove any theorems about the definition.

[Kevin Buzzard]

The inverse to Cantor's pairing function does not require floats (or reals). Your reference for it does. Just use nat.sqrt. Port it from Lean 3, I doubt it's in Lean 4 yet but it would be a fun exercise.

[František Silváši]

For floor you can always cheat if you don't mind the linear complexity. def poorMansFloor (x : Float) := x.toString.takeWhile (·≠'.')

[Kevin Buzzard]

Just glancing over the Wikipedia ref you posted, it seems that the issue is that given a natural $z$ you want to find $x$ and $y$ such that $z=\pi(x,y)$. The definition of $\pi(x,y)$ is "some triangular number, + y", and the triangular number is the largest triangular number which is $\leq z$. So what you _really_ need is a good algorithm to find the largest triangular number (i.e. number of the form $w(w+1)/2$) which is at most $z$. So you need to find the largest natural $w$ such that $(2w+1)^2\leq 8z+1$. You don't need floats or reals for that, you could knock up a dumb algorithm easily and a smarter algorithm with some work.

[Xubai Wang]

You can also use

def Float.toNat (x : Float) : Nat :=
  x.toUInt64.toNat

but it seems that Float is not meant for mathematical use.

[Kevin Buzzard]

For example you could start with 1 and then keep adding powers of 2 and backtrack when you go over.

[Kevin Buzzard]

(the dumb algorithm is just to start with 1 and then keep adding 2 until you go over)

[Mario Carneiro]

FYI the inverse to cantor's pairing function is implemented in lean 3, see src#nat.unpair

[Mario Carneiro]

also src#nat.sqrt if you are interested in how to do sqrt without floats

[Kevin Buzzard]

Looking at the Lean code that looks to me at first sight like it's a different bijection to the one on the Wikipedia page.

[Marcus Rossel]

Thanks for all the feedback :blush:
My purpose for this is really just to have a method for iterating over all tuples in $\mathbb{N}^{26}$.
So I thought a generalized inverse pairing function would do the job :D

[Mario Carneiro]

Oh, actually that's true, this is the box-shaped bijection, not the diagonal one. It just changes a couple constants

[Mario Carneiro]

Note that for high dimensions, iterating the unpairing function results in (inverse) superexponential growth, so you get really biased coverage

[Marcus Rossel]

Awesome! unpair is perfect for my purposes.

[Marcus Rossel]

Mario Carneiro said:

Note that for high dimensions, iterating the unpairing function results in (inverse) superexponential growth, so you get really biased coverage

What does that mean?

[Kevin Buzzard]

The Lean bijection is more convenient than the Wikipedia definition because you don't need "largest odd integer whose square is <= n", you need "largest integer whose square is <= n" , and there's already a name for that.

[Mario Carneiro]

If you map n0, ..., n25 to (((n0, n1), ... n25) then if each ni is O(k) then (n0, n1) is O(k^2), ((n0, n1), n2) is O((k^2)^2), and so on so that (((n0, n1), ... n25) is O(k^(2^25))

[Mario Carneiro]

Which means that if you won't hit (3,3,3, ..., 3) until about 3^(2^25)

[Marcus Rossel]

Hmmm... I guess I didn't consider the number of combinations :sweat_smile:

[Mario Carneiro]

A much more balanced way to hit the numbers is to convert every number into binary and then read a sequence like 101,10,111,...,1000 as a number written in ternary on the alphabet 0 1 ,

[Mario Carneiro]

I think that is within a constant factor of optimal; you can do a bit better to encode the fact that there are exactly 25 ,'s

[Mario Carneiro]

but depending on what you are doing that may or may not be important

[Marcus Rossel]

Ok now I'm not sure if we're talking about the same thing :sweat_smile:
I have a function with 26 inputs f (a b c ... x y z : Nat) : Int and would like to systematically go through all input combinations (I'm aware that there are infinitely many).

[Mario Carneiro]

Yes, that's what I'm talking about too

[Mario Carneiro]

I'm pointing out that within such functions, there is still a notion of optimality, where we ask that for small inputs we want small outputs

[Mario Carneiro]

you get okay results with iterated unpairing if you split the coordinates in a balanced way

[Marcus Rossel]

Ahhh, now I get it

[Mario Carneiro]

for a lot of theoretical purposes, it literally doesn't matter at all what the growth rate of the function is, in which case iterated unpairing is the simplest implementation

[Mario Carneiro]

and in fact that's what mathlib does in its encodable instances

[Marcus Rossel]

Now I just have to figure out how to convert Nat into a list of ternary digits

[Mario Carneiro]

src#encodable.encode_list

[Mario Carneiro]

see src#nat.digits for converting a nat into a list of digits

[Mario Carneiro]

Another variation is the high-dimensional analogue of cantor's bijection, where you iterate over the level sets of $x_0+x_1+x_2+...+x_{25}=k$

[Mario Carneiro]

I think you need inverse nth roots to express the inverse function though

[Kevin Buzzard]

Iterate over max<=k rather than sum<=k to make the inverse function nicer

[Marcus Rossel]

Actually, I don't get it ....
If I have a natural number n that I want to convert into a 26-tuple (a, b, c, ..., x, y, z), I first interpret n as ternary over symbols 0, 1 and ,. Let's say n = 01,1,001. How do I extract a to z from this? Since n's representation doesn't contain 25 ,s I don't know where to "split" n.

[Mario Carneiro]

Kevin Buzzard said:

Iterate over max<=k rather than sum<=k to make the inverse function nicer

I think you need the inverse nth root regardless, because the volume of a 26 dimensional box and a 26 dimensional simplex both grows as n^26

[Kevin Buzzard]

yes, but with the triangular one you need more than 26th root, you need "inverse of some random degree 26 polynomial"

[Kevin Buzzard]

like we needed inverse of triangular number for the Wikipedia version, but we could complete the square.

[Mario Carneiro]

aha

[Mario Carneiro]

yes, that will be a problem for d >= 5

[Kevin Buzzard]

:-)

[Kevin Buzzard]

Given that 3^26 is quite a big number, maybe a table of small values will be fine :-)

[Mario Carneiro]

@Marcus Rossel Are you allowed to have a partial inverse, because that will make things easier. You can just reject inputs that don't have 25 ,'s

[Mario Carneiro]

One way to enforce this is with some kind of stars-and-bars way of enumerating exactly where to place the commas. But at that point the high dimensional cantor is looking like a simpler solution

[Mario Carneiro]

Actually balanced unpair is much simpler. You are off from optimal by a polynomial factor depending on the amount of unbalance in the tree, which can't be perfect because 26 isn't a power of two, but that should only be something like O(n^0.4) or so from optimal, which is probably passable for practical use (certainly it's much better than n^(2^25))

[Mario Carneiro]

If you have 26 elements of O(k), then the result is O(k^32), where the optimal is O(k^26), so it's off by a factor $O(n^{3/13}) \le O(n^{0.24})$