Non-Derivability Results in Polymorphic Dependent Type Theory

Este artigo demonstra, através da construção de modelos contrários, que princípios de indução e coindução para tipos de dados não são deriváveis no cálculo puro $λ$P2, estabelecendo que extensões como a extensão funcional de funções são essenciais para a prova desses princípios.

O essencial

Imagine que você está construindo uma cidade de Lego chamada Lógica. Nessa cidade, existem regras estritas sobre como você pode encaixar as peças. O autor deste artigo, Herman Geuvers, está investigando se é possível construir certos "prédios" (conceitos matemáticos) usando apenas as peças básicas de um conjunto específico chamado λP2.

O objetivo do artigo é celebrar o aniversário de um colega, Stefano Berardi, e responder a uma pergunta que ele e outros pesquisadores faziam há anos: "O que falta nas nossas peças básicas para que possamos provar certas verdades matemáticas?"

Aqui está a explicação simplificada, usando analogias do dia a dia:

1. O Problema: A Cidade Inacabada

Na cidade de λP2, você consegue criar estruturas básicas, como números (0, 1, 2...) e listas. Você pode até definir o que é um número. Mas há um problema: você não consegue provar que esses números funcionam como esperamos.

• A Analogia: Imagine que você construiu um castelo de Lego. Você tem os blocos, mas não tem a "cola" ou o "manual de instruções" que garante que, se você empurrar uma parede, ela não vai desmoronar.
• O Princípio da Indução: É como o manual que diz: "Se o primeiro bloco está firme, e se cada bloco segura o próximo, então todo o castelo é firme." Geuvers mostra que, no λP2 puro, esse manual não existe. Você não consegue provar que a estrutura é sólida, não importa como você tente encaixar as peças.

2. A Solução Parcial: Adicionando Novas Peças

Outros pesquisadores descobriram que, se você adicionar peças extras ao seu kit de Lego, o manual de instruções aparece. Essas peças extras são:

1. Tipos de Identidade: Para dizer "isto é igual àquilo".
2. Unicidade de Provas (UIP): A ideia de que, se duas coisas são iguais, não importa como você provou que são iguais; a prova é a mesma.
3. Tipos Sigma (Σ): Uma maneira de empacotar dados juntos.
4. Extensão Funcional (FunExt): Uma regra que diz: "Se duas máquinas (funções) produzem o mesmo resultado para todas as entradas, elas são a mesma máquina".

3. O Grande Descoberta: A Peça Mágica (FunExt)

O artigo de Geuvers faz um teste de laboratório. Ele pega o kit de Lego e adiciona apenas as peças de Identidade e Sigma (sem a Extensão Funcional).

• O Resultado: O manual de instruções (Indução) ainda não aparece. O castelo continua inseguro.
• A Conclusão: A peça Extensão Funcional (FunExt) é a chave mágica. Sem ela, você não consegue provar que seus números ou listas funcionam corretamente, mesmo tendo todas as outras peças novas. É como tentar construir um motor de carro sem o pistão: você tem o chassi e as rodas, mas o motor não liga.

4. Outros Prédios que Não Funcionam

Geuvers também olhou para outros tipos de construções:

• Quotients (Divisões/Classificações): Imagine que você quer classificar todos os carros por cor, ignorando a marca. Você quer dizer "um Ford vermelho é o mesmo que um Fiat vermelho".

  • O Resultado: No λP2 básico, você não consegue criar essa classificação de forma inteligente e universal. A cidade não permite que você "apague" as diferenças irrelevantes de forma automática.

• Streams (Fluxos Infinitos): Imagine uma fita de vídeo infinita que nunca para de rodar.

  • O Resultado: Você pode desenhar a fita, mas não consegue provar que duas fitas são "iguais" apenas porque elas mostram a mesma imagem a cada segundo. No λP2, a igualdade é muito rígida; duas fitas podem parecer iguais para sempre, mas o sistema diz que são diferentes porque foram construídas de formas ligeiramente distintas.

