Tjyylli

Em sistemas de reescrita de termos quando existem duas regras l1→r1el2→r2{displaystyle l_{1},rightarrow ,r_{1},e,l_{2},rightarrow ,r_{2}} num sistema renomeadas de modo a não terem variáveis de mesmo símbolo e exista em l1{displaystyle l_{1}} um subtermo que não seja uma variável que possa ser unificado com l2{displaystyle l_{2}} gerando um substituição s, então dizemos que o par <u1,u2{displaystyle u_{1},u_{2}}> é um par crítico do sistema onde u1{displaystyle u1} é o resultado da aplicação de s sobre r1{displaystyle r_{1}} e u2{displaystyle u_{2}} é o resultado da substituição s aplicado a r2{displaystyle r_{2}} do subtermo de l1{displaystyle l_{1}} usado na unificação.

Teoria |

Dada duas regras l1→r1el2→r2{displaystyle l_{1},rightarrow ,r_{1},e,l_{2},rightarrow ,r_{2}} do sistema de reescrita de termos dizemos que elas se sobrepõem se após renomearmos as variáveis das regras, de modo que não haja variáveis em comum entre elas, exista um subtermo de l1{displaystyle l_{1}} (ou ele próprio), que não seja uma variável, que possa ser unificada com l2{displaystyle l_{2}} gerando uma substituição s.

Dada duas regras l1→r1el2→r2{displaystyle l_{1},rightarrow ,r_{1},e,l_{2},rightarrow ,r_{2}} que se sobrepõem e uma substituição s sendo o resultado da unificação de l2{displaystyle l_{2}} com um subtermo de l1{displaystyle l_{1}} numa posição p, dizemos que o par <u1,u2{displaystyle u_{1},u_{2}}> é um par crítico onde u1{displaystyle u_{1}} é o resultado da aplicação de s sobre r1{displaystyle r_{1}} e u2{displaystyle u_{2}} é o resultado da substituição de s aplicado a r2{displaystyle r_{2}} na posição p de l1{displaystyle l_{1}}.

Os pares críticos de um sistema de reescrita de termos são os pares críticos obtidos da cada sobreposição de regras do sistema. Observe que isto inclui a sobreposição de uma regra com ela mesma, isto é, a sobreposição de uma regra l com ela mesma renomeada. Observe que os pares críticos são únicos a menos de uma renomeação.

Quando os termos do par crítico são iguais dizemos que é um par crítico trivial. Veremos mais adiante que eles não são importantes e podem ser desconsiderados no conjunto dos pares críticos.

Quando um dos termos do par crítico pode ser reescrito no outro termo do par através de uma cadeia de redução de zero ou mais passos dizemos que o par crítico é convergente.

Exemplo |

Mostraremos como construir o conjunto dos pares críticos de um sistema de reescrita.

Seja o R = { f(g(f(x))) →{displaystyle rightarrow } x, f(g(x)) →{displaystyle rightarrow } g(f(x)) } um sistema de reescrita.

Construir o conjunto dos pares críticos do sistema é o processo de verificar para cada par de regras do sistema se existe uma sobreposição e neste caso determinar o par crítico.

• Caso 1: Verificando a primeira regra com ela mesma:

1: f(g(f(x))) →{displaystyle rightarrow } x

Renomeando:

2: f(g(f(y))) →{displaystyle rightarrow } y

Observando as duas regras vemos que existe somente um subtermo de 1 que pode ser unficado com 2, o qual é f(x) na posição 11, isto é, o primeiro subtermo de f(g(f(x))) o qual é g(f(x)) e o primeiro subtermo de g(f(x)) o qual é f(x). Unificando f(x) com f(g(f(y))) obtemos a substituição σ{displaystyle sigma } = { x →{displaystyle rightarrow } g(f(y)) }.

Aplicando σ{displaystyle sigma } a x que é o lado direito da regra 1 obtemos g(f(y)).

1.1: Aplicando σ{displaystyle sigma } a f(g(f(x))) obtemos f(g(f(g(f(y))))).

1.2: Aplicando σ{displaystyle sigma } a x que é o lado direito da regra 2 obtemos g(f(y)).

Substituindo 1.2 em 1.1 na posição 11 obtemos f(g(y)).

Logo temos o par crítico <g(f(y)),f(g(y))> resultante da sobreposição da primeira regra com ela mesma na posição 11.

• Caso 2: Verificando a primeira regra com a segunda:

1: f(g(f(x))) →{displaystyle rightarrow } x

Renomeando:

2: f(g(y)) →{displaystyle rightarrow } g(f(y))

Observando as duas regras vemos que existe somente um subtermo de 1 que pode ser unificado com 2, o qual é o próprio. Unificando f(g(f(x))) com f(g(y)) obtemos a substituição σ{displaystyle sigma } = { y →{displaystyle rightarrow } f(x) }.

Aplicando σ{displaystyle sigma } a x que é o lado direito da regra 1 obtemos x;

1.1: Aplicando σ{displaystyle sigma } a f(g(f(x))) obtemos f(g(f(x))).

1.2: Aplicando σ{displaystyle sigma } a g(f(y)) que é o lado direito da regra 2 obtemos g(f(f(x))).

Substituindo 1.1 por 1.2, pois é o próprio termo, obtemos f(x).

Logo temos o par crítico <x,g(f(f(x)))> resultante da sobreposição da primeira regra com ela mesma na posição vazia (o próprio termo).

• Caso 3: Verificando a segunda regra com ela mesma:

1: f(g(x)) →{displaystyle rightarrow } g(f(x))

Renomeando:

2: f(g(y)) →{displaystyle rightarrow } g(f(y))

Observando as duas regras vemos que existe somente um subtermo de 1 que pode ser unificado com 2, o qual é o próprio. Unificando f(g(x)) com f(g(y)) obtemos a substituição σ{displaystyle sigma } = { x →{displaystyle rightarrow } y }.

Aplicando σ{displaystyle sigma } a g(f(x)) que é o lado direito da regra 1 obtemos g(f(x)).

1.1: Aplicando σ{displaystyle sigma } a f(g(x)) obtemos f(g(y)).

1.2: Aplicando σ{displaystyle sigma } a g(f(y)) que é o lado direito da regra 2 obtemos g(f(y)).

Substituindo 1.1 por 1.2, pois é o próprio termo, obtemos g(f(y)).

Logo temos o par crítico <g(f(y)),g(f(y))> resultante da sobreposição da segunda regra com ela mesma. Observe que o par crítico é trivial.

• Caso 4: Verificando a segunda regra com a primeira

Chegaremos a um par crítico equivalente ao caso 2.

Como examinos as sobreposições de todos os casos possíveis de combinações de duas regras obtemos o conjunto dos pares críticos para o sistema R a seguir: { <g(f(y)),f(g(y))>, <x,g(f(f(x)))>, <g(f(y)),g(f(y))>};

Principais Resultados |

Como principais resultados podemos citar que se um sistema de reescrita de termos não é confluente então existe um par crítico que não é convergente, assim os pares críticos são fontes potenciais de falhas de confluência. Esse fato motivou os dois resultados a seguir:

• 
  Lema do par crítico: Se um termo s pode derivar dois termos distintos t1{displaystyle t_{1}} e t2{displaystyle t_{2}} pela aplicação de duas regras do sistema de reescrita de termos, então existe uma cadeia de redução iniciada por t1{displaystyle t_{1}} até t2{displaystyle t_{2}} ou existem subtermos u1{displaystyle u_{1}} e u2{displaystyle u_{2}} de s tais que u1=t2{displaystyle u_{1},=,t_{2}} e u2=t2{displaystyle u_{2},=,t_{2}}. Neste caso <u1,u2{displaystyle u_{1},u_{2}}> ou <u2,u1{displaystyle u_{2},u_{1}}> é um par crítico de R.


• 
  Teorema do Par Crítico: Um sistema de reescrita de termos é localmente confluente se e somente se para cada par crítico <u1,u2{displaystyle u_{1},u_{2}}> do sistema existir uma cadeia de redução iniciada por u1{displaystyle u_{1}} até u2{displaystyle u_{2}}.

Associando o teorema do par crítico com o lema de Newman obtemos que um sistema de reescrita de termos é confluente se e somente se para cada par crítico <u1,u2{displaystyle u_{1},u_{2}}> do sistema existir uma cadeia de redução iniciada por u1{displaystyle u_{1}} até u2{displaystyle u_{2}}. Por essa razaão podemos desconsiderar os pares críticos onde os dois termos são iguais já que não podem ser fontes de problemas para a confluência.

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 |

• Sistema de reescrita de termos


• Sistema de redução abstrato


• Unificação