Nivel 6 · El CIC y Lean

Recursores y eliminación

La consecuencia más profunda de definir un tipo por sus constructores es que el sistema puede generar automáticamente su principio de eliminación, también conocido como recursor . Esta página lo presenta primero en el caso familiar de $\mathbb{N}$ , luego en su forma esquemática general, y cierra con la regla de cómputo que lo hace efectivo: la $\iota$ -reducción.

El recursor de los naturales

Para los números naturales, el recursor permite definir funciones por recursión primitiva. El artículo de Paulin-Mohring (Paulin-Mohring, 1993) lo denota $R(C, x, f, n)$ , con las siguientes reglas de cómputo:

$R(C, x, f, 0)$ se comporta como $x$ ;
$R(C, x, f, (S\ n))$ se comporta como $(f\ n\ R(C, x, f, n))$ ;

donde $C$ es el tipo de retorno, $x$ el valor devuelto en el caso base, $f$ la función del paso inductivo (que calcula el resultado para $S\ n$ a partir de $n$ y de la llamada recursiva) y $n$ el argumento sobre el cual se elimina.

Este recursor se generaliza a un principio de inducción completo, la eliminación dependiente. El eliminador unificado es una función cuyo tipo es el principio de inducción matemática:

\forall P : \texttt{nat} \to \text{Prop},\ (P\ 0) \to (\forall u{:}\,\texttt{nat},\ (P\ u) \to (P\ (S\ u))) \to \forall n{:}\,\texttt{nat},\ (P\ n)

Leído componente a componente: para cualquier propiedad $P$ sobre los naturales, si se proporciona una prueba del caso base $P\ 0$ y una prueba del paso inductivo (una función que, para cualquier $u$ , transforma una prueba de $P(u)$ en una de $P(S\ u)$ ), se obtiene una función que, para cualquier $n$ , construye una prueba de $P(n)$ . La inducción ya no es un principio inalcanzable sobre una codificación: es un principio de razonamiento generado automáticamente por la propia definición del tipo.

Nota 10.2 (Lo que un matemático ya conoce: teorema de recursión e inducción de Peano)

Vale la pena traducir el recursor a un lenguaje familiar, porque no introduce nada ajeno a la matemática ordinaria; solo lo vuelve primitivo. Las dos reglas de cómputo del recursor sobre $\mathbb{N}$ , a saber, $R(C,x,f,0) = x$ y $R(C,x,f,(S\,n)) = f\ n\ R(C,x,f,n)$ , son exactamente las ecuaciones del teorema de recursión: dado un valor inicial $x$ y una regla de paso $f$ , existe una única función con $g(0) = x$ y $g(n{+}1) = f(n, g(n))$ . Por ejemplo, el factorial es la instancia $R(\mathbb{N},\ 1,\ (\lambda\, n\, r.\ (S\,n)\cdot r),\ n)$ . Y el tipo de la versión dependiente, $\forall P,\ P\,0 \to (\forall u,\ P\,u \to P\,(S\,u)) \to \forall n,\ P\,n$ , es, leído palabra por palabra, el principio de inducción de Peano. La diferencia con la matemática usual no es de contenido sino de estatus: donde Peano postula la inducción como axioma y la codificación impredicativa ni siquiera permite demostrarla (solo proporciona la recursión; la inducción dependiente no es derivable en el CoC puro (Geuvers, 2001) ), el CIC la genera junto con el tipo. Definir un tipo inductivo equivale, pues, a obtener de una vez su definición por constructores, su teorema de recursión y su principio de inducción.

Las reglas generales de eliminación

La regla de eliminación es la pieza central que dota de poder computacional y lógico a las definiciones inductivas. Se introduce un pseudo-término $\text{Elim}(c, Q)\lbrace f_1 \mid \dots \mid f_n \rbrace$ que generaliza la recursión sobre los naturales a cualquier estructura inductiva. Se distinguen dos casos: eliminación no dependiente (para definir funciones) y dependiente (para pruebas por inducción).

Ejemplo 10.5 (El eliminador es la recursión de siempre (ℕ))

Antes de la regla general conviene fijar el caso de $\mathbb{N}$ , con constructores $\texttt{zero}$ y $\texttt{succ}$ . El eliminador no dependiente $\text{Elim}(n, Q)\lbrace f_0 \mid f_S \rbrace$ recibe un valor $f_0 : Q$ para el caso $\texttt{zero}$ y un manejador $f_S$ para $\texttt{succ}$ , y es la recursión primitiva:

\text{Elim}(\texttt{zero}, Q)\lbrace f_0 \mid f_S \rbrace = f_0, \qquad \text{Elim}(\texttt{succ}\ k, Q)\lbrace f_0 \mid f_S \rbrace = f_S\ k\ \big(\text{Elim}(k, Q)\lbrace f_0 \mid f_S \rbrace\big).

La notación $C_i\lbrace I, Q \rbrace$ que aparece en las reglas no es más que el tipo de cada manejador tras reemplazar la ocurrencia recursiva por un resultado de tipo $Q$ : para $\texttt{zero}$ es $C_{\texttt{zero}}\lbrace\mathbb{N}, Q\rbrace = Q$ ; para $\texttt{succ}$ es $C_{\texttt{succ}}\lbrace\mathbb{N}, Q\rbrace = \mathbb{N} \to Q \to Q$ (el predecesor y el resultado de la llamada recursiva). En la versión dependiente, donde $Q$ depende del valor, el caso $\texttt{succ}$ se vuelve $C_{\texttt{succ}}\lbrace\mathbb{N}, Q, \texttt{succ}\rbrace = (n{:}\,\mathbb{N}) \to Q\,n \to Q\,(\texttt{succ}\ n)$ , que es exactamente el paso inductivo de Peano. Las reglas generales que siguen solo expresan esto mismo para un tipo inductivo cualquiera.

Eliminación no dependiente. Se usa para definir funciones cuyo tipo de retorno no depende del valor de entrada. Sea $I := \text{Ind}(X{:}A)\lbrace C_1 \mid \dots \mid C_n \rbrace$ con $A \equiv (\vec{x}{:}\vec{A})\,s$ (el $\equiv$ denota aquí descomposición estructural: $A$ se analiza como una secuencia de productos que termina en la sort $s$ ). La regla de tipado es

\frac{\Gamma \vdash c : (I\ \vec{a}) \qquad \Gamma \vdash Q : (\vec{x}{:}\vec{A})\,s' \qquad \Gamma \vdash f_i : C_i\lbrace I, Q \rbrace\ \ (\forall i = 1,\dots,n)}{\Gamma \vdash \text{Elim}(c, Q)\lbrace f_1 \mid \ldots \mid f_n \rbrace : (Q\ \vec{a})} \quad (\text{Nodep}_{s,s'})

Aquí $Q$ es el tipo de retorno y cada $f_i$ maneja el caso del constructor $i$ -ésimo; $C_i\lbrace I, Q \rbrace$ es la transformación del tipo del constructor para incluir las llamadas recursivas, que ahora devuelven un resultado de tipo $Q$ .

Eliminación dependiente. Es la forma más general y corresponde al principio de inducción estructural: el tipo de retorno $Q$ puede depender no solo de los parámetros del tipo inductivo, sino también del valor inductivo mismo.

\frac{\Gamma \vdash c : (I\ \vec{a}) \qquad \Gamma \vdash Q : (\vec{x}{:}\vec{A})(I\ \vec{x}) \to s' \qquad \Gamma \vdash f_i : C_i\lbrace I, Q, \text{Constr}(i, I) \rbrace\ \ (\forall i = 1,\dots,n)}{\Gamma \vdash \text{Elim}(c, Q)\lbrace f_1 \mid \ldots \mid f_n \rbrace : (Q\ \vec{a}\ c)} \quad (\text{Dep}_{s,s'})

La notación $C_i\lbrace I, Q, \text{Constr}(i, I) \rbrace$ representa el tipo del caso $i$ -ésimo, donde las hipótesis inductivas tienen ahora el tipo dependiente $Q$ aplicado a los subtérminos recursivos.

