functional programming - ¿Cuáles son las equivalencias más interesantes que surgen del isomorfismo de Curry-Howard?

functional-programming formal-methods (10)

Me encontré con el isomorfismo de Curry-Howard relativamente tarde en mi vida de programación, y tal vez esto contribuye a que me fascine por completo. 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:

Entonces, a mi pregunta: ¿cuáles son algunas de las implicaciones más interesantes / oscuras de este isomorfismo? No soy 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 conozco nombres concisos en lógica:

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

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

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

Editar:

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

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

Aquí hay uno ligeramente oscuro que me sorprende que no haya sido mencionado anteriormente: la programación reactiva funcional "clásica" corresponde a la lógica temporal.

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

Entonces, primero, ¿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 básicos de datos: eventos y comportamientos.

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

Los comportamientos son valores que existen constantemente pero que pueden cambiar continuamente. La posición del mouse es un gran ejemplo: es solo un comportamiento de 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 conjunto de pasos discretos.

¿Y qué es la lógica temporal? Apropiadamente, es un conjunto de reglas lógicas para tratar proposiciones cuantificadas a lo largo del tiempo. Básicamente, extiende la lógica de primer orden normal con dos cuantificadores: □ y ◇. El primero significa "siempre": lea □ φ como "holds siempre se sostiene". 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 estos tipos están habitados, esto debería tener sentido: un comportamiento está habitado en todo momento posible, mientras que un evento solo ocurre una vez.

Dado que usted pidió explícitamente los más interesantes y oscuros:

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

EDITAR: Una referencia que recomendaría a cualquier persona interesada en aprender más acerca de las 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 parte de los primeros principios y gran parte de él está destinado a ser accesible para no teóricos / teóricos del lenguaje. (Aunque soy el segundo autor, soy parcial.)

El soporte de continuación 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 equivale 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-old/handouts/callcc.pdf

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

La no terminación representa una contradicción, una lógica inconsistente. Sin embargo, una lógica inconsistente le permitirá probar anything , incluida la falsedad.

Ignorando inconsistencias, los sistemas de tipo típicamente corresponden a una lógica intuicionista , y son necesariamente constructivist , lo que significa que ciertas piezas de lógica clásica no pueden expresarse 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 medio de construir lo que sea que haya probado la existencia .

Una característica principal del sabor constructivista es que la doble negación no es equivalente a la no negación. De hecho, la negación rara vez es primitiva en un sistema de tipos, por lo que podemos representarlo como que implica falsedad, por ejemplo, not P convierte en P -> Falsity . La doble negación sería, por lo tanto, una función con tipo (P -> Falsity) -> Falsity , que claramente no es equivalente a algo así como simplemente escriba P

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

Pero, ¿cuál es el punto? ¿Por qué escribir un tipo como ese? ¿ Significa algo en términos de programación? Bueno, puedes pensar que es una función que ya tiene algo del tipo P alguna parte, y necesita que le des una función que tome P como argumento, con todo siendo 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 pueden componerse juntos, pasarse, invocarse, lo que sea. Esto debería comenzar a sonar familiar para los fanáticos de algunos lenguajes, como Scheme o Ruby, porque lo que significa es que la doble negación corresponde al estilo de continuación de paso , y de hecho, el tipo que di más arriba es exactamente la mónada de continuación en Haskell.

Me gusta mucho esta pregunta No sé mucho, pero tengo algunas cosas (con la ayuda del artículo de Wikipedia , que tiene algunas tablas ordenadas y tal):

