Quelles sont les équivalences les plus intéressantes de l’isomorphisme Curry-Howard?

Je suis tombé sur l’ isomorphisme Curry-Howard relativement tard dans ma vie de programmation, et cela consortingbue peut-être à ce que je sois fasciné par cet isomorphisme . Cela implique que pour chaque concept de programmation, il existe un analogue précis dans la logique formelle et inversement. Voici une liste “de base” de ces analogies:

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 SZ paramesortingc polymorphism | universal quantification 

Donc, à ma question: quelles sont certaines des implications les plus intéressantes / obscures de cet isomorphisme? Je ne suis pas logicien donc je suis sûr que je n’ai fait qu’effleurer la surface avec cette liste.

Par exemple, voici quelques notions de programmation pour lesquelles je ne connais pas de noms épineux en logique:

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

Et voici quelques concepts logiques que je n’ai pas encore bien définis en termes de programmation:

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

Modifier:

Voici quelques autres équivalences recueillies à partir des réponses:

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

Puisque vous avez explicitement demandé les plus intéressants et les plus obscurs:

Vous pouvez étendre CH à de nombreuses logiques et formulations de logiques intéressantes pour obtenir une très grande variété de correspondances. Ici, j’ai essayé de me concentrer sur certains des plus intéressants plutôt que sur l’obscur, en plus de quelques aspects fondamentaux qui n’ont pas encore été abordés.

 evaluation | proof normalisation/cut-elimination variable | assumption SK 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 dissortingbuted programs | modal logic S5/Hybrid logic meta variables | modal assumptions explicit substitutions | contextual modal necessity pi-calculus | linear logic 

EDIT: Une référence que je recommande à tous ceux qui souhaitent en savoir plus sur les extensions de CH:

“Reconstruction Judiciaire de la Logique Modale” http://www.cs.cmu.edu/~fp/papers/mscs00.pdf – c’est un bon sharepoint départ car il part des premiers principes et une grande partie est destinée à être accessible aux non-logiciens / théoriciens des langues. (Je suis le deuxième auteur cependant, donc je suis partial).

Vous brouillez les choses un peu en ce qui concerne la non-révolte. La fausseté est représentée par des types inhabités , qui, par définition, ne peuvent pas se terminer car il n’y a rien de ce type à évaluer en premier lieu.

La non-résiliation représente une contradiction – une logique incohérente. Une logique incohérente vous permettra bien sûr de prouver quoi que ce soit , y compris la fausseté.

En ignorant les incohérences, les systèmes de types correspondent généralement à une logique intuitionniste et sont nécessairement constructivistes , ce qui signifie que certains éléments de la logique classique ne peuvent pas être exprimés directement, voire pas du tout. D’un autre côté, cela est utile, car si un type est une preuve constructive valable, un terme de ce type est un moyen de construire ce dont vous avez prouvé l’existence .

Une caractéristique majeure de la saveur constructiviste est que la double négation n’est pas équivalente à la non-négation. En fait, la négation est rarement une primitive dans un système de types, de sorte que nous pouvons au contraire la représenter comme impliquant le mensonge, par exemple, not P devient pas P -> Falsity . La double négation serait donc une fonction de type (P -> Falsity) -> Falsity , qui n’est évidemment pas équivalente à quelque chose de simplement tapez P

Cependant, il y a une tournure intéressante à ce sujet! Dans un langage avec polymorphism paramésortingque, les variables de type couvrent tous les types possibles, y compris les types inhabités, donc un type entièrement polymorphe tel que ∀a. a ∀a. a est en quelque sorte presque-faux. Alors que se passe-t-il si nous écrivons une double quasi-négation en utilisant le polymorphism? Nous obtenons un type qui ressemble à ceci: ∀a. (P -> a) -> a ∀a. (P -> a) -> a . Est-ce équivalent à quelque chose de type P ? En effet, il suffit de l’appliquer à la fonction identité.

Mais à quoi ça sert? Pourquoi écrire un type comme ça? Cela signifie- t-il quelque chose en termes de programmation? Eh bien, vous pouvez le voir comme une fonction qui a déjà quelque chose de type P quelque part, et vous devez lui donner une fonction qui prend P comme argument, le tout étant polymorphe dans le type de résultat final. En un sens, cela représente un calcul suspendu , en attendant que le rest soit fourni. En ce sens, ces calculs suspendus peuvent être composés ensemble, contournés, invoqués, peu importe. Cela devrait sembler familier aux fans de certaines langues, comme Scheme ou Ruby – parce que cela signifie que la double-négation correspond au style de continuation-continuation , et en fait le type que j’ai donné ci-dessus est exactement la monade de continuation dans Haskell.

