Setoids in Intensional Type Theory

Resumo Técnico: Setoids em Teoria de Tipos Intensional

Problema
O artigo aborda o desafio de construir um modelo para a Teoria de Tipos Extensional com Universos (ETU) dentro da Teoria de Tipos Intensional (ITT). Embora a ITT (especificamente a versão implementada no Agda com --safe e --without-K, referida como IRU) seja amplamente utilizada para formalizar a sintaxe e a meta-teoria, ela carece dos princípios de extensionalidade (como a extensionalidade de funções e a unicidade de provas de identidade) inerentes à ETU. O autor observa que, embora a literatura contenha modelos de setoids para extensionalidade, faltava uma construção totalmente verificada por máquina de uma semântica para a ETU dentro do sistema IRU básico. Abordagens existentes, como Palmgren (2022), ou deixam as funções semânticas e as provas de correção implícitas ou dependem de condições de coerência mais complexas e interpretações de teoria dos conjuntos. Além disso, definir a semântica para expressões bem formadas (em vez de apenas derivações de bem-formação) na ITT apresenta "dificuldades técnicas surpreendentes" devido à falta de igualdade definicional para igualdade proposicional, exigindo o tratamento cuidadoso de funções parciais e irrelevância de prova.

Metodologia
O artigo emprega uma abordagem de "setoid exibida" (displayed setoid) para modelar tipos dependentes no IRU. A metodologia procede da seguinte forma:

1. Estrutura (IRU): A construção ocorre no Safe Agda (IRU), que inclui tipos de funções dependentes, tipos de registros dependentes, tipos de dados indutivos (com --without-K) e uma hierarquia de universos fechada sob definições indutivo-recursivas (IRU).
2. Setoids Exibidas: A inovação central é o uso de uma noção específica de "setoid exibida" (Definição 3.2). Diferente de abordagens anteriores que exigem condições de coerência complexas ou proposições de irrelevância de prova (SProp), esta definição utiliza setoids "selvagens" (wild) onde as relações de equivalência são valoradas em Set. Para lidar com a dependência de tipos sobre termos sem depender de proposições de irrelevância de prova, os autores substituem o produto dependente na relação de equivalência por um produto cartesiano. Isso exige o tratamento explícito de equivalência "heterogênea" e a inclusão de termos de coerção (coe) e coerência (coh) para gerenciar a regra de conversão da teoria de tipos dependente.
3. Universos de Setoids: Os autores constroem uma hierarquia contável de universos de setoids ($U_l$) e setoids exibidas associadas ($E\ell_l$) usando definições indutivo-recursivas. Estes universos contêm códigos para:
   • Números naturais e o tipo vazio.
   • Tipos de igualdade extensional.
   • Tipos de produto dependente ($\Pi$-tipos) com conversão $\eta$.
   • Uma hierarquia de universos propriamente ditos.
   • Crucialmente, um universo de setoid separado ($C$) para contextos de tipagem, permitindo a modelagem da igualdade definicional de contextos.
4. Representação Sintática: A sintaxe da ETU é formalizada extrinsecamente usando uma representação "localmente sem nome bem escalonada" (well-scoped locally nameless). Julgamentos (bem-formação de contextos, tipos e termos) são definidos indutivamente como tipos de dados no Agda.
5. Construção da Semântica: Seguindo a estratégia de Streicher (1991), os autores definem funções semânticas parciais sobre a sintaxe bruta. Eles então provam que essas relações são totais e de valor único (no sentido de setoids) para todas as expressões bem formadas. Isso envolve definir relações semânticas para contextos, tipos e termos, e provar sua correção com relação à igualdade definicional.

Contribuições Principais

• Definição de Setoid Exibida: O artigo introduz uma definição simplificada de setoids exibidas (Definição 3.2) que evita as complexas condições de coerência encontradas em Palmgren (2022) e não requer um universo de proposições de irrelevância de prova. Ela se baseia em produtos cartesianos e termos de coerência explícitos para gerenciar a heterogeneidade.
• Universo de Contexto: A construção inclui um universo de setoid especificamente para códigos de contextos de tipagem ($C$), um recurso que o autor nota ser novo neste contexto. Isso permite um tratamento semântico direto da igualdade de contextos.
• Semântica Completa em IRU: O artigo fornece uma formalização completa, verificada por máquina, da semântica da ETU dentro do IRU. Isso inclui a definição das funções semânticas para todos os construtores de tipos (incluindo $\Pi$-tipos e igualdade extensional) e a prova de suas propriedades (totalidade, valor único e correção).
• Prova de Consistência: Como um corolário direto da semântica, o artigo deriva uma prova verificada por máquina da consistência da ETU dentro do IRU.

Resultados

• Teorema 6.8 (Consistência): O artigo prova que existe um termo IRU do tipo $\neg (\Sigma_{a \in \text{Tm}} (\diamond \vdash a :_0 \text{Emp}))$. Isso estabelece que a ETU é consistente em relação ao IRU. A prova baseia-se no fato de que a interpretação semântica do tipo vazio no modelo construído é verdadeiramente vazia (uma função de um tipo unidade para o tipo vazio), e que qualquer derivação de um habitante do tipo vazio levaria a uma contradição no modelo.
• Correção (Soundness): As relações semânticas são provadas corretas com relação às regras de igualdade definicional da ETU (Teorema 6.7 e Seção 6.5). Especificamente, se dois termos são definicionalmente iguais na ETU, suas interpretações semânticas são equivalentes no setoid correspondente.

Significância
O artigo reivindica significância principalmente em fundamentos. Ele esclarece a extensão em que construções semânticas para linguagens que dependem de extensionalidade podem ser realizadas dentro de uma teoria de tipos intensional.

• Interesse Fundamental: Demonstra que uma semântica "inspirada em Streicher" para a teoria de tipos extensional pode ser alcançada em um ambiente intensional muito minimalista (IRU) sem assumir axiomas de extensionalidade ou usar tipos indutivos de quociente complexos.
• Formalização Prática: Serve como uma formalização verificável por máquina desses conceitos no Safe Agda, fornecendo um exemplo concreto de como lidar com as dificuldades técnicas da semântica intensional (como funções parciais e irrelevância de prova) sem recorrer a pressupostos lógicos mais fortes.
• Meta-Teoria: O trabalho apoia o uso da teoria de tipos intensional para representar a sintaxe de vários linguagens e investigar sua meta-teoria, mostrando que propriedades extensionais podem ser modeladas internamente via setoids. O autor observa que, embora o modelo possa não ter aplicações computacionais diretas, é um passo necessário para compreender a consistência relativa da extensionalidade em sistemas intencionais e para trabalhos futuros sobre versões intencionais de construções como a normalização por avaliação em teoria de tipos dependentes.