Are Dependent Types in Set Theory Feasible?

Visão Geral

O artigo propõe uma implementação mecanizada de tipos dependentes dentro de um assistente de prova baseado em Teoria dos Conjuntos (especificamente a teoria de Tarski-Grothendieck), desafiando a predominância atual de sistemas baseados em Teoria dos Tipos Dependentes (DTT) como Rocq (antigo Coq) e Lean. Os autores demonstram que é possível obter as vantagens sintáticas e de raciocínio dos tipos dependentes mantendo a simplicidade e a verificabilidade formal da lógica de primeira ordem com axiomas de conjuntos.

---

1. O Problema

• Dominância da DTT: A maioria dos assistentes de prova modernos (Rocq, Lean 4) baseia-se na Teoria dos Tipos Dependentes. Embora ofereçam propriedades práticas úteis (como verificação de tipos previsível e recursão estrutural), seus núcleos lógicos são complexos, difíceis de validar e propensos a bugs de implementação.
• Fragilidade da Base: A Teoria dos Conjuntos de Zermelo-Fraenkel (ZFC) é a fundação padrão da matemática há mais de um século, mas os assistentes de prova baseados nela (como Mizar) carecem de recursos avançados de tipos dependentes.
• Interoperabilidade: Há uma necessidade crescente de transferir provas entre diferentes assistentes (ex: de Lean para sistemas baseados em conjuntos). Para isso, o sistema receptor precisa simular fielmente os recursos do sistema de origem sem codificações excessivamente complexas.
• Questão Central: É viável implementar um sistema de tipos dependentes rico (com universos e produtos dependentes) sobre uma fundação puramente conjuntista, mantendo a verificação automática e a correção formal?

2. Metodologia

Os autores utilizam o assistente de prova Lisa, que possui um núcleo lógico pequeno baseado em Lógica de Primeira Ordem (LPO) e Teoria dos Conjuntos.

A. Embedding em $\lambda$FOL

Para representar termos de tipos dependentes (que envolvem abstração $\lambda$) dentro da lógica de primeira ordem, eles utilizam uma extensão chamada $\lambda$FOL (Lógica de Primeira Ordem com termos $\lambda$ e o operador $\epsilon$ de Hilbert).

• Representação:
  • Abstração ($\lambda x:T. u$): Mapeada para um conjunto de pares ordenados definidos por uma função abs.
  • Aplicação ($t\ u$): Mapeada para o operador $\epsilon$ (escolha de Hilbert), onde app(t)(u) retorna um $y$ tal que $(u, y) \in t$.
  • Produto Dependente ($\Pi x:T_1. T_2$): Representado como o conjunto de todas as funções funcionais $f$ cujos valores para cada $x \in T_1$ pertencem a $T_2(x)$.

B. Gerenciamento de Universos

A ZFC padrão não possui universos internos fechados sob todas as construções (necessários para hierarquias cumulativas de tipos).

• Solução: Utilizam o Axioma de Tarski, que garante a existência de infinitos universos de Grothendieck (conjuntos fechados sob operações de conjuntos, incluindo produtos dependentes).
• Definição: Definiram um predicado isUniverse que simplifica as propriedades de fechamento necessárias para a formação de tipos dependentes, permitindo a criação de uma hierarquia cumulativa ($Type_i : Type_{i+1}$).

C. Verificação de Tipos Bidirecional

Implementaram uma tática de prova chamada Typecheck.prove que realiza a verificação de tipos de forma bidirecional (inferência e verificação), gerando objetos de prova verificáveis pelo núcleo do Lisa.

• Modos:
  • Check Mode: Verifica se um termo $e$ tem um tipo esperado $T_{exp}$.
  • Infer Mode: Infere o tipo de um termo $e$.
  • Subset Mode: Gerencia subtipos (subtyping) usando cumulatividade de universos e covariância no codomínio.

3. Principais Contribuições

1. Embedding Mecanizado: Primeira implementação prática de produtos dependentes com universos em um assistente de prova baseado em lógica de primeira ordem e teoria dos conjuntos (Lisa).
2. Tática de Prova Produtora: Desenvolvimento de uma tática automatizada que não apenas verifica se um termo é bem-tipado, mas constrói a prova formal correspondente dentro do núcleo do Lisa, baseada em axiomas de conjuntos.
3. Suporte a Subtipos: Implementação de uma forma de subtipagem (subtyping) que suporta covariância no codomínio e invariantes no domínio, provando sua correção dentro da teoria dos conjuntos.
4. Interoperabilidade Potencial: O trabalho serve como um passo fundamental para a tradução de provas de sistemas baseados em tipos (como Lean 4) para sistemas baseados em conjuntos, facilitando a interoperabilidade.

4. Resultados

• Correção Formal: As regras de inferência de tipos dependentes (como $\beta$-redução, introdução e eliminação de produtos) foram provadas como teoremas derivados diretamente dos axiomas de Tarski-Grothendieck e das regras de inferência da lógica de primeira ordem.
• Exemplo Prático: Os autores demonstraram o sistema com um exemplo de composição polimórfica de funções (similar a um exemplo em Lean). O sistema inferiu automaticamente que a composição de uma função $f: A \to B$ com uma função identidade polimórfica é bem-tipada, gerando a prova de pertinência ao conjunto correspondente.
• Eficiência: O sistema consegue lidar com a verificação de tipos e a geração de provas sem a complexidade de um núcleo de DTT, mantendo a simplicidade do kernel do Lisa.

5. Significado e Impacto

• Viabilidade Teórica: O trabalho responde afirmativamente à pergunta do título: tipos dependentes são viáveis na teoria dos conjuntos. Isso desafia a noção de que a teoria dos tipos é estritamente necessária para suportar recursos modernos de prova.
• Simplicidade e Segurança: Ao manter a fundação na Lógica de Primeira Ordem e Teoria dos Conjuntos, o sistema herda a simplicidade de validação e a menor superfície de ataque (menos bugs no núcleo) comparado a sistemas como Lean ou Coq.
• Futuro da Interoperabilidade: Oferece uma via para "traduzir" o ecossistema de provas de Lean (muito popular entre matemáticos) para fundamentos conjuntistas, permitindo que provas complexas sejam verificadas em sistemas com kernels menores e mais robustos.
• Extensibilidade: A abordagem permite adicionar recursos de teoria dos tipos (como recursão ou indutivos, mencionados como trabalho futuro) sobre uma base já validada, garantindo a correção de novos recursos através dos axiomas de conjuntos.

Em resumo, o artigo estabelece uma ponte robusta entre a expressividade da teoria dos tipos dependentes e a simplicidade formal da teoria dos conjuntos, demonstrando que é possível ter o "melhor dos dois mundos" através de uma implementação mecanizada cuidadosa.