Quelles sont les équivalences plus intéressants découlant de l’isomorphisme de Curry-Howard ?

Question

Je suis tombé sur le Curry-Howard Isomorphisme relativement tard dans ma vie de programmation, et peut-être ce qui contribue à mon être totalement fasciné par elle. Elle implique que, pour chaque concept de programmation, il existe une précision analogue à la logique formelle, et vice versa. Voici une "base", la liste de ces analogies, sur le dessus 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

Donc, ma question: quels sont certains des plus intéressant/obscur implications de cet isomorphisme? Je ne suis pas un logicien, donc je suis sûr que j'ai seulement gratté la surface avec cette liste.

Pour exemple, voici quelques notions de programmation, pour lequel je suis pas au courant de lapidaire noms de logique:

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

Et voici quelques notions logiques qui je n'ai pas très bien placés 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 explicitement demandé le plus intéressant et obscures:

Vous pouvez étendre C-H à la plupart des logiques et des formules de logiques d'obtenir une très grande variété de correspondances. J'ai essayé ici de mettre l'accent sur certaines des plus intéressants plutôt que sur l'obscur, plus quelques fondamentaux de ceux qui ne l'ont pas encore.

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, je le recommande à toute personne intéressée à en apprendre plus sur les extensions de C-H:

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

Answer 2

Vous êtes troubler les choses un peu concernant nontermination. La fausseté est représenté par inhabitée types, qui, par définition, ne peut pas être non-résiliation, car il n'y a rien de ce type, pour évaluer en premier lieu.

Non-résiliation représente contradiction--pas très logique. Pas très logique sera bien sûr de vous permettre de prouver quelque chose, y compris de la fausseté, cependant.

Ignorant les incohérences, les systèmes de type généralement correspondre à une logique intuitionniste, et sont, par nécessité, constructiviste, ce qui signifie que certaines pièces de la logique classique ne peut pas être exprimé directement, si à tous. D'un autre côté c'est utile, parce que si un type est valide constructif preuve, alors un terme de ce type est un moyen de construire tout ce que vous avez prouvé l'existence d'.

Une des principales caractéristiques de l'approche constructiviste de la saveur, c'est que la double négation n'est pas équivalente à la non-négation. En fait, la négation est rarement primitive dans un système de type, donc à la place on peut la 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 n'est clairement pas l'équivalent de quelque chose de juste taper P.

Cependant, il y a une tournure intéressante sur ce! Dans un langage de polymorphisme paramétrique, les variables de type intervalle sur tous les types possibles, y compris inhabitée, donc entièrement de type polymorphe comme ∀a. a est, en un certain sens, la quasi-faux. De sorte que si nous écrivons le double de la quasi-négation par l'utilisation du polymorphisme? Nous obtenons un type qui ressemble à ceci: ∀a. (P -> a) -> a. C'est que l'équivalent de quelque chose de type P? En effet, c'estsimplement l'appliquer à la fonction identité.

Mais quel est le point? Pourquoi écrire un type comme ça? Il ne signifie rien en termes de programmation? Eh bien, vous pouvez la considérer comme une fonction qui a déjà quelque chose de type P quelque part, et a besoin de vous pour lui donner une fonction qui prend en P comme argument, le tout étant polymorphe dans le résultat final type. Dans un sens, il représente une suspension de calcul, en attente pour le reste à fournir. En ce sens, ces suspendu les calculs peuvent être composées ensemble, passé autour, invoquée, que ce soit. Cela devrait commencer à son familier pour les fans de certaines langues, comme le Régime ou Ruby--parce que ce que cela signifie, c'est que la double-négation correspond à la continuation passing style, et en fait le type que j'ai donné ci-dessus est exactement la continuation de la monade en Haskell.

Answer 3

Votre tableau n'est pas tout à fait à droite; dans de nombreux cas, vous avez confondu avec des types de 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'une Turing-complète et fonctionnelle de la langue est incohérent. La récursivité n'a pas de correspondance dans l'optique des théories. Une incohérence logique/dénuée de la théorie de la preuve, vous pourriez l'appeler une règle qui entraîne une incohérence/troubles.

