# Zulip Chat Archive

## Stream: general

### Topic: Floats and reals

#### Patrick Massot (Dec 26 2022 at 10:34):

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 (Dec 26 2022 at 10:41):

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

#### Eric Wieser (Dec 26 2022 at 11:18):

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

#### Jihoon Hyun (Dec 26 2022 at 14:12):

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 (Dec 26 2022 at 16:00):

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 (Dec 26 2022 at 16:26):

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 (Dec 27 2022 at 12:51):

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 (Dec 27 2022 at 13:05):

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 (Dec 27 2022 at 13:10):

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

computationwith 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 (Dec 27 2022 at 13:17):

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 (Dec 27 2022 at 13:36):

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 (Dec 27 2022 at 13:40):

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 (Dec 27 2022 at 13:59):

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 (Dec 27 2022 at 14:01):

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

and similar.

#### Mario Carneiro (Dec 27 2022 at 16:42):

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 (Dec 27 2022 at 16:45):

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 (Dec 27 2022 at 16:59):

The product of two floats can be +infinity??

#### Martin Dvořák (Dec 27 2022 at 17:04):

Yes.

#### Martin Dvořák (Dec 27 2022 at 17:22):

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 (Dec 27 2022 at 17:29):

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

#### Martin Dvořák (Dec 27 2022 at 17:35):

Yeah. Computers are merciless.

#### Junyan Xu (Dec 27 2022 at 17:36):

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

#### Kevin Buzzard (Dec 27 2022 at 17:51):

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

#### Joseph Myers (Dec 27 2022 at 18:14):

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 (Dec 27 2022 at 18:17):

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

#### Mario Carneiro (Dec 27 2022 at 18:18):

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

#### Mario Carneiro (Dec 27 2022 at 18:20):

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 (Dec 27 2022 at 18:29):

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 (Dec 27 2022 at 18:33):

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 (Dec 27 2022 at 18:35):

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 (Dec 27 2022 at 19:18):

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

explicitlyas nondeterministic functions (...)

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

#### Mario Carneiro (Dec 27 2022 at 19:25):

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 (Dec 27 2022 at 19:27):

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 (Dec 27 2022 at 19:29):

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 (Dec 28 2022 at 08:43):

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 (Dec 28 2022 at 08:46):

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

#### Martin Dvořák (Dec 28 2022 at 08:56):

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 (Dec 28 2022 at 08:57):

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

#### Martin Dvořák (Dec 28 2022 at 08:58):

They are terrible but useful.

#### Martin Dvořák (Dec 28 2022 at 08:58):

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

#### Trebor Huang (Dec 28 2022 at 09:01):

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 (Dec 28 2022 at 09:46):

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 (Dec 28 2022 at 09:49):

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

#### Eric Wieser (Dec 28 2022 at 09:58):

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

#### Henrik Böving (Dec 28 2022 at 12:58):

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 ⚛️ (Dec 28 2022 at 14:18):

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

#### Tyler Josephson ⚛️ (Dec 28 2022 at 14:24):

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 (Dec 28 2022 at 14:28):

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 (Dec 28 2022 at 14:34):

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 ⚛️ (Dec 28 2022 at 14:48):

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 ⚛️ (Dec 28 2022 at 14:50):

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 (Dec 28 2022 at 15:41):

docs#real is a type not a typeclass

#### Eric Wieser (Dec 28 2022 at 15:42):

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 (Dec 28 2022 at 18:33):

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 (Jan 01 2023 at 20:31):

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!

Last updated: Dec 20 2023 at 11:08 UTC