# [Haskell-cafe] NaN as Integer value

Levent Erkok erkokl at gmail.com
Wed Apr 17 19:23:36 CEST 2013

```For better or worse; IEEE-754 settled many of these questions.
I personally think the standard is a good compromise of what's practical,
efficiently implementable, and mathematically sensible. I find the
following paper by Rummer and Wahl an especially good read:

http://www.ccs.neu.edu/home/wahl/Publications/rw10.pdf

The paper focuses on how to formalize floating-point in SMT-solvers; but
section 3 is a great read for understanding how floating-point semantics
work, regardless whether you care for SMT-solving or not. It could be the
basis for a nice software implementation of floating-point, for instance.

-Levent.

On Wed, Apr 17, 2013 at 10:11 AM, wren ng thornton <wren at freegeek.org>wrote:

> On 4/14/13 8:53 PM, Kim-Ee Yeoh wrote:
> > On Sun, Apr 14, 2013 at 3:28 PM, wren ng thornton <wren at freegeek.org>
> wrote:
> >> Whereas the problematic
> >> values due to infinities are overspecified, so no matter which answer
> you
> >> pick it's guaranteed to be the wrong answer half the time.
> >>
> >> Part of this whole problem comes from the fact that floats *do* decide
> to
> >> give a meaning to 1/0 (namely Infinity).
> >
> > I'm not sure what you mean about overspecification here, but in
> > setting 1/0 as +infinity (as opposed to -infinity), there's an easily
> > overlooked assumption that the limit is obtained "from above" as
> > opposed to "from below."
>
> Setting 1/0 = +inf isn't the problem, or at least not the main one. Of
> course, there's always the question about which completion of the reals to
> use--- i.e., whether we have +inf vs -inf, or whether we just have a
> single point infinity.
>
> Rather, the NaN problem comes from trying to resolve things like:
>
>     inf - inf
>     inf * 0
>     inf / inf
>     0 / 0
>
> The overspecification problem I mentioned is that each of these
> expressions has "too many" solutions. For example, we have the following
> equations:
>
>     x   * 0 == 0               -- where x is finite
>     inf * y == inf * signum y  -- where y /= 0
>     inf * 0 == ??
>
>     x   - inf == -inf  -- where x is finite
>     inf - y   == inf   -- where y is finite
>     inf - inf == ??
>
>     x / 0 == inf * signum x  -- where x /= 0
>     0 / y == 0               -- where y /= 0
>     0 / 0 == ??
>
> --
> Live well,
> ~wren
>
>
> _______________________________________________