Par crítico

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

Teoria

Dada duas regras $l_{1} \to r_{1} e l_{2} \to 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 $l_{1}$ (ou ele próprio), que não seja uma variável, que possa ser unificada com $l_{2}$ gerando uma substituição s.

Dada duas regras $l_{1} \to r_{1} e l_{2} \to r_{2}$ que se sobrepõem e uma substituição s sendo o resultado da unificação de $l_{2}$ com um subtermo de $l_{1}$ numa posição p, dizemos que o par < $u_{1}, u_{2}$ > é um par crítico onde $u_{1}$ é o resultado da aplicação de s sobre $r_{1}$ e $u_{2}$ é o resultado da substituição de s aplicado a $r_{2}$ na posição p de $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))) $\to$ x, f(g(x)) $\to$ 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))) $\to$ x

Renomeando:

2: f(g(f(y))) $\to$ 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 $σ$ = { x $\to$ g(f(y)) }.

Aplicando $σ$ a x que é o lado direito da regra 1 obtemos g(f(y)).

1.1: Aplicando $σ$ a f(g(f(x))) obtemos f(g(f(g(f(y))))).

1.2: Aplicando $σ$ 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))) $\to$ x

Renomeando:

2: f(g(y)) $\to$ 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 $σ$ = { y $\to$ f(x) }.

Aplicando $σ$ a x que é o lado direito da regra 1 obtemos x;

1.1: Aplicando $σ$ a f(g(f(x))) obtemos f(g(f(x))).

1.2: Aplicando $σ$ 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)) $\to$ g(f(x))

Renomeando:

2: f(g(y)) $\to$ 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 $σ$ = { x $\to$ y }.

Aplicando $σ$ a g(f(x)) que é o lado direito da regra 1 obtemos g(f(x)).

1.1: Aplicando $σ$ a f(g(x)) obtemos f(g(y)).

1.2: Aplicando $σ$ 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 $t_{1}$ e $t_{2}$ pela aplicação de duas regras do sistema de reescrita de termos, então existe uma cadeia de redução iniciada por $t_{1}$ até $t_{2}$ ou existem subtermos $u_{1}$ e $u_{2}$ de s tais que $u_{1} = t_{2}$ e $u_{2} = t_{2}$ . Neste caso < $u_{1}, u_{2}$ > ou < $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 < $u_{1}, u_{2}$ > do sistema existir uma cadeia de redução iniciada por $u_{1}$ até $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 < $u_{1}, u_{2}$ > do sistema existir uma cadeia de redução iniciada por  $u_{1}$  até  $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

Par crítico

Índice

Teoria

Exemplo

Principais Resultados

Bibliografia

Ver também

Menu de navegação

Par crítico

Teoria

Exemplo

Principais Resultados

Bibliografia

Ver também

Menu de navegação

Pesquisa