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:

We'll start with code for simplifying a proposition:

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 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:

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:

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).

The Full Program