On Fri, Sep 28, 2012 at 5:39 AM, Andrew Sutton <asutton.list@gmail.com> wrote:
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):
*cringe* Don't think about eq(). That was a compromise between myself and Marcin Zalewski. We couldn't determine if <=> should be interpreted as logical equivalence or behavioral equivalence (as in the previous axioms work). We ended assigning <=> to logical equivalence and using eq() as a kind of oracle that decided equality: either according to the rules of == or memberwise equality comparison.
Just to put it into perspective, equality comes from Elements of Programming. Page 7 shows that there is a "specification" equality and a "C++" equality. If one reads the first chapter of EoP, the notion of equality is explained well in context of what the types actually represent. In a sense, there is an implicit assumption of "denotational" semantics that assigns to every value an abstract *mathematical* entity. Then, equality is simply mathematical equality on these entities. The == operator *does not* have to always be implemented. The book discusses this as well. Sometimes it is hard, and sometimes it is impossible to implement ==. Sometimes it is enough to just compare some kind of a hash. In some other cases, we may settle for representational equality, where we just compare bits. This gives us a partial implementation of a true equality. There is a paper related to this subject, by John Lakos: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2007/n2479.pdf This paper has a similar notion of equality.
In retrospect, I think this was the wrong choice. Using <=> to describe the behavioral equivalence of two expressions provides a much more robust way of stating the relative meaning of operations.
To put this into perspective too, I think that "behavioral" equivalence here would be an equivalence in terms of "operational" semantics. I don't think that either approach is wrong in any way. Each approach fits some applications better then others. If behavioral equivalence is taken to mean equality defined in terms of operational semantics, then defining it works out a bit differently. For example, we must deal with cases such as 1/2 and 2/4 being equal which comes for free in denotational semantics, but requires some fiddling in operational semantics. We just need to be careful about how we defined "behavioral equivalence," but that is not to say that it is impossible. So, to summarize, the current approach is a direct descendant of EoP where we have simply renamed the "specification" = from page 7 to eq(). Reading EoP carefully can help in understanding how it works. For operational definitions of equality, one can look back at the existing work. BTW, just an additional example to keep in mind, which we have used frequently. Two vectors with equal elements but different capacities (allocated memory) are trivially equal in denotational approach (such as used in EoP) since they end up representing identical mathematical sequences. With operational semantics one has to sweat a bit more, and perhaps say something like "the two vectors will behave the same with respect to some operations." This has to be a recursively applied definition, since these operations may themselves return something that differs only, say, in memory allocation. Thus, for operational definition, we always need some "context" to decide when things are equal. The denotational definition needs a context too, but it takes care of it right away and once and for all.
Andrew
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost