Nivel 6 · El CIC y Lean

Prop, Type y universos

Las páginas anteriores usaron las sorts $\text{Set}$, $\text{Prop}$ y $\text{Type}$ con una explicación mínima. Esta página las presenta con precisión: qué es una sort, cómo se especifica el CoC como sistema de tipos puro, y por qué la distinción entre $\text{Prop}$ y $\text{Type}$ es la decisión de diseño que separa las proposiciones de los datos.

Sorts: los tipos de los tipos

Una sort es un «tipo de tipos»: la categoría a la que pertenece un tipo, así como un número pertenece a $\mathbb{N}$. Un Sistema de Tipos Generalizado (GTS, o PTS) se especifica con tres datos: las sorts $\mathcal{S}$, los axiomas $\mathcal{A}$ (qué sort habita cada sort) y las reglas $\mathcal{R}$ (qué dependencias de producto están permitidas) (Barendregt, 1991) .

El diccionario con la notación del cubo lambda es directo: $\Pi x{:}A.\,B \leftrightarrow (x{:}A)\,B$, $\lambda x{:}A.\,t \leftrightarrow [x{:}A]\,t$, $*$ (tipos habitables) $\leftrightarrow \text{Set}$, y $\square$ (kinds) $\leftrightarrow \text{Type}_S$.

La jerarquía de universos

Detenerse en dos sorts genera una incomodidad: si $\text{Set} : \text{Type}_S$, ¿en qué vive $\text{Type}_S$? Postular $\text{Type}_S : \text{Type}_S$ conduce a inconsistencia (la paradoja de Girard, análoga en teoría de tipos a la paradoja de Russell). La solución de Coq y Lean es una jerarquía infinita y predicativa de universos:

Predicativa significa que un producto $(x{:}A)\,B$ cuantificando sobre un universo $\text{Type}_i$ aterriza en un universo estrictamente mayor: no se puede definir un habitante de $\text{Type}_i$ cuantificando sobre todo $\text{Type}_i$. En Lean, Type u abrevia Sort (u+1) y la jerarquía completa es Sort 0, Sort 1, Sort 2, ..., con Prop = Sort 0 y Type = Type 0 = Sort 1.

La sort $\text{Prop}$, en cambio, es impredicativa: el producto $(A{:}\,\text{Prop})\,A \to A \to A$ cuantifica sobre todas las proposiciones y, sin embargo, es él mismo una proposición (habita $\text{Prop}$). Esta es exactamente la capacidad que las codificaciones impredicativas de la primera página explotan. La impredicatividad es consistente en $\text{Prop}$ precisamente porque sus habitantes se tratan como proposiciones sin contenido computacional relevante y su eliminación está restringida, como se vio en la nota sobre restricciones de eliminación.

Proposiciones borrables frente a datos

La consecuencia práctica de la nota anterior merece desarrollarse, porque gobierna el diseño de toda formalización en Lean.

• Un dato en $\text{Type}$ importa por su valor. Dos habitantes distintos de $\mathbb{N}$ son objetos matemáticos distintos: $3 \neq 5$. Al compilar un programa, los datos deben conservarse.
• Una prueba en $\text{Prop}$ importa solo por su existencia. Si $h_1$ y $h_2$ son dos pruebas de la misma proposición $\varphi$, ningún cómputo puede distinguirlas: las restricciones de eliminación garantizan que ningún dato en $\text{Type}$ puede depender del contenido de una prueba en $\text{Prop}$ (salvo la eliminación singleton). Por eso el compilador puede borrarlas: en el código ejecutable las pruebas desaparecen sin alterar ningún resultado.

Este es el sentido preciso de la irrelevancia de pruebas. Y explica la decisión de diseño que el lector verá en el módulo 07: el tipo Formula de las fórmulas proposicionales vive en Type, porque una fórmula es un dato sobre el que se computa (se evalúa una valuación , se mide su tamaño, se recorre su árbol sintáctico); la relación de derivabilidad vive en Prop, porque de una derivación solo interesa que exista. Ambos son tipos inductivos , pero habitan sorts distintas por razones matemáticas precisas.

inductive Formula : Type where          -- dato: se computa con él
  | bot  : Formula
  | var  : Nat → Formula
  | impl : Formula → Formula → Formula

inductive ND : List Formula → Formula → Prop where  -- proposición: solo importa su existencia
  | ax   : φ ∈ Γ → ND Γ φ
  -- ... (una regla de inferencia por constructor)