Correspondencia entre Curry y Howard

Al principio fue una simple observación en el libro de Curry y Feys de 1958 sobre lógica combinatoria: los tipos más simples para los combinadores básicos K y S de la lógica combinatoria correspondían sorprendentemente a los respectivos esquemas axiomáticos α → ( β → α ) y ( α → ( β → γ )) → (( α → β ) → ( α → γ )) utilizados en los sistemas de deducción de estilo Hilbert . Por esta razón, estos esquemas ahora se denominan a menudo axiomas K y S. A continuación se presentan ejemplos de programas vistos como demostraciones en una lógica de estilo Hilbert .

Si nos restringimos al fragmento intuicionista implicacional, una forma sencilla de formalizar la lógica al estilo de Hilbert es la siguiente. Sea Γ una colección finita de fórmulas, consideradas como hipótesis. Entonces δ se puede derivar de Γ, denotado Γ ⊢ δ, en los siguientes casos:

• δ es una hipótesis, es decir, es una fórmula de Γ,
• δ es una instancia de un esquema axiomático; es decir, bajo el sistema axiomático más común:
  • δ tiene la forma α → ( β → α ), o
  • δ tiene la forma ( α → ( β → γ )) → (( α → β ) → ( α → γ )),
• δ se deduce, es decir, para algún α , tanto α → δ como α ya se pueden derivar de Γ (esta es la regla del modus ponens ).

Esto se puede formalizar utilizando reglas de inferencia , como se muestra en la columna izquierda de la siguiente tabla.

La lógica combinatoria tipada puede formularse utilizando una sintaxis similar: sea Γ una colección finita de variables, anotadas con sus tipos. Un término T (también anotado con su tipo) dependerá de estas variables [Γ ⊢ T: δ ] cuando:

• T es una de las variables en Γ,
• T es un combinador básico; es decir, bajo la base de combinadores más común:
  • T es K: α → ( β → α ) [donde α y β denotan los tipos de sus argumentos], o
  • T es S:( α → ( β → γ )) → (( α → β ) → ( α → γ )),
• T es la composición de dos subtérminos que dependen de las variables en Γ.

Las reglas de generación definidas aquí se presentan en la columna derecha. La observación de Curry simplemente indica que ambas columnas están en correspondencia biunívoca. La restricción de la correspondencia a la lógica intuicionista implica que algunas tautologías clásicas , como la ley de Peirce (( α → β ) → α ) → α , quedan excluidas de dicha correspondencia.

Desde una perspectiva más abstracta, la correspondencia puede reformularse como se muestra en la siguiente tabla. En particular, el teorema de deducción propio de la lógica de Hilbert coincide con el proceso de eliminación de abstracciones de la lógica combinatoria.

Gracias a esta correspondencia, los resultados de la lógica combinatoria pueden transferirse a la lógica de Hilbert y viceversa. Por ejemplo, la noción de reducción de términos en lógica combinatoria puede transferirse a la lógica de Hilbert, lo que proporciona una forma de transformar canónicamente demostraciones en otras demostraciones de la misma proposición. También se puede transferir la noción de términos normales a una noción de demostraciones normales, expresando que las hipótesis de los axiomas nunca necesitan estar completamente separadas (ya que de lo contrario podría producirse una simplificación).

Por el contrario, la no demostrabilidad en la lógica intuicionista de la ley de Peirce puede transferirse de nuevo a la lógica combinatoria: no hay ningún término tipificado de la lógica combinatoria que sea tipificable con tipo

(( α → β ) → α ) → α .

También se pueden transferir resultados sobre la completitud de algunos conjuntos de combinadores o axiomas. Por ejemplo, el hecho de que el combinador X constituya una base de un punto de la lógica combinatoria (extensional) implica que el esquema de axioma único

((( α → ( β → γ )) → (( α → β ) → ( α → γ ))) → (( δ → ( ε → δ )) → ζ )) → ζ ,

que es el tipo principal de X , es un reemplazo adecuado para la combinación de los esquemas axiomáticos

α → ( β → α ) y

( α → ( β → γ )) → (( α → β ) → ( α → γ )).

Después de que Curry enfatizara la correspondencia sintáctica entre la deducción intuicionista de estilo Hilbert y la lógica combinatoria tipada , Howard explicitó en 1969 una analogía sintáctica entre los programas del cálculo lambda simplemente tipado y las demostraciones de la deducción natural . A continuación, el lado izquierdo formaliza la deducción natural implicacional intuicionista como un cálculo de secuencias (el uso de secuencias es estándar en las discusiones del isomorfismo de Curry-Howard, ya que permite enunciar las reglas de deducción de manera más clara) con debilitamiento implícito y el lado derecho muestra las reglas de tipado del cálculo lambda . En el lado izquierdo, Γ, Γ ₁ y Γ ₂ denotan secuencias ordenadas de fórmulas, mientras que en el lado derecho, denotan secuencias de fórmulas con nombre (es decir, tipadas) con todos los nombres diferentes.

