¿Curry-Howard para un lenguaje de programación imperativo?

Question

El isomorfismo Curry-Howard vincula las pruebas de las proposiciones, con los "programas" y los tipos.

Pero tal y como me lo han presentado, los "programas" se interpretan de forma funcional, es decir, en cálculo lambda con teoría de tipos dependientes.

Me pregunto:

• ¿Se sigue aplicando el isomorfismo "programas como pruebas" cuando consideramos "programas imperativos" en lugar de cálculo lambda?

• ¿Existe una forma práctica (es decir, un asistente de pruebas concreto) para programar realmente las pruebas utilizando un estilo de lenguaje más imperativo, con teoría de tipos dependiente? (ps. mi pregunta está motivada porque realmente quiero probar esto)

Answer 1

Una perspectiva (extrema) de Curry-Howard (como principio general) es que afirma que los teóricos de las pruebas y los teóricos de los lenguajes de programación/teóricos de los tipos simplemente están utilizando palabras diferentes para la exacto las mismas cosas. Desde esta perspectiva (extrema), la respuesta a tu primera pregunta es trivialmente "sí". Simplemente llama a los tipos de su lenguaje imperativo "fórmulas", llama a los programas "pruebas", llama a las reglas de reducción de una semántica operativa "transformaciones de pruebas", y llama a (la parte de mapeo de tipos de una) semántica denotacional una "interpretación" (en el sentido teórico del modelo), y et voilà, tenemos un sistema de pruebas.

Por supuesto, para la mayoría de los lenguajes de programación, este sistema de pruebas tendrá horribles propiedades metateóricas, será inconsistente 1 y probablemente no tendrá un obvio conexión con (los sistemas de prueba para) las lógicas habituales. Los resultados interesantes del estilo Curry-Howard suelen conectar un sistema de pruebas preexistente con un lenguaje de programación/teoría de tipos preexistente. Por ejemplo, la correspondencia arquetípica Curry-Howard conecta el presentación de la deducción natural de la lógica proposicional intuicionista a (una presentación específica) del cálculo lambda simplemente tipado. A presentación del cálculo secuencial de la lógica proposicional intuitonista se conectaría (más directamente) con una presentación diferente del cálculo lambda simplemente tipado. Por ejemplo, en la presentación correspondiente a la deducción natural (y suponiendo que tenemos productos), tendrías términos $\pi_i:A_1\times A_2\to A_i$ y $\langle M,N\rangle : A_1\times A_2$ donde $M:A_1$ y $N:A_2$ . En una presentación de cálculo secuencial, no tendrías las proyecciones, sino que tendrías una coincidencia de patrones $\mathsf{let}$ Por ejemplo $\mathsf{let}\ \langle x,y\rangle = T\ \mathsf{in}\ U$ donde $T:A_1\times A_2$ y $U:B$ y $x$ y $y$ puede producirse de forma gratuita en $U$ con tipos $A_1$ y $A_2$ respectivamente. Como tercer ejemplo, una presentación al estilo de Hilbert de la lógica mínima (el fragmento de sólo implicación de la lógica intuicionista) te da la lógica combinatoria SKI. (Tengo entendido que este tercer ejemplo se acerca más a lo que hizo Curry).

Otra forma de utilizar Curry-Howard es aprovechar las herramientas e intuiciones de la teoría de la prueba con fines computacionales. El proyecto de Atsushi Ohori Asignación de registros por transformación de pruebas es un ejemplo de sistema de pruebas construido en torno a un lenguaje imperativo sencillo (que pretende ser de bajo nivel). Este sistema no pretende corresponder a ninguna lógica preexistente. Por otro lado, las interpretaciones computacionales pueden arrojar luz sobre los sistemas de prueba existentes o sugerir lógicas y sistemas de prueba completamente nuevos. Cosas como el Marco lógico concurrente aprovechar claramente la interacción entre la teoría de la prueba y la programación.

