# 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].

#### concatenation

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

conc(PREFIX, SUFFIX, RESULT)

- 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()

def conc(PREFIX, SUFFIX, RESULT):

HEAD, TAIL, CONC = unify.variable('HEAD', 'TAIL', 'CONC')

with unify:

unify(PREFIX, EMPTY) and unify(SUFFIX, RESULT)

yield

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'):

print(unify['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):

print(unify['SUFFIX'])

>>>

(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'])

print()

>>>

PREFIX = ()

SUFFIX = RESULT

RESULT = RESULT

PREFIX = ('HEAD_18', ())

SUFFIX = CONC_18

RESULT = ('HEAD_18', 'CONC_18')

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

SUFFIX = CONC_19

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

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

SUFFIX = CONC_20

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

...

https://github.com/coells/100days

https://notebooks.azure.com/coells/libraries/100days

#### algorithm

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

self.checkpoint[-1].append(var_x)

return True

# unify free variable Y

if isinstance(var_y, str):

self.reference[var_y] = var_x

self.checkpoint[-1].append(var_y)

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

self.checkpoint.append([])

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