Parafraseando la correspondencia, probar Γ ⊢ α significa tener un programa que, dados valores con los tipos listados en Γ, fabrica un objeto de tipo α . Un axioma/hipótesis corresponde a la introducción de una nueva variable con un nuevo tipo no restringido, la regla → I  corresponde a la abstracción de funciones y la regla → E  corresponde a la aplicación de funciones . Nótese que la correspondencia no es exacta si el contexto Γ se toma como un conjunto de fórmulas, ya que, por ejemplo, los términos λ λ x .λ y . x y λ x .λ y . y de tipo α → α → α no se distinguirían en la correspondencia. A continuación se dan ejemplos .

Howard demostró que la correspondencia se extiende a otros conectores de la lógica y otras construcciones del cálculo lambda simplemente tipado. Vista a un nivel abstracto, la correspondencia puede resumirse como se muestra en la siguiente tabla. En particular, también muestra que la noción de formas normales en el cálculo lambda coincide con la noción de deducción normal de Prawitz en la deducción natural , de lo cual se deduce que los algoritmos para el problema de la habitabilidad de tipos pueden transformarse en algoritmos para decidir la demostrabilidad intuicionista .

La correspondencia de Howard se extiende naturalmente a otras extensiones de la deducción natural y del cálculo lambda tipado simple . He aquí una lista no exhaustiva:

• El sistema F de Girard-Reynolds como lenguaje común tanto para la lógica proposicional de segundo orden como para el cálculo lambda polimórfico,
• lógica de orden superior y el sistema F _ω de Girard
• tipos inductivos como tipo de datos algebraicos
• necesidad${\displaystyle \Box }$en lógica modal y computación por etapas ^{[ 12 ]}
• posibilidad${\displaystyle \Diamond }$en lógica modal y tipos monádicos para efectos ^{[ 11 ]}
• El cálculo λ _I (donde la abstracción se restringe a λx . E donde x tiene al menos una ocurrencia libre en E) y el cálculo CL _I corresponden a la lógica relevante . ^{[ 13 ]}
• La modalidad de verdad local (∇) en la topología de Grothendieck o la modalidad "relajada" equivalente (◯) de Benton, Bierman y de Paiva (1998) corresponden a la lógica CL que describe "tipos de computación". ^{[ 14 ]}

En la época de Curry, y también en la de Howard, la correspondencia entre las pruebas y los programas se refería únicamente a la lógica intuicionista , es decir, una lógica en la que, en particular, la ley de Peirce no era deducible. La extensión de esta correspondencia a la ley de Peirce y, por ende, a la lógica clásica, se hizo evidente a partir del trabajo de Griffin sobre operadores de tipado que capturan el contexto de evaluación de la ejecución de un programa dado, de modo que este contexto de evaluación pueda reinstalarse posteriormente. La correspondencia básica al estilo Curry-Howard para la lógica clásica se presenta a continuación. Nótese la correspondencia entre la traducción de doble negación utilizada para mapear las pruebas clásicas a la lógica intuicionista y la traducción de paso de continuaciones utilizada para mapear términos lambda que implican control a términos lambda puros. Más concretamente, las traducciones de paso de continuaciones por nombre se relacionan con la traducción de doble negación de Kolmogorov , y las traducciones de paso de continuaciones por valor se relacionan con un tipo de traducción de doble negación debida a Kuroda.

Existe una correspondencia más precisa entre Curry y Howard para la lógica clásica si se define esta no mediante la adición de un axioma como la ley de Peirce , sino permitiendo varias conclusiones en secuencias. En el caso de la deducción natural clásica, existe una correspondencia de demostraciones como programas con los programas tipados del cálculo λμ de Parigot .

Se puede establecer una correspondencia entre las demostraciones y los programas para el formalismo conocido como cálculo de secuencias de Gentzen , pero no se trata de una correspondencia con un modelo de computación preexistente bien definido, como sí ocurría con las deducciones naturales y al estilo de Hilbert.

El cálculo de secuencias se caracteriza por la presencia de reglas de introducción izquierda, regla de introducción derecha y una regla de corte que puede eliminarse. La estructura del cálculo de secuencias se relaciona con un cálculo cuya estructura es cercana a la de algunas máquinas abstractas . La correspondencia informal es la siguiente:

En un artículo publicado en 1970, pero basado en una charla impartida en el Primer Simposio Escandinavo de Lógica, celebrado en Åbo/Turku en 1968, Dag Prawitz definió un homomorfismo entre derivaciones de deducción natural para la lógica de primer orden mínima e intuicionista y términos de construcción de un lenguaje muy similar al cálculo lambda tipado (la correspondencia surge de una prueba de la solidez de esas lógicas sobre el lenguaje de términos de construcción). ^{[ 15 ]} Aunque el homomorfismo de Prawitz es menos potente que el isomorfismo de Curry-Howard, con un lenguaje de tipos más fuerte también se convierte en un isomorfismo, aunque aún carece de tipos dependientes. Es de suponer que Prawitz desconocía el trabajo de Howard, especialmente porque la charla de la que se extrae su artículo de 1970 se impartió un año antes de que el manuscrito de Howard comenzara a circular.

