Matching on steroids ....

--------------------------------------------------------

I am continuing to use literate Haskell ...

Prolog, our next language, uses more powerful version of matching called
"unification" which is matching on steroids ...

Recall that the idea of MATCHING is that we are given an expression/term
(with variables), s, and a "template" (or a "pattern"), t, which is another
expression/term with variables which do not repeat.   The expression/term,
s, is said to match the template/pattern t in case there is a substitution
[t_1/x_1,...,t_n/x_n] of t such that

                      s == t[t_1/x_1,...,t_n/x_n]

The idea of UNIFICATION is completely symmetric:  we are given two abitrary
terms s_1 and s_2 (with no restriction on the variables) and the objective is
to find a substitution which makes them equal.  This means a substitution
                      [t_1/x_1,...,t_n/x_n]
such that
                      s_1[t_1/x_1,...,t_n/x_n] = s_2[t_1/x_1,...,t_n/x_n].

Such a substitution is called a UNIFIER (as applying it make the terms
syntactically exactly equal).  However, there are many unifiers!  Fortunately,
upto naming of variables, there is a "MOST GENERAL UNIFIER". This is a
substitution which is
(a) a unifier but has the additional property that
(b) any other unifier can be obtained by substituting it.

Let us make that property (b) a bit more explicit:

Suppose we are unifying s1 and s2 and we are given a unifier
           [t_1/x_1,...,t_n/x_n]
so that as above

           t = s_1[t_1/x_1,...,t_n/x_n] = s_2[t_1/x_1,...,t_n/x_n].

A most general unifier [u_1/x_1,...,un/x_n] is a unifier, so

            t' = s_1[u_1/x_1,...,un/x_n] =s_2[u_1/x_1,...,un/x_n]

but furthermore there is a substitution of t' which obtains t, that is
there is a [v_1/y_1,...,v_m/y_m] so that

                           t = t'[v_1/y_1,...,v_m/y_m]

OK a bit of a mouthful! HOWEVER, to understand Prolog you really need to
understand unification!! Of course, just as for matching, unification can
fail: that is given two terms s_1 and s_2 it is quite possible that there
is no unifier.

There is a huge amount of fundamental Computer Science work on unification
(try googling "unification" (computer science)): the main algorithms for
unification (Alberto Martelli and Ugo Montanari) were only developed as
recently as 1982 although the ideas go farther back.

OK so we have to write a unification algorithm.  Lets start with the
datatype of expressions:

> data Exp f v  = Opn f [Exp f v]
>               | Var v
>    deriving (Show,Eq)

Of course we need the fold for expressions:

> foldExp:: (f -> [c] -> c) -> (v -> c) -> (Exp f v) -> c
> foldExp opn var (Var v) = var v
> foldExp opn var (Opn f args) = opn f (map (foldExp opn var) args)

A substitution for expressions with  function type f and variable type v
looks like:

> type Sub f v = (v,Exp f v)
> type Subs f v = [(v,Exp f v)]

Lets start with a warm up and program a single substitution:

> substitution:: Eq v => (Sub f v) -> (Exp f v) -> (Exp f v)
> substitution (v,s) = foldExp Opn (\w -> if v==w then s else Var w)


Note all this involves is substituting the leaves holding a variable equal
to v with s otherwise leaving it alone.

So now lets program a whole substitution list ...
How do we do this: well we can use a fold over lists.

> substitutions:: Eq v => (Exp f v) -> (Subs f v) -> (Exp f v)
> substitutions t = foldr substitution t 


There is something to notice with this substitution as it isperforms the
substitutions sequentially in the sense that the first substitution
performed is the last in the list:
      t[s_1/x_1,...,s_n/x_n] = (...(...(t[s_n/x_n])...)[s_2/x_2])[s_1/x_1])
this means that substitutions earlier in the list can substitute
substitutions later in the list but not vice versa.  A substitution list is
"linearized" if, for j>i, the variable x_j does not occur in the term s_i.

When, for i =/= j the variable x_j does not occur in the term s_i then the
substitution is said to be "parallel" (and the order in which the
substitutions are performed does not matter).

Well that went pretty well (although there is a subtely over linearized
and parallel substitution lists to bear in mind) ... here is an expression
and a substitution list so you can try things out and check
that the code works!!! Invent your own test here ...

> e1 = Opn "add" [Opn "mult" [Var 1,Var 2],Var 1]
> e2 = Opn "mult" [Var 6,Var 7]
> e3 = Opn "add" [Var 1,Opn "mult" [Var 6,Var 7]]
> e4 = Opn "add" [Var 3,Opn "mult" [Var 4,Var 2]]
> e5 = Opn "add" [Var 9,Var 10]
> subs1 = [(1,e2),(2,e1)]

