Correspondencia entre Curry y Howard

Isomorfismo entre programas informáticos y demostraciones matemáticas constructivas.

En la teoría del lenguaje de programación y la teoría de la prueba , la correspondencia Curry-Howard (también conocida como isomorfismo o equivalencia de Curry-Howard , o interpretación de pruebas como programas y proposiciones o fórmulas como tipos ) es la relación directa entre programas de computadora. y pruebas matemáticas .

Es una generalización de una analogía sintáctica entre sistemas de lógica formal y cálculos computacionales que fue descubierta por primera vez por el matemático estadounidense Haskell Curry y el lógico William Alvin Howard . ^[1] Es el vínculo entre lógica y computación lo que generalmente se atribuye a Curry y Howard, aunque la idea está relacionada con la interpretación operativa de la lógica intuicionista dada en diversas formulaciones por LEJ Brouwer , Arend Heyting y Andrey Kolmogorov (ver Brouwer-Heyting –Interpretación de Kolmogorov ) ^[2] y Stephen Kleene (ver Realizabilidad ). La relación se ha ampliado para incluir la teoría de categorías como la correspondencia de tres vías Curry-Howard-Lambek . ^{[3] [4] [5]}

Origen, alcance y consecuencias

Los inicios de la correspondencia Curry-Howard se encuentran en varias observaciones:

1. En 1934, Curry observa que los tipos de combinadores podrían verse como esquemas de axiomas para la lógica implicacional intuicionista . ^[6]
2. En 1958 observa que cierto tipo de sistema de prueba , denominado sistemas de deducción al estilo de Hilbert , coincide en algún fragmento con el fragmento tipificado de un modelo estándar de computación conocido como lógica combinatoria . ^[7]
3. En 1969, Howard observa que otro sistema de prueba de "alto nivel" , denominado deducción natural , puede interpretarse directamente en su versión intuicionista como una variante tipificada del modelo de cálculo conocido como cálculo lambda . ^[8]

La correspondencia Curry-Howard es la observación de que existe un isomorfismo entre los sistemas de prueba y los modelos de computación. Es la afirmación de que estas dos familias de formalismos pueden considerarse idénticas.

Si uno hace abstracción de las peculiaridades de cualquiera de los formalismos, surge la siguiente generalización: una prueba es un programa, y ​​la fórmula que demuestra es el tipo del programa . De manera más informal, esto puede verse como una analogía que establece que el tipo de retorno de una función (es decir, el tipo de valores devueltos por una función) es análogo a un teorema lógico, sujeto a hipótesis correspondientes a los tipos de valores de argumento pasados. a la función; y que el programa para calcular esa función es análogo a una demostración de ese teorema. Esto establece una forma de programación lógica sobre una base rigurosa: las pruebas se pueden representar como programas, y especialmente como términos lambda , o se pueden ejecutar pruebas .

La correspondencia ha sido el punto de partida de un amplio espectro de nuevas investigaciones después de su descubrimiento, lo que condujo en particular a una nueva clase de sistemas formales diseñados para actuar como un sistema de prueba y como un lenguaje de programación funcional tipificado . Esto incluye la teoría de tipos intuicionista de Martin-Löf y el Cálculo de construcciones de Coquand , dos cálculos en los que las pruebas son objetos regulares del discurso y en los que se pueden enunciar las propiedades de las pruebas de la misma manera que las de cualquier programa. Este campo de investigación suele denominarse teoría de tipos moderna .

Estos cálculos lambda tipificados derivados del paradigma de Curry-Howard condujeron a software como Coq en el que las pruebas vistas como programas pueden formalizarse, comprobarse y ejecutarse.

Una dirección inversa es utilizar un programa para extraer una prueba , dada su exactitud , un área de investigación estrechamente relacionada con el código portador de pruebas . Esto sólo es factible si el lenguaje de programación para el que está escrito el programa está muy tipificado: el desarrollo de tales sistemas de tipos ha sido motivado en parte por el deseo de hacer que la correspondencia Curry-Howard sea prácticamente relevante.

