Printing all float digits

Stream: lean4

[Tyler Josephson ⚛️]

Inspired by this lovely URL, I wanted to see how Lean handles 0.1 + 0.2 using floats.

#eval 0.1 + 0.2only prints 0.300000, truncating the output.
#eval 0.1 + 0.2 > 0.3 returns true, as expected

How can I see all the digits?

[Mario Carneiro]

Okay, this seems to work to extract the exact rational value of a (finite) Float:

import Std.Data.Rat

def toRatParts (f : Float) : Option (Int × Int) :=
  if f.isFinite then
    let (f', exp) := f.frExp
    let x := (2^53:Nat).toFloat * f'
    let v := if x < 0 then
      (-(-x).floor.toUInt64.toNat : Int)
    else
      (x.floor.toUInt64.toNat : Int)
    some (v, exp - 53)
  else none

def toRat (f : Float) : Rat :=
  if let some (v, exp) := toRatParts f then
    if exp ≥ 0 then
      v * ((2^exp.toNat:Nat) : Rat)
    else
      (v : Rat) / ((2^(-exp).toNat : Nat):Rat)
  else 0

def toStringFull (f : Float) : String :=
  if let some (v, exp) := toRatParts f then
    let v' := v.natAbs
    let s := if exp ≥ 0 then
      toString (v' * (2^exp.toNat:Nat))
    else
      let e := (-exp).toNat
      let intPart := v' / 2^e
      let rem := v' % 2^e
      if rem == 0 then
        toString intPart
      else
        let rem := toString ((2^e + v' % 2^e) * 5^e)
        let rem := rem.dropRightWhile (· == '0')
        s!"{intPart}.{rem.extract ⟨1⟩ rem.endPos}"
    if v < 0 then s!"-{s}" else s
  else "not finite"

#eval toRat (0.1 + 0.2 : Float) -- (1351079888211149 : Rat)/4503599627370496
#eval toRat (0.3 : Float)       -- (5404319552844595 : Rat)/18014398509481984

#eval toStringFull (0.1 + 0.2 : Float) -- 0.3000000000000000444089209850062616169452667236328125
#eval toStringFull (0.3 : Float)       -- 0.299999999999999988897769753748434595763683319091796875

[John Velkey ⚛️]

Tyler Josephson ⚛️ said:

Inspired by this lovely URL, I wanted to see how Lean handles 0.1 + 0.2 using floats.

#eval 0.1 + 0.2only prints 0.300000, truncating the output.
#eval 0.1 + 0.2 > 0.3 returns true, as expected

How can I see all the digits?

As far as all digits, I don't know that there's a way to arbitrarily extend the number of decimal digits displayed. Based on quickly skimming through some of the Float documentation, I think that the Lean does the truncation when it's told to display the value (e.g. via # eval), but for mathematical interests it handles further decimals appropriately.
#eval (0.1 + 0.3)*(10.0^24.0)--400000000000000033554432.000000
I tried to see if multiplication like this would "push" v. small decimal values past the decimal to be displayed. I have no idea where these values come from, the decimal zeros are persistent, even when you increase/decrease the exponential term, so I'm skeptical of the exact nature of these values.
#eval (0.1 + 0.3).toString.toList[8]? -- none
I think this is limited for the same reason that I think Lean's display of Floats is limited.
#eval (0.0000000000000000123456 * 10.0^16.0) -- 0.123456
This isn't useful for instances like 0.1 + 0.2where the decimal of interest has an unknown value and location (if it even exists), but shows that Lean does appropriately handle decimals in excess of 6 places.

[Mario Carneiro]

I tried to see if multiplication like this would "push" v. small decimal values past the decimal to be displayed. I have no idea where these values come from, the decimal zeros are persistent, even when you increase/decrease the exponential term, so I'm skeptical of the exact nature of these values.

This fails because Float is a 64-bit floating point value (with 53 bits of mantissa), and numbers in the vicinity of 400000000000000033554432 require more than that many bits of precision to represent. The random numbers at the end are where the precision runs out

[Mario Carneiro]

you can confirm this by noting that 400000000000000033554432 is unusually divisible by 2:

#eval 400000000000000033554432 % 2^26 -- 0
#eval 2^26 -- 67108864

It is in fact the nearest multiple of 2^26 to 400000000000000000000000

[Mario Carneiro]

Oh, and on the subject of 0.30000000000000004.com , it is worth mentioning of course that if you use Rat instead of Float you get the exactly correct answer:

import Std.Data.Rat

#eval (0.1 + 0.2 : Rat)  -- (3 : Rat)/10
#eval (0.3 : Rat)        -- (3 : Rat)/10
#eval (0.1 + 0.2 : Rat) == 0.3 -- true

[Tyler Josephson ⚛️]

Neat, thanks!

[Eric Wieser]

Perhaps someone should write a Lean version of Grisu3 or Dragon4 (numpy uses the latter); this paper has some background.

[Eric Wieser]

Instead of printing _all_ the digits, these are about printing the shortest sequence of digits that parses to the float in question

[Mario Carneiro]

I think https://github.com/ulfjack/ryu is the state of the art. But printing the shortest sequence of digits that reprints is a rather different problem than the one here

[Kevin Buzzard]

Maybe the best way to solve this is to implement computable reals with print functionality and then define a map from floats to computable reals

[François G. Dorais]

This is a bit confounding but printing digits is not computable even for computable reals!

[François G. Dorais]

(You need a subring of R with decidable equality to get around the "table maker's dilemma".)