Correspondencia Curry-Howard

En la teoría del lenguaje de programación y la teoría de la prueba, la correspondencia de Curry-Howard (también conocida como isomorfismo de Curry-Howard o equivalencia, o las pruebas-como-programas y proposiciones- o interpretación de fórmulas-como-tipos) es la relación directa entre los programas de ordenador y las 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. Es el vínculo entre la lógica y la 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 varias formulaciones por L. E. J. Brouwer, Arend Heyting y Andrey Kolmogorov (ver interpretación de Brouwer-Heyting-Kolmogorov) 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 de Curry-Howard-Lambek.

Origen, alcance y consecuencias

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

1. En 1934 Curry observa que los tipos de los combinadores podrían verse como esquemas axiom para la lógica intuitionista implicacional.
2. En 1958 observa que un cierto tipo de sistema de prueba, denominado como sistemas de deducción de estilo Hilbert, coincide en algún fragmento con el fragmento tipo de un modelo estándar de computación conocido como lógica combinatoria.
3. En 1969 Howard observa que otro sistema de pruebas más "alto nivel", denominado deducción natural, puede ser interpretado directamente en su versión intuitionista como una variante tipoada del modelo de cálculo conocido como cálculo de lambda.

La correspondencia de 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 como idénticas.

Si uno se abstrae de las peculiaridades de cualquiera de los dos formalismos, surge la siguiente generalización: una prueba es un programa, y la fórmula que prueba es el tipo del programa. De manera más informal, esto puede verse como una analogía que establece que el tipo de devolución 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 prueba 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 las pruebas se pueden ejecutar.

La correspondencia ha sido el punto de partida de un amplio espectro de nuevas investigaciones después de su descubrimiento, 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 tipado. Esto incluye la teoría intuicionista de tipos 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 establecer 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 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 usar un programa para extraer una prueba, dada su corrección, un área de investigación estrechamente relacionada con el código portador de prueba. Esto solo es factible si el lenguaje de programación para el que está escrito el programa tiene muchos tipos: el desarrollo de tales sistemas de tipos ha sido motivado en parte por el deseo de hacer que la correspondencia de 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 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 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.

De manera especulativa, se podría esperar que la correspondencia Curry-Howard conduzca a una unificación sustancial entre la lógica matemática y la informática fundamental:

La lógica al estilo de Hilbert y la deducción natural no son más que dos tipos de sistemas de prueba entre una gran familia de formalismos. Las sintaxis alternativas incluyen cálculo secuencial, redes de prueba, cálculo de estructuras, etc. Si se admite la correspondencia de Curry-Howard como el principio general de que cualquier sistema de prueba oculta un modelo de cálculo, una teoría de la estructura computacional no tipificada subyacente de este tipo de prueba El sistema debe ser posible. Entonces, una pregunta natural es si se puede decir algo matemáticamente interesante sobre estos cálculos computacionales subyacentes.

Por el contrario, la lógica combinatoria y el cálculo lambda de tipo simple tampoco son los únicos modelos de computación. La lógica lineal de Girard se desarrolló a partir del análisis fino del uso de recursos en algunos modelos de cálculo lambda; ¿Hay una versión mecanografiada de la máquina de Turing que se comportaría como un sistema de prueba? Los lenguajes ensambladores tipificados son una instancia de "nivel bajo" modelos de computación que portan tipos.

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 lidiar con el cómputo arbitrario desde un punto de vista lógico sigue siendo una pregunta de investigación que se debate activamente, pero un enfoque popular se basa en el uso de mónadas para segregar el código comprobable que termina del código que potencialmente no termina (un enfoque que también se generaliza a códigos mucho más ricos). modelos de computación, y está relacionado con la lógica modal por una extensión natural del isomorfismo de Curry-Howard). Un enfoque más radical, defendido por la programación funcional total, es eliminar la recursividad sin restricciones (y renunciar a la integridad de Turing, aunque aún conserva una alta complejidad computacional), utilizando una correcursión más controlada donde sea que realmente se desee un comportamiento sin terminación.

