Lecture 24: Propositional Logic: A Tautology Checker

Our next program will be a simple brute-force tautology checker. It greatly simplifies this program to have the following function-defining function for Proposition, which we'll add to the Proposition module:

primrec :: (String -> a) -- ^ Var -> (Bool -> a) -- ^ Boolean -> (a -> a) -- ^ Not -> (a -> a -> a) -- ^ And -> (a -> a -> a) -- ^ Or -> (a -> a -> a) -- ^ Implies -> Proposition -> a primrec varf boolf notf andf orf impliesf = result where result prop = case prop of Var a -> varf a Boolean b -> boolf b Not p -> unary notf p And p q -> binary andf p q Or p q -> binary orf p q Implies p q -> binary impliesf p q unary op p = op (result p) binary op p q = op (result p) (result q)

This looks scary, but it's actually quite simple: we use primrec to define a function of type Proposition -> a by providing it with functions for processing variables, boolean constants, negations, compositions, disjunctions, and implications.

Our tautology checker will work as follows. Given a proposition p, it will:

  1. Compute the set v of variables that occur in p.
  2. Generate a list valuations consisting of all possible maps from v to Bool.
  3. Evaluate the proposition p at each valuation in turn, producing a list of valuations at which the proposition is false
  4. Generate output, either noting that the formula is a tautology, or providing a refuting refutation.

The first step uses primrec to extract the list of names of variables in order of occurrence, and then we filter that list down to single occurrences via Data.List.nub:

variables ::Proposition -> [String] variables = nub . primrec (:[]) (const []) id (++) (++) (++)

Note here that (:[]) is a function which given a value (in this context, a String), encloses it in a list of length 1.

Actually, that use of nub is inefficient, and it's a bit offensive to have such an obvious and unnecessary inefficiency. Instead, we can read a list into and out of a Set, obtaining the effect of a sorting and uniquing, at a complexity of $O(n \log n)$ rather than $O(n^2)$, very simply:

import qualified Data.Set as Set usort :: Ord a => [a] -> [a] usort = Set.toList . Set.fromList

from which

variables = usort . primrec (:[]) (const []) id (++) (++) (++)

Better.

Generating the list of valuations is trickier.

valuations :: Proposition -> [Map String Bool] valuations = map Map.fromList . sequence . assignments . variables where assignments = map (\v -> [(v,True),(v,False)])

Let's take this piece by piece, with an example proposition:

testProp :: Proposition testProp = read "a -> a | b"

First, we extract the variables:

> variables testProp ["a","b"]

Next, we compute the assignments of truth values to each variable:

> assignments . variables $ testProp [[("a",True),("a",False)],[("b",True),("b",False)]]

Next, we apply Control.Monad.sequence, to the result. This is the great magic here. Recall:

sequence :: Monad m => [m a] -> m [a]

Intuitively, sequence does a bind on each of the monads on the list, returning the list of results. In this case, we're applying sequence to a list of lists, so the monad in question is [], and what happens is that we'll build a list, each of whose elements is a list, consisting of one element from each of the original list's element lists. Stated more succinctly, applied to a list of lists, sequence returns the cartesian product of the constituent lists.

> sequence . assignments . variables $ testProp [[("a",True),("b",True)],[("a",True),("b",False)],[("a",False),("b",True)],[("a",False),("b",False)]]

Finally, we apply map Map.fromList to this list, obtaining the list of valuations.

Next up, we have to evaluate the proposition at each valuation. We'll use a simple evaluator:

eval :: (String -> Bool) -> Proposition -> Bool eval varf = primrec varf id not (&&) (||) (\x y -> not x || y)

Isn't it nice how much work primrec saves?

Next, we generate a list of exceptional valuations, i.e., valuations for which a given proposition is not true:

exceptions :: Proposition -> [Map String Bool] exceptions p = [v | v <- valuations p, not . eval (v!) $ p]

Finally, there's the IO code to make it all work. The taut program processes its command line arguments, reading each as a Proposition, and then reporting whether the resulting Proposition is or is not a tautology. There's nothing especially remarkable about the code involved:

processArg :: String -> IO () processArg arg = do mp <- try (readIO arg) :: IO (Either IOError Proposition) case mp of Left _ -> putStrLn $ "Could not parse \'" ++ arg ++ "\'." Right p -> case exceptions p of [] -> putStrLn $ show p ++ " is a tautology." v:_ -> do putStrLn $ show p ++ " is not a tautology, cf." putStr . unlines . map (\(k,v) -> " " ++ k ++ ": " ++ show v) . Map.toList $ v main :: IO () main = do args <- getArgs mapM_ processArg args

A sample run looks like this:

$ taut "a -> a" "a -> b" "(a -> b) -> (b -> c) -> (a -> c)" "a ->" a -> a is a tautology. a -> b is not a tautology, cf. a: True b: False (a -> b) -> (b -> c) -> a -> c is a tautology. Could not parse 'a ->'. $

On one hand, this is a fairly useful little program, but on another, it's a bit unsatisfying. If we process a refutable proposition, we're given a refuting valuation. But if the proposition is a tautology, all we get is a bare assertion that this is so. If we want to do more, we'll have to work harder.

Code