Correspondencia entre Curry y Howard

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

En la teoría de lenguajes de programación y teoría de pruebas , la correspondencia de Curry-Howard es la relación directa entre los programas informáticos y las pruebas matemáticas . También se la conoce como isomorfismo o equivalencia de Curry-Howard , o interpretación de las pruebas como programas y de las proposiciones o fórmulas como tipos .

Se trata de 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 el que usualmente se atribuye a Curry y Howard, aunque la idea está relacionada con la interpretación operacional de la lógica intuicionista dada en varias formulaciones por LEJ Brouwer , Arend Heyting y Andrey Kolmogorov (ver Interpretación de Brouwer–Heyting–Kolmogorov ) ^[2] y Stephen Kleene (ver Realizabilidad ). La relación se ha extendido 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 axiomáticos para la lógica implicacional intuicionista . ^[6]
2. En 1958 observa que un cierto tipo de sistema de prueba , conocido como sistemas de deducción de estilo 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 "nivel más alto" , conocido como deducción natural , puede interpretarse directamente en su versión intuicionista como una variante tipificada del modelo de computación conocido como cálculo lambda . ^[8]

La correspondencia Curry-Howard es la observación de que existe un isomorfismo entre los sistemas de demostración 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 cada formalismo, surge la siguiente generalización: una prueba es un programa, y ​​la fórmula que prueba es el tipo para el programa . Más informalmente, 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 los valores de los argumentos pasados ​​a la función; y que el programa para calcular esa función es análogo a una prueba de ese teorema. Esto establece una forma de programación lógica sobre una base rigurosa: las pruebas pueden representarse como programas, y especialmente como términos lambda , o las pruebas pueden ejecutarse .

La correspondencia ha sido el punto de partida de un amplio espectro de nuevas investigaciones tras su descubrimiento, que han conducido en particular a una nueva clase de sistemas formales diseñados para actuar tanto como un sistema de pruebas como un lenguaje de programación funcional tipado . 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 en el caso de cualquier programa. Este campo de investigación suele denominarse teoría de tipos moderna .

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

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