NG de Bruijn utilizó la notación lambda para representar las demostraciones del verificador de teoremas Automath , y representó las proposiciones como "categorías" de sus demostraciones. Esto ocurrió a finales de la década de 1960, en el mismo período en que Howard escribió su manuscrito; es probable que de Bruijn desconociera el trabajo de Howard y que la correspondencia se estableciera de forma independiente. ^{[ 16 ]} Algunos investigadores tienden a utilizar el término correspondencia Curry-Howard-de Bruijn en lugar de correspondencia Curry-Howard.

La interpretación BHK interpreta las demostraciones intuicionistas como funciones, pero no especifica la clase de funciones relevante para dicha interpretación. Si se considera el cálculo lambda para esta clase de funciones, entonces la interpretación BHK expresa lo mismo que la correspondencia de Howard entre la deducción natural y el cálculo lambda.

La realizabilidad recursiva de Kleene divide las demostraciones de la aritmética intuicionista en dos pares: una función recursiva y una demostración de una fórmula que expresa que la función recursiva "se realiza", es decir, instancia correctamente las disyunciones y los cuantificadores existenciales de la fórmula inicial, de modo que la fórmula se vuelve verdadera.

La realizabilidad modificada de Kreisel se aplica a la lógica de predicados intuicionista de orden superior y demuestra que el término lambda simplemente tipado, extraído inductivamente de la prueba, realiza la fórmula inicial. En el caso de la lógica proposicional, coincide con la afirmación de Howard: el término lambda extraído es la prueba misma (considerada como un término lambda sin tipar) y la afirmación de realizabilidad es una paráfrasis del hecho de que el término lambda extraído tiene el tipo que la fórmula significa (considerado como un tipo).

La interpretación dialéctica de Gödel realiza (una extensión de) la aritmética intuicionista con funciones computables. La conexión con el cálculo lambda no está clara, incluso en el caso de la deducción natural.

A principios de la década de 1970, Joachim Lambek demostró que las demostraciones de la lógica proposicional intuicionista y los combinadores de la lógica combinatoria tipada comparten una teoría ecuacional común: la teoría de las categorías cartesianas cerradas . La expresión «correspondencia de Curry-Howard-Lambek» se utiliza actualmente para referirse a las relaciones entre la lógica intuicionista, el cálculo lambda tipado y las categorías cartesianas cerradas. Según esta correspondencia, los objetos de una categoría cartesiana cerrada pueden interpretarse como proposiciones (tipos) y los morfismos como deducciones que asignan un conjunto de supuestos ( contexto de tipado ) a un consecuente válido (término bien tipado). ^{[ 17 ]}

La correspondencia de Lambek es una correspondencia de teorías ecuacionales, que abstrae la dinámica de la computación, como la reducción beta y la normalización de términos, y no es la expresión de una identidad sintáctica de estructuras, como ocurre con las correspondencias de Curry y Howard: es decir, la estructura de un morfismo bien definido en una categoría cartesiana cerrada no es comparable a la estructura de una demostración del juicio correspondiente en la lógica de Hilbert ni en la deducción natural. Por ejemplo, no es posible afirmar ni demostrar que un morfismo sea normalizador, establecer un teorema de tipo Church-Rosser ni hablar de una categoría cartesiana cerrada "fuertemente normalizadora". Para aclarar esta distinción, la estructura sintáctica subyacente de las categorías cartesianas cerradas se reformula a continuación.

Los objetos (proposiciones/tipos) incluyen:

• ${\displaystyle \top }$como objeto
• dado${\displaystyle \alpha }$y${\displaystyle \beta }$como objetos, entonces${\displaystyle \alpha \times \beta }$y${\displaystyle \alpha \rightarrow \beta }$como objetos.

Los morfismos (deducciones/términos) incluyen:

• identidades:${\displaystyle {\text{id}}_{\alpha }:\alpha \to \alpha }$
• composición: si${\displaystyle t:\alpha \to \beta }$y${\displaystyle u:\beta \to \gamma }$son morfismos${\displaystyle u\circ t:\alpha \to \gamma }$es un morfismo
• morfismos terminales :${\displaystyle \star _{\alpha }:\alpha \to \top }$
• productos: si${\displaystyle t:\alpha \to \beta }$y${\displaystyle u:\alpha \to \gamma }$son morfismos,${\displaystyle (t,u):\alpha \to \beta \times \gamma }$es un morfismo
• proyecciones:${\displaystyle \pi _{\alpha ,\beta ,1}:\alpha \times \beta \to \alpha }$y${\displaystyle \pi _{\alpha ,\beta ,2}:\alpha \times \beta \to \beta }$
• evaluación:${\displaystyle {\text{eval}}_{\alpha ,\beta }:(\alpha \to \beta )\times \alpha \to \beta }$
• curry: si${\displaystyle t:\alpha \times \beta \to \gamma }$es un morfismo,${\displaystyle \lambda t:\alpha \to \beta \to \gamma }$es un morfismo.

