2009-05-13 11 views
10

La domandaQual è l'algoritmo "più generale unificatore generale" ottimale?

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

Ho cercato di trovare la risposta su Google ma continuo a trovare file PDF privati ​​a cui posso accedere solo tramite un abbonamento ACM.

ho trovato una discussione in SICP: here

Spiegazione di ciò che un "algoritmo di unificazione più generale" è: Prendete 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 legare (x = 1) e (z = 1) e che avrebbe anche fare E1 ed E2 equivalente ma sarebbe più specifico.

L'articolo della SICP sembra implicare che sia ragionevolmente costoso.

Per informazioni, il motivo per cui lo chiedo è perché so che l'inferenza di tipo coinvolge anche questo algoritmo di "unificazione" e mi piacerebbe capirlo.

risposta

8

L'algoritmo semplice utilizzato in pratica (ad es. In Prolog) è esponenziale per i casi patologici.

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

+0

Sei a conoscenza di un documento che lo descrive? È fondamentalmente lo stesso descritto in SICP? –

+0

Sì, l'algoritmo semplice è essenzialmente lo stesso descritto in SICP. La solita presentazione usa regole come decomposizione, scontro, verifica di verifica, ..., quindi potresti voler cercarlo. – starblue

4

Baader and Snyder ha pubblicato diversi algoritmi di unificazione, sia per l'unificazione sintattica che per l'unificazione equa.

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