Formulación general

En su formulación más general, la correspondencia de Curry-Howard es una correspondencia entre cálculos de prueba formales y sistemas tipo para modelos de computación. En particular, se divide en dos correspondencias. Uno a nivel de fórmulas y tipos que es independiente de qué sistema de prueba o modelo de cálculo en particular se considere, y otro a nivel de pruebas y programas que, esta vez, es específico para la elección particular de 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 una función tipo, la conjunción como un "producto" tipo (esto puede llamarse tupla, estructura, lista o algún otro término dependiendo del idioma), disyunción como tipo suma (este tipo puede llamarse unión), la fórmula falsa como tipo vacío y la fórmula verdadera fórmula como el tipo de unidad (cuyo único miembro es el objeto nulo). Los cuantificadores corresponden al espacio de función dependiente o productos (según corresponda). Esto se resume en la siguiente tabla:

A nivel de sistemas de prueba y modelos de computación, la correspondencia muestra principalmente la identidad de estructura, primero, entre algunas formulaciones particulares de sistemas conocidos como sistema de deducción estilo Hilbert y lógica combinatoria, y, segundo, 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 intuitivos al estilo de Hilbert y lógica combinatoria tipificada

Al principio, era una simple observación en el libro de 1958 de Curry y Feys 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 Hilbert- sistemas de deducción de estilo. Por esta razón, estos esquemas ahora a menudo 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 uno se restringe 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 flexión,
• δ es una instancia de un esquema de axioma; es decir, bajo el sistema de axioma más común:
  • δ tiene la forma α →β → α), o
  • δ tiene la forma (α →β → γ) → (α → β) →α → γ)),
• δ follows by deduction, i.e., for some α, ambos α → δ y α ya son derivados de Dimension (esta es la regla de modus ponens)

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

La lógica combinatoria tipada se puede formular usando 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 Dimension,
• T es un combinador básico; es decir, bajo la base de combinación más común:
  • T es K:α →β → α[donde] α y β denota los tipos de sus argumentos], o
  • T es S:(α →β → γ) → (α → β) →α → γ)),
• T es la composición de dos subtérminos que dependen de las variables en Dimension.

Las reglas de generación definidas aquí se proporcionan en la columna de la derecha a continuación. El comentario 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 ((α → β) → α) → α, quedan excluidos de la correspondencia.

