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

97

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
Tom Crockett
fuente
cierre ~ = conjunto de axiomas
Apocalipsis
+1 Esta pregunta y todas las respuestas y comentarios de calidad me enseñaron más sobre CHI de lo que pude aprender a través de Internet.
Alexandre C.
24
@Paul Nathan:goto | jumping to conclusions
Joey Adams
Creo que el conjunto de todos los programas válidos sería un modelo
Daniil
1
fst / snd | eliminación de conjunción, izquierda / derecha | introducción de disyunción
Tony Morris

Respuestas:

33

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).

RD1
fuente
gracias por proporcionar algunos ejemplos menos triviales (que realmente era el espíritu de la pregunta original), aunque admito que varios de estos están sobre mi cabeza ... ¿los términos "necesidad" y "posibilidad" están definidos con precisión en lógica? ¿Cómo se traducen a sus equivalentes computacionales?
Tom Crockett
2
Puedo señalar artículos publicados para cada uno de estos, por lo que están definidos con precisión. La lógica modal se ha estudiado mucho (desde Aristóteles) y relaciona diferentes modos de verdad: "A es necesariamente verdadero" significa "en todos los mundos posibles A es verdadero", mientras que "A es posiblemente verdadero" significa "A es verdadero en un mundo posible" . Puede probar cosas como "(necesariamente (A -> B) y posiblemente A) -> posiblemente B". Las reglas de inferencia modal producen directamente las construcciones de expresión, las reglas de tipificación y reducción, como es habitual en CH. Ver: en.wikipedia.org/wiki/Modal_logic y cs.cmu.edu/~fp/papers/mscs00.pdf
RD1
2
@pelotom: es posible que desee leer un poco sobre otros tipos de lógica . La lógica clásica simple a menudo no es útil en este contexto; mencioné la lógica intuicionista en mi respuesta, pero la lógica modal y lineal son incluso más "extrañas", pero también realmente asombrosas.
CA McCann
1
Gracias por los consejos, ¡parece que tengo algo que leer!
Tom Crockett
2
@ RD1: Crees que eso es malo, he pasado tanto tiempo pensando en Haskell que tengo que traducir mentalmente fórmulas de lógica de predicados en firmas de tipos antes de que tengan sentido. :( Sin mencionar que la ley del medio excluido y demás comienza a parecer realmente confusa y quizás sospechosa.
CA McCann
26

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.

CA McCann
fuente
Gracias por la corrección, eliminé "falsedad" como sinónimo de no determinación. +1 para doble negación <=> CPS!
Tom Crockett
No entiendo la intuición detrás de representar ¬p como P -> Falsity. Entiendo por qué funciona (¬p ≡ p → ⊥), pero no obtengo la versión del código. P -> ⊥debe ser habitada precisamente cuando Pno lo está, ¿no? Pero, ¿no debería estar siempre habitada esta función? ¿O es posible nunca, en realidad, ya que no puede devolver una instancia de ? No veo la condicionalidad de esto. ¿Cuál es la intuición aquí?
Antal Spector-Zabusky
1
@Antal SZ: ¡La intuición es lógica intuicionista, por supuesto! Pero sí, escribir una función así es realmente difícil. Veo en su perfil que conoce a Haskell, así que tal vez esté pensando en tipos de datos algebraicos y coincidencia de patrones. Tenga en cuenta que un tipo deshabitado no debe tener constructores y, por lo tanto, no debe haber nada con lo que hacer coincidir el patrón. Tendría que escribir una "función" sin cuerpo, que no es legal Haskell. De hecho, que yo sepa, no hay forma de escribir un término de tipo negado en Haskell sin usar excepciones de tiempo de ejecución o no terminación.
CA McCann
1
@Antal SZ: Por otro lado, si la lógica equivalente es consistente, todas las funciones deben ser totales, por ejemplo, todas las coincidencias de patrones deben ser exhaustivas. Entonces, para escribir una función sin patrones, el tipo de parámetro no debe tener constructores, por ejemplo, estar deshabitado. Por lo tanto, tal función sería legal - y por lo tanto su propio tipo estaría habitada - precisamente y solo cuando su argumento esté deshabitado. Por tanto, una función P -> Falsityequivale a Pser falsa.
CA McCann
Ajá, creo que lo entiendo. La versión que había estado entreteniendo era algo así como f x = x, que sería instanciable iff P = ⊥, pero eso claramente no era lo suficientemente genérico. Entonces, la idea es que para devolver un tipo sin valor, no se necesita cuerpo; pero para que la función sea definible y total, no se necesitan estuches , y si Pestá deshabitado, ¿todo funciona? Eso es un poco extraño, pero creo que lo veo. Eso parece interactuar de manera bastante extraña con mi definición del Xortipo ... Tendré que pensar en eso. ¡Gracias!
Antal Spector-Zabusky
15

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 -> *.

Frank Atanassow
fuente
[1] - sí, debería haber sido más específico. Me refería a "recursividad estructural" en lugar de recursividad sin restricciones, que supongo que es lo mismo que "plegar". [3] - existe en idiomas de tipo dependiente
Tom Crockett
[1] El hecho es que si una llamada de función de recursividad (modus ponens) no hace que el programa no termine, los parámetros (hipótesis) dados a la llamada o al entorno DEBEN ser diferentes entre esas llamadas. Entonces, la recursividad es simplemente aplicar el mismo teorema varias veces. Si hay algo especial, suele ser números crecientes / decrecientes (paso inductivo) y verificar con un caso existente (caso base), que corresponde a - Inducción matemática en lógica.
Earth Engine
Realmente me gusta este gráfico, pero no diría "n / a", ya que la lógica consistente no es el único tipo de lógica, así como los programas de terminación no son el único tipo de programa. Una función no terminante correspondería a un "argumento circular", y es una excelente ilustración del isomorfismo de Curry-Howard: "seguir" un argumento circular lo pone en un bucle sin fin.
Joey Adams
14
function composition      | syllogism
Apocalipsis
fuente
13

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.

Antal Spector-Zabusky
fuente
1
+1 por señalar que O es inclusivo-o. Tenga en cuenta que (O aa) es un teorema (para todo a).
Apocalisp
Pregunta re. 2 (b): ¿cuál es la diferencia entre un tipo de función cuyo único habitante es no terminante y un tipo de función deshabitado? Por ejemplo, si declaro un tipo B sin constructores, luego definí una función A-> B así: fun (a: A): B: = f (a) esto se verificaría en muchos idiomas, aunque es imposible devolver una B. Así que la función está "habitada" en un sentido, pero su "habitante" es absurdo ... por lo que en realidad no está habitada en absoluto. Espero que esto tenga algún sentido :)
Tom Crockett
3
Los fondos no son pruebas. “Es absurdo e imposible suponer que lo incognoscible y lo indeterminado deba contener y determinar”. - Aristoteles
Apocalisp
2
@Tom: Solo para enfatizar el punto sobre la no terminación, si la lógica es consistente, todos los programas terminan . La no terminación solo ocurre en sistemas de tipos que representan lógicas inconsistentes o, de manera equivalente, sistemas de tipos para lenguajes completos de Turing.
CA McCann
1
Apocalipsis: Either a a no debería ser un teorema: Either ⊥ ⊥todavía está deshabitado. Tom: Como dijo Camccann, la coherencia implica la terminación. Por lo tanto, un sistema de tipos coherente no le permitirá expresarse f :: a -> b, por lo que el tipo estaría deshabitado; un sistema de tipos inconsistente tendría un habitante para el tipo, pero uno que no terminaría. camccann: ¿Hay sistemas de tipos inconsistentes que no sean Turing completos y que ocupen algún punto intermedio en la jerarquía? ¿O es ese último paso (agregar recursividad general o lo que sea) exactamente equivalente a la inconsistencia?
Antal Spector-Zabusky
12

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.

Tikhon Jelvis
fuente
8

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.

James Iry
fuente
4

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.

reyezuelo romano
fuente
4

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

Daniil
fuente
¡Gracias por esa información!
paulotorrens
4
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.

Motor de tierra
fuente