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.

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 remarkable that sequence does this, but it does.

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 = sequence . foldMap (`Map.singleton` [True,False])

This is remarkable! Fully 3/5ths of the list traversing we were doing was unnecessary. As it turns out, this codes is not only type-correct, it's value-correct. This does not come as a major surprise.

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've mooted the need for 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 unparseable 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 print out 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.

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.

CMSC-16100

Honors Introduction to Programming, I

Autumn Quarter, 2017

Lecture 24: Propositional Logic: A Tautology Checker

Code