# 
# File: unify
# 
# Installation (Unix level):  $ maple < unify
# 
# Usage (Maple level):  > libname := libname , `/home/(userdir)/(unifydir)`;
#                       > with(unify);
#                       > ?unify
# 


# Due to the help text still necessary:
readlib(unassign):


#
# Short names for the user
# ------------------------
#
# help texts:
#
unify[`help/text/unify`]          := `help/unify/text/unify`:
unify[`help/text/substitution`]   := `help/unify/text/substitution`:
unify[`help/text/isubstitution`]  := `help/unify/text/substitution`:
unify[`help/text/psubstitution`]  := `help/unify/text/substitution`:
unify[`help/text/msubstitution`]  := `help/unify/text/substitution`:
unify[`help/text/subst`]          := `help/unify/text/subst`:
unify[`help/text/compose`]        := `help/unify/text/compose`:
unify[`help/text/inverse`]        := `help/unify/text/inverse`:
unify[`help/text/idempotent`]     := `help/unify/text/idempotent`:
unify[`help/text/generalization`] := `help/unify/text/equivalent`:
unify[`help/text/equivalent`]     := `help/unify/text/equivalent`:
unify[`help/text/minimal`]        := `help/unify/text/minimal`:
unify[`help/text/inversion`]      := `help/unify/text/inversion`:
unify[`help/text/Eunify`]         := `help/unify/text/Eunify`:
unify[`help/text/rank`]           := `help/unify/text/rank`:
unify[`help/text/redundant`]      := `help/unify/text/redundant`:
unify[`help/text/rewrite`]        := `help/unify/text/rewrite`:
unify[`help/text/Cunify`]         := `help/unify/text/Cunify`:
#
# procedures:
#
unify[subst]          := `unify/subst`:
unify[compose]        := `unify/compose`:
unify[inverse]        := `unify/inverse`:
unify[idempotent]     := `unify/idempotent`:
unify[generalization] := `unify/generalization`:
unify[equivalent]     := `unify/equivalent`:
unify[minimal]        := `unify/minimal`:
unify[inversion]      := `unify/inversion`:
unify[Eunify]         := `unify/Eunify`:
unify[rank]           := `unify/rank`:
unify[redundant]      := `unify/redundant`:
#
# types:
#
unify[substitution]  := `unify/substitution`:
unify[isubstitution] := `unify/isubstitution`:
unify[psubstitution] := `unify/psubstitution`:
unify[msubstitution] := `unify/msubstitution`:


`unify/init` := proc()
   # protect the type names:
   protect( 'substitution', 'isubstitution', 'psubstitution', 'msubstitution' )
end:


`help/unify/text/unify` := TEXT(
`   `,
`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}`,
`   `,
`   `
):


# Reference for the procedure type/substitution:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 591

`type/unify/substitution` := proc(s)
   local S,b,e,elim;
   # Test for proper Maple type:
   if type(s,name=algebraic) then S := {s}
      elif type(s,set(name=algebraic)) then S := s
      else RETURN(false) 
   fi;
   # A substitution must not contain an equation x=x and must
   # not have common variables on the lhs of the equations:
   elim := [];
   for b in S do 
       e := lhs(b);
       if e=rhs(b) or member(e,elim) then RETURN(false)
                                     else elim := [op(elim),e]
       fi
   od;
   true
end:


# Reference for the procedure type/isubstitution:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 601, Proposition 7

`type/unify/isubstitution` := proc(s)
   local S;
   if not type(s,`unify/substitution`) then RETURN(false) fi;
   if type(s,set) then S := s else S := {s} fi;
   # Check that no variable on the lhs of an equation
   # occurs on the rhs of some equation:
   evalb( map(lhs,S) intersect indets(map(rhs,S),name) = {} )
end:


# Reference for the procedure type/psubstitution:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 605, Proposition 13

`type/unify/psubstitution` := proc(s)
   if not type(s,`unify/substitution`) then RETURN(false) fi;
   # a single equation cannot be a permutation:
   if not type(s,set(name=name)) then RETURN(false) fi;
   # test if domain(s) = range(s):
   evalb( map(lhs,s) = map(rhs,s) )
end:


# Reference for the procedure type/msubstitution:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 606, Proposition 15

`type/unify/msubstitution` := proc(s)
   local S, rightterms, rightnames, v;
   if not type(s,`unify/substitution`) then RETURN(false) fi;
   if type(s,set) then S := s else S := {s} fi;
   rightterms := map(rhs,S);
   rightnames := select(type,rightterms,name);
   # if a variable v occurs on the lhs of an equation and on the rhs of an
   # equation, then there must exist an equation x=v for some variable x:
   for v in map(lhs,S) intersect indets(rightterms,name) do
      if not member(v,rightnames) then RETURN(false) fi
   od;
   true
end:


`help/unify/text/substitution` := TEXT(
`   `,
`HELP FOR: The types substitution, isubstitution,`,
`                    psubstitution and msubstitution`,
`   `,
`SYNOPSIS:  `, 
`- A substitution is a set of equations x_i=t_i where each x_i is a variable`,
`  (Maple type name), each t_i is a term (Maple type algebraic), t_i is not`,
`  identical to the variable x_i, and each variable occurs only once at the`,
`  lhs of an equation. A single equation is called binding.`,
`   `,
`- If the substitution consists only of one equation, then the parantheses {..}`,
`  may be omitted.`,
`   `,
`- An isubstitution is an idempotent substitution, i.e. delta is idempotent iff`,
`  compose(delta,delta)=delta.`,
`   `,
`- A psubstitution is a (substitution which is a) permutation of variables,`,
`  e.g. { x=y, y=z, z=x, u=v, v=u } and { } are of type psubstitution.`,
`  A permutation of variables is called invertible substitution, too.`,
`   `,
`- An msubstitution is a (substitution which is a) most general unifier of some`,
`  equation (set). An equivalent (but syntactic) definition is that sigma is`,
`  of type msubstitution iff: If a variable v occurs in the lhs of some binding`,
`  in sigma and in the rhs of some binding in sigma, then there exists a binding`,
`  x=v in sigma for some variable x.`,
`   `,
`- Each isubstitution and each psubstitution is an msubstitution, too.`,
`   `,
`- Note that the domain of a substitution sigma can be computed by`,
`  map(lhs,sigma) . `,
`   `,
`EXAMPLES:   `,
`> type( x=f(a) , substitution );`,
`   `,
`                                  true`,
`   `,
`   `,
`> type( x=x , substitution );`,
`   `,
`                                  false`,
`   `,
`   `,
`> type( {x=f(a),x=z} , substitution );`,
`   `,
`                                  false`,
`   `,
`   `,
`> type( {x=f(a),y=x,z=h(z)} , substitution );`,
`   `,
`                                  true`,
`   `,
`   `,
`> type( {x=f(a),y=x,z=h(z)} , isubstitution );`,
`   `,
`                                  false`,
`   `,
`   `,
`> type( {x=f(y),y=x} , psubstitution );`,
`   `,
`                                  false`,
`   `,
`   `,
`> type( {x=a,y=x,z=x} , msubstitution );`,
`   `,
`                                  true`,
`   `,
`   `,
`> type( x=f(x) , msubstitution );`,
`   `,
`                                  false`,
`   `,
`   `,
`SEE ALSO: unify, subst, compose, idempotent, Eunify`
):


# Reference for the procedure subst:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 591

`unify/subst` := proc()
   local i;
   if nargs=0 then ERROR(`wrong number of parameters`) fi;
   for i to nargs-1 do
       if not type(args[i],`unify/substitution`)
       then ERROR(`wrong type of parameters`) fi
   od;
   # for future restrictions:
   if not type(args[nargs],anything) 
   then ERROR(`wrong type of parameters`) fi;
   # After type checking we just call the builtin procedure subs:
   subs(args)
end:


`help/unify/text/subst` := TEXT(
`   `,
`FUNCTION: subst - apply a substitution to an expression`,
`   `,
`CALLING SEQUENCE:`,
`   subst(s_1,s_2,...,s_n,expr)`,
`   `,
`PARAMETERS:`,
`   s_1,... - substitutions (type substitution)`,
`   expr    - any expression`,
`   `,
`SYNOPSIS:   `,
`- The function subst returns an expression resulting from applying the`,
`  substitutions specified by the first arguments to the last argument expr.`,
`   `,
`- The substitutions are performed sequentially starting with s1.`,
`   `,
`- The equations (bindings) in each substitution are performed simultaneously.`,
`   `,
`- Every variable of the left hand side of an equation from the substitution`,
`  which appears in expr is replaced by the expression on the right hand side`,
`  of the equation.`,
`   `,
`- The action of substitution is not followed by evaluation.  In cases where`,
`  full evaluation is desired, it is necessary to use the eval function to`,
`  force an evaluation.`,
`   `,
`- For efficiency reasons after checking the arguments for proper type, the`,
`  builtin procedure subs is called.`,
`   `,
`EXAMPLES:   `,
`> subst( x=f(a) , f(x) );`,
`   `,
`                                  f(f(a))`,
`   `,
`   `,
`> subst( {x=y,y=x}, x=a , f(x,y) );`,
`   `,
`                                  f(y,a)`,
`   `,
`   `,
`SEE ALSO: unify, type/substitution, compose`
):


# Composition of two substitutions. For internal use only. No type checking.
`unify/compose2` := proc(delta,theta)
   local Sigma,Theta,x;
   # Apply theta to the rhs of each equation in delta:
   Sigma := { seq(lhs(x)=`unify/subst`(theta,rhs(x)),x=delta) };
   # Eliminate the substitutions in theta that have a common variable with Sigma
   # on the lhs of an equation:
   Theta := select( proc(z,elim) not member(lhs(z),elim) end, theta, map(lhs,delta));
   # Eliminate all equations x=x in Sigma:
   select( proc(z) lhs(z)<>rhs(z) end , Sigma ) union Theta
