Reescrevendo - Rewriting

Em matemática , ciência da computação e lógica , reescrever cobre uma ampla gama de métodos (potencialmente não determinísticos ) de substituição de subtermos de uma fórmula por outros termos. Os objectos de foco para este artigo incluem sistemas de reescrita (também conhecidos como sistemas de reescrita , motores de reescrita , ou sistemas de redução ). Em sua forma mais básica, eles consistem em um conjunto de objetos, além de relações sobre como transformar esses objetos.

A reescrita pode ser não determinística . Uma regra para reescrever um termo pode ser aplicada de muitas maneiras diferentes a esse termo, ou mais de uma regra pode ser aplicável. Os sistemas de reescrita não fornecem um algoritmo para alterar um termo para outro, mas um conjunto de possíveis aplicações de regras. Quando combinados com um algoritmo apropriado, entretanto, os sistemas de reescrita podem ser vistos como programas de computador , e vários provadores de teoremas e linguagens de programação declarativas são baseados na reescrita de termos.

Casos de exemplo

Lógica

Na lógica , o procedimento para obter a forma normal conjuntiva (CNF) de uma fórmula pode ser implementado como um sistema de reescrita. As regras de um exemplo de tal sistema seriam:

( eliminação de dupla negação )
( Leis De Morgan )
( distributividade )

onde o símbolo ( ) indica que uma expressão correspondente ao lado esquerdo da regra pode ser reescrita para outra formada pelo lado direito, e cada um dos símbolos denota uma subexpressão. Nesse sistema, cada regra é escolhida de modo que o lado esquerdo seja equivalente ao lado direito e, consequentemente, quando o lado esquerdo corresponde a uma subexpressão, a reescrita dessa subexpressão da esquerda para a direita mantém a consistência lógica e o valor de toda a expressão .

Aritmética

Os sistemas de reescrita de termos podem ser empregados para calcular operações aritméticas em números naturais . Para tanto, cada um desses números deve ser codificado como um termo . A codificação mais simples é o utilizado nos axiomas Peano , com base na constante de 0 (zero) e a função sucessor S . por exemplo, os números 0, 1, 2 e 3 são representados pelos termos 0, S (0), S (S (0)) e S (S (S (0))), respectivamente. O seguinte termo sistema de reescrita pode ser usado para calcular a soma e o produto de dados números naturais.

Por exemplo, o cálculo de 2 + 2 para resultar em 4 pode ser duplicado pela reescrita do termo da seguinte forma:

onde os números das regras são fornecidos acima da seta para reescrever .

Como outro exemplo, o cálculo de 2⋅2 se parece com:

onde a última etapa compreende o cálculo do exemplo anterior.

Linguística

Em linguística , as regras de estrutura de frase , também chamadas de regras de reescrita , são usadas em alguns sistemas de gramática generativa , como um meio de gerar as sentenças gramaticalmente corretas de uma língua. Essa regra normalmente assume a forma A → X, onde A é um rótulo de categoria sintática , como sintagma nominal ou sentença , e X é uma sequência de tais rótulos ou morfemas , expressando o fato de que A pode ser substituído por X na geração do estrutura constituinte de uma frase. Por exemplo, a regra S → NP VP significa que uma frase pode consistir em um sintagma nominal seguido por um sintagma verbal ; outras regras especificarão em quais subconstituintes um sintagma nominal e um sintagma verbal podem consistir, e assim por diante.

Sistemas de reescrita de abstratos

A partir dos exemplos acima, fica claro que podemos pensar em reescrever sistemas de maneira abstrata. Precisamos especificar um conjunto de objetos e as regras que podem ser aplicadas para transformá-los. A configuração mais geral (unidimensional) dessa noção é chamada de sistema abstrato de redução ou sistema abstrato de reescrita (abreviado ARS ). Um ARS é simplesmente um conjunto A de objetos, junto com uma relação binária → em A chamada de relação de redução , relação de reescrita ou apenas redução .