[2] Encore une fois, c'est une conséquence de l'exhaustivité. Ce serait une preuve d'un anti-théorème si la logique étaient conformes -- donc, il ne peut pas exister.

[3] N'existe pas dans les langages fonctionnels, car ils éluder de première ordre logique caractéristiques: tous quantification et le paramétrage se fait via les formules. Si vous avez eu de premier ordre fonctionnalités, il y aurait une sorte d'autre que *, * -> *, etc.; le type des éléments du domaine de discours. Par exemple, en Father(X,Y) :- Parent(X,Y), Male(X), X et Y l'aire du domaine du discours (appelons - Dom), et Male :: Dom -> *.

Answer 4

function composition      | syllogism

Answer 5

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

1. Je pense que la somme types/types d'union (par exemple, data Either a b = Left a | Right b) sont équivalents aux inclusive disjonction. Et, même si je ne suis pas très bien informé de Curry-Howard, je pense que cela démontre. Considérons la fonction suivante:

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

   Si je comprends les choses correctement, le type dit que (a ∧ b) → (a ★ b) et la définition dit que c'est vrai, où ★ est soit inclusif ou exclusif ou, selon la Either représente. Vous avez Either représentant exclusif ou, ⊕; toutefois, (a ∧ b) ↛ (a ⊕ b). Par exemple, ⊤ ∧ ⊤ ≡ ⊤, mais ⊤ ⊕ ⊥ ≡ ⊥, et ⊤ ↛ ⊥. En d'autres termes, si les deux a et b sont vrais, alors l'hypothèse est vraie, mais la conclusion est fausse, et donc, cette implication doit être faux. Cependant, clairement, (a ∧ b) → (a ∨ b), car si les deux a et b sont vrais, alors l'un au moins est vraie. Ainsi, si les victimes de syndicats sont une certaine forme de disjonction, ils doivent être de la variété. Je pense que cela est une preuve, mais se sentent plus libres de me détromper de cette notion.

2. De même, les définitions de la tautologie et l'absurdité que la fonction identité et de la non-terminaison de fonctions, respectivement, sont un peu hors. La vraie formule est représentée par le type d'unité, qui est le type qui a un seul élément (data ⊤ = ⊤; souvent orthographié () et/ou Unit dans les langages de programmation fonctionnelle). C'est logique: depuis que le type est garanti à être habitée, et depuis il n'y a qu'un possible habitant, ça doit être vrai. L'identité de la fonction juste à l'représente le particulier de la tautologie que un → un.

   Votre commentaire à propos de la non-terminaison des fonctions est, selon ce que vous voulez dire, plus au large. Curry-Howard fonctions sur le type de système, mais non la résiliation n'est pas codé. Selon Wikipedia, le domaine de la non-dénonciation est un problème, que l'ajout de ce produit incompatible logiques (par exemple, je peux définir wrong :: a -> b par wrong x = wrong x, et ainsi "prouver" que un → b pour tout a et b). Si c'est ce que vous entendez par "l'absurde", alors vous êtes au bon endroit. Si au contraire vous signifiait, la fausse déclaration, puis ce que vous voulez, au contraire, est tout inhabitée type, par exemple, quelque chose de défini par data ⊥-c'est un type de données, sans possibilité de le construire. Cela garantit qu'il n'a pas de valeurs à tous, et elle doit donc être inhabitée, ce qui est équivalent à false. Je pense que vous pourriez probablement aussi utiliser a -> b, car si nous nous interdisons de non-terminaison des fonctions, c'est aussi inhabité, mais je ne suis pas sûr à 100%.