Votre tableau n’est pas tout à fait correct. dans de nombreux cas, vous avez confondu les types avec les termes.

 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 | SN) 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 paramesortingc 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 logique d’un langage fonctionnel Turing-complet est incohérente. La récursivité n’a pas de correspondance dans les théories cohérentes. Dans une logique incohérente de logique / preuve infondée, vous pourriez l’appeler une règle qui provoque des incohérences / des faiblesses.

[2] Encore une fois, ceci est une conséquence de la complétude. Ce serait une preuve d’un anti-théorème si la logique était cohérente – ainsi, elle ne peut pas exister.

[3] N’existe pas dans les langages fonctionnels, car ils éliminent les fonctions logiques de premier ordre: toute quantification et paramésortingsation se fait sur des formules. Si vous aviez des fonctionnalités de premier ordre, il y en aurait une autre que * , * -> * , etc. le genre d’éléments du domaine du discours. Par exemple, dans Father(X,Y) :- Parent(X,Y), Male(X) , X et Y compris dans le domaine du discours (appelez-le Dom ) et Male :: Dom -> * .

 function composition | syllogism 

J’aime vraiment cette question. Je ne connais pas grand chose, mais j’ai quelques petites choses (aidé par l’article de Wikipedia , qui contient des tables bien rangées et autres):

  1. Je pense que les types de sum / types d’union ( par exemple, les data Either ab = Left a | Right b ) sont équivalentes à une disjonction inclusive . Et bien que je ne connaisse pas très bien Curry-Howard, je pense que cela le démontre. Considérons la fonction suivante:

     andImpliesOr :: (a,b) -> Either ab andImpliesOr (a,_) = Left a 

    Si je comprends bien les choses, le type dit que ( ab ) → ( ab ) et la définition dit que ceci est vrai, où ★ est inclusif ou exclusif, selon ce que l’un ou l’ Either représente. Vous avez Either exclusif ou, ⊕; cependant, ( ab ) ↛ ( ab ). Par exemple, ⊤ ∧ ⊤ ≡ ⊤, mais ⊤ ⊕ ⊥ ≡ ⊥ et ⊤ ↛ ⊥. En d’autres termes, si a et b sont tous deux vrais, l’hypothèse est vraie mais la conclusion est fausse et cette implication doit donc être fausse. Cependant, clairement, ( ab ) → ( ab ), puisque si a et b sont vrais, alors au moins un est vrai. Ainsi, si les unions discriminées sont une forme de disjonction, elles doivent être la variété inclusive. Je pense que cela constitue une preuve, mais je suis plus que libre de me désabuser de cette notion.

  2. De même, vos définitions de la tautologie et de l’absurdité en tant que fonction d’identité et fonctions de non-terminaison, respectivement, sont un peu décalées. La vraie formule est représentée par le type d’unité , qui est le type qui ne comporte qu’un seul élément ( data ⊤ = ⊤ ; souvent orthographié () et / ou Unit dans les langages de programmation fonctionnels). Cela a du sens: puisque ce type est assuré d’être habité et qu’il n’y a qu’un seul habitant possible, cela doit être vrai. La fonction identité ne représente que la tautologie particulière aa .

    Votre commentaire sur les fonctions non terminées est, en fonction de ce que vous vouliez dire, plus large. Curry-Howard fonctionne sur le système de type, mais la non-résiliation n’y est pas codée. Selon Wikipedia , traiter la non-résiliation est un problème, car l’append produit des logiques incohérentes ( par exemple , je peux définir wrong :: a -> b par un wrong x = wrong x , et donc «prouver» qu’un → b pour tout a et b ). Si c’est ce que vous entendiez par «absurdité», alors vous avez tout à fait raison. Si au lieu de cela vous vouliez dire la déclaration fausse, alors vous voulez plutôt un type inhabité, par exemple quelque chose défini par data ⊥ c’est-à-dire un type de données sans aucun moyen de le construire. Cela garantit qu’il n’a aucune valeur et qu’il doit donc être inhabité, ce qui équivaut à false. Je pense que vous pourriez probablement aussi utiliser a -> b , car si nous interdisons les fonctions qui ne sont pas terminées, cela est également inhabité, mais je ne suis pas sûr à 100%.

  3. Wikipedia dit que les axiomes sont encodés de deux manières différentes, selon la manière dont vous interprétez Curry-Howard: soit dans les combinateurs, soit dans les variables. Je pense que la vue combinatoire signifie que les fonctions primitives que nous recevons codent les choses que nous pouvons dire par défaut (similaire à la façon dont le modus ponens est un axiome car l’application de la fonction est primitive). Et je pense que la vue des variables peut en réalité signifier la même chose: les combinateurs, après tout, ne sont que des variables globales qui sont des fonctions particulières. En ce qui concerne les types primitifs: si je pense à cela correctement, alors je pense que les types primitifs sont les entités – les objects primitifs sur lesquels nous essayons de prouver des choses.

  4. Selon ma classe de logique et de sémantique, le fait que ( ab ) → ca → ( bc ) (et aussi que b → ( ac )) est appelé loi d’équivalence d’exportation, au moins en déduction naturelle preuves. Je n’avais pas remarqué à ce moment-là que c’était juste le curry — j’aurais aimé l’avoir, parce que c’est cool!

  5. Bien que nous ayons maintenant un moyen de représenter la disjonction inclusive , nous n’avons aucun moyen de représenter la variété exclusive. Nous devrions pouvoir utiliser la définition de la disjonction exclusive pour la représenter: ab a ( ab ) ∧ ¬ ( ab ). Je ne sais pas comment écrire la négation, mais je sais que ¬ pp → ⊥ et l’implication et le mensonge sont faciles. Nous devrions donc pouvoir représenter une disjonction exclusive par:

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

    Cela définit comme étant le type vide sans valeur, ce qui correspond à la fausseté; Xor est alors défini pour contenir à la fois ( et ) Either un a ou un b ( ou ) et une fonction ( implication ) de (a, b) ( et ) au type inférieur ( false ). Cependant, je n’ai aucune idée de ce que cela signifie . ( Edit 1: Maintenant je le fais, voir le paragraphe suivant!) Comme il n’y a pas de valeurs de type (a,b) -> ⊥ (y a-t-il?), Je ne peux pas comprendre ce que cela signifierait dans un programme. Est-ce que quelqu’un connaît une meilleure façon de penser à cette définition ou à une autre? ( Edit 1: Oui, camccann .)

    Edit 1: Grâce à la réponse de camccann (plus particulièrement, les commentaires qu’il a laissés pour m’aider), je pense voir ce qui se passe ici. Pour construire une valeur de type Xor ab , vous devez fournir deux éléments. Tout d’abord, un témoin de l’existence d’un élément de soit a ou b comme premier argument; c’est-à-dire une Left a ou une Right b . Et deuxièmement, une preuve qu’il n’y a pas d’éléments des deux types a et b – en d’autres termes, une preuve que (a,b) est inhabité – comme second argument. Puisque vous ne pourrez écrire une fonction que de (a,b) -> ⊥ si (a,b) est inhabité, que signifie-t-il pour que cela soit le cas? Cela voudrait dire qu’une partie d’un object de type (a,b) ne pourrait pas être construite; en d’autres termes, au moins un, et peut-être les deux, de a et b sont également inhabités! Dans ce cas, si nous pensons à la correspondance de motifs, vous ne pourriez probablement pas faire de correspondance avec un tel tuple: en supposant que b soit inhabité, qu’est-ce qui pourrait correspondre à la seconde partie de ce tuple? Par conséquent, nous ne pouvons pas créer de correspondance avec ce modèle, ce qui peut vous aider à comprendre pourquoi cela le rend inhabité. Maintenant, la seule façon d’avoir une fonction totale qui ne prend pas d’arguments (comme celui-ci doit l’être, puisque (a,b) est inhabité) est que le résultat soit aussi inhabité – si nous pensons à cela à partir d’un perspective de correspondance de modèle, cela signifie que même si la fonction n’a pas de cas, il n’y a pas de corps possible, et donc tout va bien.

