¿Cuáles son las equivalencias más interesantes que surgen del isomorfismo de curry-howard?

https://stackoverflow.com/questions/2969140

24-10-2019
|

Pregunta

Me encontré con el Isomorfismo de curry-howard Relativamente tarde en mi vida de programación, y tal vez esto contribuye a que esté completamente fascinado por ella. Implica que para cada concepto de programación existe un análogo preciso en la lógica formal y viceversa. Aquí hay una lista "básica" de tales analogías, fuera de mi cabeza:

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

Entonces, a mi pregunta: ¿Cuáles son algunas de las implicaciones más interesantes/oscuras de este isomorfismo? No soy un lógico, así que estoy seguro de que solo he arañado la superficie con esta lista.

Por ejemplo, aquí hay algunas nociones de programación para las cuales no soy consciente de los nombres concurridos en la lógica:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known theory + hypotheses"

Y aquí hay algunos conceptos lógicos que no he fijado en términos de programación:

primitive type?           | axiom
set of valid programs?    | theory

Editar:

Aquí hay algunas equivalencias más recolectadas de las respuestas:

function composition      | syllogism                -- from Apocalisp
continuation-passing      | double negation          -- from camccann

Solución

Ya que solicitaste explícitamente los más interesantes y oscuros:

Puede extender el CH a muchas lógicas y formulaciones interesantes de lógicas para obtener una amplia variedad de correspondencias. Aquí he tratado de centrarme en algunos de los más interesantes que en lo oscuro, además de un par de fundamentales que aún no han surgido.

evaluation             | proof normalisation/cut-elimination
variable               | assumption
S K combinators        | axiomatic formulation of logic   
pattern matching       | left-sequent rules 
subtyping              | implicit entailment (not reflected in expressions)
intersection types     | implicit conjunction
union types            | implicit disjunction
open code              | temporal next
closed code            | necessity
effects                | possibility
reachable state        | possible world
monadic metalanguage   | lax logic
non-termination        | truth in an unobservable possible world
distributed programs   | modal logic S5/Hybrid logic
meta variables         | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus            | linear logic

Editar: Una referencia que recomendaría a cualquier persona interesada en aprender más sobre extensiones de CH:

"Una reconstrucción crítica de la lógica modal" http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - Este es un gran lugar para comenzar porque comienza desde los primeros principios y gran parte está destinado a ser accesible para los no lógicos/teóricos del idioma. (Sin embargo, soy el segundo autor, así que soy parcial).

Otros consejos

Estás enredando un poco las cosas con respecto a la no terminación. La falsedad está representada por tipos deshabitados, que, por definición, no puede ser finalizado porque no hay nada de ese tipo que evaluar en primer lugar.

No terminación representa contradicción-una lógica inconsistente. Una lógica inconsistente, por supuesto Permitirle probar cualquier cosa, incluida la falsedad, sin embargo.

Ignorando las inconsistencias, los sistemas de tipo generalmente corresponden a un lógica intuicionista, y son por necesidad constructivista, lo que significa que ciertas piezas de lógica clásica no se pueden expresar directamente, si es que lo hacen. Por otro lado, esto es útil, porque si un tipo es una prueba constructiva válida, entonces un término de ese tipo es un medios para construir lo que haya demostrado la existencia de.

Una característica importante del sabor constructivista es que doble negación no es equivalente a la no negación. De hecho, la negación rara vez es una primitiva en un sistema de tipo, por lo que en cambio podemos representarlo como una falsedad, por ejemplo, not P convertirse en P -> Falsity. Por lo tanto, la doble negación sería una función con el tipo (P -> Falsity) -> Falsity, que claramente no es equivalente a algo de tipo solo P.

Sin embargo, ¡hay un giro interesante en esto! En un lenguaje con polimorfismo paramétrico, las variables de tipo rango en todos los tipos posibles, incluidos los deshabitados, por lo que un tipo totalmente polimórfico como ∀a. a es, en cierto sentido, casi falso. Entonces, ¿qué pasa si escribimos la doble casi negación usando el polimorfismo? Obtenemos un tipo que se ve así: ∀a. (P -> a) -> a. Es ese equivalente a algo de tipo P? De hecho, es, simplemente aplíquelo a la función de identidad.

Pero, ¿cuál es el punto? ¿Por qué escribir un tipo como ese? Lo hace significar ¿Algo en términos de programación? Bueno, puedes pensar que es una función que ya tiene algo de tipo P en algún lugar, y necesita que le dé una función que toma P Como argumento, todo el asunto es polimórfico en el tipo de resultado final. En cierto sentido, representa un cálculo suspendido, esperando que se proporcione el resto. En este sentido, estos cálculos suspendidos se pueden componer juntos, transmitidos, invocados, lo que sea. Esto debería comenzar a sonar familiares para los fanáticos de algunos idiomas, como Scheme o Ruby, porque lo que significa es que es que doble negación corresponde a Estilo de avance de continuación, y de hecho, el tipo que di arriba es exactamente la monad de continuación en Haskell.

