Lecture 25: A Quine's Method Theorem Prover

Let's remember the basics of Quine's method. Given a proposition p, we simplify p, i.e., we produce a new proposition p' which logically equivalent to p, such that p' is either:

Boolean True, in which case it is a tautology,
Boolean False, in which case it is refutable, i.e., not a tautology, or
there are no Boolean nodes remaining, in which case we
1. select a variable v which occurs in p.
2. create two new propositions pt and pf, by substituting Boolean True and Boolean False for v in the original proposition. Then p is a tautology if and only if both pt and pf are.

We'll start with code for simplifying a proposition:


    simplify :: Proposition -> Proposition
    simplify = primrec Var Boolean notf andf orf impliesf where
        notf p = case p of
            Boolean b -> Boolean (not b)
            Not q -> q                              -- eliminate double negations
            p -> Not p
        andf p q = case (p,q) of
            (Boolean True,q) -> q
            (Boolean False,_) -> Boolean False
            (p,Boolean True) -> p
            (p,Boolean False) -> Boolean False
            (p,q) -> And p q
        orf p q = case (p,q) of
            (Boolean True,q) -> Boolean True
            (Boolean False,q) -> q
            (p,Boolean True) -> Boolean True
            (p,Boolean False) -> p
            (p,q) -> Or p q
        impliesf p q = case (p,q) of
            (Boolean True,q) -> q
            (Boolean False,q) -> Boolean True
            (p,Boolean True) -> Boolean True
            (p,Boolean False) -> Not p
            (p,q) -> Implies p q

Much of the heavy lifting is done by primrec, which ensures that each of the case-handling functions are passed arguments that are already simplified, and so already meet the contract for simplify, i.e., they're either Boolean nodes, or they contain no Boolean subnodes. The case-handing functions just need to make sure that they handle any Boolean constituents so as to preserve that contract. Note here also that we've added double-negation elimination to the simplifier.

The simplify function can be thought of as a partial-evaluator, i.e., it takes an existing expression, and partially evaluates it, resulting in a simpler expression that can be used more efficiently in lieu of the original in subsequent processing. Partial evaluators are important in many optimizations, and one of the nice things about Haskell is that it often makes writing partial evaluators easy.

Next up, we have the job of creating substitution instances of our proposition, in which the selected variable is set to True and False respectively. First, we'll write a general purpose substitution routine:


    type Substitution = Map String Proposition
    
    substitute :: Substitution -> Proposition -> Proposition
    substitute sub = primrec varf Boolean Not And Or Implies where
        varf name = case name `Map.lookup` sub of
            Nothing -> Var name
            Just prop -> prop

Next, we'll write a special purpose routine that sets just a single variable to a boolean, given a Bool.


    setVar :: String -> Bool -> Proposition -> Proposition
    setVar name val = substitute (Map.singleton name (Boolean val))

With these preliminaries in place, we're ready for a first cut at our theorem prover. First, we define a type for the result of analyzing a Proposition using Quine's algorithm:


    data QuineProof
        = Split
            Proposition     -- ^ the proposition to be proven
            String          -- ^ the name of the variable to split on
            QuineProof      -- ^ case where the split variable is True
            QuineProof      -- ^ case where the split variable is False
        | Trivial
        deriving (Show)
     
    type Analysis = Maybe QuineProof

This will get more sophisticated, but it's a start. With this, we can do our first pass at our quine theorem prover.


    quine :: Proposition -> Analysis
    quine prop = case simplify prop of
        Boolean True -> return Trivial
        Boolean False -> Nothing
        q -> Split q v <$> branch True <*> branch False where
            v = head . variables $ q
            branch b = quine (setVar v b q)

This is just a simple realization of Quine's algorithm. This code is good enough to to find our our bearings, but a little bit of exploration reveals a need to do more work:


    > let runQuine = quine . read
    > runQuine "a -> a"
    Just (Split a -> a "a" Trivial Trivial)
    > runQuine "a -> b"
    Nothing
    > runQuine "a | b -> (a -> c) -> (b -> c) -> c"
    Just (Split a | b -> (a -> c) -> (b -> c) -> c "a" (Split c -> (b -> c) -> c "b" (Split c -> c -> c "c" Trivial Trivial) (Split c -> c "c" Trivial Trivial)) (Split b -> (b -> c) -> c "b" (Split c -> c "c" Trivial Trivial) Trivial))

We're getting proofs out, and it's worth understanding that first.

Let's consider the analysis of a -> a, a familiar tautology. It doesn't simplify to a tautology, but rather to itself. We split "a", and substitute in Boolean True and Boolean False for Var "a" in the true and false branches of the proof, in both cases resulting in formula that simplify to Boolean True, and so have trivial proofs.

Next, we have a -> b, which isn't a tautology. Since the formula is refutable, we return Nothing, as there is no Quine proof to return.

