A formalization of System I with type Top in Agda

1. Problema e Contexto

O artigo aborda o Cálculo Lambda Simplesmente Tipado (STLC) estendido com pares e isomorfismos de tipos. Em sistemas tradicionais, tipos isomórficos (como $A \times B$ e $B \times A$, ou $A \to (B \times C)$ e $(A \to B) \times (A \to C)$) são tratados como distintos, embora semanticamente equivalentes. O System I (introduzido por Díaz-Caro e Dowek) propõe tratar tipos isomórficos como iguais, permitindo que programas com sintaxe diferente, mas semântica equivalente, sejam considerados idênticos.

O problema central enfrentado pelos autores é a formalização rigorosa e a prova de propriedades metateóricas (como progressão e normalização forte) de uma variante do System I que inclui o tipo Top ($\top$), representando a proposição "Verdadeira". A inclusão de $\top$ introduz novos isomorfismos (como $A \times \top \equiv A$ e $A \to \top \equiv \top$) e desafios adicionais para garantir que o cálculo permaneça normalizável (ou seja, que toda redução termine), especialmente ao lidar com termos que poderiam levar a loops infinitos (como o termo $\Omega$) se não forem tratados corretamente.

2. Metodologia

Os autores utilizam a linguagem de prova interativa Agda para formalizar o cálculo. A metodologia baseia-se nos seguintes pilares:

• Tipagem Intrínseca (Intrinsically Typed Terms): Ao contrário de abordagens extrínsecas onde termos e tipos são definidos separadamente, aqui os termos são definidos diretamente como provas de que possuem um certo tipo em um determinado contexto. Isso garante que apenas termos bem-tipados existam no formalismo, eliminando a necessidade de provar preservação de tipos separadamente.
• Índices de De Bruijn: Para lidar com variáveis, utilizam-se índices numéricos em vez de nomes, o que torna a formalização mais compacta e evita problemas de renomeação de variáveis.
• Testemunhas Explícitas de Isomorfismo: Para aplicar a regra de conversão de tipos (se $t : A$ e $A \equiv B$, então $t : B$), o sistema exige uma testemunha explícita ($\rho$) que prova o isomorfismo. A sintaxe dos termos é estendida com um construtor $[\rho]_\equiv t$.
• Redirecionamento de Equivalências: Em vez de tratar as equivalências de termos como uma relação simétrica e transitiva ($\Leftrightarrow$), os autores direcionam essas regras para criar relações de reescrita ($\rightsquigarrow$). Isso é crucial para garantir a terminação, impedindo que regras como a comutatividade de pares sejam aplicadas infinitamente.
• Técnica de Redutibilidade (Reducibility): Para provar a normalização forte, utilizam uma adaptação da técnica de redutibilidade de Tait/Girard, seguindo a abordagem de Schäfer (e sua variante para Agda de András Kovács). Isso envolve a definição de uma interpretação semântica dos termos e a prova de um teorema de "adequação".

3. Principais Contribuições

O trabalho apresenta três contribuições fundamentais:

1. Extensão do System I com o Tipo Top:

   • Introduziram o tipo $\top$ e os isomorfismos associados (identidade de produto, identidade de implicação e absorção).
   • Adaptaram o cálculo para suportar formalização, exigindo testemunhas explícitas para cada aplicação de isomorfismo.
   • Definiram um conjunto de regras de reescrita de termos que cobrem não apenas os isomorfismos clássicos (troca, associação, distribuição, curry), mas também os novos relacionados a $\top$ e regras auxiliares (como $\eta$-expansão e regras de "split") para evitar que termos fiquem "presos" (stuck).

2. Formalização Completa em Agda:

   • Implementaram a sintaxe, regras de tipagem, semântica operacional e a relação de equivalência de termos.
   • O código é totalmente verificável, onde cada termo é uma prova de tipagem.

3. Provas de Propriedades Metateóricas:

   • Progresso (Progress): Provaram que todo termo fechado e bem-tipado é ou um valor (abstração, par de valores, ou $\top$) ou pode realizar um passo de redução.
   • Normalização Forte (Strong Normalization): Provaram que toda sequência de redução a partir de um termo bem-tipado é finita. A prova é construtiva, o que permite extrair um algoritmo de avaliação.

4. Resultados

• Terminação Garantida: A prova de normalização forte confirma que a adição do tipo $\top$ e das testemunhas explícitas não introduz ciclos infinitos no sistema, mesmo na presença de termos complexos como $\Omega = (\lambda x. x x)(\lambda x. x x)$, que neste sistema é tipável e reduz a $\top$ (representado por $\star$).
• Função de Avaliação Total: Devido à prova construtiva de normalização forte, os autores definiram uma função de avaliação eval em Agda que é total (sempre termina). Esta função recebe um termo fechado e prova de que ele é normalizável, retornando a sequência de passos até o valor final.
• Resolução de Não-Determinismo: O sistema lida com a não-determinismo inerente à projeção de pares (devido à comutatividade) através da tipagem baseada no tipo do elemento projetado, e resolve conflitos de ordem de argumentos em aplicações de função através das regras de reescrita direcionadas.

5. Significado e Impacto

• Consistência Lógica: Sob a perspectiva da correspondência de Curry-Howard, a normalização forte garante a consistência do sistema lógico subjacente. Se o cálculo fosse não-normalizável, permitiria a derivação de falsos.
• Avanço na Formalização de Cálculos Modulo Isomorfismos: Este é, segundo os autores, o primeiro formalização de uma prova de normalização para um cálculo lambda modulo isomorfismos. A complexidade das regras de equivalência torna a verificação manual propensa a erros; o uso do Agda fornece uma garantia mecânica de correção.
• Programação e Inferência de Tipos: O trabalho demonstra a viabilidade de sistemas de tipos onde a igualdade de tipos é mais flexível, permitindo que funções aceitem argumentos em qualquer ordem ou estruturas de dados reorganizadas sem necessidade de conversão manual explícita no código fonte, desde que o compilador (ou verificador) possa inferir os isomorfismos.
• Base para Futuras Extensões: O formalismo estabelecido serve como base para explorar sistemas mais complexos, como o System I polimórfico (System F modulo isomorfismos) e variantes não tipadas, além de investigar a relação com a extensão $\eta$ do System I.

Em resumo, o artigo fornece uma fundação sólida e verificada mecanicamente para o estudo de cálculos lambda onde a estrutura dos tipos é tratada de forma mais flexível, resolvendo desafios teóricos de terminação e oferecendo ferramentas práticas para implementação de compiladores e assistentes de prova.