* Unification and Substitutions (aka Binding Lists) * * This code is borrowed from "Paradigms of AI Programming: Case Studies * in Common Lisp", by Peter Norvig, published by Morgan Kaufmann, 1992. * The complete code from that book is available for ftp at mkp.com in * the directory "pub/Norvig". Note that it uses the term "bindings" * rather than "substitution" or "theta". The meaning is the same. ** * @author Michael S. Braverman * @author Peter Norvig * @see Variable * @see Bindings * @see Expression */ // In the current documentation, we show the original LISP code corresponding // to each JAVA method so that they may be more easily compared public class Unify { /** * Parses the input
String into an expression which may be
* processed by the various unify methods. In particular, tokens in the
* input that are prefixed appropriately are converted into
* Variable objects.
*
* @return An expression suitable as input to the various Unify methods
* @param exprStr An expression to parse.
* @exception Exception May be thrown if the expression String
* does not parse properly.
* @see #unify
* @see #unifier
* @see Variable#getPrefix
*/
static public Object parse(String exprStr) throws Exception {
return parseVariables(Expression.parse(exprStr));
}
/**
* Processes a (compound or atomic) expression to create a new expression
* in which all atoms, whose print names have an appropriate prefix
* character, are replaced with Variable objects.
*
* @return An expression suitable as input to the various Unify methods
* @param obj An expression to process.
* @see #unify
* @see #unifier
* @see Expression
* @see Variable#getPrefix
*/
static public Object parseVariables(Object obj) {
if (Expression.isAtomic(obj)) {
if ((obj instanceof String) &&
(((String)obj).charAt(0) == Variable.getPrefix())) {
return new Variable(((String)obj).substring(1));
} else {
return obj;
}
} else {
return Expression.reuse(parseVariables(Expression.car(obj)),
parseVariables(Expression.cdr(obj)),
obj);
}
}
/**
* Returns something that unifies with both x and y (or fail).
*
* @return An expression that unifies with both x and y, or the
* Bindings object that represents failure.
* @param x An expression (atomic or compound) to unify.
* @param y An expression (atomic or compound) to unify.
* @see Bindings#getFailure
* @see Expression
* @see #unify
*/
/* Original LISP:
* (defun unifier (x y)
* "Return something that unifies with both x and y (or fail)."
* (subst-bindings (unify x y) x))
*/
static public Object unifier(Object x, Object y) {
// note: I reversed the order of the parameters to substBindings
return substBindings(x,unify(x,y));
}
/**
* Determines if the given expressions match and
* returns a Bindings object that would make them equal.
*
*
* By default, the Bindings object returned is
* in terms of a ListBindings implementation.
* If you want to explicitly specify the Bindings
* implementation to use, use the alternative version of unify
* where you should pass in an empty Bindings object
* of the desired implementation type. For instance:
*
* Unify.unify(x,y,HashBindings.getEmpty()); ** would return the results of the unification in a *
HashBindings Bindings implementation.
*
* @return A Bindings object that would make the
* input parameters match, or the Bindings object that
* represents failure if they do not match.
* @param x An expression (atomic or compound) to unify.
* @param y An expression (atomic or compound) to unify.
* @see Bindings
* @see ListBindings
* @see HashBindings
* @see Variable
* @see Expression
*/
/*
* (defun unify (x y &optional (bindings +no-bindings+))
* "See if x and y match with given bindings. If they do,
* return a binding list that would make them equal [p 303]."
* (cond ((eq bindings +fail+) +fail+)
* ((eql x y) bindings)
* ((variable? x) (unify-var x y bindings))
* ((variable? y) (unify-var y x bindings))
* ((and (consp x) (consp y))
* (unify (rest x) (rest y)
* (unify (first x) (first y) bindings)))
* (t +fail+)))
*/
static public Bindings unify(Object x, Object y) {
return unify(x,y,ListBindings.getEmpty());
}
/**
* Determines if the given expressions match subject to the variable
* bindings given in the initial Bindings object and returns a
* Bindings object that would make them equal.
*
* @return A Bindings object that would make the
* input parameters match, or the Bindings object that
* represents failure if they do not match.
* @param x An expression (atomic or compound) to unify.
* @param y An expression (atomic or compound) to unify.
* @param theBindings An initial set of bindings to begin with.
* @see Bindings
* @see Variable
* @see Expression
*/
static public Bindings unify(Object x, Object y,
Bindings theBindings) {
if (theBindings.isFailure()) {
return theBindings;
} else if (Expression.eql(x,y)) {
return theBindings;
} else if (x instanceof Variable) {
return unifyVar((Variable) x,y,theBindings);
} else if (y instanceof Variable) {
return unifyVar((Variable) y,x,theBindings);
} else if (Expression.isTrueCompound(x) &&
Expression.isTrueCompound(y)) {
return unify(Expression.rest(x),Expression.rest(y),
unify(Expression.first(x),Expression.first(y),theBindings));
} else {
return theBindings.getFailure();
}
}
/**
* Determines if the given Variable occurs anywhere inside
* the given expression, subject to the bindings contained in the given
* Bindings object.
*
* @return true iff var is contained is x subject
* to theBindings
* @param var Variable for which to search.
* @param x An expression (atomic or compound) to search.
* @param theBindings An set of bindings on the variables in x
* @see Bindings
* @see Variable
* @see Expression
*/
/*
(defun occurs-in? (var x bindings)
"Does var occur anywhere inside x?"
(cond ((eq var x) t)
((and (variable? x) (get-binding x bindings))
(occurs-in? var (lookup x bindings) bindings))
((consp x) (or (occurs-in? var (first x) bindings)
(occurs-in? var (rest x) bindings)))
(t nil)))
*/
static public boolean occursIn(Variable var, Object x,
Bindings theBindings) {
if (var == x) {
return true;
} else if ((x instanceof Variable) &&
theBindings.isBound((Variable) x)) {
return occursIn(var, theBindings.getBinding((Variable) x),
theBindings);
} else if (Expression.isTrueCompound(x)) {
return (occursIn(var, Expression.first(x), theBindings) ||
occursIn(var, Expression.rest(x), theBindings));
} else {
return false;
}
}
/**
* Creates an isomorphic expression to the given expression in which all
* the variables have been replaced with new ones. If a variable appears
* more than once in the expression, then it is given the same replacement
* at each position in which it occurs.
*
* @return An isomorphic expression with new Variables.
* @param x An expression (atomic or compound) to process.
* @see Variable
* @see Expression
*/
/*
* (defun rename-variables (x)
* "Replace all variables in x with new ones."
* (sublis (mapcar #'(lambda (var) (make-binding var (new-variable var)))
* (variables-in x))
* x))
*/
static public Object renameVariables(Object x) {
// I didn't want to reimplement sublis right now, so instead I build
// a map from existing variables to new variables, and then just use
// substBindings to rename the variables in the Object passed.
Bindings b = buildNewVarMap(x, HashBindings.getEmpty());
return substBindings(x, b);
}
/**
* Creates a new expression in which the values of the variables indicated
* in the given Bindings object are substituted into the given
* (compound or atomic) expression.
*
*
* Note: The order of the parameters might be different than what you
* may be used to seeing if you are familiar with the LISP version of this
* function (but they are more in line with all the other methods in the
* Unify class).
*
* @return An expression where the Variable values have been
* substituted in place of the Variables themselves.
* @param x An expression (atomic or compound) to process.
* @param theBindings The variable bindings.
* @see Bindings
* @see Variable
* @see Expression
*/
/*
* (defun subst-bindings (bindings x)
* "Substitute the value of variables in bindings into x,
* taking recursively bound variables into account."
* (cond ((eq bindings +fail+) +fail+)
* ((eq bindings +no-bindings+) x)
* ((and (variable? x) (get-binding x bindings))
* (subst-bindings bindings (lookup x bindings)))
* ((atom x) x)
* (t (reuse-cons (subst-bindings bindings (car x))
* (subst-bindings bindings (cdr x))
* x))))
*/
// Note: swapped the order of the bindings and object to make more sense
// (i.e., to people who have never heard of sublis):
static public Object substBindings(Object x, Bindings theBindings) {
if (theBindings.isFailure()) {
return theBindings;
} else if (theBindings.isEmpty()) {
return x;
} else if ((x instanceof Variable) &&
theBindings.isBound((Variable) x)) {
return substBindings(theBindings.getBinding((Variable) x),
theBindings);
} else if (Expression.isAtomic(x)) {
return x;
} else {
return Expression.reuse(substBindings(Expression.first(x),theBindings),
substBindings(Expression.rest(x),theBindings),
x);
}
}
/**
* Unifies the given Variable with the given expression,
* using (and maybe extending) the given Bindings object.
*
* @return A Bindings object that would make the
* variable match the expression, or the Bindings object that
* represents failure if they do not match.
* @param var A Variable to unify.
* @param x An expression (atomic or compound) to unify.
* @param theBindings An initial set of bindings to begin with.
* @see Bindings
* @see Variable
* @see Expression
*/
/*
* (defun unify-var (var x bindings)
* "Unify var with x, using (and maybe extending) bindings [p 303]."
* (cond ((get-binding var bindings)
* (unify (lookup var bindings) x bindings))
* ((and (variable? x) (get-binding x bindings))
* (unify var (lookup x bindings) bindings))
* ((occurs-in? var x bindings)
* +fail+)
* (t (extend-bindings var x bindings))))
*/
static private Bindings unifyVar(Variable var,Object x,
Bindings theBindings) {
if (theBindings.isBound(var)) {
return unify(theBindings.getBinding(var), x, theBindings);
} else if ((x instanceof Variable) &&
theBindings.isBound((Variable) x)) {
return unify(var, theBindings.getBinding((Variable) x), theBindings);
} else if (occursIn(var,x,theBindings)) {
return theBindings.getFailure();
} else {
return theBindings.extendBindings(var,x);
}
}
/**
* Searches the given (compound or atomic) expression to find all the
* Variables it contains and returns a Bindings
* object mapping from each Variable in the expression to
* a new, previously non-existant, Variable.
*
* @return A Bindings map from old to new
* Variables.
* @param x An expression (atomic or compound) to process.
* @param varMap A mapping from old to new Variables to extend.
* @see Bindings
* @see Variable
* @see Expression
*/
private static Bindings buildNewVarMap(Object x, Bindings varMap) {
if (x instanceof Variable) {
if (!varMap.isBound((Variable) x)) {
return varMap.extendBindings((Variable) x,
new Variable((Variable) x));
} else {
return varMap;
}
} else if (Expression.isTrueCompound(x)) {
return buildNewVarMap(Expression.first(x),
buildNewVarMap(Expression.rest(x),
varMap));
} else {
return varMap;
}
}
/**
* Placeholder to keep Unify objects from being created.
*/
private Unify() {
// This keeps Unify objects from being created.
}
/**
* Used in testing out the functionality of this class.
* @param obj1 An expression to unify.
* @param obj2 An expression to unify.
*/
static private void testIt(Object obj1, Object obj2) {
System.out.println("unify("+obj1+","+obj2+") ="+
unify(obj1,obj2));
System.out.println("unifier("+obj1+","+obj2+") ="+
unifier(obj1,obj2));
System.out.println("-----");
}
/**
* Tests out the functionality of this class.
* @param args Ignored.
* @exception Exception Thrown in case of an internal parsing error.
*/
static public void main(String [] args) throws Exception {
Object x = parse("(a b)");
Object y = parse("(a b)");
Object v1 = parse("?x");
Object v2 = parse("?x");
Variable vy = new Variable("y");
Object z1 = parse("(a . c)");
Object z2 = new Expression("a",new Variable("x"));
Object z3 = new Expression(vy,vy);
Object z4 = renameVariables(z3);
Object z5 = parse("(?x y z)");
Object z6 = parse("(z y ?x)");
Object z7 = parse("(?y ?y z)");
Object z8 = parse("(?y ?y ?x)");
testIt(v1,v2);
testIt(x,y);
testIt(x,z1);
testIt(x,z2);
testIt(x,z3);
testIt(z3,z3);
testIt(z3,z4);
testIt(z4,z5);
testIt(z5,z6);
testIt(z6,z7);
testIt(z7,z8);
}
}