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