Tu gráfico no está del todo bien; En muchos casos, ha confundido tipos con términos.

function type              implication
function                   proof of implication
function argument          proof of hypothesis
function result            proof of conclusion
function application RULE  modus ponens
recursion                  n/a [1]
structural induction       fold (foldr for lists)
mathematical induction     fold for naturals (data N = Z | S N)
identity function          proof of A -> A, for all A
non-terminating function   n/a [2]
tuple                      normal proof of conjunction
sum                        disjunction
n/a [3]                    first-order universal quantification
parametric polymorphism    second-order universal quantification
currying                   (A,B) -> C -||- A -> (B -> C), for all A,B,C
primitive type             axiom
types of typeable terms    theory
function composition       syllogism
substitution               cut rule
value                      normal proof

1] La lógica para un lenguaje funcional completado de Turing es inconsistente. La recursión no tiene correspondencia en teorías consistentes. En una teoría de lógica inconsistente/prueba no sólida, podría llamarlo una regla que causa inconsistencia/falta de liquidación.

2] Nuevamente, esto es una consecuencia de la integridad. Esto sería una prueba de un antiefrética si la lógica fuera consistente, por lo tanto, no puede existir.

3] No existe en lenguajes funcionales, ya que eluden características lógicas de primer orden: toda la cuantificación y la parametrización se realizan sobre fórmulas. Si tuviera funciones de primer orden, habría un tipo más que *, * -> *, etc.; El tipo de elementos del dominio del discurso. Por ejemplo, en Father(X,Y) :- Parent(X,Y), Male(X), X y Y rango sobre el dominio del discurso (llámalo Dom), y Male :: Dom -> *.

function composition      | syllogism

Realmente me gusta esta pregunta. No sé mucho, pero tengo algunas cosas (asistidas por el artículo de Wikipedia, que tiene algunas tablas ordenadas y tal en sí):

Creo que tipos de suma/tipos de unión (p.ej data Either a b = Left a | Right b) son equivalentes a inclusivo disyunción. Y, aunque no estoy muy familiarizado con Curry-Howard, creo que esto lo demuestra. Considere la siguiente función:
```
andImpliesOr :: (a,b) -> Either a b
andImpliesOr (a,_) = Left a
```
Si entiendo las cosas correctamente, el tipo dice que (a ∧ b) → (a ★ b) y la definición dice que esto es cierto, donde ★ es inclusivo o exclusivo o, cualquiera que sea Either representa. Tú tienes Either representando exclusivo o, ⊕; sin embargo, (a ∧ b) ↛ (a ⊕ b). Por ejemplo, ⊤ ∧ ⊤ ≡ ⊤, pero ⊤ ⊕ ⊥ ≡ ⊥, y ⊤ ↛ ⊥. En otras palabras, si ambos a y b son verdaderos, entonces la hipótesis es cierta, pero la conclusión es falsa, por lo que esta implicación debe ser falsa. Sin embargo, claramente, (a ∧ b) → (a ∨ b), ya que si ambos a y b son ciertos, entonces al menos uno es verdad. Por lo tanto, si los sindicatos discriminados son alguna forma de disyunción, deben ser la variedad inclusiva. Creo que esto es una prueba, pero se siente más que libre de deshacerme de esta noción.
Del mismo modo, sus definiciones de tautología y absurdo como función de identidad y funciones no terminadas, respectivamente, están un poco desactivadas. La verdadera fórmula está representada por el tipo de unidad, que es el tipo que solo tiene un elemento (data ⊤ = ⊤; a menudo deletreado () y/o Unit en lenguajes de programación funcional). Esto tiene sentido: ya que ese tipo es garantizado Para estar habitado, y dado que solo hay un posible habitante, debe ser cierto. La función de identidad solo representa la tautología particular que a → a.

