Towards an HRS Category in TermCOMP

Resumo Técnico: Rumo a uma Categoria HRS no TermCOMP

Problema
A competição anual de terminação (TermCOMP) inclui uma categoria para reescrita de ordem superior. Historicamente, esta categoria tem utilizado a semântica de Sistemas Algébricos Funcionais (AFSs), que dependem de correspondência simples (plain matching) e regras explícitas de $\beta$-redução. Embora os Sistemas de Reescrita de Ordem Superior (HRSs) de Nipkow, que realizam reescrita módulo $\beta\eta$ e tipicamente utilizam padrões de Miller (PRSs) ou o mais recente Sistema de Reescrita de Padrões Determinísticos de Ordem Superior (DPRSs), sejam formalismos bem estabelecidos, eles não foram totalmente integrados ao framework competitivo do TermCOMP. O desafio reside em reconciliar a semântica dos HRSs (reescrita módulo $\beta\eta$) com o atual framework do TermCOMP (baseado em AFSs e meta-substituições) para permitir que ferramentas voltadas para HRSs possam competir diretamente contra aquelas voltadas para AFSs.

Metodologia
Os autores propõem uma ponte formal entre os HRSs e a atual semântica de ordem superior do TermCOMP, definida como Sistemas de Reescrita de Meta-Substituição de Ordem Superior Simplesmente Tipados (STMRSs). A metodologia envolve três etapas principais:

1. Generalização de Padrões: Os autores introduzem os Sistemas de Reescrita de Padrões Estendidos (EPRSs), uma subclasse de HRSs que generaliza tanto PRSs quanto DPRSs. Os EPRSs utilizam "Padrões Estendidos" (EPATs), que relaxam as restrições de correspondência determinística dos DPRSs, mantendo uma estrutura onde variáveis livres são aplicadas a argumentos de não-abstração. Esta classe é definida primordialmente para facilitar a prova teórica, em vez de servir como uma ferramenta prática autônoma.
2. Extensão da Semântica STMRS: Os autores estendem a definição das regras STMRS (o padrão atual do TermCOMP) para permitir que os lados esquerdos sejam EPATs em vez de apenas padrões padrão. Eles introduzem o conceito de termos bem-comportados (well-behaved) e quase-bem-comportados (quasi-well-behaved). Estas restrições sintáticas garantem que, quando as meta-substituições são aplicadas, os termos resultantes permaneçam em forma normal $\beta$ (especificamente forma normal longa $\beta\eta$) sem gerar novos $\beta$-redexes que exigiriam passos de redução adicionais.
3. Implementação via Reescrita Normalizada: A contribuição técnica central é estabelecer que a reescrita em um STMRS bem-comportado, seguida de $\beta$-normalização, simula a reescrita em o correspondente EPRS. Os autores definem uma tradução entre substituições ordinárias (usadas em EPRSs) e meta-substituições (usadas em STMRSs) para provar que os dois sistemas são equivalentes em relação à terminação.

Principais Contribuições

• Definição de EPRSs: Uma nova subclasse sintática de HRSs que generaliza os DPRSs, permitindo uma gama mais ampla de benchmarks enquanto mantém propriedades de correspondência gerenciáveis.
• Restrições Sintáticas para Equivalência: A introdução de regras STMRS "bem-comportadas". Estas regras restringem os lados esquerdos para serem bem-comportados e os lados direitos para serem quase-bem-comportados. Isso garante que a aplicação de meta-substituições não crie $\beta$-redexes, preservando a forma normal $\beta$ dos termos.
• Teorema de Equivalência Formal: O artigo prova que, para um STMRS bem-comportado $R$ e um termo $s$ em forma normal longa $\beta\eta$, um passo de reescrita na semântica EPRS ($s \to_R t$) ocorre se, e somente se, um passo de reescrita na semântça STMRS seguido de $\beta$-normalização ocorre ($s \Rightarrow_R \cdot \Rightarrow!_\beta t$).

Resultos
O resultado principal é o Teorema 15, que estabelece a correspondência entre as relações de reescrita dos STMRSs bem-comportados e seus correspondentes EPRSs. Especificamente:

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ se, e somente se, $s \to_R t$ (vendo $R$ como um EPRS).
• Isto leva ao Corolário 20, que afirma que a terminação da estratégia "reescrever então $\beta$-normalizar" em um STMRS bem-comportado coincide com a terminação universal do correspondente EPRS.

Os autores demonstram que esta equivalência se mantém para termos em forma normal longa $\beta\eta$. Eles observam que, para STMRSs de segunda ordem, a correspondência é ainda mais forte, oferecendo um mapeamento um-para-um entre os passos, pois as meta-substituições não podem criar $\beta$-redexes naquele contexto específico.

Significância
O artigo afirma estabelecer a fundação formal para uma (sub)categoria de HRS no TermCOMP. Ao definir um subconjunto de benchmarks sintaticamente verificável (STMRSs bem-comportados) dentro do formato TPDB existente, os autores permitem:

1. Competição Direta: Ferramentas projetadas para HRSs (usando reescrita $\beta\eta$) podem agora competir contra ferramentas projetadas para AFSs dentro da mesma categoria, uma vez que suas propriedades de terminação são provadas como coincidentes sob as semânticas propostas.
2. Suporte de Ferramentas Mais Amplo: O resultado de implementação permite a comparação de propriedades além da mera terminação, pois a simulação é baseada em uma correspondência passo a passo, em vez de apenas uma propriedade de terminação global.
3. Refinamento de Trabalhos Existentes: O resultado fortalece implementações anteriores de PRSs em AFSMs (Kop) e sistemas combinatórios (van Oostrom e van Raamsdonk) ao estendê-las para uma classe mais geral de HRSs (EPRSs) e fornecer uma prova rigorosa da equivalência entre reescrita normalizada e reescrita de ordem superior.

Os autores mantêm-se modestos quanto ao escopo, reconhecendo que o resultado não cobre todos os HRSs porque a meta-substituição é estritamente menos poderosa que a substituição de ordem superior completa. No entanto, argumentam que a subclasse definida é suficiente para acomodar uma parte significativa dos benchmarks existentes e os DPRSs específicos introduzidos em seu trabalho anterior.