Quelqu'un peut-il clarifier cet algorithme d'unification?

Question

J'ai eu du mal à comprendre un algorithme d'unification pour la logique du premier ordre, car je ne sais pas ce qu'est une expression composée. Je l'ai googlé, mais je n'ai trouvé rien de pertinent. Je ne sais pas non plus ce que signifie une liste dans ce contexte. Une liste de quoi?

Edit: Je pense que je me suis effacé avec les expressions composées et ce que les listes contiennent dans ce contexte, à partir de la réponse de Yuval Filmus. Cependant, maintenant j'ai d'autres problèmes:

• Dans Unify-Var, il utilise la variable (?) Val, même si Val n'a jamais été déclaré. Le thêta pourrait-il {var / val} e (avec la signification e est un sous-ensemble de) une fonction qui renvoie si VAR est déjà dans Theta, quelle que soit la valeur à laquelle il est mappé?
• L'algorithme semble se casser lors de l'unification des expressions composées. Pour les unifier, il divise les expressions composées en deux listes: une pour les symboles de fonction et un pour les arguments, puis appelle Unify sur les deux individuellement. Lorsque vous essayez d'unifier la liste des symboles de fonction, il divise la liste en symboles de fonction individuels, puis appelle Unify sur chaque symbole de fonction individuelle. Mais Unify n'a pas de cas pour gérer les symboles de fonction, donc il renvoie simplement l'échec, même si les deux symboles de fonction à unifiés sont identiques!

Merci.

Pseudocode de l'intelligence artificielle Une approche moderne (3e édition): 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 L'algorithme d'unification. L'algorithme fonctionne en comparant les structures des entrées, éléments par élément. La substitution thêta qui est l'argument à unifier est construite en cours de route et est utilisée pour s'assurer que les comparaisons ultérieures sont cohérentes avec les liaisons qui ont été établies plus tôt. Dans une expression composée, telle que F (A, B), le champ OP choisit le symbole de fonction F et le champ Args choisit la liste des arguments (A, B).