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