Quels sont les plus intéressants provenant des équivalences du Curry-Howard Isomorphisme?

Question

Je suis venu sur le Isomorphisme Curry-Howard relativement tard dans mon la vie de la programmation, et peut-être ce qui contribue à mon être tout à fait fasciné par elle. Cela implique que pour chaque concept de programmation, il existe un analogue précis dans la logique formelle, et vice versa. Voici une liste « de base » de ces analogies, du haut de ma tête:

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

Alors, à ma question: Quelles sont quelques-unes des conséquences les plus intéressantes / obscures de cet isomorphisme Je ne suis pas logicien donc je suis sûr que je ne l'ai gratté la surface avec cette liste .

Par exemple, voici quelques notions de programmation dont je ne connais pas les noms de lapidaires dans la logique:

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

Et voici quelques concepts logiques que je ne l'ai pas tout à fait épinglé en termes de programmation:

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

Edit:

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

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

Answer 1

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

Vous pouvez étendre C-H à plusieurs logiques intéressantes et des formulations de logiques pour obtenir une très grande variété de correspondances. Ici, j'ai essayé de me concentrer sur quelques-uns des plus intéressants plutôt que sur l'obscur, plus deux ou trois les fondamentaux qui n'ont pas encore trouvé.

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

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

"A Judgemental reconstruction de Modal Logic" http: //www.cs .cmu.edu / ~ fp / papiers / mscs00.pdf - c'est un excellent endroit pour commencer, car il commence à partir des principes et une grande partie est destinée à être accessible aux non-logiciens / théoriciens de la langue. (Je suis le deuxième auteur, donc je suis partial.)

Answer 2

Vous choses brouillant un peu en ce qui concerne nontermination. Falsity est représenté par types inhabitées , qui par définition ne peut pas être non-terminaison parce qu'il n'y a rien de ce type d'évaluer en premier lieu.

Non terminaison représente contradiction - une logique incohérente. Une logique incohérente sera bien sûr vous permettra de prouver quoi que ce soit , y compris faux, cependant.

En ignorant les incohérences, les systèmes de type correspondent généralement à une logique intuitionniste , et sont par nécessité constructiviste , ce qui signifie que certains morceaux de la logique classique ne peuvent être exprimées directement, le cas échéant. D'autre part ce qui est utile, parce que si un type est une preuve constructive valide, un terme de ce type est un moyens de construire ce que vous avez prouvé l'existence de .

Une caractéristique importante de la saveur constructiviste est que double négation n'est pas équivalent à la non-négation. En fait, la négation est rarement une primitive dans un système de type, donc au lieu que nous pouvons le représenter comme impliquant le mensonge, par exemple, not P devient P -> Falsity. double négation serait donc une fonction de type (P -> Falsity) -> Falsity, ce qui est évidemment pas équivalent à quelque chose d'un peu de type P.

Cependant, il y a une tournure intéressante à ce sujet! Dans un langage avec polymorphisme paramétrique, les variables de type couvrent tous les types possibles, y compris inhabités, donc un type entièrement polymorphes, comme ∀a. a est, dans un certain sens, presque faux. Alors, que si nous écrivons presque le double négation en utilisant polymorphisme? Nous obtenons un type qui ressemble à ceci: ∀a. (P -> a) -> a. Est-ce équivalent à quelque chose de type P? En effet, il est , ne font qu'appliquer à la fonction d'identité.

Mais quel est le point? Pourquoi écrire un type comme ça? Est-il mean quoi que ce soit en termes de programmation? Eh bien, vous pouvez penser en fonction qui a déjà quelque chose de quelque part le type de P, et a besoin de vous pour lui donner une fonction qui prend P comme argument, le tout étant polymorphes dans le type de résultat final. Dans un sens, il représente un calcul en suspension , en attendant le reste à fournir. En ce sens, ces calculs en suspension peuvent être composés ensemble, circulaient, invoqué, peu importe. Cela devrait commencer à sembler familier aux fans de certaines langues, comme Scheme ou Ruby - parce que cela signifie est que double négation correspond à le style passage de continuation , et en fait le type I donné ci-dessus est exactement la monade de continuation dans Haskell.

Answer 3

