Constructing (Co)inductive Types via Large Sizes

1. Declaração do Problema

Os assistentes de prova (por exemplo, Agda, Lean, Rocq) baseiam-se na teoria dos tipos dependentes para garantir consistência e decidibilidade. Um requisito crítico é que todas as funções recursivas devem ser totais (terminantes) e todas as funções corecursivas devem ser produtivas.

• Limitações Atuais: A maioria dos sistemas impõe totalidade por meio de verificações sintáticas (por exemplo, recursão estrutural ou terminação por mudança de tamanho). Essas verificações são frequentemente restritivas, não modulares e sensíveis a refatorações de código.
• Tipos Dimensionados: Uma alternativa baseada em tipos utiliza "tamanhos" (ordinais) para anotar tipos, permitindo que a terminação seja provada por indução bem-fundada sobre o tamanho.
• A Inconsistência do Agda: O Agda implementa tipos dimensionados, mas introduz um maior tamanho ($\infty$) para definir o tipo indutivo/coindutivo completo como sua aproximação em $\infty$. Isso leva a uma inconsistência lógica: o sistema prova $\infty < \infty$, violando a irreflexividade das ordens estritas bem-fundadas.
• Trabalho Teórico Anterior: Tentativas anteriores de corrigir isso usando quantificadores paramétricos (existencial $\exists$ para indutivo, universal $\forall$ para coindutivo) foram limitadas. Especificamente, elas só podiam construir tipos indutivos de ramificação finita, porque o tipo de tamanho era interpretado como o conjunto dos números naturais ($\mathbb{N}$), que carece de ordinais limites necessários para estruturas de ramificação infinita.

Objetivo: Construir uma teoria de tipos consistente que suporte todos os tipos (co)indutivos (incluindo os de ramificação infinita) usando tipos dimensionados e quantificadores paramétricos, sem depender de um maior tamanho inconsistente.

2. Metodologia

Os autores estendem a Teoria dos Tipos de Martin-Löf (MLTT) com recursos específicos para alcançar essa construção e provam sua consistência por meio de um modelo de realizabilidade.

A. A Teoria dos Tipos Estendida

A teoria inclui recursos padrão da MLTT (universos, $\Sigma$, $\Pi$, tipos de identidade) mais:

1. Um Tipo de Tamanhos (Size):
   • Equipado com um zero ($0$) e sucessor ($\uparrow i$).
   • Ordenado por uma pré-ordem ($\leq$) codificada como uma mera proposição.
   • Crucialmente: Size é um tipo grande (não está no universo $U$), mas a quantificação sobre ele pode produzir tipos pequenos.
2. Quantificadores Paramétricos:
   • $\exists i. A(i)$ (Existencial): Representa a união de aproximações. Os termos são pares $\langle s, a \rangle$, mas o tamanho $s$ é abstrato (não pode ser usado em correspondência de padrões). A eliminação é restrita a tipos pequenos.
   • $\forall i. A(i)$ (Universal): Representa a interseção de aproximações. As funções atuam uniformemente em qualquer tamanho.
   • Axiomas de Parametricidade: A teoria inclui axiomas afirmando que esses quantificadores comutam com construtores de tipos (por exemplo, $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). Isso internaliza a ideia de que os tamanhos são tratados uniformemente.
3. Indução Bem-Fundada (fix):
   • Um operador de ponto fixo que permite definição por indução sobre tamanhos: $fix\ f : \forall i. A(i)$ dado $f : \forall i. ((\forall j < i. A(j)) \to A(i))$.
   • A regra $\beta$ é proposicional (não definicional) para preservar a decidibilidade da verificação de tipos.

B. Construção de Tipos (Co)indutivos

Os autores codificam tipos (co)indutivos como álgebras iniciais e coalgebras finais para endofuntores polinomiais ($F$).

1. Aproximações Ordinais: Eles definem funtores indexados por tamanho $F[\exists -]$ e $F[\forall -]$. Usando o operador fix, constroem álgebras iniciais ($\mu_3 F$) e coalgebras finais ($\nu_2 F$) para esses funtores indexados por tamanho. Estes representam o tipo truncado em um tamanho específico.
2. Tipos Completos via Quantificação:
   • Tipos Indutivos: Definidos como $\mu F := \exists i. (\mu_3 F) i$. O quantificador existencial coleta todos os termos limitados por algum tamanho.
   • Tipos Coindutivos: Definidos como $\nu F := \forall i. (\nu_2 F) i$. O quantificador universal garante que os termos sejam observáveis em qualquer profundidade.
