Lambda the Ultimate

You simply need multiple equality predicates. Sometimes you're basically interested in the concrete representation, and sometimes you want to compare structure, or the "mathematical" value.

That's old news: IEEE float equality is not an equivalence relation. Many people consider that a bad move, but we have to live with it. If you care about built-in equality having nice properties, then either make it inapplicable to floats (like e.g. = in SML), or give it a semantics different from IEEE. In either case, you want a separate operator to implement IEEE equality (e.g. Real.== in SML).

As a quick aside; when you link to your blog please link to a specific story. That makes it easier for somebody to find which blog post you were referring to when people stumble upon this LtU post months and years down the road. For example, use

http://bertrandmeyer.com/2010/02/06/reflexivity-and-other-pillars-of-civilization/

instead of

http://bertrandmeyer.com/

You should be able to edit this story as well as your old stories to update the links. Of course, you probably want to give the link a nice textual description, instead of making the URL directly visible.

It's true, the IEEE 754 standard is nuts. No reasonable specification for computing would define a value system in which vital foundational properties like "for all x, x=x" don't hold.

The consensus here is reasonable: To support IEEE 754 in a sensible language, you shouldn't let the crazy specification's notion of equality pollute the language's notion of equality. Rather, expose its comparison as an ordinary function, e.g. ieee754_compare(a:float,b:float):bool.

Using the = comparison operator on floats is generally a bad idea, due to all the nasty rounding side-effects, particularly on machines where the registers internal format is different from the stored one (e.g. x87: 80bits internal vs. 64bits IEEE doubles). There is little guarantee that if X:=Y, then X is_exactly_equal_to Y.

The result of IEEE comparaisons can have 4 values : '=' , '>', '<' and Unordered. Any comparison involving NaNs shall return 'Unordered'. From these 4 values, one can define 16 predicates, for example, in the SPARC Instruction Set :

FBA Branch Always
FBN Branch Never
FBU Branch on Unordered
FBG Branch on Greater
FBUG Branch on Unordered or Greater
FBL Branch on Less
FBUL Branch on Unordered or Less
FBLG Branch on Less or Greater
FBNE Branch on Not Equal
FBE Branch on Equal
FBUE Branch on Unordered or Equal
FBGE Branch on Greater or Equal
FBUGE Branch on Unordered or Greater or Equal
FBLE Branch on Less or Equal
FBULE Branch on Unordered or Less or Equal
FBO Branch on Ordered

A compiler can choose either FBE or FBUE for equality, or maybe FBN is the safest :-)

From the standard-defined operations, NaN appears as the result of sqrt(negative_number), 0/0, or as user-defined source operands. Then, the NaNs propagates across all operations, tracing that somewhere the calculation gone bad. There is no need to check for NaNs after every operation.

Sometimes, the valid answer to a question is 'i don't know' instead of 'true' or 'false'. NaN means 'Not a Number', literally, these are not values, it is like returning an error code. NaNs can also be used for detecting unitialised memory (the FFFFFFFF pattern is a QNaN), there is no legitimate comparison between unitialised variables.

Correctly handling floating point operations in a programming language is very complex. For example :
- Many operations are imprecises, and non associative, which is bad for optimisers. Combined Multiply-Accumulate is different than separate multiply and add operations.
- The IEEE standard mandates the availability of 4 rounding modes, with fun corner cases. There is very little support of that feature in programming languages.

The IEEE standard is diffcult, both for software handling and hardware implementation, nevertheless, it does the _right_ thing, a reasonable way to handle something that look likes algebra but isn't actually real maths.

See : Kahan Paper :Lecture notes on the status of IEEE Standard 754 for Binary Floating-Point Arithmetic