Programar un mini-Lean en el sistema de tipos de Julia

Traducción automática del original en inglés, todavía sin revisar. Leer el original.

Este artículo está basado en la charla de Guillermo Angeris “Programming a (mini-)Lean in Julia’s type system”.

Un demostrador de teoremas (theorem prover), reducido a su motor, es un kernel de confianza chiquito, un type checker y una frontera entre los dos.

Guillermo Angeris responde a esto programando en vivo, dentro de Julia, un kernel de juguete para demostrar teoremas que ilustra cómo funciona Lean en términos de arquitectura. El resultado es un kernel chiquito que hace visible la frontera de confianza: si aceptás el kernel, entonces todo lo que se construya encima tiene que pasar por el type checker.

Este es el tercer artículo de la serie Demostración de teoremas. El primer artículo cubre la correspondencia de Curry-Howard. El segundo implementa un demostrador chiquito de forma explícita en Python. Este artículo mete esas mismas ideas dentro del sistema de tipos de un lenguaje anfitrión.

#La arquitectura

Podrías construir un demostrador de teoremas tratando las demostraciones como strings e implementando reglas de reescritura de símbolos encima. Funciona, pero pelea contra el lenguaje anfitrión. Curry-Howard ofrece un camino mejor para los lenguajes de programación: convertir las proposiciones en tipos, las demostraciones en valores, y dejar que el type checker haga cumplir las reglas.

Todo demostrador de teoremas real tiene la misma estructura básica:

1. Un kernel de confianza chiquito que define las reglas del juego
2. Código de demostración del usuario que se construye sobre esas reglas
3. Un type checker que hace cumplir la frontera

El kernel es el único código en el que tenés que confiar. Todo lo que está afuera, cada demostración, cada teorema, solo puede combinar resultados que produjo el kernel. Si el kernel es correcto, entonces cualquier demostración que pase el chequeo de tipos es correcta, sin importar lo compleja que sea.

A esto a veces se lo llama el criterio de de Bruijn: hacer el kernel lo bastante chico como para que una persona pueda leer cada línea, convencerse de que es correcto y después confiar en todo lo que el sistema deriva. El kernel de Lean tiene unos pocos miles de líneas de C++. El del mini-Lean tiene 61 líneas de Julia.

#Construir el kernel: aritmética de Peano en el sistema de tipos de Julia

Angeris codifica la aritmética de Peano enteramente dentro del sistema de tipos de Julia. La aritmética de Peano es una forma formal de definir los números naturales (0, 1, 2, 3, …) desde cero usando dos reglas simples.

#Números naturales como tipos

Los números naturales se definen con apenas dos reglas:

1. Cero existe y es un número natural.
2. Sucesor: para cualquier número natural n, existe S(n), que también es un número natural.

Esto te da: 0 = Zero, 1 = Succ{Zero}, 2 = Succ{Succ{Zero}}, 3 = Succ{Succ{Succ{Zero}}}, y así sucesivamente. Todo número natural es cero o el sucesor de algún otro número natural. No hay tercera opción.

En Julia, esto se convierte en un tipo abstracto Nat con dos subtipos: Zero <: Nat (un tipo sin datos, que solo representa el concepto de cero) y Succ{N} <: Nat donde N tiene que ser a su vez un Nat. Así que Succ{Zero} es 1, Succ{Succ{Zero}} es 2, y así.

Estos existen puramente a nivel de tipos. Julia nunca crea valores en tiempo de ejecución para ellos. El type checker hace todo el trabajo durante la compilación.

#La igualdad como tipo

La igualdad entre dos números a nivel de tipos es un tipo llamado Eq{A, B}. Los dos parámetros de tipo son los dos lados de la ecuación. Entonces la proposición “1 + 1 = 2” es el tipo Eq{Add{Succ{Zero}, Succ{Zero}}, Succ{Succ{Zero}}}. Parece ruidoso, pero lo único que dice es “la suma de 1 y 1 es igual a 2”.