5. Como ele provou isso? (Os Espelhos)

Geuvers não apenas disse "não funciona". Ele construiu espelhos (modelos) da cidade.

• A Analogia: Imagine que você cria um "mundo paralelo" onde as regras do Lego são um pouco diferentes. Nesse mundo paralelo, ele mostra que, se você tentar usar o manual de instruções, ele simplesmente não existe ou é uma folha em branco.
• Se algo não funciona nesse mundo paralelo (que segue as mesmas regras básicas), então é impossível provar que funciona no mundo real da lógica pura. Ele usou esses "mundos espelho" para mostrar que, sem a peça mágica (FunExt), a cidade de λP2 está incompleta.

Resumo Final

Este artigo é como um relatório de engenharia que diz:

"Caros colegas, descobrimos que nossa cidade de lógica básica (λP2) tem buracos. Não conseguimos provar que nossos números são sólidos nem que nossas classificações funcionam. Se adicionarmos apenas algumas ferramentas novas, ainda não resolve. Precisamos obrigatoriamente da ferramenta chamada Extensão Funcional para que tudo funcione como deveria."

É uma homenagem a Stefano Berardi, que começou a investigar esses buracos na lógica, mostrando que, às vezes, para construir algo sólido, precisamos de regras mais flexíveis sobre o que significa "ser igual".

Resumo técnico

Resumo Técnico: Resultados de Não-Derivabilidade em $\lambda P2$

1. Problema e Contexto

O artigo aborda as limitações fundamentais da Teoria de Tipos Dependente Polimórfica de Segunda Ordem ($\lambda P2$), um subsistema do Cálculo das Construções (CC). Embora o $\lambda P2$ permita a codificação de tipos de dados indutivos (como números naturais, listas) e coindutivos (como streams) através de codificações de Church (impredicativas), uma questão central permanece: os princípios de indução e coindução são deriváveis (prováveis) dentro do sistema puro?

A literatura estabelece que a codificação padrão de números naturais em $\lambda P2$ não suporta o princípio de indução. Trabalhos recentes (como Awodey, Frey e Speight [1]) mostraram que, ao estender o $\lambda P2$ com tipos $\Sigma$, tipos de identidade, Unicidade de Provas de Identidade (UIP) e Extensãoalidade Funcional (FunExt), é possível definir tipos de dados onde a indução é provável.

O artigo de Geuvers investiga as seguintes lacunas:

1. É possível definir tipos quociente com princípios de indução no $\lambda P2$ puro?
2. Os tipos coindutivos definíveis (como streams) satisfazem o princípio de coindução (são álgebras co-iniciais) no $\lambda P2$?
3. Quais das extensões mencionadas acima são essenciais? Especificamente, a Extensãoalidade Funcional é necessária para obter a indução?

2. Metodologia

O autor utiliza uma abordagem baseada em modelos sintáticos para provar a não-derivabilidade. Em vez de tentar provar a impossibilidade de forma puramente sintática, o autor constrói contra-modelos específicos onde certas propriedades falham.

• Estrutura dos Modelos: Os modelos são baseados em Álgebras Combinatórias Fracamente Extensionais (WECA - Weakly Extensional Combinatory Algebras). O exemplo principal utilizado é o conjunto de termos $\lambda$ não tipados (abertos) módulo igualdade $\beta$ (ou $\beta\eta$).
• Semântica de Realizabilidade: O sistema é interpretado através de uma estrutura de "polysets" (subconjuntos da álgebra combinatória). Os tipos são interpretados como conjuntos de realizadores (elementos da álgebra).
• Estratégia de Prova: Para mostrar que um princípio (como indução ou coindução) não é derivável, o autor constrói um modelo onde:
  1. O tipo de dados (ex: stream ou números naturais) é bem definido.
  2. O princípio lógico correspondente (ex: a igualdade de streams bisimilares ou o princípio de indução) resulta em um conjunto vazio (não habitado) no modelo.
  3. Se o princípio fosse derivável no sistema, ele teria que ser verdadeiro em todos os modelos (Teorema de Correção/Soundness). A existência de um modelo onde falha prova a não-derivabilidade.

