Floats and reals

Stream: general

[Patrick Massot]

Junyan Xu said:

The author is apparently on this Zulip but the last activity was in 2019 ...

This is really painful to read. I know that we are all participating in a giant quest going far beyond individual contributions. But it would be really nice to find a way to pass around the history of this quest. Junyan, I'm not blaming you for anything, but I want to tell you that nothing you see here would exist without Johannes Hölzl. He was contributing to mathlib before any mathematician joined. He is the one who started the topology library and defined real numbers (that definition was later replaced by another one, but it was used to start a lot of things). He was a strong advocate of (complete)lattices, galois connections and filters. His views still have a very profound impact on today's mathlib, and will continue in mathlib4.

[Johan Commelin]

He's also listed as emeritus at the bottom of https://github.com/leanprover-community/mathlib/

[Eric Wieser]

Something that might be nice to attempt to expose history is to add a "relevant zulip discussions" section to module docstring

[Jihoon Hyun]

Is this something related to real computation and iRRAM? If so please let me know since I once studied about it as an undergrad, and the topic was so much fun!

[Junyan Xu]

Yeah, sorry for being ignorant about the history! I found the name very familiar when I saw the author of the paper, but didn't remember where I'd seen it, so I searched on Zulip, and there are only about 20 messages since my account joined Zulip; if I had clicked to expand the history ("search all public streams") I would get much more results and would not significantly underestimate his contribution. So it could be an improvement Zulip to search all public history by default.

[Jihoon Hyun]

Tell me if I'm wrong, but there are some related implementations in coq, although I have never used it.
One verification of iRRAM on coq I know: https://cp.kaist.ac.kr/jeehoon.kang/
Axiomatic Reals and Certified Efficient Exact Real Computation: https://doi.org/10.1007/978-3-030-88853-4_16

[Martin Dvořák]

I haven't looked into Lean 4 yet, but is my impression correct that Lean 4 doesn't require as much boilerplate as Lean 3 requires when it comes to computation with floats?

[Martin Dvořák]

Kevin Buzzard said:

Right -- I'm allowing the bounds to grow -- I'm only asking for inequalities. So the more stuff you do to real numbers the less accuracy you have.

If I understand your suggestions correctly, I believe it cannot work. Your hypothetical functions lower and upper violate the congr_arg property unless you make them return something like -∞ and ∞ respectively.

[Henrik Böving]

Martin Dvořák said:

I haven't looked into Lean 4 yet, but is my impression correct that Lean 4 doesn't require as much boilerplate as Lean 3 requires when it comes to computation with floats?

THey are just a built-in type (that as explained above is a very rudimentary facade for C level floats) with all the operations you'd expect to be defined on floats defined on it you can just start away basically instantly.

[Martin Dvořák]

By "boilerplate" I meant meta and native. in declarations like:

meta def solve_quadratic_equation (a b c : native.float) : list native.float := sorry

[Henrik Böving]

Neither of these keywords do exist anymore in the Lean 4 realm so...yup!

def solveQuadratic (a b c : Float) : List Float :=
  let discr := b^2 - 4 * a * c
  let sol1 := (-b + discr.sqrt) / (2 * a)
  let sol2 := (-b - discr.sqrt) / (2 * a)
  [sol1, sol2]

#eval solveQuadratic 1.5 4 (-120.3)

also note that the compiler is smart enough to figure out all of the duplicate stuff going on here so it is also efficient to write it down like this \o/

[Martin Dvořák]

Martin Dvořák said:

If I understand your suggestions correctly, I believe it cannot work. Your hypothetical functions lower and upper violate the congr_arg property unless you make them return something like -∞ and ∞ respectively.

As you probably can probably imagine, for every real number r and every float f there exists a formula that evaluates to r over reals but to f over floats.

[Kevin Buzzard]

Yes but I was not demanding that evaluation of formulas preserves lower and upper, I was only asking for inequalities, so your observation doesn't contradict what I'm asking for.

[Martin Dvořák]

Then I probably wrongly understood what you meant by lower(f)+lower(g) <= lower (f+g) and similar.

[Mario Carneiro]

Kevin Buzzard said:

