2026-04-08

La Correspondencia Curry-Howard: De la Lógica Intuicionista a la Clásica

Recordemos que la correspondencia Curry-Howard establece un puente fundamental entre la lógica y la computación: los tipos corresponden a proposiciones y los programas corresponden a demostraciones.

En Haskell, esto se puede ver de la siguiente manera: $\lambda x.x:P⟹P$

teorema :: p -> p
teorema = \x -> x

A la vez que compila nuestro programa con éxito, nuestra demostración es verificada por el sistema de tipos.

De manera más precisa, la correspondencia Curry-Howard clásica establece una conexión entre la lógica intuicionista y el cálculo lambda tipado (el cual, como sabemos, es la base de lenguajes funcionales como Haskell).

La lógica intuicionista se caracteriza por rechazar el principio del tercio excluso: $P\vee \neg P$. Algo que en su momento ofendió a muchos matemáticos, entre ellos al gran David Hilbert:

“Quitarle el principio del tercio excluso al matemático sería lo mismo, digamos, que prohibirle el telescopio al astrónomo o al boxeador el uso de sus puños”.

La razón por la cual la lógica intuicionista rechaza este principio es porque exige que las demostraciones sean constructivas; es decir, se debe construir evidencia tangible de lo que se afirma. Para afirmar $A\vee B$, debes dar evidencia explícita de $A$, o bien dar evidencia explícita de $B$.

ej1 :: a -> Either a b
ej1 = \x -> Left x
 
ej2 :: b -> Either a b
ej2 = \x -> Right x

El Problema del Paro

import Data.Void
type No a = a -> Void
 
tercioExcluso :: Either p (No p)
-- tercioExcluso = IMPOSIBLE

Si intentamos demostrar $P\vee \neg P$ escribiendo una función, pronto nos daremos por vencidos, pues esto nos exigiría un algoritmo capaz de decidir cualquier proposición de antemano.

Para convencernos de esto, supongamos por un momento, que existe tal programa, entonces podríamos resolver el problema del paro, es decir, podríamos escribir un algoritmo que decida si una máquina se detiene o no, la función analizador toma una cadena (que puede ser código en tu lenguaje favorito) y devuelve t si el código se detiene o \neg t en caso contrario.

analizador :: String -> Either t (No t)
analizador _ = tercioExcluso

La Lógica Clásica

Por otro lado, la lógica clásica se caracteriza por aceptar el principio del tercio excluso y todas sus formas equivalentes, algunas de ellas son:

• $P\vee \neg P$ (Tercio excluso)
• $\neg \neg P⟹P$ (Eliminación de la doble negación)
• $((P⟹Q)⟹P)⟹P$ (Ley de Peirce)

Por años, se creyó que no existía correspondencia Curry-Howard para la lógica clásica. Hasta que en 1990, Tim Griffin respondió a la pregunta: Si la lógica intuicionista se conecta con el cálculo lambda tipado, ¿con qué se conecta la lógica clásica?

Para entenderlo, tenemos que hablar de continuaciones. Una continuación es simplemente una función que representa el “resto de la ejecución” de un programa en un punto específico. Ejemplo: Haskell

ej :: Int
ej = (1 + 2) * (3 + 4)
 
ejCont :: Int
ejCont = (\a ->
            (\b ->
                a * b
            ) (3 + 4)
         ) (1 + 2)

• La continuación de ej en el punto $p=(1+2)$ es $\lambda a\to a\ast (3+4)$
• La continuación de ej en el punto $p^{\prime }=(3+4)$ es $\lambda b\to (1+2)\ast b$

El Estilo de Paso de Continuaciones (CPS) es una técnica utilizada para manipular este flujo. Veamos el factorial tradicional vs. CPS:

factorial :: Int -> Int
factorial 0 = 1
factorial n = n * factorial (n - 1)
 
factCPS :: Int -> (Int -> r) -> r
factCPS 0 k = k 1
factCPS n k = factCPS (n - 1) (\x -> k (n * x))

Para ahorrarnos traducir el código manualmente, usamos la mónada Cont:

import Control.Monad.Cont
 
fact :: Int -> Cont r Int
fact 0 = return 1
fact n = do
    m <- fact (n - 1)
    return (n * m)

Lo importante aquí son los tipos: en factorial teníamos Int -> Int, en factCPS tenemos Int -> (Int -> r) -> r. La mónada Cont r transforma un tipo A en (A -> r) -> r.

En lógica intuicionista, definimos la negación como $\neg P:=P⟹\perp$. Si tomamos el tipo de nuestras continuaciones y asumimos que r puede representar $\perp$, el tipo (P -> r) -> r se lee lógicamente como $\neg \neg P$.

Si escribimos el tercio excluso en estilo de continuaciones puras:

tercioExclusoDobleNeg :: Cont r (Either p (p -> r))
tercioExclusoDobleNeg = cont $ \k -> k (Right (\p -> k (Left p)))

Aquí hay una sutileza crucial: el tipo de arriba se traduce lógicamente como $\neg \neg (P\vee \neg P)$. ¡Sorprendentemente, la doble negación del tercio excluso sí es un teorema válido en la lógica intuicionista!

La mónada Cont en Haskell simplemente simula este comportamiento clásico operando con dobles negaciones por debajo. Para tener una lógica clásica verdaderamente “nativa”, es necesario abandonar los lenguajes funcionales tradicionales y utilizar cálculos abstractos diseñados desde cero. Hoy en día existen múltiples propuestas teóricas para lograr esto, y es por ello que la correspondencia Curry-Howard para la lógica clásica constituye un fascinante campo de estudio en sí mismo.

Aun así, a nivel conceptual, podemos cerrar con la siguiente gran conclusión:

Si la lógica intuicionista corresponde al cálculo lambda tipado puro, la lógica clásica corresponde al cálculo lambda tipado extendido con operadores de control (como las continuaciones, las excepciones u otros mecanismos que nos permiten alterar el flujo de nuestros programas).