A bug with Sum (as in Monoid)

[Levent Erkok]

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
the non-associativity of addition:

http://hackage.haskell.org/package/sbv-8.5/docs/Documentation-SBV-Examples-Misc-Floating.html#v:assocPlusRegular

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 at haskell.org
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >>>
> >>
> >
> >
> > _______________________________________________
> > Libraries mailing list
> > Libraries at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >
> 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
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20191106/d4fd698b/attachment.html>