Blog

Verifying tautologies with Haskell

14th Jun 2019 haskell logic programming

This post gives the source code for a small Haskell program that finds if a formula is a tautology.

Verifying tautologies with Haskell

A tautology is a formula that is true regardless of the logical value we attribute to the variables it contains. For example, the propositional formula $P \vee \neg P$ is always true, regardless of $P$ being true or false. But not every tautology is as simple as the one I just showed. For example, showing that

$(P \implies Q) \implies [(Q \implies R) \implies (P \implies R)]$

is a tautology requires a bit more thought. But thinking is too tiring, so let us write a Haskell program that takes a formula and decides if the formula is a tautology or not! (By the way, said program is available in my GitHub...) First, we need to be able to represent a proposition, and we will create a data type just for that. We will call our type "Prop," from proposition, from propositional logic.

	data Prop =
	Const Bool
	\| Var String
	\| Neg Prop
	\| And Prop Prop
	\| Or Prop Prop
	\| Equiv Prop Prop
	\| Impl Prop Prop
	deriving (Eq, Show)

view raw tautologies.hs hosted with ❤ by GitHub

where we provided data constructors for all sorts of propositional formulas. The idea is that now the formula $P \vee \neg P$ is represented as Or (Var "P") (Neg (Var "P")).

Now we have a way of representing formulas. What we are left with is having a way of evaluating those formulas to check if they are tautologies... Propositions will have variables, so we will need to collect the variables of a proposition, generate all possible combinations of values to attribute to all the variables, and then evaluate the logical value of the proposition with the given attribution. Notice that most of our functions will make use of the structure of the data Prop in order to do some sort of "recursion," but on the structure of the proposition. For example, if you have a proposition p = Or p1 p2, then the variables in $p$ are the variables in $p_1$ concatenated with the variables in $p_2$ .

	-- given a proposition, return a list with all the variables that show up
	collectVars :: Prop -> [String]
	collectVars (Const _ ) = []
	collectVars (Var s ) = [s]
	collectVars (Neg prop) = nub $ collectVars prop
	-- these four patterns are rather annoying
	collectVars (And p1 p2) = nub $ (collectVars p1) ++ (collectVars p2)
	collectVars (Or p1 p2) = nub $ (collectVars p1) ++ (collectVars p2)
	collectVars (Equiv p1 p2) = nub $ (collectVars p1) ++ (collectVars p2)
	collectVars (Impl p1 p2) = nub $ (collectVars p1) ++ (collectVars p2)

view raw tautologies.hs hosted with ❤ by GitHub

Now that we have all variables, we can generate all the possible combinations of values they can take. If we only have one variable, that is $T, F$ . If we have two variables, that's $TT$ , $TF$ , $FT$ , $FF$ . If we have three variables, ... I define the function that generates all possible combinations of true/false values and then put them together with our variables.

	type Attribution = [(String, Bool)]

	-- given a list of variables, returns a list with all possible attributions
	varAttributions :: [String] -> [Attribution]
	--varAttributions vars = map (zipWith (,) vars) tables
	varAttributions vars = map (zip vars) tables
	where
	tables = allTruthTables $ length vars

	-- generates all 2^n truth tables for n variables
	allTruthTables :: Int -> [[Bool]]
	allTruthTables 0 = [[]]
	allTruthTables n = ((True:) <$> prevTables) ++ ((False:) <$> prevTables)
	where
	prevTables = allTruthTables (n-1)

view raw tautologies.hs hosted with ❤ by GitHub

And now that we can define attributions for our variables, we can write a function that takes a proposition and an attribution, and evaluates the proposition according to the attribution! Our function will have the signature Prop -> Attribution -> Maybe Bool because we cannot know for sure that the attribution that is passed in contains all the variables present in the proposition.

	-- given a proposition and an attribution, return its truth value
	-- (TODO) could be nice to implement the binary operators with short-circuiting logic
	truthValue :: Prop -> Attribution -> Maybe Bool
	truthValue (Const bool) _ = Just bool
	truthValue (Var v ) attrs = lookup v attrs
	truthValue (Neg p ) attrs = not <$> (truthValue p attrs)
	truthValue (And p1 p2) attrs = (&&) <$> (truthValue p1 attrs) <*> (truthValue p2 attrs)
	truthValue (Or p1 p2) attrs = (\|\|) <$> (truthValue p1 attrs) <*> (truthValue p2 attrs)
	truthValue (Equiv p1 p2) attrs = (==) <$> (truthValue p1 attrs) <*> (truthValue p2 attrs)
	-- maybe it is cheating, but b1 <= b2 as "less than or equal to" evaluates to the same thing
	-- as "b1 implies b2"!
	truthValue (Impl p1 p2) attrs = (<=) <$> (truthValue p1 attrs) <*> (truthValue p2 attrs)

view raw tautologies.hs hosted with ❤ by GitHub

We are very close to the finish line! Given a proposition $p$ , how do we check if it is a tautology? Well, we should generate all of the possible attributions for it, evaluate each one of them, and check if all the attributions made the proposition true! And that is exactly what we do in the next few lines:

	-- given a proposition, evaluate it at all of its attributions
	extensiveEvaluation :: Prop -> [Bool]
	extensiveEvaluation prop = unwrap values
	where
	vars = collectVars prop
	attributions = varAttributions vars
	-- use sequence to make this [Maybe Bool] a Maybe [Bool]
	values = sequence $ map (truthValue prop) attributions
	unwrap (Just j) = j
	-- if "attributions" is calculated with my varAttributions then "truthValue"
	-- will never return a Nothing, so that "map (truthValue prop) attributions" is
	-- a list of a lot of (Just bool) and no Nothing shows up
	unwrap Nothing = error "everything just crashed!"

	-- checks if a given proposition is a tautology
	tautology :: Prop -> Bool
	tautology = and . extensiveEvaluation

view raw tautologies.hs hosted with ❤ by GitHub

Now that our program is written down, we can actually check some tautologies!

We will check the tautology I presented in the beginning and three more tautologies: the definitions of "and," "or," and "equivalent" in terms of negation and implication. That is, $P \vee Q$ , $P \wedge Q$ , and $P \iff Q$ can be written down only using negations and implications, and I will use this program to check that!

	-- P v Q <=> (~P => Q)
	prop1 = Equiv
	(Or (Var "P") (Var "Q"))
	(Impl (Neg (Var "P")) (Var "Q"))
	-- P ^ Q <=> ~(P => ~Q)
	prop2 = Equiv
	(And (Var "P") (Var "Q"))
	(Neg (Impl (Var "P") (Neg (Var "Q"))))
	-- (P <=> Q) <=> ~((P => Q) => ~(Q => P))
	prop3 = Equiv
	(Equiv (Var "P") (Var "Q"))
	(Neg (Impl
	(Impl (Var "P") (Var "Q"))
	(Neg (Impl (Var "Q") (Var "P")))
	))
	-- (P => Q) => [(Q => R) => (P => R)]
	prop4 = Impl
	(Impl (Var "P") (Var "Q"))
	(Impl
	(Impl (Var "Q") (Var "R"))
	(Impl (Var "P") (Var "R"))
	)

	main = do
	print $ tautology prop1
	print $ tautology prop2
	print $ tautology prop3
	print $ tautology prop4

view raw tautologies.hs hosted with ❤ by GitHub

And obviously, this will print "True" four times.

On my GitHub page, you can find this program with two extra functions, falsify and truthify, that try to find an attribution that makes the given proposition evaluate to false/true.

Come take a course!

The next cohort of the Intermediate Python Course starts soon.

Grab your spot now and learn the Python skills you've been missing!

Previous Post Next Post