Can someone clarify this unification algorithm?

Question

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

Answer 1

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.

On to your questions.

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

Answer 2

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.

Answer 3

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.