# Can someone clarify this unification algorithm?

I've been having trouble understanding a unification algorithm for first order logic, as I don't know what a compound expression is. I googled it, but found nothing relevant. I also don't know what a list means in this context. A list of what?

Edit: I think I've cleared up with compound expressions are and what lists contain in this context, from Yuval Filmus's answer. However, now I have other problems:

• In Unify-Var, it uses the variable(?) val, even though val was never declared. Could {var/val} E theta (with E meaning is a subset of) instead be a function that returns whether var is already in theta, regardless of what value it's mapped to?
• The algorithm seems to break when unifying compound expressions. To unify them, it breaks compound expressions into two lists: one for function symbols and one for arguments and then calls Unify on both individually. When trying to unify the list of function symbols, it breaks the list into individual function symbols and then calls Unify on each individual function symbol. But Unify has no case to deal with function symbols, so it just returns failure, even if the two function symbols to be unified are identical!

Thanks.

Pseudocode from Artificial Intelligence A Modern Approach (3rd Edition): Figure 9.1, page 328:

function UNIFY(x, y, theta) returns a substitution to make x and y identical
inputs: x, a variable, constant, list, or compound expression
y, a variable, constant, list, or compound expression
theta, the substitution built up so far (optional, defaults to empty)

if theta = failure then return failure
else if x = y the return theta
else if VARIABLE?(x) then return UNIFY-VAR(x, y, theta)
else if VARIABLE?(y) then return UNIFY-VAR(y, x, theta)
else if COMPOUND?(x) and COMPOUND?(y) then
return UNIFY(x.ARGS, y.ARGS, UNIFY(x.OP, y.OP, theta))
else if LIST?(x) and LIST?(y) then
return UNIFY(x.REST, y.REST, UNIFY(x.FIRST, y.FIRST, theta))
else return failure

---------------------------------------------------------------------------------------------------

function UNIFY-VAR(var, x, theta) returns a substitution

if {var/val} E theta then return UNIFY(val, x, theta)
else if {x/val} E theta then return UNIFY(var, val, theta)
else if OCCUR-CHECK?(var, x) then return failure
else return add {var/x} to theta


Figure 9.1 The unification algorithm. The algorithm works by comparing the structures of the inputs, elements by element. The substitution theta that is the argument to UNIFY is built up along the way and is used to make sure that later comparisons are consistent with bindings that were established earlier. In a compound expression, such as F(A, B), the OP field picks out the function symbol F and the ARGS field picks out the argument list (A, B).

• I answered your further questions in comments to my answer. But I really feel that this information appears in the textbook somewhere, perhaps in earlier chapters. Finally, it would probably be better if you could talk to peers, TAs or the helpdesk, or consult a different textbook, since explaining every line of code is probably out of scope here. – Yuval Filmus Dec 14 '14 at 19:49
• @YuvalFilmus This is my second time reading the textbook and I already read ahead again after I got stuck. What's a TA? I couldn't find a help desk for Artificial Intelligence: A Modern Approach nor do I have any peers, as I'm not taking a course that uses the book. – Kelmikra Dec 14 '14 at 20:25
• TA=Teaching Assistant – babou Dec 16 '14 at 1:40

First, unification algorithms are tricky. Studying other textbooks will help.

Second, things will probably get clearer if you look at actual code implementations. Have a look at the online code repository for your textbook. The code in Lisp, for example, is here.

A helpful note to remember when looking at first-order unification algorithms is that function symbols and predicates must match exactly in order to be correct.

• (Where is val declared?) This is a notational trick in the pseudocode that creates more confusion than good. It hearkens back to the old days of Lisp association lists. Maybe giving an example of theta would help: ((x 1) (y 2) (z 3)). This means x is bound to 1, y is bound to 2, and z is bound to 3. So var/val refers to a pair in theta like (x 1). So the first clause in UNIFY-VAR means, "if the pair (var val) is a member of theta, then return the result of doing UNIFY on whatever val is in that pair, with x and theta".
• (How do function symbols get unified?) Remember that function symbols must match exactly as I pointed out above. So actually the clause else if x = y then return theta covers this. This is via a recursive call through an outer COMPOUND case.
• Can you clarify a little bit more in how the function symbols get unified? – novalain Mar 31 '16 at 15:23