Finally, we have the analysis of a | b -> (a -> c) -> (b -> c) -> c. The proof that was returned isn't that easy to read, so it's helpful to write it a bit differently (note that this isn't valid Haskell)


    Split 
        a | b -> (a -> c) -> (b -> c) -> c
        "a" 
        Split c -> (b -> c) -> c
             "b"
             Split c -> c -> c "c" Trivial Trivial
             Split c -> c "c" Trivial Trivial
        Split b -> (b -> c) -> c
            "b"
            Split c -> c "c" Trivial Trivial
            Trivial

We see that the analysis of the original formula results in a splitting on Var "a", resulting in two formula that simplify to c -> (b -> c) -> c and b -> (b -> c) -> c respectively. The analysis of the first of these does a split on Var "b", which is unfortunate, because a split on Var "c" would result in trivial instances. Likewise, the analysis of b -> (b -> c) -> c splits on Var "b", resulting in a non-trivial branch, whereas a split on Var "c" instead would have resulting in two trivial branches.

So it's a start, but there's a lot to be unhappy with if this particular theorem prover is to live up to its potential:

The simplification process is abrupt. We only get to see the beginning and ending steps of the simplifications, and simplification is a nontrivial process. It would be helpful to illustrate a step-by-step sequence of simplifications.
Our goal is to give a result that is human checkable, but we fail badly in the case of a refutable statement. Our prover is just returning the fact of refutability, rather than an explanation. Our brute-force tautology prover did better, and we should too.
Our theorem prover forces us to pursue the process of splitting a formula all the way down to success (Boolean True) or failure (Boolean False). We can give more concise proofs by recognizing when we've reduced a formula to a (substitution instance of) a known tautology, and quit there.
The proofs we're producing aren't particularly economical. If our goal is human readability, we should value concision, even at the cost of much more computation.
The result we return is unnecessarily opaque. Accepting the default formatting of the result isn't a particularly friendly thing to do. We should format the final result better.

These changes involve a certain amount of additional book-keeping, and the difficulty of doing so isn't to be slighted. But the more essential difficulties are in writing the step-by-step simplifier and the instance checker.

We'll start with the step-by-step simplifier:


    step :: Proposition -> Maybe Proposition
    step p = case p of
        Var _ -> Nothing
        Boolean _ -> Nothing
        Not q -> case (q, step q) of
            (Boolean b, _) -> Just (Boolean (not b))
            (_,Nothing) -> Nothing
            (_,Just r) -> Just (Not r)
        And q r -> case (q,r,step q, step r) of
            (Boolean True,_,_,_) -> Just r
            (Boolean False,_,_,_) -> Just (Boolean False)
            (_,_,Just sq,_) -> Just (And sq r)
            (_,Boolean True,Nothing,_) -> Just q
            (_,Boolean False,Nothing,_) -> Just (Boolean False)
            (_,_,Nothing,Just sp) -> Just (And q sp)
            (_,_,Nothing,Nothing) -> Nothing
        Or q r -> case (q,r,step q, step r) of
            (Boolean True,_,_,_) -> Just (Boolean True)
            (Boolean False,_,_,_) -> Just r
            (_,_,Just sq,_) -> Just (Or sq r)
            (_,Boolean True,Nothing,_) -> Just (Boolean True)
            (_,Boolean False,Nothing,_) -> Just q
            (_,_,Nothing,Just sr) -> Just (Or q sr)
            (_,_,Nothing,Nothing) -> Nothing
        Implies q r -> case (q,r,step q, step r) of
            (Boolean True,_,_,_) -> Just r
            (Boolean False,_,_,_) -> Just (Boolean True)
            (_,_,Just sq,_) -> Just (Implies sq r)
            (_,Boolean True,Nothing,_) -> Just (Boolean True)
            (_,Boolean False,Nothing,_) -> Just (Not q)
            (_,_,Nothing,Just sr) -> Just (Implies q sr)
            (_,_,Nothing,Nothing) -> Nothing

There's a lot going on here. First, we'll use the Maybe type to distinguish between the cases where a simplification was made, and where it wasn't. Notice here that our computation can't be expressed in terms of primrec, as we require access to the both "stepped" and "unstepped" forms of the subexpressions we're analyzing, and primrec would only give us the "stepped" forms. There's also some careful work in setting up the cases, both to avoid unnecessarily evaluation, and deep nesting of alternatives. To make debugging easier, we'll use the -Wall flag to ghc/ghci to warn us about all errors, including both overlapping and non-exhaustive case statements.

We use the step function to build a a new simplify :: Proposition -> [Proposition], returning a (non-empty) sequence of simplification steps:


    simplify :: Proposition -> [Proposition]
    simplify p = iter (Just p) where
        iter Nothing = []
        iter (Just a) = a : iter (step a)

We now can tackle the issue of getting simplification steps into our proofs, by modifying the definition of QuineProof so that it includes the simplification steps, and not just the final result of simplification.


    data QuineProof
        = Split
            [Proposition]   -- ^ simplification of proposition to be proven
            String          -- ^ the name of the variable to split on
            QuineProof      -- ^ case where the split variable is True
            QuineProof      -- ^ case where the split variable is False
        | Trivial
            [Proposition]

Because refutations are also more complex, we replace the use of the Maybe type with a type that can carry a value in the failure case:


    type Valuation = Map String Bool
    
    toSub :: Valuation -> Substitution
    toSub = Map.map Boolean

    type Analysis = Either ([Proposition],Valuation) QuineProof

We can now write a version of quine for these new types:


    quine :: Proposition -> Analysis
    quine prop =
        let props = simplify prop
        in case last props of
            Boolean True -> return $ Trivial props
            Boolean False -> Left (props,Map.empty)
            q -> case (branch True, branch False) of
                (Left (_,s),_) -> Left (props,Map.insert v True s)
                (_,Left (_,s)) -> Left (props,Map.insert v False s)
                (Right p1, Right p2) -> return $ Split props v p1 p2
                where
                v = head . variables $ q
                branch b = quine (setVar v b q)

At this time, it seems prudent to tackle the problem of formatting. To that end, we'll use the BlockWriter type, which is a Monad for pretty-printing indented text that has two functions:

line :: String -> BlockWriter () which writes a line of text (at the current level of indentation),
block :: BlockWriter () -> BlockWriter () which increases the level of indentation for the argument BlockWriter(), and
render :: String -> BlockWriter () -> String, whose first argument is the indentation string, and whose second argument is a block to be printed.

We use these functions to produce a function for converting an Analysis to a human readable String.


    showAnalysis :: Analysis -> BlockWriter ()
    showAnalysis (Left (ps,val)) = do
        line $ "Refutable: " ++ show (head ps)
        block $ do
            when (not . null . tail $ ps) $ do
                line "Simplify: "
                block $ mapM_ (line . show) ps
            line "Refuting valuation:"
            block $ mapM_ (line . (\(k,v) -> k ++ " := " ++ show v)) (Map.toList val)
            line "Reduction:"
            block $ mapM_ (line . show) (simplify . substitute (toSub val). last $ ps)
    showAnalysis (Right qp) = do
        line $ "Tautology: " ++ show (getProp qp)
        block $ showQuine qp
        where
        getProp (Split ps _ _ _) = head ps
        getProp (Trivial ps) = head ps
        showQuine (Split ps v tp fp) = do
            when (not . null . tail $ ps) $ do
                line "Simplify: "
                block $ mapM_ (line . show) ps
            line $ unwords ["Case:",v,":= True"]
            block $ showQuine tp
            line $ unwords ["Case:",v,":= False"]
            block $ showQuine fp
        showQuine (Trivial ps) = mapM_ (line . show) ps

With this, and a simple main function, we have:


    $ quine "a -> a" "a | b -> a & b" "a | b -> (a -> c) -> (b -> c) -> c"
    Tautology: a -> a
      Case: a := True
        T -> T
        T
      Case: a := False
        F -> F
        T
    
    Refutable: a | b -> a & b
      Refuting valuation:
        a := True
        b := False
      Reduction:
        T | F -> T & F
        T -> T & F
        T & F
        F
    
    Tautology: a | b -> (a -> c) -> (b -> c) -> c
      Case: a := True
        Simplify: 
          T | b -> (T -> c) -> (b -> c) -> c
          T -> (T -> c) -> (b -> c) -> c
          (T -> c) -> (b -> c) -> c
          c -> (b -> c) -> c
        Case: b := True
          Simplify: 
            c -> (T -> c) -> c
            c -> c -> c
          Case: c := True
            T -> T -> T
            T -> T
            T
          Case: c := False
            F -> F -> F
            T
        Case: b := False
          Simplify: 
            c -> (F -> c) -> c
            c -> T -> c
            c -> c
          Case: c := True
            T -> T
            T
          Case: c := False
            F -> F
            T
      Case: a := False
        Simplify: 
          F | b -> (F -> c) -> (b -> c) -> c
          b -> (F -> c) -> (b -> c) -> c
          b -> T -> (b -> c) -> c
          b -> (b -> c) -> c
        Case: b := True
          Simplify: 
            T -> (T -> c) -> c
            (T -> c) -> c
            c -> c
          Case: c := True
            T -> T
            T
          Case: c := False
            F -> F
            T
        Case: b := False
          F -> (F -> c) -> c
          T
    $

While not perfect, this comes reasonably close to our goal of a human-readable proof. We still have the "proof optimization" to do, but this is enough for the Wednesday before Thanksgiving.

CMSC-16100

Honors Introduction to Programming, I

Autumn Quarter, 2015

Lecture 25: A Quine's Method Theorem Prover

Source Files: