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}