Nota 10.6 (Restricciones sobre los pares (s, s'))

Las reglas anteriores no valen para pares $(s, s')$ arbitrarios. La eliminación fuerte (hacia $\text{Type}$ ) se restringe a tipos inductivos pequeños, y un inductivo que habita $\text{Prop}$ solo puede eliminarse hacia $\text{Prop}$ , salvo en los casos vacío y unitario (eliminación singleton). Sin estas restricciones el sistema sería inconsistente (eliminación fuerte sobre una sort impredicativa) y las pruebas en $\text{Prop}$ dejarían de ser borrables, contra la irrelevancia de pruebas que la página sobre universos explica en detalle (Paulin-Mohring, 1993) .

La reducción iota

El comportamiento computacional del eliminador se define mediante una nueva regla de reducción, la reducción- $\iota$ , que estipula cómo se reduce una aplicación de $\text{Elim}$ a un término construido con $\text{Constr}$ :

\text{Elim}((\text{Constr}(i, I)\ \vec{m}), Q)\lbrace \vec{f} \rbrace \longrightarrow_{\iota} \left( C_i\left[ I,\ \text{Fun\_Elim}(I, Q, \vec{f}),\ f_i \right]\ \vec{m} \right)

La expresión del lado derecho es compleja, pero su intuición es simple: se selecciona la función $f_i$ correspondiente al constructor $i$ y se le aplican los argumentos del constructor $\vec{m}$ ; la parte $C_i[\dots]$ se encarga de sustituir las llamadas recursivas por aplicaciones del propio término de eliminación, encapsulado en

\text{Fun\_Elim}(I, Q, \vec{f}) \equiv [\vec{x}{:}\vec{A}]\,[c{:}(I\ \vec{x})]\ \text{Elim}(c, Q)\lbrace \vec{f} \rbrace,

que actúa como el manejador de las llamadas recursivas dentro de la estructura del término. Para los naturales, esto instancia las conocidas reglas de reducción de la recursión:

\begin{aligned} \text{Elim}(\texttt{zero}, Q)\lbrace f_0 \mid f_S \rbrace &\longrightarrow_{\iota} f_0 \\ \text{Elim}((S\ n), Q)\lbrace f_0 \mid f_S \rbrace &\longrightarrow_{\iota} (f_S\ n\ \text{Elim}(n, Q)\lbrace f_0 \mid f_S \rbrace) \end{aligned}

En Lean, la igualdad por definición incluye la regla $\iota$ (un recursor aplicado a un constructor se reduce por definición) y todo inductive trae su recursor T.rec. De ahí que, para Nat.rec, las igualdades siguientes se cierren con rfl:

example (Q : Nat → Sort u) (z : Q 0)
  (s : (n : Nat) → Q n → Q (n+1)) :
  Nat.rec z s 0 = z := rfl

example (Q : Nat → Sort u) (z : Q 0)
  (s : (n : Nat) → Q n → Q (n+1)) (n : Nat) :
  Nat.rec z s (Nat.succ n) = s n (Nat.rec z s n) := rfl

La regla $\iota$ computa el recursor: en $0$ devuelve la base $z$ y en $S\,n$ aplica el paso $s$ al resultado recursivo; como ambas son reducciones por definición, se cierran con rfl.

Nota (A quién pertenecen las reglas iota)

Las reglas de $\iota$ -reducción se generan para el tipo inductivo: gobiernan a Nat.rec aplicado a constructores. Las ecuaciones de una definición recursiva como Nat.add (la suma, notación +, definida internamente mediante Nat.rec) no son reglas primitivas nuevas: el núcleo las valida desplegando la definición (reducción $\delta$ ) y aplicando $\beta$ e $\iota$ sobre Nat.rec. Así, que Nat.add m 0 sea definicionalmente igual a m es un teorema del cómputo $\delta + \beta + \iota$ , no un axioma adicional.

Nota 10.7 (Anatomía de un tipo inductivo)

Conviene reunir las piezas vistas, que son siempre las mismas cuatro y aparecen generadas por una sola declaración:

Formación (Ind): se declara el tipo enumerando sus constructores (por ejemplo, Nat con zero y succ).
Introducción (Constr): los constructores son las únicas maneras de construir un habitante del tipo.
Eliminación (Elim/recursor): la única manera de usar un habitante; en su forma no dependiente define funciones por recursión, y en la dependiente es el principio de inducción.
Cómputo ( $\iota$ -reducción): fija cómo se reduce el eliminador frente a cada constructor, haciendo el cálculo efectivo y la verificación de tipos decidible.

Todo tipo inductivo de Lean (incluidas la sintaxis de fórmulas y la relación de derivabilidad del módulo 07) se entiende con este mismo molde.