Proof question -- (==) over Bool
I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition: (==) :: Bool -> Bool -> Boolx == y = (x && y) || (not x && not y) My question is: are the proofs below for reflexivity and symmetricity rigorous, and what is the proof of transitivity, which eludes me? Thanks. Theorem (reflexivity): For all x `elem` Bool, x == x. Proof: x == x = {definition of "=="} (x && x) || (not x && not x) = {logic (law of the excluded middle)} True Theorem (symmetricity): For all x, y `elem` Bool, if x == y, then y == x. Proof: x == y = {definition of "=="} (x && y) || (not x && not y) = {lemma: "(&&)" is commutative} (y && x) || (not x && not y) = {lemma: "(&&)" is commutative} (y && x) || (not y && not x) = {definition of "=="} y == x Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y == z,then x == z. Proof: ? _________________________________________________________________ Hotmail has tools for the New Busy. Search, chat and e-mail from your inbox. http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:W...
2010/5/21 R J
I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition: (==) :: Bool -> Bool -> Bool x == y = (x && y) || (not x && not y) My question is: are the proofs below for reflexivity and symmetricity rigorous, and what is the proof of transitivity, which eludes me? Thanks.
Theorem (reflexivity): For all x `elem` Bool, x == x. Proof: x == x = {definition of "=="} (x && x) || (not x && not x) = {logic (law of the excluded middle)} True
This one depends on what you mean by rigorous. But you would have to have lemmas showing that && and || correspond to the predicate logic notions. I would do this by cases: x = True: (True && True) || (not True && not True) ... True || False True x = False (False && False) || (not False && not False) ... False || True True
Theorem (symmetricity): For all x, y `elem` Bool, if x == y, then y == x. Proof: x == y = {definition of "=="} (x && y) || (not x && not y) = {lemma: "(&&)" is commutative} (y && x) || (not x && not y) = {lemma: "(&&)" is commutative} (y && x) || (not y && not x) = {definition of "=="} y == x
Yes, given the lemmas about && and ||, this is rigorous. You can prove those lemmas by case analysis.
Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y == z, then x == z. Proof: ?
My first hunch here is to try the following lemma: Lemma: if (x == y) = True if and only if x = y. where == is the version you defined, and = is regular equality from logic, if you are allowed to rely on that. I would prove this by cases. At this point, you can convert transitivity of == to transitivity of =, which is assumed by the axioms. You could do the same for the other proofs you asked about instead of brute-forcing them. If you aren't allowed such magic, then I guess you could do all 8 cases of x, y, and z (i.e. proof by truth table). Somebody else might have a cleverer idea. Luke
On Sat, 2010-05-22 at 00:15 +0000, R J wrote:
I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition:
(==) :: Bool -> Bool -> Bool x == y = (x && y) || (not x && not y)
My question is: are the proofs below for reflexivity and symmetricity rigorous, and what is the proof of transitivity, which eludes me? Thanks.
Theorem (reflexivity): For all x `elem` Bool, x == x.
Proof:
x == x = {definition of "=="} (x && x) || (not x && not x) = {logic (law of the excluded middle)} True
I'd add additional step: x == x <=> (x && x) || (not x && not x) <=> x || not x <=> T def A && A = A A || not A = T However it depends on your level - the more advanced you are the more step you can omit.
Theorem (symmetricity): For all x, y `elem` Bool, if x == y, then y == x.
Proof:
x == y = {definition of "=="} (x && y) || (not x && not y) = {lemma: "(&&)" is commutative} (y && x) || (not x && not y) = {lemma: "(&&)" is commutative} (y && x) || (not y && not x) = {definition of "=="} y == x
Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y == z, then x == z.
Proof: ?
For example by cases in Y (assume Y is true and prove it correct and then assume Y is false and prove it correct. As in logic where there is law of excluded middle Y have to be true or false it holds). It took around 7 lines. Regards
R J
I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition:
(==):: Bool -> Bool -> Bool x == y = (x && y) || (not x && not y)
Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it.
Not really. Bottom isn't a value, so much as an expression for computations that don't refer to "real" values. It's close enough to be treated as a value in many contexts, but this isn't one of them. Proof by pattern matching (i.e., proof by truth table) is sufficient to ensure that bottom (as a value) isn't included. After all, the Bool type is enumerable. At least in principle. So perhaps the constructive Haskell proof would go something like: -- Claim to prove transitivity :: Bool -> Bool -> Bool -> Bool transitivity x y z = if (x == y) && (y && z) then x == z else True -- "The" proof unifier :: Bool unifier = all (True ==) $ [ transitivity x y z | x <- [ True, False ] , y <- [ True, False ] , z <- [ True, False ] ] This includes some syntactic sugar R J might not be "entitled" to, but the intent is pretty clear. We are programmatically validating that every assignment of truth values to the sentence "if (x == y) && (y && z) then x == z" is true. (The theorem is "vacuously true" for assignments where the antecedent of the conditional is false)
Note that "all (True ==)" is logically equivalent to "all id" and to
the "and" function from the prelude.
A more general approach based on type classes, the function taut takes
a boolean function and determines (by exhaustive search) if it is a
tautology:
class BooleanFunction a where
taut :: a -> Bool
instance BooleanFunction Bool where
taut = id
instance (Bounded a,Enum a, BooleanFunction b)
=> BooleanFunction (a -> b) where
taut f = and $ map (taut . f) $ enumFrom minBound
unifier = taut transitivity
On 22 May 2010 19:37, Alexander Solla
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it.
Not really. Bottom isn't a value, so much as an expression for computations that don't refer to "real" values. It's close enough to be treated as a value in many contexts, but this isn't one of them. Proof by pattern matching (i.e., proof by truth table) is sufficient to ensure that bottom (as a value) isn't included. After all, the Bool type is enumerable. At least in principle. So perhaps the constructive Haskell proof would go something like: -- Claim to prove transitivity :: Bool -> Bool -> Bool -> Bool transitivity x y z = if (x == y) && (y && z) then x == z else True -- "The" proof unifier :: Bool unifier = all (True ==) $ [ transitivity x y z | x <- [ True, False ] , y <- [ True, False ] , z <- [ True, False ] ] This includes some syntactic sugar R J might not be "entitled" to, but the intent is pretty clear. We are programmatically validating that every assignment of truth values to the sentence "if (x == y) && (y && z) then x == z" is true. (The theorem is "vacuously true" for assignments where the antecedent of the conditional is false) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Alexander Solla
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it.
Not really. Bottom isn't a value, so much as an expression for computations that don't refer to "real" values. It's close enough to be treated as a value in many contexts, but this isn't one of them.
It seems to me relevant here, because one of the uses to which one might put the symmetry rule is to replace an expression “e1 == e2” with “e2 == e1”, which can turn a programme that terminates into a programme that does not. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31)
On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
It seems to me relevant here, because one of the uses to which one might put the symmetry rule is to replace an expression “e1 == e2” with “e2 == e1”, which can turn a programme that terminates into a programme that does not.
I don't see how that can be (but if you have a counter example, please show us). Even if we extend == to apply to equivalence classes of bottom values, we would have to evaluate both e1 and e2 to determine the value of e1 == e2 or e2 == e1. Prelude> undefined == True *** Exception: Prelude.undefined Prelude> True == undefined *** Exception: Prelude.undefined Prelude> undefined == undefined *** Exception: Prelude.undefined That is, if one case is exceptional, so is the other. You can't really even quantify over bottoms in Haskell, as a language. The language runtime is able to do some evaluation and sometimes figure out that a bottom is undefined. Sometimes. But the runtime isn't a part of the language. The runtime is an implementation of the language's interpetation function. Bottoms are equivalent by conceptual fiat (in other words, vacuously) since not even the id :: a -> a function applies to them.
For Bool, I'm not sure, but for, e.g., () it's certainly true.
Take this definition of ==
() == _ = True
Using case analysis of just the constructors, ignoring the value
bottom, you can easily prove symmetry.
But '() == undefined' terminates, whereas 'undefined == ()' does not.
Ignore bottom at your own peril.
BTW, the id function works fine on bottom, both from a semantic and
implementation point of view.
-- Lennart
On Sun, May 23, 2010 at 11:23 AM, Alexander Solla
On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
It seems to me relevant here, because one of the uses to which one might put the symmetry rule is to replace an expression “e1 == e2” with “e2 == e1”, which can turn a programme that terminates into a programme that does not.
I don't see how that can be (but if you have a counter example, please show us). Even if we extend == to apply to equivalence classes of bottom values, we would have to evaluate both e1 and e2 to determine the value of e1 == e2 or e2 == e1.
Prelude> undefined == True *** Exception: Prelude.undefined Prelude> True == undefined *** Exception: Prelude.undefined Prelude> undefined == undefined *** Exception: Prelude.undefined
That is, if one case is exceptional, so is the other.
You can't really even quantify over bottoms in Haskell, as a language. The language runtime is able to do some evaluation and sometimes figure out that a bottom is undefined. Sometimes. But the runtime isn't a part of the language. The runtime is an implementation of the language's interpetation function. Bottoms are equivalent by conceptual fiat (in other words, vacuously) since not even the id :: a -> a function applies to them._______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On May 23, 2010, at 2:53 AM, Lennart Augustsson wrote:
BTW, the id function works fine on bottom, both from a semantic and implementation point of view.
Yes, but only because it doesn't work at all. Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will "crash" before you ever call id. Of course, the identity function "should" have produced a value that crashed in exactly the same way. But we never got there. It works in same way (==) works on bottoms. Vacuously. Indeed, functions only work on values. There is no value of type (forall a . a). Ergo, id does not work on undefined, as a function applying to a value. It is happy coincidence that the behavior of the runtime can be made mostly compatible with our familiar semantics. But not entirely. Consider: *Main> let super_undefined = super_undefined *Main> undefined == super_undefined *** Exception: Prelude.undefined *Main> super_undefined == super_undefined (wait forever) *Main> id super_undefined (wait forever) *Main> id undefined *** Exception: Prelude.undefined From a mathematical perspective, super_undefined is Prelude.undefined. But it takes some runtime level hackery to make undefined an exceptional "value". Without it, super_undefined loops, despite the fact that their definitions are exactly the same (The "value" defined by itself). I did not suggest those are the wrong semantics. Only that the study of their semantics doesn't belong to the study of Haskell as a logic/ language.
That's totally false. You don't evaluate 'undefined' before calling 'id'.
(Or if you, it's because you've made a transformation that is valid
because 'id' is strict.)
On Mon, May 24, 2010 at 9:05 AM, Alexander Solla
Yes, but only because it doesn't work at all. Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will "crash" before you ever call id. Of course, the identity function "should" have produced a value that crashed in exactly the same way. But we never got there.
Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will "crash" before you ever call id. Of >course, the identity function "should" have produced a value that crashed in exactly the same way. But we >never got there.
In which sense does id need to evaluate its argument? If evaluating
the statement "id undefined" in ghci, then the print function (and
ultimately the show function) evaluates the undefined. I suppose that
if the show function does not evaluate its argument then there will be
no error, right?
/Jonas
On 24 May 2010 09:05, Alexander Solla
On May 23, 2010, at 2:53 AM, Lennart Augustsson wrote:
BTW, the id function works fine on bottom, both from a semantic and implementation point of view.
Yes, but only because it doesn't work at all. Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will "crash" before you ever call id. Of course, the identity function "should" have produced a value that crashed in exactly the same way. But we never got there.
It works in same way (==) works on bottoms. Vacuously. Indeed, functions only work on values. There is no value of type (forall a . a). Ergo, id does not work on undefined, as a function applying to a value. It is happy coincidence that the behavior of the runtime can be made mostly compatible with our familiar semantics. But not entirely.
Consider:
*Main> let super_undefined = super_undefined *Main> undefined == super_undefined *** Exception: Prelude.undefined *Main> super_undefined == super_undefined (wait forever) *Main> id super_undefined (wait forever) *Main> id undefined *** Exception: Prelude.undefined
From a mathematical perspective, super_undefined is Prelude.undefined. But it takes some runtime level hackery to make undefined an exceptional "value". Without it, super_undefined loops, despite the fact that their definitions are exactly the same (The "value" defined by itself).
I did not suggest those are the wrong semantics. Only that the study of their semantics doesn't belong to the study of Haskell as a logic/language. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Monday 24 May 2010 15:48:14, Jonas Almström Duregård wrote:
Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will "crash" before you ever call id. Of >course, the identity function "should" have produced a value that crashed in exactly the same way. But we >never got there.
In which sense does id need to evaluate its argument?
It doesn't need to, and it doesn't. It just returns its argument untouched.
If evaluating the statement "id undefined" in ghci, then the print function (and ultimately the show function) evaluates the undefined. I suppose that if the show function does not evaluate its argument then there will be no error, right?
Right: Prelude Text.Show.Functions> id undefined :: (Bool -> Bool) <function>
/Jonas
Alexander Solla
On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
It seems to me relevant here, because one of the uses to which one might put the symmetry rule is to replace an expression “e1 == e2” with “e2 == e1”, which can turn a programme that terminates into a programme that does not.
I don't see how that can be (but if you have a counter example, please show us).
Oops! I was thinking of the symmetry rule in general. What I said applies to “a && b” and not to “a == b”, but my point was that surely you can’t be sure of that until after you’ve finished a proof that does consider ⊥? -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31)
participants (8)
-
Alexander Solla -
Daniel Fischer -
Jon Fairbairn -
Jonas Almström Duregård -
Lennart Augustsson -
Luke Palmer -
Maciej Piechotka -
R J