Unificação

O átomo contido num nó não terminal de uma árvore de prova, é uma instância de uma cabeça de cláusula. Excluindo a raiz, esse átomo é também uma instância de um átomo do corpo de uma cláusula. A construção de uma árvore de prova, em grosso modo, reduz-se à procura de instâncias comuns a dois átomos. É este facto que motiva as considerações que se seguem. Para explicarmos o conceito de unificação, na sua forma mais geral, e também para estarmos de acordo com a funcionalidade do Prolog, vamos, antes de mais, generalizar o conceito de átomo. Tinhamos dito que um átomo escreve-se com um símbolo de predicado e um número de termos igual à aridade do símbolo do predicado em questão e que estes termos constituiam os chamados argumentos do átomo. Vamos agora permitir (definição recursiva!) que os argumentos possam ser, eles mesmo, átomos. Dois átomos atomo₁ e atomo₂ são unificáveis, se existir uma substituição s tal que s(atomo₁) = s(atomo₂). Nesse caso dizemos que s é um unificador de atomo₁ e atomo₂. Por exemplo os átomos atomo₁ = p(X,b) e atomo₂ = p(a,Y) são unificáveis pelo unificador $s = \left\{X \leftarrow a, Y \leftarrow b\right\}$ . Uma constante é apenas unificável com ela própria e com uma variável. Intuitivamente, um unificador do atomo₁ e do atomo₂, é uma substituição que consegue ``instanciar'' suficientemente as variáveis de modo a satisfazer a equação atomo₁ = atomo₂. Um unificador minimal, é um unificador que instancia o menos possível as variáveis. Por exemplo os dois átomos atomo₁ = p(X,Y) e atomo₂ = p(Y,X) são unificáveis por $s_1 = \left\{Y\leftarrow X\right\}$ , por $s_2 = \left\{X\leftarrow Y\right\}$ , por $s_3 = \left\{X\leftarrow a,\,Y\leftarrow a\right\}$ , ...mas s₁ e s₂ são os unificadores minimais. Formalmente, o unificador s é minimal se, para todo o unificador s', existe uma substituição s'' tal que $s' = s'' \circ s$ (composição de substituições). Pode-se mostrar que se existir um unificador entre dois átomos, então existe um unificador minimal. Também é possível demonstrar que se X é uma variável e atomo um átomo, então atomo e X são unificáveis se, e somente se, atomo não contiver a variável X (quando a varável X não tem ocorrência em atomo). Existe um algoritmo (algoritmo de Robinson) que, dados dois átomos, calcula um unificador minimal, se os os dois átomos são unificáveis, ou então termina com a indicação da impossibilidade de unificação. Seguem-se dois exemplos simples que ilustram o método. Ajuda representar os átomos na forma de árvore. A ideia é tentar construir o unificador por aproximações sucessivas, por composição de substituições. Em cada etapa procuramos uma variável que é uma folha numa das árvores e tentamos unificá-la com a sub-árvore correspondente na outra árvore. Nos esquemas que se seguem, essas variáveis e essas sub-árvores são envoltas com uma curva fechada.

Primeiro Exemplo: atomo₁ = p(X,Y), $atomo_2 = p\left(Y,g(a)\right)$

Etapa $\mathbf{n^{\footnotesize {o}} 1}$

$\xymatrix{ & {\underline{atomo_1}} & & & & {\underline{atomo_2}} & \\ & p \... ...\\ *++[o][F-]{X} & & Y & & *++[o][F-]{Y} & & g \ar@{-}[d] \\ & & & & & & a}$

$s_1 = \left\{ X \leftarrow Y \right\}$

Etapa $\mathbf{n^{\footnotesize {o}} 2}$

$\xymatrix{ & {\underline{s_1\left(atomo_1\right)}} & & & & {\underline{s_1\lef... ...g \ar@{-}[d] \\ & & & & & & a \save ''3,7''.''4,7''*[e][F-]\frm{} \restore }$

$s_2 = \left\{ Y \leftarrow g(a) \right\}$

Etapa $\mathbf{n^{\footnotesize {o}} 3}$

$\xymatrix{ & {\underline{s_2\left(s_1(atomo_1)\right)}} & & & & {\underline{s_... ...d] & & g \ar@{-}[d] & & g \ar@{-}[d] & & g \ar@{-}[d] \\ a & & a & & a & & a }$

Conclusão: unificador minimal dado por

$\begin{displaymath}s_2 \circ s_1 = \left\{ X \leftarrow g(a),\, Y \leftarrow g(a) \right\} \end{displaymath}$

Segundo Exemplo:

$\begin{displaymath}atomo_1 = p\left(Y,h(a,X)\right), \quad atomo_2 = p\left(X,h(Y,b)\right) \end{displaymath}$

Etapa $\mathbf{n^{\footnotesize {o}} 1}$

$\xymatrix{ & {\underline{atomo_1}} & & & & & {\underline{atomo_2}} & & \\ &... ... & & *++[o][F-]{X} & & h \ar@{-}[dl] \ar@{-}[dr] & \\ & a & & X & & & Y & & b}$

$s_1 = \left\{Y\leftarrow X\right\}$

Etapa $\mathbf{n^{\footnotesize {o}} 2}$

$\xymatrix{ & {\underline{s_1\left(atomo_1\right)}} & & & & & {\underline{s_1\l... ...\ar@{-}[dl] \ar@{-}[dr] & \\ & *++[o][F-]{a} & & X & & & *++[o][F-]{X} & & b}$

$s_2 = \left\{ X \leftarrow a \right\}$

Etapa $\mathbf{n^{\footnotesize {o}} 3}$

$\xymatrix{ & {\underline{s_2\left(s_1(atomo_1)\right)}} & & & & & {\underline{... ...\ar@{-}[dl] \ar@{-}[dr] & \\ & a & & *++[o][F-]{a} & & & a & & *++[o][F-]{b}}$

Conclusão: os átomos não são unificáveis (a constante a não unifica com a constante b).
Dois átomos atomo₁ e atomo₂ são duas variantes, se podermos passar de um ao outro por uma simples mudança do nome das variáveis (duas variáveis distintas mudadas sempre por duas variáveis distintas). Por outro lado, atomo₂ é uma renomeação do atomo₁, em relação a um conjunto V₁ de variáveis, se atomo₂ é uma variante do atomo₁ e se atomo₂ não contiver nenhuma variável em V₁. As nocões de unificação e de renomeação, definidas para átomos, estendem-se, da maneira natural, para as cláusulas.

Delfim F. Marado Torres
1999-03-16