Lab03

In this scenario we investigate how to represent and manipulate formulas of first-order logic in Haskell.

Imports and utility functions

We begin with importing some basic modules and defining some utility functions that will be used throughout.

{-# LANGUAGE UnicodeSyntax, TypeSynonymInstances, FlexibleInstances, LambdaCase #-}
import Data.List
import Control.Monad
import Test.QuickCheck hiding (Fun)
partitions :: [a] -> [[[a]]]
partitions [] = [[]]
partitions (x:xs) = [[x]:yss | yss <- partitions xs] ++ [(x:ys):yss | (ys:yss) <- partitions xs]
-- all possible ways to split n into the sum of stricly positive integers
catalan :: Int -> [[Int]]
catalan n = map (map length) $ partitions [1..n]
todo = undefined
1.8s

Syntax of first-order logic

Names

For simplicity we use plain Strings to represent variable, function, and relation names.

type VarName = String
type FunName = String
type RelName = String
-- enumerate variants of a variable name
variants :: VarName -> [VarName]
variants x = x : [x ++ show n | n <- [0..]]
0.5s

For the purpose of testing, we want to generate just few distinct names:

instance {-# OVERLAPPING #-} Arbitrary VarName where
  arbitrary = elements ["x", "y", "z", "t"]
  
instance {-# OVERLAPPING #-} Arbitrary FunName where
  arbitrary = elements ["f", "g", "h", "i"]
  
instance {-# OVERLAPPING #-} Arbitrary RelName where
  arbitrary = elements ["R", "S", "T", "U"]
0.3s

Terms

Terms are defined by structural induction. In the base case we have just a variable. In the inductive case, we have a functional symbol together with a (possibly empty) list of arguments.

data Term = Var VarName | Fun FunName [Term] deriving (Eq, Show)
0.3s

For instance, we can compute the list of variables appearing in a term.

varsT :: Term -> [VarName]
varsT (Var x) = [x]
varsT (Fun _ ts) = nub $ concatMap varsT ts
0.3s

Generation of random terms, useful for testing:

instance Arbitrary Term where
  arbitrary = resize 8 $ sized f where
    f size | size == 0 || size == 1 = do x <- arbitrary
                                         return $ Var x
           | otherwise = frequency [ (1, go sizes) | sizes <- catalan size]
              where go sizes = do ts <- sequence $ map f sizes
                                  return $ Fun "f" ts
0.4s

Formulas

Formulas are also defined by structural induction. In the base case we have atomic formulas F, T, and relations applied to a list of terms Rel RelName [Term]. We also have the usual boolean connectives Not, And, Or, Implies, and Iff.

Finally, we have quantifiers. The existentially quantified formula inline_formula not implemented is represented by Exists x phi, where x is a variable name and phi is a formula. The case of the universal quantifier is similar.

data Formula =
  T |
  F |
  Rel RelName [Term] |
  Not Formula |
  And Formula Formula |
  Or Formula Formula |
  Implies Formula Formula |
  Iff Formula Formula |
  Exists VarName Formula |
  Forall VarName Formula deriving (Eq, Show)
infixr 8 /\, ∧
(/\) = And
(∧) = And
infixr 5 \/, ∨, ==>
(\/) = Or
(∨) = Or -- input with "\or"
(==>) = Implies
infixr 4 <==>, ⇔
(<==>) = Iff
(⇔) = Iff -- input with "\lr"
0.3s

Generation of random formulas for the purpose of testing:

instance Arbitrary Formula where
    arbitrary = resize 30 $ sized f where
      f 0 = do ts <- arbitrary
               return $ Rel "R" ts
      f size = frequency [
        (1, liftM Not (f (size - 1))),
        (4, do
              size' <- choose (0, size - 1)
              conn <- oneof $ map return [And, Or, Implies, Iff]
              left <- f $ size'
              right <- f $ size - size' - 1
              return $ conn left right),
        (5, do conn <- oneof $ map return [Exists, Forall]
               phi <- f $ size - 1
               x <- arbitrary
               return $ conn x phi)
        ]
0.5s

Variables

The following function collects all variables appearing in a formula:

vars :: Formula -> [VarName]
vars T = []
vars F = []
vars (Rel _ ts) = varsT (Fun "dummy" ts)
vars (Not phi) = vars phi
vars (And phi psi) = nub $ vars phi ++ vars psi
vars (Or phi psi) = nub $ vars phi ++ vars psi
vars (Implies phi psi) = nub $ vars phi ++ vars psi
vars (Iff phi psi) = nub $ vars phi ++ vars psi
vars (Exists x phi) = nub $ x : vars phi
vars (Forall x phi) = nub $ x : vars phi
0.3s

A variable is fresh in a formula if it does not appear therein:

freshIn :: VarName -> Formula -> Bool
x `freshIn` phi = not $ x `elem` vars phi
0.3s

The following function returns a variable which is fresh in a given formula. This will be useful later to avoid variable capture when working with substitution.

freshVariant :: VarName -> Formula -> VarName
freshVariant x phi = head [ y | y <- variants x, y `freshIn` phi ]
0.3s

Variable renaming

The following function replaces free occurrences of a variable name with another one.

renameT :: VarName -> VarName -> Term -> Term
renameT x y (Var z)
  | z == x = Var y
  | otherwise = Var z
renameT x y (Fun f ts) = Fun f (map (renameT x y) ts)
rename :: VarName -> VarName -> Formula -> Formula
rename x y T = T
rename x y F = F
rename x y (Rel r ts) = Rel r (map (renameT x y) ts)
rename x y (Not phi) = Not (rename x y phi)
rename x y (And phi psi) = And (rename x y phi) (rename x y psi)
rename x y (Or phi psi) = Or (rename x y phi) (rename x y psi)
rename x y (Implies phi psi) = Implies (rename x y phi) (rename x y psi)
rename x y (Iff phi psi) = Iff (rename x y phi) (rename x y psi)
rename x y (Forall z phi)
  | z == x = Forall z phi
  | otherwise = Forall z (rename x y phi)
rename x y (Exists z phi)
  | z == x = Exists z phi
  | otherwise = Exists z (rename x y phi)
0.4s

Example formulas

We can construct and print some example formulas. Drinker's paradox:

d x = Rel "d" [Var x]
drinker = Exists "x" (d "x" ==> Forall "y" (d "y"))
print drinker
0.5s

A version of the law of the excluded middle:

t x y = Rel "t" [Var x, Var y]
lem = Forall "x" $ Forall "y" $ t "x" "y" ∨ (Not $ t "x" "y")
print lem
0.5s
flip = Exists "x" (Forall "y" $ t "x" "y") ==> Forall "y" (Exists "x" $ t "x" "y")
print flip
0.5s

Normal forms

We are now ready to investigate normal form transformations.

Negation normal form (Exercise)

In the negation normal form (NNF) negation is applied only to atomic formulas (i.e., formulas of the form Rel r ts) and neither implication Implies nor bi-implication Iff is allowed*:*

is_nnf :: Formula -> Bool
is_nnf T = True
is_nnf F = True
is_nnf (Rel _ _) = True
is_nnf (Not (Rel _ _)) = True
is_nnf (And phi psi) = is_nnf phi && is_nnf psi
is_nnf (Or phi psi) = is_nnf phi && is_nnf psi
is_nnf (Implies phi psi) = False
is_nnf (Iff phi psi) = False
is_nnf (Not _) = False
is_nnf (Exists _ phi) = is_nnf phi
is_nnf (Forall _ phi) = is_nnf phi
0.9s

Define a function that transforms a given formula of first-order logic into a logically equivalent formula in NNF. Hint: Push the negation inside the formula based on de Morgan’s laws. For the universal quantifier, we have inline_formula not implemented, and dually for the existential quantifier.

nnf :: Formula -> Formula
nnf = todo
0.3s

We can test that nnf produces formulas in NNF:

nnfProp :: Formula -> Bool
nnfProp phi = is_nnf (nnf phi)
-- quickCheck nnfProp
0.3s

Prenex normal form (Exercise)

A formula is in prenex normal form (PNF) if its quantifiers appear at the beginning of the formula:

is_pnf :: Formula -> Bool
is_pnf (Forall _ phi) = is_pnf phi
is_pnf (Exists _ phi) = is_pnf phi
is_pnf phi = qf phi
-- check whether the formula is quantifier-free
qf :: Formula -> Bool
qf (Rel _ _) = True
qf (Not phi) = qf phi
qf (And phi psi) = qf phi && qf psi
qf (Or phi psi) = qf phi && qf psi
qf (Implies phi psi) = qf phi && qf psi
qf (Iff phi psi) = qf phi && qf psi
qf _ = False
0.3s

Write a function that transforms every formula of first-order logic into a logically equivalent formula in PNF.

Hint: Apply NNF first. Then pull the quantifiers outside inside-out (i.e., starting from the innermost formulas) using the following equivalences:

formula not implemented

Similar equivalences hold for extracting a quantifier on the right, and for the existential quantifier (eight equivalences in total). The side condition inline_formula not implemented requires that inline_formula not implemented is fresh in inline_formula not implemented. If inline_formula not implemented is not fresh in inline_formula not implemented, then:

  1. We need to find a variable inline_formula not implemented which is fresh in inline_formula not implemented and inline_formula not implemented. We can use freshVariant for this.

  2. We need to replace every free occurrence of inline_formula not implemented in inline_formula not implemented with inline_formula not implemented. We can use rename for this.

TODO: discuss optimisations pertaining pulling two quantifiers at once when applicable.

pnf :: Formula -> Formula
pnf = todo
0.3s

Tests:

pnfProp = is_pnf . pnf
-- quickCheck pnfProp
0.3s

Runtime setup (IGNORE ME)

stack install QuickCheck
4.9s
Runtimes (2)
Runtime Languages (1)