La correspondencia Curry-Howard también planteó nuevas preguntas sobre el contenido computacional de los conceptos de prueba que no estaban cubiertos por los trabajos originales de Curry y Howard. En particular, se ha demostrado que la lógica clásica corresponde a la capacidad de manipular la continuación de programas y la simetría del cálculo secuencial para expresar la dualidad entre las dos estrategias de evaluación conocidas como llamada por nombre y llamada por valor.

Debido a la posibilidad de escribir programas sin terminación, los modelos de computación completos de Turing (como los lenguajes con funciones recursivas arbitrarias ) deben interpretarse con cuidado, ya que la aplicación ingenua de la correspondencia conduce a una lógica inconsistente. La mejor manera de abordar el cálculo arbitrario desde un punto de vista lógico sigue siendo una cuestión de investigación activamente debatida, pero un enfoque popular se basa en el uso de mónadas para segregar código con terminación demostrable del código potencialmente sin terminación (un enfoque que también se generaliza a códigos mucho más ricos). modelos de computación, ^[9] y está en sí mismo relacionado con la lógica modal por una extensión natural del isomorfismo de Curry-Howard ^{[ext 1]} ). Un enfoque más radical, defendido por la programación funcional total , es eliminar la recursividad sin restricciones (y renunciar a la completitud de Turing , aunque aún conserva una alta complejidad computacional), utilizando una correcursión más controlada dondequiera que realmente se desee un comportamiento no terminante.

formulación general

En su formulación más general, la correspondencia Curry-Howard es una correspondencia entre cálculos de prueba formales y sistemas de tipos para modelos de computación . En particular, se divide en dos correspondencias. Uno en el nivel de fórmulas y tipos que es independiente de qué sistema de prueba o modelo de cálculo particular se considere, y otro en el nivel de pruebas y programas que, esta vez, es específico de la elección particular del sistema de prueba y modelo de cálculo. consideró.

A nivel de fórmulas y tipos, la correspondencia dice que la implicación se comporta igual que un tipo de función, la conjunción como un tipo de "producto" (esto puede llamarse tupla, estructura, lista o algún otro término dependiendo del idioma). ), la disyunción como tipo suma (este tipo puede denominarse unión), la fórmula falsa como tipo vacío y la fórmula verdadera como tipo unidad (cuyo único miembro es el objeto nulo). Los cuantificadores corresponden a espacios funcionales dependientes o productos (según corresponda). Esto se resume en la siguiente tabla:

A nivel de sistemas de prueba y modelos de cálculo, la correspondencia muestra principalmente la identidad de estructura, en primer lugar, entre algunas formulaciones particulares de sistemas conocidas como sistema de deducción estilo Hilbert y lógica combinatoria , y, en segundo lugar, entre algunas formulaciones particulares de sistemas conocidos como sistema de deducción estilo Hilbert y lógica combinatoria . como deducción natural y cálculo lambda .

Entre el sistema de deducción natural y el cálculo lambda existen las siguientes correspondencias:

Sistemas correspondientes

Sistemas de deducción intuicionistas al estilo de Hilbert y lógica combinatoria tipificada

Al principio era 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 lógica combinatoria sorprendentemente correspondían a los respectivos esquemas de axiomas α → ( β → α ) y ( α → ( β → γ )) → (( α → β ) → ( α → γ )) utilizado en los sistemas de deducción estilo Hilbert . Por esta razón, estos esquemas ahora se denominan axiomas K y S. A continuación se dan ejemplos de programas vistos como pruebas 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 δ es derivable de Γ, denotado Γ ⊢ δ, en los siguientes casos:

• δ es una hipótesis, es decir, es una fórmula de Γ,
• δ es un ejemplo de un esquema de axioma; es decir, bajo el sistema de axiomas más común:
  • δ tiene la forma α → ( β → α ), o
  • δ tiene la forma ( α → ( β → γ )) → (( α → β ) → ( α → γ )),
• δ se sigue por deducción, es decir, para algunos α , tanto α → δ como α ya son derivables de Γ (esta es la regla del modus ponens )

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

