Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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 -> SBool Source

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

`>>>`

Falsifiable. Counter-example: s0 = -7.888609e-31 :: SFloat s1 = 3.944307e-31 :: SFloat s2 = NaN :: SFloat`prove assocPlus`

Indeed:

`>>>`

`let i = 0/0 :: Float`

`>>>`

NaN`((-7.888609e-31 + 3.944307e-31) + i) :: Float`

`>>>`

NaN`(-7.888609e-31 + (3.944307e-31 + i)) :: Float`

But keep in mind that `NaN`

does not equal itself in the floating point world! We have:

`>>>`

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

assocPlusRegular :: IO ThmResult Source

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:

`>>>`

Falsifiable. Counter-example: x = -3.7777752e22 :: SFloat y = -1.180801e18 :: SFloat z = 9.4447324e21 :: SFloat`assocPlusRegular`

Indeed, we have:

`>>>`

-2.83342e22`((-3.7777752e22 + (-1.180801e18)) + 9.4447324e21) :: Float`

`>>>`

-2.8334201e22`(-3.7777752e22 + ((-1.180801e18) + 9.4447324e21)) :: Float`

Note the loss of precision in the first expression.

# FP addition by non-zero can result in no change

nonZeroAddition :: IO ThmResult Source

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:

`>>>`

Falsifiable. Counter-example: a = 2.1474839e10 :: SFloat b = -7.275957e-11 :: SFloat`nonZeroAddition`

Indeed, we have:

`>>>`

True`2.1474839e10 + (-7.275957e-11) == (2.1474839e10 :: Float)`

But:

`>>>`

False`-7.275957e-11 == (0 :: Float)`

# FP multiplicative inverses may not exist

multInverse :: IO ThmResult Source

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:

`>>>`

Falsifiable. Counter-example: a = 1.2354518252390238e308 :: SDouble`multInverse`

Indeed, we have:

`>>>`

`let a = 1.2354518252390238e308 :: Double`

`>>>`

0.9999999999999998`a * (1/a)`