Acá está el truco crucial: el constructor de Eq no se exporta a los usuarios. Podés escribir el tipo Eq{A, B} (podés enunciar una proposición), pero no podés crear un valor de ese tipo directamente (no podés fabricar una demostración). La única forma de obtener un valor Eq es a través de las funciones de axioma que provee el kernel.

#La suma a nivel de tipos

La suma se define de forma recursiva, de la misma manera en que le enseñarías a un chico a sumar contando para arriba:

• Add{Zero, N} se reduce a N. Sumarle cero a cualquier cosa te devuelve esa misma cosa. (0 + 5 = 5.)
• Add{Succ{M}, N} se reduce a Succ{Add{M, N}}. Para sumar un número distinto de cero, le sacás uno, sumás lo que queda y después volvés a poner el uno arriba. (3 + 5 = 1 + (2 + 5) = 1 + (1 + (1 + 5)) = 8.)

Julia usa multiple dispatch para elegir la regla correcta según los tipos. El sistema de tipos evalúa estas reducciones durante la compilación. Para cuando tu código corre (si hay algo para correr), los tipos ya se calcularon por completo.

#Los seis axiomas

El kernel exporta exactamente seis funciones de axioma. Son las únicas formas legítimas de construir demostraciones de igualdad:

1. Reflexividad. Para cualquier n, podés construir Eq{n, n}. Cualquier cosa es igual a sí misma. Este es el punto de partida, la demostración más simple que existe.

2. Simetría. Dado Eq{a, b}, produce Eq{b, a}. La igualdad es una calle de doble mano.

3. Transitividad. Dados Eq{a, b} y Eq{b, c}, produce Eq{a, c}. Este es el axioma de encadenamiento crítico. La mayoría de las demostraciones son secuencias de igualdades conectadas por transitividad: “A = B, y B = C, y C = D, por lo tanto A = D.”

4. Congruencia del sucesor. Dado Eq{a, b}, produce Eq{Succ{a}, Succ{b}}. Aplicar la misma operación a los dos lados de una igualdad preserva la igualdad. Esto te permite “levantar” una demostración a través de una capa de sucesor.

5. Caso base de la suma: Zero + n = n. Produce Eq{Add{Zero, N}, N}. Esto codifica directamente la primera cláusula de la definición recursiva de la suma.

6. Caso recursivo de la suma: Succ(m) + n = Succ(m + n). Produce Eq{Add{Succ{M}, N}, Succ{Add{M, N}}}. Esto codifica la segunda cláusula.

Esa es toda la base. Seis funciones más las definiciones de tipo de Nat, Zero, Succ, Eq y Add. Unas 61 líneas de Julia contando los espacios en blanco.

Estas seis funciones de axioma son el único código autorizado a crear valores Eq desde cero. Todo lo que está afuera del kernel solo puede combinar valores Eq que produjeron los axiomas. La frontera de confianza de la sección anterior ahora es concreta: las 61 líneas del kernel son el único código que tenés que auditar.

#Demostrar 1 + 1 = 2

Con el kernel en su lugar, el primer objetivo es demostrar que 1 + 1 = 2. Formalmente, esto significa construir un valor cuyo tipo sea:

Eq{Add{Succ{Zero}, Succ{Zero}}, Succ{Succ{Zero}}}

La demostración es una cadena de aplicaciones de axiomas:

Paso 1. Aplicar la regla de suma 2 (el caso recursivo). Succ{Zero} + Succ{Zero} se reduce a Succ{Zero + Succ{Zero}}. Esto nos da un Eq entre Add{Succ{Zero}, Succ{Zero}} y Succ{Add{Zero, Succ{Zero}}}. Le sacamos una capa de sucesor al operando izquierdo.

Paso 2. Aplicar la regla de suma 1 (el caso base) al término interno. Zero + Succ{Zero} se reduce a Succ{Zero}. Esto nos da Eq{Add{Zero, Succ{Zero}}, Succ{Zero}}.

Paso 3. Aplicar congruencia del sucesor al paso 2. Como Zero + Succ{Zero} = Succ{Zero}, envolver los dos lados en Succ nos da Succ{Zero + Succ{Zero}} = Succ{Succ{Zero}}.