De forma equivalente a las anotaciones anteriores, los morfismos bien definidos (términos tipados) en cualquier categoría cartesiana cerrada pueden construirse según las siguientes reglas de tipado . La notación habitual de morfismos categóricos${\displaystyle f:\alpha \to \beta }$se reemplaza con la notación de contexto de tipado${\displaystyle \alpha \vdash f:\beta }$.

Identidad:

${\displaystyle {\frac {}{\alpha \vdash {\text{id}}:\alpha }}}$

Composición:

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \beta \vdash u:\gamma }{\alpha \vdash u\circ t:\gamma }}}$

Tipo de unidad ( objeto terminal ):

${\displaystyle {\frac {}{\alpha \vdash \star$ :\arriba }}}

Producto cartesiano:

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \alpha \vdash u:\gamma }{\alpha \vdash (t,u):\beta \times \gamma }}}$

Proyección izquierda y derecha:

${\displaystyle {\frac {}{\alpha \times \beta ~\vdash ~\pi _{1}:\alpha }}\qquad {\frac {}{\alpha \times \beta ~\vdash ~\pi _{2}:\beta }}}$

Curry :

${\displaystyle {\frac {\alpha \times \beta ~\vdash ~t:\gamma }{\alpha \vdash \lambda t:\beta \to \gamma }}}$

Solicitud :

${\displaystyle {\frac {}{(\alpha \rightarrow \beta )\times \alpha \vdash {\text{eval}}:\beta }}}$

Finalmente, las ecuaciones de la categoría son

• ${\displaystyle {\text{id}}\circ t=t}$
• ${\displaystyle t\circ {\text{id}}=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star ={\text{id}}}$ (si está bien escrito)
• ${\displaystyle \star \circ u=\star }$
• ${\displaystyle \pi _{1}\circ (t,u)=t}$
• ${\displaystyle \pi _{2}\circ (t,u)=u}$
• ${\displaystyle (\pi _{1},\pi _{2})=id}$
• ${\displaystyle (t_{1},t_{2})\circ u=(t_{1}\circ u,t_{2}\circ u)}$
• ${\displaystyle {\text{eval}}\circ (\lambda t\circ \pi _{1},\pi _{2})=t}$
• ${\displaystyle \lambda {\text{eval}}={\text{id}}}$
• ${\displaystyle \lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))}$

Estas ecuaciones implican lo siguiente:${\displaystyle \eta }$-leyes:

• ${\displaystyle (\pi _{1}\circ t,\pi _{2}\circ t)=t}$
• ${\displaystyle \lambda ({\text{eval}}\circ (t\circ \pi _{1},\pi _{2}))=t}$

Ahora bien, existe tal que${\displaystyle \alpha _{1}\times \ldots \times \alpha _{n}\vdash t:\beta }$si y solo si${\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta }$es demostrable en lógica intuicionista implicacional.

Como ejemplo, consideremos una demostración del teorema α → α . En cálculo lambda , este es el tipo de la función identidad I = λx . x y en lógica combinatoria, la función identidad se obtiene aplicando S = λfgx . fx ( gx ) dos veces a K = λxy . x . Es decir, I = (( S K ) K ) . Como descripción de una demostración, esto dice que se pueden usar los siguientes pasos para probar α → α :

• instanciar el segundo esquema de axioma con las fórmulas α , β → α y α para obtener una prueba de ( α → (( β → α ) → α )) → (( α → ( β → α )) → ( α → α )) ,
• Instancie el primer esquema axiomático una vez con α y β → α para obtener una prueba de α → (( β → α ) → α ) ,
• Instanciar el primer esquema axiomático una segunda vez con α y β para obtener una prueba de α → ( β → α ) ,
• aplicar modus ponens dos veces para obtener una prueba de α → α

En general, el procedimiento consiste en que siempre que el programa contenga una aplicación de la forma ( PQ ), se deben seguir estos pasos:

1. Primero , demuestre los teoremas correspondientes a los tipos de P y Q.
2. Dado que P se aplica a Q , el tipo de P debe tener la forma α → β y el tipo de Q debe tener la forma α para algún α y β . Por lo tanto, es posible separar la conclusión, β , mediante la regla del modus ponens.

Como ejemplo más complejo, veamos el teorema que corresponde a la función B. El tipo de B es ( β → α ) → ( γ → β ) → γ → α . B es equivalente a ( S ( K S ) K ). Este es nuestro mapa de ruta para la demostración del teorema ( β → α ) → ( γ → β ) → γ → α .

El primer paso es construir ( K S ). Para que el antecedente del axioma K se parezca al axioma S , establezca α igual a ( α → β → γ ) → ( α → β ) → α → γ , y β igual a δ (para evitar colisiones de variables):

