A Formalization of Abstract Rewriting in Agda

Este artigo apresenta uma formalização construtiva de Sistemas de Reescrita Abstratos (ARS) no assistente de prova Agda, eliminando o uso de lógica clássica, refinando critérios de terminação e confluência e demonstrando a aplicabilidade geral através de uma formalização do cálculo lambda.

O essencial

Imagine que você está organizando uma grande biblioteca de livros antigos e empoeirados. Cada livro tem regras estranhas sobre como você pode reorganizá-los: às vezes você pode trocar a capa, às vezes pode mudar o título, e às vezes pode até rasgar uma página e colar outra. O objetivo é chegar a um estado final onde o livro está "perfeito" e não pode mais ser alterado.

O problema é: como você garante que, não importa por onde você comece a reorganizar, você sempre chegará ao mesmo livro final? E como garante que você nunca vai ficar preso em um ciclo infinito de mudanças, trocando a capa para frente e para trás eternamente?

Esse é o problema central que o artigo "Uma Formalização de Abstração de Reescrita em Agda" tenta resolver, mas de uma maneira muito especial.

Aqui está a explicação simples, usando analogias do dia a dia:

1. O que é "Reescrita Abstrata"?

Pense em "Reescrita Abstrata" como um manual de instruções universal para jogos de lógica. Não importa se você está jogando xadrez, resolvendo equações matemáticas ou organizando seus e-mails. Se existe uma regra que diz "se você tem o item A, você pode trocá-lo pelo item B", isso é um sistema de reescrita.

Os autores (Samuel Arkle e Andrew Polonsky) criaram um "manual mestre" desses jogos usando uma ferramenta chamada Agda. O Agda é como um arquiteto de software super rigoroso que não apenas verifica se suas regras fazem sentido, mas também escreve o código do jogo para você enquanto você prova que ele funciona.

2. O Grande Desafio: "Sem Truques de Mágica"

A maioria dos livros de matemática usa "truques de mágica" (lógica clássica) para provar que algo é verdade. Eles dizem: "Ou você chega ao final, ou não chega. Se não chega, é um absurdo, então você tem que chegar."

Os autores disseram: "Não, queremos ver o mágico fazendo o truque!"
Eles quiseram uma prova construtiva. Isso significa que, em vez de apenas dizer "o livro vai ficar perfeito", eles querem que o computador mostre exatamente como transformar o livro em sua versão perfeita, passo a passo. Se o computador não consegue fazer o passo a passo, a prova não vale.

3. Os Dois Grandes Objetivos do Jogo

No mundo desses jogos de reescrita, existem dois sonhos que todo mundo quer alcançar:

• Normalização Forte (Terminação): Garantir que o jogo nunca fique preso em um loop infinito. Você sempre chega a um ponto de parada (o livro perfeito).
  • Analogia: É como garantir que, não importa quantas vezes você misture as cartas, o baralho eventualmente vai parar de se mover e ficar em uma ordem específica.
• Confluência (Unicidade): Garantir que, não importa quais caminhos você escolha para reorganizar o livro, você sempre chegará ao mesmo livro final.
  • Analogia: Se você e seu amigo reorganizarem a mesma pilha de livros de maneiras diferentes, no final, os dois devem ter exatamente a mesma pilha organizada.

4. A Descoberta: "O Mapa é Mais Complexo do que Parecia"

Os autores pegaram um livro famoso chamado Terese (que é a "bíblia" dessas regras) e o reescreveram inteiramente para o Agda. Ao fazer isso, eles descobriram coisas novas:

• A Ponte de Ouro (Lemma de Newman): Existe uma regra famosa que diz: "Se o jogo sempre para (Normalização) E se ele tem uma propriedade local de não se perder (Confluência Fraca), então ele é perfeito (Confluência Total)."
  • A novidade: Eles mostraram que você pode usar uma versão mais fraca e fácil de provar dessa regra para chegar ao mesmo resultado, economizando esforço.
