Lecture 25: Propositional Logic: A Tautology Checker
Propositional logic is an important tool for reasoning about many things, including programs. But our immediate goal is to write programs that will help us in working with propositional formulae. Haskell is very well suited for this sort of work. We'll start by declaring the type of propositional formulae:
data Proposition
= Var String
| Boolean Bool
| Not Proposition
| And Proposition Proposition
| Or Proposition Proposition
| Implies Proposition Proposition
Exercise 25.1 If you would like more practice with parsing, work through these Propositional Logic: Parsing notes. Below, we will assume the presence of the parser developed there.
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:
- Compute the set
v
of variables that occur inp
. - Generate a list
valuations
consisting of all possible maps fromv
toBool
. - Evaluate the proposition
p
at each valuation in turn, producing a list of valuations at which the proposition is false - 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 (++) (++) (++)
or even
variables = Set.toList . primrec (const Set.singleton) Set.empty id Set.union Set.union Set.union
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:
refutations :: Proposition -> [Map String Bool]
refutations 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 refutations 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.