Day 77: Unification

For today I have something really cool. It’s a unification process and it will allow me to write a mind-bending function. If you have programmed in Prolog before, you know where I am heading, right?

But first, what is unification? It is similar to equality, but it is a much deeper concept and I will be a little bit formal, now.

Equality says that two objects X and Y are equal, X=Y, if and only if they both belong to the same equality class E. Or should I say, equality is a property of an object X and means X belongs to class E.

Unification, on the other hand, says that two objects X and Y are unified, X=Y, if and only if they both represent the same entity.

In advance, unification brings a concept of free and bound variables. Free variable can be always unified [even to self] and bound variable can be unified only if its bound value can be unified.

It’s probably easier to show some examples. X and Y denote free variables.

1 = 1    # unifiable
1 = 2 # not unifiable
X = 1, Y = 1, X = Y    # unifiable
X = 1, Y = 2, X = Y # not unifiable
(X, Y) = (1, (2, 3))   # unifiable for X=1, Y=(2,3)
X = (1, X)    # tricky one...

For my purpose, I will only support these Python types:

  • integer — represents atomic value
  • string — represents variable
  • tuple — represents compound structure

I will also represent lists using nested tuples, e.g. (1, (2, (3, tuple()))) is a list of values [1, 2, 3].


Now I can implement a function to concatenate two lists using recursive definition.


  • if PREFIX is empty, SUFFIX is RESULT
  • otherwise RESULT is the head of PREFIX followed by concatenation of PREFIX tail with SUFFIX
unify = Unify()
EMPTY = tuple()
HEAD, TAIL, CONC = unify.variable('HEAD', 'TAIL', 'CONC')
    with unify:
unify(PREFIX, EMPTY) and unify(SUFFIX, RESULT)
    with unify:
unify(PREFIX, (HEAD, TAIL)) and unify(RESULT, (HEAD, CONC))
yield from conc(TAIL, SUFFIX, CONC)

Let’s give it a try. Remember that string represents a free variable.

prefix = (1, (2, EMPTY))
suffix = (3, (4, EMPTY))
for _ in conc(prefix, suffix, 'RESULT'):
(1, (2, (3, (4, ()))))

Sooo… I have written 100+ lines to just append one list to another? In which way is this cool?

What about this one.

prefix = (1, (2, EMPTY))
result = (1, (2, (3, (4, EMPTY))))
for _ in conc(prefix, 'SUFFIX', result):
(3, (4, ()))

I asked what do I need to append to [1, 2] to get [1, 2, 3, 4] and the same function gave me an answer [3, 4]!

What about something even more cool?

result = (1, (2, (3, (4, EMPTY))))
for _ in conc('PREFIX', 'SUFFIX', result):
print('possible answer is', unify['PREFIX'],
'and', unify['SUFFIX'])
possible answer is () and (1, (2, (3, (4, ()))))
possible answer is (1, ()) and (2, (3, (4, ())))
possible answer is (1, (2, ())) and (3, (4, ()))
possible answer is (1, (2, (3, ()))) and (4, ())
possible answer is (1, (2, (3, (4, ())))) and ()

I only know the result is [1, 2, 3, 4], what did I concatenated? And it gave me all the possible answers!

And here’s the killer.

If I don’t know neither prefix nor suffix nor result, the answer is rather intriguing. I get all the possible lists… until stack overflow stops the fun.

for _ in conc('PREFIX', 'SUFFIX', 'RESULT'):
print('PREFIX =', unify['PREFIX'])
print('SUFFIX =', unify['SUFFIX'])
print('RESULT =', unify['RESULT'])

PREFIX = ('HEAD_18', ())
RESULT = ('HEAD_18', 'CONC_18')

PREFIX = ('HEAD_18', ('HEAD_19', ()))
RESULT = ('HEAD_18', ('HEAD_19', 'CONC_19'))

PREFIX = ('HEAD_18', ('HEAD_19', ('HEAD_20', ())))
RESULT = ('HEAD_18', ('HEAD_19', ('HEAD_20', 'CONC_20')))


class Unify:

def __init__(self):
self.reference = {} # variable bindings
self.checkpoint = [] # unification checkpoints
self.var_ctx = 0 # unique variable id
    def variable(self, *args):
self.var_ctx += 1
return ['%s_%d' % (var, self.var_ctx) for var in args]
    def __call__(self, var_x, var_y):
# resolve variable X
while isinstance(var_x, str) and var_x in self.reference:
var_x = self.reference[var_x]
        # resolve variable Y
while isinstance(var_y, str) and var_y in self.reference:
var_y = self.reference[var_y]
        # unified to self?
if isinstance(var_x, str) and isinstance(var_y, str):
if var_x == var_y:
return True
        # unify free variable X
if isinstance(var_x, str):
self.reference[var_x] = var_y
return True
        # unify free variable Y
if isinstance(var_y, str):
self.reference[var_y] = var_x
return True
        # tuple is unified element-wise
if isinstance(var_x, tuple) and isinstance(var_y, tuple):
if len(var_x) == len(var_y):
return all(self(i, j) for i, j in zip(var_x, var_y))
        # atom is unified on equality
if isinstance(var_x, int) and isinstance(var_y, int):
if var_x == var_y:
return True
        # not unifiable
raise KeyError()
    def __getitem__(self, var):
# resolve tuple by members
if isinstance(var, tuple):
return tuple(self[i] for i in var)
        # resolve variable recursively
if isinstance(var, str):
if var in self.reference:
return self[self.reference[var]]
return var
        # atomic value
if isinstance(var, int):
return var
        # invalid object
raise TypeError()
    def __enter__(self):
# store unification checkpoint
    def __exit__(self, exc_type, *args):
# remove checkpoint and unbind variables
for var in self.checkpoint.pop():
if var in self.reference:
del self.reference[var]
        # suppress exception
if exc_type is not GeneratorExit:
return True
One clap, two clap, three clap, forty?

By clapping more or less, you can signal to us which stories really stand out.