Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

1. Problema e Contexto

O teorema de Interpolação de Craig é um resultado fundamental na lógica e ciência da computação, estabelecendo que, se uma fórmula $A$ implica $B$, existe uma fórmula intermediária $I$ (o interpolante) que utiliza apenas os símbolos de predicado comuns a $A$ e $B$, tal que $A \vdash I$ e $I \vdash B$.

O artigo foca na interpolação relevante a provas (proof-relevant interpolation), uma refinamento onde não apenas a fórmula intermediária é encontrada, mas também os termos de prova (no cálculo lambda) que conectam $A$ a $I$ e $I$ a $B$, de modo que a composição desses termos seja equivalente ao termo original.

O trabalho revisita o teorema de interpolação de Čubrić para o Cálculo Lambda Simplesmente Tipado com Somas e Tipos Vazios (STLC+). O teorema original de Čubrić, embora correto, apresentava uma prova complexa baseada em indução no tamanho dos termos, substituindo subtermos por variáveis. Os autores identificaram falhas na clareza da prova original (casos tratados como "iguais" que não eram) e a dificuldade de formalização devido à complexidade estrutural.

2. Metodologia

Os autores propõem uma nova abordagem baseada em tipagem bidirecional (bidirectional typing) para caracterizar as formas normais do STLC+.

• Tipagem Bidirecional e Formas Normais: O sistema de tipos é dividido em regras de inferência (onde o tipo é uma saída) e verificação (onde o tipo é uma entrada). Isso permite uma caracterização indutiva e mútua de formas normais (termos que não reduzem) e formas neutras (termos que podem ser o argumento principal de uma eliminação sem criar redexes).
• Conversões Comutativas: Para lidar com a presença de tipos positivos (somas $+$ e tipo vazio $\bot$), os autores não utilizam apenas a redução $\beta$, mas também as conversões comutativas (commuting conversions). Essas regras empurram eliminações através de outras eliminações de tipos positivos, garantindo que as formas normais resultantes satisfaçam a propriedade de subfórmula, essencial para a interpolação.
• Normalização por Relações Lógicas: Para provar que todo termo bem-tipado reduz a uma forma normal, os autores utilizam uma prova de normalização baseada em relações lógicas (inspirada em Abel e Sattler), definindo valores e termos "cobertos" (covered) para lidar com a complexidade das eliminações de tipos positivos.
• Indução Mútua: A prova de interpolação é realizada por indução mútua sobre a estrutura das formas normais e formas neutras, utilizando uma partição do contexto (dividindo variáveis entre "fonte" e "alvo") para rastrear o vocabulário comum.

3. Principais Contribuições

1. Nova Prova de Interpolação: Os autores fornecem uma prova mais direta e estruturada do teorema de interpolação relevante a provas de Čubrić, substituindo a indução no tamanho do termo por uma indução sobre a caracterização indutiva de formas normais via tipagem bidirecional.
2. Formalização em Rocq: O trabalho inclui a primeira formalização completa da metateoria do STLC+ com conversões comutativas no assistente de prova Rocq (antigo Coq). Isso inclui:
   • Prova de normalização para o cálculo com conversões comutativas.
   • Prova do teorema de interpolação relevante a provas.
3. Conexão entre Tipagem Bidirecional e Propriedade de Subfórmula: O artigo estabelece e destaca explicitamente a relação entre sistemas de tipagem bidirecional e a propriedade de subfórmula, argumentando que a tipagem bidirecional captura naturalmente as formas normais que possuem essa propriedade, mesmo na presença de somas (o que é frequentemente mal compreendido).
4. Tratamento de Constantes e Equações: O teorema é generalizado para linguagens com constantes e equações arbitrárias, mantendo a validade da interpolação.

4. Resultados

• Teorema de Interpolação: Para qualquer termo normal $t$ tal que $\Gamma \vdash t : T$, existe um tipo $M$ (construído apenas com vocabulário comum entre o contexto e o tipo alvo) e termos $l$ e $r$ tais que $t$ é equivalente à composição $r[l..]$.
• Normalização: Foi provado que todo termo bem-tipado no STLC+ com conversões comutativas reduz a uma forma normal.
• Eficiência da Formalização: A formalização em Rocq é compacta (aproximadamente 4.000 linhas de código, incluindo código gerado), significativamente menor que formalizações anteriores de interpolação uniforme, e compila em cerca de 30 segundos.
• Automação: O uso de solvers como AutoSubst2 e setoid rewriting foi crucial para gerenciar a complexidade das substituições e das equações de conversão, embora os autores relatem desafios com a incompletude e velocidade de algumas ferramentas.

5. Significado e Impacto

• Simplificação de Provas Complexas: O trabalho demonstra que a tipagem bidirecional oferece uma estrutura indutiva superior para provar teoremas que dependem da propriedade de subfórmula, simplificando drasticamente provas que antes eram enganosas ou difíceis de formalizar (como a de Čubrić).
• Avanço na Teoria de Categorias: Como o STLC+ é a linguagem interna de categorias cartesianas fechadas bi- (biCCC), os resultados têm implicações categóricas, fornecendo "categorificações" de resultados sobre álgebras de Heyting.
• Base para Futuras Extensões: A formalização robusta serve como base para extensões futuras, como:
  • Interpolação para termos não normais (com redexes).
  • Interpolação uniforme relevante a provas.
  • Extensão para tipos dependentes (embora isso apresente desafios adicionais devido à falta de conversões comutativas bem-tipadas em geral).
• Relevância para Verificação Formal: O artigo oferece um exemplo prático de como organizar provas de metateoria em assistentes de prova modernos, utilizando técnicas de automação para lidar com a complexidade sintática (substituições) enquanto mantém o foco na lógica estrutural.

Em resumo, o artigo não apenas revisita e corrige uma prova clássica, mas também estabelece uma nova metodologia baseada em tipagem bidirecional que torna a interpolação relevante a provas mais acessível, compreensível e formalizável, preenchendo lacunas na literatura sobre normalização e interpolação em cálculos com tipos de soma.