La lógica combinatoria tipificada se puede formular 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 del combinador 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 dan en la columna derecha a continuación. La observación de Curry simplemente afirma que ambas columnas están en correspondencia uno a uno. La restricción de la correspondencia a la lógica intuicionista significa que algunas tautologías clásicas , como la ley de Peirce (( α → β ) → α ) → α , quedan excluidas de la correspondencia.

Vista a un nivel más abstracto, la correspondencia se puede reformular como se muestra en la siguiente tabla. Especialmente, el teorema de deducción específico de la lógica de estilo Hilbert coincide con el proceso de eliminación de la abstracción de la lógica combinatoria.

Gracias a la correspondencia, los resultados de la lógica combinatoria se pueden transferir a la lógica de estilo Hilbert y viceversa. Por ejemplo, la noción de reducción de términos en lógica combinatoria se puede transferir a la lógica de estilo Hilbert y proporciona una manera de transformar canónicamente pruebas en otras pruebas del mismo enunciado. También se puede transferir la noción de términos normales a una noción de pruebas normales, expresando que las hipótesis de los axiomas nunca necesitan ser completamente separadas (ya que de lo contrario puede ocurrir una simplificación).

Por el contrario, la no demostrabilidad en la lógica intuicionista de la ley de Peirce se puede transferir de nuevo a la lógica combinatoria: no existe ningún término tipificado de lógica combinatoria que se pueda tipificar con tipo.

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

También se pueden transferir los resultados sobre la integridad de algunos conjuntos de combinadores o axiomas. Por ejemplo, el hecho de que el combinador X constituya una base de un solo 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 a la combinación de los esquemas de axiomas

α → ( β → α ) y

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

Deducción natural intuicionista y cálculo lambda mecanografiado

Después de que Curry enfatizara la correspondencia sintáctica entre la deducción intuicionista al estilo de Hilbert y la lógica combinatoria tipificada , Howard hizo explícita en 1969 una analogía sintáctica entre los programas de cálculo lambda simplemente tipificados y las pruebas de deducción natural . A continuación, el lado izquierdo formaliza la deducción natural implicacional intuicionista como un cálculo de secuentes (el uso de secuentes es estándar en las discusiones sobre el isomorfismo de Curry-Howard ya que permite establecer las reglas de deducción de manera más limpia) con debilitamiento implícito y el lado derecho El lado derecho muestra las reglas de escritura 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 nombradas (es decir, escritas) con todos los nombres diferentes.

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

Howard demostró que la correspondencia se extiende a otros conectivos de la lógica y otras construcciones del cálculo lambda simplemente tipificado. Vista a nivel abstracto, la correspondencia se puede resumir como se muestra en la siguiente tabla. Especialmente, 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 que se deduce que los algoritmos para el problema de habitabilidad tipo pueden convertirse en algoritmos para decidir la demostrabilidad intuicionista .

La correspondencia de Howard se extiende naturalmente a otras extensiones de la deducción natural y al cálculo lambda simplemente mecanografiado . Aquí hay 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 en lógica modal y computación por etapas ^{[ext 2]} ${\displaystyle \Box }$
• posibilidad en lógica modal y tipos monádicos para efectos ^{[ext 1]} ${\displaystyle \Diamond }$
• El cálculo λ _I (donde la abstracción está restringida a λx . E donde x tiene al menos una aparición libre en E) y el cálculo CL _I corresponden a la lógica relevante . ^[10]
• La modalidad de verdad local (∇) en la topología de Grothendieck o la modalidad "laxa" equivalente (◯) de Benton, Bierman y de Paiva (1998) corresponden a la lógica CL que describe "tipos de cálculo". ^[11]

Operadores de lógica y control clásicos.

En la época de Curry, y también en la época de Howard, la correspondencia de pruebas como programas se refería sólo a la lógica intuicionista , es decir, a una lógica en la que, en particular, la ley de Peirce no era deducible. La extensión de la correspondencia con la ley de Peirce y, por tanto, con la lógica clásica quedó clara a partir del trabajo de Griffin sobre operadores de tipificación que capturan el contexto de evaluación de la ejecución de un programa determinado para que este contexto de evaluación pueda reinstalarse más adelante. A continuación se proporciona la correspondencia básica estilo Curry-Howard para la lógica clásica. Tenga en cuenta la correspondencia entre la traducción de doble negación utilizada para asignar pruebas clásicas a la lógica intuicionista y la traducción de estilo de paso de continuación utilizada para asignar términos lambda que implican control a términos lambda puros. Más particularmente, las traducciones de estilo de continuación de paso de llamada por nombre se relacionan con la traducción de doble negación de Kolmogorov y las traducciones de estilo de paso de continuación de llamada por valor se relacionan con una especie de traducción de doble negación debida a Kuroda.

