Floats are inconsistent

[mr-infty]

Steps to reproduce:

module Main

%default total

minusZeroEqualsZero : negate 0.0 = 0.0
minusZeroEqualsZero = Refl

minusInftyEqualsPlusInfty : recip (negate 0.0) = recip 0.0
minusInftyEqualsPlusInfty = cong recip minusZeroEqualsZero

f : Double -> Bool
f x = x < 0

trueEqualsFalse' : f (recip (negate 0.0)) = f (recip 0.0)
trueEqualsFalse' = cong f minusInftyEqualsPlusInfty

fInftyEqualsFalse : f (recip 0.0) = False
fInftyEqualsFalse = Refl

fMinusInftyEqualsTrue : f (recip (negate 0.0)) = True
fMinusInftyEqualsTrue = Refl

trueEqualsFalse : True = False
trueEqualsFalse = trans (sym fMinusInftyEqualsTrue) $ trans trueEqualsFalse' fInftyEqualsFalse

voidIsInhabited : Void
voidIsInhabited = uninhabited trueEqualsFalse

infix 10 ^
(^) : Nat -> Nat -> Nat
(^) x Z = 0
(^) x (S n) = (x^n) * x

fermatsLastTheorem : (n : Nat) -> (3 <= n = True) ->
                     (x,y,z : Nat) -> (x <= 1 = True) -> (y <= 1 = True) ->
                     (x^n + y^n = z^n) -> Void
fermatsLastTheorem n pf_n x y z pf_x pf_y pf = voidIsInhabited

main : IO ()
main = do putStrLn "I have discovered a truly remarkable proof of this theorem that even fits in this margin."

Expected behaviour

You shouldn't be able to prove that -0.0 equals 0.0.

[gallais]

:fireworks:

@wenkokke will be happy to see that Idris' floats are extremely powerful.

[RyanGlScott]

This seems reminiscent of this Idris 1 bug, where one could also prove that -0.0 = 0.0. My best guess on how to fix this issue, based off the corresponding fix in Idris 1, is that this line of code would need to be changed:

https://github.com/idris-lang/Idris2/blob/969f5443a9a728e9f8fa9709c5d893324a140f16/src/Core/TT.idr#L131

I'm assuming that (==) treats 0.0 and -0.0 as equal. Does Idris provide a version of floating-point equality that checks for identical bitpatterns?

[gallais]

Does Idris provide a version of floating-point equality that checks for identical bitpatterns?

We have a cast from Double to both Int and Integer which I assume do this? It would be nicer to have a proper one to Bits64 though.

[wenkokke]

@gallais That cast might just round the Double, though?

[gallais]

Yeah, you're right. :/

Main> the Integer (cast $ the Double 1.2)
1
Main> the Int (cast $ the Double 1.2)
1

[wenkokke]

Honestly, if Idris2 is implemented in Idris2, and Idris2 doesn't have the ability to distinguish -0.0 and 0.0, then this might end up being a pain to fix.

[gallais]

Clearly recip is a way to distinguish them. :angel:

[RyanGlScott]

I did some digging, and this is how (==) for Double is implemented:

(define prim__eq_Double (lambda (arg-0 arg-1) (or (and (= arg-0 arg-1) 1) 0)))

So we may just need to concoct a variation of this that uses bitwise equality (i.e., what the identicalIEEE function does in Haskell) instead of =. I'm not a Scheme expert, but I think eqv? might fit the bill here.

[plt-amy]

I'm not a Scheme expert, but I think eqv? might fit the bill here.

Aye, this is the function you'd want. R7RS says:

The eqv? procedure returns #f if: [...] obj1 and obj2 are both inexact numbers such that either they are numerically unequal (in the sense of =), or they do not yield the same results (in the sense of eqv?) when passed as arguments to any other procedure that can be defined as a finite composition of Scheme’s standard arithmetic procedures, provided it does not result in a NaN value. As an exception, the behavior of eqv? is unspecified when both obj1 and obj2 are NaN.

[samth]

Furthermore, both Chez and Racket make (eqv? nan.0 nan.0) true, which is probably what you want (although maybe not?).

[RyanGlScott]