Fully expecting the answer no: are there functions lower, upper : Float -> Real with the property that "the real number modelled by f : Float" (whatever that means, if it means anything at all) is in the closed inteval [lower f, upper f] and for all the operations in (whatever operations computer scientists deem are the canonical operations on Float) there are corresponding compatible interval arithmetic theorems in Real, e.g. lower(f)+lower(g) <= lower (f+g) and upper(f+g) <= upper(f)+upper(g)?

Looking again at this, I guess the inequalities are pointing in the right direction, but I think it is still not satisfied because of examples that go out of range. For example, if I have a finite float x somewhere above the square root of the largest finite float, then we get x * x = +inf so upper(x*x) = ∞ > upper(x) * upper(x) = (x + ε) ^ 2

[Mario Carneiro]

that's assuming that upper(+inf) = ∞, which seems reasonable, as well as that upper(x) is finite (it's a middling finite number so this also seems reasonable). As long as there is any boundary where upper goes from being finite to being infinite you can play the same trick, so you end up arguing that upper(x) = ∞ for all x

[Kevin Buzzard]

The product of two floats can be +infinity??

[Martin Dvořák]

Yes.

[Martin Dvořák]

After a short experimentation, I can see that addition of two floats can lead to ∞ too.
Let M be the largest possible float and x be a positive float.
Then M+x evaluates either to M or to ∞.
It seems that (I am not sure about the following) M+x ends up being M when x is small enough so that M-x = M.
If M - (M-x) gives a positive number, then M+x evaluates to ∞.

[Junyan Xu]

It's called "overflow" as in Stack Overflow or MathOverflow.

[Martin Dvořák]

Yeah. Computers are merciless.

[Junyan Xu]

Oh wait, stack overflow is a different kind of overflow, like memory overflow.

[Kevin Buzzard]

If infinity is a float then does one have to use ereal to model them? :-/

[Joseph Myers]

