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

Me encontré con el isomorfismo de Curry-Howard relativamente tarde en mi vida como programador, y tal vez esto contribuya 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, que se me viene a la 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 que 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

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

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

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 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 lógicos / teóricos del lenguaje. (Sin embargo, soy el segundo autor, así que soy parcial).

Estás enturbiando 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 inconclusos 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 cualquier cosa , incluida la falsedad.

Ignorando las inconsistencias, los sistemas de tipos suelen corresponder a una lógica intuicionista y son necesariamente constructivistas , lo que significa que ciertas piezas de la 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 cualquier cosa de la que hayas probado la existencia .

Una característica importante 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 un primitivo en un sistema de tipos, por lo que en su lugar podemos representarlo como que implica falsedad, por ejemplo, se not Pconvierte P -> Falsity. La doble negación sería, por tanto, una función con tipo (P -> Falsity) -> Falsity, que claramente no es equivalente a algo del tipo justo 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. aes, en cierto sentido, casi falso. Entonces, ¿qué pasa si escribimos doble casi negación usando polimorfismo? Obtenemos un tipo que tiene este aspecto: ∀a. (P -> a) -> a. ¿Es eso equivalente a algo de tipo P? De hecho lo es , simplemente aplíquelo a la función de identidad.

Pero cual es el punto? ¿Por qué escribir un tipo así? ¿ Significa algo en términos de programación? Bueno, puede pensar en ella como una función que ya tiene algo de tipo en Palguna parte, y necesita que le asigne una función que lo tome Pcomo argumento, siendo todo polimórfico en el tipo de resultado final. En cierto sentido, representa un cálculo suspendido , a la espera de que se proporcione el resto. En este sentido, estos cálculos suspendidos se pueden componer juntos, pasar, invocar, 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 y pase., y de hecho, el tipo que di arriba es exactamente la mónada de continuación en Haskell.

Su gráfico no es del todo correcto; 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 de un lenguaje funcional completo de Turing es inconsistente. La recursividad no tiene correspondencia en teorías consistentes. En una lógica inconsistente / teoría de prueba poco sólida, podría llamarla una regla que causa inconsistencia / falta de solidez.

[2] Nuevamente, esto es una consecuencia de la integridad. Esta 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 omiten características lógicas de primer orden: toda la cuantificación y parametrización se realiza mediante fórmulas. Si usted tuviera características de primer orden, habría una otra clase de *, * -> *, etc .; el tipo de elementos del dominio del discurso. Por ejemplo, en Father(X,Y) :- Parent(X,Y), Male(X), Xy Yabarcan el dominio del discurso (llámelo Dom), y Male :: Dom -> *.

function composition      | syllogism

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 demás):

1. Creo que los tipos de suma / tipos de unión ( por ejemplo data Either a b = Left a | Right b ) son equivalentes a la disyunción inclusiva . Y, aunque no conozco muy bien a 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, lo que Eitherrepresente. Tiene Eitherrepresentación exclusiva o, ⊕; sin embargo, ( a  ∧  b ) ↛ ( a  ⊕  b ). Por ejemplo, ⊤ ∧ ⊤ ≡ ⊤, 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 verdaderas, entonces al menos una es verdadera. 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 de desengañarme de esta noción.

2. De manera similar, sus definiciones de tautología y absurdo como función de identidad y funciones no terminantes, respectivamente, están un poco fuera de lugar. La verdadera fórmula está representada por el tipo de unidad , que es el tipo que tiene un solo elemento ( data ⊤ = ⊤; a menudo escrito ()y / o Uniten lenguajes de programación funcionales). Esto tiene sentido: dado que se garantiza que ese tipo estará habitado, y dado que solo hay un habitante posible, debe ser cierto. La función de identidad simplemente representa la tautología particular que a  →  a .

   Su comentario sobre las funciones no terminantes es, dependiendo de lo que quiera decir exactamente, más apagado. Curry-Howard funciona en el sistema de tipos, 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 -> bpor 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 estás en lo correcto. Si en cambio te refieres a la declaración falsa, entonces lo que quieres es cualquier tipo deshabitado, por ejemplo , algo definido pordata ⊥—Es decir, un tipo de datos sin ninguna forma de construirlo. Esto asegura que no tenga ningún valor, por lo que debe estar deshabitado, lo que equivale a falso. Creo que probablemente también podrías usarlo a -> b, ya que si prohibimos las funciones no terminantes, esto también está deshabitado, pero no estoy 100% seguro.

3. Wikipedia dice que los axiomas se codifican de dos formas diferentes, dependiendo de cómo interpretes 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 por defecto (similar a la forma en que modus ponens es un axioma porque la aplicación de la función es primitiva). Y creo que la vista de variables 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, creo que los tipos primitivos son las entidades, los objetos primitivos sobre los que estamos tratando de probar cosas.

