Construyendo un pequeño demostrador de teoremas en Python

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

El primer artículo de esta serie explicó la correspondencia de Curry-Howard: las proposiciones son tipos, las demostraciones son programas. Eso te dice por qué la demostración de teoremas encaja tan naturalmente con los lenguajes de programación. Todavía no te dice cómo es la máquina.

Un demostrador de teoremas (theorem prover), en concreto, es más chico de lo que la mayoría espera. Un pequeño demostrador de teoremas es apenas:

1. un lenguaje para términos
2. un lenguaje para tipos / proposiciones
3. un checker que decide si un término tiene un tipo
4. un kernel de confianza, chiquito, que define las jugadas legales

Este artículo construye esa arquitectura en Python puro. No estamos abusando del propio sistema de tipos de Python. Python es solo el lenguaje de implementación. El demostrador que construimos tiene sus propios términos, sus propias proposiciones y su propio checker.

Esa distinción importa. El objetivo acá no es lucirse con trucos del lenguaje anfitrión. Quiero que las piezas móviles sean imposibles de pasar por alto.

#El núcleo útil más chico

Si reducís la demostración de teoremas al hueso, no necesitás aritmética, tácticas, automatización, ni siquiera un parser. Necesitás un puñado de formas de términos y un puñado de reglas de tipado.

Para un primer demostrador, el objetivo correcto es:

• implicación
• variables
• abstracción de funciones
• aplicación de funciones
• supuestos con nombre en un contexto

Esto alcanza para representar el cálculo lambda simplemente tipado, que bajo Curry-Howard corresponde a la lógica proposicional intuicionista.

Eso significa que ya podemos representar y verificar demostraciones de enunciados como:

• A -> A
• A -> B -> A
• (A -> B) -> (B -> C) -> A -> C

No son ejemplos de juguete de programación. Son teoremas lógicos.

#Términos, proposiciones y contextos

Necesitamos tres tipos de datos:

• Tipos: proposiciones como A, B o A -> B
• Términos: demostraciones/programas como variables, lambdas y aplicaciones
• Contextos: los supuestos que están en alcance en este momento

En Python:

from dataclasses import dataclass


class Type:
    pass


@dataclass(frozen=True)
class Atom(Type):
    name: str


@dataclass(frozen=True)
class Arrow(Type):
    left: Type
    right: Type


class Term:
    pass


@dataclass(frozen=True)
class Var(Term):
    name: str


@dataclass(frozen=True)
class Lam(Term):
    param: str
    param_type: Type
    body: Term


@dataclass(frozen=True)
class App(Term):
    fn: Term
    arg: Term

El contexto es simplemente un mapeo de nombres de variables a tipos:

Context = dict[str, Type]

Ese mapeo es todo el lenguaje de demostraciones.

¿Por qué estos constructores?

• Var(x) significa “usá el supuesto llamado x”
• Lam(x, A, body) significa “suponé x : A, y después demostrá body”
• App(f, a) significa “aplicá una demostración de A -> B a una demostración de A para obtener una demostración de B”

Así es exactamente como funciona la implicación en deducción natural.

#El checker es el kernel

Ahora escribimos lo único que realmente importa: el checker.

def infer(ctx: Context, term: Term) -> Type:
    if isinstance(term, Var):
        if term.name not in ctx:
            raise TypeError(f"unbound variable: {term.name}")
        return ctx[term.name]

    if isinstance(term, Lam):
        new_ctx = dict(ctx)
        new_ctx[term.param] = term.param_type
        body_type = infer(new_ctx, term.body)
        return Arrow(term.param_type, body_type)

    if isinstance(term, App):
        fn_type = infer(ctx, term.fn)
        arg_type = infer(ctx, term.arg)

        if not isinstance(fn_type, Arrow):
            raise TypeError(f"attempted to apply non-function: {fn_type}")

        if fn_type.left != arg_type:
            raise TypeError(
                f"function expected {fn_type.left}, got {arg_type}"
            )

        return fn_type.right

    raise TypeError(f"unknown term: {term}")

Este es el kernel de confianza.

Si infer es correcta, entonces cualquier término que acepte es una demostración válida del tipo que devuelve. Si infer está mal, el sistema es inconsistente (unsound). Los demostradores de teoremas apuntan a kernels chiquitos porque cada línea de esta función es código en el que tenés que confiar.

#Qué significan las reglas en términos lógicos

Cada rama de infer es una regla de demostración.

#Variables

infer(ctx, Var("x")) == ctx["x"]

En términos lógicos, esto significa:

• si x : A está entre tus supuestos
• entonces podés concluir A

Esa es la regla del supuesto.

#Lambdas

infer(ctx, Lam("x", A, body)) == Arrow(A, body_type)

En términos lógicos:

• suponé A
• bajo ese supuesto, derivá B
• por lo tanto, derivá A -> B

Esa es la introducción de la implicación.

#Aplicaciones

infer(ctx, App(f, a))

En términos lógicos:

• si f demuestra A -> B
• y a demuestra A
• entonces f(a) demuestra B

Esa es la eliminación de la implicación, más conocida como modus ponens.

El checker aplica las reglas de inferencia lógica directamente.

#Primera demostración: A -> A

La función identidad es la demostración más simple del sistema:

A = Atom("A")

identity = Lam("x", A, Var("x"))
print(infer({}, identity))

El tipo inferido es:

Arrow(Atom("A"), Atom("A"))

