Propositional logic and recursive datatypes

Sentences of propositional logic:

• \(p \wedge q\)
• \(p \wedge (q \rightarrow r)\)
• \(p \vee \neg (q \wedge p)\)
• \(\bot \rightarrow (\top \vee (q \wedge r))\)

To state a grammar for propositional logic, we first need a set of variables \(\mathbf{Var} := \set{p, q, r, \ldots}\), and a set of constants \(\set{\top,\bot}\).

• If \(p \in \mathbf{Var} \cup \set{\top,\bot}\), then \(p\) is a sentence of propositional logic.
• If \(\phi,\psi\) are sentences of propositional logic, then \((\phi \wedge \psi)\) is a sentence of propositional logic.
• If \(\phi,\psi\) are sentences of propositional logic, then \((\phi \vee \psi)\) is a sentence of propositional logic.
• If \(\phi,\psi\) are sentences of propositional logic, then \((\phi \rightarrow \psi)\) is a sentence of propositional logic.
• If \(\phi \) is a sentence of propositional logic, then so is \(\neg \phi \)

We'll use a sum type to implement the grammar of propositional logic. We can start with just the following:

data PropL = PVar String deriving (Eq,Show)

ghci> :t (PVar "p1")
PropL
ghci> :t (PVar "p3")
PropL

data PropL = PVar String | PNot PropL deriving (Eq,Show)

Note that we reuse PropL in the constructor for negative sentences; this means that if an expression p is of type PropL, then PNot p is of type PropL.

