Lab04

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 Control.Monad.State
import Test.QuickCheck hiding (Fun)
update :: Eq a => (a -> b) -> a -> b -> a -> b
update f a b x | x == a = b
               | otherwise = f x
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]
-- alternating merge of two (potentially infinite) lists
merge :: [a] -> [a] -> [a]
merge [] bs = bs
merge (a : as) bs = a : merge bs as
-- alternating merge of a (potentially infinite) list of (potentially infinite) lists
merges :: [[a]] -> [a]
merges [] = []
merges (as:ass) = merge as (merges ass)
-- collect all functions from a finite list to a (potentially infinite) list
functions :: Eq a => [a] -> [b] -> [a -> b]
functions [] _ = [undefined]
functions (a:as) bs = merges [[update f a b | f <- functions as bs] | b <- bs]
todo = undefined
previousLab = undefined
2.1s

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.4s

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.2s

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.6s

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.3s

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.4s

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

Free variables [NEW]

fv :: Formula -> [VarName]
fv T = []
fv F = []
fv (Rel _ ts) = varsT (Fun "dummy" ts)
fv (Not phi) = fv phi
fv (And phi psi) = nub $ fv phi ++ fv psi
fv (Or phi psi) = nub $ fv phi ++ fv psi
fv (Implies phi psi) = nub $ fv phi ++ fv psi
fv (Iff phi psi) = nub $ fv phi ++ fv psi
fv (Exists x phi) = delete x $ fv phi
fv (Forall x phi) = delete x $ fv phi
prop_fv = fv (Exists "x" (Rel "R" [Fun "f" [Var "x", Var "y"], Var "z"])) == ["y", "z"]
quickCheck prop_fv
0.5s

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.3s

Substitution [NEW]

We generalise variable renaming in two respects:

  1. We replace a variable with a whole term (rather than just another variable).

  2. We replace several variables at once.

type Substitution = VarName -> Term
substT :: Substitution -> Term -> Term
substT σ (Var x) = σ x
substT σ (Fun f ts) = Fun f (map (substT σ) ts)
subst :: Substitution -> Formula -> Formula
subst _ T = T
subst _ F = F
subst σ (Rel r ts) = Rel r $ map (substT σ) ts
subst σ (Not phi) = Not $ subst σ phi
subst σ (And phi psi) = And (subst σ phi) (subst σ psi)
subst σ (Or phi psi) = Or (subst σ phi) (subst σ psi)
subst σ (Implies phi psi) = Implies (subst σ phi) (subst σ psi)
subst σ (Iff phi psi) = Iff (subst σ phi) (subst σ psi)
subst σ (Exists x phi) = Exists x (subst (update σ x (Var x)) phi)
subst σ (Forall x phi) = Forall x (subst (update σ x (Var x)) phi)
0.3s

Note that in the case of quantifiers we need to enforce that the quantified variable x is replaced by itself during the substitution (since its occurrences are not free).

Generalisation (universal closure) [NEW]

We will need a simple function which transforms a formula into a sentence by universally quantifying all free variables.

generalise :: Formula -> Formula
generalise phi = go $ fv phi
  where go [] = phi
        go (x:xs) = Forall x $ go xs
prop_generalise = generalise (Exists "x" (Rel "R" [Fun "f" [Var "x", Var "y"], Var "z"])) == Forall "y" (Forall "z" (Exists "x" (Rel "R" [Fun "f" [Var "x",Var "y"],Var "z"])))
quickCheck prop_generalise
0.5s

Fresh rename [NEW]

It will be convenient to have a function giving unique names to all quantified variables.

fresh :: Formula -> Formula
fresh phi = evalState (go phi) []
  where go :: Formula -> State [VarName] Formula
        go T = return T
        go F = return F
        go phi@(Rel _ _) = return phi
        go (Not phi) = liftM Not (go phi)
        go (And phi psi) = liftM2 And (go phi) (go psi)
        go (Or phi psi) = liftM2 Or (go phi) (go psi)
        go (Implies phi psi) = liftM2 Implies (go phi) (go psi)
        go (Iff phi psi) = liftM2 Iff (go phi) (go psi)
        go (Forall x phi) = go2 Forall x phi
        go (Exists x phi) = go2 Exists x phi
        
        go2 quantifier x phi =
          do xs <- get
             let y = head [y | y <- variants x, not $ y `elem` xs]
             let psi = rename x y phi
             put $ y : xs
             liftM (quantifier y) $ go psi
0.3s

Example:

phi = Exists "x" (Exists "x" (Rel "r" [Fun "f" [Var "x", Var "y"]]))
psi = Exists "x" (Rel "r" [Fun "f" [Var "x"]])
fresh (And phi psi)
0.4s

Normal forms

We are now ready to investigate normal form transformations.

Negation normal form

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

Prenex normal form

-- prenex normal form (all quantifiers in front)
pnf :: Formula -> Formula
pnf = previousLab
0.4s

Skolem normal form (Exercise)

A formula is in Skolem normal form if it is in PNF and containing only universally quantified variables.

  1. Close the formula by quantifying existentially all the free variables, thus obtaining a sentence. (Recall that we want to produce an equisatisfiable formula.)

  2. Transform the sentence to NNF. Use nnf.

  3. Give all the existentially quantified variables globally unique names. Use fresh.

  4. [OPTIONAL] Miniscoping: Push the quantifiers as much as possible inside the formula. (This transformation is the inverse of PNF.)

  5. Replace an existential variable y under the scope of universally quantified variables x1...xn by the term (Skolem function) Fun y [x1, ..., xn]. Proceed top-down by structural induction on the formula.

  6. Transform the sentence to PNF.