Bajo Curry-Howard, eso significa que el término demuestra A -> A.

fun x => x es a la vez:

• un programa que devuelve su entrada
• una demostración de que si vale A, entonces vale A

El mismo término habita las dos interpretaciones.

#Una demostración un poco menos trivial: A -> B -> A

Ahora demostremos que si vale A y vale B, entonces vale A.

A = Atom("A")
B = Atom("B")

proof = Lam("x", A, Lam("y", B, Var("x")))
print(infer({}, proof))

El tipo inferido es:

Arrow(A, Arrow(B, A))

En términos lógicos, eso es:

A -> B -> A

La demostración es simplemente “ignorá el segundo supuesto y devolvé el primero”.

La programación funcional común y la demostración formal son la misma estructura vista de dos maneras.

#Composición: (A -> B) -> (B -> C) -> A -> C

Ahora algo que se siente como razonamiento de verdad:

A = Atom("A")
B = Atom("B")
C = Atom("C")

compose = Lam(
    "f", Arrow(A, B),
    Lam(
        "g", Arrow(B, C),
        Lam(
            "x", A,
            App(Var("g"), App(Var("f"), Var("x")))
        )
    )
)

print(infer({}, compose))

El checker devuelve:

Arrow(Arrow(A, B), Arrow(Arrow(B, C), Arrow(A, C)))

Esto es demostración como composición de evidencia:

• f convierte evidencia de A en evidencia de B
• g convierte evidencia de B en evidencia de C
• así que juntas convierten evidencia de A en evidencia de C

En lógica, eso es un teorema. En programación, es composición de funciones.

El mismo término admite las dos lecturas.

#Lo que este pequeño demostrador todavía no puede hacer

A esta altura tenemos un demostrador real, pero extremadamente chico.

Todavía no puede expresar:

• conjunción (A and B)
• disyunción (A or B)
• cuantificadores sobre valores
• igualdad
• números naturales
• inducción
• cómputo dentro de los tipos

Está bien así. La primera implementación existe para que la arquitectura del kernel se pueda leer.

Incluso en esta forma chiquita, ya podés ver el patrón completo:

• los términos son demostraciones
• los tipos son proposiciones
• chequear es verificar demostraciones

Todo lo más avanzado es una extensión de esa base.

#La siguiente extensión útil: pares

Si quisieras hacer crecer este demostrador un paso, la mejor jugada siguiente sería la conjunción.

Agregá:

• un PairType(A, B)
• un PairTerm(a, b)
• proyecciones Fst y Snd

Entonces el checker suma tres reglas más:

• si a : A y b : B, entonces (a, b) : A and B
• si p : A and B, entonces fst(p) : A
• si p : A and B, entonces snd(p) : B

Eso te permitiría demostrar enunciados como:

• A -> B -> (A and B)
• (A and B) -> A
• (A and B) -> B

La arquitectura no cambiaría. Solo agregarías más formas de términos y más reglas.

Ese es el tema recurrente en los demostradores de teoremas: reglas chicas y explícitas se componen en sistemas poderosos.

#Lo que Lean agrega más allá de esto

El checker de juguete de acá y Lean son el mismo tipo de máquina, pero Lean agrega varias capas que extrañás apenas intentás demostrar algo no trivial:

• Tipos dependientes: los tipos pueden mencionar valores
• Igualdad definicional: los términos pueden reducirse durante el chequeo
• Tipos inductivos: números naturales, listas, árboles, igualdad, todo incorporado a la teoría central
• Elaboración: Lean completa los argumentos omitidos, infiere los implícitos y resuelve la notación
• Tácticas (tactics): trabajás al nivel del estado de la demostración en vez de con términos lambda crudos
• Automatización: simplificadores, solvers aritméticos, reescritura, procedimientos de decisión
• Una frontera de confianza real: constructores privados, aislamiento del kernel, nada librado a la buena fe

Pero nada de eso cambia el cuadro central. Sigue habiendo un kernel. Sigue habiendo términos. Sigue habiendo tipos. Sigue habiendo un checker.

Por eso construir aunque sea un demostrador chiquito aclara tanto. Separa las partes que hacen funcionar la lógica de las partes que hacen que el sistema sea cómodo de usar.

#Por qué Python es el lenguaje correcto para este artículo

El sistema de tipos de Python es demasiado débil para el truco al estilo Julia de hacer que el lenguaje anfitrión haga las demostraciones. Justamente por eso es útil acá.

En este artículo, el demostrador es explícito:

• los términos son tus dataclasses
• las proposiciones son tus dataclasses
• el checker es tu función
• la frontera de confianza es código que podés señalar con un dedo

No hay nada escondido en el lenguaje anfitrión. Eso hace de Python un buen lenguaje para enseñar la arquitectura, aunque sería un mal lenguaje para metaprogramación con el sistema de tipos del anfitrión.

#La verdadera lección

La distancia entre el código de un intérprete común y el kernel de un demostrador de teoremas es mucho más chica de lo que piensa la mayoría de los programadores. Empezás con:

• una sintaxis
• unas pocas reglas de inferencia
• un checker que las hace cumplir

Eso alcanza para tener una noción real de demostración.

Lean es la misma arquitectura, llevada más lejos y mejor construida.

El próximo artículo muestra la perspectiva complementaria: en vez de implementar el demostrador explícitamente, mete uno chiquito dentro del propio sistema de tipos de Julia. Las mismas ideas, otra lección.