¿Por qué es interesante el isomorfismo de Curry-Howard?

Answer 1

No puedo hacer nada mejor que la respuesta general de Sridhar Ramesh , pero creo que algunas cositas podrían ayudar con los detalles de la pregunta.

Dado que el isomorfismo relaciona las pruebas con los términos y las proposiciones con los tipos, verificar una prueba es como verificar un término. Para la mayoría de los sistemas tipográficos que probablemente nos interesen, eso es decidible.

No es tanto que el isomorfismo se aplique solo a programas que se detienen, sino que los lenguajes sin terminación corresponden a sistemas a prueba de sonido. Para ver por qué es así, considere el esquema de tipo del combinador Y en el cálculo lambda de tipo simple:

[matemáticas] (A \ a {A}) \ a {A} [/ matemáticas]

Si tiene Y, entonces, para cualquier proposición [matemática] A [/ matemática], puede obtener una prueba aplicando Y a la función de identidad en ese tipo. Por lo tanto, agregar el combinador Y a STLC lo hace poco lógico para la lógica intuicionista. (Si STLC no está en tu callejón, podemos hacer más o menos lo mismo en, por ejemplo, Java. Ver más abajo). Los lenguajes que siempre terminan son triviales desde algunas perspectivas, pero no necesariamente desde otros. En realidad, hay mucho que puedes hacer con la recursividad primitiva, y muchos lenguajes completos de Turing incluyen fragmentos de normalización que aún son interesantes.

“Ejecutar” una prueba es la normalización de la prueba. En particular, la regla beta estándar del cálculo lambda corresponde a la eliminación del corte:

[matemáticas] \ frac {\ frac {\ Delta, x: A \ vdash {M: B}} {\ Delta \ vdash \ lambda {x} .M: A \ to {B}} \ quad \ Delta \ vdash { N: A}} {\ Delta \ vdash (\ lambda {x} .M) \, N: B} \ longmapsto {\ Delta \ vdash {M [N / x]: B}} [/ math]

Esto significa que los sistemas de prueba con algoritmos de eliminación de cortes corresponden a lenguajes de programación de normalización (terminación).

Creo que Sridhar cubrió la mayor parte de por qué es importante. Dos razones más:

• En un lenguaje de programación mecanografiado con tipos suficientemente expresivos, los tipos se pueden usar para establecer teoremas sobre programas, y las pruebas de los teoremas son en sí mismos programas. La verificación de la prueba es realmente una verificación de tipo. Esta es la idea detrás de los asistentes de pruebas basados ​​en la teoría de tipos como Coq, Agda y Twelf.
• La lógica puede inspirar nuevos sistemas de tipos para lenguajes de programación. Por ejemplo, algunas personas se han preguntado acerca de las interpretaciones de Curry-Howard de las lógicas modales. Es decir, ¿qué lenguaje de programación y sistema de tipos podría corresponder a una lógica modal dada? Algunas personas han presentado respuestas interesantes a esto, por ejemplo, utilizando el operador modal para indicar recursos remotos en un idioma para programas distribuidos. Del mismo modo, la lógica lineal ha inspirado el trabajo en los sistemas de tipos conscientes de los recursos.

Ahora para el bit prometido de Java. Podemos construir un sistema de prueba (¡poco sólido!) En Java. Usaremos tipos Java para representar proposiciones en lógica intuicionista, y construir un valor Java (o clase) con ese tipo es una prueba de la proposición.