(The optional miniscoping (step 4) improves the quality of Skolemisation since it reduces the dependency of existential variables on the universal ones, and thus it reduces the arity of the Skolem functions created in step 5.)

skolemise :: Formula -> Formula
skolemise = todo
0.8s
prop_skolemise1 = skolemise (Forall "x" $ Exists "y" $ Rel "P" [Var "x", Var "y"] /\ Rel "Q" [Var "y"]) == Forall "x" (And (Rel "P" [Var "x", Fun "y" [Var "x"]]) (Rel "Q" [Fun "y" [Var "x"]]))
0.3s

Decision procedure for the inline_formula not implemented fragment

In this section we define a decision procedure aedecide to solve the tautology problem for formulas in the inline_formula not implemented-fragment of first order logic containing only constant symbols, and no function symbols.

Signature

We define a function that extracts the functional signature inline_formula not implemented from a given formula. A signature is just a list of function symbol names together with their arity.

type Arity = Int
type Signature = [(FunName, Arity)]
0.2s

The code to extract the signature from terms and formulas is straightforward:

sigT :: Term -> Signature
sigT (Var _) = []
sigT (Fun f ts) = nub $ (f, length ts) : concatMap sigT ts
sig :: Formula -> Signature
sig T = []
sig F = []
sig (Rel r ts) = concatMap sigT ts
sig (Not phi) = sig phi
sig (And phi psi) = nub $ sig phi ++ sig psi
sig (Or phi psi) = nub $ sig phi ++ sig psi
sig (Implies phi psi) = nub $ sig phi ++ sig psi
sig (Iff phi psi) = nub $ sig phi ++ sig psi
sig (Exists _ phi) = sig phi
sig (Forall _ phi) = sig phi
0.3s

It will be useful to select the constants (i.e., arity-0 function symbols) from a given signature:

constants :: Signature -> [Term]
constants s = [Fun c [] | (c, 0) <- s]
0.2s

Ground instances (Exercise)

A term or formula is ground if it does not contain any variable. Ground formulas are very close to formulas of propositional logic, except that atomic formulas are of the form inline_formula not implemented and the terms inline_formula not implemented's contain only constant and functional symbols (no variables).

Write a function that given a quantifier-free formula and a list of (ground) terms returns the list of all formulas with can be obtained by replacing the free variables with the (ground) terms in all possible ways (c.f. the example below).

groundInstances :: Formula -> [Term] -> [Formula]
groundInstances φ ts = todo
0.3s

Example:

groundInstances
  (Rel "r" [Var "x", Var "x", Var "y"])
  [Fun "c" [], Fun "d" []]
    == [
      Rel "r" [Fun "c" [],Fun "c" [],Fun "c" []],
      Rel "r" [Fun "d" [],Fun "d" [],Fun "c" []],
      Rel "r" [Fun "c" [],Fun "c" [],Fun "d" []],
      Rel "r" [Fun "d" [],Fun "d" [],Fun "d" []]
      ]
0.4s

Atomic formulas

We need the following straightforward procedure that computes all the atomic formulas of a given formula.

atomicFormulas :: Formula -> [Formula]
atomicFormulas T = []
atomicFormulas F = []
atomicFormulas phi@(Rel _ ts) = [phi]
atomicFormulas (Not phi) = atomicFormulas phi
atomicFormulas (And phi psi) = nub $ atomicFormulas phi ++ atomicFormulas psi
atomicFormulas (Or phi psi) = nub $ atomicFormulas phi ++ atomicFormulas psi
atomicFormulas (Implies phi psi) = nub $ atomicFormulas phi ++ atomicFormulas psi
atomicFormulas (Iff phi psi) = nub $ atomicFormulas phi ++ atomicFormulas psi
atomicFormulas (Exists x phi) = atomicFormulas phi
atomicFormulas (Forall x phi) = atomicFormulas phi
0.3s

SAT solver for ground formulas

The following is a naive SAT solver for ground formulas that just enumerates all possible interpretations for the atomic formulas. Any more sophisticated SAT solver would give great performance improvements.

sat :: Formula -> Bool
sat phi = or [ev int phi | int <- functions atoms [True, False]]
  where atoms = atomicFormulas phi
        
        ev :: (Formula -> Bool) -> Formula -> Bool
        ev int T = True
        ev int F = False
        ev int atom@(Rel _ _) = int atom
        ev int (Not φ) = not (ev int φ)
        ev int (Or φ ψ) = ev int φ || ev int ψ
        ev int (And φ ψ) = ev int φ && ev int ψ
        ev _ φ = error $ "unexpected formula: " ++ show φ
0.3s

Decision procedure (Exercise)

Consider the following steps: In order to decide whether the formula inline_formula not implemented is a tautology:

  1. Close the formula by quantifying universally all the free variables, thus obtaining a sentence, still in the inline_formula not implemented -fragment.

  2. Negate inline_formula not implemented (which thus becomes a formula of the inline_formula not implemented fragment),

  3. Skolemise (thus obtaining a universal formula).

  4. Remove the prefix of universal quantifiers.

  5. Generate all groundInstances.

  6. Check whether the conjunction of all ground instances is unsatisfiable. This is the answer to the original problem.

aedecide :: Formula -> Bool
aedecide φ = todo
0.3s

Examples

forallImpliesExists = Forall "x" (Rel "r" [Var "x"]) ==> Exists "x" (Rel "r" [Var "x"])
aedecide forallImpliesExists
0.4s

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")
aedecide lem
0.5s
flip = Exists "x" (Forall "y" $ t "x" "y") ==> Forall "y" (Exists "x" $ t "x" "y")
aedecide flip
0.4s

Runtime setup (IGNORE ME)

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