A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

A continuación presento un resumen técnico detallado del artículo "A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism" (Una teoría algebraica generalizada para la teoría de tipos con polimorfismo explícito de universos), escrito por Marc Bezem, Thierry Coquand, Peter Dybjer y Martín Escardó.

1. Problema y Contexto

El artículo aborda la necesidad de proporcionar una caracterización abstracta y uniforme de las teorías de tipos, específicamente aquellas que incluyen polimorfismo de universos explícito.

• El desafío: Las presentaciones tradicionales de la teoría de tipos se basan en gramáticas y reglas de inferencia. Estas presentaciones dependen de elecciones sintácticas específicas y requieren numerosas reglas de "contabilidad" (como reglas de igualdad generales), lo que dificulta probar la equivalencia entre diferentes opciones sintácticas y establecer una noción matemática única y abstracta de la teoría.
• El objetivo de Voevodsky: El trabajo se alinea con el proyecto de la "Conjetura de Inicialidad" de Vladimir Voevodsky, que busca definir una clase general de teorías de tipos dependientes y desarrollar una metateoría genérica. La conjetura postula que el modelo de términos de una teoría de tipos debe ser un objeto inicial en la categoría de sus modelos.
• La limitación actual: Aunque se han probado casos particulares (como la teoría de tipos de Martin-Löf con una torre externa de universos), falta un marco unificado que maneje el polimorfismo de universos explícito (donde los niveles de universo son variables y no fijos) de manera algebraica y categórica.

2. Metodología

Los autores utilizan un enfoque basado en la Lógica Categórica, específicamente empleando:

• Teorías Algebraicas Generalizadas (GATs): Introducidas por Cartmell, son una generalización de las teorías algebraicas de muchas clases donde los símbolos de sortos y operadores pueden tener tipos dependientes.
• Familias con Contextos (CwFs): Estructuras categóricas que modelan las reglas básicas de la teoría de tipos dependientes (formación de contextos, morfismos de contexto, sustitución, etc.).

Estrategia de construcción:
En lugar de definir las teorías mediante reglas de inferencia, los autores definen dos GATs específicas. El objetivo es demostrar que las teorías de tipos correspondientes son modelos iniciales de estas GATs. Esto permite abstraer los detalles sintácticos y centrarse en la estructura categórica de alto nivel.

El trabajo se divide en dos presentaciones principales:

A. Teoría con una Torre Externa de Universos ($\Sigma_{tower}$)

• Objetivo: Caracterizar la teoría de tipos de Martin-Löf con una torre de universos indexada externamente por números naturales ($l \in \mathbb{N}$).
• Enfoque: Se presenta una GAT infinitaria ($\Sigma_{tower}$) que extiende la GAT de CwFs con operadores para los formadores de tipos pequeños ($\Pi, \Sigma, N, W, Id$, etc.) y una torre de universos $U_l$.
• Mecanismo: Los universos y sus códigos se tratan como operadores indexados externamente. Se define un modelo de términos $T_{\Sigma_{tower}}$ como la unión de modelos finitos truncados.

B. Teoría con Polimorfismo Explícito de Universos ($\Sigma_{up}$)

• Objetivo: Caracterizar la teoría de tipos con polimorfismo explícito, donde los niveles de universo son variables internas y existen productos indexados por niveles.
• Enfoque: Se presenta una GAT finitaria ($\Sigma_{up}$) basada en CwFs indexados por niveles.
• Estructura Jerárquica:
  1. UCWF de Niveles: Primero se define una "Familia con Contextos de un solo tipo" (ucwf) para los niveles de universo. Esto incluye sortos para contextos de niveles, morfismos de niveles y términos de niveles.
  2. Operadores de Niveles: Se introducen operadores para la unión de niveles ($\vee$) y la función "siguiente nivel" ($+$), formando un semilattice superior.
  3. Sortos de Igualdad de Niveles: Para manejar restricciones como $l < m$ (definido como $l^+ \vee m = m$) dentro de la GAT, se introduce un nuevo sorto leq y un operador de reflexividad. Esto permite expresar condiciones de orden sin violar las reglas de las GATs.
  4. CwF Indexado: Se define un CwF donde los contextos, tipos y términos dependen de un contexto de niveles $n$. Los operadores de sustitución de niveles actúan sobre esta estructura.
  5. Universos Internos y Productos: Se añaden operadores para universos indexados por niveles ($U_l$), sus decodificaciones y productos indexados por niveles ($[\alpha]A$).

