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.
Sei a conoscenza di un documento che lo descrive? È fondamentalmente lo stesso descritto in SICP? –
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