Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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) > > /Jonas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
>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 wrote: > > 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 > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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 wrote: > 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proof question -- (==) over Bool
Alexander Solla writes: > 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.fairba...@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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 wrote: > > 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 > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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
[Haskell-cafe] Re: Proof question -- (==) over Bool
Alexander Solla writes: > 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.fairba...@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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 wrote: > > 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 > > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
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
[Haskell-cafe] Re: Proof question -- (==) over Bool
R J writes: > 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.fairba...@cl.cam.ac.uk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proof question -- (==) over Bool
On Sat, 2010-05-22 at 00:15 +, 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
signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
