diff options
author | Yale AI Dept <ai@nebula.cs.yale.edu> | 1993-07-14 13:08:00 -0500 |
---|---|---|
committer | Duncan McGreggor <duncan.mcgreggor@rackspace.com> | 1993-07-14 13:08:00 -0500 |
commit | 4e987026148fe65c323afbc93cd560c07bf06b3f (patch) | |
tree | 26ae54177389edcbe453d25a00c38c2774e8b7d4 /progs/demo/prolog/Subst.hs |
Import to github.
Diffstat (limited to 'progs/demo/prolog/Subst.hs')
-rw-r--r-- | progs/demo/prolog/Subst.hs | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/progs/demo/prolog/Subst.hs b/progs/demo/prolog/Subst.hs new file mode 100644 index 0000000..f96e462 --- /dev/null +++ b/progs/demo/prolog/Subst.hs @@ -0,0 +1,65 @@ +-- +-- Substitutions and Unification of Prolog Terms +-- Mark P. Jones November 1990 +-- +-- uses Haskell B. version 0.99.3 +-- +module Subst(Subst(..), nullSubst, (>!), (@@), apply, unify) where + +import PrologData + +infixr 3 @@ +infix 4 >! + +--- Substitutions: + +type Subst = Id -> Term + +-- substitutions are represented by functions mapping identifiers to terms. +-- +-- apply s extends the substitution s to a function mapping terms to terms +-- nullSubst is the empty substitution which maps every identifier to the +-- same identifier (as a term). +-- i >! t is the substitution which maps the identifier i to the term t, +-- but otherwise behaves like nullSubst. +-- s1 @@ s2 is the composition of substitutions s1 and s2 +-- N.B. apply is a monoid homomorphism from (Subst,nullSubst,(@@)) +-- to (Term -> Term, id, (.)) in the sense that: +-- apply (s1 @@ s2) = apply s1 . apply s2 +-- s @@ nullSubst = s = nullSubst @@ s + +apply :: Subst -> Term -> Term +apply s (Var i) = s i +apply s (Struct a ts) = Struct a (map (apply s) ts) + +nullSubst :: Subst +nullSubst i = Var i + +(>!) :: Id -> Term -> Subst +(>!) i t j | j==i = t + | otherwise = Var j + +(@@) :: Subst -> Subst -> Subst +s1 @@ s2 = apply s1 . s2 + +--- Unification: + +-- unify t1 t2 returns a list containing a single substitution s which is +-- the most general unifier of terms t1 t2. If no unifier +-- exists, the list returned is empty. + +unify :: Term -> Term -> [Subst] +unify (Var x) (Var y) = if x==y then [nullSubst] else [x>!Var y] +unify (Var x) t2 = [ x >! t2 | not (x `elem` varsIn t2) ] +unify t1 (Var y) = [ y >! t1 | not (y `elem` varsIn t1) ] +unify (Struct a ts) (Struct b ss) = [ u | a==b, u<-listUnify ts ss ] + +listUnify :: [Term] -> [Term] -> [Subst] +listUnify [] [] = [nullSubst] +listUnify [] (r:rs) = [] +listUnify (t:ts) [] = [] +listUnify (t:ts) (r:rs) = [ u2 @@ u1 | u1<-unify t r, + u2<-listUnify (map (apply u1) ts) + (map (apply u1) rs) ] + +--- End of Subst.hs |