3. Contribuciones Clave

1. Caracterización Algebraica de Universos Explícitos: Se logra la primera presentación completa de una GAT para la teoría de tipos de Martin-Löf con polimorfismo de universos explícito y productos indexados por niveles.
2. Abstracción de la Sintaxis: Al definir estas teorías como modelos iniciales de GATs, se demuestra que la esencia de la teoría reside en su estructura categórica, independientemente de la sintaxis concreta (gramática) o las reglas de inferencia específicas.
3. Tratamiento de la Igualdad de Niveles: La introducción del sorto leq y el operador de reflexividad es una innovación técnica crucial. Permite codificar restricciones de orden entre niveles de universo dentro del marco de las GATs, superando la limitación de que las GATs no permiten igualdades como hipótesis directas.
4. Construcción de Modelos Iniciales: Se esbozan las construcciones de los modelos iniciales tanto para la torre externa ($T_{tower}$) como para la teoría indexada por niveles ($T_{up}$), demostrando que son objetos iniciales en sus respectivas categorías de modelos ($CwF_{tower}$ y $CwF_{up}$).
5. Conexión con la Conjetura de Inicialidad: El trabajo proporciona un marco formal robusto para abordar la Conjetura de Inicialidad de Voevodsky, mostrando cómo las teorías de tipos complejas pueden definirse como modelos iniciales de estructuras algebraicas.

4. Resultados

• Existencia de Modelos Iniciales: Se establece que para cada presentación finita de una GAT (como $\Sigma_{up}$), existe un modelo de términos inicial. Para la GAT infinitaria ($\Sigma_{tower}$), el modelo inicial se construye como un límite de modelos finitos truncados.
• Equivalencia de Enfoques: Se demuestra que la construcción basada en sustitución explícita (dentro de la GAT) es isomorfa a la construcción basada en sustitución implícita (la teoría de tipos estándar con reglas de inferencia), validando que la GAT captura correctamente la teoría.
• Generalización: El enfoque no se limita a la teoría de tipos dependientes; los autores sugieren que variaciones de CwFs indexados pueden capturar otros sistemas lógicos (lógica de predicados no tipada, lógica de predicados tipada, etc.) de manera uniforme.

5. Significado e Impacto

Este trabajo es significativo por varias razones:

• Unificación Teórica: Ofrece una visión unificada de la lógica categórica basada en GATs y CwFs, demostrando que es posible formalizar sistemas complejos como el polimorfismo de universos explícito sin depender de detalles sintácticos frágiles.
• Avance en la Metateoría: Proporciona las herramientas necesarias para desarrollar metateoría genérica para clases de teorías de tipos, un paso esencial para el proyecto de Voevodsky sobre fundamentos univalentes.
• Herramienta para la Verificación Formal: Al caracterizar las teorías como modelos iniciales, se facilita la implementación y verificación en asistentes de prueba (como Agda o Coq), ya que se puede trabajar con la estructura algebraica abstracta en lugar de manipular reglas de inferencia ad hoc.
• Puente entre Lógica y Álgebra: Refuerza la idea de que los sistemas de deducción formal pueden tratarse como teorías cuasi-equacionales, permitiendo el uso de herramientas algebraicas para estudiar propiedades de sistemas lógicos complejos.

En resumen, el artículo representa un avance fundamental en la comprensión categórica de las teorías de tipos modernas, proporcionando un marco algebraico riguroso para el polimorfismo de universos explícito y sentando las bases para futuros trabajos en la formalización de fundamentos matemáticos unificados.