3. Wikipedia dit que les axiomes sont codés de deux façons différentes, en fonction de comment vous interprétez de Curry-Howard: soit dans les combinators ou dans les variables. Je pense que le combinateur de vue signifie que les fonctions primitives qui nous est donné, codent pour des choses que nous pouvons dire par défaut (de la même façon que le modus ponens est un axiome, car la fonction de demande est primitif). Et je pense que la vue variable peut signifier la même chose-combinators, après tout, ce sont juste des variables globales qui sont des fonctions particulières. Comme pour les types primitifs: si je suis en train de réfléchir correctement, alors je pense que les types primitifs sont les entités-les objets primitifs que nous essayons de prouver des choses sur.

4. Selon ma logique et de la sémantique de la classe, le fait que (a ∧ b) → c ≡ a → (b → c) (et aussi que b → (a → c)) est appelé l'exportation de l'équivalence de la loi, au moins dans la déduction naturelle preuves. Je n'avais pas remarqué à l'époque que c'était juste nourrissage-je souhaite que j'avais, parce que c'est cool!

5. Alors que nous avons maintenant une manière de représenter inclusive disjonction, nous n'avons pas une manière de représenter la variété exclusive. Nous devrions être en mesure d'utiliser la définition de la disjonction exclusive pour le représenter: a ⊕ b ≡ (a ∨ b) ∧ (a ∧ b). Je ne sais pas comment écrire la négation, mais je sais que p ≡ p → ⊥, et à la fois l'implication et le mensonge sont faciles. Nous devrions donc pouvoir représenter la disjonction exclusive par:

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

   Ceci définit ⊥ à être le type vide avec pas de 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 (implicitement) à partir de (a,b) (et) pour le type de fond (false). Cependant, je n'ai aucune idée de ce que cela signifie. (Edit 1: Maintenant, je n', voir le paragraphe suivant!) Puisqu'il n'existe pas de valeurs de type (a,b) -> ⊥ (?), Je ne peux pas imaginer ce que cela signifie dans un programme. Quelqu'un sait-il une meilleure façon de penser à propos cette définition ou un autre? (Edit 1: Oui, camccann.)

   Edit 1: Merci à camccann de réponse (plus particulièrement, les commentaires qu'il a laissé sur elle pour m'aider), je pense que je vois ce qu'il se passe ici. Pour construire une valeur de type Xor a b, vous devez fournir deux choses. Tout d'abord, un témoignage de l'existence d'un élément de a ou b comme premier argument, Left a ou Right b. Et la seconde, une preuve qu'il n'y a pas des éléments des deux types a et b-en d'autres termes, preuve qu' (a,b) est inhabitée-comme deuxième argument. Puisque vous ne serez en mesure d'écrire une fonction à partir d' (a,b) -> ⊥ si (a,b) est inhabitée, ce qui veut dire que ce sera le cas? Cela signifierait qu'une partie d'un objet de type (a,b) n'a pu être construite; en d'autres termes, qu'au moins un, et peut-être les deux, a et b sont inhabitées! Dans ce cas, si on pense à propos de la correspondance de motif, vous ne pouvait pas faire correspondre à un modèle sur un tel n-uplet: en supposant que l' b est inhabitée, qu'aurions-nous écrire qui pourrait correspondre à la deuxième partie de ce tuple? Ainsi, nous ne pouvons pas en correspondance du modèle, ce qui peut vous aider à voir pourquoi cela fait-il inhabitée. Maintenant, la seule façon d'avoir un total d'une fonction qui ne prend pas d'arguments (comme celui-ci doit, depuis (a,b) est inhabitée) est pour que le résultat soit d'une inhabitée type trop-si nous pensons à ce à partir d'un modèle d'appariement de point de vue, cela signifie que, même si la fonction n'a aucun cas, il n'est pas possible du corps qu'elle pourrait avoir, et que donc tout est OK.

Beaucoup de c'est moi la pensée à haute voix/de prouver (espérons-le) de choses à la volée, mais j'espère que c'est utile. Je recommande vraiment l'article de Wikipédia; je n'ai pas lu en détail, mais ses tableaux sont un très bon résumé, et c'est très complet.