A continuación, declaro las clases True para representar la proposición [math] \ top [/ math] y False para representar la proposición [math] \ bot [/ math]. El primero puede ser instanciado (dando una prueba de [math] \ top [/ math]), pero el último no. La interfaz Impl representa la implicación [math] A \ to {B} [/ math]. Debajo de eso, doy varias clases correspondientes a los teoremas de la lógica intuicionista, y una clase que no debería ser un teorema, pero es demostrable en Java usando la recursividad. (Todos estos son demostrables usando null también.) No quiero decir que sea una buena demostración del isomorfismo de Curry-Howard, pero podría ayudar a demostrar por qué la no terminación conduce a la falta de solidez.

 class CurryHoward { // Truth public class True { }; // Falsity (no instances) public class False { private False () { } }; // Implication public interface Impl { B pf (A a); }; // A -> A public class I implements Impl { public A pf (A a) { return a; } }; // A -> B -> A public class K implements Impl<A, Impl> { public Impl pf (final A a) { return new Impl() { public A pf (B b) { return a; } }; } } // (A -> B -> C) -> (A -> B) -> (A -> C) public class S implements Impl<Impl<A, Impl>, Impl<Impl, Impl>> { public Impl<Impl, Impl> pf (final Impl<A, Impl> f) { return new Impl<Impl, Impl>() { public Impl pf (final Impl g) { return new Impl() { public C pf (A a) { return f.pf(a).pf(g.pf(a)); } }; } }; } } // recursion leads to unsoundness: // A -> B public class AtoB implements Impl { public B pf(A a) { return pf(a); } } }; 

Answer 2

Muchas propiedades no triviales de los programas son decidibles (p. Ej., “¿Es esto un palíndromo?”, “¿Es este código Java válido?”, “¿Se detiene esto dentro de los 500 pasos en la entrada de modo regular?”); son solo las propiedades que dependen únicamente de la función parcial que calcula un programa (es decir, las propiedades que dependen únicamente de qué entradas hacen que se ejecute para siempre y qué salidas produce en las otras entradas) que deben ser triviales si pueden decidirse para programas arbitrarios.

La importancia de la correspondencia de Curry-Howard es que, una y otra vez, resulta que una estructura abstracta que es estudiada por los lógicos como una conexión lógica y otra estructura abstracta que es estudiada independientemente por los informáticos como una construcción del lenguaje de programación resulta para ser exactamente lo mismo. Además, este también suele ser el caso porque ambos simplemente estaban investigando, con sus propias motivaciones, alguna estructura teórica de categoría natural [cuando se enfatiza esta conexión, la correspondencia a veces se llama más vergonzosamente la correspondencia de Curry-Howard-Lambek]. Como sucede muy a menudo, resulta útil, como perspectiva organizativa, pensar en cualquier construcción de cualquiera de estas áreas como también una construcción en cualquiera de las otras áreas.

Con más detalle, el caso tradicional y epónimo de esto fue la comprensión de que la lógica proposicional intuicionista, el cálculo lambda simplemente tipado y las categorías cerradas cartesianas son esencialmente lo mismo, con las siguientes correspondencias respectivas:

• Propuestas correspondientes a tipos correspondientes a objetos.
• Pruebas de implicaciones entre proposiciones correspondientes a términos que describen funciones entre tipos correspondientes a morfismos entre objetos.
• Equivalencias entre pruebas (en el sentido de la teoría de la prueba) correspondientes a equivalencias beta-eta entre términos de cálculo lambda correspondientes a igualdades entre morfismos
• La implicación conectiva correspondiente al constructor del tipo de función correspondiente al bifunctor exponencial

La naturaleza de la correspondencia es que las reglas que usted daría para describir cómo construir proposiciones, pruebas e igualdades de prueba en la lógica proposicional intuicionista son exactamente las mismas que daría sobre cómo construir tipos, términos e igualdad de términos en el simplemente tecleó cálculo lambda y los que daría sobre cómo construir objetos, morfismos e igualdades de morfismo en categorías cerradas cartesianas. De hecho, estas tres nociones son solo tres formas diferentes de describir exactamente lo mismo. Aunque originalmente llegó con diferentes motivaciones por diferentes investigadores, la estructura matemática que describían en cada caso es esencialmente idéntica.

El significado perdurable de la correspondencia Curry-Howard (-Lambek) es la idea de que cualquier categoría se puede ver como un sistema de prueba, y cualquier categoría se puede ver como un lenguaje de programación, y viceversa, lo que permite cambiar de perspectiva, con el ayuda de los primeros tres puntos anteriores. [De hecho, con el aumento de la lógica categórica, también podemos agregar más puntos a esta correspondencia: cualquier categoría puede verse como una especie de teoría de conjuntos, y viceversa, con objetos que corresponden a conjuntos definibles, morfismos que corresponden a funciones definibles , e igualdades entre morfismos correspondientes a la igualdad de funciones extensible demostrable]. Lo que es natural en uno de estos dominios a menudo se considera de manera natural en cualquiera de los otros. No es tan significativo como un teorema matemático (porque es un teorema diferente cada vez que se ve de nuevo que las estructuras abstractas estudiadas independientemente de dos o más de estos dominios coinciden) como una forma fructífera de ver las cosas.