Votre tableau n'est pas tout à fait raison; dans de nombreux cas, vous avez confondu types avec des 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 | 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 logique d'un langage fonctionnel Turing-complet est incompatible. Récursivité n'a pas de correspondance dans les théories cohérentes. Dans une théorie logique incohérente / preuve mal fondée, vous pouvez l'appeler une règle qui entraîne l'incohérence / inconsistance.

[2] Encore une fois, ceci est une conséquence de l'exhaustivité. Ce serait une preuve d'un anti-théorème si la logique était cohérente -. Par conséquent, il ne peut exister

[3] n'existe pas dans les langages fonctionnels, car ils élident de premier ordre logique caractéristiques: tous quantification et paramétrisation se fait sur des formules. Si vous aviez des fonctionnalités de premier ordre, il y aurait une autre espèce que *, * -> *, etc .; le genre d'éléments du domaine du discours. Par exemple, dans Father(X,Y) :- Parent(X,Y), Male(X), X et la gamme de Y sur le domaine du discours (appellent Dom) et Male :: Dom -> *.

Answer 4

function composition      | syllogism

Answer 5

Je aime vraiment cette question. Je ne sais pas beaucoup, mais j'ai quelques petites choses (aidés par l'article de Wikipedia , qui a quelques tables soignées et comme lui-même):

1. Je pense que les types de somme / types syndicaux ( par exemple. data Either a b = Left a | Right b) sont équivalentes à inclus disjunction. Et, bien que je pense pas que je connais très bien Curry-Howard, cela démontre. Considérez la fonction suivante:

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

   Si je comprends bien les choses, le type dit que ( a ? b ) ? ( a ? b ) et la définition dit que cela est vrai, où est ? soit inclusif ou exclusif ou, selon Either représente. Vous avez Either représentant exclusif ou, ?; cependant, ( a ? b ) ? ( a ? b ). Par exemple, ? ? ? = ?, mais ? ? ? = ? et ? ? ?. En d'autres termes, si les deux a et b sont vraies, alors l'hypothèse est vraie, mais la conclusion est fausse, et donc cette implication doit être fausse. Cependant, il est clair ( a ? b ) ? ( a ? b ), car si les deux un et b sont vraies, alors au moins un est vrai. Ainsi, si les syndicats sont victimes de discrimination une certaine forme de disjonction, ils doivent être inclus la variété. Je pense que cela est comme une preuve, mais je me sens plus à me détromper de cette notion.

2. De même, vos définitions pour tautologie et absurde que la fonction d'identité et les fonctions non-terminaison, respectivement, sont un peu hors. La véritable formule est représenté par la type d'unité , qui est du type qui ne comporte qu'un seul élément (data ⊤ = ⊤; () souvent écrit et / ou Unit dans les langages de programmation fonctionnels). Cela est logique: puisque ce type est garantie peuplera, et puisqu'il n'y a qu'un seul habitant possible, il doit être vrai. La fonction d'identité ne représente que la tautologie particulière que a ? a .

   Votre commentaire sur les fonctions non-terminaison est, en fonction de ce que vous vouliez dire précisément, plus large. fonctions Curry-Howard sur le système de type, mais non de terminaison ne sont pas codées là. Selon Wikipedia , traitant de la non-dénonciation est un problème, car l'ajouter produit incompatible logiques ( par exemple , je peux définir wrong :: a -> b par wrong x = wrong x, et donc « prouver » que a ? b pour tout a et b ). Si c'est ce que vous entendez par « absurdité », alors vous êtes tout à fait correct. Si, au lieu que vous vouliez dire la fausse déclaration, alors ce que vous voulez est plutôt tout type inhabitée, par exemple. quelque chose défini par data ⊥ qui est un type de données sans aucun moyen de le construire. Cela garantit qu'il n'a pas de valeur du tout, et il doit donc être inhabitée, ce qui équivaut à faux. Je pense que vous pouvez probablement utiliser aussi a -> b, car si nous interdisons les fonctions non-terminaison, cela est aussi inhabitée, mais je ne suis pas sûr à 100%.

