Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs

Resumo Técnico: Compressão para Reescrita Coindutiva Infinitária

Título Original: Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs
Autores: Rémy Cerda e Alexis Saurin

1. O Problema (Problem)

O artigo aborda o estudo de objetos infinitos (como termos de $\lambda$-cálculo infinitários ou árvores de derivação de provas não-bem-fundadas) e sua dinâmica de reescrita. Tradicionalmente, a reescrita infinitária é tratada através de sequências de passos indexadas por ordinais arbitrários, utilizando conceitos de convergência métrica e topológica.

O problema central é a propriedade de compressão. Em sistemas de reescrita infinitária, uma sequência de passos de comprimento ordinal muito grande (ex: $\omega \cdot 2$) pode ser "comprimida" em uma sequência de comprimento $\omega$. A compressão é crucial porque garante que aproximações finitas do limite de um processo possam ser computadas em tempo finito. Sem a compressão, o sistema pode ser "não-produtivo" do ponto de vista computacional, pois exigiria passos transfinitos para produzir resultados que deveriam ser visíveis em etapas finitas.

O desafio específico que os autores enfrentam é a falta de uma apresentação coindutiva unificada que englobe tanto a reescrita de termos (como o $\lambda$-cálculo) quanto a reescrita de provas (eliminação de cortes em sistemas não-bem-fundados), permitindo provas de compressão que não dependam de indução transfinita direta sobre ordinais.

2. Metodologia (Methodology)

Os autores propõem uma mudança de paradigma: em vez de usar completamento métrico (topologia), eles utilizam a coindução para definir objetos e processos infinitos. A metodologia divide-se em três pilares:

1. Apresentação Genérica: Eles introduzem um framework de "árvores de derivação" que utiliza regras mistas (indutivas e coindutivas). Isso permite modelar qualquer objeto sintático construído por indução e coindução simultaneamente.
2. Formalismo Coindutivo de Reescrita: Definem a reescrita infinitária ($\to^\infty$) como a união de relações indexadas por ordinais ($\to^\gamma_\infty$), onde a progressão é controlada por regras de "levantamento" (lift) e "divisão" (split), permitindo uma descrição puramente coindutiva.
3. Caracterização da Compressão: Em vez de provar a compressão caso a caso, eles desenvolvem uma propriedade lógica (denotada como $Q$) que serve como condição necessária e suficiente para que um sistema de reescrita seja compressível.

3. Principais Contribuições (Key Contributions)

• Framework Unificado: Uma apresentação genérica que unifica a reescrita de termos de primeira ordem, o $\lambda$-cálculo infinitário e a eliminação de cortes em provas não-bem-fundadas.
• Teorema de Caracterização da Compressão: O principal resultado teórico é o Teorema 14, que identifica a propriedade $Q$. Esta propriedade permite verificar a compressibilidade de um sistema analisando apenas como os passos de reescrita interagem com padrões de derivação, sem recorrer à complexidade da indução transfinita.
• Prova Coindutiva Direta: Ao contrário de trabalhos anteriores que usavam "atalhos" via sequências de ordinais, os autores fornecem um procedimento coindutivo explícito para comprimir derivações.
• Aplicação à Teoria de Provas: A aplicação do framework ao sistema $\mu\text{MALL}_\infty$ (Lógica Linear Aditiva-Multiplicativa com pontos fixos), provando que a eliminação de cortes nesse sistema possui a propriedade de compressão.

4. Resultados (Results)

• Generalidade: O framework provou ser capaz de recuperar resultados conhecidos para reescrita de primeira ordem e $\lambda$-cálculo, mas de forma mais elegante e unificada.
• Prova de Compressão para $\mu\text{MALL}_\infty$: Os autores demonstraram que, para o sistema de lógica linear com pontos fixos, a eliminação de cortes (que envolve regras complexas de multicut) satisfaz a propriedade $Q$. Isso é alcançado mostrando que todos os passos de raiz da reescrita transformam padrões finitos em padrões finitos (Lemmas de Pattern Extraction e Pattern Filling).
• Equivalência de Definições: Demonstraram que a definição coindutiva de reescrita é equivalente à definição topológica baseada em convergência forte.

5. Significância (Significance)

Este trabalho é significativo por dois motivos principais:

1. Teórico: Ele fornece a base matemática para uma "Teoria de Provas Não-Bem-Fundada" puramente coindutiva. Isso facilita a formalização de metateorias de lógicas complexas (com operadores de ponto fixo) em assistentes de prova como o Coq/Rocq, onde a coindução é uma ferramenta nativa e poderosa.
2. Prático/Computacional: Ao garantir a compressão, o trabalho assegura que os processos de eliminação de cortes em sistemas de lógica circular ou com pontos fixos sejam "produtivos". Isso significa que, embora o processo de prova possa ser infinito, qualquer parte finita do resultado pode ser obtida em um número finito de passos, validando a aplicabilidade desses sistemas em busca de provas e computação reativa.