Qual é o ideal “unificador mais geral” algoritmo?

Question

A Pergunta

O que é o algoritmo MGU mais eficiente? Qual é a sua complexidade de tempo? É simples o suficiente para descrever como uma resposta de estouro de pilha?

Eu tenho tentado encontrar a resposta no Google, mas continuo achando .PDFs privadas que só posso acesso através de uma subscrição ACM.

Eu encontrei uma discussão em SICP: aqui

Explicação do que é um "algoritmo de unificação geral mais" é: Tome duas árvores de expressão contendo "variáveis ??livres" e "constantes" ... por exemplo.

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

Então, o Unificador algoritmo mais geral retorna o conjunto mais geral de ligações que faz com que as duas expressões equivalentes.

i.

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

Por "mais geral", você poderia, em vez bind (x = 1) e (z = 1) e que também faria E1 e E2 equivalente mas seria mais específico.

O artigo SICP parece implicar que é razoavelmente caro.

Para informações, a razão que eu estou pedindo é porque eu sei que tipo de inferência também envolve este algoritmo "unificação" e eu gostaria de compreendê-lo.

Answer 1

O simples algorith que é usado na prática (por exemplo em Prolog) é exponencial para casos patológicos.

Há um algoritmo teoricamente mais eficiente por Martelli e Montanari (IIRC é linear), mas é muito mais lento para os casos simples que ocorrem na prática, por isso não é muito usado.

Answer 2

Baader e Snyder publicados vários algoritmos de unificação, para tanto sintática unificação e unificação equational.

Eles afirmam que o seu terceiro algoritmo unificação sintáctica (na secção 2.3) é executado em O (n alfa (n)), onde alfa (N) é o inverso da função de Ackermann -. Em situações práticas é equivalente a uma constante pequena