Une grande partie de ce que je pense à haute voix / prouver (espérons) des choses à la volée, mais j’espère que c’est utile. Je recommande vraiment l’article de Wikipedia ; Je ne l’ai pas lu dans le moindre détail, mais ses tableaux sont un très bon résumé, et c’est très complet.

Voici une version un peu obscure qui n’a pas été abordée plus tôt: la programmation réactive fonctionnelle «classique» correspond à la logique temporelle.

Bien sûr, à moins d’être philosophe, mathématicien ou programmeur fonctionnel obsessionnel, cela soulève probablement plusieurs autres questions.

Donc, tout d’abord: qu’est-ce qu’une programmation réactive fonctionnelle? C’est une façon déclarative de travailler avec des valeurs variables dans le temps . Ceci est utile pour écrire des éléments tels que les interfaces utilisateur car les entrées de l’utilisateur sont des valeurs qui varient dans le temps. “Classique” FRP a deux types de données de base: les événements et les comportements.

Les événements représentent des valeurs qui n’existent qu’à des moments discrets. Les frappes sont un bon exemple: vous pouvez considérer les entrées du clavier comme un personnage à un moment donné. Chaque pression de touche est alors juste une paire avec le caractère de la touche et l’heure à laquelle elle a été pressée.

Les comportements sont des valeurs qui existent en permanence mais peuvent évoluer en permanence. La position de la souris est un bon exemple: il s’agit simplement d’un comportement des coordonnées x, y. Après tout, la souris a toujours une position et, conceptuellement, cette position change continuellement lorsque vous déplacez la souris. Après tout, le déplacement de la souris est une simple action prolongée, pas un groupe de pas discrets.

