2012/9/27 Andrew Sutton <asutton.list@gmail.com>
I'm glad to see this discussion.
I believe that N3351 is not a good place to learn axioms from.
It's a reasonable place to start as long as you don't expect too much from them. The axioms presented in that paper were primarily intended to document the semantics of a type; we had not planned (at that time) any particular ideas about how they should or could be used by the compiler.
The point I tried to stress is that equivalences and implications in axioms were not intended (at least in N2887) to be operations on boolean values, but on expression trees. This difference is negligible when describing immutable functions that return values (common in STL) like: *op(a, op(b, c)) <=> op(op(a, b), c)*; But becomes important when dealing with functions with side effects and functions returning nothing: * ++i <=> i += 1 c.resize(0) <=> c.clear();* N3351 describes axioms as operations on boolean values, but it was my impression that the authors still intended the behavior similar to that of N2887, but chose not to describe it at that time. Or am I wrong? Regards, &rzej