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

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top