Document floating point number caveats

[curiousleo]

Ideally this is clear and self-contained enough that we can link to this from #137.

---

[curiousleo]

Q: is there a way to link to a named chunk in another module?

[curiousleo]

This should probably mention NaN and Infinity too. I am tempted say that for any a and b, be they NaN, Infinity, normal or denormal, you get precisely the semantics of (b - a) * x + b. That is concise and covers all the edge cases. Perhaps we could include a few examples.

[curiousleo]

Ready for the next review round.

[lehins]

Looks great

[idontgetoutmuch]

Very clear - thanks

[LeventErkok]

@curiousleo

Minor comment: The documentation states floating-point operations are not commutative. This is not true. Floating-point addition and multiplication are both commutative in IEEE754 semantics, in any rounding mode. (To be absolutely precise, swapping the arguments will always produce the same result, assuming a NaN result is considered equivalent to any other NaN; which is an important point but doesn't really violate the spirit of the commutativity. i.e., you can get different NaNs if you swap the order, but if you get a NaN in one way, you'll also get a NaN if you swap.)

The comment regarding the operations being not-associative and the usual distributive laws not holding are, of course, both absolutely correct.

I should add that the documentation of the floating-point caveats is absolutely wonderful. These are often ignored in library documentations, very happy to see them explicitly captured.

[curiousleo]

Thank you for the clarification @LeventErkok! I will fix the documentation. I actually used sbv to find the counterexamples now included in the documentation: #105 (comment) - as an SMT frontend, I found it a joy to use.

I should add that the documentation of the floating-point caveats is absolutely wonderful. These are often ignored in library documentations, very happy to see them explicitly captured.

That's really nice to hear, thank you! We spent quite some time discussing whether to implement a better algorithm for uniformly random floating point numbers with nicer semantics, but decided to focus on other improvements for now. As a consequence, though, we became very aware of the issues with the current method.

[idontgetoutmuch]

@LeventErkok Thanks for this - we had long debates over floating point - it turns out you can sample every floating point number in a reasonably efficient way by working through the binades with the right sampling strategy. In practice there are binades that will be almost never be sampled and we opted for a simpler sampling strategy that won't sample some floating point numbers even in theory. I see @curiousleo replied before I did but I will post this anyway.

[LeventErkok]

@curiousleo @idontgetoutmuch

Fantastic! I'm glad sbv found some practical use.

Uniformly sampling a float can be tricky indeed. The simplest thing to do would be to sample a 32-bit unsigned number (64-bit for doubles), and reinterpret the bit-pattern as a float. The problem with that would be it would sample NaNs way more often than anything else, as NaN payloads can differ without changing the fact that they are NaNs. And then there's the scaling issue to a given range, of course. I'm by no means an expert on sampling but I'm glad to see you guys are giving this the proper treatment it deserves. Best of luck!