Unificação: diferenças entre revisões

← Ver a alteração anterior Ver a alteração posterior →

Conteúdo apagado Conteúdo adicionado

Em linha

Revisão das 13h24min de 24 de abril de 2014

Existe um modo diferente, em que a unificaçao significa junçao,exemplo: se um país encontrar com outro na Terra eles se unificaram 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: σ = [(t₁, v₁), . . . , (t_n, v_n)]. O primeiro elemento de cada componente é um termo e o segundo elemento é uma variável, tal que:

1. v_i ≠ v_j se i ≠ j

2. v_i não ocorre em t_j 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, α[(t₁, v₁), . . . , (t_n, v_n)] denota o resultado de trocar simultaneamente todas as ocorrências das diferentes variáveis v₁, . . . , v_n, em α, por t₁, . . . , t_n, respectivamente.

Como exemplo, os polinômios, X² e Y³ podem ser unificados a Z⁶ tomando σ = [(Z³, X), (Z², Y)].

Unificação em Prolog

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

• 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.

Veja também

Ligações externas

Unification at MathWorld

@@ Linha 3: / Linha 3: @@
 {{Desambigexplicada2|um tema de ciência da computação|a unificação em geopolítica|união política}}
+Existe um modo diferente, em que a unificaçao significa junçao,exemplo: se um país encontrar com outro na Terra eles se unificaram
 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.