Paso 4. Aplicar transitividad para conectar los pasos 1 y 3. El paso 1 dice Succ{Zero} + Succ{Zero} = Succ{Zero + Succ{Zero}}. El paso 3 dice Succ{Zero + Succ{Zero}} = Succ{Succ{Zero}}. La transitividad los encadena: Succ{Zero} + Succ{Zero} = Succ{Succ{Zero}}. Eso es 1 + 1 = 2.

El valor final tiene exactamente el tipo objetivo. El type checker de Julia verifica cada paso intermedio. Si le pasás el Eq equivocado a la transitividad, o si los tipos de dos igualdades encadenadas no comparten un término del medio en común, la compilación falla.

La demostración es verbosa y mecánica. Ese es el punto. Cada paso se puede verificar de forma independiente, y el compilador es el árbitro.

Toda la derivación ocurre durante la compilación, a nivel de tipos. La demostración existe puramente como una cadena de valores Eq cuyos tipos se restringen entre sí hasta formar una derivación válida. Si le errás a cualquier eslabón de la cadena, el código no compila. El sistema de tipos atrapa el error antes de que corra nada, de la misma forma en que te atraparía si quisieras sumarle un string a un entero.

#Cuantificación universal: para todo n, n + 1 = Succ(n)

Demostrar algo sobre todos los números naturales requiere otra herramienta: un tipo función.

El enunciado “para todo n, n + 1 = Succ(n)” significa: no importa qué número elijas, sumarle 1 te da el número siguiente. Bajo Curry-Howard, esto se convierte en un tipo función: dado cualquier tipo de número natural N, devolver un valor de tipo Eq{Add{N, Succ{Zero}}, Succ{N}}.

Una demostración específica como “1 + 1 = 2” es como probar un input. Una demostración universal como “para todo n, n + 1 = Succ(n)” es como escribir una función que pasa para todos los inputs. No estás testeando, estás demostrando.

La demostración es una función que toma un parámetro de tipo abstracto N <: Nat, no un número específico sino un lugar para cualquier número. Dentro del cuerpo, Angeris encadena los mismos axiomas que antes, pero ahora operan sobre el N genérico en vez de sobre un Succ{Zero} concreto.

La idea clave: la función de demostración funciona por recursión estructural sobre N. Para Zero, aplicás el caso base de la suma. Para Succ{M}, usás la regla recursiva de la suma, aplicás la demostración recursivamente para M y después usás congruencia y transitividad para armar el resultado.

El hecho de que esta función compile es la demostración. El type checker de Julia verificó que para cualquier N posible, el tipo de retorno es Eq{Add{N, Succ{Zero}}, Succ{N}}. Podés instanciarla: llamar a la función con Succ{Zero} (el número 1) recupera el hecho específico de que 1 + 1 = 2. Llamarla con Succ{Succ{Zero}} te da 2 + 1 = 3. Pero la función en sí, la versión genérica, demuestra el enunciado universal.

El “para todo” no necesita maquinaria especial. Es simplemente una función genérica, el mismo concepto que ya usás cuando escribís código que funciona sobre “cualquier lista” o “cualquier tipo comparable”.

#Un pequeño bonus propio de Julia

Angeris también muestra un truco extra propio de Julia: el retículo de subtipos termina reflejando parte de la relación entre demostraciones genéricas y específicas. Igual, lo importante sigue siendo el kernel, los términos de demostración y la frontera del type checker.

#Demostrar la negación: cero no es igual a uno

Hasta ahora, cada demostración fue sobre mostrar que dos cosas son iguales. Pero la matemática también necesita la negación, la capacidad de demostrar que algo es falso. ¿Cómo representás “0 ≠ 1” como tipo?

#Lo falso como tipo inhabitable

El truco es elegante. Definí un tipo llamado FalseProp que no tiene constructor público. Es un tipo que nunca puede tener un valor. Podés escribir el tipo (podés enunciar “Falso”), pero nunca podés crear un valor de él (nunca podés demostrar Falso).

