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

Estás enturbiando un poco las cosas con respecto a la no discriminació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 contradicción an una lógica inconsistente. Una lógica inconsistente por supuesto le permitirá probar cualquier cosa, incluyendo la falsedad, sin embargo.

Ignorando inconsistencias, escriba sistemas típicamente corresponden a una lógica intuicionista , y son por necesidad 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 lo que sea que hayas probado la existencia de.

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

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

Pero ¿cuál es el punto? ¿Por qué escribir un tipo así? ¿Significa algo en términos de programación? Bueno, se puede pensar en ella como una función que ya tiene algo de tipo P en algún lugar, y necesita que le dé un función que toma P como argumento, siendo todo 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 ser compuestos juntos, pasados, invocados, lo que sea. Esto debería comenzar a sonar familiar a los fans de algunos lenguajes, como Scheme o Ruby because porque lo que significa es que la doble negación corresponde a la continuación de paso estilo, 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 para un lenguaje funcional Turing-completo es inconsistente. La recursividad no tiene correspondencia en teorías consistentes. En una lógica inconsistente / teoría de prueba no sólida se podría llamar una regla que causa inconsistencia / falta de solidez.

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

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

function composition      | syllogism

Realmente me gusta esta pregunta. No se mucho, pero tengo algunas cosas (ayudada por el artículo de Wikipedia , que tiene algunas tablas ordenadas y así mismo):

1. Creo que los tipos de suma/tipos de unión ( e. g. data Either a b = Left a | Right b) son equivalentes a inclusive 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 (un ∧ b) → (un ★ b) y la definición dice que esto es cierto, donde ★ es inclusivo o exclusivo o, lo que Either representa. Usted tiene Either representación exclusiva o, ⊕; sin embargo, (un ∧ b) ↛ (un ⊕ b). Por ejemplo,⊤ ∧ ⊤ ≡ ⊤, pero but, y⊤ ↛ ⊥. En otras palabras, si ambos a y b son verdaderos, entonces la hipótesis es verdadera pero la conclusión es falsa, y por lo tanto esta implicación debe ser falsa. Sin embargo, claramente, (un ∧ b) → (un ∨ b), ya que si ambos un y 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. Del mismo modo, sus definiciones de tautología y absurdo como la función de identidad y las funciones no terminantes, respectivamente, están un poco apagadas. La fórmula verdadera está representada por el tipo de unidad , que es el tipo que tiene un solo elemento (data ⊤ = ⊤; a menudo escrito () y/o Unit en lenguajes de programación funcionales). Esto tiene sentido: puesto que ese tipo estágarantizado para ser habitado, y puesto que solo hay un habitante posible, debe ser cierto. La función de identidad solo representa la tautología particular que a → a .

   Su comentario sobre las funciones no terminantes es, dependiendo de lo que quiso decir exactamente, más apagado. Curry-Howard funciona en el sistema de tipos, pero la no terminación no está codificada allí. De acuerdo con Wikipedia , tratar 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 un → b para cualquier ay b). Si esto es lo que querías decir con "absurdo", entonces estás exactamente en lo correcto. Si en su lugar se refería a la declaración falsa, entonces lo que desea en su lugar es cualquier 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 en absoluto, por lo que debe estar deshabitada, lo que equivale a false. Creo que probablemente también podría usar a -> b, ya que si prohibimos las funciones no terminantes, entonces esto también está deshabitado, pero estoy no estoy 100% seguro.

3. Wikipedia dice que los axiomas están codificados de dos maneras diferentes, dependiendo de cómo interpretes Curry-Howard: ya sea en los combinadores o en las variables. Creo que la vista combinator 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 yo creo que la vista variable puede significar lo mismo los combinadores de cosas, 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.

4. De Acuerdo a mi lógica y la semántica de la clase, el hecho de que (un ∧ b) → c ≡ un → (b → c) (y también que b → (a → c )) se llama la ley de equivalencia de exportación, al menos en las pruebas de deducción natural. No me di cuenta en ese momento de que solo estaba curando-Ojalá lo hubiera hecho, porque eso es genial!

