Thursday, January 31, 2008

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.














17 comments:

ido said...

I think you forgot the line:

a = mg.constant("a")

In your example.

Filox said...

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

ido said...

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)"?

Filox said...

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.

Filox said...

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

ido said...

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

Filox said...

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

stefan.ciobaca said...

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:

Filox said...

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)

stefan.ciobaca said...

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?

Filox said...

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.

stefan.ciobaca said...

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

stefan.ciobaca said...

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.

Filox said...

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?

stefan.ciobaca said...

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.

stefan.ciobaca said...

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.

Rohit said...

No..I think its broken. It performs something without giving an error.
Seems like you don't have occur check in your code.