# This algorithm presentation is indeed pedagogically unclear.

I will not repeat here the previous contributions. However, I believe some points need clarification. Sorry if some of it is a bit subtle: this program is far from being pedagogically written. I am thinking in particular of the presentation of the function UNIFY-VAR which is analyzed below.

First one should note that we have two languages here, both with variables and constants, which may lead to much confusion if one is not very careful in the terminology. Hence my somewhat verbose presentation:

• the object language defining the expressions being unified

• the programming language which is a meta-language for the object language, and in which the unification algorithm is expressed.

## Regarding the object language

Apparently the OP could not find in his book the definition of the object language, and hence did not know what a compound expression may be. I do not have the book to check and can only guess. But it is quite abnormal to give a unification algorithm without a reference to a precise definition and terminology of the object language in which unification is defined. There are many such object languages, and unification may depend on them and their properties.

In this case my guess is that compound expression stands for an expression composed of an operator and its operands. So if the metavariable x has a compound expression as value, then x.OP is the operator while x.ARGS is the list of its arguments.

But then we do not see anywhere what unifies operators. The explanation is probably, as indicated by Yval Filmus in a comment, that operators are treated as constant. Actually, as far as I know, the habit is more to say that constants are operators without arguments. But indeed, both can be treated in the same way. But again, being explicit about it would not hurt the pedagogy, since few students are used to treat the + symbols as a constant, for example.

To conclude, the object language is just a language composed of expressions, where an expression is either an atomic expression, i.e. a constant or a variable, or a compound expression that applies an operator (given by its name) to a list of arguments which are expressions.

The name compound expression is in this context opposed to atomic expression. The former has to be decomposed for unification, while the latter cannot be decomposed.

## About the function function UNIFY-VAR(var, x, theta) returns a substitution

First note that the value of the argument var is always an object variable, while the value of x is always an object expression (which could be reduced to a variable).

The use of if {var/val} E theta here is a strange thing to do when describing a unification algorithm for the object language, since it is implicitly using unification at the programming language level, and in a strange way.

In the pair {var/val}

• var stands for the value of the meta-variable (i.e. programming language variable) var, i.e. for the object variable passed as argument. This object variable is a constant from the meta point of view of the programming language.

• val stands for itself, as a meta-variable: it was not assigned any value, and thus can hardly be expected to stand for its value.

• the pair {var/val} is just a meta compound expression, a construction, involving the pair operator, a constant (the value of var), and the variable val, at the meta level of the programming language.

The use of if {var/val} E theta then do X is actually intended to say, but at the meta level:

if the meta expression {[var]/val} unifies with an element of theta , then do X.

where I insist again with the notation [var] that the variable var is replaced by its value, while val is not (and acts somewhat as what Prolog calls a logical variable).

Furthermore it does have a side effect: when the unification succeeds, then the variable val takes the value of the second component of the substitution pair with whch it actually unified. And this value is to be used in whatever is to be done, in this case return UNIFY(val, x, theta).

So this is not at all trivial. Furthermore, it is pedagogically unwise (to understate it), when teaching beginners, since it is using unification at the programming level to define unification at the object level.

Note that is no unification succeeds in the above test, the variable val remains undefined. Then the next test if {x/val} E theta then ... is again a unification, slightly more complex, since the meta variable x is not necessarily a variable, though it will unify only if it is one.

In the last line the construction {var/x} is used again, but in this case, both variables stand for their values.

So again, reading this piece of programming is a bit subtle, at least for a beginner. It do not mean it is nad programming, only that it mixes too many concepts and levels from a pedagogical point of view.

## Occur-check

Finally, I do hope you understand what the call to OCCUR-CHECK? is supposed to do, because it is an essential part of the algorithm.

Essentially it is suppose to verify that when you try to unify a variable with an expression that the variable does not appear in the expression (allowing it would correspond to looping structures that are not usually allowed in the language).

