Stability | experimental |
---|---|
Maintainer | erkokl@gmail.com |
Safe Haskell | None |
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.
- assocPlus :: SFloat -> SFloat -> SFloat -> SBool
- assocPlusRegular :: IO ThmResult
- nonZeroAddition :: IO ThmResult
- multInverse :: IO ThmResult
FP addition is not associative
assocPlus :: SFloat -> SFloat -> SFloat -> SBoolSource
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 ThmResultSource
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 ThmResultSource
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 ThmResultSource
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