end:


# Reference for the procedure compose:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 601

`unify/compose` := proc()
   local c,i;
   if nargs=0 then ERROR(`wrong number of parameters`) fi;
   if not type([args],list(`unify/substitution`))
      then ERROR(`wrong type of parameters`) fi;
   if type(args[1],set) then c := args[1] else c := {args[1]} fi;
   # Apply the substitutions from the left to the right:
   for i from 2 to nargs do 
       if type(args[i],set) then c := `unify/compose2`(c,args[i]) 
                            else c := `unify/compose2`(c,{args[i]})
       fi
   od;
   c
end:
   

`help/unify/text/compose` := TEXT(
`   `,
`FUNCTION: compose - composition of substitutions`,
`   `,
`CALLING SEQUENCE:`,
`   compose(s_1,s_2,...,s_n)`,
`   `,
`PARAMETERS:`,
`   s_1,... - substitutions (type substitution)`,
`   `,
`SYNOPSIS:   `,
`- The function compose returns a substitution resulting from composing the`,
`  substitutions specified by the arguments.`,
`   `,
`- The composition of the substitutions delta={x_1=t_1,x_2=t_2,...} and`,
`  theta={y_1=s_1,...} is the substitution obtained by removing elements of`,
`  the form y_k=s_k, where y_k is identical to a variable x_j, and those of`,
`  the form x_i=x_i from the set`,
`  {x_1=(t_1 theta), x_2=(t_2 theta), ..., y_1=s_1, y_2=s_2, ...}.`,
`   `,
`- Substitution composition is defined in this manner, so that`,
`  subst(t,compose(delta,theta)) = subst(subst(t,delta),theta).`,
`  As a consequence, substitution composition is associative.`,
`   `,
`EXAMPLES:   `,
`> compose( x=f(y) , y=h(a) );`,
`   `,
`                                  {x = f(h(a)), y = h(a)}`,
`   `,
`   `,
`> compose( x=f(z) , {z=a,y=v} , v=c );`,
`   `,
`                                  {x = f(a), z = a, y = c, v = c}`,
`   `,
`   `,
`> compose( {x=y,y=x}, {x=y,y=x} );`,
`   `,
`                                  { }`,
`   `,
`   `,
`SEE ALSO: unify, type/substitution, subst, inverse`
):


# Reference for the procedure inverse:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 605

`unify/inverse` := proc(s:`unify/psubstitution`)
   local S;
   if nargs<>1 then ERROR(`wrong number of parameters`) fi;
   if type(s,set) then S := s else S := {s} fi;
   map( proc(x) rhs(x)=lhs(x) end , S )
end:


`help/unify/text/inverse` := TEXT(
`   `,
`FUNCTION: inverse - compute the inverse of a permutation of variables`,
`   `,
`CALLING SEQUENCE:`,
`   inverse(sigma)`,
`   `,
`PARAMETERS:`,
`   sigma - a permutation of variables (type psubstitution)`,
`   `,
`SYNOPSIS:   `,
`- The function inverse returns an inverse substitution of the permutation`,
`  of variables sigma, i.e. compose(sigma,inverse(sigma)) = { } .`,
`   `,
`EXAMPLES:   `,
`> sigma := {x=y,y=z,z=x,u=v,v=u};`,
`   `,
`                     sigma := {x = y, y = z, z = x, u = v, v = u}`,
`   `,
`   `,
`> delta := inverse(sigma);`,
`   `,
`                     delta := {y = x, z = y, x = z, v = u, u = v}`,
`   `,
`   `,
`> compose(sigma,delta);`,
`   `,
`                     { }`,
`   `,
`   `,
`> compose(delta,sigma);`,
`   `,
`                     { }`,
`   `,
`   `,
`SEE ALSO: unify, type/psubstitution, compose, inversion`
):


`unify/idempotent` := proc(s:`unify/substitution`)
   local vars,result,b;
   if nargs<>1 then ERROR(`wrong number of parameters`) fi;
   if type(s,set) then result := s else result := {s} fi;
   vars := map(lhs,result);
   # while not idempotent:
   while vars intersect indets(map(rhs,result),name) <> {} do
      for b in result do
         if has(rhs(b),lhs(b)) then RETURN(NULL) fi # cyclic term exists
      od;
      result := { seq(lhs(b)=`unify/subst`(s,rhs(b)),b=result) }
   od;
   result
end:


`help/unify/text/idempotent` := TEXT(
`   `,
`FUNCTION: idempotent - compute an equivalent and idempotent substitution`,
`   `,
`CALLING SEQUENCE:`,
`   idempotent(delta)`,
`   `,
`PARAMETERS:`,
`   delta - a substitution (type substitution)`,
`   `,
`SYNOPSIS:   `,
`- The function idempotent returns an equivalent substitution mu which is`,
`  idempotent, i.e. equivalent(delta,mu)=true, and compose(mu,mu)=mu.`,
`   `,
`- If delta cannot be transformed into an idempotent substitution, the`,
`  value NULL is returned. (see example below)`,
`   `,
`EXAMPLES:   `,
`> sigma := idempotent( {x=f(y),y=g(z),z=a} );`,
`   `,
`                          sigma := {x = f(g(a)), y = g(a), z = a}`,
`   `,
`   `,
`> type(sigma,isubstitution);`,
`   `,
`                          true`,
`   `,
`   `,
`> idempotent( x=a );`,
`   `,
`                          {x = a}`,
`   `,
`   `,
`> idempotent( x=f(x) );`,
`   `,
`                          `,
`   `,
`   `,
`SEE ALSO: unify, type/isubstitution, compose, equivalent`
):


# Reference for the procedure generalization:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 602

`unify/generalization` := proc(mu:`unify/substitution`,sigma:`unify/substitution`)
   local Mu,Sigma;
   if nargs<>2 then ERROR(`wrong number of parameters`) fi;
   Mu := `unify/idempotent`(mu);
   Sigma := `unify/idempotent`(sigma);
   if Sigma=NULL then RETURN(true) fi;
   if Mu=NULL then RETURN(false) fi;
   evalb(`unify/compose`(Mu,Sigma)=Sigma)
end:


# Reference for the procedure equivalent:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 602

`unify/equivalent` := proc(mu:`unify/substitution`,sigma:`unify/substitution`)
   local Mu,Sigma;
   if nargs<>2 then ERROR(`wrong number of parameters`) fi;
   Mu := `unify/idempotent`(mu);
   Sigma := `unify/idempotent`(sigma);
   if Mu=NULL or Sigma=NULL then evalb(Mu=Sigma)
   else evalb(`unify/compose`(Mu,Sigma)=Sigma and `unify/compose`(Sigma,Mu)=Mu)
   fi
end:


`help/unify/text/equivalent` := TEXT(
`   `,
`FUNCTION: generalization, equivalent - compare substitutions`,
`   `,
`CALLING SEQUENCE:`,
`   generalization(mu,sigma)`,
`   equivalent(mu,sigma)`,
`   `,
`PARAMETERS:`,
`   mu,sigma - substitutions (type substitution)`,
`   `,
`SYNOPSIS:   `,
`- The function generalization determines whether mu is a generalization`,
`  of sigma, i.e. whether there exists a substitution lambda such that`,
`  compose(mu,lambda)=sigma.`,
`   `,
`- If sigma is not solvable, then mu is more general than sigma.`,
`   `,
`- The function equivalent determines whether mu and sigma are equivalent`,
`  substitutions, i.e. whether on the one hand mu is a generalization of`,
`  sigma and on the other hand sigma is a generalization of mu.`,
`   `,
`- If mu_1 and mu_2 are different results of the same unification problem`,
`  then equivalent(mu_1,mu_2) becomes true.`,
`   `,
`EXAMPLES:   `,
`> equivalent( x=y , y=x );`,
`   `,
`                                  true`,
`   `,
`   `,
`> equivalent( {x=y,y=a} , {x=a,y=a} );`,
`   `,
`                                  true`,
`   `,
`   `,
`> generalization( x=y , {x=a,y=a} );`,
`   `,
`                                  true`,
`   `,
`   `,
`> generalization( {x=a,y=a} , x=y );`,
`   `,
`                                  false`,
`   `,
`   `,
`> generalization( { } , x=f(x) );`,
`   `,
`                                  true`,
`   `,
`   `,
`SEE ALSO: unify, type/substitution, idempotent, minimal`
):


# Reference for the procedure minimal:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 597, Theorem 3 (reference to something related)

`unify/minimal` := proc()
   local sols,result,sigma;
   sols := { args };
   if not type(sols,set(`unify/substitution`)) then 
      ERROR(`wrong type of parameters`) fi;
   sols := map( `unify/idempotent` , sols ); # make all substitutions idempotent
   result := NULL;
   while sols<>{} do
      sigma := op(1,sols);
      sols := sols minus {sigma};
      # if none of the substitutions in sols or result is more general that sigma:
      if select( `unify/generalization` , sols union {result} , sigma ) = {} then
         result := result , sigma
      fi
   od;
   result
end:


`help/unify/text/minimal` := TEXT(
`   `,
`FUNCTION: minimal - compute a minimal base of idempotent solutions`,
`   `,
`CALLING SEQUENCE:`,
`   minimal(s_1,s_2,...,s_n)`,
`   `,
`PARAMETERS:`,
`   s_1,... - substitutions (type substitution)`,
`   `,
`SYNOPSIS:   `,
`- The function minimal first converts s_1,...,s_n into idempotent`,
`  substitutions, and then removes all redundant substitutions.`,
`   `,
`- The output is a sequence of substitutions.`,
`   `,
`- This procedure can be used to compute an idempotent base of the`,
`  output from a unification algorithm which contains redundant`,
`  solutions (e.g. from unification under commutativity).`,
`   `,
`EXAMPLES:   `,
`> minimal( {x=y} , {x=a,y=a} );`,
`   `,
`                                  {x = y}`,
`   `,
`   `,
`> minimal( {x=f(y),y=c} , {x=f(c)} , {z=a} );`,
`   `,
`                                  {x = f(c)} , {z = a}`,
`   `,
`   `,
`> minimal( { } , x=a );`,
`   `,
`                                  { }`,
`   `,
`   `,
`> minimal( x=f(x) );`,
`   `,
`                                  `,
`   `,
`   `,
`SEE ALSO: unify, type/substitution, equivalent`
):


# Reference for the procedure inversion:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 605, Proposition 14

`unify/inversion` := proc(mu:`unify/isubstitution`,theta:`unify/isubstitution`)
   local Mu,Theta,carrier;
   if nargs<>2 then ERROR(`wrong number of parameters`) fi;
   if not `unify/equivalent`(mu,theta) then ERROR(`parameters must be equivalent`) fi;
   if type(mu,set) then Mu := mu else Mu := {mu} fi;
   if type(theta,set) then Theta := theta else Theta := {theta} fi;
   # variables in the domain of Mu that are not in the domain of Theta:
   carrier := map(lhs,Mu) minus map(lhs,Theta);
   # apply Mu to the variables in carrier; create permutations of variables:
   map( proc(x,s) x=`unify/subst`(s,x) , `unify/subst`(s,x)=x end , carrier , Mu )
end:


`help/unify/text/inversion` := TEXT(
`   `,
`FUNCTION: inversion - compute the transform between equivalent substitutions`,
`   `,
`CALLING SEQUENCE:`,
`   inversion(mu,theta)`,
`   `,
`PARAMETERS:`,
`   mu,theta - equivalent and idempotent substitutions (type isubstitution)`,
`   `,
`SYNOPSIS:   `,
`- The function inversion computes from two equivalent and idempotent`,
`  substitutions mu and theta an invertible substitution (type psubstitution)`,
`  alpha such that mu = compose(theta,alpha).`,
`   `,
`- Such equivalent and idempotent substitutions may be the result of`,
`  different unification processes on the same equation set.`,
`   `,
`- If mu and theta are not equivalent, then an error message is returned.`,
`   `,
`EXAMPLES:   `,
`> inversion( {x=y} , {y=x} );`,
`   `,
`                        {x = y, y = x}`,
`   `,
`   `,
`> mu    := { x=g(y) , z=y }:`,
`> theta := { x=g(z) , y=z }:`,
`> alpha := inversion(mu,theta);`,
`   `,
`                        alpha := {z = y, y = z}`,
`   `,
`   `,
`> mu = compose( theta , alpha );`,
`   `,
`                        {x = g(y) ,z = y} = {x = g(y) ,z = y}`,
`   `,
`   `,
`> theta = compose( mu , inverse(alpha) );`,
`   `,
`                        {x = g(z) ,y = z} = {x = g(z) ,y = z}`,
`   `,
`   `,
`SEE ALSO: unify, type/isubstitution, inverse, equivalent, Eunify`
):


# Reference for the procedure Eunify:
# Baader and Siekmann, "Unification Theory",
# Subsection 3.3.2 (Algorithm of J. Corbin and M. Bidoit)
`unify/Eunify` := proc(equs:{algebraic=algebraic,set(algebraic=algebraic)},
                       Vars:{name,set(name)})
   local Map, vars, todo, free, e, k1, k2, u, v, i, result;
   if nargs=3 then 
      if args[3]<>'map' then ERROR(`third parameter must be 'map'`) fi
   elif nargs<>2 then ERROR(`wrong number of parameters`) 
   fi;
   Map := evalb(nargs=3);
   if type(equs,set) then todo := equs else todo := {equs} fi;
   if type(Vars,set) then vars := Vars else vars := {Vars} fi;
   if Map then free := map(op@indets,map(lhs,todo),name) intersect vars fi;
   while todo <> {} do
      e := op(1,todo); # get one equation
      todo := todo minus {e};
      k1 := lhs(e); k2 := rhs(e);
      if k1=k2 then next fi; # nothing to do if k1=k2
      if member(k2,eval(vars,1)) # k2 is a variable
         then u := k2; v := k1
         else u := k1; v := k2
      fi;
      # if one of the nodes is a variable node then u is now a variable
      # node; if both nodes are variables then u=rhs and v=lhs.
      if member(u,eval(vars,1)) then # u is a variable node
         if has(v,u) then # occur-check failure
            unassign(op(eval(vars,1)));
            RETURN(NULL)
         else # assign v to the variable u (u := v)
            if Map and member(u,free) then # not permitted
               unassign(op(eval(vars,1)));
               RETURN(NULL)
            fi;
            assign(u,v)
         fi
      else # u and v are both function nodes
         if type(u,name) then # u is a constant
            if u<>v then # clash failure
               unassign(op(eval(vars,1)));
               RETURN(NULL)
            fi
         elif op(0,u)<>op(0,v) or nops(u)<>nops(v) then # clash failure
            unassign(op(eval(vars,1)));
            RETURN(NULL)
         else # general case
            todo := todo union { seq(op(i,u)=op(i,v),i=1..nops(u)) }
         fi
      fi;
      todo := eval(todo);
   od;
   result := map( proc(x) eval(x,1)=eval(x) end , eval(vars,1) );
   unassign(op(eval(vars,1))); # reset all variables
   # remove the equations of the form x=x
   select( proc(x) lhs(x)<>rhs(x) end , result )