Existe una correspondencia Curry-Howard más fina para la lógica clásica si se define la lógica clásica no agregando 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 pruebas como programas con los programas tipificados del cálculo λμ de Parigot .

Cálculo secuencial

Se puede establecer una correspondencia de pruebas como programas para el formalismo conocido como cálculo secuente de Gentzen , pero no es una correspondencia con un modelo de cálculo preexistente bien definido como lo fue para el estilo de Hilbert y las deducciones naturales.

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

Correspondencias relacionadas de pruebas como programas

El papel de De Bruijn

NG de Bruijn utilizó la notación lambda para representar pruebas del verificador de teoremas Automath y representó proposiciones como "categorías" de sus pruebas. Fue 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 declaró la correspondencia de forma independiente (Sørensen y Urzyczyn [1998] 2006, págs. 98-99). Algunos investigadores tienden a utilizar el término correspondencia Curry-Howard-de Bruijn en lugar de correspondencia Curry-Howard.

Interpretación BHK

La interpretación BHK interpreta las pruebas intuicionistas como funciones pero no especifica la clase de funciones relevantes para la interpretación. Si se toma el cálculo lambda para esta clase de función, entonces la interpretación de BHK dice lo mismo que la correspondencia de Howard entre la deducción natural y el cálculo lambda.

Realizabilidad

La realizabilidad recursiva de Kleene divide las pruebas de la aritmética intuicionista en el par de una función recursiva y de una prueba de una fórmula que expresa que la función recursiva "realiza", es decir, instancia correctamente las disyunciones y los cuantificadores existenciales de la fórmula inicial para que la fórmula obtenga verdadero.

La realizabilidad modificada de Kreisel se aplica a la lógica de predicados intuicionista de orden superior y muestra que el término lambda simplemente tipado y 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 (visto como un término lambda sin tipo) 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 (visto como un tipo).

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

Correspondencia Curry-Howard-Lambek

Joachim Lambek demostró a principios de la década de 1970 que las pruebas de la lógica proposicional intuicionista y los combinadores de la lógica combinatoria tipificada comparten una teoría ecuacional común, la teoría de las categorías cerradas cartesianas . La expresión correspondencia Curry-Howard-Lambek es utilizada ahora por algunas personas ^{[ ¿por quién? ]} para referirse a las relaciones entre la lógica intuicionista, el cálculo lambda tipificado y las categorías cerradas cartesianas, interpretando los objetos como tipos o proposiciones y los morfismos como términos o pruebas. La correspondencia de Lambek es una correspondencia de teorías ecuacionales, que se abstrae de dinámicas de cálculo 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 es el caso de cada una de 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 prueba del juicio correspondiente ni en la lógica del estilo de Hilbert ni en la deducción natural. Por ejemplo, no es posible afirmar o demostrar que un morfismo es normalizante, establecer un teorema de tipo Church-Rosser o hablar de una categoría cartesiana cerrada "fuertemente normalizante". Para aclarar esta distinción, a continuación se reformula la estructura sintáctica subyacente de las categorías cerradas cartesianas.

Los objetos (tipos) están definidos por

• ${\displaystyle \top }$es un objeto
• si α y β son objetos, entonces y son objetos. ${\displaystyle \alpha \times \beta }$ ${\displaystyle \alpha \rightarrow \beta }$

Los morfismos (términos) se definen por

• ${\displaystyle id}$, , , y son morfismos ${\displaystyle \star }$ ${\displaystyle \operatorname {eval} }$ ${\displaystyle \pi _{1}}$ ${\displaystyle \pi _{2}}$
• si t es un morfismo, λ t es un morfismo
• si t y u son morfismos, y son morfismos. ${\displaystyle (t,u)}$ ${\displaystyle u\circ t}$