Su comentario sobre funciones no terminadas es, dependiendo de lo que quisieras precisamente, más desactivado. Curry-howard funciona en el sistema de tipos, pero la no terminación no está codificada allí. De acuerdo a Wikipedia, tratar con la no terminación es un problema, ya que agregarlo produce lógicas inconsistentes (p.ej, Puedo definir wrong :: a -> b por wrong x = wrong x, y así "probar" que a → b para cualquier a y b). Si esto es lo que quisiste decir con "absurdo", entonces eres exactamente correcto. Si en su lugar se refería a la declaración falsa, entonces lo que quieres en su lugar es un tipo deshabitado, p.ej algo definido por data ⊥—Se es, un tipo de datos sin ninguna forma de construirlo. Esto asegura que no tenga valores en absoluto, por lo que debe estar deshabitado, lo cual es equivalente a los falsos. Creo que probablemente también podrías usar a -> b, dado que si prohibimos las funciones no terminadas, esto también está deshabitado, pero no estoy 100% seguro.
Wikipedia dice que los axiomas están codificados de dos maneras diferentes, dependiendo de cómo interprete el curry-howard: ya sea en los combinadores o en las variables. Creo que la vista del combinador significa que las funciones primitivas que se nos dan codifican las cosas que podemos decir de manera predeterminada (similar a la forma en que Modus Ponens es un axioma porque la aplicación de funciones es primitiva). Y yo pensar Que la vista variable en realidad puede significar lo mismo: los combinadores, después de todo, son solo variables globales que son funciones particulares. En cuanto a los tipos primitivos: si estoy pensando en esto correctamente, entonces creo que los tipos primitivos son las entidades, los objetos primitivos de los que estamos tratando de probar las cosas.
Según mi clase de lógica y semántica, el hecho de que (a ∧ b) → C ≡ a → (b → C) (y también que b → (a → C)) se llama Ley de equivalencia de exportación, al menos en pruebas de deducción natural. No noté en ese momento que solo era curry, ¡desearía haberlo hecho, porque eso es genial!
Mientras que ahora tenemos una forma de representar inclusivo Disjunción, no tenemos una forma de representar la variedad exclusiva. Deberíamos poder usar la definición de disyunción exclusiva para representarla: a ⊕ b ≡ (a ∨ b) ∧ ¬(a ∧ b). No sé cómo escribir negación, pero sí sé que ¬pags ≡ pags→ ⊥, y tanto la implicación como la falsedad son fáciles. Por lo tanto, debemos representar la disyunción exclusiva por:
```
data ⊥
data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
```
Esto define ⊥ ser el tipo vacío sin valores, que corresponden a la falsidad; Xor luego se define para contener ambos (y) Either un a o b (o) y una función (implicación) de (A, B) (y) al tipo inferior (falso). ~~Sin embargo, no tengo idea de lo que esto medio.~~ (Editar 1: Ahora lo hago, ¡mira el próximo párrafo!) ~~Dado que no hay valores de tipo (a,b) -> ⊥ (¿Ahí?), No puedo entender lo que esto significaría en un programa. ¿Alguien sabe una mejor manera de pensar en esta definición u otra?~~ (Editar 1: Sí, camcann.)

Editar 1: Gracias a Respuesta de Camccann (Más particularmente, los comentarios que dejó en él para ayudarme), creo que veo lo que está pasando aquí. Para construir un valor de tipo Xor a b, necesitas proporcionar dos cosas. Primero, un testigo de la existencia de un elemento de cualquiera a o b como el primer argumento; eso es un Left a o Right b. Y segundo, una prueba de que no hay elementos de ambos tipos a y b—En otras palabras, una prueba de que (a,b) está deshabitado, como el segundo argumento. Ya que solo podrás escribir una función de (a,b) -> ⊥ si (a,b) No está inhabitado, ¿qué significa que ese sea el caso? Eso significaría que alguna parte de un objeto de tipo (a,b) no se pudo construir; en otras palabras, que al menos uno, y posiblemente ambos, de a y b ¡Están deshabitados también! En este caso, si estamos pensando en la coincidencia de patrones, no podría coincidir con un patrón en tal tupla: suponiendo que b ¿Está deshabitado, qué escribiríamos que podría coincidir con la segunda parte de esa tupla? Por lo tanto, no podemos combinar contra él, lo que puede ayudarlo a ver por qué esto lo hace deshabitado. Ahora, la única forma de tener una función total que no toma argumentos (como esta debe, ya que (a,b) está deshabitado) es para que el resultado sea de un tipo deshabitado también, si estamos pensando en esto desde una perspectiva de coincidencia de patrones, esto significa que, aunque la función no tiene casos, no hay posible cuerpo Podría haberlo hecho, y todo está bien.

Mucho de esto soy yo pensando en voz alta/demostrando (con suerte) cosas sobre la marcha, pero espero que sea útil. Realmente lo recomiendo el artículo de Wikipedia; No lo he leído en ningún tipo de detalle, pero sus tablas son un resumen realmente agradable, y es muy minucioso.

Aquí hay una ligeramente oscura que me sorprende que no se haya mencionado anteriormente: la programación reactiva "clásica" "clásica" corresponde a la lógica temporal.

