home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / gofer230.zip / Progs / Gofer / Demos / Prolog / Subst < prev   
Text File  |  1994-06-23  |  2KB  |  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.28
  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. -- app 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.  app is a monoid homomorphism from (Subst,nullSubst,(**))
  24. --           to (Term -> Term, id, (.)) in the sense that:
  25. --                  app (s1 ** s2) = app s1 . app s2
  26. --                 s ** nullSubst = s = nullSubst ** s
  27.  
  28. app                     :: Subst -> Term -> Term
  29. app s (Var i)            = s i
  30. app s (Struct a ts)      = Struct a (map (app 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                 = app 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 (app u1) ts)
  60.                                                      (map (app u1) rs) ]
  61.  
  62. --- End of Subst.hs
  63.