Is it legal "to state" with axioms, something that is not true in
general case?
That's an open question--for me. There may be a good answer to that question in the literature or addressed in other domains.
Axioms so far have not been standardized, nor has anyone prepared a formal, unambiguous specification of how they would be handled. People have different views on and expectations of axioms. N2887 has been the best attempt so far to specify what axioms are supposed to mean to the compiler and other tools. So some answer could be given based on N2887. Basically, what it says is that axioms only reflect current practice of writing generic code, rather than inventing something new. So what do you think of STL algorithms that operate on doubles in C++11?: void find_me( std::vector<double> const& vec, double n ) { std::find(vec.begin(), vec.end(), 10.2); std::find(vec.begin(), vec.end(), n); } Is it legal? Is it correct? Is it good practice? can 'n' be NaN? My answer is: STL algorithms will make an assumption that operations on 'T' are symmetrical, that comparisons for 'T' meet the three relations (reflexivity, symmetry, transitivity). STL implementations will not in general verify these assumptions, but may use these assumptions in as many places as they want, and you will never know when. Some implementations may do some run-time checks (in debug versions), where they know they could not spoil the program, but this is QoI issue. Should the programmer instantiate STL algorithms for 'T' == double? My answer is: they know the risks (of potentially not meeting the assumptions), they should assess if the risk is low or make sure they eliminate the usage of NaNs, and they should make the call at their own risk. If the program has a bug due to type double not having met the assumptions on 'T' it is the fault of the programmer who requested the instantiation of the algorithm with type double. Axioms (according to N2887) do not change this situation. An assumption of type 'T' is never 'valid' or 'invalid'. It is just an assumption that one may use or not. When you request an instantiation of an algorithm constrained with an 'axiom-rich' concept with type X, you take the responsibility for X meeting or not the expectations expressed in the concept.
Just to clarify: question was about C++ axioms. Is it illegal (from formal point of view of C++ axioms), to have:
axiom { a.size() == a.length(); } and: int T:size() { return 0;} int T:length() { return 1;} ?
Does compiler have the authority (from formal point of view of C++ axioms) to stop compilation with error in such case(of course, if it able to diagnose that)?
It may be sufficient to simply assume that floating point operations
satisfy the abstract mathematical requirements. We generally do anyways.
For most cases - we may assume floating-point addition associativity. For some cases not. Currently, we may control this by compiler-dependent flags. For instance /fp:fast /fp:precise flags of MSVC compiler - with /fp:fast MSVC2012 does auto-vectorization (SSE) of floating-point accumulation.
If compiler has right to reject wrong axioms when he able to diagnose, then we can't use C++ axioms to express in code our assumption about floating-point addition associativity.
This question is somewhat similar to: can compiler refuse to compile the following code: void Terminator() noexcept { throw std::runtime_error(); } We know that the compiler must not in general check this, but in the above particular case it is obvious that someone has planted a bug. But the answer is still: the compiler must not reject this code. However, it is allowed to report a warning (compilation warnings are not in scope of the C++ standard); and it would be surprising if a good compiler didn't do it. And you are allowed to set the compiler option to treat warnings (at least of this type) as errors. The good strategy for compilers, regarding axioms, would be to make use of axioms only if they have some way of verifying if type 'X' meets them, (either by limited static code analysis or run-time checks). This might require selecting only a subset of all axioms that the compiler is able to check and utilize only this subset. Regards, &rzej