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

----

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.

StackExchange Computer Science Q#35280, answer score: 5