Prolog/Unificação

O conceito de unificação, uma das principais idéias por trás do Prolog, foi proposto por w:Jacques Herbrand (1930), e o 1º algoritmo se deve a Robinson (1965). Este conceito representa o mecanismo de ligar os conteúdos das variáveis e pode ser visto como um tipo de atribuição. Em Prolog, esta operação é denotada pelo símbolo “=”.

1. No Prolog tradicional, a variável X que não está instanciada, ou seja, sobre a qual nenhuma unificação foi feita, pode ser unificada com um átomo, um termo ou com outra variável não instanciada. Em muitos dialetos modernos de Prolog e na Lógica de primeira ordem, uma variável não pode ser unificada com um termo que a contém.

2. Um átomo em Prolog só pode ser unificado com o mesmo átomo.

3. Similarmente, um termo pode ser unificado com outro termo se os símbolos e a aridade das funções sob as quais eles ocorrem são idênticos e se os parâmetros podem ser unificados simultaneamente. Note que este é um comportamento recursivo.

Devido a sua natureza declarativa, a ordem numa seqüência de unificações não é importante (em geral). Para todo par de expressões que deve ser unificado, existe um único unificador mais geral (umg), ou seja, uma unificação que faz a menor quantidade possível de substituições, no sentido de que instancia variáveis, sempre que possível, para unificar um dado conjunto de expressões.

Note que na terminologia da Lógica de primeira ordem, um átomo é uma proposição básica e é unificado similarmente a um termo de Prolog.

Exemplos de Unificação

• A = A: Unificação bem sucedida (tautologia)

• A = B, B = abc : A e B são unificados com o átomo abc

• xyz = C, C = D : A unificação é simétrica

• abc = abc : A unificação é bem sucedida

• abc = xyz : Falha em unificar porque os átomos são diferentes

• f(A) = f(B) : A é unificado com B

• f(A) = g(B) : Falha porque as cabeças dos termos são diferentes

• f(A) = f(B, C) : A unificação falha porque os termos têm aridades diferentes

• f(g(A)) = f(B) : Unifica B com o termo g(A)

• f(g(A), A) = f(B, xyz) : Unifica A com o átomo xyz e B com o termo g(xyz)

• A = f(A) : Unificação infinita, A é unificado com f(f(f(f(...)))). Na Lógica de Primeira Ordem propriamente dita e em vários dialetos modernos de Prolog, isto é proibido (ou reforçado pelo Occurs check)

• A = abc, xyz = X, A = X : Falha na unificação; efetivamente abc = xyz

• Seja α = { P(X, a, Y) – α₁

¬P(f(z), W, a) v ¬P(Z, d, W) – α₂

P(f(a), U, a) v ¬P(U, a, f(a)) } – α₃

onde X, Y, Z, W, U são variáveis e a, d são constantes (átomos)

σ₁ = [(f(z), X), (a, Y), (a, W)]

σ₂ = [(f(a), Z), (d, U)]

σ₃ = [(d, X), (f(a), Y)]

• Considere as sentenças:

amigo(joão, marcos)  %João é amigo de Marcos.
amigo(Y, daniel)
amigo(Y, mãe(Y))
amigo(X, aline)

Resultados da unificação:

amigo(joão, X) , amigo(joão, marcos) [(marcos, X)]
amigo(joão, X) , amigo(Y, daniel) [(daniel, X), (joão, Y)]
amigo(joão, X) , amigo(Y, mãe(Y)) [(joão, Y), (mãe(joão), X)]
amigo(joão, X) , amigo(X, aline) Falha a unificação pois X não pode receber dois valores diferentes.

O "Underscore"

Em prolog, o símbolo _ (chamado, em inglês, de underscore) é usado para representar "qualquer coisa". Após a unificação, o interpretador cria uma variável para unificar com ele.

Por exemplo:

 f(X,_) = f(1,2).

Irá unificar X=1, ignorando o underscore.

Por outro lado,

 f(X,_) = Y.

irá unificar Y = f(X, _6181), em que, em vez de _6181, pode aparecer uma outra expressão com o "underscore".