Preámbulo · Lean desde cero

Tipos que se construyen

¿De dónde salen Nat y Bool? No son primitivos misteriosos del sistema: están declarados en la biblioteca de Lean, con la misma orden que cualquier usuario puede usar. La orden se llama inductive, y su filosofía cabe en una frase: un tipo es su lista de maneras de construir elementos. El caso más pequeño posible:

inductive Bool where
  | true
  | false

Esto declara un tipo nuevo, Bool, y afirma tres cosas a la vez: true es un Bool, false es un Bool, y no hay más elementos que esos. La cláusula de cierre (nada es un Bool salvo lo construido por la lista) no se escribe: es parte del significado de inductive. Cada línea con | es un constructor, y el tipo queda completamente determinado por sus constructores.

Peano en tres líneas

El mismo mecanismo, con un giro, produce los naturales:

inductive Nat where
  | zero
  | succ (n : Nat)

Léase junto a los axiomas de Peano que todo matemático conoce: « $0$ es un natural; el sucesor de un natural es un natural; nada más lo es». Las tres cláusulas son, línea por línea, la declaración: zero es el cero, succ toma un Nat ya construido y produce otro (el constructor puede mencionar al propio tipo que se está definiendo, de ahí el nombre tipo inductivo ), y la cláusula de exclusión viene gratis. El 3 de las páginas anteriores es, por dentro, succ (succ (succ zero)): los numerales son abreviaturas.

Que un sistema de axiomas se convierta en una declaración de datos no es un truco de notación. Es el corazón del diseño de Lean: los objetos matemáticos básicos se construyen, no se postulan, y de la construcción Lean extrae automáticamente el principio de inducción correspondiente. La ruta teórica desarrolla esto con rigor; aquí basta ver el patrón.

Desarmar lo construido: match

Si todo Nat viene de zero o de succ, entonces para definir una función sobre Nat basta decir qué hacer en cada caso. La orden es match:

def doble (n : Nat) : Nat :=
  match n with
  | Nat.zero => Nat.zero
  | Nat.succ k => Nat.succ (Nat.succ (doble k))

El match distingue por constructor: si n es zero, el doble es zero; si n es succ k (el sucesor de algún k), el doble es el doble de k más dos sucesores. La definición se llama a sí misma sobre k: es una definición recursiva, la contraparte computacional de la inducción.

Nota (La recursión tiene que terminar)

Aquí hay que ser honestos: no toda «definición» recursiva define algo. Una función que se llama a sí misma sobre el mismo argumento no termina nunca y no define función alguna. Lean verifica la terminación: acepta doble porque la llamada recursiva es sobre k, estrictamente más pequeño que succ k, y rechaza las recursiones que no puede ver decrecer. Esta vigilancia no es pedantería: si Lean aceptara definiciones que no terminan, podría «demostrarse» cualquier cosa, y el asistente perdería todo su valor. En la tesis, el capítulo de completitud depende de una recursión cuya terminación es un teorema en sí mismo.

El anticipo: las fórmulas de la tesis

Todo este preámbulo apunta a un objetivo concreto, y aquí aparece por primera vez. La tesis formaliza la lógica proposicional, y su primer archivo declara qué es una fórmula:

inductive Formula where
  | atom (n : Nat)
  | neg (φ : Formula)
  | impl (φ ψ : Formula)

Léase con los ojos ya entrenados: una fórmula es una variable atómica $p_n$ (numerada por un Nat), o la negación $\neg \varphi$ de una fórmula ya construida, o la implicación $\varphi \to \psi$ de dos de ellas. Y nada más lo es. La definición «el conjunto de fórmulas es el menor conjunto tal que…», que en un libro de lógica ocupa un párrafo cuidadoso, es una declaración de datos de cuatro líneas, del mismo género que Nat. Las fórmulas de la lógica son un tipo de datos como los naturales, y las funciones sobre fórmulas (evaluar, sustituir, medir) se definirán con match, como doble. Este es, literalmente, el archivo Syntax.lean de la tesis.

Nota (Sin laboratorio en esta página)

El laboratorio del preámbulo no admite tipos declarados por el usuario, así que esta página es de lectura. Todo el código mostrado es Lean 4 legítimo y puede pegarse tal cual en una instalación real o en live.lean-lang.org.

Lo que ya sabes

inductive declara un tipo dando su lista de constructores; el tipo es esa lista, y nada fuera de ella habita el tipo.
Los axiomas de Peano son la declaración de Nat: zero y succ, con la exclusión incluida de fábrica.
match define funciones por casos sobre los constructores; la recursión está permitida y Lean verifica que termina.
Las fórmulas de la lógica proposicional son un tipo inductivo de tres constructores: el primer archivo de la tesis.

Los tipos vistos hasta ahora clasifican datos: números, valores de verdad, funciones, fórmulas. La página siguiente presenta el giro que hace de Lean un asistente de pruebas y no solo un lenguaje: tipos que clasifican afirmaciones.