# Lecture 25: A Quine's Method Theorem Prover

Our goal for today is ambitious. We will write a program that will take as input a series of propositions (intended to be tautologies, but checked as such), and will produce a web page that consists of a series of Quine-style proofs, using the mathematical typesetting language TeX (strictly speaking, LaTeX) to render boolean formulae in a attractive way. I.e., we'll take input file that looks like this:

``` a -> a a -> b -> a a -> (a -> b) -> b ```

and produce web content that looks like this:

There are a lot of moving parts here!

## Quine's method

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.

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

Much of the heavy lifting is done by `simpleEval`, which essentially eliminates the contextualizing type constructor of the last lecture's `abstractEval`.

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, as it does here.

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 = simpleEval varf Boolean Not And Or Implies where varf v = Map.findWithDefault (Var v) v sub ```

The idea here is that `substitution` includes as keys only the names of variables that we're substituting out, so a missing key simply means a variable that we're not changing.

Our first cut at our theorem prover uses a simple type for representing a quine-style proof:

``` 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 -- ^ the proof of True 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.

``` analyze :: Proposition -> Analysis analyze prop = case simplify prop of Boolean True -> pure Trivial Boolean False -> Nothing q -> Split q v <\$> branch True <*> branch False where v = elemAt 0 . variables \$ q branch b = analyze (substitute (Map.singleton v (Boolean b)) q) ```

This is just a simple realization of Quine's algorithm. We will get more sophisticated soon. 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 `Boolean True`, but rather to itself. We split on `"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 format 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.

``` simplifyInSteps :: Proposition -> [Proposition] simplifyInSteps = converge step where converge f = untilFixed . iterate f where untilFixed (p:qs@(q:_)) | p == q = [p] | otherwise = p : untilFixed qs untilFixed _ = error "untilFixed: impossible error" step prop = case prop of v@(Var _) -> v b@(Boolean _) -> b Not p -> case p of Boolean b -> Boolean (not b) Not p' -> p' _ -> Not \$ step p And p q -> case (p,q) of (Boolean True,_) -> q (Boolean False,_) -> Boolean False (_,Boolean True) -> p (_,Boolean False) -> Boolean False _ -> And (step p) (step q) Or p q -> case (p,q) of (Boolean True,_) -> Boolean True (Boolean False,_) -> q (_,Boolean True) -> Boolean True (_,Boolean False) -> p _ -> Or (step p) (step q) Implies p q -> case (p,q) of (Boolean True,_) -> q (Boolean False,_) -> Boolean True (_,Boolean True) -> Boolean True (_,Boolean False) -> Not p _ -> Implies (step p) (step q) ```

This isn't a perfect solution to the simplify-in-steps problem (it may make multiple simplifications, but at least they'll be in distinct parts of the expression), but it's a bit of improvement for now. The key is the local `step` function, which only calls itself recursively in the cases where it can't make progress otherwise. This is driven by `converge`, which iterates `step` until it reaches a fixed point.

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] -- ^ simplifications String -- ^ variable to split on QuineProof -- ^ case where split variable is true QuineProof -- ^ case where split variable is false | Trivial [Proposition] -- ^ simplifications ```

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:

``` data Refutation = Refutation (Map String Bool) type Analysis = Either Refutation QuineProof ```

But we're not done yet. We want to handle a sequence of propositions, as logic texts invariably do, precisely so that we can make our proofs "shallower," by cutting off our Quine-style proofs when we get a formula that's a substitution instance of an earlier formula. This results in an appreciably more complex type for our :

``` type Heuristic = Proposition -> Maybe String analyzeWithHeuristic :: Heuristic -- variable selection heuristic -> [(Int,Proposition)] -- list of indexed tautologies -> Proposition -- the Proposition to analyze -> Analysis ```

There are a couple of twists here. The `Heuristic` type is used to pick a variable for splitting on. We allow a `Heuristic` to return `Nothing` if its argument contains no variables. The second argument to `analyzeWithHeuristic` is a list of tautologies (already proven), paired with an `Int` which identifies the proposition which established it.

To determine whether or not a `Proposition` is a substitution instance of a given propositional formula, we use

``` instanceOf :: Proposition -> Proposition -> Maybe Substitution instanceOf target pattern = case (target,pattern) of (t, Var v) -> Just \$ Map.singleton v t (Boolean t,Boolean p) -> guard (t == p) >> pure Map.empty (Not t, Not p) -> instanceOf t p (And t1 t2, And p1 p2) -> process t1 t2 p1 p2 (Or t1 t2, Or p1 p2) -> process t1 t2 p1 p2 (Implies t1 t2, Implies p1 p2) -> process t1 t2 p1 p2 _ -> Nothing where process t1 t2 p1 p2 = do m1 <- instanceOf t1 p1 m2 <- instanceOf t2 p2 if m1 `Map.intersection` m2 == m2 `Map.intersection` m1 then pure \$ Map.union m1 m2 else Nothing ```

This tries to build substitutions, but the trickiness comes from combining them. We do this fairly simply, by relying on the left-bias of `Map` operators, in this case `intersection`, to insure that in the case we have to follow two branches, that we derive identical substitutions or fail.

There are a fair number of details being swept under the rug here, which you can find out by reading the code.

## Producing HTML

The output side of this program will use `Text.Blaze.Html5` and related modules to render HTML. We'll pass over the specifics of generating TeX—as they're not all that different from generating the kind of text-based output we've used so far.

A key output handling procedure is

``` renderProof ix prop proof = do h2 \$ "Proposition " >> toHtml ix >> ": " >> toHtml' prop format proof p ! class_ "box" \$ "\$\\Box\$ Proposition " >> toHtml ix where format prf = case prf of Split props var trueb falseb -> do when (length props > 1) \$ do p "Simplification" ul . void \$ traverse (li . toHtml') props let prop' = last props p "Quine Alternatives:" ul \$ do li \$ showBranch prop' var True trueb li \$ showBranch prop' var False falseb Trivial props -> do p "Simplification" ul . void \$ traverse (li . toHtml') props p \$ "Reduced to " >> toHtml' (Boolean True) >> "." Reference props citation pattern bindings -> do ul . void . traverse (li . toHtml') \$ props p \$ "Substitution instance of Proposition " >> toHtml citation >> "\$[" >> toTeX pattern >> "]\$ at" ul . void . flip Map.traverseWithKey bindings \$ \k v -> li \$ "\$" >> greekDict Map.! k >> " := " >> toTeX v >> "\$" showBranch prop' var bool branch = p \$ do toHtml' prop' >> " \$[" >> greekDict Map.! var >> ":=" >> boolDict Map.! bool >> "]\$" format branch ```

Note here the additional `Reference` case to `QuineProof`. This is a fairly straightforward recursive processing of a proof tree, in as much as the structure of `QuineProof` type is mirrored in the structure of the resulting HTML. There are a couple of things to notice here. We have the `{-# LANGUAGE OverloadedStrings #-}` pragma on, which allows literal strings in the source to be interpreted via the `IsStrihg` type class, which implements a `fromString :: String -> a` function, similar to `fromInt`. There's also the `toHtml'` function, which parallels `Blaze`'s `toHtml`, but is specific to the `Proposition` type (a minor work-around necessary to avoid a orphaned instance warning).