Saltar para o conteúdo

Confluência (sistemas de reescrita de termos)

Origem: Wikipédia, a enciclopédia livre.

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 pode ser reescrita de duas maneiras: simplificando inicialmente a primeira expressão entre parêntese ou a segunda. Simplificando a primeira expressão, teremos: . Simplificando a segunda, temos: . 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.

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

Considere um sistema de redução abstrato (A,). Dados , dizemos que e são ligáveis se tal que e . Definimos ainda como o fecho reflexivo de , como o fecho transitivo de , e como o fecho transitivo e reflexivo de . Dizemos que (A,) é confluente se para quaisquer se então e 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: e e . 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 e se temos 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,) dizemos que um elemento x pertencente a A é semi-confluente se e somente se então existe um elemento z pertencente a A tal que . Se todos os elementos de A são semi-confluentes então dizemos que (A,) é 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 então e são ligáveis. Isto é, sempre que a partir de um elemento x pudermos chegar a um elemento e a 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 então existe z tal que . Isto é, sempre que a partir de um elemento x pudermos chegar a um elemento e a um elemento com um passo de redução, e alcançarão um elemento comum z sendo que alcançará z a partir de uma cadeia de derivação iniciada por e alcançará z por um passo de redução ou é 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 e se e for fortemente confluente, então é 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 então existe z tal que . 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,) é confluente se e somente se possui a propriedade diamante.

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