Después definí “no P” como “una función de P a FalseProp”. En otras palabras: si suponer P te permite producir un valor de FalseProp, algo salió mal, porque los valores de FalseProp no pueden existir. Entonces P tiene que ser falso.

Así funciona la matemática constructiva: “no P” significa “P lleva a una contradicción”.

Julia no tiene control de acceso de verdad, así que esto es una convención. Los usuarios técnicamente podrían llamar al constructor interno y hacer trampa. (Más sobre esto en la sección de limitaciones.) Pero la versión disciplinada es: el kernel nunca exporta el constructor de FalseProp, así que las demostraciones legítimas nunca pueden producir uno.

#El último axioma de Peano

El último axioma de Peano codifica un hecho básico sobre los números naturales: ningún sucesor es cero. 1 no es 0. 2 no es 0. 47 no es 0. Siempre podés contar para adelante, pero nunca das la vuelta hasta cero.

En el kernel, este axioma es una función con tipo Eq{Succ{N}, Zero} → FalseProp para cualquier N. Dice: dame una demostración de que algún sucesor es igual a cero, y te doy una demostración de Falso. Como los valores de FalseProp nunca se pueden crear legítimamente, esto significa que tampoco puede existir ninguna demostración legítima de Succ(n) = 0. La función de axioma tiene permitido usar el constructor interno de FalseProp porque es parte del kernel de confianza.

#Demostrar 0 ≠ 1

Para demostrar que Succ{Zero} ≠ Zero, es decir 1 ≠ 0, escribís una función de tipo Eq{Succ{Zero}, Zero} → FalseProp:

1. Suponé una “mala suposición”, una demostración hipotética de que Succ{Zero} = Zero.
2. Pasale esta suposición al axioma de Peano succ_ne_zero.
3. El axioma devuelve FalseProp.

La función compila y pasa el chequeo de tipos. Su firma de tipo es el enunciado “1 = 0 implica Falso”, que es el enunciado “1 ≠ 0”. Demostración completa.

Esto es demostración por contradicción, una de las técnicas más viejas de la matemática, codificada como una función. Suponés algo (1 = 0), mostrás que lleva a algún lugar imposible (FalseProp) y concluís que la suposición estaba mal. “Imposible” es un tipo sin valores. “Lleva a lo imposible” es una función que devuelve ese tipo.

Un sistema completo también necesitaría el principio de explosión: “de lo falso se sigue cualquier cosa”. Si de alguna forma tuvieras un valor de FalseProp, podrías producir un valor de cualquier tipo. Suena absurdo, pero es seguro porque los valores de FalseProp nunca pueden existir en primer lugar.

#Inducción: la recursión como demostración

La inducción matemática es la forma de demostrar cosas sobre todos los números naturales. La idea: si algo es verdadero para 0, y que sea verdadero para cualquier número implica que también es verdadero para el siguiente, entonces es verdadero para todos los números.

Bajo Curry-Howard, la inducción no necesita ser una regla aparte. Es programación recursiva. Una demostración por inducción es una función recursiva que:

1. Caso base: dado Zero, devuelve una demostración de P(Zero).
2. Paso inductivo: dado Succ{N} y una demostración de P(N) (obtenida por recursión), construye una demostración de P(Succ{N}).

Si esta función compila, la inducción es válida. El compilador verifica que cada caso esté cubierto y que cada tipo de retorno coincida con el objetivo.

La demostración universal de “para todo n, n + 1 = Succ(n)” ya usa este patrón. Hace recursión sobre la estructura de N: resuelve el caso cero, y después resuelve el caso sucesor llamándose a sí misma sobre un número más chico. La inducción es simplemente cómo se ve la recursión cuando tus tipos de retorno llevan contenido lógico.

Angeris empieza a programar un combinador induction independiente pero se queda corto de tiempo. La idea es una función de orden superior (una función que toma otras funciones como argumentos) que acepta una demostración del caso base y una función de paso, y después las compone recursivamente.

