Does the associative/commutative/distributive/etc property hold for arithmetic performed with IEEE 754 floats?
Obviously the answer is no to most of those questions, but do any of the properties of standard arithmetic hold? How can one formulate proofs (or at least proof-like statements) explaining why any particular property does or does not hold?
The IEEE 754 standard defines exactly how floating-point arithmetic is performed. For many interesting theorems, you will need to examine the exact definition. For some less interesting ones, like a+b = b+a or ab = ba, all you need to know that IEEE 754 always calculates the exact result, rounded in a deterministic way. For non-theorems, like (a+b)+c = a+(b+c), which is false, all you need is a counterexample which is usually easy to find.
According to this talk (see p. 40) IEEE 754 arithmetic (additon and multiplication) is in general commutative, but neither associative or distributive. This concerns properly represented reals. For more details see this technical report (p. 8) from 2018, where it is stated in particular that addition and multiplications are not required to be commutative to comply with IEEE 754 if both operands are NaNs. See p. 37 of the talk for concrete python examples that fail associativity for +, while the same examples preserve associativity in C (Cf. this answer for an explanation of this behavior in so far as C does not obey IEEE 754).
The talk seems to be from 2023 (see p. 23). I am not sure about the quality, as the slides talk about "Z3 Zeus" and probably mean "Z3 Zuse" (also p. 23) - but they get Zuse's name right in other places (p. 70). Also note that IEEE 754 evolves (slowly with a 10 year life cycle and mostly in minute changes) over time, so this information may become outdated at some future point in time.
Here are some more explicit couterexamples partially inspired by the talk or this answer. They also highlight different aspects (lack of precision, out of range of represented numbers - this concerns aspects of "proof" indicated in the question) why some laws fail. These are given in Python and I have tested them on my machine (Python 3.10.12, Intel i9-9900K). According to the Python documentation "almost all platforms map Python floats to IEEE 754 binary64 “double precision” values".
Nonassociativity of "+":
x = -1e9
y = 1e9
z = 1e-9
print((x+y)+z) #result: 1e-09
print(x+(y+z)) #result: 0.0
Nonassociativity of "*":
x = 1e200
y = 1e200
z = 1e-200
print((x*y)*z) #result: inf
print(x*(y*z)) #result: 1e+200
Failure of inverse property for "*" (imho a reasonable "etc" from the original question):
print(1 / 0.18 * 0.18) #result: 0.9999999999999999
Note that the inverse property for + is a more delicate issue. It seems to hold (in my numerical experiments comparing "x-x", "x+(-x)" resp. "(-x)+x" against "0") up to the fact that there are several representations of zero including a +0.0 and -0.0, which, when compared semantically, yield equality in Python, but do not have the same bit-by-bit representation stored in hardware. Cf. this answer. Also note that
print((-1+0.8) + 0.2) #result: 5.551115123125783e-17
This is because -1+0.8 by representation error of 0.8 and subsequent rounding error for the "+"-operation is evaluated to something different from (the closest float-representation of) "-0.2" in Python. This sketches a proof of the failure of this property. You could view this as some failure of the inverse property for "+", although it involves not a single but two nontrivial additions. On the other hand this is technically similar to the example above which involves also two operations, a "/" and a "*", although one could argue that the first "1/0.18" should be considered trivial in only producing a representation (up to finite precision arithmetic) of the multiplicative inverse of 0.18.
Failure of distribution:
x = 0.7571726635553984
y = 0.49156357837557363
z = 0.15529475249590363
print(x*y+x*z) #result: 0.48978344532895557
print(x*(y+z)) #result: 0.4897834453289556
This last example was found using a small Python program which in most runs produced 20 to 40 failures out of 100 trials showing that this failure is quite common in the sense of pseudorandom numbers.
import random
for i in range(100):
x = random.random()
y = random.random()
z = random.random()
a = x * y + x * z
b = x * (y + z)
if a != b:
print(x, y, z, " --> ", a, b)
If one is interested if a certain property holds (generically in the sense of numerical experiments with a bunch of pseudorandom numbers), one may just adjust this program to whatever property one is interested in. Whether this reflects aspects of IEEE 754 depends on the compliance of the computer system used with that standard - see disclaimer above on the relation of IEEE 754 and Python.
Some more "weird", but instructive examples (Note that "//" does not seem to have a direct equivalent in IEEE 754 and that "%" in python seems to behave differently than the IEEE 754 operation "remainder" as remainder is defined via a "round to nearest integer", while Pythons "%" is compatible with its "//" using "round down to integer". The first two of these four examples should however use IEEE 754 compliant Python operations):
print(0.1*0.1) #result: 0.010000000000000002
print(1000000000000000000 - 1000000000000000001.0) #result: 0.0
print(1000000000000000000 // 1000000000000000001.0) #result: 1.0
print(1000000000000000000 % 1000000000000000001.0) #result: 0.0
This adds a few more details and explicit examples to the answer of gnasher729 and references.
Check e.g. Goldberg's "What every computer scientist should know about floating point". Heavy reading, but a must.
