home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / MacHaskell 2.2 / progs / demo / prolog / Subst.hs < prev    next >
Encoding:
Text File  |  1994-09-27  |  2.2 KB  |  66 lines  |  [TEXT/YHS2]
  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
  66.