Generic function UNIFY
Package:
COMMONLISP.EXTENSIONS.DATAANDCONTROLFLOW.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 MAKEEMPTYENVIRONMENT.
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 UNIFICATIONFAILURE is signaled.

unify (v symbol) (object t) &optional substitution => substitution
The symbol v must be an unification variable. If not, an error of type UNIFICATIONFAILURE 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 OCCURSINP. OCCURSINP is called by the unification machinery if the variable *OCCURRENCECHECKP* is nonNIL (the default.) If *OCCURENCECHECKP* is nonNIL, and if the variable v occurs in the object (i.e. OCCURSINP returns a nonNIL value,) then an error of type UNIFICATIONFAILURE 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 UNIFICATIONFAILURE 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 *UNIFYSTRINGCASESENSITIVEP* is T (the default) then the two strings s1 and s2 are compared using STRING=, otherwise they are compared using STRINGEQUAL.
If the two strings s1 and s2 are equal then substitution is returned unchanged, otherwise an error of type UNIFICATIONFAILURE 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 UNIFICATIONFAILURE 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 ROWMAJORAREF. Otherwise an error of type UNIFICATIONFAILURE is signaled.
An error of type UNIFICATIONFAILURE is also signaled if the two arrays have different total size (as returned by ARRAYTOTALSIZE.)

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 UNIFICATIONFAILURE is signaled.
The next methods all involve a unification template. Again all these methods are commutative in their required arguments.

unify (s structureobject) (st structureobjecttemplate) &optional substitution => substitution
This method UNIFYs a s against a STRUCTUREOBJECTTEMPLATE st. st has the following (general) structure.
(<structureclass specifier> [ (<reader> <value>) ]* )
The structureclass specifier is a symbol naming a structure class, reader is one of the DEFSTRUCTgenerated accessors, and value is a regular CL object, a unification variable, or a unification template.
The class of s must be a subclass of structureclass specifier. Otherwise, an error of type UNIFICATIONFAILURE 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 UNIFICATIONFAILURE is signaled.

unify (s standardobject) (st standardobjecttemplate) &optional substitution => substitution
This method UNIFYs a s against a STANDARDOBJECTTEMPLATE st. st has the following (general) structure.
(<standardclass specifier> [ ([slotvalue  slotaccessor] <slotspec> <value>) ]* )
The standardclass specifier is a symbol naming a class, slotspec is a valid slot accessor when
slotvalue
is specified, or a valid slot name for the class, whenslotvalue
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 standardclass specifier. Otherwise, an error of type UNIFICATIONFAILURE 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 SLOTVALUE.
If all the (recursive) calls to UNIFY succeed, then a possibly augmented substitution is returned. Otherwise, an error of type UNIFICATIONFAILURE is signaled.
Affected By:
None.
Exceptional Situations:
If object1 and object2 cannot be unified, then an error of type UNIFICATIONFAILURE is signaled.
See Also:
MAKEEMPTYENVIRONMENT, UNIFICATIONFAILURE, *UNIFYSTRINGCASESENSITIVEP*, OCCURSINP, *OCCURENCECHECKP*.
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 258282.