• O Mistério da Decisão: Para garantir que o jogo pare, às vezes precisamos saber se uma regra pode ser aplicada ou não. Em matemática pura, às vezes assumimos que sabemos isso. Mas no mundo real (computação), às vezes não sabemos. Eles mapearam exatamente onde precisamos dessa "sabedoria" e onde podemos viver sem ela.

5. Por que isso importa? (O Exemplo do Lambda Cálculo)

No final do artigo, eles mostram como isso serve para algo real: a Lógica Lambda (a base de linguagens de programação modernas como Haskell e partes do JavaScript).

Imagine que você está construindo um motor de carro (um programa). Você precisa ter certeza de que o motor não vai explodir (não entrar em loop infinito) e que, se dois mecânicos diferentes ajustarem o motor, o carro vai andar da mesma forma.
Graças ao trabalho deles, agora os programadores podem usar esse "manual mestre" para provar automaticamente que seus programas são seguros, sem ter que reinventar a roda para cada novo projeto.

Resumo em uma frase

Os autores criaram um guia de instruções infalível e prático para garantir que sistemas de regras (como programas de computador) sempre cheguem a um resultado final e único, sem usar "atalhos mágicos" da lógica, garantindo que tudo o que é provado possa ser executado como um código real.

Eles transformaram a teoria matemática abstrata em uma ferramenta de engenharia que funciona de verdade no computador.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "A Formalization of Abstract Rewriting in Agda", apresentado em português:

Resumo Técnico: Formalização de Reescrita Abstrata em Agda

1. O Problema
A teoria de Sistemas de Reescrita Abstrata (ARS) é fundamental para a fundamentação de linguagens de programação e lógica. No entanto, as apresentações clássicas dessa teoria (como no livro Terese de Bezem, Klop e De Vrijer) dependem extensivamente da lógica clássica (ex: Lei do Terceiro Excluído, prova por contradição). Isso cria uma barreira para a sua aplicação em assistentes de prova baseados em teoria de tipos construtiva, como o Agda.

O problema central abordado pelos autores é a necessidade de uma formalização construtiva e efetiva dos resultados fundamentais de ARS. Em um contexto construtivo, muitas implicações clássicas (como a de que "Normalização Forte implica Normalização Fraca") não são automaticamente válidas sem hipóteses adicionais de decidibilidade. Além disso, a falta de uma biblioteca construtiva robusta dificulta o desenvolvimento de teorias de linguagens de programação formalizadas que exijam computação efetiva a partir das provas.

2. Metodologia
Os autores desenvolveram uma biblioteca em Agda (um assistente de prova baseado na Teoria de Tipos de Martin-Löf) seguindo rigorosamente o paradigma Construtivo (Provas como Programas).

• Restrições de Design: A formalização evita axiomas clássicos, como extensão funcional, unicidade de provas de identidade (axioma K), univalência e, crucialmente, a Lei do Terceiro Excluído.
• Abordagem: Em vez de apenas verificar a validade de teoremas, as provas em Agda são programas que computam testemunhas explícitas. Por exemplo, uma prova de que um sistema é Church-Rosser gera automaticamente uma função que calcula um redutor comum entre termos convertíveis.
• Análise de Decidibilidade: O trabalho investiga onde a lógica clássica é necessária e identifica classes de sistemas (como TRS de primeira ordem e Cálculo Lambda) onde hipóteses de decidibilidade (ex: relação de reescrita decidível e ramificação finita) tornam os resultados efetivos.
• Revisão de Conceitos: Os autores redefiniram e refinaram conceitos de bem-fundamentação (well-foundedness), terminação e confluência para distinguir entre versões clássicas e construtivas.

3. Principais Contribuições