Cool, then eqv? sounds like a promising direction. I'm not quite sure how to modify the Scheme bootstrapping code, however. The files bootstrap/idris2_app/idris2.{rkt,ss} (which contain the definition of prim__eq_Double, among other things) appear to be autogenerated, and I'm unclear as to what generated them in the first place.

[melted]

The source for the scheme support code is in support/chez/support.ss (and corresponding for racket and gambit). As the compiler itself doesn't rely on it, there is no need for a new bootstrap file.

[melted]

It would also be good to see if the Javascript backend is susceptible.

[wenkokke]

I'd like to add, based on having spent several days trying to nail down similar problems in Agda:

1. Denotational equality on floating-point numbers should be implemented as bitwise equality after unifying NaNs, since NaNs carry information, but that behaviour isn't consistent across platforms. Just eqv won't work.
2. Propositional equalities on floating-point numbers should be discouraged, since their behaviour cannot be guaranteed across backends. See the following Agda program:

   nonDeterministic : let x = 1e308 in x ≡ (x * x) ÷ x
   nonDeterministic = refl
   

   This programs doesn't necessarily typecheck or compile, but whether it does depends on the architecture that you're running on and the optimisations you're applying. Either x * x overflows into Infinity, or it fits in memory, and the equality holds. You can only guarantee consistent proofs on floating-point numbers if you have full control over the way they're executed, and can ensure that they're always truncated to the expected size (e.g., 64 bits) between each and every computation.

If Idris is still going by the ideology of being a programming language first and a proof assistant second, I don't think there's a problem with keeping these inconsistencies as a trade-off for having fast floating-point arithmetic, and just slapping a huge warning on trying to prove things about floating-point arithmetic. It might help to not provide any primitive proofs about the floating-point operators, if they were ever there to begin with.

[mr-infty]

I'd like to add, based on having spent several days trying to nail down similar problems in Agda:

1. Denotational equality on floating-point numbers should be implemented as bitwise equality after unifying NaNs, since NaNs carry information, but that behaviour isn't consistent across platforms. Just eqv won't work.

2. Propositional equalities on floating-point numbers should be discouraged, since their behaviour cannot be guaranteed across backends. See the following Agda program:

   nonDeterministic : let x = 1e308 in x ≡ (x * x) ÷ x
   nonDeterministic = refl
   

   This programs doesn't necessarily typecheck or compile, but whether it does depends on the architecture that you're running on and the optimisations you're applying. Either x * x overflows into Infinity, or it fits in memory, and the equality holds. You can only guarantee consistent proofs on floating-point numbers if you have full control over the way they're executed, and can ensure that they're always truncated to the expected size (e.g., 64 bits) between each and every computation.

If Idris is still going by the ideology of being a programming language first and a proof assistant second, I don't think there's a problem with keeping these inconsistencies as a trade-off for having fast floating-point arithmetic, and just slapping a huge warning on trying to prove things about floating-point arithmetic. It might help to not provide any primitive proofs about the floating-point operators, if they were ever there to begin with.

I don’t agree that type safety and execution efficiency are in opposition. Also, I don‘t think that one needs full knowledge/control over floats (or any other builtin type, for that matter), in order to avoid inconsistency: it should only be necessary to have enough knowledge/control to guarantee the identity proofs that should be admissible, to which the equality between negative zero and positive zero certainly doesn’t belong.

[wenkokke]

@mr-infty Sure, but whether or not the equality x ≡ (x * x) ÷ x holds for a specific floating-point number depends on the size of the number, the architecture, and the compiler flags. If there's any inconsistency between those for the platform you're compiling on and the platform you're running on, you end up with a false identity at runtime.

[mr-infty]

@mr-infty Sure, but whether or not the equality x ≡ (x * x) ÷ x holds for a specific floating-point number depends on the size of the number, the architecture, and the compiler flags. If there's any inconsistency between those for the platform you're compiling on and the platform you're running on, you end up with a false identity at runtime.

Yes. Therefore I would say, it’s unreasonable that such an identity is derivable, i.e. whether or not something type-checks shouldn’t depend on the backend or execution environment.

Also, I think that there is at least potentially a very compelling practical reason to be interested in logically sound propositions about floats, namely numerical solutions to ODEs with guaranteed bounds.

[wenkokke]