Acá es donde Julia empieza a crujir. En Lean, los tipos de retorno de una función pueden depender de los valores de los argumentos. Eso es lo que significa “tipos dependientes”: el tipo de la salida cambia según la entrada. En Julia, podés simular esto con tipos paramétricos y multiple dispatch, pero es indirecto. El sistema de tipos es lo bastante poderoso como para codificar las demostraciones, pero la ergonomía no está pensada para eso.

#Dónde se queda corto Julia

El mini-Lean funciona, pero Julia no fue diseñado para esto, y se nota.

#Sin constructores privados

Julia no tiene campos ni constructores privados. Todo es accesible por nombre. Angeris muestra el problema en vivo escribiendo directamente Eq{Succ{Zero}, Zero}(), fabricando una demostración de que 1 = 0 sin pasar por ningún axioma.

Una vez que tenés un enunciado falso, podés derivar cualquier cosa. (Es el principio de explosión de antes, solo que ahora juega en tu contra.) Todo el sistema se derrumba si los usuarios hacen trampa. En Lean, el kernel es una frontera de confianza dura con constructores genuinamente privados, así que esto no puede pasar. En Julia, es un sistema basado en la palabra de honor.

#Sin tácticas, solo demostraciones a mano

Lean tiene un lenguaje de tácticas (tactics) que automatiza los pasos de demostración rutinarios. ring resuelve igualdades de anillos, simp simplifica expresiones, omega se encarga de la aritmética lineal. Cuando necesitás demostrar 2 + 2 = 4 en Lean, es una línea.

En el mini-Lean, cada demostración se arma a mano, axioma por axioma. Extender la demostración de 1+1=2 a 2+1=3 implica más desenrollado, más congruencias, más transitividades. Angeris se choca con errores de tipos en vivo y pasa minutos debuggeando, murmurando “I have no idea what the hell is wrong here”. Lo hace andar sin entender del todo qué cambió, se encoge de hombros y sigue.

Esta es la mejor demostración de lo que te compra la automatización con tácticas. En Lean, escribirías by omega y la demostración estaría lista. El sistema de tácticas sabe resolver igualdades aritméticas automáticamente. Puede verificar 100 + 100 = 200 con la misma facilidad que 1 + 1 = 2, porque tiene algoritmos en vez de desenrollado manual. Lean también tiene simp (simplificar usando hechos conocidos), norm_num (cómputo numérico verificado) y la posibilidad de escribir tácticas propias.

La distancia entre el mini-Lean y el Lean de producción está casi toda en la automatización, no en las ideas de base. El motor es el mismo. Lean simplemente tiene dirección asistida.

#Los mensajes de error de tipos no ayudan

Cuando un paso de demostración falla en Lean, ves tu estado de demostración: qué estás intentando demostrar, qué ya sabés y dónde se rompieron las cosas. En Julia, te sale un error genérico de tipos que no coinciden, sin contexto. Debuggear implica desparramar llamadas a typeof() por todos lados y quedarse mirando valores intermedios. Es debuggear con printf, pero para tipos.

#Rendimiento: el truco de @generated

Una nota práctica: por defecto, Julia recalcula las operaciones a nivel de tipos en cada llamada. Para demostraciones con tipos muy anidados (imaginate demostrar algo sobre el número 100, que es Succ envuelto 100 veces), esto se vuelve lento. Las funciones @generated de Julia pueden cachear los cálculos a nivel de tipos para que la verificación de la demostración ocurra una sola vez por cada conjunto único de parámetros de tipo.

#Qué agregan los demostradores de producción

Este ejercicio muestra qué son los demostradores de teoremas a nivel del kernel, y qué te compran las capas de arriba.

#El kernel es el mismo

Lean, en su núcleo, funciona exactamente como este mini-Lean. Kernel de confianza chiquito, código de demostración no confiable encima, type checker haciendo cumplir la frontera. La diferencia es de escala y alcance: el kernel de Lean maneja tipos dependientes, polimorfismo de universos y tipos inductivos. El mini-Lean maneja aritmética de Peano. Pero la arquitectura es la misma.

Toda la enorme biblioteca matemática verificada de Lean se reduce a chequeos contra un kernel de unos pocos miles de líneas de C++.