Now the unification algorithm starts with a "matching" step in which the
trees are matched against each other and whenever one tree ends in a
variable where the other tree continues one obtains a substitution.  The
substitution is only valid, however, if it passes what is called the
"occurs check" this checks that the substituted variable does NOT occur
in the term which is to replace it (without the occurs check one gets
an infinite tree!!).

We need the succeess or fail datatype and some basic utilities:

> data SF  a = SS a | FF
>  deriving (Show,Eq)
>
> sfmap::(a -> b) -> (SF a) -> (SF b)
> sfmap f (SS a) = SS (f a)
> sfmap f FF = FF
>
> sflist:: [SF a] -> (SF [a])
> sflist = foldr (\x xs -> case (x,xs) of
>                             ((SS a),(SS as)) -> SS(a:as)
>                             _ -> FF)
>                (SS [])
>
> sfflatten:: (SF (SF a)) -> SF a
> sfflatten (SS x) = x
> sfflatten FF = FF

Now let us program the occurs check.  Note that v occuring in the expression
the variable v itself, is OK: but no substitution is needed hence an empty
list is returned (this is why a substitution list is produced).

> occurs_check::(Eq f,Eq v) => (Sub f v) -> (SF (Subs f v))
> occurs_check (v,t)| t == (Var v) = SS []
>                   | occurs v t = FF
>                   | otherwise = SS [(v,t)]
>     where
>          occurs v = foldExp (\_ -> foldr (||) False) ((==) v)

Here now is the matching step:

> matching::(Eq f,Eq v) => (Exp f v,Exp f v) -> (SF (Subs f v))
> matching ((Var v),t) = occurs_check (v,t)
> matching (s,(Var v)) = occurs_check (v,s)
> matching ((Opn f1 args1),(Opn f2 args2))
>   | f1 == f2 && (length args1) == (length args2)
>               = sfmap concat $ sflist $ map matching $ zip args1 args2
>   | otherwise = FF

This produces a (non-linearized) substitution list: we need to go through
the substitution list to "tidy" it up into a linearized substitution.
Thus we want a list of substitutions

        [t_1/x_1,t_2/x_2,...,t_n/x_n]

such that for 1 =< i < j =< n the variable x_j does not occur in t_i.  We
can achieve this by substituting out (here "subout") the variable x_i by
t_i in each later substitution t_j/x_i.  However there are two basic things
that can go wrong.
(1) First x_i could equal x_j in which case we retain the first substitution
but replace the second by the substitutions obtained from matching
on the two right hand sides (as they must be made equal!).
(2) Second one can perform the substitution of x_i and the result can
fail the occurs check as x_j occurs in t_i ... in which case everything
must fail.

This gives:

> linearize:: (Eq v, Eq f) => (Subs f v) -> (SF (Subs f v))
> linearize subs = linearize_helper [] subs
>      where
>         linearize_helper:: (Eq v,Eq f) => (Subs f v) -> (Subs f v) -> (SF (Subs f v))
>         linearize_helper (lin_subs) [] = SS lin_subs
>         linearize_helper lin_subs (sub:subs) =
>           case subout sub subs of
>             SS nsubs -> linearize_helper (sub:lin_subs) nsubs  -- reify sub!
>             FF -> FF

The process of removing the variable of a substitution from the rest of the
substitution list is given by:

> subout:: (Eq f,Eq v)=>(Sub f v)->(Subs f v)->SF (Subs f v)
> subout s [] = SS []
> subout sub@(x,t1) ((y,t2):subs)
>            | x==y = case matching (t1,t2) of
>                         SS msubs -> case subout sub subs of
>                              SS subouts ->  SS (msubs++subouts)
>                              _ -> FF
>                         _ -> FF
>            | otherwise = case occurs_check (y,substitution sub t2) of
>                           FF -> FF
>                           SS subst -> case (subout sub subs) of
>                                   SS subouts -> SS (subst++subouts)
>                                   _ -> FF

Please note the ugly nested case statements!!
... we shall show how this code can be improved using the exception monad
shortly.

Once one has a linearized substitution list one can parallelize it by
substituting all the substitutions later in the list by the substitutions
earlier in the list:

> parallelize:: Eq v => (Subs f v) -> (Subs f v)
> parallelize = foldr subsubstitutes [] where
>   subsubstitutes:: Eq v => (Sub f v) -> (Subs f v) -> (Subs f v)
>   subsubstitutes sub subs = sub:(map (\(x,s) -> (x,substitution sub s)) subs) 

Then we have a unify which gives a linearized substitution:

> unify t1 t2 = sfflatten $ sfmap linearize $ matching (t1,t2)

Or a unify which gives a parallelized substitution:

> punify t1 t2 = sfmap parallelize $ unify t1 t2
                    
Test the code try "unify ei ej" ... make up your own tests!