La correspondencia Curry-Howard también planteó nuevas preguntas sobre el contenido computacional de los conceptos de prueba que no estaban contempladas en los trabajos originales de Curry y Howard. En particular, se ha demostrado que la lógica clásica se corresponde con la capacidad de manipular la continuación de los 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 no terminantes, los modelos de computación Turing-completos (como 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 tratar la computación arbitraria desde un punto de vista lógico es todavía una cuestión de investigación debatida activamente, pero un enfoque popular se basa en el uso de mónadas para segregar el código demostrablemente terminante del código potencialmente no terminante (un enfoque que también se generaliza a modelos de computación mucho más ricos, ^[9] y está 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 recursión sin restricciones (y renunciar a la completitud de Turing , aunque aún se conserva una alta complejidad computacional), utilizando una correcursión más controlada donde sea 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: una a nivel de fórmulas y tipos que es independiente de qué sistema de prueba o modelo de computación en particular se considera, y otra a nivel de pruebas y programas que, esta vez, es específica de la elección particular del sistema de prueba y modelo de computación considerados.

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 "producto" (esto puede llamarse una tupla, una estructura, una lista o algún otro término dependiendo del lenguaje), la disyunción como un tipo de suma (este tipo puede llamarse una unión), la fórmula falsa como el tipo vacío y la fórmula verdadera como el tipo de unidad (cuyo único miembro es el objeto nulo). Los cuantificadores corresponden al espacio de funciones dependientes o productos (según corresponda). Esto se resume en la siguiente tabla:

A nivel de sistemas de prueba y modelos de cálculos, la correspondencia muestra principalmente la identidad de estructura, en primer lugar, entre algunas formulaciones particulares de sistemas conocidos como sistema de deducción de estilo Hilbert y lógica combinatoria , y, en segundo lugar, entre algunas formulaciones particulares de sistemas conocidos 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 de estilo Hilbert y lógica combinatoria tipificada

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

Si nos limitamos al fragmento intuicionista implicacional, una manera 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 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 sigue por deducción, es decir, para algún α , 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 de 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 de la derecha a continuación. La observación de Curry simplemente establece 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 (( α → β ) → α ) → α , están excluidas de la correspondencia.

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

Gracias a la correspondencia, los resultados de la lógica combinatoria pueden transferirse a la lógica de estilo Hilbert y viceversa. Por ejemplo, la noción de reducción de términos en la lógica combinatoria puede transferirse a la lógica de estilo Hilbert y proporciona una manera de transformar canónicamente las demostraciones en otras demostraciones del mismo enunciado. 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 todas 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 hay ningún término tipificado de la lógica combinatoria que sea tipificable con el tipo

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

Los resultados sobre la completitud de algunos conjuntos de combinadores o axiomas también pueden transferirse. 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 a la combinación de los esquemas axiomáticos

α → ( β → α ) y

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

Deducción natural intuicionista y cálculo lambda tipificado

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 tipificado 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 del isomorfismo Curry-Howard ya que permite que las reglas de deducción se establezcan de manera más clara) con debilitamiento implícito y el lado derecho muestra las reglas de tipificación 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, tipificadas) 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 sin restricciones, la regla →  I corresponde a la abstracción de la función y la regla →  E corresponde a la aplicación de la función. Obsérvese que la correspondencia no es exacta si el contexto Γ se toma como un conjunto de fórmulas como, por ejemplo, los λ-términos λ x . λ y . x y λ x . λ y . y del 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 de tipos simples. Vista a un nivel abstracto, la correspondencia puede entonces 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 Prawitz de deducción normal en la deducción natural , de lo que se deduce que los algoritmos para el problema de habitabilidad de tipos 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 del cálculo lambda de tipos simples . A continuación se ofrece 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 ocurrencia 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 de Howard, la correspondencia de las pruebas como programas sólo concernía 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 la correspondencia a la ley de Peirce y, por lo tanto, a la lógica clásica se hizo evidente a partir del trabajo de Griffin sobre los operadores de tipificación que capturan el contexto de evaluación de una ejecución de programa dada, de modo que este contexto de evaluación pueda reinstalarse más tarde. A continuación se muestra la correspondencia básica de estilo Curry-Howard para la lógica clásica. 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 estilo de paso de continuación utilizada para mapear los términos lambda que involucran control a términos lambda puros. Más particularmente, las traducciones de estilo de paso de continuación 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 un tipo de traducción de doble negación debido 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 añadiendo 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 secuencial de Gentzen , pero no es una correspondencia con un modelo de computación preexistente bien definido como lo fue para las deducciones naturales y de estilo Hilbert.

El cálculo secuencial se caracteriza por la presencia de reglas de introducción por la izquierda, reglas de introducción por la derecha y una regla de corte que puede eliminarse. La estructura del cálculo secuencial 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 entre pruebas como programas

El papel de De Bruijn

NG de Bruijn utilizó la notación lambda para representar las pruebas del verificador de teoremas Automath y representó las proposiciones como "categorías" de sus pruebas. Fue a fines de la década de 1960, en el mismo período en que Howard escribió su manuscrito; de Bruijn probablemente desconocía el trabajo de Howard y enunció la correspondencia de forma independiente (Sørensen & Urzyczyn [1998] 2006, pp 98-99). Algunos investigadores tienden a utilizar el término correspondencia Curry-Howard-de Bruijn en lugar de correspondencia Curry-Howard.

Interpretación de BHK

La interpretación de BHK interpreta las demostraciones 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 funciones, 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 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 muestra que el término lambda simplemente tipificado 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 (vista como un término lambda no tipificado) 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 (vista como un tipo).

La interpretación dialéctica de Gödel realiza una (extensión de) aritmética intuicionista con funciones computables. La conexió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 los años 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 cartesianas cerradas . 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 cartesianas cerradas. Bajo 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 suposiciones ( contexto de tipificación ) a un consecuente válido (término bien tipificado). ^[12]

La correspondencia de Lambek es una correspondencia de teorías ecuacionales, que se abstrae de dinámicas de 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 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 en la lógica de estilo Hilbert o en la deducción natural. Por ejemplo, no es posible afirmar o probar que un morfismo es normalizador, establecer un teorema de tipo Church-Rosser o 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 un objeto
• dados y como objetos, entonces y como objetos. ${\displaystyle \alpha }$ ${\displaystyle \beta }$ ${\displaystyle \alpha \times \beta }$ ${\displaystyle \alpha \rightarrow \beta }$

