Confluência (sistemas de reescrita de termos)

A confluência é uma propriedade de sistemas de reescrita de termos definida do seguinte modo: dado um sistema de reescrita de termos R e um termo t neste sistema, a escolha de uma das regras de R a ser aplicada sobre t não modificará o resultado obtido pela reescrita de t, isto é, não importa as regras escolhidas a serem aplicadas, pois a escolha de diferentes regras sempre resultará em um elemento comum atingido a partir de cada escolha possível para reescrita do termo.

Exemplos como motivação

Considere as regras básicas da aritmética. Podemos pensar nestas regras como um sistema de reescrita de termos. A expressão $(11+9)\times (2+4)$ pode ser reescrita de duas maneiras: simplificando inicialmente a primeira expressão entre parêntese ou a segunda. Simplificando a primeira expressão, teremos: $20\times (2+4)=20\times 6=120$. Simplificando a segunda, temos: $(11+9)\times 6=20\times 6=120$. Obtemos o mesmo resultado da reescrita do termo de duas maneiras diferentes. Isto sugere que o sistema de reescrita formado pela aritmética básica é um sistema de reescrita de termos confluente.

Definição

Figura 1: definição de confluência.

Considere um sistema de redução abstrato (A,$\to$). Dados $x_1,x_2\in A$, dizemos que $x_1$ e $x_2$ são ligáveis se $\mathrm{\exists }z\in A$ tal que $x_1\to z$ e $x_2\to z$. Definimos ainda ${\to }^{=}$ como o fecho reflexivo de $\to$, ${\to }^{+}$ como o fecho transitivo de $\to$, e ${\to }^{*}$ como o fecho transitivo e reflexivo de $\to$. Dizemos que (A,$\to$) é confluente se para quaisquer $x,y_1,y_2\in A$ se $y_1{\leftarrow }^{*}x{\to }^{*}{y}_2$ então $y_1$ e $y_2$ são ligáveis. Isto quer dizer que para cada elemento x que se reduza a dois outros elementos, sempre existirá um quarto elemento comum ao qual estes dois últimos elementos podem ambos ser reduzidos.

Podemos definir diagramaticamente a propriedade de confluência (figura 1) onde as linhas sólidas do diagrama representam a quantificação universal e as linhas tracejadas representam a quantificação existencial. A figura 1 representa a definição de confluência conforme descrito anteriormente e podemos interpretar a figura 1 do seguinte modo: $\mathrm{\forall }x,y_1,y_2\in A.\mathrm{\exists }z\in A.x{\to }^{*}{y}_1$ e $x{\to }^{*}{y}_2\Rightarrow y_1{\to }^{*}z$ e $y_2{\to }^{*}z$. Esta notação será usada no restante das figuras presentes neste artigo.

Outras Propriedades Relacionadas

Existem também outras propriedades mais fracas ou equivalentes à confluência: semi-confluência, confluência forte, confluência fraca, propriedade diamante e a propriedade de Church-Rosser.

Propriedade de Church-Rosser

A propriedade de Church-Rosser garante que para um sistema de redução abstrato $(A,\to )$ e $x,y,z\in A$ se temos $x{\leftrightarrow }^{*}y$ então x e y são ligáveis. Isto é, sempre que existir uma cadeia de redução iniciada por x levando a um termo y e também existir uma cadeia de redução iniciada por y levando a x então existirá um elemento z tal que existe uma cadeia de redução iniciada por x levando a z e existe uma cadeia de redução iniciada por y levando a z.

A propriedade de Church-Rosser é equivalente à propriedade de confluência, ou seja, um sistema de redução abstrato é confluente se e somente ele é Church-Rosser.

Tal propriedade foi usada pelo teorema de Church-Rosser para demonstrar a confluência do cálculo lambda.

Semi-Confluência

Figura 2: definição de semi-confluência.

Dado um sistema abstrato de redução (A,$\to$) dizemos que um elemento x pertencente a A é semi-confluente se e somente se $y_1\leftarrow x{\to }^{*}{y}_2$ então existe um elemento z pertencente a A tal que $y_1\to ze{y}_2\to z$. Se todos os elementos de A são semi-confluentes então dizemos que (A,$\to$) é semi-confluente.

Um elemento semi-confluente não é necessariamente confluente, mas um sistema abstrato de redução semi-confluente é sempre confluente.

Na figura 2 podemos visualizar a definição diagramática de semi-confluência.

Confluência Local ou Confluência Fraca

Figura 3: definição de Confluência Local.

Um sistema abstrato de redução é localmente confluente se e somente se $y_1\leftarrow x\to y_2$ então $y_1$ e $y_2$ são ligáveis. Isto é, sempre que a partir de um elemento x pudermos chegar a um elemento $y_1$ e a $y_2$ com um passo de redução, eles alcançarão um elemento comum a partir de uma cadeia de derivação iniciada por eles.

Na figura 3 podemos visualizar a definição diagramática de confluência local.

Confluência local é uma propriedade mais fraca que confluência. No entanto, caso o sistema abstrato de redução seja terminante e também seja localmente confluente então o sistema abstrato de redução também será confluente (lema de Newman).

Confluência Forte

Figura 4: definição de confluência forte.

Um sistema abstrato de redução é fortemente confluente se e somente se $y_1\leftarrow x\to y_2$ então existe z tal que $y_1{\to }^{*}z{\leftarrow }^{=}{y}_2$. Isto é, sempre que a partir de um elemento x pudermos chegar a um elemento $y_1$ e a um elemento $y_2$ com um passo de redução, $y_1$ e $y_2$ alcançarão um elemento comum z sendo que $y_1$ alcançará z a partir de uma cadeia de derivação iniciada por $y_1$ e $y_2$ alcançará z por um passo de redução ou $y_2$ é igual a z.

Na figura 4 podemos visualizar a definição diagramática de confluência forte.

Todo sistema abstrato de redução fortemente confluente também é confluente. Está propriedade pode ser usada com o auxílio do seguinte teorema segundo o qual: dado dois sistemas de redução abstratos $(A,{\to }_1)$ e $(A,{\to }_2)$ se ${\to }_1\subseteq {\to }_2\subseteq \underset{1}{\overset{*}{\to }}$ e $(A,{\to }_2)$ for fortemente confluente, então $(A,{\to }_1)$ é confluente.

Propriedade Diamante

Figura 5: definição da propriedade diamante.

Um sistema de redução abstrato possui a propriedade diamante se e somente se $y_1\leftarrow x\to y_2$ então existe z tal que $y_1\to z\leftarrow y_2$. Isto é, para todo elemento x os seus sucessores diretos se reduzem a um elemento comum.

Na figura 5 podemos visualizar a definição diagramática da propriedade diamante.

Claro que a propriedade diamante é mais forte que todas as outras, logo se um sistema possui a propriedade diamante ele também é confluente e fortemente confluente. Outro fato interessante é que um sistema abstrato de redução (A,$\to$) é confluente se e somente se ${\to }^{*}$ possui a propriedade diamante.

Bibliografia

• Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003.
• Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998.

Ver também

• Sistemas de reescrita de termos
• Sistema de redução abstrato
• Teorema de Church-Rosser
• Lema de Newman