Directed proof-relevant logical relations in simplicial HoTT

Resumo Técnico: Relações Lógicas com Relevância de Prova Direcionada em Simplicial HoTT

Enunciado do Problema
As relações lógicas tradicionais com relevância de prova (frequentemente formuladas via colagem categórica) interpretam tipos como famílias de termos computáveis, onde os predicados de computabilidade são famílias de tipos em vez de meras proposições. Em apresentações equacionais de teoria de tipos, a igualdade julgamental é representada pela igualdade meta-teórica, e as relações lógicas dependem de um lema de "fechamento sob expansão": se um termo $M$ reduz a $M'$, e $M'$ é computável, então $M$ é computável. No entanto, esta abordagem trata a computação como uma relação simétrica (via igualdade) ou depende de provas manuais de fechamento para trás. Ela não internaliza nativamente a natureza direcionada da redução, onde termos evoluem para outros termos ($M \to M'$), mas não necessariamente o contrário. O artigo aborda o desafio de construir uma relação lógica com relevância de prova que dê conta de reduções direcionadas internamente, sem depender de relações de redução externas ou lemas de expansão de irrelevância de prova.

Metodologia
Os autores desenvolvem seu framework dentro da teoria de tipos homotópica simplicial (Simplicial HoTT), uma extensão direcionada da HoTT que inclui um intervalo direcionado e tipos de desigualdade ($x \leq_A y$).

1. Sintaxe Direcionada via QIITs Direcionadas:
   A sintaxe da linguagem-objeto é apresentada como um tipo indutivo-indutivo de quociente direcionado (directed QIIT). Diferente das QIITs padrão que são quotientadas por igualdades julgamentais (construtores de caminho), esta sintaxe inclui construtores direcionados que geram tipos de desigualdade. Por exemplo, a redução $\beta$ para produtos é internalizada como uma desigualdade:
   $$\times\beta_1 : \text{fst}(\text{pair } a \, b) \leq a$$
   A sintaxe é construída para ser um "tipo Segal fino", garantindo que as reduções componham e que as desigualdades entre os mesmos pontos sejam únicas (irrelevantes à prova), modelando um pré-ordem em vez de uma categoria geral.

2. Contravariância como Expansão com Relevância de Prova:
   A principal intuição teórica é que as famílias contravariantes na teoria de tipos simplicial fornecem exatamente a estrutura necessária para o fechamento com relevância de prova sob expansão. Neste cenário, um predicado de computabilidade $A^\bullet$ para um tipo $A$ não é apenas uma família de tipos; ele deve ser uma família contravariante.

   • Definição: Uma família $C: X \to \mathcal{U}$ é contravariante se, para cada desigualdade $f: x \leq_X y$ e testemunha $v: C(y)$, o tipo dos levantamentos $\sum_{u:C(x)} u \leq_{C(f)} v$ for contraível.
   • Implicação: Esta contração garante uma operação de "transporte para trás" única e funcional $f^*: C(y) \to C(x)$. Esta operação internaliza o lema de expansão: a evidência de computabilidade pode ser transportada para trás ao longo de reduções de modo a respeitar identidades e composição automaticamente.

3. Tratamento de Tipos Dependentes e Universos:
   A extensão para tipos dependentes introduz um conflito: a conversão de tipos requer igualdade simétrica, mas a sintaxe fornece apenas desigualdades direcionadas.

   • Discretização: Os autores discretizam o universo de tipos ($Ty$) adicionando um construtor que transforma desigualdades de tipos em igualdades ($A \leq Ty B \implies A = Ty B$). Isso permite a conversão de tipos padrão enquanto preserva as reduções direcionadas para termos.
   • Modalidade Flat: Para manter a relevância de prova para predicados de universo sem perder a discretização, os autores empregam a modalidade flat ($\flat$) da teoria de tipos crisp. Os predicados de computabilidade para universos são armazenados como códigos flat. Como $\flat X$ é discreto, as desigualdades entre predicados colapsam em igualdades, garantindo a unicidade necessária para a testemunha de computabilidade do universo.

Principais Contribuições

1. Sintaxe de Quociente Direcionada: Uma formalização de sintaxe de teoria de tipos onde as reduções julgamentais são internalizadas como desigualdades direcionadas via directed QIITs.
2. Contravariância como Expansão: A identificação de famílias contravariantes em teoria de tipos simplicial como a generalização com relevância de prova do lema de expansão, provendo funcionalidade intrínseca e propriedades universais para o transporte para trás.
3. Modelo de Relação Lógica Unária: Uma construção de um modelo de relação lógica unária que prova a canonicidade booleana direcionada: todo termo booleano fechado $M$ satisfaz $M \leq \text{true}$ ou $M \leq \text{false}$.
4. Mecanização: Uma prova de conceito mecanizada em Cubical Agda para o fragmento simplesmente tipado (produtos, funções, Booleanos), demonstrando a viabilidade da abordagem direcionada.
5. Extensão para Tipos Dependentes e Universos: Uma solução para tipos dependentes usando a discretização de tipos e a modalidade flat para lidar com predicados de universo.
6. Parametricidade Binária: Uma adaptação do método para relações lógicas binárias, separando as reduções verticais (contravariância) da parametricidade horizontal, ilustrada via um argumento de independência de representação para filas (queues).

Resultos

• Canonicidade Direcionada: O teorema fundamental das relações lógicas é estabelecido para o cenário direcionado. Para qualquer termo booleano fechado $M$, o modelo produz uma testemunha de que $M$ reduz a um booleano canônico.
• Independência de Representação: A relação lógica binária separa com sucesso a dimensão vertical (redução/contravariância) da dimensão horizontal (parametricidade), permitindo contas de independência de representação onde a relação é um span em vez de um zig-zag.
• Mecanização: O fragmento simplesmente tipado, incluindo a construção da sintaxe direcionada e o modelo de relação lógica, foi formalizado em Cubical Agda.

Significância e Alegações
O artigo afirma fornecer uma internalização tipográfica da ideia de que as relações lógicas devem validar canonicidade e parametricidade mesmo quando a sintaxe é apresentada por reduções em vez de igualdades.

• Unificação Teórica: Unifica a visão operacional de computação (redução direcionada) com a visão semântica de relações lógicas (colagem com relevância de prova) ao alavancar a estrutura direcionada nativa da teoria de tipos simplicial.
• Novo Papel para a Contravariância: Ele eleva as famílias contravariantes de uma ferramenta para teoria de categorias sintéticas a um mecanismo fundamental para relações lógicas, substituindo lemas de expansão ad-hoc por uma propriedade universal.
• Modéstia: Os autores observam que o resultado é "não surpreendente" em sua conclusão (relações lógicas devem funcionar para reduções), mas significativo em sua internalização. Eles reconhecem que a extensão para tipos dependentes apresenta desafios significativos de transporte e que a mecanização atual é limitada ao caso simplesmente tipado. Eles não pretendem ter resolvido todos os problemas relativos a tipos de identidade em cenários direcionados, sugerindo trabalhos futuros envolvendo distinções de fase ou modalidades monádicas.

O trabalho demonstra que a teoria de tipos simplicial não é apenas uma ferramenta para teoria de $\infty$-categorias sintéticas, mas também uma metateoria viável para raciocinar sobre a semântica de redução de linguagens de programação e teorias de tipos.