Muitas noções e notações podem ser definidas no cenário geral de um ARS. é o fechamento transitivo reflexivo de . é o fechamento simétrico de . é o fechamento simétrico transitivo reflexivo de . O problema da palavra para um ARS é determinar, dados x e y , se . Um objeto x em A é chamado redutível se existe algum outro y em A tal que ; caso contrário, é denominado irredutível ou uma forma normal . Um objeto y é chamado de "forma normal de x " se , e y é irredutível. Se a forma normal de x for única, isso geralmente é denotado com . Se cada objeto tiver pelo menos uma forma normal, o ARS é chamado de normalização . ou X e Y são ditos ser acopláveis se existe algum z com a propriedade de que . Diz-se que um ARS possui a propriedade Church-Rosser se implicar . Um ARS é confluente se para todos os w , x e y em A , implica . Um ARS é localmente confluentes se e somente se para todo w , x e y em A , implica . Diz-se que um ARS está terminando ou é noetheriano se não houver uma cadeia infinita . Um ARS confluente e terminal é chamado convergente ou canônico .

Teoremas importantes para sistemas de reescrita abstratos são que um ARS é confluente se tiver a propriedade Church-Rosser, lema de Newman que afirma que um ARS de terminação é confluente se e somente se for localmente confluente, e que o problema da palavra para um ARS é indecidível em geral.

Sistemas de reescrita de strings

Um sistema de reescrita de strings (SRS), também conhecido como sistema semi-Thue , explora a estrutura monóide livre das strings (palavras) sobre um alfabeto para estender uma relação de reescrita,, para todas as strings no alfabeto que contêm esquerda e direita, respectivamente - lados de algumas regras como substrings . Formalmente, um sistema semi-Thue é uma tupla onde é um alfabeto (geralmente finito) e é uma relação binária entre algumas strings (fixas) no alfabeto, chamado de conjunto de regras de reescrita . A reescrita relação um passo induzido por em é definido como: para quaisquer cadeias se e somente se existirem tais que , , e . Uma vez que é uma relação ligada , o par se encaixa na definição de um sistema de reescrita abstrato. Obviamente, é um subconjunto de . Se a relação for simétrica , o sistema é denominado sistema Thue .

Em um SRS, a relação de redução é compatível com a operação monoidal, o que significa que implica para todas as strings . Da mesma forma, o fechamento simétrico transitivo reflexivo de , denotado , é uma congruência , o que significa que é uma relação de equivalência (por definição) e também é compatível com a concatenação de strings. A relação é chamada de congruência Thue gerada por . Em um sistema Thue, ou seja, se for simétrico, a relação de reescrita coincide com a congruência Thue .

A noção de um sistema semi-Thue coincide essencialmente com a apresentação de um monóide . Como é uma congruência, podemos definir o fator monóide do monóide livre pela congruência Thue. Se um monóide é isomórfico com , então o sistema semi-Thue é chamado de apresentação monóide de .

Imediatamente obtemos algumas conexões muito úteis com outras áreas da álgebra. Por exemplo, o alfabeto { a , b } com as regras { ab → ε, ba → ε}, onde ε é a string vazia , é uma apresentação do grupo livre em um gerador. Se, em vez disso, as regras são apenas { ab → ε}, então obtemos uma apresentação do monóide bicíclico . Assim, os sistemas semi-Thue constituem uma estrutura natural para resolver o problema da palavra para monoides e grupos. Na verdade, todo monóide tem uma apresentação da forma , ou seja, pode sempre ser apresentado por um sistema semi-Thue, possivelmente sobre um alfabeto infinito.

O problema da palavra para um sistema semi-Thue é indecidível em geral; este resultado é às vezes conhecido como teorema Post-Markov .

Sistemas de reescrita de termos

Fig.1: Diagrama de triângulo esquemático da aplicação de uma regra de reescrita na posição em um termo, com substituição correspondente
Pic.2: Regra lhs termo correspondência no termo

Um sistema de reescrita de termos ( TRS ) é um sistema de reescrita cujos objetos são termos , que são expressões com subexpressões aninhadas. Por exemplo, o sistema mostrado em § Lógica acima é um sistema de reescrita de termos. Os termos deste sistema são compostos de operadores binários e e o operador unário . Também estão presentes nas regras as variáveis, que representam qualquer termo possível (embora uma única variável sempre represente o mesmo termo em uma única regra).

Em contraste com os sistemas de reescrita de strings, cujos objetos são sequências de símbolos, os objetos de um sistema de reescrita de termos formam um termo álgebra . Um termo pode ser visualizado como uma árvore de símbolos, o conjunto de símbolos admitidos sendo fixado por uma determinada assinatura .

Definição formal