Et quelle est la logique temporelle? À juste titre, il s’agit d’un ensemble de règles logiques pour traiter les propositions quantifiées au fil du temps. Essentiellement, il étend la logique normale du premier ordre avec deux quantificateurs: □ et ◇. Le premier signifie “toujours”: lisez φ comme “holds tient toujours”. Le second est “finalement”: φ φ signifie que “φ finira par tenir”. C’est un type particulier de logique modale . Les deux lois suivantes concernent les quantificateurs:

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

Donc, □ et ◇ sont identiques les uns aux autres de la même manière que ∀ et ∃.

Ces deux quantificateurs correspondent aux deux types de FRP. En particulier, □ correspond aux comportements et ◇ correspond aux événements. Si nous pensons à la façon dont ces types sont habités, cela devrait avoir un sens: un comportement est habité à tout moment, tandis qu’un événement ne se produit qu’une fois.

Relatif à la relation entre les continuations et la double négation, le type d’appel / cc est la loi de Peirce http://en.wikipedia.org/wiki/Call-with-current-continuation

CH est généralement indiqué comme une correspondance entre la logique intuitionniste et les programmes. Cependant, si nous ajoutons l’opérateur call-with-current-continuation (callCC) (dont le type correspond à la loi de Peirce), nous obtenons une correspondance entre la logique classique et les programmes avec callCC.

Bien que ce ne soit pas un simple isomorphisme, cette discussion sur le LEM constructif est un résultat très intéressant. En particulier, dans la section de conclusion, Oleg Kiselyov explique comment l’utilisation des monades pour obtenir une élimination de la double négation dans une logique constructive est analogue à la distinction des propositions décidables par calcul (pour lesquelles LEM est valide dans un contexte constructif) de toutes les propositions. L’idée que les monades capturent les effets du calcul est ancienne, mais cet exemple de l’isomorphisme Curry-Howard permet de le mettre en perspective et aide à comprendre ce que signifie réellement la double négation.

Le support de continuations de première classe vous permet d’exprimer $ P \ lor \ neg P $. L’astuce est basée sur le fait que ne pas appeler la suite et sortir avec une expression équivaut à appeler la suite avec cette même expression.

Pour plus de détails, veuillez consulter: 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 

Une chose qui est importante, mais qui n’a pas encore été étudiée, est la relation de 2-continuation (suites qui prennent 2 parameters) et le trait de Sheffer . Dans la logique classique, le trait de Sheffer peut constituer un système logique complet par lui-même (plus quelques concepts non-opérateurs). Ce qui signifie que le familier and or not peut not être implémenté en utilisant uniquement le stoke ou le nand Sheffer.

Ceci est un fait important de sa correspondance de type de programmation car il demande qu’un combinateur de type unique puisse être utilisé pour former tous les autres types.

La signature de type d’une suite double est (a,b) -> Void . Par cette implémentation on peut définir 1-continuation (continuations normales) comme (a,a) -> Void, type de produit comme ((a,b)->Void,(a,b)->Void)->Void , sum tapez comme ((a,a)->Void,(b,b)->Void)->Void . Cela nous donne un impressionnant pouvoir d’expression.

Si nous creusons plus loin, nous découvrirons que le graphe existentiel de Piece est équivalent à un langage dont le seul type de données est n-continuation, mais je n’ai vu aucun langage existant sous cette forme. Donc, en inventer un pourrait être intéressant, je pense.