🔢 mathematics

Rewriting Systems on Arbitrary Monoids

Este artigo introduz sistemas de reescrita monoidais (MRS) como uma abstração de reescrita de strings sobre monoides ambientes arbitrários para abordar limitações lógicas de monoides livres, e estabelece uma biejunção canônica entre a 2-categoria de MRS Noetrianos Confluentes e a categoria de monoides enquanto classifica todos esses sistemas que apresentam um monóide fixo via Transformações de Tietze Elementares Generalizadas.

Autores originais: Eduardo Magalhães

Publicado 2026-02-02

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Eduardo Magalhães

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando resolver um quebra-cabeça onde possui um conjunto de regras para transformar uma coisa em outra. No mundo da ciência da computência e da matemática, isso é geralmente feito com cadeias de letras (como palavras em um dicionário). Se você tem a palavra "gato" e uma regra que diz que "gato" se torna "cachorro", você pode trocá-las. Esta é a forma tradicional de fazer as coisas, chamada Reescrita de Strings.

No entanto, o autor deste artigo, Eduardo Magalhães, faz uma pergunta simples, mas profunda: E se não estivermos apenas brincando com palavras? E se estivermos brincando com números, formas ou até mesmo ideias abstratas que não se parecem nada com palavras?

Aqui está uma decomposição das principais ideias do artigo usando analogias do cotidiano:

1. O Problema: Ser Exigente Demais com "Palavras"

Tradicionalmente, os sistemas de reescrita só funcionam em Monoideis Livres. Pense em um Monoideio Livre como um armazém gigante e vazio onde você só pode empilhar caixas (letras) em linha. Você só pode combiná-las unindo-as.

O Problema: O artigo argumenta que isso é muito limitante. É como dizer que você só pode rearranjar móveis se estiver em um armazém sem paredes. No mundo real (e na lógica), lidamos frequentemente com estruturas que possuem suas próprias regras internas (como um relógio onde 12 + 1 = 1, ou um grupo de amigos onde "Alice + Bob" é apenas "O Grupo").
A Lacuna Lógica: O autor aponta que "ser um armazém livre" é uma regra muito específica e difícil de definir na linguagem da lógica. Se você quiser estudar esses sistemas usando ferramentas lógicas padrão, você fica travado porque não consegue definir facilmente o que é "livre" dentro do próprio sistema.

2. A Solução: Sistemas de Reescrita Monoidais (MRS)

O autor introduz os Sistemas de Reescrita Monoidais (MRS).

A Analogia: Em vez de apenas rearranjar letras em uma linha, imagine que você tem uma caixa de ferramentas (um Monoide). Esta caixa de ferramentas tem uma maneira específica de combinar ferramentas (multiplicação).
- Em um sistema de strings, você só pode colar "A" e "B" para fazer "AB".
- Em um MRS, você pode combinar quaisquer dois itens em sua caixa de ferramentas, desde que eles sigam as regras da caixa. Talvez sua caixa de ferramentas seja um conjunto de números onde você os soma, ou um conjunto de formas onde elas se sobrepõem.
A Mudança: O artigo diz: "Vamos parar de fingir que tudo é uma palavra. Vamos deixar as regras trabalharem diretamente nos próprios objetos". Isso torna o sistema mais flexível e "interno" à estrutura que ele descreve.

3. O Estado "Perfeito": Noetherian e Confluente

Em qualquer jogo de reescrita, você quer que duas coisas aconteçam:

Noetherian (Terminação): O jogo deve eventualmente terminar. Você não pode ficar mudando as coisas para sempre em um loop. (ex: Você não pode ter uma regra que transforma "A" em "B" e "B" de volta em "A" para sempre).
Confluente (Consistência): Não importa em qual ordem você aplique as regras, você deve chegar ao mesmo resultado final. (ex: Se você tem um quarto bagunçado, não deve importar se você recolhe as meias primeiro ou os livros primeiro; o quarto deve terminar limpo da mesma forma).

Quando um sistema possui ambos, você pode pegar qualquer entrada bagunçada e reduzi-la a uma "Forma Normal" única (a versão mais limpa e simples daquele objeto).

4. A Grande Conexão: O "Tradutor" (Biadjunção)

O artigo constrói uma ponte entre dois mundos:

Mundo A: O mundo bagunçado e cheio de regras dos Sistemas de Reescrita (MRS).
Mundo B: O mundo limpo e simples dos Monoides (as estruturas finais).

O autor cria um Tradutor (uma ferramenta matemática chamada biadjunção) que funciona nos dois sentidos:

Das Regras para a Estrutura: Se você tem um conjunto de regras, o tradutor encontra a estrutura "limpa" escondida nelas (o Monoide dos irreduzíveis).
Da Estrutura para as Regras: Se você tem uma estrutura limpa (como o número 5), o tradutor pode construir um conjunto "canônico" de regras que a gera.

A Metáfora: Imagine que você tem uma escultura (o Monoide).

Uma maneira de descrevê-la é dizer: "É feita de argila". (A Estrutura).
Outra maneira é dar uma lista de instruções: "Pegue um pedaço, achate-o, corte um círculo, suavize as bordas". (O Sistema de Reescrita).
O artigo prova que essas duas descrições estão perfeitamente ligadas. Você pode ir das instruções para a escultura, e da escultura de volta para o melhor conjunto possível de instruções, sem perder nenhuma informação.

5. As Transformações de "Tietze": As Varinhas Mágicas

Finalmente, o artigo responde a uma pergunta complicada: "Se eu tiver dois conjuntos diferentes de regras que constroem a mesma escultura, como eles se relacionam?"

No velho mundo da reescrita de strings, havia um conjunto famoso de movimentos chamados Transformações de Tietze que podiam transformar um conjunto de regras em outro. O autor inventa as Transformações de Tietze Elementares Generalizadas (GETTs) para este novo mundo mais amplo.

A Analogia: Imagine que você tem duas receitas diferentes para fazer um bolo.
- Receita A diz: "Misture farinha, açúcar, ovos".
- Receita B diz: "Misture ingredientes secos, depois ingredientes úmidos, então asse".
- Embora os passos pareçam diferentes, eles fazem o mesmo bolo.
O Resultado: O artigo prova que você pode transformar qualquer receita válida (MRS Noetherian Confluente) em qualquer outra receita válida para o mesmo bolo usando uma sequência desses "movimentos GETT".
- Movimento 1: Adicionar uma regra que já é verdadeira (redundante).
- Movimento 2: Remover uma regra que já é coberta por outras.
- Movimento 3: Introduzir um novo ingrediente (símbolo) para ajudar a explicar um passo.
- Movimento 4: Um movimento complexo que simplifica todo o sistema ao focar em uma parte específica das regras.

Resumo

Este artigo pega o conceito de "reescrita" (mudar coisas baseando-se em regras) e o liberta da restrição de "palavras". Ele mostra que:

Você pode fazer isso em qualquer estrutura matemática, não apenas em strings.
Existe uma ponte lógica perfeita entre as regras e o resultado.
Quaisquer dois conjuntos de regras que produzem o mesmo resultado podem ser transformados um no outro usando um conjunto específico e universal de movimentos.

É um pouco como perceber que, embora você possa descrever uma casa listando seus tijolos (strings), você também pode descrevê-la pelo seu projeto arquitetônico (monoide), e pode provar matematicamente que todo projeto tem um conjunto único e perfeito de instruções para construí-lo, e que cada conjunto de instruções leva a um projeto único.

Resumo Técnico: Sistemas de Reescrevimento em Monoides Arbitrários

Enunciado do Problema
O estudo de sistemas de reescrevimento tem sido historicamente dominado pelos Sistemas de Reescrevimento de Strings (SRS), onde as reduções são definidas sobre monoides livres gerados por um alfabeto. Embora o SRS forneça um arcabouço robusto para resolver o problema da palavra e analisar estruturas algébricas, ele possui uma limitação estrutural: está intrinsecamente vinculado a monoides livres. Do ponto de vista lógico, isso cria um descompasso fundamental. A classe de monoides livres não é axiomatizável em primeira ordem; consequentemente, ao aplicar métodos de primeira ordem ou de teoria modelos a apresentações de reescrevimento, a propriedade de "liberdade" não pode ser tratada internamente, mas deve ser imposta como uma condição semântica externa. Além disso, o reescrevimento clássico depende fortemente da representação sintática de palavras, o que pode não ser estritamente necessário para as propriedades algébricas subjacentes da redução, tais como confluência e terminação.

Metodologia
Para abordar essas limitações, o artigo introduz os Sistemas de Reescrevimento Monoidais (MRS), uma abstração onde as reduções são definidas diretamente sobre um monoide ambiente arbitrário $(M, \cdot)$ em vez de um monoide livre de palavras. Um MRS é definido como uma terna $(M, \cdot, R)$ , onde $R \subseteq M \times M$ é uma relação binária. A relação de redução $a \to_R b$ é definida pela existência de $x, y, s, t \in M$ tal que $a = xsy$, $b = xty $, e$ (s, t) \in R$.

A metodologia procede através de três etapas principais:

Generalização Algébrica: O artigo estabelece que as propriedades fundamentais de SRS (como a propriedade de Church-Rosser, Noetherianidade e a existência de formas normais únicas) generalizam-se diretamente para MRS. Prova-se que, para um MRS confluente e Noetherian, o conjunto de elementos irredutíveis forma um monoide isomorfo ao monoide quociente $M / \leftrightarrow^*_R$ .
Formulação Categórica: Os sistemas são organizados dentro de um arcabouço 2-categórico estrito. O autor define $\mathbf{NCRS}_2$ como a 2-categoria de MRS Noetherianos Confluentes, onde 0-células são os sistemas, 1-células são homomorfismos que preservam a estrutura de redução, e 2-células representam equivalências entre homomorfismos. Esta estrutura é comparada à 2-categoria de monoides, $\mathbf{Mon}$ .
Teoria de Transformação: Para classificar a família de MRS que apresentam um monoide fixo, o artigo introduz as Transformações de Tietze Elementares Generalizadas (GETTs). Estas são quatro tipos de operações (adicionar/remover regras, adicionar novos geradores e colapsar subconjuntos coerentes de regras) adaptadas ao contexto de monoide arbitrário.

Contribuições Principais e Resultados

Definição de MRS e Propriedades Fundamentais: O artigo formaliza o MRS e demonstra que as restrições sintáticas de monoides livres não são necessárias para os lemas centrais da teoria de reescrevimento. Prova que o quociente de um MRS pela sua relação de congruência é isomorfo ao monoide de seus elementos irredutíveis.
Biadjunção entre $\mathbf{NCRS}_2$ e $\mathbf{Mon}$ : Um resultado central é a existência de uma biadjunção canônica entre a 2-categoria de MRS Noetherianos Confluentes ( $\mathbf{NCRS}_2$ $NCRS_{2}$ ) e a 2-categoria de monoides ( $\mathbf{Mon}$ $Mon$ ).
- O adjunto à direita $I: \mathbf{NCRS}_2 \to \mathbf{Mon}$ mapeia um sistema para seu monoide de irredutíveis.
- O adjunto à esquerda $G: \mathbf{Mon} \to \mathbf{NCRS}_2$ constrói um MRS "canônico", Noetheriano e confluente para qualquer dado monoide $M$ , utilizando o monoide livre gerado por $M \setminus \{1\}$ e codificando a multiplicação do monoide como regras de redução.
- Esta biadjunção estabelece uma propriedade universal: mapas de uma apresentação canônica $G(M)$ para qualquer sistema $A$ correspondem unicamente (até isomorfismo de 2-célula) a homomorfismos de monoide de $M$ para o monoide de irredutíveis de $A$ .
Teorema de Tietze Generalizado: O artigo generaliza o Teorema de Tietze para o contexto de monoides arbitrários. Define quatro tipos de GETTs e prova que quaisquer dois MRS Noetherianos confluentes que apresentam o mesmo monoide estão conectados por uma sequência (possivelmente infinita) destas transformações. Especificamente, se dois sistemas apresentam o mesmo monoide $M$ , um pode ser transformado no outro usando no máximo $|B|$ GETTs, onde $|B|$ é a cardinalidade do conjunto subjacente do sistema alvo.

Significância
O artigo afirma que este trabalho fornece uma caracterização completa de sistemas geradores para um monoide até a equivalência por GETT, removendo a dependência de monoides livres. Ao deslocar o cenário de monoides livres para monoides arbitrários, o arcabouço permite que sistemas de reescrevimento sejam tratados internamente na lógica de primeira ordem e na teoria de modelos, uma vez que a restrição de "liberdade" não é mais um pré-requisito para a definição do sistema.

Além disso, a organização 2-categórica destes sistemas oferece uma perspectiva de dimensão superior sobre o reescrevimento. Trata sistemas geradores não meramente como apresentações estáticas, mas como estruturas dinâmicas onde equivalências entre sistemas podem ser estudadas usando ferramentas categóricas. O resultado da biadjunção esclarece especificamente a relação entre mapas de monoide "semânticos" e mapas "sintáticos" de sistemas de reescrevimento, mostrando que estes últimos são unicamente determinados pelos primeiros até a estrutura inerente de 2-dimensão de $\mathbf{NCRS}_2$ .

O trabalho também fornece diversos exemplos ilustrando a versatilidade do MRS, incluindo aplicações a espaços topológicos (operadores de fechamento), toposes elementares (topologias de Lawvere-Tierney) e teorias de Horn em lógica, demonstrando que a estrutura monoidal é o componente essencial para o reescrevimento, e não a sintaxe específica de palavras.