IEEE 754 (see 3.2 in IEEE 754-2019) defines four specification levels. Level 1 "Extended real numbers" corresponds to ereal. Level 2 "Floating-point data" adds NaN and distinguishes positive and negative 0. Level 3 "Representations of floating-point data" represents finite numbers as (sign, exponent, significand) (so also distinguishing different quantum exponents for the same real number, in the decimal floating-point case) and also distinguishes qNaN from sNaN; almost all IEEE 754 operations have fully defined results at this level, modulo implementation choices such as tininess detection before or after rounding (there are a few cases where results aren't fully specified, e.g. quantum exponents for minimum/maximum operations). Level 4 is "Bit strings", which brings in choices of NaN signs and payloads (relevant if you want to model the exact semantics of machine instructions, not so relevant for most analysis of floating-point algorithms at a higher level than individual machine instructions) as well as non-canonical decimal encodings in certain cases.

[Mario Carneiro]

I would be inclined to level 3 there for a formalized float library on the level of say flocq

[Mario Carneiro]

I think you can't really do level 4 unless you explicitly select various architectures to implement

[Mario Carneiro]

and if you want it to correspond to lean code using Float then even that's not sufficient because the programs have to propagate through a compiler like LLVM which has its own ideas about float semantics

[Joseph Myers]

I'd agree that level 3 is probably the right level for most floating-point formalization purposes, with explicit parameters somewhere for such things as "is tininess detected before or after rounding" (only relevant for exceptions, not the floating-point results) and "does fma(0, Inf, NaN) raise invalid" (likewise) and for operations where level 3 operands don't fully determine level 3 results (copySign copying the sign from a NaN operand, min/max operations with decimal operands with the same value and sign but different quantum exponents).

[Mario Carneiro]

for functions that are not deterministic at level 3 (most explicitly, toBits, but also things like copySign), I think it is best to represent them explicitly as nondeterministic functions and not attempt to treat them as opaque functions like is currently done in Float, because even opaque functions are functions and I don't think this is a safe assumption - the same operation on the same inputs can yield different results depending on whether it was evaluated by LLVM or the target machine (or the other target machine because it was compiled into an olean and then moved to another architecture)

[Joseph Myers]

Or as another example, on x86, the rules for choice of NaN result given two NaN operands are different for x87 (larger payload) and SSE (based on order of operands to the instruction).

[Martin Dvořák]

Mario Carneiro said:

for functions that are not deterministic at level 3 (most explicitly, toBits, but also things like copySign), I think it is best to represent them explicitly as nondeterministic functions (...)

What is the most idiomatic way to deal with handle nondeterministic functions in Lean?

[Mario Carneiro]

It's a bit annoying to work with but the most direct representation of nondeterminism that is available to the lean logic is Quot

[Mario Carneiro]

So you can for example use Squash Bool (Squash being the quotient by the true relation, called trunc in lean 3) to represent a nondeterministic boolean value

[Mario Carneiro]

to the lean compiler, Squash Bool is just the same as Bool, but to the logic Squash Bool is a type with (provably) only one element

[Alistair Tucker]

In another thread someone (possibly someone unreliable) said:

You may want to resolve this issue by making your functions polymorphic; your proofs will apply to the Real version but you can use the Float version to get numbers out.

Is that in fact a reasonable plan of action to address the question raised at the top of this thread?

[Alistair Tucker]

Or would it have to involve some metaprogram as @Henrik Böving suggests

[Martin Dvořák]

OT: Do we really want to compare floats to reals? They are almost a subset of rational numbers. Why don't we compare floats to rationals instead?

[Trebor Huang]

When I talk about floats with my CS friends they keep telling me that floats are terrible.

[Martin Dvořák]

They are terrible but useful.

[Martin Dvořák]

They are so useful that we might want to start to care about them.

[Trebor Huang]

I think the best we can do is

• Make a "Float or Real" typeclass for a quick relation between them, we prove stuff about the real version, and use the float version.
• Metaprogramming to replace reals with floats.
• Formalize IEEE standards.

There will not be a set of workhorse theorems that are easy to use, like to give a concise bound of errors.

[Eric Wieser]

I suppose that typeclass would look something like

class FloatOrReal (R) extends Add R, Mul R where
  sqrt : R →R
  sin : R →R
  // and every other function in the IEEE spec

[Alistair Tucker]

I guess I’m not clear on exactly what the metaprogram would be translating

[Eric Wieser]

Yeah, the whole point in the typeclass would be to avoid the need to do any translation

[Henrik Böving]

Alistair Tucker said:

Or would it have to involve some metaprogram as Henrik Böving suggests

The meta program would be a more extreme version of the typeclass approach where we could add arbitrary custom things into the "polymorphism" basically. It might very well be that the TC approach is completely sufficient.

[Tyler Josephson ⚛️]

Thanks for all the discussion, everyone! I'm learning a lot here.

[Tyler Josephson ⚛️]

We almost have data.real.basic finished porting, and I'd try this for myself if it were. But I'm curious - what should happen if one imported the real numbers and then executed:
#eval (1 / 3 : Real)
Would Lean run forever, increasing the precision of 0.3333... without end? Or would it fail to compile, because it has no guarantee that such a computation will halt? If the Lean code were compiled to C, what would be the type of the result?

[Mario Carneiro]

If implemented directly the way it is in mathlib, Real is a cauchy sequence of rationals, so computationally it's a Nat -> Rat function. There is even a meta instance for real which ignores the quotient to get at the function and then prints the first 5 or so values, so if you #eval (1 / 3 : real) you see [1/3, 1/3, 1/3, 1/3, 1/3, ...]

[Mario Carneiro]

I don't think we can safely do this in lean 4 though. We can have it as an unsafe instance : Repr Real but ignoring a quotient is not a safe operation, you can cause false proofs in native_decide with it

[Tyler Josephson ⚛️]

Okay, that's helpful. The output of the function is Rat so it wouldn't even try to resolve it into a decimal representation, it would compute and show the resulting Rat itself.

[Tyler Josephson ⚛️]

So to check my understanding:
For computing (approximate) decimal representations, we should convert the real number into a float (by extending the real typeclass to a float typeclass, or through metaprogramming). The resulting type would correspond to precisely-described IEEE standards, which would allow us to compute decimal representations safely (i.e. no false proofs). We wouldn't need to prove things about the numerical properties of floats, but we could if we wanted to.

[Eric Wieser]

docs#real is a type not a typeclass

[Eric Wieser]

There is of course docs#conditionally_complete_linear_ordered_field which uniquely characterizes the reals, but floats come nowhere close to satisfying it.

[Marc Huisinga]

On a semi-related note, the semantics of the SMT-LIB float theory are described in An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic (it targets level 2).

[Thomas Murrills]

In case it’s useful as a case study or for inspiration, there’s this package for validated numerics in Julia, which is capable of quite a bit!