Data.SBV.Examples.Misc.Floating

Several examples involving IEEE-754 floating point numbers, i.e., single precision Float (SFloat) and double precision Double (SDouble) types.

Note that arithmetic with floating point is full of surprises; due to precision issues associativity of arithmetic operations typically do not hold. Also, the presence of NaN is always something to look out for.

FP addition is not associative

assocPlus :: SFloat -> SFloat -> SFloat -> SBool

Prove that floating point addition is not associative. We have:

>>> prove assocPlus
Falsifiable. Counter-example:
  s0 = -Infinity :: SFloat
  s1 = Infinity :: SFloat
  s2 = -9.403955e-38 :: SFloat

Indeed:

>>> let i = 1/0 :: Float
>>> ((-i) + i) + (-9.403955e-38) :: Float
NaN
>>> (-i) + (i + (-9.403955e-38)) :: Float
NaN

But keep in mind that NaN does not equal itself in the floating point world! We have:

>>> let nan = 0/0 :: Float in nan == nan
False

assocPlusRegular :: IO ThmResult

Prove that addition is not associative, even if we ignore NaN/Infinity values. To do this, we use the predicate isFPPoint, which is true of a floating point number (SFloat or SDouble) if it is neither NaN nor Infinity. (That is, it's a representable point in the real-number line.)

We have:

>>> assocPlusRegular
Falsifiable. Counter-example:
  x = 1.5775295e-30 :: SFloat
  y = 1.92593e-34 :: SFloat
  z = -2.1521e-41 :: SFloat

Indeed, we have:

>>> (1.5775295e-30 + 1.92593e-34) + (-2.1521e-41) :: Float
1.5777222e-30
>>> 1.5775295e-30 + (1.92593e-34 + (-2.1521e-41)) :: Float
1.577722e-30

Note the loss of precision in the second expression.

FP addition by non-zero can result in no change

nonZeroAddition :: IO ThmResult

Demonstrate that a+b = a does not necessarily mean b is 0 in the floating point world, even when we disallow the obvious solution when a and b are Infinity. We have:

>>> nonZeroAddition
Falsifiable. Counter-example:
  a = -4.0 :: SFloat
  b = 4.5918e-41 :: SFloat

Indeed, we have:

>>> -4.0 + 4.5918e-41 == (-4.0 :: Float)
True

But:

>>> 4.5918e-41 == (0 :: Float)
False

FP multiplicative inverses may not exist

multInverse :: IO ThmResult

The last example illustrates that a * (1/a) does not necessarily equal 1. Again, we protect against division by 0 and NaN/Infinity.

We have:

>>> multInverse
Falsifiable. Counter-example:
  a = 1.3999060872492817e-308 :: SDouble

Indeed, we have:

>>> let a = 1.3999060872492817e-308 :: Double
>>> a * (1/a)
0.9999999999999999