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.

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.

*CL Unification: Standard Generic Function UNIFY* Home \| Previous \| Next \| Downloads \| Links
	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.
	News News in chronological order, most recent on top. 2004-04-12 Completed description.
© 2003-2004, Marco Antoniotti, all rights reserved.