Unificação

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Question book.svg
Esta página ou secção não cita nenhuma fonte ou referência, o que compromete sua credibilidade (desde Janeiro de 2013).
Por favor, melhore este artigo providenciando fontes fiáveis e independentes, inserindo-as no corpo do texto por meio de notas de rodapé. Encontre fontes: Googlenotícias, livros, acadêmicoScirusBing. Veja como referenciar e citar as fontes.


Na lógica matemática, a unificação de dois termos serve para descobrir substituições que façam expressões diferentes se tornarem idênticas.

Uma substituição σ é um conjunto de componentes de substituições independentes: σ = [(t1, v1), . . . , (tn, vn)]. O primeiro elemento de cada componente é um termo e o segundo elemento é uma variável, tal que:

1. vivj se ij

2. vi não ocorre em tj para quaisquer i e j.

Se uma variável v é trocada em cada uma de suas ocorrências livres, na fbf α, pelo termo t, a fórmula resultante é chamada uma instância de substituição de α, e denotada por α[(t, v)], cuja leitura é “α com t no lugar de v”. Analogamente, α[(t1, v1), . . . , (tn, vn)] denota o resultado de trocar simultaneamente todas as ocorrências das diferentes variáveis v1, . . . , vn, em α, por t1, . . . , tn, respectivamente.

Como exemplo, os polinômios, X2 e Y3 podem ser unificados a Z6 tomando σ = [(Z3, X), (Z2, Y)].

Unificação em Prolog[editar | editar código-fonte]

O conceito de unificação, uma das principais idéias por trás do Prolog, foi proposto por 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[editar | editar código-fonte]

• 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) – α1

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

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

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

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

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

σ3 = [(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.

Veja também[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]