Los morfismos (deducciones/términos) incluyen

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

De manera equivalente a las anotaciones anteriores, se pueden construir morfismos bien definidos (términos tipificados) en cualquier categoría cartesiana cerrada según las siguientes reglas de tipificación . La notación de morfismos categóricos habitual se reemplaza por la notación de contexto de tipificación . ${\displaystyle f:\alpha \to \beta }$ ${\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 :\top }}}$

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 las siguientes leyes: ${\displaystyle \eta }$

• ${\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 t tal que si y solo si es demostrable en la lógica intuicionista implicacional. ${\displaystyle \alpha _{1}\times \ldots \times \alpha _{n}\vdash t:\beta }$ ${\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta }$

Ejemplos

Gracias a la correspondencia Curry-Howard, una expresión tipificada cuyo tipo corresponde a una fórmula lógica es análoga a una demostración de esa fórmula. A continuación se ofrecen algunos ejemplos.

El combinador de identidad visto como una prueba dealfa→alfaen lógica de estilo Hilbert

Como ejemplo, considere una prueba 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 prueba, esto dice que se pueden usar los siguientes pasos para demostrar α → α :

• instanciar el segundo esquema de axioma con las fórmulas α , β → α y α para obtener una prueba de ( α → (( β → α ) → α )) → (( α → ( β → α )) → ( α → α ) ) ,
• instanciar 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 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. Como 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 deducir la conclusión, β , mediante la regla del modus ponens.

El combinador de composición visto como una prueba de (β→alfa) → (gamma→β) →gamma→alfaen 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 ( K S ). Para que el antecedente del axioma K se parezca al axioma S , iguale α a ( α → β → γ ) → ( α → β ) → α → γ , y β a δ (para evitar colisiones entre 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 apliquemos 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. Especialice 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  : ( β → γ ) → ( α → β ) → α → γ

Cambiando los nombres de las variables α y γ obtenemos

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

que era lo que quedaba por demostrar.

La prueba normal de (β→alfa) → (gamma→β) →gamma→alfaEn la deducción natural se considera 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, se ha propuesto el isomorfismo como una forma de definir la partición del espacio de búsqueda en la programación genética . ^[13] El método indexa conjuntos de genotipos (los árboles de programa desarrollados por el sistema GP) por su prueba isomórfica de Curry-Howard (a la que se hace referencia como especie).

Como señala el director de investigación del INRIA , Bernard Lang ^[14] , 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 en secreto sus pruebas y rechaza la responsabilidad por cualquier error.

Generalizaciones

Las correspondencias que se enumeran 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 (que corresponde a la lógica lineal ), que generaliza el cálculo lambda de tipos simples como el lenguaje interno de las categorías cerradas cartesianas. Además, se puede demostrar que estas corresponden a cobordismos ^[15] , que desempeñan un papel vital en la teoría de cuerdas .

También se explora un conjunto extendido de equivalencias en la teoría de tipos de homotopía . Aquí, la teoría de tipos se extiende mediante el axioma de univalencia ("equivalencia es equivalente a igualdad") que permite que la teoría de tipos de homotopía se use como base para todas las matemáticas (incluida 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 de 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 identidad o el tipo igualdad de la teoría de tipos se interpreta como un camino). ^[16]

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 la 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. Springer. pág. 184. ISBN 978-3-030-66545-6.
4. Coecke, Bob; Kissinger, Aleks (2017). Representación de procesos cuánticos. Cambridge University Press. pág. 82. ISBN 978-1-107-10422-8.
5. "Trilogía computacional". nLab . 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. 76-81La 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. Lambek, Joachim; Scott, PJ (1989). Introducción a la lógica categórica de orden superior . Cambridge New York Port Chester [etc.]: Cambridge University Press. ISBN 0521356539.
13. F. Binard y A. Felty, "Programación genética con tipos polimórficos y funciones de orden superior". En Actas de la 10.ª conferencia anual sobre computación genética y evolutiva, páginas 1187-1194, 2008.[1]
14. "Artículo". bat8.inria.fr . Archivado desde el original el 17 de noviembre de 2013 . Consultado el 31 de enero de 2020 .
15. John c. Baez y Mike Stay, "Física, topología, lógica y computación: una piedra de Rosetta", (2009) ArXiv 0903.0340 en New Structures for Physics , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlín, 2011, págs. 95-174.
16. Teoría de tipos de homotopía: Fundamentos univalentes de las matemáticas. (2013) Programa de Fundamentos univalentes. Instituto de Estudios Avanzados .

Referencias seminales

• 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. 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.). Combinatory Logic . Studies in Logic and the Foundations of Mathematics. Vol. 1. North-Holland Publishing Company. LCCN  a59001593; con dos secciones de Craig, William; véase el párrafo 9E{{cite book}}: CS1 maint: postscript (link)
• De Bruijn, Nicolaas (1968), Automath, a language for mathematics , Departamento de Matemáticas, Universidad Tecnológica de Eindhoven, TH-report 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 de 1969], "La noción de construcción de fórmulas como tipos" (PDF) , en Seldin, Jonathan P.; Hindley, J. Roger (eds.), Para HB Curry: Ensayos sobre lógica combinatoria, cálculo lambda y formalismo , Academic Press , págs. 479–490, ISBN 978-0-12-349050-6.

