Teoría de tipos cúbicos

En lógica matemática y ciencias de la computación teórica , la teoría de tipos cúbicos es una variante de la teoría de tipos que proporciona una interpretación computacional a los fundamentos univalentes (también conocida como teoría de tipos homotópicos ).

En la teoría de tipos cúbicos, la extensionalidad y la univalencia de las funciones no se postulan como axiomas, sino que se pueden demostrar como teoremas. A diferencia de la teoría de tipos homotópicos tradicional, donde el postulado de univalencia crea términos cerrados fijos, la teoría de tipos cúbicos posee la propiedad de canonicidad . ^{[ 1 ]} También goza de normalización . ^{[ 2 ] [ 3 ]}

Esto se logra añadiendo primitivas geométricas a las reglas básicas de la teoría de tipos, incluyendo un objeto de intervalo formal, variables de intervalo y operaciones para rellenar cubos parciales.

La primera teoría de tipo cúbico es la teoría de tipo cúbico CCHM, que recibe su nombre de sus inventores Cohen, Coquand , Huber y Mörtberg. ^{[ 4 ]} Las variantes posteriores incluyen la teoría de tipo cúbico cartesiano. ^{[ 5 ] [ 6 ]}

Las teorías de tipos cúbicos tienen semántica en varios tipos de conjuntos cúbicos .

El asistente de pruebas Agda incluye una implementación de la teoría de tipos cúbicos. ^{[ 7 ] [ 8 ]}

• Teoría de tipos cúbicos en el Laboratorio n