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
