La pregunta¿Cuál es el algoritmo óptimo "más general unificador"?
¿Cuál es el algoritmo de MGU más eficiente? ¿Cuál es su complejidad de tiempo? ¿Es lo suficientemente simple describir como una respuesta de desbordamiento de pila?
He intentado encontrar la respuesta en Google, pero sigo encontrando .PDF privados a los que solo puedo acceder a través de una suscripción de ACM.
encontré una discusión en SICP: here
Explicación de lo que un "algoritmo de unificación general de la mayoría" es: Tomar dos árboles de expresión que contiene las variables "libres" y "constantes" ... por ejemplo,
e1 = (+ x? (* y? 3) 5) e2 = (+ z? q? r?)
A continuación, el algoritmo más general Unificador devuelve el conjunto más general de vinculaciones que hace que las dos expresiones equivalentes.
decir
mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5
Por "más general", en su lugar podría obligar (x = 1) y (z = 1) y que también haría que E1 y E2 equivalentes, pero sería más específico.
El artículo del SICP parece implicar que es razonablemente costoso.
Para más información, la razón por la que pregunto es porque sé que la inferencia de tipo también involucra este algoritmo de "unificación" y me gustaría entenderlo.
¿Conoces un documento que lo describa? ¿Es básicamente el mismo que se describe en SICP? –
Sí, el algoritmo simple es esencialmente el mismo que se describe en SICP. La presentación habitual utiliza reglas como la descomposición, el choque, la comprobación de ocurrencias, ..., por lo que es posible que desee buscar eso. – starblue