Those with even a passing familiarity with Prolog should recognise statements like
[H|T] = [1,2,3]. In particular,
= here is not “is equal to” but rather “unifies with”. So that statement causes the variable
H to unify with
T with the rest of the list,
Clojure’s abstract bindings provide much the same capability –
(let [[h & t] '(1 2 3)] <do stuff>) – modulo the difference between pattern matching and unification, of course.
There’s a subtlety in something like
[H|T] = [1,2,3], at least, if your lists aren’t built of nested cons cells. Consider Smalltalk arrays. Suppose we have some
ListUnifier that will rip a
SequenceableCollection‘s head off, like
#(1 2 3). We’d like the tail to unify with
#(2 3) in other words. But that’s not a node in the original structure – it’s an entirely artificial node we wish to construct from the original collection. Firstly, how can we unify with only part of a structure and, secondly, how can we determine a solution from that partition?
Let’s try model the parts:
Then we can write the original Prolog statement as
As mentioned above, first we want to be able to construct an equivalence relation on the above (or, expressed differently, partition the set of nodes in the structure together with the artificial nodes we create) such that
#x asVariable and
1 are in the same class, and ditto for
#y asVariable and
The mild complication around
head isCollection lets us support a head that is itself a collection. So let’s check that we can construct a partition using parts of things:
We see that the partition that originally would only hold nodes in the structures may now hold parts of the original structure.
The original algorithm for determining the most general unifier from some partition as described in Baader & Snyder (pp. 461-462) runs the solution finder starting from the left operand in the unification. Consider the partition we have above. What elements are in the equivalence class of
ListUnifier? Well, just the
ListUnifier itself! Clearly we need to adjust the solution finder a bit. The obvious approach would be to start the solution-finding from an element in each class, and merge the partial solutions:
#addAll: merges the various
MostGeneralUnifiers generated and
#inject:into: folds over the representative node in each equivalence class. (Remember, a union-find always has a representative for each equivalence class, namely,
myPartition find: someObject.) And it works, at the cost of turning a linear algorithm into a (worst case) quadratic one:
But “finding a solution” really means “to what must we assign each variable?”. So we can at least speed things up by only solution-finding in those classes in which variables occur:
This makes finding a solution O(NM), where N is the number of nodes in the structure, M the number of classes containing variables.