On Thu, Sep 27, 2012 at 12:29 PM, Marc Glisse <marc.glisse@inria.fr> wrote:
On Thu, 27 Sep 2012, Lorenzo Caminiti wrote:
On Thu, Sep 27, 2012 at 12:03 PM, Nathan Ridge <zeratul976@hotmail.com> wrote:
Again, I'm learning these things as we go... but aren't => and <=> the "implies" and "if and only if" logical operators? If so, their operand must be boolean predicates so I don't understand what this axioms means:
c.resize(0) <=> c.clear()
Oh, I see, <=> is some sort of magic "equivalence" operator as it can be defined only meta+programmatically in the programmer's mind. This axiom means that "the effect of c.resize(0) must be /equivalent/ to c.clear()" in a way that the program will never be able to assert. I can't even check that syntactically, can I? What does it mean to check the axiom above syntactically given that I'd have to completely strip away the <=> operator because it cannot be represented programmatically? Then such an axiom is just a code comment and maybe it should be programmed as such IMO.
Perhaps we can interpret this formally as "all the variables that appear in both expressions [in this case, c] compare equal after the expressions are evalauted"?
Yeah, I was thinking more about it and maybe we can program it more or less like this:
c1.resize(0); c2.clear(); assert( eq(c1, c2) ); // the actual check
For every (this "for every" part is going to be hard to implement) c1 and c2 of type C and where eq returns true iff c1 and c2 are equal (eq could be implemented as operator== at least to start with).
One could write axioms for types that don't have an operator==, or where comparison doesn't make sense: p=malloc(n) <=> p=realloc(0,n)
Wouldn't this mean the following? For any p and q of some type T: p = malloc(n); q = realloc(0, n); assert( eq(p, q) ); Where eq() is the N3351 equality operator that checks if two objects are equal. eq could be implemented using == but it's more of a logical equality so even if a type doesn't have == than it is still logically sensible to check if two objects for that type are the same. In reality however, eq will have to be implemented and checkable somehow so if a type doesn't have a way to programatically checked for equality (using == or some other boolean function eq(), equal(), is_equal(), etc) then either you don't program the axiom or you add an assertion requirement to guard against the lack of == (like Boost.Contract does): p = malloc(n); q = realloc(0, n); assert( p == q ), requires has_equal<T>::value; // with assertion requirement that T has == For a given T, if has_equal<T>::value is true, assert( p == q ) will be compiled and checked at run-time, otherwise it will not even be compiled.
v.random_shuffle().random_shuffle() <=> v.random_shuffle() (x+y)+z <=> x+(y+z) for double (somewhat like passing -fassociative-math to gcc)
--Lorenzo