Uma regra de reescrita é um par de termos , comumente escritos como , para indicar que o lado esquerdo l pode ser substituído pelo lado direito r . Um sistema de reescrita de termos é um conjunto R de tais regras. Uma regra pode ser aplicada a um termo s se o termo esquerdo l corresponder a algum subtermo de s , isto é, se houver alguma substituição tal que o subtermo de enraizado em alguma posição p seja o resultado da aplicação da substituição ao termo l . O subtermo correspondente ao lado esquerdo da regra é denominado redex ou expressão redutível . O termo resultante t desta aplicação de regra é então o resultado da substituição do subtermo na posição p em s pelo termo com a substituição aplicada, ver figura 1. Neste caso, é dito que foi reescrito em uma etapa , ou reescrito diretamente , para pelo sistema , formalmente indicado como , ou como por alguns autores.

Se um termo pode ser reescrita em várias etapas em um termo , isto é, se , o termo é dito ser reescrito para , formalmente indicado como . Em outras palavras, a relação é o fechamento transitivo da relação ; frequentemente, também a notação é usada para denotar o fechamento reflexivo-transitivo de , isto é, se s = t ou . Uma reescrita de termo dada por um conjunto de regras pode ser vista como um sistema de reescrita abstrato conforme definido acima , com os termos como seus objetos e como sua relação de reescrita.

Por exemplo, é uma regra de reescrita, comumente usada para estabelecer uma forma normal com relação à associatividade de . Essa regra pode ser aplicada ao numerador no termo com a substituição correspondente , veja a figura 2. Aplicar essa substituição ao lado direito da regra produz o termo ( a * ( a + 1)) * ( a +2) , e substituir o numerador por esse termo produz , que é o termo de resultado da aplicação da regra de reescrita. Ao todo, a aplicação da regra de reescrita conseguiu o que é chamado de "aplicação da lei associatividade para a " em álgebra elementar. Alternativamente, a regra poderia ter sido aplicada ao denominador do termo original, rendendo .

Terminação

Além da seção Término e convergência , sutilezas adicionais devem ser consideradas para os sistemas de reescrita de termos.

Mesmo a terminação de um sistema que consiste em uma regra com um lado esquerdo linear é indecidível. A rescisão também é indecidível para sistemas que usam apenas símbolos de função unária; no entanto, é decidível para sistemas terrestres finitos .

O seguinte sistema de reescrita de termos está normalizando, mas não terminando e não confluente:

Os dois exemplos a seguir de sistemas de reescrita de termo de rescisão são devidos a Toyama:

e

Sua união é um sistema não rescisório, desde então . Este resultado refuta uma conjectura de Dershowitz , que afirmou que a união de dois sistemas de reescrita de termo final e está novamente terminando se todos os lados esquerdo e direito de forem lineares , e não houver " sobreposições " entre os lados esquerdo lados e lados direitos de . Todas essas propriedades são satisfeitas pelos exemplos de Toyama.

Consulte Ordem de reescrita e ordenação de caminho (reescrita de termo) para relações de ordenação usadas em provas de rescisão para sistemas de reescrita de termo.

Sistemas de reescrita de ordem superior

Os sistemas de reescrita de ordem superior são uma generalização dos sistemas de reescrita de termos de primeira ordem para termos lambda , permitindo funções de ordem superior e variáveis ​​associadas. Vários resultados sobre TRSs de primeira ordem também podem ser reformulados para HRSs.

Sistemas de reescrita de gráficos

Sistemas de reescrita Gráfico são outra generalização de sistemas de reescrita prazo, operando em gráficos em vez de ( solo -) termos / seus correspondentes árvore de representação.

Sistemas de reescrita de rastreamento

A teoria do traço fornece um meio para discutir o multiprocessamento em termos mais formais, como por meio do monóide traço e do monóide histórico . A reescrita também pode ser realizada em sistemas de rastreamento.

Filosofia

Os sistemas de reescrita podem ser vistos como programas que inferem efeitos finais de uma lista de relações de causa e efeito. Dessa forma, os sistemas de reescrita podem ser considerados provadores automatizados de causalidade .

Veja também

Notas

Referências

Leitura adicional

Reescrita de cordas
  • Ronald V. Book e Friedrich Otto, String-Rewriting Systems , Springer (1993).
  • Benjamin Benninghofen, Susanne Kemmerich e Michael M. Richter , Sistemas de Reduções . LNCS 277 , Springer-Verlag (1987).
De outros

links externos