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.

## 17 comments:

I think you forgot the line:

a = mg.constant("a")

In your example.

So I did, thanks! I've corrected that now. I've also put a new version of the file for download (the old one had a bug in it).

I've played with your code a bit more today and have two additional remarks:

1. If I change the the first expression to be

"not P(f(a), g(y), f(w))"by setting"expr1 = [not P, [f, a], [g, y], [f, w]]", I'd expect the most general unifier to remain the same, while the expression after applying the unifier to change to something like"uni(expr1)=[Not P, [f, a], [g, [f, [f, a]]], [f, [f, a]]]".You code sets uni(expr1) in that case to

"[False, [f, a], [g, [f, [f, a]]], [f, [f, a]]]", which I'm guessing was not your intention.2. How can I represent an expression with more than one predicate, E.g.

"P(f(a), g(y), f(w)) AND Q(x)"?Well, both of your remarks are actually a specific case of a more general problem -- can the unifying algorithm unify expressions that contain logical operators? As it turns out, this algorithm is not designed to solve that problem. Unification is supposed to work only on expressions that contain predicates, variables, constants, or functions, not logical operators. See for example, http://mathworld.wolfram.com/Unification.html or http://ale.cs.toronto.edu/docs/ref/ale_trale_ref/ale_trale_ref-node4.html

Also, if you try to unify something like P(y) AND Q(x) with P(a) AND Q(b) in a language like Prolog (which is based on unification) you'll see that there is no way to do this.

Yeah, you should also check out the Wikipedia article about unification:

http://en.wikipedia.org/wiki/Unification

Hope this helps

(there is still one more bug in the program, which I'll fix when I find some time. The problem is that unifying two expressions of unequal length should throw an error, which it doesn't, e.g., try to unify P(a, b) and P(a) ).

You are right, my understanding of the unification algorithm was lacking.

Maybe I could fix that bug myself sometime soon, if I do I could send you the modifications (in case you haven't done it yourself in the meanwhile).

Hey, if you want to, feel free to send me the fix. It would be something in the line of:

if not k1 or not k2:

if k1 or k2:

return error("The expressions are not of equal length!")

else:

return supstitution()

That's just of the top of my head, I haven't tested it. If you feel like it, you can test this change and tell me if it works...

Your implementation is totally incorrect.

>>> uni = mg.mgUnifier(x, y)

Traceback (most recent call last):

File "mgunifier.py", line 174, in mgUnifier

if k1 in k2:

Stefan, I've fixed the problem with unifying two variables (it was just a matter of adding an __iter__ method to variable class -- I'd hardly say my implementation is totally incorrect)

Sorry, it still doesn't work properly:

mg.mgUnifier([g, [f, x, y], [f, y, x]], [g, [f, z, z], z])

yields a run-time error.

Also, as a general remark, why do you differentiate between predicates and functions?

Well, I've fixed your problem, although there are bound to be other bugs in the code...

The difference between functions and predicates is there simply because there is a difference between the two in logic in general. In this particular algorithm, there is no obvious difference between them and I could've used just one to represent both. In general, AFAIK, predicates evaluate to true or false whereas functions can have arbitrary codomains.

I take it you haven't uploaded the new code?

Sorry about the previous comment, your file ends in .PY instead of .py and I accidentally loaded the old file.

[quote]Well, I've fixed your problem, although there are bound to be other bugs in the code...[/quote]

Not my code => not my problem.

Try this one:

mg.mgUnifier([g, [f, z, z], z], [g, [f, x, y], [f, y, x]])

{(x/z), (y/[f, y, y]), ([f, y, y]/x)}

First of all, the two expressions are not unifiable, and second, the "substitution" you output is not really what you want.

Your point was to illustrate how python reads nicely, but if it's that easy to create wrong code, it doesn't serve your point well.

The first thing to correct in your code is to drop the difference between predicates and functions, as this will eliminate code paths that currently must be simply duplicates of one another.

[quote]The difference between functions and predicates is there simply because there is a difference between the two in logic in general.[/quote]

Not good enough of a reason to duplicate code. You can still make the difference between them externally, but make sure you have the same code for both.

[quote]In this particular algorithm, there is no obvious difference between them and I could've used just one to represent both.[/quote]

Correct.

Sorry, but the example you give works as it should. Running mg.mgUnifier([g, [f, z, z], z], [g, [f, x, y], [f, y, x]])

gives an error, as it is supposed to. Maybe you're still using the old version?

And no, the difference between predicates and functions is not a problem and there is no code duplication because of existence of both of them. Can you point the piece of code you think is a duplicate?

Yes, I think I have the latest version. Did you actually try the example? Python version?

This is a direct copy from my terminal:

stefan@stefan-laptop:~/tmp$ ls *.py*

mgunifier.py

stefan@stefan-laptop:~/tmp$ python

Python 2.5.2 (r252:60911, Jul 31 2008, 17:28:52)

[GCC 4.2.3 (Ubuntu 4.2.3-2ubuntu7)] on linux2

Type "help", "copyright", "credits" or "license" for more information.

>>> import mgunifier as mg

>>> f = mg.function("f")

>>> g = mg.function("g")

>>> x = mg.variable("x")

>>> y = mg.variable("y")

>>> z = mg.variable("z")

>>> mg.mgUnifier([g, [f, z, z], z], [g, [f, x, y], [f, y, x]])

{(x/z), (y/[f, y, y]), ([f, y, y]/x)}

>>> mg.mgUnifier([g, [f, x, y], [f, y, x]], [g, [f, z, z], z])error: z in [f, z, z]

>>>

stefan@stefan-laptop:~/tmp$ md5sum mgunifier.py

b570185760c69121eaea0f5072b524c5 mgunifier.py

I didn't look at the code (yet), but I'll take a look now.

I've taken a look at your code, and I think it's totally broken.

The main problem I see is that when you call alpha(beta) you need to recursively call mgUnifier.

For example, imagine

alpha = f(a,b)/x

beta = f(y,b)/x

when you do the merging of the two substitutions you'd need to recursively call mgunifier again...

But I think it's safer to just implement the standard mgu algorithm.

No..I think its broken. It performs something without giving an error.

Seems like you don't have occur check in your code.

Post a Comment