Languages like ML, Newspeak, and Scala support pattern matching: it’s a bit like a case/switch statement, only instead of matching on a series of boolean conditions you switch on the *shape* of some variable. But Prolog goes twice as far: Prolog uses *unification*. What’s that, you ask?

In a nutshell, unification is *bidirectional* pattern matching. For instance, when you say `X = 1`

in Prolog you are not assigning the value of `1`

to a variable `X`

. No, no, no! You are saying “to what do I need to map `X`

so that the left and right sides have the same value?” “Huh?” you ask? Well, consider this: `f(x, A) = f(B, y)`

. To what must we map variables `A`

and `B`

so that the two sides have the same value? Clearly `{A -> y, B -> x}`

will do the job. Apply that *unifier* and you turn `f(x, A)`

into `f(x, y)`

and `f(B, y)`

into `f(x, y)`

.

A *most general unifier* or *mgu* is, loosely speaking, that unifier such that any other unifier must consist of the mgu followed by some other substitution. The mgu is also unique, up to variable renaming.

Of course, sometimes there’s no mapping possible: `1 = 2`

will never unify, nor will `f(X) = f(X, Y)`

. (Nor, for that matter, will `X = f(X)`

– there is no value to which you can map X to match both sides.)

Unification’s a really neat part of automated reasoning, discovered/invented first by John Robinson in the paper “A Machine-Oriented Logic Based on the Resolution Principle”. SICP describes a simple recursive descent unification algorithm that works just fine in most cases, but has an exponential time worst case. Gérard Huet (yes, he of zipper fame) came up with a near-linear time algorithm. (To be precise, O(n α(n)), where α(n) is the inverse Ackermann function.) Baader and Snyder have a nice explanation in Chapter 8 of the Handbook of Automated Reasoning. And, of course, we’re going to implement it in Smalltalk.

The general idea is this: given any directed acyclic object graph, we’re going to construct a *term relation* between the nodes of that graph, that is, an equivalence relation that says that nodes within the same equivalence class have been unified. The *unification closure* of two nodes is the least unification relation which makes those nodes equivalent. Once we the term relation is fully defined (if it exists), we extract the most general unifier, and we’re done.

Another piece of machinery we’re going to need is a *schema function* σ from equivalence classes to terms such that for any equivalence class C

- σ(C) ∈ of C; and
- σ(C) is a variable (an instance of MetaVariable) if and only if every element in C is a variable.

We’ll call σ(C) the *schema term* for C.

We’d like to be able to unify arbitrary objects. We don’t want to splatter unification-specific data all over the place, so we will use a Decorator-like pattern to store our data. Some objects contain other objects. To keep things simple, we’ll treat instances of AlgebraicDataTypes specially, and treat everything else as opaque. In other words, we’ll unify sub-parts of AlgebraicDataType instances, but treat other instances as black boxes. (One could also use something like Magritte to provide a uniform way of accessing an instance’s substructures. We’ll save that for another day.) A MetaVariable is something representing a variable: `Leaf value: (MetaVariable named: #x)`

represents a leaf node in a tree containing some unknown value `x`

.

instanceVariableNames: ''.

AlgebraicDataType subclass: #MetaVariable

instanceVariableNames: 'name'.

Object subclass: #UnificationEquivalenceClass

instanceVariableNames: 'classPointer classSize schemaTerm visited

acyclic vars node'.

Object subclass: #TermRelation

instanceVariableNames: 'map'.

TermRelation >> initialize

super initialize.

map := Dictionary new.

TermRelation >> classFor: anObject

"Lazily decorate anObject."

^ map

at: anObject

ifAbsentPut: [UnificationEquivalenceClass decorate: anObject].

(I should mention that I take liberties with Smalltalk’s syntax in these snippets. I either strip out stuff not necessary to what we’re trying to understand (like all the other stuff that goes into defining a class) or add extra explanatory bits (like adding “`Class >>`

” to the beginning of method names).)

First, our “entry API”, how we call the library.

^ Unifier unify: self with: anObject.

Unifier >> unify: s with: t

termRelation := TermRelation new.

(termRelation classFor: s)

unificationClosureWith: (termRelation classFor: t)

in: termRelation.

^ (termRelation classFor: s)

findSolutionWithUnifier: Dictionary new

in: termRelation.

(Note the lack of “functiony” stuff: I’ve chosen to copy the algorithm quite closely. We’ll be using side effects within UnificationEquivalenceClass and TermRelation, but from an outsider’s perspective unification will still look like a purely functional calculation.)

The term relation is initially the identity relation. If the member of the equivalence class is a variable (a MetaVariable, in our terminology), then the set of variables associated with that class (i.e., those variables that will be mapped to this class) is that variable; otherwise, the set of variables is the empty set.

self node: aNode.