• Formalização Original de ARS: Uma implementação completa da teoria básica de ARS (baseada em Terese), cobrindo propriedades de terminação, confluência e suas inter-relações, pronta para uso em projetos maiores de teoria de linguagens de programação.
• Ontologia Refinada de Propriedades:
  • Introdução de novos conceitos, como Formas Mínimas (MF), Minimização Forte (SM) e Minimização Fraca (WM), para criar uma hierarquia mais granular entre terminação e confluência.
  • Substituição da propriedade de "Aumento" (Inc) por propriedades mais gerais e construtivas, como a Propriedade de Recorrência (RP) e a Propriedade de Recorrência Fraca (RP-).
• Generalização do Lema de Newman:
  • Os autores provam uma versão generalizada do Lema de Newman: WCR (Fraca Confluência) + SM (Minimização Forte) ⇒ CR (Confluência).
  • Isso é significativo porque permite provar a confluência em sistemas que não são fortemente normalizantes (SN), mas satisfazem a minimização forte, algo que a versão clássica não cobria diretamente sem assumir SN.
• Análise de Bem-Fundamentação Construtiva:
  • O artigo mapeia as relações lógicas entre várias definições de bem-fundamentação (acessível, indutiva, coredutiva, minimização, sequencial).
  • Demonstra que, construtivamente, essas definições não são equivalentes. Por exemplo, a implicação de que "todo elemento é acessível" a partir de "todo subconjunto não vazio tem um elemento mínimo" requer princípios clássicos.
  • Identifica que, para sistemas com ramificação finita e relação decidível, a implicação SN ⇒ WN (Normalização Forte implica Fraca) torna-se válida.

4. Resultados Chave

• Eficácia para Sistemas Práticos: A maioria dos resultados principais de ARS pode ser tornada completamente efetiva para exemplos práticos encontrados em sistemas de reescrita de primeira ordem (TRS) e Cálculo Lambda.
• Hierarquia de Implicações: As tabelas de implicações no artigo mostram exatamente quais combinações de propriedades (locais ou globais) são suficientes para garantir Confluência (CR) e Normalização Forte (SN).
  • Exemplo: A combinação de WN (Normalização Fraca) + UN→ (Propriedade de Forma Normal Única de Redução) implica CR sem necessidade de axiomas clássicos ou da propriedade WCR, diferentemente do caso clássico que exigiria SN.
• Validação no Cálculo Lambda: A biblioteca foi aplicada com sucesso na formalização do Cálculo Lambda não tipado. A estrutura de tipos aninhados (nested types) usada para representar termos lambda foi compatível com a teoria de ARS, permitindo derivar automaticamente propriedades como a decidibilidade de formas normais e a consistência equacional.

5. Significado e Impacto

• Infraestrutura para Teoria de Linguagens: O trabalho serve como uma "base de inicialização" (bootstrapping) para um repositório de teoria de linguagens de programação formalizada na Appalachian State University. Permite que teoremas complexos sejam provados reutilizando resultados gerais de ARS, em vez de serem reprovados a cada novo sistema.
• Computação a partir de Provas: Ao eliminar a lógica clássica, as provas geram algoritmos executáveis. Isso é crucial para aplicações onde se deseja não apenas saber que um sistema é confluente, mas extrair um algoritmo que compute o redutor comum.
• Refinamento Teórico: O artigo esclarece as nuances da lógica construtiva aplicada à reescrita, mostrando que muitas suposições clássicas são excessivas para casos práticos e propondo generalizações que ampliam o escopo dos teoremas (como o Lema de Newman generalizado).
• Guia para Futuras Formalizações: O trabalho estabelece princípios claros para formalizações futuras, enfatizando a necessidade de explicitar hipóteses de decidibilidade e evitar axiomas de igualdade não construtivos.

Em suma, o artigo transforma a teoria clássica de reescrita abstrata em uma ferramenta prática e computacionalmente efetiva dentro do ecossistema Agda, refinando conceitos teóricos e demonstrando sua aplicabilidade direta em sistemas complexos como o Cálculo Lambda.