Por supuesto, a menos que sea filósofo, matemático o programador funcional obsesivo, esto probablemente plantea varias preguntas más.

Entonces, en primer lugar: ¿Qué es la programación reactiva funcional? Es una forma declarativa de trabajar con valores variables en el tiempo. Esto es útil para escribir cosas como interfaces de usuario porque las entradas del usuario son valores que varían con el tiempo. El FRP "clásico" tiene dos tipos de datos básicos: eventos y comportamientos.

Los eventos representan valores que solo existen en momentos discretos. Las teclas de teclas son un gran ejemplo: puede pensar en las entradas del teclado como un personaje en un momento dado. Cada KeyPress es solo un par con el carácter de la tecla y el tiempo que se presionó.

Los comportamientos son valores que existen constantemente pero que pueden cambiar continuamente. La posición del ratón es un gran ejemplo: es solo un comportamiento de las coordenadas X, Y. Después de todo, el mouse siempre tiene una posición y, conceptualmente, esta posición cambia continuamente A medida que mueve el mouse. Después de todo, mover el mouse es una sola acción prolongada, no un montón de pasos discretos.

¿Y qué es la lógica temporal? Apropiadamente, es un conjunto de reglas lógicas para tratar las proposiciones cuantificadas con el tiempo. Esencialmente, extiende la lógica normal de primer orden con dos cuantificadores: □ y ◇. El primero significa "siempre": leer □ φ como "φ siempre se mantiene". El segundo es "eventualmente": ◇ φ significa que "φ eventualmente se mantendrá". Este es un tipo particular de lógica modal. Las siguientes dos leyes relacionan los cuantificadores:

□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ

Entonces □ y ◇ son duales entre sí de la misma manera que ∀ y ∃.

Estos dos cuantificadores corresponden a los dos tipos en FRP. En particular, □ corresponde a comportamientos y ◇ corresponde a eventos. Si pensamos en cómo se habitan estos tipos, esto debería tener sentido: un comportamiento está habitado en cada tiempo posible, mientras que un evento solo ocurre una vez.

Relacionado con la relación entre continuaciones y doble negación, el tipo de llamada/CC es la ley de Peirce http://en.wikipedia.org/wiki/call-with-current-contination

CH generalmente se establece como correspondencia entre la lógica y los programas intuicionistas. Sin embargo, si agregamos el operador de llamada con la corriente de corriente (CallCC) (cuyo tipo corresponde a la ley de Peirce), obtenemos una correspondencia entre lógica clásica y programas con Callcc.

Si bien no es un isomorfismo simple, Esta discusión de LEM constructivo es un resultado muy interesante. En particular, en la sección de conclusión, Oleg Kiselyov analiza cómo el uso de las mónadas para obtener la eliminación de doble negación en una lógica constructiva es análogo a distinguir proposiciones computacionalmente decidibles (para las cuales LEM es válida en un entorno constructivo) de todas las proposiciones. La noción de que las monadas capturan los efectos computacionales es antigua, pero esta instancia del curry: el isomorfismo, ayuda a ponerlo en perspectiva y ayuda a obtener lo que realmente "significa".

El soporte de continuaciones de primera clase le permite expresar $ P lor neg P $. El truco se basa en el hecho de que no llamar a la continuación y salir con alguna expresión es equivalente a llamar a la continuación con esa misma expresión.

Para una vista más detallada, consulte: http://www.cs.cmu.edu/~rwh/courses/logic/www yandouts/callcc.pdf

2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

Una cosa que es importante, pero que aún no se ha investigado es la relación de 2 continuación (continuaciones que requieren 2 parámetros) y Sheffer Stroke. En la lógica clásica, Sheffer Stroke puede formar un sistema lógico completo por sí solo (más algunos conceptos no operadores). Lo que significa lo familiar and, or, not se puede implementar utilizando solo el Sheffer Stoke o nand.

Este es un hecho importante de su correspondencia de tipo de programación porque solicita que un combinador de un solo tipo se pueda usar para formar todos los demás tipos.

La firma de tipo de una continuación de 2 es (a,b) -> Void. Mediante esta implementación podemos definir 1 continuación (continuaciones normales) como (a,a) -> nulo, tipo de producto como ((a,b)->Void,(a,b)->Void)->Void, tipo de suma como ((a,a)->Void,(b,b)->Void)->Void. Esto nos da una impresión de su poder de expresividad.

Si cavamos más, descubriremos esa pieza gráfico existencial es equivalente a un idioma con el único tipo de datos es la continuación N, pero no vi que ningún lenguaje existente esté en esta forma. Así que inventar uno podría ser interesante, creo.

Licenciado bajo: CC-BY-SA con atribución

No afiliado a StackOverflow