Confluência (sistemas de reescrita de termos)

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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[editar | editar código-fonte]

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\times6\,=\,120. Simplificando a segunda, temos: (11+9)\times6\,=\,20\times6\,=\,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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

A propriedade de Church-Rosser garante que para um sistema de redução abstrato (A,\rightarrow) e x,y,z\,\isin 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

  • 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[editar | editar código-fonte]