What does it take to certify a conversion checker?

Resumo Técnico: O que é necessário para certificar um verificador de conversão?

Declaração do Problema
A certificação de kernels de assistentes de prova (os componentes centrais responsáveis pela verificação de provas) é um desafio crítico na teoria dos tipos dependentes. Embora o "critério de de Bruijn" permita depositar confiança em um kernel pequeno, certificar o próprio kernel é difícil porque as teorias de tipos dependentes dependem de invariantes complexos. Especificamente, provar a correção de um verificador de conversão (que decide a igualdade definicional, $\sim=$) exige tradicionalmente provar a normalização do sistema (a terminação da redução). No entanto, devido ao segundo teorema da incompletude de Gödel, um sistema não pode provar sua própria consistência ou normalização. Consequentemente, a certificação total de um kernel de tipo dependente dentro do próprio sistema é inviável. O artigo busca identificar as propriedades metateóricas mínimas necessárias para certificar verificadores de conversão sem depender de uma prova completa de normalização, visando uma "falha graciosa" (graceful failure), onde o verificador é certificado com base em propriedades mais fracas e prováveis.

Metodologia
Os autores adotam uma abordagem modular, separando a metateoria (a "caixa de ferramentas opaca" de propriedades como injetividade e normalização) da certificação algorítmica (a implementação do verificador).

1. Sistema Formal: O trabalho é formalizado no assistente de prova Rocq (anteriormente Coq) para uma versão da Teoria dos Tipos de Martin-Löf (MLTT) apresentando tipos de função dependente ($\Pi$) e pares ($\Sigma$), tipos indutivos (vazio, números naturais, identidade) e um universo, todos com eliminação grande.
2. Algoritmos: Dois algoritmos de verificação de conversão são implementados e certificados:
   • Conversão Tipada: Um algoritmo direcionado ao tipo, bidirecional, semelhante aos do Coq e Agda, que mantém a informação de tipo durante toda a verificação.
   • Conversão Não Tipada: Um algoritmo direcionado ao termo, semelhante aos do Rocq e Lean, que não mantém a informação de tipo durante a redução de termos, mas depende de uma especificação tipada para sua correção.
3. Estrutura de Certificação: Os algoritmos são implementados usando o monad de recursão livre de McBride (via PartialFun) para lidar com a parcialidade. Os autores definem precondições (invariantes) e pós-condições para os algoritmos. A correção é decomposta em:
   • Solidez Positiva: Se o algoritmo retorna "sim", os termos são convertíveis.
   • Solidez Negativa: Se o algoritmo retorna "não", os termos não são convertíveis.
   • Terminação: O algoritmo sempre para.

Principais Contribuições
A principal contribuição do artigo é a identificação e demonstração de que as propriedades de injetividade dos construtores de tipos e termos são as propriedades metateóricas cruciais e suficientes para certificar a solidez dos verificadores de conversão, sendo amplamente independentes da normalização.

• Injetividade como o Requisito Central: Os autores mostram que a injetividade dos construtores de tipos (por exemplo, se $\Pi x:A.B \sim= \Pi x:A'.B'$, então $A \sim= A'$ e $B \sim= B'$) e a ausência de confusão (por exemplo, $\Pi x:A.B$ não pode ser conversível a $N$) são suficientes para provar a solidez positiva.
• Injetividade ao Nível do Termo: Para provar a solidez negativa, os autores demonstram que propriedades de injetividade para construtores de termos (especificamente para números naturais e tipos $\Pi$) e a completude da comparação de neutros (garantindo que neutros conversíveis possam ser comparados estruturalmente) são necessárias.
• Equivalência entre Não Tipada e Tipada: O artigo apresenta uma certificação inédita de um verificador de conversão não tipado contra uma especificação tipada. Ele esclarece que a conversão "não tipada" é efetivamente uma "conversão direcionada ao termo tipada", onde a informação de tipo é implícita nos invariantes em vez de explícita nos passos de redução.
• Análise de Dependência: Ao utilizar type classes no Rocq, os autores fornecem um mapa de dependência detalhado (Figura 1 no artigo) mostrando exatamente quais propriedades metateóricas (Injetividade, Normalização, etc.) são necessárias para cada propriedade algorítmica (Solidez, Terminação).

Resultos
A formalização (adicionando cerca de 10 mil linhas de código à base existente do Rocq) produz os seguintes resultados específicos:

1. Solidez Positiva: Provada para ambos os algoritmos, tipado e não tipado, utilizando apenas a injetividade dos construtores de tipos. Esta propriedade não implica consistência lógica e pode ser provada em uma metateoria mais fraca que a teoria objeto.
2. Solidez Negativa: Provada usando injetividade de construtores de tipos e termos além da completude da comparação de neutros.
   • Para o algoritmo tipado, a completude da comparação de neutros é necessária apenas em tipos positivos (Propriedade 9).
   • Para o algoritmo não tipado, a completude é necessária em todos os tipos (Propriedade 7), devido à ausência de informação de tipo para guiar a $\eta$-expansão de tipos negativos.
3. Terminação: Provada para ambos os algoritmos assumindo normalização profunda (Propriedade 11). Esta propriedade é a única que implica consistência lógica e requer uma metateoria mais forte que a teoria objeto.
4. Equivalência: Os autores provam que os algoritmos tipado e não tipado são equivalentes (Proposições 22 e 24). A prova baseia-se em fortalecimento (remoção de variáveis irrelevantes do contexto) e normalização. O algoritmo não tipado é mostrado como uma implementação válida da especificação tipada.

Significância e Alegações
O artigo afirma que a "pedra angular" para certificar um verificador de tipos não é a prova completa de normalização, mas sim as propriedades de injetividade do sistema de tipos.

• Falha Graciosa: Os autores argumentam que, mesmo que a normalização não possa ser provada (devido às limitações de Gödel), ainda é possível certificar a solidez de um verificador. Isso permite a certificação de implementações complexas e otimizadas (como as do Rocq ou Lean) assumindo a injetividade como um axioma ou provando-a em uma metateoria mais fraca.
• Modularidade: O trabalho defende uma abordagem de "metateoria como uma caixa preta". A certificação do algoritmo deve depender apenas de um pequeno conjunto de propriedades axiomatizadas (injetividade, completude de neutros) em vez de uma prova monolítica de toda a teoria de tipos.
• Certificação Não Tipada: O artigo demonstra que certificar verificadores de conversão direcionados ao termo (não tipados) é viável e que a distinção entre conversão tipada e não tipada diz menos sobre a ausência de tipos e mais sobre a direção do algoritmo (direcionado ao termo vs. direcionado ao tipo).
• Limitações: Os autores notam modestamente que seu trabalho cobre uma versão simplificada de MLTT. Eles reconhecem que recursos como tipos unitários definicionais (onde todos os habitantes são conversíveis) ou proposições estritas (irrelevância de prova) complicam a completude da comparação de neutros, exigindo estratégias específicas (como reinferência de tipos ou rastreamento de universos) em kernels do mundo real. Eles também observam que teorias de tipos extensionais e cubicais apresentam desafios adicionais quanto ao fortalecimento e completude de neutros.

Em resumo, o artigo fornece um roteiro para certificar verificadores de conversão ao isolar a injetividade como a condição suficiente para a solidez, desconectando assim a certificação do algoritmo da tarefa difícil de provar a normalização completa.