Lógica intuitiva al estilo Hilbert	Tipo de lógica combinatoria
α α ▪ ▪ .. .. ⊢ ⊢ α α Assum{displaystyle {frac {alpha in Gamma }{Gamma vdash alpha }qquad qquad {text{Assum}}}	x:α α ▪ ▪ .. .. ⊢ ⊢ x:α α {displaystyle {frac {x:alpha in Gamma }{Gamma vdash x:alpha }
.. ⊢ ⊢ α α → → ()β β → → α α )AxK{displaystyle {frac {}{Gamma vdash alpha rightarrow (beta rightarrow alpha)}}qquad {text{Ax}_{K}}	.. ⊢ ⊢ K:α α → → ()β β → → α α ){displaystyle {frac {}{Gamma vdash K:alpha rightarrow (beta rightarrow alpha)}}}}}
.. ⊢ ⊢ ()α α → → ()β β → → γ γ ))→ → ()()α α → → β β )→ → ()α α → → γ γ ))AxS{displaystyle {frac {}{Gamma vdash (alpha !rightarrow !(beta !rightarrow !gamma)!derecha !(alpha !derecha !beta)!derecha !(alpha !gamma)};{text\\]}\\\\]}\\\\\\]\\]\\\\]\\\]\]\\\\\]]\\\\\\\\\\]\\\\\\\\\\\\]\\\]]\]\\\\\\\]\\\\\\\\]\\	.. ⊢ ⊢ S:()α α → → ()β β → → γ γ ))→ → ()()α α → → β β )→ → ()α α → → γ γ )){displaystyle {frac {}{Gamma vdash S:(alpha !rightarrow !(beta !rightarrow !gamma))!derecho !(alpha !derecha !beta)!derechilla !alpha !gamma)}}}}}}}} {
.. ⊢ ⊢ α α → → β β .. ⊢ ⊢ α α .. ⊢ ⊢ β β Modus Ponens{displaystyle {frac {Gamma vdash alpha rightarrow beta qquad Gamma vdash alpha } {text{Modus Ponens}}	.. ⊢ ⊢ E1:α α → → β β .. ⊢ ⊢ E2:α α .. ⊢ ⊢ E1E2:β β {displaystyle {frac {Gammavdash E_{1}:alpha rightarrow beta qquad Gamma vdash E_{2}:alpha }{Gamma vdash E_{1};E_{2}:beta }

Visto en 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 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 la lógica combinatoria se puede transferir a la lógica al estilo de Hilbert y proporciona una forma de transformar canónicamente las pruebas en otras pruebas del mismo enunciado. También se puede trasladar la noción de términos normales a una noción de pruebas normales, expresando que las hipótesis de los axiomas nunca necesitan estar del todo 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 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 lógica combinatoria (extensional) implica que el esquema de axioma único

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

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

α →β → α) y

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

Deducción natural intuitiva 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 tipeada, Howard hizo explícita en 1969 una analogía sintáctica entre los programas de cálculo lambda simplemente tipeado 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 secuencias (el uso de secuencias es estándar en las discusiones sobre el isomorfismo de Curry-Howard, ya que permite que las reglas de deducción se establezcan de manera más clara) con debilitamiento implícito y la derecha -lado de la mano muestra las reglas de escritura del cálculo lambda. En el lado izquierdo, Γ, Γ₁ y Γ₂ indican secuencias ordenadas de fórmulas, mientras que en el lado derecho indican secuencias de fórmulas nombradas (es decir, escritas).) fórmulas con todos los nombres diferentes.

Deducción natural intuitiva	Reglas de asignación de tipo Lambda
.. 1,α α ,.. 2⊢ ⊢ α α Ax{displaystyle {frac {fnMicrosoft Sans Serif} Gamma _{2}vdash alpha } {text{Ax}}	.. 1,x:α α ,.. 2⊢ ⊢ x:α α {fnMicroc {fnK} {fnMicrosoft} {fnMicrosoft}} {fnMicroc} {fnMicroc}} {fnMicrosoft}} {fnMicrosoft} {fn}} {fnMicroc}} {fnMicroc}}} {f}}}}}} {f}}}}}} {f}}}}}}}}}}}}}}}}}}}}}}}}}} { Gamma - ¿Qué? Gamma _{2}vdash x:alpha }
.. ,α α ⊢ ⊢ β β .. ⊢ ⊢ α α → → β β → → I{displaystyle {frac {Gammaalpha vdash beta }{Gamma vdash alpha rightarrow beta ♪♪ Yo...	.. ,x:α α ⊢ ⊢ t:β β .. ⊢ ⊢ ()λ λ x:α α .t):α α → → β β {displaystyle {frac {Gammax:alpha vdash t:beta }{Gamma vdash (lambda x!:!alpha.~t):alpha rightarrow beta }
.. ⊢ ⊢ α α → → β β .. ⊢ ⊢ α α .. ⊢ ⊢ β β → → E{displaystyle {frac {Gamma vdash alpha rightarrow beta qquad Gamma vdash alpha }{Gamma vdash beta ♪♪ E.	.. ⊢ ⊢ t:α α → → β β .. ⊢ ⊢ u:α α .. ⊢ ⊢ tu:β β {displaystyle {frac {Gamma vdash t:alpha rightarrow beta qquad Gamma vdash u:alpha }{Gamma vdash t;u:beta }

Parafraseando la correspondencia, probar Γ ⊢ α 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 nuevo tipo sin restricciones, la regla → I corresponde a la abstracción de funciones y la regla → E la regla corresponde a la aplicación de la función. Observe 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 de tipo α → α → α no se distinguiría 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 tipificado. Visto en un nivel abstracto, la correspondencia se puede resumir como se muestra en la siguiente tabla. En especial, 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 cual se deduce que los algoritmos para el problema de ocupación de tipos pueden convertirse en algoritmos para decidir la demostrabilidad intuicionista.

La correspondencia de Howard naturalmente se extiende a otras extensiones de la deducción natural y al cálculo lambda simplemente tipeado. Aquí hay una lista no exhaustiva:

• Sistema Girard-Reynolds F como un lenguaje común para la lógica proposición de segundo orden y el cálculo de lambda polimorfo,
• lógica de orden superior y sistema de Girard Fω
• tipos inductivos como tipo de datos algebraicos
• necesidad ▪ ▪ {displaystyle Box} modal logic and staged computation
• posibilidad Cause Cause {displaystyle Diamond modal logic and monadic types for effects
• El λ_I cálculo (donde la abstracción se limita a λx.E Donde x tiene al menos una ocurrencia libre en E) y CL_I El cálculo corresponde a la lógica relevante.
• La modalidad de la verdad local (llamada) en la topología Grothendieck o la modalidad equivalente "lax" (◯) de Benton, Bierman y de Paiva (1998) corresponden a CL-logic describiendo "tipos de computación".

Operadores lógicos y de control clásicos

En la época de Curry, y también en la época de Howard, la correspondencia de las pruebas como 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 deducible. La extensión de la correspondencia a la ley de Peirce y, por lo tanto, a la lógica clásica quedó clara a partir del trabajo de Griffin sobre la tipificación de operadores 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 tarde. La correspondencia básica de estilo Curry-Howard para la lógica clásica se da a continuación. 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 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 de 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 secuencial de Gentzen, pero no es una correspondencia con un modelo de computación preexistente bien definido como lo fue para el estilo de Hilbert y deducciones naturales.

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

El papel de de Bruijn

N. G. de Bruijn usó la notación lambda para representar pruebas del verificador de teoremas Automath y representó 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 declaró 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 BHK

La interpretación BHK interpreta las pruebas intuicionistas como funciones pero no especifica la clase de funciones relevantes para la interpretación. Si uno 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.

Realización

La realizabilidad recursiva de Kleine 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, ejemplifica correctamente las disyunciones y los cuantificadores existenciales de la fórmula inicial para que la fórmula sea verdadera.

La realizabilidad modificada de Kreisel se aplica a la lógica intuicionista de predicados de orden superior y muestra que el término lambda simplemente tipeado y extraído inductivamente de la prueba da cuenta de la fórmula inicial. En el caso de la lógica proposicional, coincide con la declaración de Howard: el término lambda extraído es la prueba en sí misma (visto como un término lambda sin tipo) y la declaración de realizabilidad es una paráfrasis del hecho de que el término lambda extraído tiene el tipo que significa la fórmula (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 conexión con el cálculo lambda no está clara, incluso en el caso de la deducción natural.

Correspondencia entre Curry, Howard y 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 que es la de las categorías cerradas cartesianas. Algunas personas utilizan ahora la expresión correspondencia de Curry-Howard-Lambek para referirse al isomorfismo de tres vías entre la lógica intuicionista, el cálculo lambda tipado y las categorías cerradas cartesianas, con los objetos que se interpretan como tipos o proposiciones y los morfismos como términos o pruebas. La correspondencia funciona a nivel ecuacional 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 un La categoría cerrada cartesiana no es comparable a la estructura de una prueba del juicio correspondiente en la lógica al estilo de Hilbert o en la deducción natural. 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 α α × × β β {displaystyle alpha times beta } y α α → → β β {displaystyle alpha rightarrow beta } son objetos.

Los morfismos (términos) se definen por

• id{displaystyle id}, ⋆ ⋆ {displaystyle star }, eval{displaystyle operatorname {eval}, π π 1{displaystyle pi ¿Qué? y π π 2{displaystyle pi _{2} son morfismos
• si t es un morfismo, λt es un morfismo
• si t y u son morfismos, ()t,u){displaystyle (t,u)} y u∘ ∘ t{displaystyle ucirc t} son morfismos.

Los morfismos bien definidos (títulos tipodos) se definen por las siguientes reglas de escritura (en las que la notación de morfismo categórica habitual) f:α α → → β β {displaystyle f:alpha to beta } es reemplazado por notación de cálculo secuencial f:− − α α ⊢ ⊢ β β {displaystyle F:beta }).

Identidad:

id:− − α α ⊢ ⊢ α α {fnMicroc} {}{id:! ~vdash ~alpha }

Composición:

t:− − α α ⊢ ⊢ β β u:− − β β ⊢ ⊢ γ γ u∘ ∘ t:− − α α ⊢ ⊢ γ γ {displaystyle {frac {fnMicrosoft Sans Serif} ~vdash ~beta qquad u:! ~vdash ~gamma.. }

Tipo de unidad (objeto terminal):

⋆ ⋆ :− − α α ⊢ ⊢ ⊤ ⊤ {displaystyle {frac {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} ~ 'vdash ~ 'top }

Producto cartesiano:

t:− − α α ⊢ ⊢ β β u:− − α α ⊢ ⊢ γ γ ()t,u):− − α α ⊢ ⊢ β β × × γ γ {displaystyle {frac {fnMicrosoft Sans Serif} ~vdash ~beta qquad u:! ~vdash ~gamma }{(t,u):!!-~~alpha ~vdash ~beta times gamma }

Proyección izquierda y derecha:

π π 1:− − α α × × β β ⊢ ⊢ α α π π 2:− − α α × × β β ⊢ ⊢ β β {fnMicroc {fnK} {fnMicrosoft} {fnMicrosoft}} {fnMicroc} {f}} {fn}}} {fnMicrosoft}}}}} {fnMicroc}}} {f}} {f}fnK}}f}}}}}f}f}}}fnf}}}}fnf}fnfnf}f}fnf}f}f}f}f}fnfnfnfnfnfnfnfnfnfnfnKfnKfnKfnKfnKfnKfnKfnfnfnKfnKfnKfnKfnKfnKfnKfnKfnh}}}}}}fn - ¿Por qué? ~vdash ~alpha }qquad {frac {fnMicrosoft Sans Serif} - ¿Por qué? ~vdash ~beta }