end:


`help/unify/text/Eunify` := TEXT(
`   `,
`FUNCTION: Eunify - compute a most general unifier (mgu)`,
`   `,
`CALLING SEQUENCE:`,
`   Eunify(equs,vars)`,
`   Eunify(equs,vars,'map')`,
`   `,
`PARAMETERS:`,
`   equs - (set of) equation(s)`,
`   vars - (set of) variable(s)`,
`   `,
`SYNOPSIS:   `,
`- The function Eunify returnes a most general unifier (mgu) of the equation`,
`  set (or single equation) equs with respect to the variables vars.`,
`  Eunify computes an mgu w.r.t. the empty theory (Robinson Unification).`,
`   `,
`- If equs is not unifiable, then the value NULL is returned.`,
`   `,
`- If a third parameter 'map' is given, then only the variables on the`,
`  rhs of the equation(s) may be bound by the unifier.`,
`   `,
`- To test whether phi is an mgu of an equation (set) equs, first compute any`,
`  mgu muof equs by:  mu:=Eunify(equs,vars);  Then check if phi and mu are`,
`  equivalent by:  equivalent(phi,mu);`,
`   `,
`- The algorithm implemented has a quadratic time complexity. An informal`,
`  description can be found in F. Baader and J.H. Siekmann, "Unification`,
`  Theory", Handbook of Logic in Artificial Intelligence and Logic Programming.`,
`  Full Paper: J. Corbin and M. Bidoit, "A Rehabilitation of Robinson's`,
`  Unification Algorithm", Information Processing 83.`,
`   `,
`EXAMPLES:   `,
`   `,
`> s := f(a,g(x,y)):`,
`> t := f(z,g(b,b)):`,
`> mu := Eunify( s = t , {x,y,z} );`,
`   `,
`                        mu := {x = b, y = b, z = a}`,
`   `,
`   `,
`> subst(mu,s) = subst(mu,t);`,
`   `,
`                        f(a,g(b,b)) = f(a,g(b,b))`,
`   `,
`   `,
`> Eunify( x = f(x) , x );`,
`   `,
`   `,
`> Eunify( {f(a) = g(a), c=c} , x );`,
`   `,
`   `,
`> Eunify( f(x) = f(a) , x );`,
`   `,
`                        {x = a}`,
`   `,
`   `,
`> Eunify( f(x) = f(a) , x , 'map' );`,
`   `,
`   `,
`SEE ALSO: unify, minimal, rank, equivalent, inversion, redundant`
):


# Reference for the procedure rank:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 595, Proposition 2

`unify/rank` := proc(equs:{algebraic=algebraic,set(algebraic=algebraic)},
                     vars:{name,set(name)})
   local mgu;
   if nargs<>2 then ERROR(`wrong number of parameters`) fi;
   mgu := `unify/Eunify`(equs,vars);
   if mgu=NULL then ERROR(`equation (set) is not unifiable`) fi;
   nops( mgu )
end:


`help/unify/text/rank` := TEXT(
`   `,
`FUNCTION: rank - compute the rank of a solvable equation (set)`,
`   `,
`CALLING SEQUENCE:`,
`   rank(equs,vars)`,
`   `,
`PARAMETERS:`,
`   equs - solvable (set of) equation(s)`,
`   vars - (set of) variable(s)`,
`   `,
`SYNOPSIS:   `,
`- The function rank returns the rank of the solvable equation set`,
`  (or single equation) equs with respect to the variables vars.`,
`  The rank of equs is the number of bindings in one of its mgus.`,
`  This number is known to be constant, depending only on equs and vars,`,
`  as equivalent substitutions have the same rank.`,
`   `,
`- The output is a natural integer.`,
`   `,
`- The dimension of an equation (set) equs can be computed by:`,
`   `,
`          nops(vars) - rank(equs,vars)`,
`   `,
`- If equs is not unifiable, then an error message is returned.`,
`   `,
`EXAMPLES:   `,
`   `,
`> Eunify( f(x,y,z)=f(a,b,c) , {x,y,z} );`,
`   `,
`                             {x = a, y = b, z = c}`,
`   `,
`   `,
`> rank( f(x,y,z)=f(a,b,c) , {x,y,z} );`,
`   `,
`                                    3`,
`   `,
`   `,
`> rank( {f(a)=f(a),c=c} , x );`,
`   `,
`                                    0`,
`   `,
`   `,
`> rank( a=b , {} );`,
`   `,
`Error, (in unify/rank) equation (set) is not unifiable`,
`   `,
`   `,
`SEE ALSO: unify, Eunify, equivalent, redundant`
):


