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