Ampliaciones 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, Rowan; Pfenning, Frank (2001), "Un análisis modal de 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 las fórmulas como tipos", Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, 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, S2CID3005134 ​.
• Parigot, Michel (1992), "Lambda-mu-calculus: An algorithmic interpret of classic natural deduction", Conferencia internacional sobre programación lógica y razonamiento automatizado: LPAR '92 Proceedings, 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 de estilo Gentzen", en Pacholski, Leszek; Tiuryn, Jerzy (eds.), Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Polonia, 25-30 de septiembre de 1994, Selected Papers , Lecture Notes in Computer Science, vol. 933, Springer-Verlag , pp. 61-75, ISBN 978-3-540-60017-6.
• Gabbay, Dov; de Queiroz, Ruy (1992). "Extendiendo la interpretación de Curry-Howard a lógicas lineales, relevantes y de otros recursos". Journal of Symbolic Logic . Vol. 57. Association for Symbolic Logic. págs. 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, 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 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.), 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), "Labeled Natural Deduction", en Ohlbach, Hans-Juergen; Reyle, Uwe (eds.), Logic, Language and Reasoning. 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 la deducción natural etiquetada", Logic Journal of the Interest Group in Pure and Applied Logics , vol. 7, Oxford University Press , págs. 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 informática, Springer , ISBN 978-0-387-23759-6, trata de la adaptación de la síntesis de programas de pruebas como programas 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 una 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.)

Interpretaciones filosóficas

• 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 temprana presentada en el Coloquio de Lógica '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, pp. 693–734(Versión preliminar presentada en el Decimocuarto Simposio Internacional de 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 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 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, pp. 55–138 , archivado desde el original (PDF) el 5 de julio de 2017, contiene una introducción sintética a la correspondencia Curry-Howard.
• Wadler, Philip (2014), "Proposiciones como tipos" (PDF) , Communications of the 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 seminales de Curry-Feys y Howard, un artículo de de Bruijn y algunos otros.
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Lecciones sobre el isomorfismo de Curry-Howard , Estudios de lógica y fundamentos de las matemáticas, vol. 149, Elsevier Science , CiteSeerX  10.1.1.17.7385 , ISBN 978-0-444-52077-7, notas sobre teoría de pruebas y teoría de tipos, que incluye una presentación de la correspondencia Curry-Howard, con un enfoque en la correspondencia de fórmulas como tipos
• Girard, Jean-Yves (1987–1990), Prueba y tipos, 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-3, archivado desde el original el 18 de abril de 2008, 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.
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Adaptación de pruebas como programas: el protocolo Curry-Howard , Monografías en informática, Springer , ISBN 978-0-387-23759-6, trata de la adaptación de la síntesis de programas de pruebas como programas 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 una 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, págs. 1187–94, doi :10.1145/1389095.1389330, ISBN 9781605581309, Número de identificación del sujeto  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.

Lectura adicional

• Johnstone, PT (2002), "D4.2 Cálculo λ y categorías cartesianas cerradas", 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
• El lector de mónadas 6: Aventuras en la tierra clásica: Curry–Howard en Haskell, la ley de Pierce.