# Reference for the procedure redundant:
# Lassez, Maher, and Marriott, "Unification Revisited",
# Page 596, Proposition 5

`unify/redundant` := proc(equs:{algebraic=algebraic,set(algebraic=algebraic)},
                          vars:{name,set(name)})
   local Equs,e,r,newr,result;
   if nargs<>2 then ERROR(`wrong number of parameters`) fi;
   if type(equs,set) then Equs := equs else Equs := {equs} fi;
   # test if equs is solvable
   if `unify/Eunify`(Equs,vars)=NULL then ERROR(`equation (set) is not unifiable`) fi;
   # compute the rank of equs:
   r := `unify/rank`(Equs,vars);
   # now search for redundant equations:
   result := NULL;
   while Equs <> { } do
      e := op(1,Equs);
      Equs := Equs minus {e};
      newr := `unify/rank`(Equs,vars);
      if newr = r # e is a redundant equation
         then result := result , e
         else r := newr
      fi
   od;
   { result }
end:


`help/unify/text/redundant` := TEXT(
`   `,
`FUNCTION: redundant - compute a maximal subset of redundant equations`,
`   `,
`CALLING SEQUENCE:`,
`   redundant(equs,vars)`,
`   `,
`PARAMETERS:`,
`   equs - solvable (set of) equation(s)`,
`   vars - (set of) variable(s)`,
`   `,
`SYNOPSIS:   `,
`- The procedure redundant returns a maximal subset of redundant equations`,
`  of equs with respect to the variables vars. The equation (set) equs`,
`  must be solvable. Otherwise an error message is returned.`,
`   `,
`- The number of redundant equations is constant. This number can also`,
`  be computed by:   nops(equs) - rank(equs,vars);`,
`   `,
`- To obtain an equivalent equation (set) which contains no redundant`,
`  equations, compute: equs minus idempotent(equs,vars);`,
`   `,
`- If equs is not unifiable, then an error message is returned.`,
`   `,
`EXAMPLES:   `,
`   `,
`> redundant( {x=y,y=x,a=a} , {x,y} );`,
`   `,
`                             {y = x, a = a}`,
`   `,
`   `,
`> equs := {x=y,x=a,y=a}:`,
`> equs minus redundant( equs , {x,y} );`,
`   `,
`                             {x = y, x = a}`,
`   `,
`   `,
`> redundant( {x=a,x=a} , x );`,
`   `,
`                              { }`,
`   `,
`   `,
`> redundant( a=b , { } );`,
`   `,
`Error, (in unify/redundant) equation (set) is not unifiable`,
`   `,
`   `,
`SEE ALSO: unify, rank, minimal, Eunify`
):


`help/unify/text/rewrite` := TEXT(
`   `,
`FUNCTION: rewrite - an experimental term rewriting system`,
`   `,
`CALLING SEQUENCE:`,
`   rewrite(term,rules,vars)`,
`   rewrite1(term,rules,vars)`,
`   `,
`PARAMETERS:`,
`   term  - expression`,
`   rules - (set of) equation(s)`,
`   vars  - (set of) variable(s)`,
`   `,
`SYNOPSIS:   `,
`- The procedure rewrite1 applies the rule(s) once on the term w.r.t.`,
`  the variables vars. The procedure rewrite applies the rule(s) as`,
`  many times as possible.`,
`   `,
`- A rule is implemented as an equation. Applying a rule is to replace`,
`  the lhs of this rule by its rhs (or an instance of them).`,
`   `,
`- The only intention of these procedures is to give an idea of how to`,
`  use the unify-library for own applications.`,
`   `,
`- These procedures have (in contrast to the unify-library) neither a`,
`  good computing performance nor a high reliability.`,
`   `,
`- To use these procedures, copy the source code from below into your`,
`  active session.`,
`   `,
`EXAMPLES:   `,
`   `,
`> rewrite1 := proc(term:algebraic,`,
`                   rules:{algebraic=algebraic,set(algebraic=algebraic)},`,
`                   vars:{name,set(name)}                                )`,
`     local Rules,Vars,subterms,replace,s,rule,mu;`,
`     if nargs<>3 then ERROR(``wrong number of parameters``) fi;`,
`     if type(rules,set) then Rules := rules else Rules := {rules} fi;`,
`     if type(vars,set) then Vars := vars else Vars := {vars} fi;`,
`     subterms := indets(term);`,
`     if Vars intersect subterms <> {} then`,
`        ERROR(``first and second parameter must not contain common variables``)`,
`     fi;`,
`     replace := NULL;`,
`     for s in subterms do`,
`         for rule in Rules do`,
`             mu := Eunify(s=lhs(rule),Vars,'map');`,
`             if mu<>NULL then`,
`                replace := replace , s=subst(mu,rhs(rule))`,
`             fi`,
`         od`,
`     od;`,
`     subs({replace},term)`,
`  end:`,
`   `,
`   `,
`> rewrite := proc(term:algebraic,`,
`                  rules:{algebraic=algebraic,set(algebraic=algebraic)},`,
`                  vars:{name,set(name)}                                )`,
`     local oldterm,newterm;`,
`     if nargs<>3 then ERROR(``wrong number of parameters``) fi;`,
`     oldterm := NULL;`,
`     newterm := term;`,
`     while oldterm<>newterm do`,
`        oldterm := newterm;`,
`        newterm := rewrite1(oldterm,rules,vars)`,
`     od;`,
`     newterm`,
`  end:`,
`   `,
`   `,
`> rules := { f(f(x))=g(x,a) , a=c };`,
`   `,
`                             rules := {f(f(x)) = g(x,a), a = c}`,
`   `,
`   `,
`> vars := {x,y,z};`,
`   `,
`                             vars := {x, z, y}`,
`   `,
`   `,
`> rewrite1( f(f(f(a))) , rules , vars );`,
`   `,
`                             g(f(a),a)`,
`   `,
`   `,
`> rewrite( f(f(f(a))) , rules , vars );`,
`   `,
`                             g(f(c),c)`,
`   `,
`   `
):


