A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Resumo Técnico: Uma Prova de Consistência Verificada por Máquina para Sistemas de Tipos Puros Impredicativos

Problema e Contexto
O artigo aborda os desafios da mecanização da teoria dos tipos, focando especificamente nas propriedades metateóricas de Sistemas de Tipos Puros (PTS). Uma dificuldade central na formalização de substituição e $\beta$-redução reside em lidar com a renomeação de variáveis para evitar a captura de nomes. As definições tradicionais (ex: Curry-Feys) exigem indução bem fundada sobre o comprimento do termo devido aos passos de renomeação não primitivos recursivos, o que torna a mecanização difícil. Abordagens alternativas, como índices de de Bruijn (dBI), sintaxe localmente sem nomes (locally nameless) e HOAS (Sintaxe Abstrata de Ordem Superior), oferecem soluções, mas introduzem seus próprios inconvenientes: dBI é incômodo para a legibilidade humana; a sintaxe localmente sem nomes exige predicados de bem-formidade que "poluem" os resultados metateóricos; e o HOAS frequentemente impede a geração de código executável ou a formulação de questões de decidibilidade.

Os autores visam avaliar a viabilidade de uma abordagem que mantenha a sintaxe clássica (usando variáveis nomeadas) enquanto utiliza as substituições simultâneas de Stoughton. Este método realiza a renomeação de variáveis ligadas simultaneamente à substituição através de uma única recursão estrutural, evitando a necessidade de indução bem fundada sobre o comprimento do termo para a maioria das provas.

Metodologia
O desenvolvimento é totalmente verificado por máquina usando Agda (v2.6.2.2) e a biblioteca padrão. A metodologia baseia-se nos seguintes componentes principais:

1. Substituições Simultâneas de Stoughton: As substituições são definidas como funções de variáveis para $\lambda$-termos ($Sub = V \to \Lambda$). A operação $M \bullet \sigma$ é definida por recursão estrutural. Para abstrações $\lambda$ e tipos $\Pi$, a variável ligada é renomeada para um novo nome $y$ escolhido por uma função $X$, e a substituição é atualizada para mapear o antigo nome da variável ligada para este novo nome. Isso garante que apenas uma chamada recursiva seja necessária por abstração, mantendo a primitividade recursiva.
2. Relações $\alpha$-Comutativas: Os autores desenvolvem uma teoria de relações que comutam com $\alpha$-conversão. Uma relação $S$ é $\alpha$-comutativa se $M \sim_\alpha N$ e $N S P$ implica a existência de um $Q$ tal que $M S Q$ e $Q \sim_\alpha P$. Este arcabouço permite que os autores tratem a confluência até a $\alpha$-conversão de forma limpa, evitando a duplicação de lemas frequentemente vista em outras formalizações.
3. Revisão de Takahashi para a Prova de Confluência: Em vez da prova original de Tait e Martin-Löf, o artigo emprega a revisão de Takahashi usando redução paralela ($\Rightarrow$). Os autores definem a redução paralela sem regras explícitas de $\alpha$-conversão nos passos de redução, baseando-se na propriedade do pentágono (uma generalização da propriedade do diamante até a $\alpha$-conversão) para provar a confluência.
4. Suposição de Normalização: A prova de consistência assume que o PTS específico sob consideração é normalizante (todo termo bem tipado é fracamente normalizante). Os autores observam que provar a normalização para sistemas impredicativos dentro do Agda é provavelmente impossível devido à falta de impredicatividade do Agda na metalinguagem.

Principais Contribuições
O artigo apresenta provas formais para três propriedades metateóricas principais:

1. Confluência da $\beta$-redução: Os autores provam o teorema de Church-Rosser para a sintaxe subjacente do PTS. Ao utilizar a teoria das relações $\alpha$-comutativas e a redução paralela de Takahashi, eles estabelecem que o fechamento estelar da redução paralela coincide com a $\beta$-redução de muitos passos e satisfaz a propriedade do pentágono.
2. Redução de Sujeito (SR): O artigo formaliza a preservação da tipagem sob redução. Seguindo ideias de McKinna e Pollack, os autores estendem as reduções para contextos e provam um teorema simultâneo sobre a validade dos contextos e a preservação da tipagem para sujeitos. Isso inclui a prova da injetividade do produto, um lema crucial para inversão.
3. Consistência para PTS Impredicativos: Os autores provam que, para uma subclasse específica de PTS impredicativos (aqueles que satisfazem axiomas e regras específicas, tais como $(\ast, \square) \in \mathcal{A}$ e $(\square, \ast, \ast) \in \mathcal{R}$), o tipo $\Pi[x : s]x$ (representando o falso sob Curry-Howard) é inabitável no contexto vazio. A prova estende a prova de caneta e papel de Coquand para o Cálculo de Construções (CC). Ela depende da correção e completude de formas normais e neutras definidas indutivamente, lemas de inversão e da suposta propriedade de normalização.

Resultos e Avaliação

• Tamanho da Formalização: Todo o desenvolvimento compreende aproximadamente 4.300 linhas de código (LoC), sendo 3.000 LoC atribuídas ao arcabouço subjacente das substituições de Stoughton e da sintaxe do PTS de trabalhos anteriores.
• Comparação: Os autores comparam seu trabalho com formalizações usando índices de de Bruijn (Barras e Werner, ~2.900 LoC) e sintaxe localmente sem nomes (Aydemir et al., ~4.800 LoC). Eles argumentam que sua abordagem é comparável em tamanho, mas oferece transparência superior em relação à sintaxe utilizada, pois espelha de perto as apresentações matemáticas informais (ex: o lema de enfraquecimento parece quase idêntico à notação clássica).
• Viabilidade: Os resultados sugerem que a abordagem usando a sintaxe clássica e substituições simultâneas é viável para teorias de tipos dependentes. Os autores observam que apenas alguns lemas exigiram indução bem fundada, e o tamanho do código não "explodiu".

Significância e Alegações
O artigo afirma que a abordagem usando as substituições de Stoughton oferece uma "apresentação e tratamento mais claros" de problemas metateóricos em comparação com desenvolvimentos similares, particularmente no que diz respeito ao tratamento da $\alpha$-conversão. Os autores afirmam que sua solução é mais transparente para leitores humanos do que as abordagens de sintaxe localmente sem nomes ou de Bruijn, pois evita o "entulho notacional" de abrir termos e gerenciar parâmetros frescos manualmente.

A significância do trabalho reside em demonstrar que uma prova de consistência verificada por máquina para sistemas impredicativos é alcançável sem abandonar a sintaxe clássica, desde que a normalização seja assumida. Os autores reconhecem modestamente que uma mecanização total da normalização para teorias impredicativas é provavelmente impossível no Agda devido às limitações de força prova-teórica (implicações do teorema da incompletude de Gödel), mas a prova de consistência em si permanece um passo substancial em direção a algoritmos de verificação de tipos corretos por construção para tais sistemas. O trabalho serve como uma validação da utilidade do arcabouço para futuras formalizações de teorias de tipos dependentes.