4. 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 deducción natural pruebas. En ese momento no me di cuenta de que solo estaba curry, ojalá lo hubiera hecho, ¡porque es genial!

5. Si bien ahora tenemos una forma de representar la disyunción inclusiva , 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é que ¬ p  ≡  p  → ⊥, y tanto la implicación como la falsedad son fáciles. Por tanto, deberíamos poder representar la disyunción exclusiva mediante:

   data ⊥
   data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
   

   Esto se define ⊥como el tipo vacío sin valores, lo que corresponde a la falsedad; Xorluego se define para contener tanto ( y ) Eitheruna a o una b ( o ) como una función ( implicación ) desde (a, b) ( y ) al tipo inferior ( falso ). Sin embargo, no tengo idea de lo que esto significa . ( Edición 1: ¡ Ahora sí, vea el siguiente párrafo!) Dado que no hay valores de tipo (a,b) -> ⊥(¿los hay?), No puedo comprender qué significaría esto en un programa. ¿Alguien conoce una mejor manera de pensar sobre esta definición u otra? ( Edición 1: Sí, camccann .)

   Edición 1: Gracias a la respuesta de camccann (más particularmente, los comentarios que dejó para ayudarme), creo que veo lo que está pasando aquí. Para construir un valor de tipo Xor a b, debe proporcionar dos cosas. Primero, un testimonio de la existencia de un elemento de ao bcomo primer argumento; es decir, a Left ao a Right b. Y en segundo lugar, una prueba de que no hay elementos de ambos tipos ay b—en otras palabras, una prueba que (a,b)está deshabitada— como segundo argumento. Dado que solo podrá escribir una función desde (a,b) -> ⊥si (a,b)está deshabitada, ¿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, ay también bestén deshabitados! En este caso, si estamos pensando en la coincidencia de patrones, no es posible que coincida con el patrón en una tupla de este tipo: suponiendo que besté deshabitada, ¿qué escribiríamos que pudiera coincidir con la segunda parte de esa tupla? Por lo tanto, no podemos igualar el patrón 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 tome argumentos (como debe hacerlo esta, ya que (a,b)está deshabitada) es que el resultado también sea de un tipo deshabitado, si pensamos en esto desde una perspectiva de coincidencia de patrones, esto significa que aunque la función no tiene casos, no hay cuerpo posible podría haberlo hecho, así que todo está bien.

Mucho de esto soy yo 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 agradable y muy completo.

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

Por supuesto, a menos que sea un filósofo, matemático o programador funcional obsesivo, esto probablemente le plantee 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 pulsaciones de teclas son un gran ejemplo: puede pensar en las entradas del teclado como un carácter en un momento dado. Cada pulsación de tecla es solo un par con el carácter de la tecla y la hora en que se pulsó.

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 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 con proposiciones cuantificadas a lo largo del tiempo. Esencialmente, extiende la lógica normal de primer orden con dos cuantificadores: □ y ◇. El primero significa "siempre": lea □ φ 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 de FRP. En particular, □ corresponde a comportamientos y ◇ corresponde a eventos. Si pensamos en cómo están habitados estos tipos, esto debería tener sentido: un comportamiento está habitado en todo momento 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-continuation

CH se suele establecer como correspondencia entre la lógica intuicionista y los programas. Sin embargo, si agregamos el operador call-with-current-continuation (callCC) (cuyo tipo corresponde a la ley de Peirce), obtenemos una correspondencia entre la lógica clásica y los programas con callCC.

Si bien no es un simple isomorfismo, esta discusión sobre LEM constructivo es un resultado muy interesante. En particular, en la sección de conclusiones, Oleg Kiselyov analiza cómo el uso de mónadas para obtener la eliminación de la doble negación en una lógica constructiva es análogo a distinguir las 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 este ejemplo del isomorfismo de Curry-Howard ayuda a ponerlo en perspectiva y ayuda a entender lo que realmente "significa" la doble negación.

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 equivale a llamar a la continuación con esa misma expresión.

Para obtener una vista más detallada, consulte: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/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 toman 2 parámetros) y el trazo de Sheffer . En la lógica clásica, el trazo de Sheffer puede formar un sistema lógico completo por sí mismo (más algunos conceptos que no son de operador). Lo que significa que el familiar and, or, notpuede ser implementado utilizando únicamente el Stoke Sheffer o nand.

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

La firma de tipo de una continuación en 2 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, tipo de suma como ((a,a)->Void,(b,b)->Void)->Void. Esto nos da un impresionante poder de expresividad.

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