3. Contribuições e Resultados Principais

O artigo apresenta três resultados principais de não-derivabilidade:

A. Falha do Princípio de Coindução para Streams

• Contexto: O tipo de stream (fluxo infinito) é definível em $\lambda P2$ via tipos existenciais.
• Resultado (Teorema 4.3): O tipo de stream definível não é uma álgebra co-inicial (final). Especificamente, a relação de bisimilaridade ($s \sim t$) não implica igualdade ($s = t$).
• Evidência: O autor constrói dois streams distintos ($s_1$ e $s_2$) que são bisimilares (têm a mesma cabeça e cauda recursivamente) mas não são iguais no modelo. A prova explora a diferença entre os termos de $\lambda$-cálculo subjacentes que, embora comportem-se igual observacionalmente, possuem formas normais distintas.

B. Não-Derivabilidade de Quocientes Paramétricos

• Contexto: Quocientes permitem identificar elementos de um tipo segundo uma relação $R$. Um "quociente paramétrico" exige que a função de projeção ($cls$) seja polimórfica.
• Resultado (Teorema 4.4): Não é possível definir tipos quociente paramétricos em $\lambda P2$.
• Evidência: O autor mostra que, em um modelo baseado em termos $\lambda$ abertos, a função de projeção $cls$ teria que ser uma função constante para satisfazer as condições de igualdade no modelo, o que contradiz a necessidade de distinguir elementos não relacionados pela relação de quociente.

C. A Necessidade Crítica da Extensãoalidade Funcional (FunExt)

• Contexto: O trabalho anterior [1] usou uma extensão com Tipos de Identidade, UIP, Tipos $\Sigma$ e FunExt para provar indução.
• Resultado (Teorema 5.11): Mesmo estendendo o $\lambda P2$ com Tipos $\Sigma$, Tipos de Identidade e UIP, o princípio de indução para números naturais ainda não é derivável.
• Conclusão Chave: A Extensãoalidade Funcional (FunExt) é o ingrediente indispensável. O autor constrói um modelo onde FunExt falha (duas funções que são extensivamente iguais não são intensionalmente iguais) e, consequentemente, a indução falha. Isso demonstra que sem FunExt, não se pode provar a indução para tipos de dados algébricos (naturais, booleanos, listas, etc.), mesmo com os outros recursos adicionados.

4. Significado e Implicações

1. Limites do $\lambda P2$ Puro: O trabalho confirma rigorosamente que a codificação impredicativa de dados em $\lambda P2$ é insuficiente para capturar a estrutura indutiva e coindutiva completa. Não existem "codificações inteligentes" que contornem essa limitação dentro do sistema puro.
2. Hierarquia de Recursos: O artigo estabelece uma hierarquia clara de recursos necessários para a teoria de tipos prática:
   • $\lambda P2$ + Tipos $\Sigma$ + Identidade + UIP $\nRightarrow$ Indução.
   • $\lambda P2$ + Tipos $\Sigma$ + Identidade + UIP + FunExt $\Rightarrow$ Indução (conforme [1]).
3. Validação de Extensões Modernas: Os resultados justificam a inclusão da Extensãoalidade Funcional em sistemas modernos de prova assistida (como Coq, Agda, Lean) quando se deseja trabalhar com tipos de dados indutivos e coindutivos definidos via quocientes ou codificações impredicativas.
4. Contribuição para a Comunidade: O artigo é dedicado a Stefano Berardi, celebrando seu trabalho seminal sobre modelos não-paramétricos. A metodologia de usar modelos sintáticos baseados em álgebras combinatórias para provar impossibilidades é uma continuação direta e refinada da abordagem de Berardi.

Em suma, o paper demonstra que a indução e a coindução fortes não são propriedades intrínsecas da codificação impredicativa, mas sim dependem crucialmente de axiomas de extensãoalidade que não estão presentes no cálculo puro.