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

Definição thumb|right|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 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 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 thumb|right|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 thumb|right|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 thumb|right|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 thumb|right|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.

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

Categoria:Sistemas de reescrita de termos