3. Tratamento de Tipos de Ramificação Infinita: A inovação chave é mostrar que funtores polinomiais comutam fracamente com o quantificador existencial. Isso requer a existência de ordinais limites (supremos de sequências de tamanhos), o que é impossível se os tamanhos forem apenas $\mathbb{N}$.

C. Prova de Consistência: Modelo de Realizabilidade

Para provar que a teoria é consistente, os autores constroem um modelo de realizabilidade baseado no Topos Efetivo de Hyland.

• Interpretação de Tipos:
  • Tipos Pequenos: Interpretados como Relações de Equivalência Parciais (PERs) sobre números naturais (dados computáveis).
  • Tipos Grandes: Interpretados como Montagens (conjuntos com relações de computabilidade).
• Interpretação de Size:
  • O tipo Size é interpretado como $\nabla \omega_1$, onde $\omega_1$ é o primeiro ordinal não enumerável (o conjunto de todos os ordinais enumeráveis).
  • É dada a relação de realizabilidade "completa", significando que os morfismos devem tratar todos os tamanhos uniformemente (parametricidade).
• Validação:
  • Como $\omega_1$ contém ordinais limites, o modelo valida os axiomas de parametricidade necessários para tipos indutivos de ramificação infinita.
  • O modelo valida Impredicatividade (quantificar sobre tipos grandes produz tipos pequenos) e Unicidade de Provas de Identidade (UIP), embora a sintaxe não as assuma. Isso demonstra que a sintaxe é compatível com teorias mais fortes (como a Teoria dos Tipos Homotópica) sem ser restrita por elas.

3. Contribuições Principais

1. Construção Geral de Tipos (Co)indutivos: Diferentemente de abordagens paramétricas anteriores limitadas a tipos de ramificação finita, este trabalho constrói todos os tipos (co)indutivos, incluindo os de ramificação infinita (por exemplo, ordinais de Brouwer, modelos de teoria dos conjuntos construtiva).
2. Resolução da Inconsistência do Agda: Ao substituir o "maior tamanho" inconsistente ($\infty$) por quantificadores paramétricos sobre um tipo grande de tamanhos, os autores fornecem uma alternativa consistente à implementação atual do Agda.
3. Quantificadores Paramétricos como Mecanismo: Eles demonstram que internalizar a parametricidade via $\exists$ e $\forall$ sobre tamanhos impõe efetivamente a abstração necessária para prevenir comportamentos não terminantes e inconsistências lógicas.
4. Modelo de Realizabilidade Robusto: A construção de um modelo onde Size é interpretado como $\omega_1$ fornece uma justificação semântica rigorosa para a teoria, provando que os axiomas de parametricidade são consistentes.

4. Resultados

• Solvência Teórica: O artigo prova que a álgebra inicial e a coalgebra final para qualquer endofunctor polinomial existem dentro da teoria estendida.
• Consistência: O modelo de realizabilidade confirma que a teoria é consistente. Ele mostra que os axiomas para quantificadores paramétricos valem quando os tamanhos são interpretados como um ordinal não enumerável.
• Compatibilidade: As construções não dependem de UIP ou impredicatividade na sintaxe, tornando os resultados compatíveis com a Teoria dos Tipos Homotópica (HoTT), apesar do modelo satisfazer essas propriedades.

5. Significado e Trabalho Futuro

• Impacto em Assistentes de Prova: Este trabalho oferece um caminho para implementar tipos dimensionados em assistentes de prova (como o Agda) sem a inconsistência atual causada pelo tamanho $\infty$. Permite verificações de terminação mais modulares e composicionais.
• Comportamento Computacional: Os autores reconhecem que, embora a teoria seja consistente, a sintaxe atual carece de comportamento computacional para os axiomas de parametricidade (eles são axiomas, não regras de redução). Trabalhos futuros precisam conectar isso com parametricidade interna (por exemplo, via tipos de ponte ou teoria dos tipos cúbicos) para garantir decidibilidade e canonicidade na prática.
• Decidibilidade da Desigualdade: O modelo implica que a desigualdade em tamanhos não é geralmente decidível (devido aos supremos). Os autores sugerem uma abordagem híbrida (desigualdade definicional versus proposicional) para implementação prática.
• Generalização: O modelo poderia potencialmente ser generalizado para outras álgebras combinatórias parciais ou integrado com efeitos e univocidade.

Em resumo, o artigo conecta com sucesso a lacuna entre a necessidade teórica de tipos dimensionados paramétricos e o requisito prático de consistência, permitindo a construção de tipos (co)indutivos complexos em um framework de teoria dos tipos sólido.