skolemization stuff

skolemizer.hs

type Variable = String 

data Term = Variable Variable |
            Function String [Term] deriving Eq

instance Show Term where
  show (Variable v) = v
  show (Function f []) = f
  show (Function f l) = f ++ (show l)
  
data Formula = FormulaContainer Formula |
               Predicate String [Term] |
               Neg Formula |
               Or Formula Formula |
               And Formula Formula |
               Exists Variable Formula |
               Forall Variable Formula |
               Implication Formula Formula deriving Eq

instance Show Formula where
  show (Predicate s l) = s ++ (show l)
  show (Neg f) = "-" ++ (show f)
  show (Or f g) = (show f) ++ " v " ++ (show g)
  show (And f g) = (show f) ++ " ^ " ++ (show g)
  show (Exists v f) = "E " ++ (v) ++ ". " ++ (show f)
  show (Forall v f) = "A " ++ (v) ++ ". " ++ (show f)
  show (Implication f g) = (show f) ++ " -> " ++ (show g)

-- my test case
ex7_3_1_1 = Forall "y" (Predicate "Q" [Function "f" [Variable "a"], Function "f" [Variable "y"]])
ex7_3_1_2 = Forall "x" (
  Forall "y" (
     Implication 
     (Predicate "Q" [Variable "y", Function "f" [Variable "y"]])
     (Predicate "P" [Function "f" [Variable "x"], Function "g" [Variable "y", Variable "b"]])
     )
  )
ex7_3_1 = And ex7_3_1_1 ex7_3_1_2
ex7_3_2 = Exists "x" (
  Exists "y" (
     Exists "z" (
        And 
        (And 
         (Predicate "P" [Variable "x", Variable "y"])
         (Predicate "P" [Function "f" [Variable "a"], Function "g" [Variable "x", Variable "b"]])
         )
        (Predicate "Q" [Variable "x", Variable "z"])
        )
     )
  )
ex7_3 = Implication ex7_3_1 ex7_3_2

-- removes all implications
removeImplications :: Formula -> Formula
removeImplications (Implication a b) = (Or (Neg a) (b))
removeImplications (Neg f) = Neg (removeImplications f)
removeImplications (Or f g) = Or (removeImplications f) (removeImplications g)
removeImplications (And f g) = And (removeImplications f) (removeImplications g)
removeImplications (Exists v f) = Exists v (removeImplications f)
removeImplications (Forall v f) = Forall v (removeImplications f)
removeImplications a = a -- all other cases

-- moves negation to the right as much as possible
adjustNegations :: Formula -> Formula
adjustNegations (Neg (Neg f)) = adjustNegations f
adjustNegations (Neg (Or f g)) = And ((adjustNegations (Neg f))) ((adjustNegations (Neg g)))
adjustNegations (Neg (And f g)) = Or ((adjustNegations (Neg f))) ((adjustNegations (Neg g)))
adjustNegations (Neg (Exists v f)) = Forall v (adjustNegations (Neg f))
adjustNegations (Neg (Forall v f)) = Exists v (adjustNegations (Neg f))
adjustNegations (Neg h@(Implication f g)) = adjustNegations (Neg (removeImplications h))

adjustNegations (Or f g) = Or (adjustNegations f) (adjustNegations g)
adjustNegations (And f g) = And (adjustNegations f) (adjustNegations g)
adjustNegations (Exists v f) = Exists v (adjustNegations f)
adjustNegations (Forall v f) = Forall v (adjustNegations f)
adjustNegations (h@(Implication f g)) = adjustNegations (removeImplications h)
adjustNegations f = f

-- replace a (variable x) by another term y in a list of terms
replaceVarL :: [Char] -> Term -> [Term] -> [Term]
replaceVarL _ _ [] = []
replaceVarL x y ((Variable v):vs) = (if x==v then y else (Variable v)):(replaceVarL x y vs)
replaceVarL x y ((Function f l):vs) = (Function f (replaceVarL x y l)):(replaceVarL x y vs)
                                                 
-- replace a variable x by another variable y in a formula, c is the "variable counter"
replaceVar :: Num a => [Char] -> Term -> Formula -> a -> Formula
replaceVar x y (Predicate s l) c = Predicate s (replaceVarL x y l)
replaceVar x y (Neg f) c = Neg (replaceVar x y f c)
replaceVar x y (Or f g) c = Or (replaceVar x y f c) (replaceVar x y g c)
replaceVar x y (And f g) c = And (replaceVar x y f c) (replaceVar x y g c)
replaceVar x y (Exists v f) c = if x==v 
                                then let newVar = 'x':(show c) in replaceVar x y (Exists newVar (replaceVar v (Variable newVar) f (c+1))) (c+1)
                                else Exists v (replaceVar x y f c)
