Rzk: a Proof Assistant for Synthetic $\infty$-Categories

Enunciado do Problema
O artigo aborda a necessidade de um assistente de provas capaz de realizar o raciocínio sintético sobre $\infty$-categorias, especificamente $(\infty, 1)$-categorias. Embora a Teoria dos Tipos Homotópicos (HoTT) forneça um arcabouço sintético para $\infty$-grupoides (onde todos os morfismos são invertíveis), ela carece do ferramental para lidar com morfismos direcionados, que são essenciais para a teoria das categorias. A Teoria de Tipos Simpliciais de Riehl e Shulman (RSTT) foi proposta como uma solução, introduzindo "formas" (como intervalos direcionados e triângulos) e "tipos de extensão" para definir morfismos e células de ordem superior definicionalmente. No entanto, a RSTT permanece amplamente um arcabouço teórico; ela não foi implementada em um assistente de provas prático. Os principais desafios para implementar a RSTT incluem tornar a verificação de tipos computacionalmente viável, lidar com as complexas condições de contorno dos tipos de extensão e formalizar as suposições metateóricas (como inclusões de formas) nas quais os teoremas da RSTT frequentemente se baseiam de forma esquemática.

Metodologia
Os autores apresentam o Rzk, um assistente de provas que implementa um refinamento computacional da RSTT. A metodologia envolve três camadas principais de desenvolvimento:

1. Refinamento Teórico (Rzk Declarativo): Os autores definem uma variante declarativa da RSTT (dRzk) que introduz duas mudanças estruturais principais para tornar a teoria mais adequada à implementação:

   • Tipos de Extensão Divididos: Em vez de um único formador de tipo de extensão, o dRzk separa o conceito em um tipo de função indexado por forma (tipo $\Pi$ sobre uma forma) e uma restrição de tipo (anexando um contorno definicional a um tipo arbitrário). Isso permite que o verificador de tipos lide com tipos intermediários onde uma função é aplicada, mas suas condições de contorno ainda não foram totalmente resolvidas.
   • Subtipagem Livre de Coerção: Para lidar com as identificações "silenciosas" frequentemente feitas em provas de artigos (por exemplo, tratar um tipo restrito como seu tipo subjacente), o dRzk introduz uma relação de subtipagem explícita e livre de coerção. Isso garante que os termos permaneçam inalterados durante as verificações de subtipagem, evitando problemas de coerência.

2. Formalização Metateórica: Os autores formalizam a "Camada de Parâmetro Metateórico" (MPL). Os teoremas da RSTT são frequentemente enunciados esquematicamente sobre cubos abstratos, topes (fórmulas lógicas sobre cubos) e famílias de tipos. O Rzk internaliza estes como parâmetros de primeira classe dentro das definições, permitindo que o sistema lide com inclusões de formas e condições laterais explicitamente, em vez de como suposições implícitas de nível meta.

3. Implementação Algorítmica: Os autores implementam uma versão algorítmica (aRzk) que apresenta:

   • Verificação de Tipos Bidirecional: Um algoritmo bidirecional padrão adaptado para carregar o contexto de tope através de todos os julgamentos.
     os
   • Computação Direcionada ao Tipo: A normalização é definida em termos elaborados que fazem cache de seus tipos, pois a redução depende de informações de tipo (especificamente, se um tope de contorno é verdadeiro).
   • Solver de Tope Automatizado: Um protótipo de solver para a lógica de formas (lógica proposicional intuicionista sobre intervalos direcionados) que verifica automaticamente as implicações necessárias para inclusões de formas e condições de contorno.
   • Integração de Subtipagem: A subtipagem é integrada à verificação de igualdade definicional usando uma flag de variância, evitando a inserção de coerções explícitas.

Principais Contribuições

• Assistente de Provas Rzk: A primeira implementação de uma teoria de tipos simpliciais para a teoria de $\infty$-categorias sintética. É escrito em Haskell e funciona como um playground baseado em navegador e via uma extensão para o VS Code.
• Tradução Formal e Conservatividade: Os autores definem uma tradução $\tau$ de RSTT para dRzk e uma tradução reversa $\sigma$. Eles provam que a tradução é fiel (cada prova de RSTT traduz-se em uma prova de Rzk) e conservativa em um fragmento natural de derivações (dRzk não prova nada novo sobre tipos de RSTT). Este fragmento exige que "restrições independentes" (restrições não anexadas a um codomínio de forma-$\Pi$) não sejam assumidas como hipóteses, apenas concluídas.
• Biblioteca sHoTT: Os autores demonstram a utilidade do Rzk através da biblioteca sHoTT, uma biblioteca padrão contendo mais de 25.000 linhas de código e quase 1.500 declarações. Esta biblioteca formaliza conceitos centrais da teoria de $(\infty, 1)$-categorias sintéticas, incluindo tipos de Segal e Rezk, famílias covariantes, adjunções e a primeira formalização do lema de Yoneda $\infty$-categórico.
• Detalhes de Implementação: O artigo detalha os algoritmos específicos para lidar com a lógica de tope, verificação de tipos bidirecional com contextos de tope e a integração de subtipagem na igualdade definicional.

Resultos

• Corretude: O sistema verifica com sucesso a biblioteca sHoTT. Os autores relatam que o solver de tope, embora incompleto, lida com a vasta maioria das consultas na biblioteca de forma eficiente (59% em um único passo, 99% dentro de 35 passos).
• Correções de Bugs: A comparação rigorosa entre a teoria declarativa e a implementação revelou dois bugs de correção (soundness) em versões anteriores (v0.7.7) relacionados à comparação de tipos de identidade e verificações de subtipagem assimétrica, que foram corrigidos na v0.7.8.
• Desempenho: O solver responde por aproximadamente 10% do tempo total de verificação de tipos. O sistema é capaz de lidar com provas complexas, como o lema de Yoneda, sem intervenção manual para inclusões de forma.

Significância e Alegações
O artigo afirma que o Rzk é o primeiro e único assistente de provas para RSTT, preenchendo a lacuna entre a proposta teórica de Riehl e Shulman e a formalização prática. Sua significância reside em:

1. Viabilizar a Teoria de $\infty$-Categorias Sintética: Permite que matemáticos raciocinem sobre $(\infty, 1)$-categorias diretamente dentro da teoria dos tipos, usando tipos de extensão para definir tipos de hom-set e composição definicionalmente, sem contabilidade proposicional.
2. Usabilidade Prática: A existência da sHoTT demonstra que a teoria não é apenas teoricamente sólida, mas também praticável para matemática não trivial.
3. Rigor Teórico: Ao provar a fidelidade e a conservatividade, os autores garantem que o Rzk é uma implementação fiel da proposta original da RSTT, não uma variante divergente.

Os autores permanecem modestos quanto aos problemas em aberto. Eles reconhecem que a conservatividade total para todas as derivações dRzk (incluindo aquelas com restrições independentes em hipóteses) é atualmente uma conjectura. Eles também observam que a terminação da normalização para RSTT não é conhecida em geral, e que o solver de tope é um protótipo que é sólido, mas incompleto. Trabalhos futuros incluem a mecanização da metateoria, a implementação de um backend de normalização por avaliação (normalization-by-evaluation) e a adição de suporte para argumentos implícitos e tipos indutivos superiores.