Just figured out how to turn on literate haskell mode in aquamacs, so I’m going to try this literate blogging thing again, by walking through the construction of a tautology checker in Haskell. I mentioned in my first post that I would be attending the Oregon Programming Languages Summer School (OPLSS), but I never made the time to blog about any of it, so this is the start of an attempt to rectify that.
Robert Constable gave a series of three lectures on the topic of "Proofs as Processes", and while I didn’t quite have the background to understand much of his talk, in his first lecture he mentioned a book "First Order Logic" by Raymond M. Smullyan. I managed to find the books at Powell’s in Portland and I will be basing the tautology checker in this post on the method of tableaux that is introduced early in Smullyan’s book.
For now all symbols used will be ascii renditions of what they are meant to look like.
~X should be read as "not" X. X /\ Y should be read as X "and" Y or the "conjunction" of X and Y. X \/ Y should be read as X "or" Y or the "disjunction" of X and Y. X => Y should be read as X "implies" Y.
Smullyan begins his presentation of analytic tableaux by making note of certain relations that hold amongst these operators that hold for any interpretation. These rules are
If ~X is true then X is false. If ~X is false then X is true. If X /\ Y is true then X is true and Y is true. If X /\ Y is false then either X is false or Y is false. If X \/ Y is true then either X is true or Y is true. If X \/ Y is false then X is false and Y is false. If X => Y is true then either X is false or Y is true. If X => Y is false then X is true and Y is false.
Before introducing the notion of a signed formula, which Smullyan uses to introduce analytic tableaux, we will first need to come up with a Haskell datatype to represent logical formulas, but this follows fairly easily from the description of the opertators above.
> data Formula = Var String > | Not Formula > | And Formula Formula > | Or Formula Formula > | Implies Formula Formula > deriving (Read,Show)
This is a pretty straightforward definition of a logical formula in Haskell. A formula can be either a variable (Var) represented by a string, the negation (Not) of another formula, the conjunction (AND) of two formulas, thedisjunction (Or) of two formulas, or the statement that one formula implies another (Implies).
Now let’s get to work and introduce signed formulas which will end up being the driving force behind this tautology checker.
> data Signed = T Formula > | F Formula > deriving (Read,Show)
That is to say a signed formula is the same as a regular logical formula as defined above, except that we will now mark it with either a T or an F. These signed formulas must obey some rules in order to be useful though, specifically we will have that if X is a formula then the following hold:
TX is true whenever X is true, and false when X is false.
FX is true whenever X is false, and false when X is true.
Now we can write down the rules above using this new notion of a signed formula.
T~X -> FX F~X -> TX T(X /\ Y) -> TX, TY F(X /\ Y) -> FX | FY T(X \/ Y) -> TX | TY F(X \/ Y) -> FX, FY T(X => Y) -> FX | TY F(X => Y) -> TX, FY
A brief note on the notation here, I am using the arrow (->) to roughly mean reduces to or something vaguely equivalent to that, similarly the bar (|) is the same symbol used in Smullyan’s book to represent the disjunction of the two options, that either could hold so we must consider each seaparately, and lastly the comma (,) also used in Smullyan’s book denotes that both of these conditions will hold if the left hand side of the arrow holds.
We can try to represent this using the datatypes we just defined.
> -- x :: Formula > -- y :: Formula > -- F (Not x) ...
Well we run into a problem pretty quick trying that, we need something to represent what’s going on the right hand side of the rules we just defined. Well everything on the right hand side of the rules above is either a signed formula, the notion that two formulas hold, or the notion that the formula branches into two signed formulas. Let’s come up with a new datatype to deal with this.
> data Tableaux = SF Signed > | Both Signed Signed > | Branch Signed Signed > deriving (Read,Show)
This will allow us to express the branching and both notions that occur when reducing complex signed formulas, and now we could write a function to reduce a signed formula (SF) using the rules we just devised.
> reduce :: Signed -> Tableaux > reduce (T f) = case f of > Not x -> SF (F x) > And x y -> Both (T x) (T y) > Or x y -> Branch (T x) (T y) > Implies x y -> Branch (F x) (T y) > reduce (F f) = case f of > Not x -> SF (T x) > And x y -> Branch (F x) (F y) > Or x y -> Both (F x) (F y) > Implies x y -> Both (T x) (F y)
I’m going to leave off here for now, and pick it up after I read a little further into the book. Check back soon for more updates to this post.