Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Resumo Técnico: Uma Tática para Correspondência de Padrões no Autosubst

Problema
O artigo aborda uma limitação específica no framework Autosubst, um gerador de código para o assistente de prova Rocq (anteriormente Coq) que automatiza o raciocínio sobre termos de de Bruijn e substituição via $\sigma$-cálculo. Embora o Autosubst automatize com sucesso a verificação de igualdade para objetivos sem premissas usando a tática asimpl, ele falha quando os usuários tentam aplicar premissas (por exemplo, regras de tipagem ou lemas) a um objetivo por meio de táticas padrão como apply ou eapply.

Nesses cenários, o usuário deve unificar um objetivo com uma premissa módulo $\sigma$-equivalência. No entanto, a automação do Autosubst não foi projetada para realizar correspondência contra premissas. Consequentemente, os usuários são forçados a empregar contornos complicados, tais como:

• Formular regras em formas indiretas (usando variáveis meta-variáveis frescas em vez de termos de substituição diretos).
• Introduzir lemas auxiliares para fazer a ponte entre o objetivo e a premissa.
• Transformar manualmente objetivos ou instanciar explicitamente variáveis existenciais durante as provas.

A dificuldade central reside no fato de que a correspondência $\sigma$ (correspondência até a $\sigma$-equivalência) não é única; um único problema de correspondência pode admitir múltiplas soluções, das quais nem todas satisfazem as premissas do contexto. Além disso, a correspondência de segunda ordem para o $\lambda\sigma$-cálculo completo é indecidível e, mesmo sem a redução $\beta$, as soluções não são necessariamente únicas.

Metodologia
Os autores propõem uma tática heurística em desenvolvimento chamada as_apply, implementada na linguagem Ltac do Rocq, para automatizar a correspondência de padrões módulo $\sigma$-equivalência. A tática opera em duas fases primárias:

1. Pré-processamento:

   • Tanto o objetivo quanto a conclusão da premissa alvo são normalizados em relação ao $\sigma$-cálculo usando a tática asimpl existente.
   • Variáveis quantificadas na premissa são substituídas por variáveis existenciais (evars).
   • As premissas da premissa são convertidas em subobjetivos a serem resolvidos após a fase de correspondência.
   • A tática lida com conversões entre operações de renomeação explícita (ex: $s\langle\xi\rangle$) e operações de instanciação ($s[\xi]$) usando substify e renamify.

2. Fase de Correspondência:

   • A tática constrói um conjunto de equações de correspondência $M = \{s_i =_\sigma t_i\}$ entre os termos do objetivo e os termos da premissa instanciada.
   • Ela processa as equações da esquerda para a direita usando um procedimento parcial, $\sigma_{min}$, que tenta realizar a correspondência módulo o fragmento $\sigma_{min}$ (um subconjunto de regras $\sigma$ que caracteriza instanciação e composicionalidade).
   • Heurísticas: Se o $\sigma_{min}$ falhar em encontrar uma correspondência, a tática aplica um conjunto de heurísticas que capturam padrões comuns em desenvolvimentos formais. Estas incluem:
     • Lidar com equações da forma $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ ao instanciar o desconhecido com uma substituição elevada ($?s \mapsto s[\Uparrow\sigma]$).
     • Lidar com casos envolvendo substituições de identidade ou estruturas de variáveis específicas.
   • Após aplicar as substituições, a tática re-normaliza a premissa. O sucesso é determinado se o objetivo e a premissa tornarem-se sintaticamente iguais.

A tática foi generalizada para suportar toda a linguagem de entrada do compilador Autosubst, incluindo múltiplos sorts mutuamente indutivos, substituições de vetores e renomeações de primeira classe.

Principais Contribuições

1. Introdução de as_apply: Uma tática heurística projetada para substituir apply/eapply em desenvolvimentos baseados em Autosubst, permitindo a correspondência módulo $\sigma$-equivalência na presença de premissas.
2. Generalização: Extensão da lógica de correspondência para cobrir toda a sintaxe suportada pelo Autosubst, incluindo ligadores (binders) complexos e operações de renomeação.
3. Avaliação Empírica: Aplicação da tática em benchmarks padrão, especificamente os desafios POPLMark e POPLMark Reloaded.

Resultos
Os autores avaliaram o as_apply nos desafios POPLMark (642 linhas) e POPLMark Reloaded (683 linhas).

• Frequência de Uso: A tática foi usada 15 vezes na solução POPLMark B e 10 vezes na solução POPLMark Reloaded.
• Eficácia: Em todos os casos testados, o as_apply resolveu com sucesso os objetivos pretendidos.
• Simplificação: O uso da tática eliminou a necessidade de formulações de regras indiretas, lemas auxiliares e transformações manuais de objetivos que caracterizavam as soluções anteriores.
• Limitações: Os autores reconhecem que o as_apply não é $\sigma$-completo e não é um decisor. Como a correspondência $\sigma$ pode ter múltiplas soluções, a natureza heurística da tática significa que ela poderia, teoricamente, selecionar uma solução incorreta quando uma correta existe, embora nenhum erro desse tipo tenha sido observado nos estudos de caso.

Significância e Alegações
O artigo alega que, embora o problema teórico da correspondência $\sigma$ seja inerentemente difícil (soluções não únicas, indecidibilidade no $\lambda\sigma$ completo), uma abordagem pragmática e heurística pode recuperar um alto nível de automação na prática. A significância reside na redução do fardo manual para os usuários que trabalham com sintaxe de de Bruijn, permitindo que eles enunciem regras de tipagem e lemas em suas formas diretas e naturais, em vez de formas indiretas ajustadas às limitações do motor de unificação do assistente de prova.

Os autores mantêm-se modestos quanto ao estado atual do trabalho, rotulando-o como "Trabalho em Progresso". Eles observam que a tática atual depende de heurísticas devido ao potencial de soluções infinitas ou múltiplas. Trabalhos futuros visam identificar o maior fragmento $\sigma'$ para o qual um critério de unicidade se mantém, potencialmente levando a uma tática de correspondência com garantias comprovadas.