5. Mientras que ahora tenemos una manera de representar la disyunción inclusiva, no tenemos una manera de representar la variedad exclusiva. Deberíamos poder utilizar la definición de disyunción exclusiva para representarla: un ⊕ b ≡ (un ∨ b) ∧ (un ∧ b). No se como escribir negación, pero si se que p ≡ p→→, y tanto la implicación como la falsedad son fáciles. Por lo tanto, debemos poder representar la disyunción exclusiva por:

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

   Esto define ⊥ como el tipo vacío sin valores, que corresponde a falsedad; Xor se define entonces para contener ambos ( y) Either an a o a b (o) y una función (implicación) de (a,b) (y) para el fondo tipo (false). Sin embargo, no tengo idea de lo que esto significa. (Editar 1: Ahora lo hago, ver el siguiente párrafo!) , Puesto que no hay valores de tipo (a,b) -> ⊥ (hay?), no puedo entender lo que esto significaría en un programa. ¿Alguien conoce una mejor manera de pensar acerca de esta definición u otra? (Editar 1: Sí, camccann.)

   Edit 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 testigo de la existencia de un elemento de a o b como primer argumento; es decir, a Left a o a Right b. Y en segundo lugar, una prueba de que no hay elementos de ambos tipos a y b - en en otras palabras, una prueba de que (a,b) está deshabitada-como segundo argumento. Dado que solo podrás escribir una función desde (a,b) -> ⊥ si (a,b) está deshabitada, ¿qué significa que sea así? Eso significaría que alguna parte de un objeto de tipo (a,b) no podría ser construido; 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 es posible que coincidan patrones en una tupla: suponiendo que b está deshabitado, ¿qué escribiríamos que pudiera coincidir con la segunda parte de esa tupla? Por lo tanto, no podemos hacer coincidir el patrón con él, lo que puede ayudarte a ver por qué esto lo hace deshabitado. Ahora, la única manera de tener una función total que no toma argumentos (como ésta debe, ya que (a,b) está deshabitada) es 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 a pesar de que la función no tiene casos, no hay ningún cuerpo posible que pudiera tener cualquiera de los dos, 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 ningún tipo de detalle, pero sus tablas son un resumen muy agradable, y es muy completo.

Aquí hay uno ligeramente 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 seas un filósofo, matemático o programador funcional obsesivo, esto probablemente te lleve a 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 tiempos 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 entonces 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. Ratón la posición es un gran ejemplo: es solo un comportamiento de coordenadas x, y. Después de todo, el ratón siempre tiene una posición y, conceptualmente, esta posición cambia continuamente a medida que mueve el ratón. Después de todo, mover el ratón 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 en el tiempo. Esencialmente, extiende la lógica normal de primer orden con dos cuantificadores: □ y ◇. El primero significa "siempre": léase □φ como "φ siempre tiene". El segundo es "eventualmente": φ φ significa que "φ eventualmente se mantendrá". Este es un tipo particular de lógica modal . Las dos leyes siguientes relacionan los cuantificadores:

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

Así que □ y ◇ son duales el uno al otro 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 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 call/cc es la ley de Peirce http://en.wikipedia.org/wiki/Call-with-current-continuation

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

Aunque no es un simple isomorfismo, esta discusión del LEM constructivo es un resultado muy interesante. En particular, en la sección de conclusión, Oleg Kiselyov discute 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 decidibles computacionalmente (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 Howard ayuda a ponerlo en perspectiva y ayuda a llegar a lo que la doble negación 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-old/handouts / callcc.pdf

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 (continuaciones que toman 2 parámetros) y Sheffer stroke. En la lógica clásica, Sheffer stroke puede formar un sistema lógico completo por sí mismo (además de algunos conceptos que no son operadores). Lo que significa lo familiar and, or, not se puede implementar usando 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 puede utilizar para formar todos los otros tipos.

La firma de tipo de una continuación 2 es (a,b) -> Void. Con esta implementación podemos definir 1-continuation (continuaciones normales) como (a,a) -> Void, product type como ((a,b)->Void,(a,b)->Void)->Void, sum type como ((a,a)->Void,(b,b)->Void)->Void. Esto nos da una impresionante de su poder de expresividad.

Si profundizamos más, descubriremos que el gráfico existencial de la pieza es equivalente a un lenguaje con el único tipo de datos es n-continuación, pero no lo hice ver cualquier idioma existente está en este formulario. Así que inventar uno podría ser interesante, creo.