Can someone clarify this unification algorithm?

Problem Detail: 

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

Asked By : Kelmikra

Answered By : ShyPerson

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/35280