# 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 []