1 -- 2 -- Substitutions and Unification of Prolog Terms 3 -- Mark P. Jones November 1990 4 -- 5 -- uses Haskell B. version 0.99.3 6 -- 7 module Subst(Subst, nullSubst, (->>), (@@), apply, unify) where 8 9 import PrologData 10 11 infixr 3 @@ 12 infix 4 ->> 13 14 --- Substitutions: 15 16 type Subst = Id -> Term 17 18 -- substitutions are represented by functions mapping identifiers to terms. 19 -- 20 -- apply s extends the substitution s to a function mapping terms to terms 21 -- nullSubst is the empty substitution which maps every identifier to the 22 -- same identifier (as a term). 23 -- i ->> t is the substitution which maps the identifier i to the term t, 24 -- but otherwise behaves like nullSubst. 25 -- s1 @@ s2 is the composition of substitutions s1 and s2 26 -- N.B. apply is a monoid homomorphism from (Subst,nullSubst,(@@)) 27 -- to (Term -> Term, id, (.)) in the sense that: 28 -- apply (s1 @@ s2) = apply s1 . apply s2 29 -- s @@ nullSubst = s = nullSubst @@ s 30 31 apply :: Subst -> Term -> Term 32 apply s (Var i) = s i 33 apply s (Struct a ts) = Struct a (map (apply s) ts) 34 35 nullSubst :: Subst 36 nullSubst i = Var i 37 38 (->>) :: Id -> Term -> Subst 39 (->>) i t j | j==i = t 40 | otherwise = Var j 41 42 (@@) :: Subst -> Subst -> Subst 43 s1 @@ s2 = apply s1 . s2 44 45 --- Unification: 46 47 -- unify t1 t2 returns a list containing a single substitution s which is 48 -- the most general unifier of terms t1 t2. If no unifier 49 -- exists, the list returned is empty. 50 51 unify :: Term -> Term -> [Subst] 52 unify (Var x) (Var y) = if x==y then [nullSubst] else [x->>Var y] 53 unify (Var x) t2 = [ x ->> t2 | not (x `elem` varsIn t2) ] 54 unify t1 (Var y) = [ y ->> t1 | not (y `elem` varsIn t1) ] 55 unify (Struct a ts) (Struct b ss) = [ u | a==b, u<-listUnify ts ss ] 56 57 listUnify :: [Term] -> [Term] -> [Subst] 58 listUnify [] [] = [nullSubst] 59 listUnify [] (r:rs) = [] 60 listUnify (t:ts) [] = [] 61 listUnify (t:ts) (r:rs) = [ u2 @@ u1 | u1<-unify t r, 62 u2<-listUnify (map (apply u1) ts) 63 (map (apply u1) rs) ] 64 65 --- End of Subst.hs