Creo que los tipos de suma / tipos de unión ( por ejemplo, data Either ab = Left a | Right b ) son equivalentes a la disyunción inclusiva . 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 Either represente. Usted tiene Either representando exclusivo o, ⊕; sin embargo, ( a ∧ b ) ↛ ( a ⊕ b ). Por ejemplo, ⊤ ∧ ⊤ ⊤ but, pero ⊤ ⊕ ⊥ ⊥ ⊥, y ⊤ ↛ ⊥. En otras palabras, si tanto a como b son verdaderas, entonces la hipótesis es verdadera, 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 tanto a como b son verdaderos, entonces al menos uno es verdadero. Por lo tanto, si las uniones discriminadas son alguna forma de disyunción, deben ser la variedad inclusiva. Creo que esto es una prueba, pero me siento más que libre para desilusionarme de esta noción.
De manera similar, sus definiciones de tautología y absurdo como función de identidad y funciones no terminadoras, respectivamente, están un poco desconectadas. La fórmula verdadera está representada por el tipo de unidad , que es el tipo que tiene un solo elemento ( data ⊤ = ⊤ , a menudo deletreado () y / o Unit en lenguajes de programación funcionales). Esto tiene sentido: ya que ese tipo está garantizado para ser 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 las funciones no terminadas es, dependiendo de lo que usted quiere decir exactamente, más apagado. Curry-Howard funciona en el sistema de tipo, pero la no terminación no está codificada allí. Según Wikipedia , lidiar con la no terminación es un problema, ya que agregarlo produce lógicas inconsistentes ( por ejemplo , puedo definir wrong :: a -> b por wrong x = wrong x , y así "probar" que a → b para cualquier ayb ). Si esto es lo que quisiste decir con "absurdo", entonces estás exactamente en lo cierto. Si, en cambio, se refería a la declaración falsa, entonces lo que quiere es un tipo deshabitado, por ejemplo , algo definido por data ⊥ , es decir, un tipo de datos sin ninguna forma de construirlo. Esto asegura que no tiene ningún valor, por lo que debe estar deshabitado, lo que es equivalente a falso. Creo que probablemente también puedas usar a -> b , ya que si prohibimos las funciones que no terminan, entonces esto también está deshabitado, pero no estoy 100% seguro.
Wikipedia dice que los axiomas están codificados de dos maneras diferentes, según cómo interpretes a Curry-Howard: 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 por defecto (similar a la forma en que modus ponens es un axioma porque la aplicación de funciones es primitiva). Y creo que la vista variable 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 sobre los que estamos tratando de probar cosas.
De acuerdo con 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 denomina ley de equivalencia de exportación, al menos en deducción natural pruebas No me di cuenta en ese momento que solo estaba currando, ¡ojalá lo hubiera hecho, porque es genial!
Si bien ahora tenemos una manera de representar la disyunción inclusiva , no tenemos una manera de representar la variedad exclusiva. Deberíamos ser capaces de usar la definición de disyunción exclusiva para representarla: a ⊕ b ≡ ( a ∨ b ) ∧ ¬ ( a ∧ b ). No sé cómo escribir la negación, pero sí sé que ¬ p ≡ p → and, y tanto la implicación como la falsedad son fáciles. Por lo tanto, deberíamos poder representar la disyunción exclusiva mediante:
data ⊥ data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
Esto define ⊥ como el tipo vacío sin valores, que corresponde a la falsedad; Xor se define entonces para que contenga ambos ( y ) Either 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 significa .~~ ( Edite 1: ¡ Ahora sí, vea el siguiente párrafo!) ~~Como no hay valores de tipo (a,b) -> ⊥ (¿están ahí?), No puedo comprender lo que esto significaría en un programa.~~ ~~¿Alguien sabe una mejor manera de pensar en esta definición u otra?~~ ( Editar 1: Sí, camccann .)
Edición 1: Gracias a camccann (más particularmente, los comentarios que dejó sobre él para ayudarme), creo que veo lo que está sucediendo aquí. Para construir un valor de tipo Xor ab , debe proporcionar dos cosas. Primero, un testigo de la existencia de un elemento de a o b como primer argumento; es decir, una Left a o una Right b . Y en segundo lugar, una prueba de que no hay elementos de ambos tipos b en otras palabras, una prueba de que (a,b) está deshabitado, como el segundo argumento. Como solo podrá escribir una función de (a,b) -> ⊥ si (a,b) está deshabitado, ¿qué significa que ese sea el caso? Eso significaría que alguna parte de un objeto de tipo (a,b) no podría construirse; en otras palabras, ¡al menos uno, y posiblemente ambos, de a y b están deshabitados! En este caso, si estamos pensando en el emparejamiento de patrones, posiblemente no podrías emparejar patrones en tal tupla: suponiendo que b está deshabitada, ¿qué escribiríamos que pudiera coincidir con la segunda parte de esa tupla? Por lo tanto, no podemos coincidir con el patrón, lo que puede ayudarnos a ver por qué esto lo deshabita. Ahora, la única forma de tener una función total que no tenga argumentos (ya que ésta debe estar, ya que (a,b) está deshabitada) es que el resultado también sea de tipo deshabitado, si estamos pensando en esto desde un la perspectiva de coincidencia de patrones, esto significa que, aunque la función no tiene ningún caso, tampoco existe un cuerpo posible que pueda tener, por lo que todo está bien.

Mucho de esto es que estoy pensando en voz alta / probando (con suerte) cosas sobre la marcha, pero espero que sea útil. Realmente recomiendo el artículo de Wikipedia ; No lo he leído en detalle, pero sus tablas son un resumen muy bueno y muy completo.

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-continuation

CH generalmente se establece como correspondencia entre lógica intuitiva y programas. Sin embargo, si agregamos el operador call-with-current-continuetion (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 simple isomorfismo, esta discusión sobre LEM constructiva es un resultado muy interesante. En particular, en la sección de conclusiones, Oleg Kiselyov discute cómo el uso de 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 mónadas capturan efectos computacionales es antigua, pero esta instancia del isomorfismo de Curry-Howard ayuda a ponerlo en perspectiva y ayuda a llegar a lo que la doble negación realmente "significa".

Su tabla no es del todo correcta; 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 completo de Turing es inconsistente. La recursividad no tiene correspondencia en teorías consistentes. En una teoría incoherente de lógica / prueba insegura podría llamarse una regla que causa incoherencia / falta de solidez.

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

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

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

Una cosa que es importante, pero aún no se ha investigado, es la relación de 2-continuación (continuación que toma 2 parámetros) y golpe de Sheffer . En la lógica clásica, el trazo de Sheffer puede formar un sistema completo de lógica por sí mismo (más algunos conceptos que no son de operador). Lo que significa que lo familiar and , or not , puede implementarse utilizando solo el stoke stoke o nand .

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

La firma de tipo de una 2-continuación es (a,b) -> Void . Mediante esta implementación podemos definir 1-continuación (continuaciones normales) como (a,a) -> Vacío, tipo de producto como ((a,b)->Void,(a,b)->Void)->Void , sum escriba como ((a,a)->Void,(b,b)->Void)->Void . Esto nos da una impresionante capacidad de expresividad.

Si profundizamos más, descubriremos que el gráfico existencial de Piece es equivalente a un lenguaje con el único tipo de datos n-continuado, pero no vi ningún idioma existente en esta forma. Así que inventar uno podría ser interesante, creo.

function composition | syllogism