# 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    # unifiable1 = 2    # not unifiable`
`X = 1, Y = 1, X = Y    # unifiableX = 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?

`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 = RESULTRESULT = RESULTPREFIX = ('HEAD_18', ())SUFFIX = CONC_18RESULT = ('HEAD_18', 'CONC_18')PREFIX = ('HEAD_18', ('HEAD_19', ()))SUFFIX = CONC_19RESULT = ('HEAD_18', ('HEAD_19', 'CONC_19'))PREFIX = ('HEAD_18', ('HEAD_19', ('HEAD_20', ())))SUFFIX = CONC_20RESULT = ('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`
One clap, two clap, three clap, forty?

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