The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

Resumo Técnico: A Ordem de Caminho de Computabilidade para Reescrevendo de Ordem Superior $\beta\eta$-Normal

Problema
A reescrita de ordem superior abrange vários formalismos, notadamente a reescrita de ordem superior "comum" (usando correspondência sintática e tratando a redução $\beta$ como uma regra de reescrita) e a reescrita de ordem superior "normal" (usando correspondência módulo $\beta\eta$ e considerando termos em suas formas normais $\beta\eta$). Embora existam métodos de terminação poderosos para a reescrita comum, como a Ordem de Caminho de Computabilidade (CPO), adaptar estes para a reescrita de ordem superior normal (especificamente Sistemas de Reescrita de Ordem Superior ou HRSs à la Nipkow) apresenta desafios significativos.

Métodos existentes para HRSs, como a NHORPO (Ordem de Caminho Recursiva de Ordem Superior Normal), frequentemente dependem de uma técnica de transformação chamada "neutralização" para lidar com sistemas onde a ordem central falha. No entanto, a neutralização complica a automação. Além disso, as ordens de caminho padrão têm dificuldade com a reescrita normal porque ordens bem fundadas compatíveis com $\beta\eta$ são geralmente não monótonas (fechadas sob contextos) ou não estáveis (fechadas sob substituições) no sentido tradicional. Por exemplo, se uma ordem é compatível com $\beta\eta$ e fechada sob contextos, ela pode levar a contradições como $c > c$, violando a bem-fundação.

Metodologia
Os autores propõem elevar a Ordem de Caminho de Computabilidade (CPO), originalmente definida para reescrita de ordem superior comum, para o cenário da reescrita de ordem superior $\beta\eta$-normal. A ordem resultante é denominada Ordem de Caminho de Computabilidade $\beta\eta$-normal (NCPO).

A metodologia baseia-se nos seguintes componentes principais:

1. Par de Ordem de Redução: Seguindo a abordagem de Jouannaud e Rubio, os autores definem uma ordem de redução como um par $(>, \sqsupset)$, onde $>$ é a ordem primária (NCPO) e $\sqsupset$ é uma variante "comum" (CPO). O par satisfaz a estabilidade $\beta\eta$-normal: se $s > t$, então $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ para todas as substituições $\sigma$, onde $\downarrow$ denota a $\beta\eta$-normalização. Isso permite que a prova de terminação dependa da bem-fundação e da monotonicidade do componente CPO comum.
2. Termos Não Versáteis: Uma inovação técnica crítica é a restrição da aplicação da ordem a termos não versáteis. Um termo é não versátil se a substituição e a subsequente $\beta\eta$-normalização apenas afetam seus subtermos próprios. Os autores fornecem uma condição suficiente melhorada para a não versatilidade (Lema 1) em comparação com trabalhos anteriores, o que é essencial para provar a estabilidade da ordem.
3. Extensões a partir de CPO: A NCPO incorpora duas extensões principais da CPO original:
   • Subtermos Acessíveis: Estes permitem que comparações recursivas ignorem diminuições estritas de tipo em casos específicos determinados por posições de tipo (posições de tipo base positivas/negativas).
   • Símbolos Pequenos: Este recurso permite que certos símbolos de função sejam tratados como "pequenos", possibilitando provas de terminação para sistemas onde as ordens de caminho recursivas padrão falham (ex: funções de processamento de listas).
4. Conjunto de Regras: A ordem é definida indutivamente via um conjunto de regras (Figura 1) que lida com símbolos de função (grandes e pequenos), aplicações e abstrações. Notavelmente, as regras para orientar reduções $\beta$ e $\eta$ são removidas, pois a ordem opera diretamente sobre formas normais. Uma nova regra, $\langle \lambda\triangleright\eta \rangle$, é introduzida para lidar com casos específicos envolvendo expansão $\eta$ no contexto de subtermos acessíveis.

Contribuições Principais

• Definição de NCPO: O artigo define formalmente a NCPO, a primeira ordem de caminho de computabilidade especificamente projetada para reescrita de ordem superior $\beta\eta$-normal que integra subtermos acessíveis e símbolos pequenos.
• Prova de Correção: Os autores provam que o par $(>_\tau, \sqsupset_\tau)$ constitui uma ordem de redução de ordem superior $\beta\eta$-normal válida (Teorema 2), garantindo assim a terminação para qualquer HRS compatível com ela.
• Condição de Não Versatilidade Melhorada: O artigo oferece uma condição de suficiência refinada para a não versatilidade, que é mais forte do que a fornecida no trabalho fundamental sobre NHORPO.
• Automação via SAT/SMT: Os autores argumentam que a NCPO é mais propensa à automação do que a NHORPO com neutralização. Enquanto a neutralização exige uma análise sintática complexa de termos transformados dependentes de parâmetros simbólicos (tornando a codificação SMT difícil), os parâmetros da NCPO (precedência, ordens de tipo, status) podem ser codificados de forma mais direta.

Resultados
Os autores implementaram um protótipo de NCPO em Haskell, utilizando o pacote Hasmtlib para codificar problemas de terminação no formato SMT-LIB 2 e resolvê-los usando o solver Z3. Os resultados experimentais (Tabela 1) comparam a NCPO contra a NHORPO (com e sem neutralização), bem como implementações de HORPO em WANDA e CSI$^{ho}$.

• Superioridade sobre a NHORPO: A NCPO prova com sucesso a terminação de vários sistemas onde a NHORPO (mesmo com neutralização) falha. Especificamente:
  • Exemplo 8 (Incremento de lista): A NCPO prova a terminação usando símbolos pequenos, um recurso ausente na NHORPO.
  • Exemplo 7 (Formas Normais de Negação): A NCPO prova a terminação usando subtermos acessíveis, enquanto a NHORPO com neutralização falha em orientar as regras devido à incapacidade de lidar com termos versáteis na comparação.
• Poder Incomparável: O estudo identifica casos (ex: neutr.p) onde a NHORPO com neutralização tem sucesso, mas a NCPO falha, demonstrando que as duas abordagens possuem poderes incomparáveis.
• Eficiência: A busca por parâmetros para a NCPO mostra-se computacionalmente eficiente, muitas vezes levando um tempo comparável às buscas da NHORPO, enquanto a busca pelos parâmetros de neutralização pode explodir em complexidade.

Significância e Alegações
O artigo alega que a NCPO fornece uma alternativa poderosa e leve à combinação de NHORPO e neutralização. Os autores enfatizam que, embora a NHORPO com neutralização seja uma forte competidora, a complexidade de automatizar a técnica de neutralização torna a NCPO uma escolha mais prática para a prova automática de terminação em reescrita de ordem superior normal.

Os autores observam modestamente que a transitividade da NCPO permanece uma questão em aberto, pois a inclusão da redução $\beta$ na ordem comum subjacente justifica a não-transitividade para CPO e NHORPO, mas as propriedades específicas da NCPO requerem investigação adicional. Além disso, sugerem que integrar a NCPO em técnicas de pares de dependência para reescrita de ordem superior normal é um próximo passo lógico. O artigo conclui destacando a necessidade de formalizações de métodos de terminação de ordem superior para evitar erros encontrados na literatura anterior, como alegações incorretas sobre a solvabilidade de certos exemplos pela NHORPO.