Qualcuno può chiarire questo algoritmo di unificazione?

Question

Ho avuto problemi a capire un algoritmo di unificazione per la logica del primo ordine, poiché non so cosa sia un'espressione composta. L'ho cercato su Google, ma non ho trovato nulla di rilevante. Inoltre, non so cosa significhi un elenco in questo contesto. Un elenco di cosa?

EDIT: penso di aver chiarito con le espressioni composte e quali elenchi contengono in questo contesto, dalla risposta di Yuval Filmus. Tuttavia, ora ho altri problemi:

• In Unify-Var, utilizza la variabile (?) Val, anche se Val non è mai stata dichiarata. Potrebbe {var/val} e theta (con il significato di un sottoinsieme) invece essere una funzione che restituisce se var è già in theta, indipendentemente da quale valore è mappato?
• L'algoritmo sembra rompersi quando unificano espressioni composte. Per unificarli, rompe le espressioni composte in due elenchi: uno per i simboli delle funzioni e uno per gli argomenti e quindi chiama Unify su entrambi individualmente. Quando si tenta di unificare l'elenco dei simboli delle funzioni, rompe l'elenco in singoli simboli di funzione e quindi chiama Unify su ogni singolo simbolo della funzione. Ma Unify non ha alcun caso per affrontare i simboli della funzione, quindi restituisce solo un fallimento, anche se i due simboli di funzione da unificare sono identici!

Grazie.

Pseudocodice dall'intelligenza artificiale Un approccio moderno (3a edizione): Figura 9.1, pagina 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

Figura 9.1 L'algoritmo di unificazione. L'algoritmo funziona confrontando le strutture degli ingressi, elementi per elemento. La sostituzione theta che è l'argomento per unificare è costruita lungo la strada e viene utilizzata per assicurarsi che i confronti successivi siano coerenti con i legami stabiliti in precedenza. In un'espressione composta, come F (A, B), il campo OP sceglie il simbolo della funzione F e il campo Args sceglie l'elenco degli argomenti (A, B).