Los morfismos bien definidos (términos tipificados) se definen mediante las siguientes reglas de tipificación (en las que la notación de morfismo categórico habitual se reemplaza por la notación de cálculo secuencial ). ${\displaystyle f:\alpha \to \beta }$ ${\displaystyle f:\!\!-~~\alpha ~\vdash ~\beta }$

Identidad:

${\displaystyle {\frac {}{id:\!\!-~~\alpha ~\vdash ~\alpha }}}$

Composición:

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

Tipo de unidad ( objeto terminal ):

${\displaystyle {\frac {}{\star :\!\!-~~\alpha ~\vdash ~\top }}}$

Producto cartesiano:

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

Proyección izquierda y derecha:

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

Curry :

${\displaystyle {\frac {t:\!\!-~~\alpha \times \beta ~\vdash ~\gamma }{\lambda t:\!\!-~~\alpha ~\vdash ~\beta \rightarrow \gamma }}}$

Solicitud :

${\displaystyle {\frac {}{eval:\!\!-~~(\alpha \rightarrow \beta )\times \alpha ~\vdash ~\beta }}}$

Finalmente, las ecuaciones de la categoría son

• ${\displaystyle id\circ t=t}$
• ${\displaystyle t\circ id=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star =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 eval\circ (\lambda t\circ \pi _{1},\pi _{2})=t}$
• ${\displaystyle \lambda eval=id}$
• ${\displaystyle \lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))}$

Estas ecuaciones implican las siguientes leyes: ${\displaystyle \eta }$

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

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

Ejemplos

Gracias a la correspondencia Curry-Howard, una expresión mecanografiada cuyo tipo corresponde a una fórmula lógica es análoga a una prueba de esa fórmula. Aquí hay ejemplos.

El combinador de identidad visto como una prueba de α → α en la lógica al estilo de Hilbert

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

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

Por lo general, el procedimiento es que siempre que el programa contenga una aplicación de la forma ( P Q ), 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 algunos α y β . Por lo tanto, es posible separar la conclusión, β , mediante la regla del modus ponens.

El combinador de composición visto como una prueba de ( β → α ) → ( γ → β ) → γ → α en la lógica de estilo Hilbert

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

El primer paso es construir ( KS ) . Para hacer 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 usando Modus Ponens:

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

Este es el teorema que corresponde al tipo de ( K S ). Ahora aplica S a esta expresión. Tomando S de la siguiente manera

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

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

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

y luego separe 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 . Especialice K nuevamente, esta vez reemplazando α con ( β → γ ) y β con α :

K  : α → β → α

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

Este es el mismo que el antecedente de la fórmula anterior por lo que desligando el consecuente:

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

Cambiando los nombres de las variables α y γ obtenemos

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

que era lo que quedaba por demostrar.

La prueba normal de ( β → α ) → ( γ → β ) → γ → α en deducción natural vista como un término λ

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) : (β → α) → (γ → β) → γ → α

Otras aplicaciones

Recientemente, el isomorfismo se ha propuesto como una forma de definir la partición del espacio de búsqueda en la programación genética . ^[12] El método indexa conjuntos de genotipos (los árboles de programas desarrollados por el sistema GP) mediante su prueba isomorfa de Curry-Howard (denominada especie).

Como señaló el director de investigación de INRIA, Bernard Lang, ^[13] la correspondencia Curry-Howard constituye un argumento contra la patentabilidad del software: dado que los algoritmos son pruebas matemáticas, la patentabilidad de los primeros implicaría la patentabilidad de los segundos. Un teorema podría ser propiedad privada; un matemático tendría que pagar por usarlo y confiar en la empresa que lo vende, pero mantiene su prueba en secreto y rechaza la responsabilidad por cualquier error.

Generalizaciones