Curry:

t:− − α α × × β β ⊢ ⊢ γ γ λ λ t:− − α α ⊢ ⊢ β β → → γ γ {displaystyle {frac {t:!!-~alpha times beta ~ 'vdash ~ 'gamma ♫{lambda t:beta rightarrow gamma }

Solicitud:

eval:− − ()α α → → β β )× × α α ⊢ ⊢ β β {displaystyle {frac {}{eval:!!-~ {alpha rightarrow beta)times alpha ~vdash ~beta }

Finalmente, las ecuaciones de la categoría son

• id∘ ∘ t=t{displaystyle idcirc t=t}
• t∘ ∘ id=t{displaystyle tcirc id=t}
• ()v∘ ∘ u)∘ ∘ t=v∘ ∘ ()u∘ ∘ t){displaystyle (vcirc u)circo t=vcirco (ucirc t)}
• ⋆ ⋆ =id{displaystyle star =id} (si está bien escrito)
• ⋆ ⋆ ∘ ∘ u=⋆ ⋆ {displaystyle star circ u=star }
• π π 1∘ ∘ ()t,u)=t{displaystyle pi _{1}circ (t,u)=t}
• π π 2∘ ∘ ()t,u)=u{displaystyle pi _{2}circ (t,u)=u}
• ()π π 1,π π 2)=id{displaystyle (pi _{1},pi _{2}=id}
• ()t1,t2)∘ ∘ u=()t1∘ ∘ u,t2∘ ∘ u){displaystyle (t_{1},t_{2})circ u=(t_{1}circ u,t_{2}circ u)}
• eval∘ ∘ ()λ λ t∘ ∘ π π 1,π π 2)=t{displaystyle evalcirc (lambda tcirc pi _{1},pi _{2})=t}
• λ λ eval=id{displaystyle lambda eval=id}
• λ λ t∘ ∘ u=λ λ ()t∘ ∘ ()u∘ ∘ π π 1,π π 2)){displaystyle lambda tcirc u=lambda (tcirc (ucirc pi _{1},pi _{2})}

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

• ()π π 1∘ ∘ t,π π 2∘ ∘ t)=t{displaystyle (pi _{1}circ t,pi _{2}circ t)=t}
• λ λ ()eval∘ ∘ ()t∘ ∘ π π 1,π π 2))=t{displaystyle lambda (evalcirc (tcirc pi _{1},pi _{2})=t}

Ahora, existe t tales que t:− − α α 1× × ...... × × α α n⊢ ⊢ β β {displaystyle t:!!-~alpha _{1}times ldots times alpha _{n}vdash beta } Sip α α 1,...... ,α α n⊢ ⊢ β β {displaystyle alpha _{1},ldotsalpha _{n}vdash beta } es prable en lógica intuitionista implicacional.

Ejemplos

Gracias a la correspondencia Curry-Howard, una expresión escrita 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 de estilo Hilbert

Como ejemplo, considere una demostración del teorema α → α. En cálculo lambda, este es el tipo de función de 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 los siguientes pasos pueden usarse para probar α → α:

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

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. Primera prueba teoremas correspondientes a los tipos de P y Q.
2. Desde P se está aplicando 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, β, a través de la regla 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 prueba del teorema (β → α) → (γ → β) → γ → α.

El primer paso es construir (K S). 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 solo S, el consecuente se puede separar usando Modus Ponens:

K: δ →α → β → γ) →α → β) → α → γ

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

