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

Question

¿Podría explicarme cuál es la conexión básica entre los fundamentos de la programación lógica y el fenómeno de la similitud sintáctica entre los sistemas de tipos y la lógica convencional?

Answer 1

La correspondencia de Curry-Howard no se trata de programación lógica, sino de programación funcional. La mecánica fundamental de Prolog está justificada en la teoría de pruebas por John Robinson resolution technique, que muestra cómo es posible verificar si las fórmulas lógicas expresadas como cláusulas Horn son satisfiable, es decir, si puede encontrar términos para sustituir sus variables lógicas que los hacen cierto.

Por lo tanto, la programación lógica se trata de especificar programas como fórmulas lógicas, y el cálculo del programa es una forma de inferencia de prueba, en la resolución Prolog, como ya he dicho. Por el contrario, la correspondencia de Curry-Howard muestra cómo las pruebas en una fórmula especial de lógica, llamada natural deduction, corresponden a programas en el cálculo lambda, con el tipo de programa correspondiente a la fórmula que la prueba prueba; La computación en el cálculo lambda corresponde a un fenómeno importante en la teoría de la prueba llamada normalización, que transforma las pruebas en pruebas nuevas y más directas. Así que la programación lógica y la programación funcional corresponden a diferentes niveles en estas lógicas: los programas lógicos combinan fórmulas de una lógica, mientras que los programas funcionales combinan las pruebas de fórmulas.

Hay otra diferencia: las lógicas utilizadas son generalmente diferentes. La programación lógica generalmente usa lógicas más simples — como dije, Prolog se basa en las cláusulas Horn, que son una clase altamente restringida de fórmulas donde las implicaciones no pueden anidarse, y no hay disyunciones, aunque Prolog recupera toda la fuerza de la lógica clásica usando el regla de corte. Por el contrario, los lenguajes de programación funcionales como Haskell hacen un uso intensivo de programas cuyos tipos tienen implicaciones anidadas, y están decorados por 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 centro excluido, sobre el cual se basa el mecanismo computacional de Robinson.

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-prolog se basa en lógica intuicionista, con un mecanismo de cálculo diferente a la resolución.
2. Dale Miller ha llamado el paradigma de la teoría de la prueba detrás de la lógica de la programación de la búsqueda como prueba de programación metáfora, para contrastar con las pruebas como programas metáfora que es otro término que se utiliza para la correspondencia de Curry-Howard.

Answer 2

La programación lógica se basa fundamentalmente en la búsqueda orientada a objetivos para las pruebas. La relación estructural entre los lenguajes tipados y la lógica generalmente involucra lenguajes funcionales, aunque a veces imperativos y otros lenguajes, pero no lenguajes lógicos de programación directamente. Esta relación relaciona pruebas con programas.

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

Crear programas completos de esta manera no es práctico, pero puede ser útil para completar tediosos detalles en los programas, y hay algunos ejemplos importantes de esto en la práctica. Un ejemplo básico de esto es el subtipado estructural, que corresponde a completar algunos pasos de prueba a través de una simple prueba de vinculación.Un ejemplo mucho más sofisticado es el sistema de clases de tipos de Haskell, que implica un tipo particular de búsqueda dirigida a objetivos; en el extremo esto implica una forma completa de programación lógica de Turing en tiempo de compilación.