Nivel 6 · El CIC y Lean

Tipos inductivos

El CIC es una extensión del CoC que resuelve los problemas de la página anterior añadiendo una herramienta fundamental: la capacidad de definir tipos inductivos de forma nativa. En lugar de codificar los números naturales, simplemente se los declara especificando sus reglas de construcción: un conjunto $\texttt{nat}$ con dos constructores,

un constructor para el cero: $0 : \texttt{nat}$ , y
una función sucesor: $S : \texttt{nat} \to \texttt{nat}$ .

Esta simpleza le da al sistema toda la información que necesita. El CIC entiende que un natural es, o bien $0$ , o bien el $S$ de otro natural, y nada más. A partir de esta definición, el sistema genera automáticamente las herramientas de razonamiento y cómputo asociadas (la página siguiente las estudia en detalle). El desarrollo formal sigue el artículo de Paulin-Mohring Paulin-Mohring (1993) .

De la intuición al formalismo: gramática y convenciones

Para enunciar las reglas con precisión se adopta la notación de los Sistemas de Tipos Generalizados (GTS), también llamados Pure Type Systems (PTS) (Paulin-Mohring, 1993) . La sintaxis abstracta de términos es

t ::= s \mid x \mid (x{:}t)\, t \mid [x{:}t]\, t \mid (t\ t)

donde $s$ recorre el conjunto de sorts. Se usan las convenciones estándar:

Producto dependiente: $(x{:}A)\,B$ denota $\Pi x{:}A.\,B$ .
Abstracción: $[x{:}A]\,t$ denota $\lambda x{:}A.\,t$ .
Flecha como caso particular: si $x \notin FV(B)$ , se escribe $A \to B \equiv (x{:}A)\,B$ .
Asociatividad: la flecha asocia a la derecha, la aplicación a la izquierda.
Sustitución: $M[x := N]$ es la sustitución de $N$ por las ocurrencias libres de $x$ en $M$ .

El símbolo $::=$ proviene de la notación BNF y define reglas de producción sintáctica; no debe confundirse con la igualdad matemática. Un tratamiento detallado de los GTS puede encontrarse en Barendregt (1991) . La página sobre universos volverá sobre las sorts; por ahora basta leer $\text{Set}$ como «la sort de los tipos de datos».

Aridades y formas de constructor

Definición (Aridad)

Una aridad de una sort $s$ describe la forma del tipo inductivo que se va a definir. Se genera por la gramática

Ar ::= s \mid (x : M)\,Ar.

Por ejemplo, la aridad de $\texttt{nat}$ es $\text{Set}$ , mientras que la de las listas (parametrizadas por un tipo) es $(A{:}\,\text{Set})\,\text{Set}$ (Paulin-Mohring, 1993) .

Lean no usa la palabra aridad; su documentación describe la firma del constructor de tipo como una secuencia de argumentos (un «telescopio»): primero los parámetros, después los índices, y al final la sort de retorno. En particular, List tiene firma $(\alpha{:}\,\texttt{Type}\ u)\,\texttt{Type}\ u$ y Fin tiene $(n{:}\,\mathbb{N})\,\texttt{Type}$ :

#check List   -- : Type u → Type u    -- parámetro α
#check Fin    -- : Nat → Type         -- parámetro n

Nota (Parámetros frente a índices)

La firma externa Nat → Type no distingue entre parámetro e índice; la diferencia está en la definición. Un parámetro aparece uniformemente a la izquierda de los dos puntos en toda la declaración: en Lean 4, el argumento $n$ de Fin es un parámetro. Un índice genuino, en cambio, es fijado por cada constructor en su conclusión: el ejemplo canónico es el segundo argumento de Eq : α → α → Prop, que el constructor Eq.refl a instancia en a. Los parámetros son constantes a lo largo de la definición; los índices varían con cada constructor.

Definición (Tipo estrictamente positivo)

Sea $A$ una aridad y $X$ una variable de tipo $A$ . Un tipo $P$ es estrictamente positivo con respecto a $X$ si $X$ no aparece a la izquierda de ninguna flecha $\to$ , a ninguna profundidad de anidamiento. Un tipo estrictamente positivo bien formado puede escribirse como $(\vec{x} : \vec{M})(X\ \vec{m})$ , con la restricción de que $X$ no aparece libremente en ningún término de $\vec{M}$ ni de $\vec{m}$ .

La notación vectorial denota secuencias finitas, posiblemente vacías: $(\vec{x} : \vec{M})$ abrevia $(x_1 : M_1)\dots(x_n : M_n)$ , y $(X\ \vec{m})$ es la aplicación de $X$ a argumentos $m_1 \dots m_k$ , cuya longitud viene dada por la aridad de $X$ .

Nota (Positividad estricta y consistencia)

La condición es estrictamente más fuerte que prohibir las posiciones contravariantes: en $(X \to A) \to B$ la ocurrencia de $X$ es covariante (dos inversiones) y, sin embargo, el tipo no es estrictamente positivo; en presencia de impredicatividad, admitir tales tipos también compromete la consistencia. La razón de fondo es la siguiente: si se admitiera una ocurrencia negativa, por ejemplo un constructor de tipo $(X \to \bot) \to X$ , se podría fabricar un punto fijo y, con él, un habitante de $\bot$ , reproduciendo dentro del sistema de tipos la paradoja de Russell. La positividad estricta es la barrera que lo impide.

Definición (Forma de constructor)

Sea $A$ una aridad y $X$ una variable de tipo $A$ . Un término $C$ es una forma de constructor con respecto a $X$ si es un tipo cuya conclusión es $X$ y donde todas las ocurrencias de $X$ en los tipos de sus argumentos son estrictamente positivas.

Por ejemplo, en la definición de los naturales, la aridad es $\text{Set}$ y $X$ una variable de tipo $\text{Set}$ ; los tipos de los constructores son $X$ (para $0$ ) y $X \to X$ (para $S$ ). Ambos son formas de constructor válidas. Los constructores realizan la introducción del tipo inductivo. En Lean:

#check Nat.zero     -- Nat
#check Nat.succ     -- Nat → Nat
#check List.nil     -- List α
#check List.cons    -- α → List α → List α

Las reglas de formación e introducción

Se introducen nuevos pseudo-términos para representar las definiciones inductivas y sus constructores. Conviene subrayar que $\text{Ind}$ , $\text{Constr}$ y $\text{Elim}$ son pseudo-términos de Paulin-Mohring (Paulin-Mohring, 1993) para describir la maquinaria interna del núcleo; no son sintaxis de Lean: allí se realizan con la palabra clave inductive (formación), los nombres de los constructores (introducción) y el eliminador .rec que el sistema genera.

Formación (Ind). Se introduce el constructor de términos $\text{Ind}(X{:}A)\ \lbrace C_1 \mid \dots \mid C_n \rbrace$ . Si $A$ es una aridad de $s$ y cada $C_i$ es una forma de constructor de $X$ bien tipada en la sort $s$ (bajo el supuesto $X : A$ ), el tipo inductivo está bien formado y tiene tipo $A$ :

\frac{\text{arity}(A, s) \qquad (\forall i = 1 \dots n)\ \ \Gamma,\, X{:}A \vdash C_i : s \qquad \text{constructor}(C_i, X)}{\Gamma \vdash \text{Ind}(X{:}A)\lbrace C_1 \mid \ldots \mid C_n \rbrace : A} \quad (\text{Ind})

El símbolo $\mid$ actúa como separador sintáctico de la lista de constructores; semánticamente denota que el tipo inductivo es una unión disjunta generada por estas reglas: un término habita el tipo si fue construido mediante $C_1$ o $C_2$ … o $C_n$ .

Ejemplo 10.4 (Números naturales)

Para definir el tipo de los números naturales se utiliza la aridad $A = \text{Set}$ . La variable $X$ representa al propio tipo $\texttt{nat}$ dentro de la definición.

El constructor del cero tiene tipo $\texttt{nat}$ , que se escribe formalmente como $X$ .
El constructor del sucesor tiene tipo $\texttt{nat} \to \texttt{nat}$ , que se escribe formalmente como $X \to X$ .

Por lo tanto, la definición formal es

\texttt{nat} \equiv \text{Ind}(X{:}\,\text{Set})\lbrace X \mid X \to X \rbrace.

Esto ilustra cómo el separador $\mid$ distingue entre el caso base (cero) y el caso recursivo (sucesor).

Introducción (Constr). Para cada tipo inductivo $I := \text{Ind}(X{:}A)\lbrace C_1 \mid \dots \mid C_n \rbrace$ se introducen términos $\text{Constr}(i, I)$ , con $1 \le i \le n$ . La regla de tipado asigna a cada constructor el tipo de su especificación, sustituyendo la variable abstracta $X$ por el propio tipo inductivo $I$ :

\frac{\Gamma \vdash I : A \qquad 1 \le i \le n}{\Gamma \vdash \text{Constr}(i, I) : C_i[X := I]} \quad (\text{Constr})

En Lean, la declaración correspondiente es directa y el paralelismo con el formalismo es exacto:

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

inductive List (α : Type u) where
  | nil  : List α
  | cons : α → List α → List α

Con la formación y la introducción en la mano, falta la pieza que dota al sistema de poder lógico y computacional: el principio de eliminación, tema de la página siguiente.