3. Wikipédia dit que les axiomes sont codés de deux façons différentes, selon sur la façon dont vous interprétez Curry-Howard: soit dans les combinateurs ou dans les variables. Je pense que les moyens de vue Combinator que les fonctions primitives nous encode les choses que nous donnés pouvons dire par défaut (similaire à la façon dont modus ponens est un axiome parce que l'application de la fonction est primitive). Et je pense que la vue variable peut en fait dire la même chose-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 objets primitifsque nous essayons de prouver des choses au sujet.

4. Selon ma logique et la classe sémantique, le fait que ( a ? b ) ? c = a ? ( b ? c ) (et que b ? ( a ? c )) est appelée la loi d'équivalence d'exportation, au moins dans les preuves de déduction naturelle. Je n'ai pas remarqué au moment où il était juste Currying-je voudrais avoir, parce que ce cool!

5. Alors que nous avons maintenant une façon de représenter inclus disjunction, nous n'avons pas une façon de représenter la variété exclusive. Nous devrions être en mesure d'utiliser la définition de disjonction exclusive pour le représenter: a ? b = ( a ? b ) ? ¬ ( a ? b ). Je ne sais pas comment la négation d'écriture, mais je sais que ¬ p = p ? ?, et à la fois l'implication et le mensonge sont faciles. Nous devrions donc en mesure de représenter disjonction exclusive par:

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

   Ceci définit ⊥ être le type vide sans valeurs, ce qui correspond à faux; Xor est alors définie pour contenir à la fois ( et ) Either un a ou b ( ou ) et une fonction ( implication ) de (a, b) ( et ) au type de fond ( false ). Cependant, je ne sais pas ce que cela signifie . ( Edit 1: Maintenant je, voir le paragraphe suivant) Comme il sont pas des valeurs de type (a,b) -> ⊥ (sont là?), je ne comprends pas ce que cela signifierait dans un programme. Est-ce que quelqu'un sait une meilleure façon de penser soit cette définition ou un autre ( Modifier 1: Oui, camccann .)

   Modifier 1: Merci réponse de camccann (plus particulièrement, les commentaires qu'il a laissé sur elle pour me aider), je pense que je vois ce qui se passe ici. Pour construire une valeur de type Xor a b, vous devez fournir deux choses. Tout d'abord, un témoin de l'existence d'un élément de l'une ou a b comme premier argument; soit un Left a ou un Right b. Et deuxièmement, une preuve qu'il n'y a pas des éléments des deux types a et b-à-dire une preuve que (a,b) est inhabitée, comme le second argument. Puisque vous ne serez en mesure d'écrire une fonction de (a,b) -> ⊥ si (a,b) est inhabitée, qu'est-ce que cela signifie pour que ce soit le cas? Cela signifierait qu'une partie d'un objet de type (a,b) n'a pas pu être construit; autrement dit, au moins un, et peut-être les deux, et a b sont inhabitées aussi! Dans ce cas, si nous réfléchissons sur la correspondance de motif, vous ne pouviez pas éventuellement motif match sur un tel tuple: en supposant que b est inhabitée, qu'aurions-nous écrire qui pourrait correspondre à la deuxième partie de ce tuple? Ainsi, nous ne pouvons pas correspondance de motif contre elle, ce qui peut vous aider à voir pourquoi cela rend inhabitée. Maintenant, la seule façon d'avoir une fonction totale qui ne prend aucun argument (comme celui-ci doit, car (a,b) est inhabitée) est le résultat d'être d'un trop si le type inhabitée, nous pensons à ce sujet dans une perspective ltrage , cela signifie que même si la fonction n'a pas cas, il n'y a pas possible body il aurait pu soit, et si le OK de tout.

Beaucoup de cela me pense des choses à haute voix / prouver (si tout va bien) à la volée, mais j'espère qu'il est utile. Je recommande vraiment laWikipedia article ; Je ne l'ai pas lu à travers elle dans toute sorte de détails, mais ses tableaux sont un résumé très agréable, et il est très complet.

Answer 6

Voici un peu obscur que je suis surpris n'a pas été soulevé plus tôt: la programmation réactive. Fonctionnelle « classique » correspond à la logique temporelle

Bien sûr, sauf si vous êtes un philosophe, mathématicien programmeur fonctionnel ou obsessionnel, cela apporte probablement plusieurs autres questions.

Alors, tout d'abord: quelle est la programmation réactive fonctionnelle? Il est une façon déclarative de travailler avec valeurs variant dans le temps . Ceci est utile pour écrire des choses comme des interfaces utilisateur parce que les entrées de l'utilisateur sont des valeurs qui varient au fil du temps. FRP « classique » dispose de deux types de données de base: les événements et les comportements.

événements représentent des valeurs qui existent seulement à des moments discrets. Sont un excellent combinaisons de touches exemple: vous pouvez penser des 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 clé et le temps qu'il a été pressé.

Behaviors sont des valeurs qui existent en permanence, mais peuvent être en train de changer en permanence. La position de la souris est un excellent exemple: il est juste un comportement de coordonnées x, y. Après tout, la souris toujours a une position et, sur le plan conceptuel, cette situation change en permanence que vous vous déplacez la souris. Après tout, le déplacement de la souris est une seule action prolongée, pas un tas d'étapes distinctes.

Et quelle est la logique temporelle? Assez convenablement, il est un ensemble de règles logiques pour faire face aux propositions quantifiées au fil du temps. Pour l'essentiel, il étend la logique normale de premier ordre avec deux quantificateurs: ? et ?. La première signifie « toujours »: lecture ? f comme « f détient toujours ». Le second est « finalement »: ? f signifie que « f finira par tenir ». Ceci est un type particulier de modale logique. Les deux lois suivantes concernent les quantificateurs:

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

? et ? sont deux à l'autre de la même manière que ? et ?.

Ces deux quantificateurs correspondent aux deux types en matériaux composites. En particulier, ? correspond à des comportements et ? correspond à des événements. Si nous pensons à la façon dont ces types sont habitées, cela devrait donner un sens: un comportement est habité à tous temps possible, alors qu'un événement se produit qu'une seule fois.

Answer 7

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

C-H est généralement indiqué que la correspondance entre la logique intuitionniste et les programmes. Toutefois, si l'on ajoute l'opérateur d'appel avec-continuation actuelle (callcc) (dont correspond le type à la loi de Peirce), nous obtenons une correspondance entre logique classique et des programmes avec callcc.

Answer 8

Bien que ce n'est pas un isomorphisme simple, cette discussion de LEM constructive est très résultat intéressant. En particulier, dans la section de conclusion, Oleg Kiselyov explique comment l'utilisation des monades pour obtenir l'élimination double négation dans une logique constructive est analogue à distinguer les propositions informatiquement décidables (pour laquelle LEM est valable dans un cadre constructif) de toutes les propositions. La notion que les monades capture des effets de calcul est un ancien, mais cette instance de Curry -. Howard aide isomorphie mettre en perspective et aide à obtenir à ce que double négation vraiment « signifie »

Answer 9

Prise en charge des 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 poursuite et la sortie avec une certaine expression équivaut à appeler la suite avec cette même expression.

Pour plus détaillée s'il vous plaît voir: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

Answer 10

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

Une chose qui est important, mais pas encore l'objet d'enquêtes est la relation de 2-continuation (continuations qui prend 2 paramètres) et Sheffer temps. Dans la logique classique, la course Sheffer peut former un système logique complet par lui-même (ainsi que quelques concepts non exploitants). Ce qui signifie que le and familier, or, not peut être mis en œuvre en utilisant uniquement le stoke Sheffer ou nand.

Ceci est un fait important de sa correspondance type de programmation, car il demande qu'un seul type combinateur peut être utilisé pour former tous les autres types.

La signature type d'un 2-poursuite est (a,b) -> Void. Par cette mise en œuvre, nous pouvons définir 1 suite (de continuations normale) comme (a,a) -> Void, type de produit ((a,b)->Void,(a,b)->Void)->Void, type somme que ((a,a)->Void,(b,b)->Void)->Void. Cela nous donne une impressionnante puissance de son expressivité.

Si nous creuser plus loin, nous allons découvrir que Piece est graphique existentiel est équivalent à un langue avec le seul type de données est n-poursuite, mais je ne vois pas toutes les langues existantes est sous cette forme. Donc, on pourrait inventer être intéressant, je pense.