Dependent Multiplicities in Dependent Linear Type Theory

Enunciado del Problema
Las teorías de tipos cuantitativas existentes, como la Teoría de Tipos Cuantitativa (QTT) y la Teoría de Tipos Modal Graded, permiten anotaciones de recursos donde las variables tienen multiplicidades que especifican la frecuencia de uso. Sin embargo, estos sistemas suelen depender de multiplicidades estáticas extraídas de un álgebra de recursos fija (por ejemplo, números naturales o semianillos). Esta naturaleza estática crea limitaciones significativas al tratar con lógica de programas que no representan recursos directamente, sino que los organizan, como la ramificación (condicionales) y la recursión.

En los sistemas actuales, una condición booleana utilizada para seleccionar entre dos ramas requiere que ambas ramas consuman recursos idénticos, lo cual a menudo es impráctico dado que las diferentes ramas suelen realizar operaciones distintas. De manera similar, en funciones de orden superior o tipos inductivos (como árboles binarios), el número de veces que se aplica una función o se consume un recurso a menudo depende de valores conocidos solo en tiempo de ejecución (por ejemplo, el número de hojas en un árbol). Los intentos previos de combinar la Teoría de Tipos Dependientes (DTT) con la lógica lineal lucharon con la cuestión de si los tipos que dependen de términos constituyen un "uso" de dichos términos. Aunque McBride y Atkey argumentaron que los tipos son para la contemplación y no para el cómputo (permitiendo la dependencia de variables lineales), su QTT resultante sigue restringiendo las multiplicidades a elementos estáticos, fallando en capturar el uso dinámico de recursos inherente a los programas recursivos y la ramificación dependiente de datos.

Metodología
El artículo propone una nueva teoría de tipos lineal dependiente que incrusta la lógica lineal directamente en una Teoría de Tipos Dependientes intuicionista estándar (la "teoría anfitriona"). La innovación central es el tratamiento de las multiplicidades no como elementos algebraicos estáticos, sino como términos dentro de la propia teoría anfitriona.

1. Dos Relaciones de Consecuencia: El sistema distingue entre dos juicios:
   • $\vdash$: La DTT intuicionista estándar (teoría anfitriona), utilizada para definir tipos, términos y dependencias.
   • $\Vdash$: Un cálculo consciente de recursos donde los términos se derivan de "suministros" (contextos lineales).
2. Suministros como Tipos Intuicionistas: A diferencia de los contextos lineales tradicionales, los suministros en este sistema son términos de la teoría anfitriona. Esto permite que la teoría anfitriona calcule con anotaciones de recursos. Específicamente, el sistema utiliza los números naturales de la teoría anfitriona para definir una "multiplicación" de suministros ($\Delta \hat{m}$), donde $m$ es un término de tipo $\mathbb{N}$. Esta operación permite duplicar un suministro $m$ veces, donde $m$ puede depender de otras variables en el contexto.
3. Multiplicidades Dinámicas: Al permitir que la multiplicidad $m$ sea un término abierto de la teoría anfitriona, el sistema soporta anotaciones de recursos dinámicas. Por ejemplo, una función que mapea sobre un árbol puede especificar que una función $f$ se utiliza exactamente leafs(t) veces, donde leafs(t) se calcula a partir de la estructura del árbol de entrada $t$.
4. Formadores de Tipos: El artículo define versiones lineales de los formadores de tipos estándar de DTT (funciones, pares, booleanos y tipos W) anotados con estas multiplicidades dinámicas. Crucialmente, las reglas de eliminación para booleanos y tipos W permiten que los recursos se distribuyan de manera diferente a través de ramas o constructores basándose en valores en tiempo de ejecución.
5. Semántica: La semántica se caracteriza como "Categorías Lineales con Familias" (lCwF), que son Categorías con Familias (CwF) indexadas en categorías monoidales simétricas. Esta estructura generaliza los CwF Cuantitativos utilizados para QTT.

Contribuciones Clave

• Sintaxis con Multiplicidades Dependientes: El artículo presenta una sintaxis donde las multiplicidades de las variables son términos de la teoría anfitriona, permitiendo la tipificación precisa de programas que involucran ramificación y recursión que anteriormente no eran tipables en sistemas lineales.
• Tipos W Lineales: Un tratamiento principista de los tipos inductivos (específicamente tipos W con posiciones finitas) en un entorno lineal. El sistema proporciona reglas de introducción y eliminación que contabilizan correctamente el uso dinámico de recursos de las estructuras recursivas.
• Caracterización Semántica: Los autores definen las lCwF como el modelo semántico para la teoría, mostrando cómo se combinan los modelos estándar de DTT y los modelos de lógica lineal. Demuestran que este modelo justifica las intrincadas reglas para los tipos W lineales y generaliza los modelos existentes para QTT.
• Realizabilidad y Borrado: Se construye un modelo de realizabilidad (basado en álgebras BCI) para mostrar que el fragmento intuicionista ($\vdash$) puede borrarse para el cómputo, dejando solo el fragmento lineal ($\Vdash$) para la ejecución, similar a los fragmentos 0 y 1 de QTT.
• Implementación: La teoría se implementa en Agda. La implementación utiliza la interpretación semántica (mapeando juicios lineales a términos intuicionistas equipados con testigos de suministro) para crear un verificador de tipos riguroso, aunque aún no práctico.

Resultados

• Expresividad: El sistema tipifica con éxito programas que requieren conteo dinámico de recursos, como una función map para árboles binarios donde el uso de la función de mapeo es proporcional al número de hojas.
• Completitud: El artículo prueba un resultado de completitud para "términos claramente lineales" (términos intuicionistas que no descartan ni duplican valores mediante eliminadores específicos), mostrando que pueden ser tipificados con precisión en el sistema lineal.
• Recuperación de la Lógica Intuicionista: Al introducir un comonad exponencial lineal ("!"), el sistema puede recuperar la lógica intuicionista completa dentro del fragmento lineal, permitiendo el uso ilimitado de recursos donde sea necesario.
• Compromiso de Decidibilidad: Los autores reconocen que la verificación de tipos es indecidible en el caso general porque requiere comparar términos abiertos de números naturales (por ejemplo, verificar si $\Delta \hat{m}$ es igual a $\Delta \hat{n}$). Sin embargo, señalan que la igualdad proposicional en la teoría anfitriona puede utilizarse para convencer al verificador de tipos de la equivalencia de recursos.

Significado
El artículo afirma proporcionar una versión más expresiva de la Teoría de Tipos Cuantitativos al pasar de álgebras de recursos estáticas a multiplicidades dinámicas y computables derivadas de la teoría anfitriona. Al incrustar la lógica lineal en la DTT en lugar de tratarlas como lógicas separadas, el sistema evita la dicotomía restrictiva entre variables intuicionistas y lineales encontrada en trabajos anteriores. Esto permite un "tratamiento principista consciente de recursos" de una gran clase de tipos inductivos y funciones de orden superior. El trabajo demuestra que los lenguajes existentes con tipos dependientes pueden extenderse con este sistema, ofreciendo un camino hacia una gestión de recursos más precisa en la programación funcional sin sacrificar la expresividad de los tipos dependientes. Los autores posicionan su trabajo como una generalización de QTT que resuelve las limitaciones de las multiplicidades estáticas al manejar el uso de recursos dependiente del tiempo de ejecución.