Note that in the call to [OCCUR-CHECK][1]?(var, x) in your program, the meta-variable var is supposed to have as value an object variable, and the meta-variable x is supposed to have as value an object expression, and the function will check that the object variable does not occur in the object expression.

• Thanks for the thorough response. I think I understand it now. Just one issue: you said that the occurs check is essential, but according to the textbook, Prolog omits the occurs check and omitting it almost never causes problems. – Kelmikra Dec 17 '14 at 1:35
• Well, I am not a Prolog specialist. Prolog has a very pragmatic view of some logical problems (occur-check is not the only one), and experienced Prolog programmers know how to deal with them. Not doing the occur-check may have sense, but you are then no longer in a world of expressions that can be represented by trees, but in a more complex universe with looping structures. The unification of a variable with and expression that contains it amounts to saying that the expression is a subexpression of itself where the variable occurs. This can make sense, but has to be properly formalized. – babou Dec 17 '14 at 2:01
• @Kyth'Py1k It may well be that for a lot of simpler programs, and some care, you do not run too much in this problem. But if you run nto it, you have a buggy program. However, saying more about it requires more experience than I have with Prolog. My remark was only that within the pure logic framework you seem to be considering, you should be careful with occur-check. Also, if future work leads you to skip it, you should make sure you understand well the implications. Unification is only a form of equation solving in specific domains. You are now using one. You may have to consider variations. – babou Dec 17 '14 at 2:10
• @Kyth'Py1k You can do a bit of research on occur-check on the web. Here is one document I found which holds a discussion by expert people (several have very high reputation as scientists): dtai.cs.kuleuven.be/projects/ALP/newsletter/archive_93_96/net/… . You may also want to look at rational trees unification. But this is probably beyong the curriculum of your class. – babou Dec 17 '14 at 12:32

Reading the code, a compound expression is a function call such as UNIFY(x, y, theta). It has an OP part, in this case UNIFY, and an ARGS part, in this case the list x, y, theta. Compound expressions can be nested or appear within other structures (such as lists). They can also appear in infix notation: 1 + 2.

A list is a primitive data structure, which decomposes into its head (first element) FIRST and the rest of the list REST. According to the code, the empty list isn't considered a list but rather a constant. If we want, we can represent lists using angular brackets: [1,2,3]. We have [1,2,3].FIRST = 1, [1,2,3].REST = [2,3], [2,3].FIRST = 2, [2,3].REST = [3], [3].FIRST = 3, [3].REST = [], where [] is apparently a constant. Lists can be nested: [1,[2,3],4]. They can also appear inside compound expressions, or appear as arguments to compound expressions.

The members of a list have arbitrary type, at least as far as this code is concerned. They could contain constants, variables, other lists, and compound expressions.

• Ok, but the algorithm still seems to make no sense. In Unify-Var, it uses the variable(?) val, even though val was never declared. Could {var/val} E theta (with E meaning is a subset of) instead be a function that returns whether var is already in theta, regardless of what value it's mapped to? – Kelmikra Dec 14 '14 at 18:47
• @Kyth'Py1k I have no idea. You have access to the textbook. I'm sure they explain the algorithm and their notation, hopefully through examples. If you have complaints maybe you should aim them at the authors. – Yuval Filmus Dec 14 '14 at 18:51
• No, unless I missed it, the book never mentions what val means. – Kelmikra Dec 14 '14 at 19:05
• Regardless, I still have other issues. The algorithm seems to break when unifying compound expressions. To unify them, it breaks compound expressions into two lists: one for function symbols and one for arguments and then calls Unify on both individually. When trying to unify the list of function symbols, it breaks the list into individual function symbols and then calls Unify on each individual function symbol. But Unify has no case to deal with function symbols, so it just returns failure, even if the two function symbols to be unified are identical! – Kelmikra Dec 14 '14 at 19:11
• @ Yuval Filmus What makes you think that a compound expression is a function call? First off, first order logic is a "declarative" language, so it can't be a literal function call. Also, the description of the algorithm gave F(A,B) as an example of a compound expression, but never actually defined it. – Kelmikra Dec 14 '14 at 19:25