Templates in Rewriting Induction

1. Declaração do Problema

O artigo aborda um gargalo crítico na Indução por Reescrita (RI), um sistema formal utilizado para provar equivalência de programas (teoremas indutivos) em Sistemas de Reescrita de Termos (TRS). Embora a RI seja poderosa, sua aplicação prática a código do mundo real frequentemente falha devido à dificuldade de geração automática de lemas.

• O Problema da Divergência: Ao provar a equivalência de dois programas (por exemplo, diferentes implementações de uma função fatorial), o processo de prova frequentemente encontra uma sequência de equações que não correspondem. Técnicas padrão de RI (análise de casos e reescrita) geram novas equações, mas não conseguem utilizar as anteriores como hipóteses de indução porque os termos divergem estruturalmente.
• Limitações dos Métodos Existentes:
  • Métodos baseados em restrições (por exemplo, [9, 12]): Estes métodos tentam descobrir invariantes de laço (por exemplo, $z = a \times j$) para generalizar equações. Embora eficazes para aritmética simples, eles falham quando a relação entre variáveis é não polinomial ou quando a estrutura do laço é complexa.
  • Foco de baixo nível: Os métodos existentes operam no nível de valores específicos de variáveis e restrições, em vez de reconhecer construções de programação de alto nível (como recursão de cauda versus recursão geral).
• Contexto: Os autores focam em Sistemas de Reescrita de Termos Simplesmente Tipados com Restrições Lógicas (LCSTRSs), que modelam código de programação real com tipos de dados primitivos (inteiros, booleanos) e restrições lógicas (guardas), tornando-os mais adequados para verificação de programas do que os TRS padrão.

2. Metodologia

Os autores propõem uma abordagem de Geração de Lemas Baseada em Modelos que integra padrões de programação de alto nível no sistema de prova RI Limitado.

A. O Conceito de Modelos

Em vez de buscar invariantes aritméticos específicos, os autores definem Modelos: esquemas de reescrita que capturam construções comuns de programação (por exemplo, recursão de cauda ascendente/descendente, recursão geral).

• Quatro Modelos Principais:
  1. TailUp ($T^+$): Recursão de cauda ascendente (o índice aumenta).
  2. TailDown ($T^-$): Recursão de cauda descendente (o índice diminui).
  3. RecUp ($R^+$): Recursão geral ascendente.
  4. RecDown ($R^-$): Recursão geral descendente.
• Recursores de Ordem Superior: Estes modelos são formalizados como recursores de ordem superior (por exemplo, tailup, recdn). Um programa específico é correspondido a um modelo identificando uma função de contexto $F$ (a operação realizada no laço) e limites ($l, u$).

B. A Estratégia de Prova

A metodologia baseia-se em um processo de prova de duas etapas dentro da RI Limitada:

1. Equivalência Modelo-Recursor: Provar que uma implementação concreta de programa é equivalente ao seu recursor de ordem superior correspondente (por exemplo, facTU $\approx$ tailup). Isso é feito por indução estrutural sobre o índice do laço.
2. Equivalência de Recursores: Provar equivalências entre os recursores abstratos em si (por exemplo, tailup $\approx$ recdn).
   • Correspondência Unilateral: Transformar um lado da equação-alvo em um recursor e, em seguida, aplicar uma equivalência de recursor conhecida para simplificar o outro lado.
   • Correspondência Bilateral: Transformar ambos os lados em seus respectivos recursores e aplicar um teorema de equivalência geral diretamente.

C. Equivalências Condicionais

Para casos onde a equivalência simples não se sustenta (por exemplo, tailup versus taildn), os autores introduzem Teoremas Indutivos Limitados Condicionais. Estas provas dependem de axiomas (por exemplo, comutatividade e associatividade da operação $F$) e requisitos de ordenação específicos para garantir a terminação e a correção.

3. Contribuições Principais

1. Nova Heurística de Geração de Lemas: O artigo introduz um método que generaliza sobre estruturas de laço em vez de valores específicos de variáveis. Isso permite provar equivalências que anteriormente estavam fora do alcance dos geradores de invariantes baseados em restrições.
2. Integração com LCSTRS: A abordagem é projetada especificamente para Sistemas de Reescrita de Termos Simplesmente Tipados com Restrições Lógicas, permitindo a modelagem direta de aritmética de inteiros e guardas booleanas sem codificações complexas.
3. Abstração de Ordem Superior: Ao utilizar recursores de ordem superior, o sistema pode lidar com operações arbitrárias (como multiplicação em fatorial ou aplicação de função em exemplos de ordem superior) como parâmetros, tornando os modelos reutilizáveis em diferentes domínios.
4. Sistema de Prova Formal: Os autores definem as regras de dedução específicas (Simplificar, Caso, Deletar, Induzir, Hipótese) e os requisitos de ordenação necessários para integrar estes modelos ao framework RI Limitada.
5. Demonstração de Poder: O artigo prova com sucesso equivalências entre várias implementações de fatorial (Ascendente vs. Descendente, Cauda vs. Recursiva) e variantes de ordem superior, incluindo casos onde os invariantes necessários são não polinomiais.

4. Resultados

• Sucesso em Implementações de Fatorial: O sistema provou com sucesso a equivalência de quatro implementações diferentes de fatorial (Iterativa Ascendente/Descendente, Recursiva Ascendente/Descendente) sob a restrição $x \ge 1$.
  • Conquista Chave: Provar facTU $\approx$ facTD (Cauda Ascendente vs. Cauda Descendente) era impossível para métodos anteriores ([9, 12]) porque os invariantes necessários não eram polinomiais. A abordagem baseada em modelos resolveu isso ao reconhecer a similaridade estrutural dos laços.
• Extensões de Ordem Superior: O método foi estendido para funções de ordem superior (por exemplo, funfacTU), provando equivalência entre implementações que aplicam uma função $h$ ao índice do laço antes da multiplicação.
• Provas Condicionais: O sistema lidou com casos que exigiam axiomas (associatividade/comutatividade) para provar equivalências entre diferentes direções de recursão (por exemplo, tailup $\approx$ taildn se a operação for comutativa).

5. Significado

• Ponte entre Lacunas: Este trabalho preenche a lacuna entre a prova automática de teoremas de baixo nível (que luta com laços complexos) e a verificação de programas de alto nível. Desloca o foco de "encontrar o invariante correto" para "reconhecer o padrão correto".
• Escalabilidade: Ao abstrair valores aritméticos específicos, o método escala para comportamentos computacionais mais complexos onde invariantes polinomiais falham.
• Potencial de Automação: Embora atualmente implementado como um processo manual/semi-automático na ferramenta Cora, os autores argumentam que o reconhecimento de modelos é amplamente sintático, sugerindo alto potencial para automação completa em ferramentas futuras.
• Fundamental para Verificação de Programas: A abordagem fornece um framework robusto para verificar transformações de programas (por exemplo, otimizar uma função recursiva em uma recursiva de cauda) na presença de restrições lógicas, o que é essencial para verificar sistemas de software modernos.

Em resumo, Hagens e Kop apresentam uma mudança de paradigma na Indução por Reescrita: passando da descoberta de invariantes para a correspondência de padrões estruturais, permitindo a verificação de equivalências de programas que anteriormente eram inprováveis devido à complexidade de seus invariantes indutivos.