vars := aNode isMetaVariable

ifTrue: [aNode asOrderedCollection]

ifFalse: [OrderedCollection new].

acyclic := false.

"All nodes start as the sole element in an equivalence class;

this makes each node a representative of its class."

classPointer := self.

schemaTerm := self.

classSize := 1.

visited := false.

We represent the equivalence class as a tree of classes. Finding the representative means walking up the chain of equivalence classes until we find that object whose `classPointer`

points to itself. As a side effect, we compress the path to the representative. That is, having found the representative, we can save ourselves some effort next time by storing the pointer to the representative directly.

"Walk up the tree representing this equivalence class to find the

representative. As a side effect, compress the path to the representative."

| result |

self isRepresentative ifTrue: [^ self].

result := classPointer findRepresentative.

classPointer := result.

^ result.

Merging two classes s and t is as simple as telling all the s_{i} in a class s `classPointer := t`

. One optimisation that we make is that we always merge the smaller equivalence class into the larger class. (`classSize`

helps us decide cheaply.)

"Given myself, a representative, and anEquivClass, another representative,

merge the two equivalence classes by folding the smaller into the larger."

(self classSize <= anEquivClass classSize)

ifFalse: [^ anEquivClass union: self].

classSize := classSize + anEquivClass classSize.

vars addAll: anEquivClass vars.

schemaTerm node isMetaVariable

ifTrue: [schemaTerm := anEquivClass schemaTerm].

anEquivClass classPointer: self.

And now for the meat of the algorithm. We calculate the unification closure between two classes in some term relation by comparing the representatives of the two classes: if they’re the same class, there’s nothing to do. Otherwise, if the schema term of one class is a MetaVariable, we merge the two classes. If neither is a MetaVariable, we compare the structures of the two schema terms.

You’ll also notice some incidental complexity. We have one set of objects – the AlgebraicDataTypes – whose structures we may easily examine, and another set of objects – everything else – for which we may make no assumptions on how to inspect their structures. Thus, we treat the “everything else” objects opaquely. If we wanted to add unification support to Magritte-described objects, we would probably need to use double dispatch on the two schema terms to control the additional complexity.

| left right sTerm t tTerm |

t := rightEquivClass findRepresentative.

self isRepresentative ifFalse: [#

^ self findRepresentative unificationClosureWith: t in: termRelation].

(self = t) ifTrue: [^ self."Nothing to do"].

sTerm := schemaTerm.

tTerm := t schemaTerm.

left := sTerm node.

right := tTerm node.

(left isMetaVariable or: [right isMetaVariable])

ifTrue: [^ self union: t].

"s, t are both terms."

(left isAlgebraic and: [right isAlgebraic])

ifTrue:

["s = f(s1, ..., sm), t = g(t1, ..., tn) where m, n > 0"

(left type = right type)

ifFalse: [UnificationFailure signal. "f ~= g"].

(left arity = right arity)

ifFalse: [UnificationFailure signal. "m ~= n"].

sTerm union: tTerm.

left children with: right children do:

[:si :ti | (termRelation classFor: si)

unificationClosureWith: (termRelation classFor: ti)

in: termRelation]]

ifFalse:

["At least one of s, t are not AlgebraicDataTypes,

but some other kind of value."

(left = right)

ifTrue: [sTerm union: tTerm]

ifFalse: ["s ~= t" UnificationFailure signal]].

Lastly, we extract the most general unifier out of the term relation. Note that we know the mgu exists at this point, because the process of calculating the unification closure would raise a UnificationFailure if it didn’t.

(self isSchemaTerm) ifTrue:

[^ self privFindSolutionWithUnifier: aDictionary in: termRelation]

^ self findRepresentative schemaTerm

findSolutionWithUnifier: aDictionary in: termRelation.

UnificationEquivalenceClass >> privFindSolutionWithUnifier: aDictionary in: termRelation

"Assume that we are the schema term for our equivalence class."

| newUnifier |

acyclic ifTrue: [^aDictionary "s is not part of a cycle."].

visited ifTrue: [UnificationFailure signal. "Cycle detected."].

newUnifier := aDictionary copy.

(node isAlgebraic and: [node hasChildren]) ifTrue:

[visited := true.

node children do:

[:each | | d |

d := (termRelation classFor: each)

findSolutionWithUnifier: newUnifier in: termRelation.

newUnifier addAll: d].

visited := false].

acyclic := true.

self findRepresentative vars do:

[:x | (x ~= node) ifTrue: [newUnifier at: x put: node]].

^ newUnifier.

As always, the code’s on SqueakSource. Fire up your Squeak image, and run the following script, and you’ll be unifying!

project: 'Nutcracker';

install: 'AlgebraicDataType';

install: 'Unification';

install: 'UnificationTests'.

## Comment