$Id: Subst.lhs,v 1.3 1998/03/02 21:00:47 leavens Exp $

Generalized Substitutions and Unification

AUTHOR: Mark P. Jones as generalized by Gary T. Leavens
        (The original is in the Prolog demo for Hugs)

> module Subst where

> import List (nub)

> infixr 3 @@
> infix  4 ->-

           SUBSTITUTIONS

A substitution is a function from logical variables to terms.

> type Subst term = LogicalVar -> term
> type LogicalVar = (Int,String)

Terms are defined by the user of this module.
Thus we give a class definition with the appropriate methods
needed to create and apply substititions to terms.

> class Substitutable term where
>   nullSubst :: Subst term
>   (->-)     :: LogicalVar -> term -> Subst term
>   app       :: Subst term -> term -> term

    nullSubst is the empty substitution;
              it is like the identity function in that, for all lv,
	              nullSubst lv = toTerm lv,
              where toTerm is a function that takes a logical variable
                    and makes a term out of it. Typically toTerm will be some
                    constructor in the grammar for terms.
    (lv ->- t) is the substitution that maps the LogicalVar lv to the term t,
              but otherwise behaves like nullSubst.
    app s     extends the substitution s to a function mapping terms to terms

    We require that the following equations hold:
      app nullSubst t = t
      app (lv ->- t) (nullSubst lv') = if lv' == lv then t else (nullSubst lv')


Using these operations one can define composition of substitutions
as follows.

> (@@) :: Substitutable term => Subst term -> Subst term -> Subst term
> s1 @@ s2                 = app s1 . s2 

Composition of substitutions should be is a monoid homomorphism
   from (Subst,        nullSubst,  (@@))
   to   (Term -> Term, (\t -> t),  (.))
in the sense that the following equations hold.
      app (s1 @@ s2) = app s1 . app s2
      s @@ nullSubst = s
      nullSubst @@ s = s


          UNIFICATION

To be unifiable, terms must have additional capabilities.
These are captured in the following class definition.

> class Substitutable term => Unifiable term where
>   toTerm :: LogicalVar -> term
>   getVar :: term -> Maybe LogicalVar
>   subterms :: term -> [term]
>   same_kind :: term -> term -> Bool

    toTerm lv is the logical variable lv made into a term
    getVar t  is (Just lv) when t is a term representing a logical variable lv,
                 and Nothing when t does not represent a logical variable
    subterms  is a list of the subterms of a term
    same_kind t1 t2  is True when t1 and t2 are the same kind of term,
                       that is they have the same operator
   
   We require that the following equations hold:
      getVar(toTerm lv) = (Just lv)
      subterms(toTerm lv) = []
      (getVar t1 == Nothing) = (getVar t2 == Nothing), if same_kind t1 t2
      

The function mgu finds the most general unifier of two terms, if it exists
It returns its result in a list; if no unifier exists, then [] is returned.

> mgu :: Unifiable term => term -> term -> [Subst term]
> mgu t1 t2 =
>   case (getVar t1, getVar t2) of
>      (Just x, Just y) -> if x==y then [nullSubst] else [x ->- toTerm y]
>      (Just x, Nothing) -> [ x ->- t2 | x `notElem` varsIn t2 ]
>      (Nothing, Just y) -> [ y ->- t1 | y `notElem` varsIn t1 ]
>      (Nothing, Nothing) -> [ u | same_kind t1 t2,
>                                  u<-listUnify (subterms t1) (subterms t2) ]

> varsIn :: Unifiable term => term -> [LogicalVar]
> varsIn t =
>   case getVar t of
>      (Just lv) -> [lv]
>      Nothing -> (nub . concat . map varsIn) (subterms t)


> listUnify :: Unifiable term => [term] -> [term] -> [Subst term]
> listUnify []     []     = [nullSubst]
> listUnify []     (r:rs) = []
> listUnify (t:ts) []     = []
> listUnify (t:ts) (r:rs) = [ u2 @@ u1 | u1 <- mgu t r,
>                                        u2 <- listUnify (map (app u1) ts)
>                                                        (map (app u1) rs) ]

Before trying to find the most general unifier of two terms,
one should make sure that they have no variables in common.
This can be accomplished by using the following function twice,
once for each term, but using two different integers.

> renameVars :: Unifiable term => Int -> term -> term
> renameVars lev t = app (\(n,s) -> toTerm (lev,s)) t