Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

Resumo Técnico: Indecidibilidade Mecanizada de $\beta$-Matching de Ordem Superior

Enunciado do Problema
O artigo aborda o problema de decisão do $\beta$-matching de ordem superior no $\lambda$-cálculo simplesmente tipado. Dados dois termos $\lambda$ simplesmente tipados, $F$ e $N$, onde $N$ não contém variáveis livres, o problema questiona se existe um termo $M$ tal que a aplicação $F M$ seja $\beta$-equivalente a $N$. Embora a indecidibilidade da $\beta$-unificação de ordem superior tenha sido estabelecida por Huet na década de 1970, a decidibilidade do $\beta$-matching permaneceu em aberto até que Loader provou sua indecidibilidade em 2003. A prova de Loader baseou-se em uma redução de uma variante da $\lambda$-definibilidade, utilizando uma maquinaria intrincada para formular restrições que especificam funções finitas arbitrárias.

Metodologia
O autor apresenta uma nova prova de indecidibilidade que diverge da abordagem de Loader ao evitar totalmente a $\lambda$-definibilidade. Em vez disso, a prova codifica uma forma restrita de reescrita de strings, especificamente o Problema $0^+ \Rightarrow^* 1^+$ dentro de sistemas semi-Thue simples, diretamente no $\beta$-matching de ordem superior.

A metodologia procede através das seguintes etapas:

1. Ponto de Partida: A redução começa com o Problema indecidível $0^+ \Rightarrow^* 1^+$, que pergunta se uma sequência não vazia de $0$s pode ser transformada em uma sequência não vazia de $1$s usando um conjunto de regras de reescrita da forma $ab \Rightarrow cd$. Este problema já é conhecido como indecidível e é mecanizado na Biblioteca de Provas de Indecidibilidade do Coq.
2. Estratégia de Codificação: O autor constrói termos $\lambda$ simplesmente tipados para simular o processo de reescrita. A codificação captura dois aspectos principais:
   • Expansão e Inicialização de Palavras: Termos são construídos para representar a expansão de uma palavra inicial de comprimento $n$ e sua inicialização com $0$s.
   • Passos de Reescrita: Termos representam a aplicação de regras de reescrita em posições específicas dentro da palavra.
3. Restrições Sintáticas e Semânticas: Para garantir que a solução do termo $\lambda$ represente fielmente o processo de reescrita sem soluções "ad hoc" (ex: termos que ignoram argumentos ou constroem resultados arbitrariamente), o autor emprega restrições de tipagem específicas e verificações de $\beta$-equivalência.
   • Restrições Sintáticas: Ao utilizar uma variável livre $u$ e o termo identidade $I$ em contextos específicos (inspirados por Dowek e Urzyczyn), o autor restringe a forma de potenciais soluções para termos "bem formados". Isso impede que soluções introduzam abstrações $\lambda$ desnecessárias ou ignorem argumentos fornecidos.
   • Restrições Semânticas: O autor define um conjunto de termos tipados ($G_\star, G_0, G_{ab \Rightarrow cd}$) que atuam como intérpretes para as regras de reescrita. Esses termos são usados em restrições de $\beta$-equivalência para verificar se uma solução candidata simula corretamente a transição de uma sequência de $0$s para uma sequência de $1$s.
4. Mecanização: Toda a prova é mecanizada no Rocq Prover (anteriormente Coq). A mecanização é livre de axiomas e abrange aproximadamente 4.000 linhas de código, cobrindo a definição do $\lambda$-cálculo simplesmente tipado, a lógica de redução e o resultado final de indecidibilidade.

Principais Contribuições

• Redução Inovadora: O artigo fornece uma nova redução do Problema $0^+ \Rightarrow^* 1^+$ para o $\beta$-matching de ordem superior. Isso contorna a complexa maquinaria de $\lambda$-definibilidade usada em provas anteriores.
• Verificação Simplificada: Devido à simplicidade dos sistemas semi-Thue subjacentes e à natureza estruturada da codificação, argumenta-se que a prova é mais simples de verificar em detalhes completos comparada às abordagens de Loader ou Joly.
• Construção Uniforme: A abordagem identifica uma construção uniforme que demonstra a indecidibilidade de três problemas relacionados: $\beta$-matching de ordem superior, habitabilidade de tipo de interseção e $\lambda$-definibilidade. O artigo vincula explicitamente a construção de $\beta$-matching às interpretações de teoria de modelos finitos usadas em provas de habitabilidade de tipo de interseção.
• Redução Certificada: O trabalho resulta em uma redução de muitos-para-um certificada do Problema da Parada para o $\beta$-matching de ordem superior, uma vez que a indecidibilidade do problema de reescrita inicial já está certificada no Rocq Prover.

Resultos

• Teorema: O $\beta$-matching de ordem superior é indecidível.
• Ordem de Indecidibilidade: A redução construída demonstra a indecidibilidade na ordem de tipo 6. Isso se alinha ao resultado de Loader de que o $\beta$-matching é indecidível na ordem 6. O artigo observa que, embora Loader tenha conjecturado que a ordem 5 poderia ser suficiente, nem a técnica de Loader nem a presente abordagem se aplicam na ordem 5, deixando a decidibilidade da ordem 5 como uma questão em aberto.
• Mecanização: A prova foi com sucesso contribuída para a Biblioteca de Provas de Indecidibilidade existente do Coq, garantindo que o resultado esteja livre das ambiguidades frequentemente presentes em provas manuais.

Significância
O artigo reivindica significância primariamente através da mecanização e simplificação da prova de indecidibilidade. Ao mudar o ponto de partida da $\lambda$-definibilidade para um problema restrito de reescrita de strings, o autor alcança uma prova que é mais adequada para verificação formal. O trabalho complementa resultados mecanizados existentes sobre $\beta$-unificação de ordem superior. Além disso, a abordagem destaca uma profunda conexão estrutural entre $\beta$-matching de ordem superior, habitabilidade de tipo de interseção e $\lambda$-definibilidade, sugerindo que esses problemas compartilham um mecanismo subjacente comum para a indecidibilidade baseado na simulação de propriedades de teoria de modelos finitos via termos $\lambda$. O autor enfatiza que a prova foi desenvolvida interativamente com o assistente de prova, baseando-se em análise de casos exaustiva para garantir a correção, minimizando assim o risco de erro humano na complexa construção lógica.