Una pregunta acerca de la lógica y la correspondencia de Curry-Howard

Question

¿Podría usted por favor me explique cuál es la conexión básica entre los fundamentos de la programación lógica y el fenómeno de similitud sintáctica entre los sistemas de tipo convencional y la lógica?

Answer 1

La correspondencia de Curry-Howard no se trata de la programación lógica, pero la programación funcional. El mecánico fundamental de Prolog se justifica en la teoría de la prueba por resolución técnica de John Robinson, que muestra cómo es posible comprobar si las fórmulas lógicas expresan como cláusulas de Horn son satisfiable , es decir, si usted puede encontrar términos a substitue por sus variables lógicas que les hacen realidad.

Por lo tanto la programación lógica es sobre la especificación de programas como fórmulas lógicas, y el cálculo del programa es alguna forma de inferencia prueba, en Prolog reolution, como he dicho. Por el contrario los espectáculos correspondencia de Curry-Howard qué pruebas en un formulasition especial de la lógica, llamado deducción natural , corresponden a programas en el cálculo lambda, con el tipo de programa correspondiente a la fórmula que la prueba demuestra; cómputo en los cálculo lambda corresponde a un fenómeno importante en la teoría de la prueba llamada normalización, que transforma las pruebas en nuevas pruebas más directas. Por lo tanto la programación lógica y la programación funcional corresponden a diferentes niveles en estas lógicas:. Programas de lógica de coincidencia fórmulas de una lógica, mientras que los programas funcionales coinciden con las pruebas de fórmulas

Hay otra diferencia: las lógicas utilizadas son generalmente diferentes. La programación lógica generalmente utiliza lógicas simples - como dije, Prolog se basa en cláusulas de Horn, que son una clase altamente restringido de fórmulas en las consecuencias no se pueden anidar, y no existen disyunciones, aunque Prolog se recupera toda la fuerza de la lógica clásica utilizando la regla de corte. Por el contrario, los lenguajes de programación funcionales como Haskell hacen un uso intensivo de los programas cuyos tipos tener implicaciones anidadas, y están decoradas con todo tipo de formas de polimorfismo. También se basan en la lógica intuicionista, una clase de lógica que prohíbe el uso del principio del tercero excluido, cuyo mecanismo de cálculo de Robinson se basa en.

Algunos otros puntos:

1. Es posible la programación lógica en la base de la lógica más sofisticadas que las cláusulas de Horn; por ejemplo, Lambda-prólogo se basa en la lógica intuicionista, con un mecanismo de cálculo diferente de resolución.
2. Dale Miller ha llamado el paradigma de la prueba teórica detrás de la lógica de la programación de la Búsqueda prueba como la programación metáfora, a diferencia de la pruebas como los programas metáfora que se utiliza otro término para la correspondencia de Curry-Howard.

Answer 2

La programación lógica se refiere fundamentalmente a la búsqueda meta dirigida a pruebas. La relación estructural entre las lenguas y la lógica escritas generalmente implica lenguajes funcionales, aunque a veces imprescindible y otros idiomas - pero no la lógica de programación directamente idiomas. Esta relación se refiere a los programas de pruebas.

Por lo tanto, la búsqueda prueba de la programación lógica se puede utilizar para encontrar pruebas que luego son interpretadas como programas funcionales. Esta parece ser la relación más directa entre los dos (como usted pidió).

programas integrales de construcción de esta manera no es práctico, pero puede ser útil para rellenar tediosos detalles de los programas, y hay algunos importantes ejemplos de esto en la práctica. Un ejemplo básico de esto es subtipificación estructural - que corresponde a llenar en pocos pasos a prueba a través de una sencilla prueba de vinculación. Un ejemplo mucho más sofisticado es el sistema de clases tipo de Haskell, que consiste en un tipo particular de búsqueda dirigida por metas -. En el extremo este implica una forma Turing completo de la programación lógica en tiempo de compilación