Las correspondencias enumeradas aquí van mucho más allá y son más profundas. Por ejemplo, las categorías cerradas cartesianas se generalizan mediante categorías monoidales cerradas . El lenguaje interno de estas categorías es el sistema de tipos lineales (correspondiente a la lógica lineal ), que generaliza el cálculo lambda de tipo simple como el lenguaje interno de las categorías cerradas cartesianas. Además, se puede demostrar que corresponden a cobordismos , ^[14] que desempeñan un papel vital en la teoría de cuerdas .

También se explora un conjunto ampliado de equivalencias en la teoría de tipos de homotopía , que se convirtió en un área de investigación muy activa alrededor de 2013 y todavía lo ^[update]es en 2018. ^[15] Aquí, la teoría de tipos se amplía mediante el axioma de univalencia ("equivalencia es equivalente a igualdad") que permite que la teoría de tipos de homotopía se utilice como base para todas las matemáticas (incluidas la teoría de conjuntos y la lógica clásica, proporcionando nuevas formas de discutir el axioma de elección y muchas otras cosas). Es decir, la correspondencia Curry-Howard de que las pruebas son elementos de tipos habitados se generaliza a la noción de equivalencia homotópica de pruebas (como caminos en el espacio, el tipo de identidad o el tipo de igualdad de la teoría de tipos se interpreta como un camino). ^[dieciséis]

Referencias

1. La correspondencia se hizo explícita por primera vez en Howard 1980. Véase, por ejemplo, la sección 4.6, p.53 Gert Smolka y Jan Schwinghammer (2007-8), Lecture Notes in Semantics
2. La interpretación de Brouwer-Heyting-Kolmogorov también se denomina 'interpretación de prueba': p. 161 de Juliette Kennedy, Roman Kossak, eds. 2011. Teoría de conjuntos, aritmética y fundamentos de las matemáticas: teoremas, filosofías ISBN  978-1-107-00804-5
3. Casadio, Claudia; Scott, Philip J. (2021). Joachim Lambek: la interacción de las matemáticas, la lógica y la lingüística. Saltador. pag. 184.ISBN​ 978-3-030-66545-6.
4. Coecke, Bob; Kissinger, Aleks (2017). Imaginando procesos cuánticos. Prensa de la Universidad de Cambridge. pag. 82.ISBN​ 978-1-107-10422-8.
5. "Trilogía computacional". nLaboratorio . Consultado el 29 de octubre de 2023 .
6. Curry 1934.
7. Curry y Feys 1958.
8. Howard 1980.
9. Moggi, Eugenio (1991), "Nociones de Computación y Mónadas" (PDF) , Información y Computación , 93 (1): 55–92, doi : 10.1016/0890-5401(91)90052-4
10. Sørenson, Morten; Urzyczyn, Paweł (1998), Conferencias sobre el isomorfismo de Curry-Howard , CiteSeerX 10.1.1.17.7385 
11. Goldblatt, "7.6 Topología de Grothendieck como modalidad intuicionista" (PDF) , Lógica modal matemática: un modelo de su evolución , págs.. La modalidad "laxa" a la que se hace referencia es de 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 
12. F. Binard y A. Felty, "Programación genética con tipos polimórficos y funciones de orden superior". En Actas de la décima conferencia anual sobre Computación genética y evolutiva, páginas 1187 1194, 2008.[1]
13. "Artículo". bat8.inria.fr . Archivado desde el original el 17 de noviembre de 2013 . Consultado el 31 de enero de 2020 .
14. Juan c. Baez y Mike Stay, "Física, topología, lógica y computación: una piedra de Rosetta", (2009) ArXiv 0903.0340 en Nuevas estructuras para la física , ed. Bob Coecke, Apuntes de conferencias de física vol. 813 , Springer, Berlín, 2011, págs. 95-174.
15. "teoría del tipo de homotopía - Tendencias de Google". tendencias.google.com . Consultado el 26 de enero de 2018 .^{[ enlace muerto permanente ]}
16. Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas. (2013) El Programa de Fundaciones Univalentes. Instituto de Estudios Avanzados .

Referencias fundamentales