@mr-infty Such an identity is derivable for literals by using reflexivity. I'm not talking about the general case, I'm talking about, e.g., 1e308 ≡ (1e308 * 1e308) ÷ 1e308.

[andrevidela]

To me it feels like the ideal solution would be:

• removed the DecEq instance for doubles
• Add a custom error message for trying to use decEq on Doubles saying "Equality on doubles cannot be proven for every platform, use Fractional instead"
• add an optimisation step for Fractional in order to use doubles in the target backend, provided a backend-specific (and hopefully correct) translation. This would be a good opportunity to more formally implement the Nat-optimisation as well

I'm unfamiliar with this topic so I would like your opinion, specially about point 1 and 3:

• would using fractional be acceptable? or does it remove too much control over the low-level representation
• Is there a way to translate from fractional to double in a way that preserves the semantics of IEEE doubles?
• Maybe we should do the opposite, and have a mapping from Double -> Fractional and have a 0-multiplicity proof depending on a runtime Double that is then mapped to a Fractional and that is the subject of the proof?

What do you think?

[mr-infty]

To me it feels like the ideal solution would be:

• removed the DecEq instance for doubles
• Add a custom error message for trying to use decEq on Doubles saying "Equality on doubles cannot be proven for every platform, use Fractional instead"
• add an optimisation step for Fractional in order to use doubles in the target backend, provided a backend-specific (and hopefully correct) translation. This would be a good opportunity to more formally implement the Nat-optimisation as well

I'm unfamiliar with this topic so I would like your opinion, specially about point 1 and 3:

• would using fractional be acceptable? or does it remove too much control over the low-level representation
• Is there a way to translate from fractional to double in a way that preserves the semantics of IEEE doubles?
• Maybe we should do the opposite, and have a mapping from Double -> Fractional and have a 0-multiplicity proof depending on a runtime Double that is then mapped to a Fractional and that is the subject of the proof?

What do you think?

DecEq does not seem to be related to this issue, as far as I can tell.

What do you mean by „Fractional“? Do you mean the interface Fractional, or do you mean fractions of integers?

[andrevidela]

sorry I was under the impression that decEq was the only way to get 0 = -0 but clearly you can just write it down and the compiler will happily accept it.

I didn't mean the Fractional interface, I meant a fraction of integers

[wenkokke]

@andrevidela It's not just equalities between, e.g., 0 and -0. There are single floating-point values which are unstable between Idris at type checking time and Idris backends at execution time.

The solution is to:

1. use a decidable equality based on bitwise equality, and only expose IEEE floating-point comparison as a function to bools;
2. ensure that any functions out of IEEE floating-point numbers behave appropriately around infinities and NaN, e.g., have floor and ceil return a Maybe Integer;
3. truncate the IEEE floating-point numbers to 64 bits after every operation which may result in an overfloat, both in Idris and in every backend.

For an example of (3), see the way we're doing this in Agda: https://github.com/agda/agda/blob/master/src/full/Agda/Utils/Float.hs#L66-L91

[wenkokke]

I understand that (2) and (3) are technically out of scope for this issue, but might as well fix all the floating-point issues in one fell swoop.

[andrevidela]

I see! Thanks for explaining!

[gallais]

Simpler proof of Void:

%default total

zeros : 0.0 === -0.0
zeros = Refl

szeros : "0.0" === "-0.0"
szeros = cong cast zeros

oops : Void
oops = replace {p = P} szeros () where

  P : String -> Type
  P "0.0" = ()
  P _ = Void

[wenkokke]

Idris still uses IEEE equality for ===?

[DemiMarie]

IMO the only reasonable approach (read: approach that does not severely harm performance) is to consider floats to be opaque objects that satisfy a set of axioms. These axioms allow proving that e.g. 1.0 + 1.0 = 2.0 or 0.25 * 4.0 = 1.0, but do not allow for proving -0.0 = 0.0. IEEE 754 equality would be exposed as a function of type Double -> Double -> Bool.

I am not sure what specific set of axioms should be used, but I do not believe Idris should prove anything about:

• Whether denormal numbers are flushed to zero.
• Whether denormal numbers are treated as zero.
• The behavior of NaN payloads in operations.

On at least ARM CPUs, denormals are flushed to zero before rounding.