CL Unification: Standard Generic Function UNIFY
 

Generic function UNIFY

Package:

COMMON-LISP.EXTENSIONS.DATA-AND-CONTROL-FLOW.UNIFICATION

Syntax:

  unify object1 object2 &optional substitution
  => substitution
  

Arguments and Values:

object1---an object

object2---an object

substitution---a substitution

Description:

The generic function UNIFY is the entry point in the unification machinery. It takes two CL objects, object1 and object2 and checks whether they can be unified by constructing a (possibly empty) consistent substitution assigning appropriate values to the unification variables appearing each object. The rules by which the unification process is carried on are dependent on the types of the two objects. The known rules are described in the "known methods" section.

UNIFY takes a substitution as an optional argument. The default value is a fresh empty substitution obtained by calling MAKE-EMPTY-ENVIRONMENT.

Known Methods:

Note that UNIFY is commutative in its two required arguments. Each method listed exists also with object1 and object2 reversed.

First, the methods defined on standard CL types are described, and then all the methods involving unification templates are described.

  •   unify (s1 symbol) (s2 symbol) &optional substitution
      => substitution
      

    The unification of two symbols depends on whether one (or both) of them is a unification variable (i.e. either the symbol with name "_", or a symbol with name starting with the character #\?.)

    If neither object is an unification variable, then UNIFY succeds if and only if the two symbols s1 and s2 are EQ.

    If s1 is an unification variable, and either s1 is not bound in substitution, or s1 is bound to s2 then UNIFY succeds. If s1 was not bound in the substitution, then a new binding for s1 to s2 is created.

    The symmetric case holds if s1 is not an unification variable but s2 is.

    Otherwise an error of type UNIFICATION-FAILURE is signaled.

  •   unify (v symbol) (object t) &optional substitution
      => substitution
      

    The symbol v must be an unification variable. If not, an error of type UNIFICATION-FAILURE will be signaled. Otherwise, the a new binding for the variable v with value object will be created in the substitution.

    The creation of the new binding for v in the substitution is dependent on the occur check implemented by the generic function OCCURS-IN-P. OCCURS-IN-P is called by the unification machinery if the variable *OCCURRENCE-CHECK-P* is non-NIL (the default.) If *OCCURENCE-CHECK-P* is non-NIL, and if the variable v occurs in the object (i.e. OCCURS-IN-P returns a non-NIL value,) then an error of type UNIFICATION-FAILURE is signaled.

  •   unify (n1 number) (n2 number) &optional substitution
      => substitution
      

    Two numbers unify if and only if they are =, in which case substitution is returned unmodified. Otherwise, an error of type UNIFICATION-FAILURE is signaled.

  •   unify (s1 string) (s2 string) &optional substitution
      => substitution
      

    Two strings unify only is they are "equal", under the following condition. If the variable *UNIFY-STRING-CASE-SENSITIVE-P* is T (the default) then the two strings s1 and s2 are compared using STRING=, otherwise they are compared using STRING-EQUAL.

    If the two strings s1 and s2 are equal then substitution is returned unchanged, otherwise an error of type UNIFICATION-FAILURE is signaled.

  •   unify (v1 vector) (v2 vector) &optional substitution
      => substitution
      

      unify (l1 list) (l2 list) &optional substitution
      => substitution
      

      unify (s1 sequence) (s2 sequence) &optional substitution
      => substitution
      

    The "sequence" methods (and the specialized ones, mostly for efficiency) extend the substitution by calling UNIFY recursively on each element of the two sequences, s1 and s2 (respectively, l1 and l2, v1 and v2.)

    An error of type UNIFICATION-FAILURE is signaled if the two sequences are of different LENGTH or if any call to UNIFY fails.

  •   unify (a1 array) (a2 array) &optional substitution
      => substitution
      

    Two arrays a1 and a2 UNIFY if and only if each of the respective elements does. The two arrays are traversed using ROW-MAJOR-AREF. Otherwise an error of type UNIFICATION-FAILURE is signaled.

    An error of type UNIFICATION-FAILURE is also signaled if the two arrays have different total size (as returned by ARRAY-TOTAL-SIZE.)

  •   unify (object1 t) (object2 t) &optional substitution
      => substitution
      

    This is the catch all method that is called as a last resort. No recursive call to UNIFY is attempted, and the call succeeds if and only if object1 and object2 are EQUALP. Otherwise, an error of type UNIFICATION-FAILURE is signaled.

The next methods all involve a unification template. Again all these methods are commutative in their required arguments.

  •   unify (s structure-object) (st structure-object-template) &optional substitution
      => substitution
      

    This method UNIFYs a s against a STRUCTURE-OBJECT-TEMPLATE st. st has the following (general) structure.

         (<structure-class specifier> [ (<reader> <value>) ]* )
      

    The structure-class specifier is a symbol naming a structure class, reader is one of the DEFSTRUCT-generated accessors, and value is a regular CL object, a unification variable, or a unification template.

    The class of s must be a subclass of structure-class specifier. Otherwise, an error of type UNIFICATION-FAILURE is signaled.

    UNIFY is called recursively on each value and the result of applying reader to s.

    If all the (recursive) calls to UNIFY succeed, then a possibly augmented substitution is returned. Otherwise, an error of type UNIFICATION-FAILURE is signaled.

  •   unify (s standard-object) (st standard-object-template) &optional substitution
      => substitution
      

    This method UNIFYs a s against a STANDARD-OBJECT-TEMPLATE st. st has the following (general) structure.

         (<standard-class specifier> [ ([slot-value | slot-accessor] <slot-spec> <value>) ]* )
      

    The standard-class specifier is a symbol naming a class, slot-spec is a valid slot accessor when slot-value is specified, or a valid slot name for the class, when slot-value is specified, and value is a regular CL object, a unification variable, or a unification template.

    The class of s must be a subclass of standard-class specifier. Otherwise, an error of type UNIFICATION-FAILURE is signaled.

    UNIFY is called recursively on each value and the result of extracting the slot value from s using either the accessor supplied, or SLOT-VALUE.

    If all the (recursive) calls to UNIFY succeed, then a possibly augmented substitution is returned. Otherwise, an error of type UNIFICATION-FAILURE is signaled.

Affected By:

None.

Exceptional Situations:

If object1 and object2 cannot be unified, then an error of type UNIFICATION-FAILURE is signaled.

See Also:

MAKE-EMPTY-ENVIRONMENT, UNIFICATION-FAILURE, *UNIFY-STRING-CASE-SENSITIVE-P*, OCCURS-IN-P, *OCCURENCE-CHECK-P*.

Notes:

The unification algorithm implemented is very flexible and provides many hooks for customization. However, it is not necessarily asymptotically efficient (it has a worst case exponential time complexity.)

It would be interesting to reimplement the kernel of the system using a linear unification algorithm like the one described in

[MM82] A. Martelli and U. Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, Vol. 4, No. 2, April 1982, Pages 258--282.