K  : α → β → α

K [ α = ( α → β → γ ) → ( α → β ) → α → γ , β = δ ]  : (( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( α → β → γ ) → ( α → β ) → α → γ

Dado que el antecedente aquí es simplemente S , el consecuente se puede separar utilizando Modus Ponens:

KS  : δ → ( α → β → γ ) → ( α → β ) → α → γ

Este es el teorema que corresponde al tipo de ( K S ). Ahora aplicamos S a esta expresión. Tomando S como sigue

S  : ( α → β → γ ) → ( α → β ) → α → γ ,

ponga α = δ , β = α → β → γ , y γ = ( α → β ) → α → γ , dando como resultado

S [ α = δ , β = α → β → γ , γ = ( α → β ) → α → γ ]  : ( δ → ( α → β → γ ) → ( α → β ) → α → γ ) → ( δ → ( α → β → γ )) → δ → ( α → β ) → α → γ

y luego separar el consecuente:

S (KS)  : ( δ → α → β → γ ) → δ → ( α → β ) → α → γ

Esta es la fórmula para el tipo de ( S ( K S )). Un caso especial de este teorema tiene δ = ( β → γ ) :

S (KS) [ δ = β → γ ]  : (( β → γ ) → α → β → γ ) → ( β → γ ) → ( α → β ) → α → γ

Esta última fórmula debe aplicarse a K. Especialicemos K nuevamente, esta vez reemplazando α con ( β → γ ) y β con α :

K  : α → β → α

K [ α = β → γ , β = α ]  : ( β → γ ) → α → ( β → γ )

Esto es lo mismo que el antecedente de la fórmula anterior, por lo que, separando el consecuente:

S (KS) K  : ( β → γ ) → ( α → β ) → α → γ

Al intercambiar los nombres de las variables α y γ obtenemos

( β → α ) → ( γ → β ) → γ → α

Eso era lo que quedaba por demostrar.

El siguiente diagrama demuestra que ( β → α ) → ( γ → β ) → γ → α en deducción natural y muestra cómo se puede interpretar como la expresión λ λ a .λ b .λ g .( a ( b g )) de tipo ( β → α ) → ( γ → β ) → γ → α .

 a:β → α, b:γ → β, g:γ ⊢ b : γ → β a:β → α, b:γ → β, g:γ ⊢ g : γ ——————————————————————————————————— ———————————————————————————————————————————————————————————————————— a:β → α, b:γ → β, g:γ ⊢ a : β → α a:β → α, b:γ → β, g:γ ⊢ bg : β ——————————————————————————————————————————————————————————————————————— a:β → α, b:γ → β, g:γ ⊢ a (bg) : α ———————————————————————————————————— a:β → α, b:γ → β ⊢ λ gramo. a (bg) : γ → α ———————————————————————————————————————— a:β → α ⊢ λ b. λ g. a (bg) : (γ → β) → γ → α ———————————————————————————————————— ⊢ λa. λb. λ g. a (bg) : (β → α) → (γ → β) → γ → α

Los científicos cognitivos han utilizado la teoría del procesamiento dual , que contrasta el pensamiento rápido e intuitivo del "Sistema 1" con el pensamiento lento y deliberativo del "Sistema 2", como marco para analizar cómo razonan y toman decisiones los grandes modelos de lenguaje (LLM). ^{[ 20 ]} Por otra parte, una técnica de ingeniería común permite que un modelo escriba y ejecute código informático mientras trabaja en un problema: en lugar de predecir una respuesta directamente en texto, el modelo escribe un programa corto, un intérprete externo lo ejecuta y el modelo lee el resultado. Se ha demostrado que delegar el cálculo a un intérprete de esta manera reduce los errores aritméticos y lógicos. ^{[ 21 ] [ 22 ]}

La correspondencia de Curry-Howard aclara qué puede y qué no puede establecer el código en ejecución. Según esta correspondencia, una prueba es un programa bien tipado y la proposición que prueba es el tipo de ese programa, por lo que verificar una prueba equivale a verificar el tipo de un programa; el contenido lógico reside en el sistema de tipos, no en la ejecución. ^{[ 23 ]} Los lenguajes de propósito general como Python, SQL y JavaScript no fueron diseñados como sistemas de prueba, y los investigadores en matemáticas formalizadas han argumentado que las pruebas y los programas desempeñan roles epistémicos fundamentalmente diferentes, por lo que la analogía entre codificación y demostración es limitada en la práctica. ^{[ 24 ]} Además, los operadores modales □ (necesidad) y ◇ (posibilidad) adquieren interpretaciones computacionales solo en sistemas de tipos modales especializados, de los que carecen los lenguajes de programación convencionales. ^{[ 11 ]}

Los asistentes de prueba como Rocq , Lean y Agda se basan directamente en la correspondencia: un teorema se enuncia como un tipo, y una prueba verificada por máquina es un programa de ese tipo. La combinación de LLM con estos sistemas (todos los cuales pueden ejecutarse como ejecución de código, junto con probadores como Sympy ) produce un razonamiento que se verifica en lugar de simplemente ejecutarse. AlphaProof, un sistema desarrollado por Google DeepMind , utilizó aprendizaje por refuerzo para entrenar un modelo para escribir pruebas Lean en un currículo de decenas de millones de enunciados de problemas formalizados automáticamente; cada prueba que produce es verificada por Lean, y el sistema logró una puntuación equivalente a una medalla de plata en la Olimpiada Internacional de Matemáticas de 2024. ^{[ 25 ]} El razonamiento verificado por máquina en lógica modal de orden superior también es alcanzable al incrustar la lógica modal en la lógica de un probador existente, un enfoque utilizado para verificar formalmente la prueba ontológica de Gödel . ^{[ 26 ]} Un obstáculo restante es la autoformalización : traducir de manera confiable enunciados matemáticos del lenguaje natural al lenguaje formal. ^{[ 27 ] [ 28 ]}

Algunos investigadores han propuesto aplicar la correspondencia directamente al razonamiento de los LLM. Una propuesta de 2025 trata cada paso de la cadena de pensamiento de un modelo como una inferencia lógica tipificada, de modo que un rastro de razonamiento que se convierte en una prueba bien tipificada sirve como un certificado verificable de su propia corrección. ^{[ 29 ]} Sin embargo, las revisiones del campo advierten que la generación de pruebas ha demostrado ser considerablemente más frágil para los LLM que la generación de código, y que la elegancia de la correspondencia por sí sola no cierra esta brecha. ^{[ 24 ]}

• Curry, HB (1934-09-20). "Funcionalidad en lógica combinatoria" . Actas de la Academia Nacional de Ciencias de los Estados Unidos de América . 20 ( 11): 584– 90. Bibcode : 1934PNAS...20..584C . doi : 10.1073/pnas.20.11.584 . ISSN 0027-8424 . PMC 1076489. PMID 16577644 .   
• Curry, Haskell B; Feys, Robert (1958). Craig, William (ed.). Lógica combinatoria . Estudios de lógica y fundamentos de las matemáticas. Vol.  1. North-Holland Publishing Company. LCCN a59001593 ; con dos secciones de Craig, William; véase el párrafo 9E. {{cite book}}: CS1 mantenimiento: postscript ( enlace )
• De Bruijn, Nicolaas (1968), Automath, un lenguaje para las matemáticas , Departamento de Matemáticas, Universidad Tecnológica de Eindhoven , informe TH 68-WSK-05. Reimpreso en forma revisada, con dos páginas de comentarios, en: Automation and Reasoning, vol. 2, Classical papers on computational logic 1967–1970 , Springer Verlag, 1983, pp.  159–200.
• Howard, William A. (septiembre de 1980) [manuscrito original del artículo de 1969], "La noción de construcción de fórmulas como tipos" (PDF) , en Seldin, Jonathan P.; Hindley , J. Roger (eds.), To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , Academic Press , pp. 479–490 , ISBN  978-0-12-349050-6
• Martin-Löf, Per (1975), "Sobre los modelos de teorías de tipos intuicionistas y la noción de igualdad definicional", en Kanger, Stig (ed.), Actas del Tercer Simposio Escandinavo de Lógica , Elsevier, pp. 81–109 . 
• Prawitz, Dag (1970), "Semántica constructiva", Actas del Primer Simposio Escandinavo de Lógica , págs. 96–114 

• Moggi, Eugenio (1991), "Nociones de computación y mónadas" (PDF) , Information and Computation , 93 (1): 55–92 , doi : 10.1016/0890-5401(91)90052-4
• Davies, Rowan; Pfenning, Frank (2001), "Análisis modal de la computación por etapas" (PDF) , Journal of the ACM , 48 (3): 555–604 , CiteSeerX 10.1.1.3.5442 , doi : 10.1145/382780.382785 , S2CID 52148006  
• Pfenning, Frank; Davies, Rowan (2001), "Una reconstrucción juiciosa de la lógica modal" (PDF) , Estructuras matemáticas en ciencias de la computación , 11 (4): 511– 540, CiteSeerX 10.1.1.43.1611 , doi : 10.1017/S0960129501003322 , S2CID 16467268  
• Benton; Bierman; de Paiva (1998), "Tipos computacionales desde una perspectiva lógica", Journal of Functional Programming , 8 (2): 177– 193, CiteSeerX 10.1.1.258.6004 , doi : 10.1017/s0956796898002998 , S2CID 6149614  
• Griffin, Timothy G. (1990), "The Formulae-as-Types Notion of Control", Actas del 17.º Simposio Anual de la ACM sobre Principios de Lenguajes de Programación, POPL '90, San Francisco, CA, EE. UU., 17-19 de enero de 1990 , págs. 47-57 , doi : 10.1145/96709.96714 , ISBN  978-0-89791-343-0, S2CID 3005134 
• Parigot, Michel (1992), "Cálculo Lambda-mu: Una interpretación algorítmica de la deducción natural clásica", Actas de la Conferencia Internacional sobre Programación Lógica y Razonamiento Automatizado: LPAR '92, San Petersburgo, Rusia , Lecture Notes in Computer Science, vol.  624, Springer-Verlag , pp. 190–201 , ISBN  978-3-540-55727-2
• Herbelin, Hugo (1995), "Una estructura de cálculo lambda isomorfa a la estructura de cálculo de secuencias de estilo Gentzen", en Pacholski, Leszek; Tiuryn, Jerzy (eds.), Lógica en Ciencias de la Computación, 8.º Taller Internacional, CSL '94, Kazimierz, Polonia, 25-30 de septiembre de 1994, Artículos seleccionados , Lecture Notes in Computer Science, vol.  933, Springer-Verlag , pp. 61-75 , ISBN  978-3-540-60017-6
• Gabbay, Dov; de Queiroz, Ruy (1992). "Extending the Curry–Howard interpretation to linear, relevant and other resource logics". Journal of Symbolic Logic . Vol.  57. Association for Symbolic Logic. pp. 1319–1365 . doi : 10.2307/2275370 . JSTOR 2275370. S2CID 7159005 .   (Versión completa del artículo presentado en el Logic Colloquium '90 , Helsinki. Resumen en JSL 56(3):1139–1140, 1991.)
• de Queiroz, Ruy; Gabbay, Dov (1994), «Igualdad en sistemas deductivos etiquetados y la interpretación funcional de la igualdad proposicional», en Dekker, Paul; Stokhof, Martin (eds.), Actas del Noveno Coloquio de Ámsterdam , ILLC/Departamento de Filosofía, Universidad de Ámsterdam, pp. 547–565 , ISBN  978-90-74795-07-4
• de Queiroz, Ruy; Gabbay, Dov (1995), "La interpretación funcional del cuantificador existencial" , Boletín del Grupo de Interés en Lógicas Puras y Aplicadas , 3 ( 2–3 ): 243–290 , doi : 10.1093/jigpal/3.2-3.243(Versión completa de un artículo presentado en el Logic Colloquium '91 , Uppsala. Resumen en JSL 58(2):753–754, 1993.)
• de Queiroz, Ruy; Gabbay, Dov (1997), "La interpretación funcional de la necesidad modal", en de Rijke, Maarten (ed.), Avances en lógica intensional , Serie de lógica aplicada, vol.  7, Springer-Verlag , pp. 61–91 , ISBN  978-0-7923-4711-8
• de Queiroz, Ruy; Gabbay, Dov (1999), «Deducción natural etiquetada» , en Ohlbach, Hans-Juergen; Reyle, Uwe (eds.), Lógica, lenguaje y razonamiento. Ensayos en honor de Dov Gabbay , Trends in Logic, vol.  7, Kluwer, pp. 173–250 , ISBN  978-0-7923-5687-5
• de Oliveira, Anjolina; de Queiroz, Ruy (1999), "Un procedimiento de normalización para el fragmento ecuacional de la deducción natural etiquetada", Logic Journal of the Interest Group in Pure and Applied Logics , vol.  7, Oxford University Press , pp. 173–215 (Versión completa de un artículo presentado en el 2.º WoLLIC'95 , Recife. Resumen en Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Adaptación de pruebas como programas: El protocolo Curry-Howard , Monografías en Ciencias de la Computación, Springer , ISBN 978-0-387-23759-6Este trabajo trata sobre la adaptación de la síntesis de programas basada en pruebas a problemas de desarrollo de programas imperativos y de grano grueso, mediante un método que los autores denominan protocolo Curry-Howard. Incluye un análisis de la correspondencia Curry-Howard desde la perspectiva de la informática.
• de Queiroz, Ruy JGB; de Oliveira, Anjolina (2011), "La interpretación funcional de los cálculos directos", Electronic Notes in Theoretical Computer Science , 269 , Elsevier : 19–40 , doi : 10.1016/j.entcs.2011.03.003(Versión completa de un artículo presentado en LSFA 2010 , Natal, Brasil).

• de Queiroz, Ruy JGB (1994), "Normalización y juegos de lenguaje", Dialectica , 48 (2): 83–123 , doi : 10.1111/j.1746-8361.1994.tb00107.x , JSTOR 42968904 (Versión preliminar presentada en el Logic Colloquium '88 , Padua. Resumen en JSL 55:425, 1990.)
• de Queiroz, Ruy JGB (2001), "Significado, función, propósito, utilidad, consecuencias: conceptos interconectados" , Logic Journal of the Interest Group in Pure and Applied Logics , vol. 9, pp  . 693–734 (Versión preliminar presentada en el Decimocuarto Simposio Internacional Wittgenstein (Celebración del Centenario) celebrado en Kirchberg/Wechsel, del 13 al 20 de agosto de 1989).
• de Queiroz, Ruy JGB (2008), "Sobre reglas de reducción, significado como uso y semántica de la teoría de la demostración", Studia Logica , 90 (2): 211–247 , doi : 10.1007/s11225-008-9150-5 , S2CID 11321602 
• Wadler, Philip (2015), Proposiciones como tipos , Communications of the ACM, 58(12), pp. 75–84.

• De Bruijn, Nicolaas Govert (1995), "Sobre el papel de los tipos en matemáticas" (PDF) , en Groote, Philippe de (ed.), De Groote 1995 , págs  ., la aportación del propio De Bruijn.
• Geuvers, Herman (1995), "El cálculo de construcciones y la lógica de orden superior", De Groote 1995 , pp.  139–191Contiene una introducción sintética a la correspondencia entre Curry y Howard.
• Gallier, Jean H. (1995), "Sobre la correspondencia entre pruebas y términos lambda" (PDF) , De Groote 1995 , pp.  55–138 , archivado del original (PDF) el 5 de julio de 2017.Contiene una introducción sintética a la correspondencia entre Curry y Howard.
• Goldblatt, Robert (2006). "La topología de Grothendieck como modalidad intuicionista" (PDF) . En Gabbay, Dov M.; Woods, John (eds.). Manual de historia de la lógica, vol. 7: Lógica y modalidades en el siglo XX.Ámsterdam: Elsevier. págs. 76–81 . ISBN  978-0-444-51622-0.
• Wadler, Philip (2014), "Proposiciones como tipos" (PDF) , Communications of the ACM , 58 (12): 75–84 , doi : 10.1145/2699407 , S2CID 11957500 

• Coecke, Bob; Kissinger, Aleks (2017). Representación de procesos cuánticos . Cambridge University Press. ISBN 978-1-107-10422-8.
• Kennedy, Juliette; Kossak, Roman, eds. (2011). Teoría de conjuntos, aritmética y fundamentos de las matemáticas: teoremas y filosofías . Cambridge University Press. ISBN 978-1-107-00804-5.
• Baez, John C.; Stay, Mike (2011). "Física, topología, lógica y computación: una piedra Rosetta" (PDF) . En Coecke, Bob (ed.). Nuevas estructuras para la física . Lecture Notes in Physics. Vol.  813. Berlín: Springer. pp. 95–174 . arXiv : 0903.0340 . 
• Casadio, Claudia; Scott, Philip J. (2021). Joachim Lambek: La interacción entre matemáticas, lógica y lingüística . Springer. ISBN 978-3-030-66545-6.
• Lambek, Joachim; Scott, PJ (1989). Introducción a la lógica categórica de orden superior . Cambridge Nueva York Port Chester [etc.]: Cambridge University Press. ISBN 0521356539.
• De Groote, Philippe, ed. (1995), El isomorfismo de Curry-Howard , Cahiers du Centre de Logique (Université catholique de Louvain), vol.  8, Academia-Bruylant, ISBN 978-2-87209-363-2Reproduce los artículos fundamentales de Curry-Feys y Howard, un artículo de de Bruijn y algunos otros.
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Lectures on the Curry–Howard isomorphism , Studies in Logic and the Foundations of Mathematics, vol.  149, Elsevier Science , CiteSeerX 10.1.1.17.7385 , ISBN  978-0-444-52077-7, notas sobre teoría de la demostración y teoría de tipos, que incluye una presentación de la correspondencia de Curry-Howard, con énfasis en la correspondencia de fórmulas como tipos.
• Girard, Jean-Yves (1987–1990), Proof and Types , Cambridge Tracts in Theoretical Computer Science, vol.  7, Traducido por y con apéndices de Lafont, Yves y Taylor, Paul, Cambridge University Press, ISBN 0-521-37181-3Archivado del original el 18 de abril de 2008., notas sobre teoría de la demostración con una presentación de la correspondencia Curry-Howard.
• Thompson, Simon (1991), Teoría de tipos y programación funcional , Addison–Wesley, ISBN 0-201-41667-0
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Adaptación de pruebas como programas: El protocolo Curry-Howard , Monografías en Ciencias de la Computación, Springer , ISBN 978-0-387-23759-6Este trabajo trata sobre la adaptación de la síntesis de programas basada en pruebas a problemas de desarrollo de programas imperativos y de grano grueso, mediante un método que los autores denominan protocolo Curry-Howard. Incluye un análisis de la correspondencia Curry-Howard desde la perspectiva de la informática.
• Binard, F.; Felty, A. (2008), "Programación genética con tipos polimórficos y funciones de orden superior" (PDF) , Actas de la 10.ª conferencia anual sobre computación genética y evolutiva , Association for Computing Machinery, pp. 1187–94 , doi : 10.1145/1389095.1389330 , ISBN  9781605581309, S2CID 3669630 
• de Queiroz, Ruy JGB; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011), La interpretación funcional de la deducción lógica , Advances in Logic, vol.  5, Imperial College Press/World Scientific, ISBN 978-981-4360-95-1