Qual è l'ottimale “più generale unificatore” algoritmo?

Question

La questione

Qual è l'algoritmo di MGU più efficiente? Qual è la sua complessità temporale? E 'abbastanza semplice da descrivere come una risposta di overflow dello stack?

Ho cercato di trovare la risposta su Google, ma continuare a trovare .PDFs private che posso solo l'accesso tramite un abbonamento ACM.

Ho trovato una discussione in SICP: qui

Spiegazione di ciò che un "algoritmo di unificazione più generale" è il seguente: Prendere due alberi di espressione contenente "variabili libere" e "costanti" ... per esempio.

 e1 = (+ x? (* y? 3) 5)
 e2 = (+ z? q? r?)

Poi l'algoritmo più generale Unificatore restituisce l'insieme più generale di attacchi che rende le due espressioni equivalenti.

cioè.

mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5

Con "più in generale", si potrebbe invece bind (x = 1) e (z = 1) e che avrebbe anche fare E1 ed E2 equivalente ma sarebbe più specifico.

L'articolo SICP sembra implicare che è ragionevolmente costoso.

Per info, il motivo che mi chiedo è perché so che l'inferenza dei tipi coinvolge anche questo algoritmo "unificazione" e mi piacerebbe capirlo.

Answer 1

La semplice algoritmo che viene utilizzato nella pratica (per esempio in Prolog) è esponenziale per casi patologici.

C'è un algoritmo teoricamente più efficiente Martelli e Montanari (IIRC è lineare), ma è molto più lento per i semplici casi che si verificano in pratica, quindi non è molto usato.

Answer 2

Baader e Snyder pubblicato diversi algoritmi di unificazione, sia sintattico unificazione e l'unificazione equazionali.

Essi affermano che il loro terzo algoritmo unificazione sintattica (nella sezione 2.3) viene eseguito in O (n alfa (n)) dove alfa (n) è la funzione di Ackermann inversa -. In situazioni pratiche è equivalente a una piccola costante