Digamos que empezamos con un cálculo lambda tipado, para familiarizarnos. ¿Qué ocurre cuando añadimos varios efectos? En realidad, lo sabemos en muchos casos (aunque normalmente los efectos tienen que ser cuidadosamente controlados, más de lo que suelen ser en los lenguajes de programación típicos). El ejemplo más conocido es callcc que nos da una lógica clásica (aunque, de nuevo, una lote de cuidado es necesario para producir un sistema de pruebas bien comportado). Diapositiva 5 (página 11) de este juego de diapositivas menciona varios otros y un esquema para codificarlos en Coq. (Puede que le resulte interesante todo el conjunto de diapositivas y otros trabajos de Pierre-Marie Pédrot .) Añadir efectos tiende a producir nuevas y potentes reglas de demostración y extensiones no triviales de lo que es demostrable (a menudo hasta el punto de la inconsistencia cuando se hace con displicencia). Por ejemplo, añadir excepciones (en el contexto de la teoría de tipos dependientes intuicionista) nos permite validar Regla de Markov . Una forma de entender las excepciones es mediante una traducción al estilo de las mónadas y la visión lógica de esto es La traducción de Friedman . Si se hace una lectura constructiva de la regla de Markov, en realidad es bastante obvio cómo se podría implementar dadas las excepciones. (Lo que es menos obvio es si añadir excepciones causa algún otro problema, lo cual, ingenuamente, claramente lo hace, ya que podemos "probar" cualquier cosa simplemente lanzando una excepción, pero si requerimos que todas las excepciones sean capturadas...)

Daniel Schepler mencionó la lógica de Hoare (una versión más moderna sería Teoría de los tipos de Hoare ), y vale la pena mencionar cómo se conecta esto. Una lógica de Hoare es en sí misma un sistema deductivo (que suele definirse en términos de una lógica tradicional). Las "fórmulas" son los triples de Hoare, es decir, los programas anotados con condiciones previas y posteriores, por lo que se trata de una forma diferente de conectar la lógica y la computación que Curry-Howard 2 .

Una perspectiva menos extrema de Curry-Howard añadiría algunas condiciones sobre lo que constituye un sistema de pruebas aceptable y, en sentido contrario, lo que constituye un lenguaje de programación aceptable. (Es muy posible especificar sistemas de pruebas que no den lugar a una noción obvia de computación). Además, la forma tradicional de utilizar Curry-Howard para producir un sistema computacional identifica la computación con la normalización de la prueba, pero hay otras formas de pensar en la computación. Independientemente de la perspectiva, los sistemas/reglas de prueba bien llevados suelen ser los más interesantes. Ciertamente, desde el punto de vista lógico, pero incluso desde el punto de vista de la programación, las buenas propiedades metateóricas del sistema de pruebas suelen corresponder a propiedades que son buenas para la comprensión de programas.

1 Las discusiones tradicionales sobre la lógica tienden a descartar las lógicas incoherentes como algo completamente sin interés. Esto es un artefacto de la irrelevancia de la prueba. Las lógicas inconsistentes pueden tener teorías de prueba interesantes. Simplemente no se puede aceptar cualquier prueba. Por supuesto, sigue siendo razonable centrarse en las teorías consistentes.

2 No pretendo sugerir que Daniel Schepler tuviera otra intención.

Answer 2

Como ya se ha sugerido en la respuesta anterior, los lenguajes imperativos pueden verse como lenguajes menos restrictivos que los funcionales. Cualquier lenguaje con un sistema de tipos suficientemente fuerte permite expresar tipos correspondientes a proposiciones matemáticas. Si se restringe a sólo un subconjunto del lenguaje, también se puede acabar con una lógica consistente.

Veamos algunos ejemplos en C++. Una implicación $A \to B$ corresponde bajo la interpretación BHK a una función, o algoritmo, del tipo $A$ a $B$ . Esto se puede expresar directamente con una función

b f(a input) {
    // here you would need to build something of type b only using the input
}

También se pueden expresar tipos de suma en C++ con enumeraciones:

enum Either { a, b };

Una prueba de $A \to A \vee B$ viene dada, por tanto, por la siguiente función

Either f(a input) {
    return (Either input);
}

Por supuesto, hay que limitarse a un estilo funcional, de lo contrario se puede probar todo construyendo elementos arbitrarios.

Tenga en cuenta que la idoneidad de un lenguaje de programación para ser un demostrador de teoremas es simplemente un continuo. Haskell puede ser considerado un probador de teoremas debido a su expresivo sistema de tipos, aunque permite la no terminación, lo que introduce un desagradable $\bot$ en el sistema de tipos.