• Curry, HB (20 de septiembre de 1934). "Funcionalidad en lógica combinatoria". Actas de la Academia Nacional de Ciencias de los Estados Unidos de América . 20 (11): 584–90. Código bibliográfico : 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. Editorial de Holanda Septentrional. LCCN  a59001593; con dos secciones de Craig, William; ver el párrafo 9E{{cite book}}: CS1 maint: postscript (link)
• De Bruijn, Nicolaas (1968), Automath, a language for math , Departamento de Matemáticas, Universidad Tecnológica de Eindhoven, TH-report 68-WSK-05. Reimpreso en forma revisada, con comentarios de dos páginas, en: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970 , Springer Verlag, 1983, págs.
• Howard, William A. (septiembre de 1980) [manuscrito original en papel de 1969], "La noción de construcción de fórmulas como tipos" (PDF) , en Seldin, Jonathan P.; Hindley, J. Roger (eds.), A HB Curry: ensayos sobre lógica combinatoria, cálculo lambda y formalismo , Academic Press , págs. 479–490, ISBN 978-0-12-349050-6.

Extensiones de la correspondencia

1. Pfenning, Frank; Davies, Rowan (2001), "Una reconstrucción crítica de la lógica modal" (PDF) , Estructuras matemáticas en informática , 11 (4): 511–540, CiteSeerX 10.1.1.43.1611 , doi :10.1017/S0960129501003322, S2CID  16467268 
2. Davies, serbal; Pfenning, Frank (2001), "Un 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 

