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, $\rightarrow$ ). Dados $x_{1},\,x_{2}\in \,A$ , dizemos que $\,x_{1}$ e $\,x_{2}$ são ligáveis se $\exists z\,\in A$ tal que $x_{1}\,\rightarrow \,z$ e $x_{2}\,\rightarrow \,z$ . Definimos ainda $\rightarrow ^{=}$ como o fecho reflexivo de $\rightarrow$ , $\rightarrow ^{+}$ como o fecho transitivo de $\rightarrow$ , e $\rightarrow ^{*}$ como o fecho transitivo e reflexivo de $\rightarrow$ . Dizemos que (A, $\rightarrow$ ) é confluente se para quaisquer $x,\,y_{1},\,y_{2}\in \,A$ se $y_{1}\,\leftarrow ^{*}\,x\,\rightarrow ^{*}\,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: $\forall \,x,\,y_{1},\,y_{2}\,\in \,A.\,\exists z\,\in \,A.\,\,x\,\rightarrow ^{*}y_{1}$ e $\,x\,\rightarrow ^{*}y_{2}\,\,\Rightarrow \,\,y_{1}\,\rightarrow ^{*}z$ e $\,y_{2}\,\rightarrow ^{*}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,\rightarrow )$ 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, $\rightarrow$ ) dizemos que um elemento x pertencente a A é semi-confluente se e somente se $y_{1}\,\leftarrow x\,\rightarrow ^{*}y_{2}$ então existe um elemento z pertencente a A tal que $y_{1}\,\rightarrow z\,e\,y_{2}\,\rightarrow z$ . Se todos os elementos de A são semi-confluentes então dizemos que (A, $\rightarrow$ ) é 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\,\rightarrow \,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\,\rightarrow \,y_{2}$ então existe z tal que $y_{1}\,\rightarrow ^{*}\,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,\rightarrow _{1})$ e $(A,\rightarrow _{2})$ se $\rightarrow _{1}\,\subseteq \,\rightarrow _{2}\,\subseteq \,\rightarrow _{1}^{*}$ e $(A,\rightarrow _{2})$ for fortemente confluente, então $(A,\rightarrow _{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\,\rightarrow \,y_{2}$ então existe z tal que $y_{1}\,\rightarrow \,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, $\rightarrow$ ) é confluente se e somente se $\rightarrow ^{*}$ 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.