# A bug with Sum (as in Monoid)

Levent Erkok erkokl at gmail.com
Wed Nov 6 22:39:44 UTC 2019

```As pointed out, most "usual" algebraic equations simply do not hold for
IEEE754 floating-point numbers. Another example is `1+x == 1 /\ x /= 0` is
a satisfiable statement. Just wanted to point out you can use modern SMT
solvers to analyze such equalities, and Haskell SBV package (shameless
plug) provides a convenient interface. Here's the counter-example showing

There are other examples in there as well that might be of interest.

Cheers,

-Levent.

On Wed, Nov 6, 2019 at 2:31 PM Lana Black <lanablack at amok.cc> wrote:

> On 06/11/2019 22:19, Dannyu NDos wrote:
> > Omg, addition is not even associative? The zeros truly ruined everything.
> >
> > 2019년 11월 7일 (목) 06:58, Brent Yorgey <byorgey at gmail.com>님이 작성:
> >
> >> How is that worse than the fact that addition is already not associative
> >> for floating point types?  At least +0 is really the identity up to
> (==).
> >>
> >> On Wed, Nov 6, 2019, 3:49 PM Dannyu NDos <ndospark320 at gmail.com> wrote:
> >>
> >>> Sum has bug with floating points. Current definition states +0 as the
> >>> identity element, while the actual identity is -0 since +0 + -0 = +0.
> >>> _______________________________________________
> >>> Libraries mailing list
> >>>
> >>
> >
> >
> > _______________________________________________
> > Libraries mailing list
> >
> This has little to do with zeroes per se. IEEE 754 addition isn't
> associative for any numbers, and examples not involving zeroes aren't
> hard to find. Here's one:
>
> Prelude> let a = 1e30 :: Double
> Prelude> let b = -1e30 :: Double
> Prelude> let c = 1 :: Double
> Prelude> a + b + c
> 1.0
> Prelude> a + (b + c)
> 0.0
>
> There is a good document describing how IEEE754 works, including this
> kind of peculiarities:
> https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html
> _______________________________________________
> Libraries mailing list
>
-------------- next part --------------
An HTML attachment was scrubbed...
```