S#α → β → γ) →α → β) → α → γ,

poner α = δ, β = α → β → γ, y γ = (α → β) → α → γ, dando

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

y luego separe el consecuente:

S (K S)#δ → α → β → γ) → δ →α → β) → α → γ

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

S (K S)[δ = β → γ#β → γ) → α → β → γ) →β → γ) →α → β) → α → γ

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 así que, separando el consecuente:

S (K S) K#β → γ) →α → β) → α → γ

Cambiando los nombres de las variables α y γ Nos da

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

que era lo que quedaba por probar.

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

El siguiente diagrama da prueba de (β → α) → (γ → β) → γ → α 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:γ ⊢ b g: β
-———————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————————
a:β → α, b:γ → β, g:γ ⊢ a (b g): α
—————————————————————————————————————————
a:β → α, b:γ → β ⊢ λ g. a (b g): γ → α
————————————————————————————————————————————
a:β → α ⊢ λ b. λ g. a (b g): (γ → β) → γ → α
—————————————————————————————————————————
⊢ λ a. λ b. λ g. a (b g): (β → α) → (γ → β) → γ → α

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. El método indexa conjuntos de genotipos (los árboles de programa desarrollados por el sistema GP) por su prueba isomórfica de Curry-Howard (denominada especie).

Como señaló el director de investigación de INRIA, Bernard Lang, la correspondencia Curry-Howard constituye un argumento en contra de la patentabilidad del software: dado que los algoritmos son pruebas matemáticas, la patentabilidad del primero implicaría la patentabilidad del segundo. Un teorema podría ser propiedad privada; un matemático tendría que pagar por usarlo y confiar en la compañía 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 lejos y más profundamente. 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 tipo lineal (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 estos corresponden a cobordismos, que juegan 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, que se convirtió en un área de investigación muy activa alrededor de 2013 y, a partir de 2018, todavía lo es. Aquí, la teoría de tipos se amplía con el axioma de univalencia ("la equivalencia es equivalente a la igualdad") que permite que la teoría de tipos homotópicos se utilice como base para todas las matemáticas (incluidas la teoría de conjuntos y la lógica clásica, proporcionando nuevas formas para 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 de identidad o el tipo de igualdad de la teoría de tipos se interpreta como un camino).