A quick and dirty unification algorithm

Posted on June 30, 2011 by phimuemue

The following is a very simple unification algorithm in Haskell.

-- simple unification for predicate logic
data AtomicFormula = Variable String |  -- single variable 
                     Function String [AtomicFormula] -- function with some args
instance Show AtomicFormula where       
         show (Variable a) = a
         show (Function f l) = f ++ (show l)
data Formula = And Formula Formula -- conjunction, not needed
               | Or Formula Formula -- disjunction, not needed
               | Neg Formula -- negation
               | Predicate String [AtomicFormula] -- predicate with name and arguments
               deriving (Show)
data UnificationResult = Success [(String, AtomicFormula)] | Error [(AtomicFormula, AtomicFormula)]
instance Show UnificationResult where
         show (Error l) = show l
         show (Success []) = ""
         show (Success ((x1, x2):xs)) = "[" ++ (x1) ++ "/" ++ (show x2) ++ "] " ++ (show (Success xs))
unify (Predicate p1 args1) (Predicate p2 args2) = 
      if p1 == p2 then unifyArgumentLists args1 args2
      else Error []  
-- eliminate variable from formula
substituteVariable v expr [] = []
substituteVariable (Variable v) expr ((Variable y):xs) = if v==y then expr:(substituteVariable (Variable v) expr xs)
                                                         else (Variable y):(substituteVariable (Variable v) expr xs)
substituteVariable v expr ((Function f a):xs) = (Function f (substituteVariable v expr a)) : (substituteVariable v expr xs)
-- occurs-check
occurs _ [] = False
occurs (Variable x) ((Variable y):ys) = if x==y then True else occurs (Variable x) ys
occurs (Variable x) ((Function f l):ys) = (occurs (Variable x) l) || (occurs (Variable x) ys)
-- unify argument lists - central part
unifyArgumentLists [] [] = Success []
unifyArgumentLists ((Variable v):xs) ((Variable y):ys) = 
                   let Success l = unifyArgumentLists (substituteVariable (Variable v) (Variable y) xs) (substituteVariable (Variable v) (Variable y) ys) 
                   in Success ((v, Variable y):l) 
unifyArgumentLists ((Function f v):xs) ((Function g y):ys) = 
                   if f == g then
                      let Success l = unifyArgumentLists v y in
                          let Success k = unifyArgumentLists xs ys in
                      Success (l++k)
                   else Error [(Function f [], Function g [])]
unifyArgumentLists ((Variable v):xs) (y:ys) = let Success rem = if occurs (Variable v) [y] then Error []
                                                                else unifyArgumentLists xs ys in Success ((v, y):rem)
unifyArgumentLists (y:ys) ((Variable v):xs) = unifyArgumentLists ((Variable v):xs) (y:ys)
unifyArgumentLists _ _ = Error []