#Qué agrega Lean encima

Capa	Mini-Lean	Lean
Kernel	61 líneas, aritmética de Peano	~4.000 líneas de C++, teoría de tipos dependientes
Frontera de confianza	Convención (palabra de honor)	Garantizada (constructores privados)
Estilo de demostración	Encadenamiento manual de axiomas	Tácticas (simp, omega, ring, rw)
Automatización	Ninguna	Procedimientos de decisión, simplificador, tácticas propias
Mensajes de error	Tipos que no coinciden, genérico	Estado de demostración: objetivos, hipótesis, contexto
Expresividad	Números naturales, igualdad	Matemática arbitraria
Biblioteca	Ninguna	mathlib (gran biblioteca estándar)
Herramientas	REPL de Julia	VS Code, LSP, widgets, documentación

La capa de automatización es la diferencia más grande. Las tácticas te permiten trabajar al nivel del razonamiento matemático en vez de encadenar axiomas mecánicamente. by omega reemplaza veinte líneas de desenrollado manual. simp [lemma1, lemma2] reemplaza largas cadenas de reescrituras. Las tácticas propias les permiten a los autores de bibliotecas empaquetar estrategias de demostración para que los usuarios no tengan que reinventarlas.

#La torre de universos

Angeris deja entrever posibilidades más profundas. Julia tiene un tipo Type, el tipo de los tipos. Y Type a su vez tiene un tipo (Type{Type}), y así sucesivamente. Esto crea una jerarquía que los teóricos de tipos llaman torre de universos, donde cada nivel puede hablar de cosas del nivel de abajo.

¿Por qué importa? Sin ella, podés crear paradojas. Si permitís un “conjunto de todos los conjuntos”, aparece la paradoja de Russell: ¿el conjunto de todos los conjuntos que no se contienen a sí mismos se contiene a sí mismo? (Si se contiene, no se contiene. Si no se contiene, se contiene.) La torre de universos lo evita diciendo: los tipos del nivel 1 solo pueden hablar de tipos del nivel 0, los tipos del nivel 2 solo pueden hablar de tipos del nivel 1, y así. Ningún nivel puede hablar de sí mismo.

En Lean, esta jerarquía está diseñada con cuidado. Prop (las proposiciones) vive en un nivel. Type (los tipos de datos) vive en otro. Type 1 (el universo que contiene a Type) vive arriba de ese. Julia tiene indicios de la misma estructura, podés escribir Type{Type} y es una expresión válida, pero es más un accidente de la implementación que un marco lógico deliberado.

#Algunos sistemas de tipos anfitriones también pueden hacer esto

Esto funciona en Julia porque su sistema de tipos es inusualmente rico en los aspectos justos: tipos paramétricos, supertipos abstractos y multiple dispatch capaz de impulsar la reducción a nivel de tipos. Algunos otros lenguajes también pueden alojar fragmentos de la misma idea. Haskell con GADTs puede acercarse. TypeScript puede codificar partes sorprendentes. Pero no es algo que obtenés automáticamente por “tener generics”.

La lección es específica: una vez que un sistema de tipos anfitrión es lo bastante expresivo, podés empezar a meterle razonamiento lógico de contrabando. Julia resulta ser apenas lo bastante fuerte como para hacer visible la arquitectura.

#Conclusión

Desde cero, sin macros ni dependencias, Angeris arma un demostrador de teoremas que funciona en 61 líneas de Julia. El kernel define los números naturales, la igualdad, la suma y seis axiomas. Solo a partir de estas primitivas, demuestra 1+1=2, demuestra n+1=Succ(n) para todo n, y demuestra 0≠1.

La construcción hace visible lo que normalmente queda oculto: los demostradores de teoremas no son magia. Son un kernel de confianza chiquito, un type checker y una frontera nítida entre los dos. Todo lo demás, las tácticas, las bibliotecas, las herramientas, es ingeniería construida sobre esa base.

El próximo artículo de esta serie pone ese motor a trabajar: escribir demostraciones reales en Lean, con toda la automatización que le falta al mini-Lean.