On 7/30/12 9:51 PM, Christian Sternagel wrote:
Thanks Wren, for the explanations (also in your previous mail)!
On 07/30/2012 01:29 PM, wren ng thornton wrote:
On 7/24/12 9:19 PM, Christian Sternagel wrote:
(x == y) = True ==> x = y (x == y) = False ==> not (x = y) (x == _|_) = _|_ (_|_ == y) = _|_
Those axioms state that (==) is sound w.r.t. to meta-equality and strict in both it's arguments.
An immediate problem that arises here is: what exactly does meta-equality denote in Isabelle/HOLCF? If it is meant to denote syntactic identity or Leibniz equality a la Coq, then the first axiom is certainly too strong for any interesting data types (e.g., Rational, Data.Set, Data.Map, Data.IntSet,...)
Btw: I don't agree that the axioms are too strong for *any* interesting data types ;). What about Bool, Int, [a], ...? (Again, this depends on how we interpret "interesting"; in formalizations the threshold for being interesting is typically lower.)
Urk. Should've been "many" :) I was waffling between a few different quantifiers there, and it seems the "m" was an unfortunate casualty of that conflict. -- Live well, ~wren