# Lecture 24: 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 a propositional formula:

```
data Proposition
= Var String
| Boolean Bool
| Not Proposition
| And Proposition Proposition
| Or Proposition Proposition
| Implies Proposition Proposition
```

**Exercise 24.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 goal for today is to write a 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:

```
abstractEval :: (Applicative m)
=> (String -> m b) -- ^ Var
-> (Bool -> m b) -- ^ Boolean
-> (b -> b) -- ^ Not
-> (b -> b -> b) -- ^ And
-> (b -> b -> b) -- ^ Or
-> (b -> b -> b) -- ^ Implies
-> Proposition
-> m b
abstractEval varf boolf notf andf orf impliesf = eval where
eval (Var a) = varf a
eval (Boolean b) = boolf b
eval (Not p) = pure notf <*> eval p
eval (And p q) = pure andf <*> eval p <*> eval q
eval (Or p q) = pure orf <*> eval p <*> eval q
eval (Implies p q) = pure impliesf <*> eval p <*> eval q
```

This looks scary, but it's actually quite simple, once you get the hang of it: we use `abstractEval`

to define an evaluator of type `Proposition -> m a`

by providing it with functions for processing variables, boolean constants, negations, compositions, disjunctions, and implications. We will use `abstractEval`

to implement a couple of different evaluators in this program, with different evaluation contexts. The generality of this function isn't just showing off! We actually need it. Indeed, it's easy to argue that `abstractEval`

isn't as general as it should be (one could imagine that functions
associated with the boolean operators returned their results in the monad `m`

), but its more generality than we need.

Our tautology checker will work as follows. Given a proposition `p`

, it will:

- Compute the set
`v`

of variables that occur in`p`

. - Generate a list
`valuations`

consisting of all possible maps from`v`

to`Bool`

. - 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 `abstractEval`

to build a function that extracts the set of names of the variables from a `Proposition`

:

```
variables :: Proposition -> Set String
variables = runIdentity . abstractEval
(Identity . Set.singleton) -- Var
(const (Identity Set.empty)) -- Boolean
id -- Not
Set.union -- And
Set.union -- Or
Set.union -- Implies
```

A key notion is that of a valuation, i.e., a representation of a function from variables to boolean values. We'll use `Map String Bool`

to represent valuations. A key problem is to produce a list of all possible valuations. We started with code that looked like this:

```
valuations :: Set String -> [Map String Bool]
valuations = map Map.fromList
. sequence
. map (\v -> [(v,True),(v,False)])
. Set.toList
```

A key twist in this is the use of `sequence`

, acts on a list of lists by building the Cartesian product of the lists, i.e., the list of lists that consist of one element from each of the original lists. It's worth thinking hard about this.

But our experience with the `Foldable`

and `Traversable`

type classes suggest that the sort of representation swizzling we're doing here (visible in the `toList`

and `fromList`

) functions should be unnecessary. This lead to a search for a better way. A first observation is that `sequence`

has a more general type:

```
sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)
```

As `[]`

is both `Traversable`

and a `Monad`

, we can use it as if it's type were

```
sequence :: [[a]] -> [[a]]
```

But our desired end result has type `[Map String Bool]`

. We can get there via `sequence`

if take an argument of type `Map String [Bool]`

, as `[]`

is a `Monad`

, and `Map String`

is `Traversable`

. This reduces the question (at least, at the level of types, if not values) to the problem of producing a function of type `Set String -> Map String [Bool]`

. To this end, we can simplify things a bit, using the fact that `Map String`

is a `Monoid`

(its monoidal action is left-biased union), but that works for us, so we can form a function of the necessary type via

```
foldMap (\v -> Map.singleton v [True,False])
```

The code fairy suggests that we replace `sequence`

with `sequenceA`

, which has a more modern type, and that we do a bit of η-reduction (as usual), giving us

```
valuations = sequenceA . foldMap (`Map.singleton` [True,False])
```

This is remarkable! Fully 3/5ths of the list traversing we were doing was unnecessary. This illustrates the genius of the `Traversable`

type class—it moots the need for most representation swizzling to and from `[]`

types.

Next up, we have to evaluate the proposition at each valuation. Fortunately, we have `abstractEval`

ready to serve us.

```
eval :: (Map String Bool)
-> Proposition
-> Bool
eval valuation prop = runReader (evalf prop) valuation where
evalf = abstractEval (reader . flip (!)) -- Var
pure -- Boolean
not -- Not
(&&) -- And
(||) -- Or
((||) . not) -- Implies
```

This takes a bit of work. The local function

```
evalf :: Proposition -> Reader (Map String Bool) Bool
```

is key. The `abstractEval`

function has no difficulty working in the context of `Reader (Map String Bool)`

, and most of the code writes itself. The tricky bit is our variable-handling argument to `abstractEval`

. Intuitive, we'll need

```
varf :: String -> Reader (Map String Bool) Bool
```

This involves lookup up the argument variable in the `Reader`

context, which we can do by the `reader`

function:

```
varf v = reader (\r -> r ! v)
```

Getting from here to

```
varf = reader . flip (!)
```

is just standard code fairy η-reduction work, but once we've gotten that far, we no longer need a local definition.

There is something mildly suspect about `eval`

. Since it relies on `(!)`

, it can throw an exception if the proposition being evaluated has a variable that's not included in the valuation. That can't happen with this program, as we only call `eval`

with a valuation that was generated from the proposition's variables, but it's worth thinking about how we might generalize `eval`

so that an undefined variable can be handled more gracefully in the code itself, but that's a project for another day. But it's worth noticing that `abstractEval`

sets us up for working with more complex evaluation contexts (e.g., contexts that handle errors).

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 . variables $ 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:

```
process :: String -> IO ()
process arg =
case readMaybe arg of
Nothing -> putStrLn $ "Could not parse \'" ++ arg ++ "\'."
Just p -> case refutations p of
[] -> putStrLn $ show p ++ " is a tautology."
r:_ -> do
putStrLn $ show p ++ " is refutable, cf.,"
void . (`Map.traverseWithKey` r) $ \k v ->
putStrLn $ printf " %s := %s" k (show v)
```

Briefly, we use `Text.Read.readMaybe`

, which parses in the `Maybe`

context, returning `Nothing`

for unparsable input. Assuming a successful parse, we then build the list of refutations of the resulting proposition. If that list is empty, we have a tautology (and so report), and if it's non-empty, we have a refutable proposition, and report both the fact of refutability, and a witnessing refutation.

Our `main`

action was originally written as

```
main :: IO ()
main = do
args <- getArgs
mapM_ processArg args
```

But again, the code fairy suggests that we should prefer the modern `traverse`

over the legacy `mapM`

, which results (after further transformations) in

```
main :: IO ()
main = void $ getArgs >>= traverse process
```

The `void`

simply throws out the result type, and it's a useful function to know about, especially to quite warnings on non-binding lines in a do expression if you compile with `-Wall`

, which is generally recommended. Alternatively, we could have used `traverse_`

, which always returns `()`

/

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 refutable, 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.