replaceVar x y (Forall v f) c = if x==v 
                                then let newVar = 'x':(show c) in replaceVar x y (Forall newVar (replaceVar v (Variable newVar) f (c+1))) (c+1)
                                else Forall v (replaceVar x y f c)
replaceVar x y h@(Implication f g) c = replaceVar x y (removeImplications h) c

-- create unique variable names, kv holds all used variables, c is variable counter
-- not sure if it is correct, but at least for my example, it works
uniquifyVariables f = _uniquifyVars f 0
_uniquifyVars (Predicate p l) c = Predicate p l
_uniquifyVars (Neg f) c = Neg (_uniquifyVars f (c+1))
_uniquifyVars (Or f g) c = Or (_uniquifyVars f (c)) (_uniquifyVars g (1+c+countQVars f))
_uniquifyVars (And f g) c = And (_uniquifyVars f (c)) (_uniquifyVars g (1+c+countQVars f))
_uniquifyVars (Exists v f) c = let newVar = 'x':(show c) in Exists newVar (replaceVar v (Variable newVar) (_uniquifyVars f (c+1)) (c + 1 +countQVars f))
_uniquifyVars (Forall v f) c = let newVar = 'x':(show c) in Forall newVar (replaceVar v (Variable newVar) (_uniquifyVars f (c+1)) (c + 1 + countQVars f))
_uniquifyVars (Implication f g) c = Implication (_uniquifyVars f (countQVars f)) (_uniquifyVars g (c + countQVars g))

-- count quantified variables
countQVars (Predicate p l) = 0
countQVars (Neg f) = countQVars f
countQVars (Or f g) = (countQVars f) + (countQVars g)
countQVars (And f g) = (countQVars f) + (countQVars g)
countQVars (Exists v f) = 1 + countQVars f
countQVars (Forall v f) = 1 + countQVars f
countQVars (Implication f g) = (countQVars f) + (countQVars g)

-- returns the same formula without quantifiers
removeQuantifiers :: Formula -> Formula
removeQuantifiers (Exists v f) = removeQuantifiers f
removeQuantifiers (Forall v f) = removeQuantifiers f
removeQuantifiers (Neg f) = Neg (removeQuantifiers f)
removeQuantifiers (Or f g) = Or (removeQuantifiers f) (removeQuantifiers g)
removeQuantifiers (And f g) = And (removeQuantifiers f) (removeQuantifiers g)
removeQuantifiers (Implication f g) = Implication (removeQuantifiers f) (removeQuantifiers g)
removeQuantifiers (Predicate p l) = Predicate p l

-- collect all the quantifiers
collectQuantifiers (Exists v f) = (Exists v f) : (collectQuantifiers f)
collectQuantifiers (Forall v f) = (Forall v f) : (collectQuantifiers f)
collectQuantifiers (Neg f) = collectQuantifiers f
collectQuantifiers (Or f g) = (collectQuantifiers f) ++ (collectQuantifiers g)
collectQuantifiers (And f g) = (collectQuantifiers f) ++ (collectQuantifiers g)
collectQuantifiers (Implication f g) = (collectQuantifiers f) ++ (collectQuantifiers g)
collectQuantifiers (Predicate p l) = []

-- move qualifiers to front
quantifiersToFront f [] = f
quantifiersToFront f ((Exists v _):qs) = Exists v (quantifiersToFront f qs)
quantifiersToFront f ((Forall v _):qs) = Forall v (quantifiersToFront f qs)

-- replace exist-quantors by functions
removeExists (Exists v f) cv = replaceVar v (Function ("f_" ++ v) cv ) (removeExists f cv) 0
removeExists (Forall v f) cv = Forall v (removeExists f (cv++[(Variable v)]))
removeExists (Neg f) cv = Neg (removeExists f cv)
removeExists (Or f g) cv = Or (removeExists f cv) (removeExists g cv)
removeExists (And f g) cv = And (removeExists f cv) (removeExists g cv)
removeExists (Implication f g) cv = Implication (removeExists f cv) (removeExists g cv)
removeExists (Predicate p l) cv = Predicate p l

-- skolemize everything with one function call
skolemize f = let rf = uniquifyVariables (adjustNegations (removeImplications f)) in
  removeExists (quantifiersToFront (removeQuantifiers rf) (collectQuantifiers rf)) []