`help/unify/text/Cunify` := TEXT(
`   `,
`FUNCTION: Cunify - an experimental unification algorithm modulo commutativity`,
`   `,
`CALLING SEQUENCE:`,
`   Cunify(equs,vars)`,
`   `,
`PARAMETERS:`,
`   equs - (set of) equation(s)`,
`   vars - (set of) variable(s)`,
`   `,
`SYNOPSIS:   `,
`- The function Cunify returns a most general unifier (mgu) modulo`,
`  commutativity of the equation set (or single equation) equs with`,
`  respect to the variables vars.`,
`   `,
`- Use the assume facility to tell the system that a function symbol is`,
`  commutative, e.g., if f is commutative, type:`,
`   `,
`          > assume( f , commutative );`,
`   `,
`- If equs is not unifiable, then the value NULL is returned.`,
`   `,
`- Only the very simple algorithm of J. Guard is implemented where all`,
`  permutations of the arguments of the commutative function symbols`,
`  are computed and afterwards Robinson unification is applied.`,
`   `,
`- The only intention of this procedure is to give an idea of how to`,
`  use the unify-library for own applications.`,
`   `,
`- This procedure has (in contrast to the unify-library) neither a`,
`  good computing performance nor a high reliability.`,
`   `,
`- To use Cunify, copy the source code from below into your active session.`,
`   `,
`EXAMPLES:   `,
`   `,
`> # returns a list of all variants of expr w.r.t. the commutativity law`,
`  unfold := proc(expr:{algebraic,algebraic=algebraic,set(algebraic=algebraic)})`,
`     local ll,T,s;`,
`     if type(expr,name) then RETURN([expr]) fi;  # nothing to commute`,
`     # expr is a function, an equation, or a set of equations`,
`     ll := map( unfold , [op(expr)] );`,
`     T := combinat[cartprod](ll);`,
`     s := NULL;`,
`     while not T[finished] do s := s , T[nextvalue]() od;`,
`     s := [s];`,
`     if type(expr,function) and nops(expr)=2 and is(op(0,expr),commutative) then`,
`        s := map( proc(x) x,[op(2,x),op(1,x)] end , s );`,
`     fi;`,
`     if   type(expr,``=``) then map( proc(x) op(1,x)=op(2,x) end , s )`,
`     elif type(expr,set) then map( proc(x) {op(x)} end , s )`,
`                         else map( op(0,expr)@op , s )`,
`     fi`,
`  end:`,
`   `,
`   `,
`> Cunify := proc(equs:{algebraic=algebraic,set(algebraic=algebraic)},`,
`                 vars:{name,set(name)}                               )`,
`     local Equs,Vars;`,
`     if nargs<>2 then ERROR(``wrong number of parameters``) fi;`,
`     if type(equs,set) then Equs := equs else Equs := {equs} fi;`,
`     if type(vars,set) then Vars := vars else Vars := {vars} fi;`,
`     minimal( op(map( Eunify , unfold(Equs) , Vars )) )`,
`  end:`,
`   `,
`   `,
`> assume( f , commutative );`,
`   `,
`> Cunify( f(f(a,b),a) = f(x,f(y,z)) , {x,y,z} );`,
`   `,
`                    {x = a, z = b, y = a}, {x = a, z = a, y = b}`,
`   `,
`   `
):


save `unify.m`;
quit;