ghci> :t (PNot (PVar "p1"))
PropL
ghci> :t (PNot (PNot (PNot (PVar "p1")))
PropL

Note that this already gives us infinite inhabitants of type PropL.

Functions that take two arguments can be used as infix operators by enclosing them in backticks. This also goes for constructors:

ghci> :t PAnd
  PropL -> PropL -> PropL
ghci> :t ((PVar "p1") `PAnd` (PVar "p2"))
PropL

You can even use infix constructors in the data declaration:

data PropL = PVar String | PNot PropL | PropL `PAnd` PropL | PropL `POr` PropL deriving (Eq,Show)

Implementing a custom Show instance for PropL simply amounts to defining a function show of type PropL -> String.

data PropL = PVar String | PNot PropL | PropL `PAnd` PropL | PropL `POr` PropL deriving Eq

instance Show PropL where
  show (PVar s) = s
  show (PNot p) = "~" ++ show p
  show (p `PAnd` q) = "(" ++ show p ++ " & " ++ show q ++ ")"
  show (p `POr` q) = "(" ++ show p ++ " | " ++ show q ++ ")"

The Show instance we just declared will automatically be used by ghci.

ghci> ((PVar "p1") `PAnd` (PNot ((PVar "p1") `POr` (PVar "p3")))
(p1 & ~(p2 | p3)) 

We can also use it explicitly by calling show on something of type PropL.

Recursive datatypes are used to create an Abstract Syntax Tree (AST) for sentences of propositional logic.

Let's say that we want to compute the number of operators in a formula. In order to do so we'll need a recursive function opsNr.

First, we define the base of the recursion (where the recursion halts):

opsNr :: PropL -> Int
opsNr (PVar _) = 0

For all other cases we need recursion:

opsNr :: PropL -> Int
opsNr (PVar _) = 0
opsNr (PNot p) = 1 + opsNr p
opsNr (PAnd p q) = 1 + opsNr p + opsNr q
opsNr (POr p q) = 1 + opsNr p + opsNr q

• Exercise: write a recursive function that returns a list of all of the variables that occur in a formula.
• As a bonus, remove duplicates and sort the output alphabetically.

• A formula of propositional logic is in conjunctive normal form (CNF) iff it is a conjunction of one of more clauses.
  • A clause is a disjunction of one or more literals; a literal is either a propositional variable, or the negation of a propositional variable.
  • Some formulas in conjunctive normal form:
• \((p \vee \neg q \vee r) \wedge s\)
• \((p \vee q) \wedge r\)
• \(p\)

• Any formula can be converted into CNF by successively applying the following rules of inference:
  • \(\neg \neg \phi \Rightarrow \phi \) (Double Negation Elimination; DNE)
  • \(\neg (\phi \vee \psi) \Rightarrow \neg \phi \wedge \neg \psi\) (De Morgan's law 1; dM1)
  • \(\neg (\phi \wedge \psi) \Rightarrow \neg \phi \vee \neg \psi\) (De Morgan's law 2; dM1)
  • \(\phi \vee (\psi \wedge \rho) \Rightarrow (\phi \vee \psi) \wedge (\phi \vee \rho)\) (Distributive Law; DL)
• Conversion to CNF can be accomplished by:
  • Pushing negations in, by repeatedly applying dM.
  • Getting rid of any double negations via DNE.
  • Repeatedly applying DL, to get rid of disjunctions applying over conjunctions.

\[\neg (\neg (p \vee q) \wedge r) \wedge \neg (p \wedge r)\]

\[\begin{aligned}[t] &\Rightarrow (\neg \neg (p \vee q) \vee r) \wedge \neg (p \wedge r)\\ &\Rightarrow (\neg \neg (p \vee q) \vee r) \wedge (\neg p \vee \neg r)\\ &\Rightarrow (p \vee q \vee r) \wedge (\neg p \vee \neg r) \end{aligned}\]

• Let's try to write a function to implement this procedure in Haskell.
• We know what the type of this function should be:

toCNF :: PropL -> PropL
toCNF = undefined

We'll break this function down into three steps.

• First, let's push negations inward by repeatedly applying dM.
• Second, let's get rid of any resulting double negations.
• Third, let's distribute conjunctions over disjunctions.

toCNF :: PropL -> PropL
toCNF = distributeConj . elimDN . pushNegsIn

dM :: PropL -> PropL
dM :: PropL -> PropL   

dne :: PropL -> PropL
dne = undefined

distLaw :: PropL -> PropL
distLaw = undefined

We can apply de Morgan's via heavy use of pattern matching.

dM :: PropL -> PropL
dM (PNot (p `POr` q)) = (PNot p) `PAnd` (PNot q)
dM p = p

Pattern matching applies wherever possible, making the second line an elsewhere case.

• Note that the function we just defined is not recursive.
  • It only applies de Morgan's if the top level formula matches the structural description imposed by pattern matching.

ghci> dM (PVar "p1" `PAnd` PNot (PVar "p2" `POr` PVar "p3"))
(p1 & ~(p2 | p3))

• In order to eventually convert to CNF we need to apply dM recursively.
• Exercise: write a recursive variant of dM.

• Double negation elimination is a bit simpler.
• First, the non-recursive variant:

dne :: PropL -> PropL
dne (PNot (PNot p)) = p
dne p = p

• Exercise: make this apply recursively

First, the non-recursive variant (we're really stretching the limits of pattern matching):

Our statement of the distributive law actually subsumes three different cases:

distLaw :: PropL -> PropL 
distLaw ((p `PAnd` q) `POr` (r `PAnd` s)) = (p `POr` r) `PAnd` (p `POr` s) `PAnd` (q `POr` r) `PAnd` (q `POr` s) -- double distributivity
distLaw (p `POr` (q `PAnd` r)) = (p `POr` q) `PAnd` (p `POr` r) --left dist
distLaw ((q `PAnd` r) `POr` p) = (q `POr` p) `PAnd` (r `POr` p) --right dist
distLaw p = p

• Exercise: write the recursive variant!

• A function that maps formulas of propositional logic to a truth table.
• You can treat a truth table as a list of pairs of variable assignments and truth values.
• A variable assignment is a list of pairs of variables and truth values.

\(\mathscr{Fin}\)