aima.core.logic.fol

Class Unifier

java.lang.Object

aima.core.logic.fol.Unifier

public class Unifier
extends java.lang.Object

Artificial Intelligence A Modern Approach (3rd Edition): Figure 9.1, page 328.

 function UNIFY(x, y, theta) returns a substitution to make x and y identical
   inputs: x, a variable, constant, list, or compound
           y, a variable, constant, list, or compound
           theta, the substitution built up so far (optional, defaults to empty)
           
   if theta = failure then return failure
   else if x = y the return theta
   else if VARIABLE?(x) then return UNIVY-VAR(x, y, theta)
   else if VARIABLE?(y) then return UNIFY-VAR(y, x, theta)
   else if COMPOUND?(x) and COMPOUND?(y) then
       return UNIFY(x.ARGS, y.ARGS, UNIFY(x.OP, y.OP, theta))
   else if LIST?(x) and LIST?(y) then
       return UNIFY(x.REST, y.REST, UNIFY(x.FIRST, y.FIRST, theta))
   else return failure
   
 ---------------------------------------------------------------------------------------------------
 
 function UNIFY-VAR(var, x, theta) returns a substitution
            
   if {var/val} E theta then return UNIFY(val, x, theta)
   else if {x/val} E theta then return UNIFY(var, val, theta)
   else if OCCUR-CHECK?(var, x) then return failure
   else return add {var/x} to theta
 

Figure 9.1 The unification algorithm. The algorithm works by comparing the structures of the inputs, elements by element. The substitution theta that is the argument to UNIFY is built up along the way and is used to make sure that later comparisons are consistent with bindings that were established earlier. In a compound expression, such as F(A, B), the OP field picks out the function symbol F and the ARGS field picks out the argument list (A, B).

Author:

Ciaran O'Reilly, Ravi Mohan, Mike Stampone

Constructor Summary

Constructors

Constructor and Description
Unifier()

Method Summary

Modifier and Type	Method and Description
protected boolean	occurCheck(java.util.Map<Variable,Term> theta, Variable var, FOLNode x)
java.util.Map<Variable,Term>	unify(FOLNode x, FOLNode y) Returns a Map representing the substitution (i.e.
java.util.Map<Variable,Term>	unify(FOLNode x, FOLNode y, java.util.Map<Variable,Term> theta) Returns a Map representing the substitution (i.e.
java.util.Map<Variable,Term>	unify(java.util.List<? extends FOLNode> x, java.util.List<? extends FOLNode> y, java.util.Map<Variable,Term> theta) Returns a Map representing the substitution (i.e.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Unifier

public Unifier()

Method Detail

unify

public java.util.Map<Variable,Term> unify(FOLNode x,
                                          FOLNode y)

Returns a Map representing the substitution (i.e. a set of variable/term pairs) or null which is used to indicate a failure to unify.

Parameters:

x - a variable, constant, list, or compound

y - a variable, constant, list, or compound

Returns:

a Map representing the substitution (i.e. a set of variable/term pairs) or null which is used to indicate a failure to unify.

unify

public java.util.Map<Variable,Term> unify(FOLNode x,
                                          FOLNode y,
                                          java.util.Map<Variable,Term> theta)

Returns a Map representing the substitution (i.e. a set of variable/term pairs) or null which is used to indicate a failure to unify.

Parameters:

x - a variable, constant, list, or compound

y - a variable, constant, list, or compound

theta - the substitution built up so far

Returns:

a Map representing the substitution (i.e. a set of variable/term pairs) or null which is used to indicate a failure to unify.

unify

public java.util.Map<Variable,Term> unify(java.util.List<? extends FOLNode> x,
                                          java.util.List<? extends FOLNode> y,
                                          java.util.Map<Variable,Term> theta)

Returns a Map representing the substitution (i.e. a set of variable/term pairs) or null which is used to indicate a failure to unify.

Parameters:

x - a variable, constant, list, or compound

y - a variable, constant, list, or compound

theta - the substitution built up so far

Returns:

a Map representing the substitution (i.e. a set of variable/term pairs) or null which is used to indicate a failure to unify.

occurCheck

protected boolean occurCheck(java.util.Map<Variable,Term> theta,
                             Variable var,
                             FOLNode x)