Unifying expressions in Python

Most of you that had some AI course in college probably heard of unification of expressions. All of you who ever programmed (and I use the term loosly) in Prolog know what this is. For all others, just a note that I'm not going to explain here what is unification and how it's done. If you don't know what it is, check out, for example this WP article.
Here we can see the algorithm for finding the most general unifier of two expressions in pseudo-code (check out the bottom of the page). And here is my implementation of unifying expressions in Python. I'm not going to explain the code here---if you're interested, you can do this yourself. I'll just give a brief example of how you can use this. So, suppose that you have the following two expressions:
expr1 = P(f(a), g(y), f(w))
and
expr2 = P(x, g(f(x)), y),
where P is a predicate, g and f are functions, and x, y and w are variables (this is an actual assignment from a test we gave our students some two months ago). Lets solve this using Python:

import mgunifier as mg    # just to make the listing shorter

# declare predicates, functions, and variables
P = mg.predicate("P")
g = mg.function("g")
f = mg.function("f")
x = mg.variable("x")
y = mg.variable("y")
w = mg.variable("w")
a = mg.constant("a")

expr1 = [P, [f, a], [g, y], [f, w]]
expr2 = [P, x, [g, [f, x]], y]
uni = mg.mgUnifier(expr1, expr2)     # find the most general unifier
new1 = uni(expr1)
new2 = uni(expr2)
print "The most general unifier is ", uni
# check if the two expressions are the same after unification
print new1
print new2

That's all there is to it. If someone has an idea on how to make things more simple or improve the code in any way, I am always glad to hear from you. Now, those of you that had some experience with Prolog probably know that, although unification is the most basic tool of this language, there's a little bug/wart when using it (this applies to SWI Prolog implementation, I don't know how others handle it). Typing, for example,

?- X = f(X).

results in X = f(**), meaning that variable X is now f(f(f(f(...)))). This is, of course, wrong, because the left and the right side of the equal sign will never be the same (and if you don't believe me, check out the algorithm). Why exactly is Prolog doing this is beyond me. Anyway, try the following code:

import mgunifier as mg

P = mg.predicate("P")
g = mg.function("g")
f = mg.function("f")
x = mg.variable("x")
y = mg.variable("y")
w = mg.variable("w")
a = mg.constant("a")

first = [P, x, [g, y], z]
second = [P, [f, a], z, y]
uni = mg.mgUnifier(first, second)
print uni

Not only that you get an error, but you can also see exactly where the algorithm failed.
Now, what's the whole point of this post? To demonstrate some Python implementation of an algorithm no one cares about? Well, partially. I was looking through the web for something similar and found only this. As it didn't satisfy me, I wrote my own program that unifies expressions, so anyone looking for something like this doesn't have to. But, what I'd really like people to see (and read) is this (copy-paste from the source):

def mgUnifier(k1, k2):
    """Return the most general unifier of two expressions k1 and k2."""
    
    if not k1 or not k2: return supstitution()
    if isinstance(k1, (constant, variable, function, predicate)) or isinstance(k2, (constant, variable, function, predicate)):
        if k1 == k2:
            return supstitution()
        if isinstance(k1, variable):
            if k1 in k2:
                return error(`k1` + " in " + `k2`)
            else:
                return supstitution(k2, k1)
        if isinstance(k2, variable):
            if k2 in k1:
                return error(`k2` + " in " + `k1`)
            else:
                return supstitution(k1, k2)
        if not isinstance(k1, variable) and not isinstance(k2, variable):
            return error(`k1` + " and " + `k2` + " cannot be unified!")

    alpha = mgUnifier(head(k1), head(k2))
    if isinstance(alpha, error):
        return alpha
    k3 = alpha(tail(k1))
    k4 = alpha(tail(k2))
    beta = mgUnifier(k3, k4)
    if isinstance(beta, error):
        return beta
    return alpha(beta)

This beautifully (IMHO) demonstrates the power and clarity of Python. Compare this code to the algorithm pseudo-code---it's almost the same. This is what I love about Python---I can simply copy the algorithm's pseudo-code and then just implement the "magic" that happens in the background.
Like I said, the purpose of this program is primarly educational, the code could probably be better written, but I stuck with the implementation that was most similar to the algorithm. Keeping that in mind, I appreciate any feedback on the code.