HELP FOR: The unify-library (overview)
   
- Unify is a library of types and procedures to compute:
  - relations between substitutions,
  - operations on substitutions,
  - algebraic properties of substitutions,
  - unifiers over the empty theory (Robinson Unification).
   
- The library consists of the following types:
  - substitution:  standard substitution,
  - isubstitution: idempotent substitution,
  - psubstitution: permutation of variables,
  - msubstitution: most general unifier (mgu) of some equation (set).
   
- The library consists of the following procedures:
  - subst: apply a substitution to an expression
  - compose: composition of substitutions
  - inverse: inverse of a permutation of variables
  - idempotent: compute an equivalent and idempotent substitution
  - equivalent: compare substitutions
  - generalization: compare substitutions
  - minimal: minimal base of idempotent solutions
  - inversion: transform between equivalent substitutions
  - Eunify: most general unifier (mgu)
  - rank: rank of a solvable equation (set)
  - redundant: maximal subset of redundant equations
   
- For each type and each procedure a help text is available under the same
  name, e.g. to get the help text for the procedure rank, type ?rank .
   
- The procedures Cunify and rewrite are two examples for the usage of the
  unify-library. See ?Cunify and ?rewrite for details.
   
- References:
  - J-L. Lassez, M.J. Maher, and K. Marriott, "Unification Revisited",
    in "Foundations of Deductive Databases and Logic Programming", ed.
    J. Minker, 1987.
  - F. Baader and J.H. Siekmann, "Unification Theory", in "Handbook of Logic
    in Artificial Intelligence and Logic Programming", ed. D. Gabbay,
    C. Hogger, J. Robinson, 1993- .
   
- Essentially, the unify-library is an implementation of the constructive
  proofs given in Lasser, Maher, and Marriott, "Unification Revisited",
  up to page 606.
   
- The unify-library is the result of a lecture on unification theory held
  at the University of Bern. 
  Contributions by: Franz Achermann, Roland Balmer, Peter Balsiger,
  Peppo Brambilla, Patrick Frey, Juerg Gertsch, Roland Loser, and
  Heinrich Zimmermann.
  Suggestions to Tyko Strassen: strassen@iam.unibe.ch .
   
   
EXAMPLES:   
   
> with( unify ):
   
> sigma := {x=f(a),y=x,z=h(z)};
   
                         sigma := {x = f(a), y = x, z = h(z)}
   
   
# Test, if sigma is a proper substitution:
   
> type( sigma , substitution );
   
                         true
   
   
# Is sigma even an idempotent substitution ?
   
> type( sigma , isubstitution );
   
                         false
   
   
# Indeed:
   
> delta := compose( sigma , sigma );
   
                         delta := {x = f(a), y = f(a), z = h(h(z))}
   
   
> evalb( sigma = delta );
   
                         false
   
   
# But sigma and delta are still equivalent:
   
> equivalent( sigma , delta );
   
                         true
   
   
# This is because sigma and delta are not solvable:
   
> type( sigma , msubstitution ); type( delta , msubstitution );
   
                         false
                         false
   
   
# Unification may be regarded as solving equations in free term algebra.
# These are in a certain sense the simplest type of equations in Computer
# Algebra:
   
> f, a, b;
   
                         f, a, b
   
   
> solve( f(x,y)=f(a,b) , {x,y} );
   
                         {y = y, x = RootOf(f(_Z,y)-f(a,b))}
   
   
> Eunify( f(x,y)=f(a,b) , {x,y} );
   
                         {x = a, y = b}
   
   
# Another example of unification:
   
> s := f(y,a); t := f(g(x),x);
   
                         s := f(y,a)
                         t := f(g(x),x)
   
   
> mu := Eunify( s=t , {x,y} );
   
                         mu := {x = a, y = g(a)}
   
   
# Apply mu to both s and t to check that mu is a unifier:
   
> subst(mu,s) = subst(mu,t);
   
                         f(g(a),a) = f(g(a),a)
   
   
# We add another binding to mu:
   
> theta := mu union { z=h(y) };
   
                         theta := {x = a, y = g(a), z = h(y)}
   
   
# mu is now more general than theta:
   
> generalization( mu , theta );
   
                         true
   
   
# theta can be converted in an equivalent but idempotent substitution:
   
> theta := idempotent( theta );
   
                         theta := {x = a, y = g(a), z = h(g(a))}
   
   
# In theta, all bindings are relevant:
   
> rank( theta , {x,y,z} );
   
                         3
   
   
# We add another binding to theta:
   
> sigma := theta union { y=g(x) };
   
                         sigma := {x = a, y = g(a), z = h(g(a)), y = g(x)}
   
   
# The rank of this substitution remains unchanged:
   
> rank( sigma , {x,y,z} );
   
                         3
   
   
# So sigma contains redundant equations.
# These equations can be removed:
   
> equations := sigma minus redundant( sigma , {x,y,z} );
   
                         {y = g(x), y = g(a), z = h(g(a))}
   
   
> sigma := Eunify( equations , {x,y,z} );
   
                         {x = a, y = g(a), z = h(g(a))}
   
   
# Let mu and phi be equivalent and most general unifiers:
   
> mu  := { x=g(y) , z=y }:
> phi := { x=g(z) , y=z }:
   
# With the help of the procedure inversion we can compute the permutation
# of variables alpha, that maps phi onto mu:
   
> alpha := inversion(mu,phi);
   
                        alpha := {z = y, y = z}
   
   
> mu = compose( phi , alpha );
   
                        {x = g(y) ,z = y} = {x = g(y) ,z = y}
   
   
# The inverse of alpha then maps mu onto phi:
   
> phi = compose( mu , inverse(alpha) );
   
                        {x = g(z) ,y = z} = {x = g(z) ,y = z}