• Griffin, Timothy G. (1990), "La noción de control de fórmulas como tipos", Conf. Récord del 17º Simposio Anual de ACM. sobre Principios de lenguajes de programación, POPL '90, San Francisco, CA, EE. UU., 17 a 19 de enero de 1990 , págs. 47 a 57, doi :10.1145/96709.96714, ISBN 978-0-89791-343-0, S2CID  3005134.
• Parigot, Michel (1992), "Lambda-mu-calculus: Una interpretación algorítmica de la deducción natural clásica", Conferencia internacional sobre programación lógica y razonamiento automatizado: Actas LPAR '92, San Petersburgo, Rusia , Lecture Notes in Computer Science, vol . 624, Springer-Verlag , págs. 190-201, ISBN 978-3-540-55727-2.
• Herbelin, Hugo (1995), "Una estructura de cálculo lambda isomorfa a la estructura de cálculo secuencial estilo Gentzen", en Pacholski, Leszek; Tiuryn, Jerzy (eds.), Computer Science Logic, octavo taller internacional, CSL '94, Kazimierz, Polonia, 25 al 30 de septiembre de 1994, artículos seleccionados , Lecture Notes in Computer Science, vol. 933, Springer-Verlag , págs. 61–75, ISBN 978-3-540-60017-6.
• Gabbay, Dov; de Queiroz, Ruy (1992). "Ampliación de la interpretación de Curry-Howard a lógicas lineales, relevantes y de otros recursos". Revista de Lógica Simbólica . vol. 57. Asociación de Lógica Simbólica. págs. 1319-1365. doi :10.2307/2275370. JSTOR  2275370. S2CID  7159005.. (Versión completa del artículo presentado en 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, págs. 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ógica pura y aplicada , vol. 3, págs. 243–290. (Versión completa de un artículo presentado en Logic Colloquium '91 , Uppsala. Resumen en JSL 58(2):753–754, 1993.)
• de Queiroz, Ruy; Gabbay, Dov (1997), "The Functional Interpretation of Modal Necessity", en de Rijke, Maarten (ed.), Advances in Intensional Logic , Applied Logic Series, vol. 7, Springer-Verlag , págs. 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 a Dov Gabbay , Trends in Logic, vol. 7, Kluwer, págs. 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 deducción natural etiquetada", Revista de lógica del grupo de interés en lógica pura y aplicada , vol. 7, Oxford University Press , págs. 173-215. (Versión completa de un artículo presentado en 2nd WoLLIC'95 , Recife. Resumen en Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Poérnomo, Imán; Crossley, Juan; Wiring; Martin (2005), Adaptación de pruebas como programas: el protocolo Curry-Howard , Monografías de informática, Springer , ISBN 978-0-387-23759-6, se refiere a la adaptación de la síntesis de programas de pruebas como programas a problemas de desarrollo de programas imperativos y de grano grueso, a través de un método que los autores llaman protocolo Curry-Howard. Incluye una discusión de la correspondencia Curry-Howard desde una perspectiva de las Ciencias de la Computación.
• de Queiroz, Ruy JGB; de Oliveira, Anjolina (2011), "La interpretación funcional de los cálculos directos", Notas electrónicas en informática teórica , 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).

Interpretaciones filosóficas

• de Queiroz, Ruy JGB (1994), "Normalización y juegos de lenguaje", Dialectica , vol. 48, págs. 83-123^{[ enlace muerto permanente ]} . (Versión inicial presentada en Logic Colloquium '88 , Padua. Resumen en JSL 55:425, 1990.)
• de Queiroz, Ruy JGB (2001), "Significado, función, propósito, utilidad, consecuencias – conceptos interconectados", Revista de Lógica del Grupo de Interés en Lógica Pura y Aplicada , vol. 9, págs. 693–734. (Versión inicial 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 las reglas de reducción, el significado como uso y la semántica de la teoría de la prueba", Studia Logica , 90 (2): 211–247, doi :10.1007/s11225-008-9150-5 , S2CID  11321602.

Papeles sintéticos

• 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 las construcciones y la lógica de orden superior", De Groote 1995, págs. 139-191, contiene una introducción sintética a la correspondencia Curry-Howard.
• Gallier, Jean H. (1995), "Sobre la correspondencia entre pruebas y términos Lambda" (PDF) , De Groote 1995, págs., contiene una introducción sintética a la correspondencia Curry-Howard.
• Wadler, Philip (2014), "Proposiciones como tipos" (PDF) , Comunicaciones de la ACM , 58 (12): 75–84, doi :10.1145/2699407, S2CID  11957500

Libros

• 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-2, reproduce los artículos fundamentales de Curry-Feys y Howard, un artículo de De Bruijn y algunos otros artículos.
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Conferencias sobre el isomorfismo de Curry-Howard , Estudios de lógica y fundamentos de las matemáticas, vol. 149, Ciencia Elsevier , CiteSeerX  10.1.1.17.7385 , ISBN 978-0-444-52077-7, notas sobre teoría de la prueba y teoría de tipos, que incluye una presentación de la correspondencia Curry-Howard, con especial atención a la correspondencia de fórmulas como tipos.
• Girard, Jean-Yves (1987–1990), Pruebas y tipos, Cambridge Tracts in Theoretical Computer Science, vol. 7, traducido y con apéndices de Lafont, Yves y Taylor, Paul, Cambridge University Press, ISBN 0-521-37181-3, archivado desde el original el 2008-04-18, notas sobre la teoría de la prueba 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.
• Poérnomo, Imán; Crossley, Juan; Wiring; Martin (2005), Adaptación de pruebas como programas: el protocolo Curry-Howard , Monografías de informática, Springer , ISBN 978-0-387-23759-6, se refiere a la adaptación de la síntesis de programas de pruebas como programas a problemas de desarrollo de programas imperativos y de grano grueso, a través de un método que los autores llaman protocolo Curry-Howard. Incluye una discusión de la correspondencia Curry-Howard desde una perspectiva de las Ciencias de la Computación.
• Binard, F.; Felty, A. (2008), "Programación genética con tipos polimórficos y funciones de orden superior" (PDF) , Actas de la décima conferencia anual sobre computación genética y evolutiva , Association for Computing Machinery, págs. 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, Avances en lógica, vol. 5, Imperial College Press/World Scientific, ISBN 978-981-4360-95-1.

Otras lecturas

• Johnstone, PT (2002), "D4.2 λ-Cálculo y categorías cerradas cartesianas", Sketches of an Elephant, A Topos Theory Compendium, vol. 2, Clarendon Press, págs. 951–962, ISBN 978-0-19-851598-2- ofrece una visión categórica de "lo que sucede" en la correspondencia Curry-Howard.

enlaces externos

• Howard sobre Curry-Howard
• La correspondencia Curry-Howard en Haskell
• The Monad Reader 6: Aventuras en la tierra clásica: Curry-Howard en Haskell, la ley de Pierce.