Isomorphisme de Curry-Howard

Question

J'ai cherché sur Internet et je ne trouve pas les explications de CHI, qui ne sont pas rapidement dégénérer en une conférence sur la théorie logique qui est radicalement dessus de ma tête. (Ces gens parlent comme si "intuitionniste proposition de calcul" est une phrase qui en réalité signifie quelque chose pour l'homme normal!)

En gros, CHI dit que les types sont des théorèmes, et les programmes sont les preuves de ces théorèmes. Mais ce que l'enfer est-ce que même moyenne??

Jusqu'à présent, j'ai compris cela:

• Envisager id :: x -> x. Son type dit "étant donné que X est vrai, on peut conclure que X est vrai". Semble raisonnable théorème de moi.

• Maintenant, considérons foo :: x -> y. Comme tout Haskell programmeur vais vous dire, c'est impossible. Vous ne pouvez pas écrire cette fonction. (Eh bien, sans tricher, de toute façon.) Lire comme un théorème, il dit: "étant donné que X est vrai, nous pouvons conclure que tout Y est vrai". C'est évidemment une absurdité. Et, bien sûr, vous ne pouvez pas écrire cette fonction.

• Plus généralement, les arguments de la fonction peut être considéré comme "ce qui est supposé être vrai", et le type de résultat peut être considéré comme "chose qui est vrai en supposant que toutes les autres choses sont". Si il y a un argument de fonction, disons x -> y, nous pouvons prendre cela comme une hypothèse que X est vrai implique que Y doit être vrai.

• Par exemple, (.) :: (y -> z) -> (x -> y) -> x -> z peut être considéré comme "en supposant que Y implique Z, X implique Y et que X est vrai, nous pouvons conclure que Z est vrai". Qui semble logiquement sensible pour moi.

Maintenant, ce que l'enfer n' Int -> Int moyenne?? o_O

La seule réponse sensée, je peux venir, c'est ça: Si vous avez une fonction X -> Y -> Z, puis la signature d'un type dit "en supposant qu'il est possible de construire une valeur de type X, et un autre de type Y, alors il est possible de construire une valeur de type Z". Et le corps de la fonction décrit exactement comment vous feriez cela.

Cela semble logique, mais ce n'est pas très intéressant. Donc clairement, il doit y avoir plus que cela...

Answer 1

Le Curry-Howard isomorphisme indique simplement que les types correspondent à des propositions, et les valeurs correspondent à des épreuves.

Int -> Int ne veut pas vraiment dire beaucoup plus intéressant qu'une proposition logique. Lors de l'interprétation de quelque chose comme une proposition logique, vous êtes seulement intéressé de savoir si le type est habitée (a toutes les valeurs) ou pas. Donc, Int -> Int signifie simplement "donné un Int, je peux vous donner un Int", et c'est, bien sûr, un vrai. Il existe de nombreuses preuves (correspondant à différentes fonctions de ce type), mais quand le prendre comme une proposition logique, vous n'avez pas de soins.

Cela ne signifie pas intéressantes propositions peut pas impliquer de telles fonctions; juste que ce type particulier est tout à fait ennuyeux, comme une proposition.

Pour une instance d'un type de fonction qui n'est pas complètement polymorphe et qui a logique du sens, de considérer p -> Void (pour certains, p), où Void est la inhabitées type: le type avec n valeurs (à l'exception ⊥, en Haskell, mais j'y reviendrai plus tard). La seule façon d'obtenir une valeur de type Void est si vous pouvez prouver une contradiction (qui est, bien sûr, impossible), et depuis Void signifie que vous avez prouvé une contradiction, vous pouvez obtenir une valeur (i.e. il existe une fonction absurd :: Void -> a). En conséquence, p -> Void correspond à p: il signifie "p implique le mensonge".

La logique intuitionniste est juste une sorte de logique commune langages fonctionnels correspondent. L'important, c'est constructif: en gros, une preuve de l' a -> b vous donne un algorithme pour calculer b de a, ce qui n'est pas vrai réguliers de la logique classique (à cause de la loi du tiers exclu, qui va vous dire que quelque chose est vrai ou faux, mais pas pourquoi).

Même si les fonctions comme Int -> Int ne signifie pas que des propositions, nous pouvons faire des déclarations au sujet avec d'autres propositions. Par exemple, on peut déclarer le type de l'égalité de deux types (à l'aide d'un GADT):

data Equal a b where
    Refl :: Equal a a

Si nous avons une valeur de type Equal a b, alors a est le même type d' b: Equal a b correspond à la proposition a = b. Le problème est que nous ne pouvons parler de l'égalité des types de cette façon. Mais si nous avions des types dépendants, on pourrait facilement généraliser cette définition de travailler avec toute la valeur, et donc, Equal a b correspondrait à l'idée que les valeurs *a* et b sont identiques. Ainsi, par exemple, on pourrait écrire:

type IsBijection (f :: a -> b) (g :: b -> a) =
    forall x. Equal (f (g x)) (g (f x))

Ici, f et g sont des fonctions classiques, de sorte que f pourrait facilement avoir le type Int -> Int. Encore une fois, Haskell ne pouvez pas faire cela, vous avez besoin des types dépendants à faire des choses comme ça.

Typique langages fonctionnels ne sont pas vraiment bien adapté à l'écriture de preuves, non seulement parce qu'ils manquent de types dépendants, mais aussi en raison de ⊥, qui, tapez a tous a, agit comme une preuve de n'importe quelle proposition. Mais le total des langues comme le Coq et Agda exploiter la correspondance pour agir à titre de preuve des systèmes ainsi que dépendante de typage des langages de programmation.

Answer 2

Peut-être la meilleure façon de comprendre ce que cela signifie est de commencer (ou d'essayer) à l'aide de types de propositions et programmes à titre de preuves. Il est préférable d'apprendre une langue avec des types dépendants, tels que Agda (c'est écrit en Haskell et semblable à Haskell). Il y a divers articles et cours sur la langue. Apprendre vous un Agda est incomplète, mais c'est essayer de simplifier les choses, tout comme LYAHFGG livre.

Voici un exemple simple de la preuve:

{-# OPTIONS --without-K #-} -- we are consistent

module Equality where

-- Peano arithmetic.
-- 
--   ℕ-formation:     ℕ is set.
-- 
--   ℕ-introduction:  o ∈ ℕ,
--                    a ∈ ℕ | (1 + a) ∈ ℕ.
-- 
data ℕ : Set where
  o : ℕ
  1+ : ℕ → ℕ

-- Axiom for _+_.
-- 
--   Form of ℕ-elimination.
-- 
infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
o + m = m
1+ n + m = 1+ (n + m)

-- The identity type for ℕ.
-- 
infix 4 _≡_
data _≡_ (m : ℕ) : ℕ → Set where
  refl : m ≡ m

-- Usefull property.
-- 
cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n
cong refl = refl

-- Proof _of_ mathematical induction:
-- 
--   P 0, ∀ x. P x → P (1 + x) | ∀ x. P x.
-- 
ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n
ind P P₀ _ o = P₀
ind P P₀ next (1+ n) = next n (ind P P₀ next n)

-- Associativity of addition using mathematical induction.
-- 
+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative m n p = ind P P₀ is m
  where
    P : ℕ → Set
    P i = (i + n) + p ≡ i + (n + p)
    P₀ : P o
    P₀ = refl
    is : ∀ i → P i → P (1+ i)
    is i Pi = cong Pi

-- Associativity of addition using (dependent) pattern matching.
-- 
+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative′ o _ _ = refl
+-associative′ (1+ m) n p = cong (+-associative′ m n p)

De là, vous pouvez voir l' (m + n) + p ≡ m + (n + p) proposition de type et de sa preuve que la fonction. Il y a des techniques plus avancées de ces preuves (par exemple, en précommande raisonnement, combinators dans Agda est comme tactiques de Coq).

Quoi d'autre peut être prouvé:

• head ∘ init ≡ head pour les vecteurs, ici.

• Votre compilateur produire un programme d'exécution qui donne la même valeur que la valeur obtenue dans l'interprétation de la même (hôte) de programme, ici, pour Coq. Ce livre est aussi une bonne lecture sur le sujet du langage de modélisation et de vérification de programmes.

• Rien d'autre, ce qui peut être prouvé en mathématiques constructives, depuis de Martin-Löf du type de la théorie dans sa puissance d'expression est l'équivalent de ZFC. En fait, Curry-Howard isomorphisme peut être étendue à la physique et à la topologie et à la topologie algébrique.

Answer 3

La seule réponse sensée, je peux venir, c'est ça: Si vous avez une fonction X -> Y -> Z, puis la signature d'un type dit "en supposant qu'il est possible de construire une valeur de type X, et un autre de type Y, alors il est possible de construire une valeur de type Z". Et le corps de la fonction décrit exactement comment vous feriez cela. Cela semble logique, mais ce n'est pas très intéressant. Donc clairement, il doit y avoir plus que cela...

Eh bien, oui, il y en a beaucoup plus, parce qu'il a beaucoup d'implications et ouvre beaucoup de questions.

Tout d'abord, votre discussion de l'CHI est encadré exclusivement en termes d'implication/types de fonction (->). Vous ne parlez pas de cela, mais vous avez probablement vu également comment la conjonction et de la disjonction correspondent au produit et somme types respectivement. Mais quid des autres opérateurs logiques comme la négation, la quantification universelle et de la quantification existentielle? Comment pouvons-nous traduire les preuves logiques portant sur ces programmes? Il s'avère que c'est à peu près comme ceci:

• La négation correspond à la première classe de suites. Ne me demandez pas d'expliquer celui-ci.
• Une quantification universelle propositionnelle (non individuelle) variables correspond à de polymorphisme paramétrique. Ainsi, par exemple, la fonction polymorphe id a vraiment le type forall a. a -> a
• Quantification existentielle sur les variables propositionnelles correspond à une poignée de choses qui ont à voir avec des données ou de mise en œuvre de la clandestinité: les types de données abstraites, systèmes de modules et de répartition dynamique. GHC existentielles de types sont liés à cela.
• Universelle et de la quantification existentielle sur les variables individuelles conduit à type de charge des systèmes.

Autres que que, elle aussi signifie que toutes sortes de preuves sur des logiques de traduire instantanément dans les épreuves sur les langages de programmation. Par exemple, le decidability de propositionnelle intuitionniste logique implique la résiliation de tous les programmes de simplement tapé lambda calcul.

Maintenant, ce que l'enfer n'Int -> Int veux dire?? o_O

C'est un type, ou, alternativement, d'une proposition. En f :: Int -> Int, (+1) noms un "programme" (dans un sens spécifique, qui admet à la fois de fonctions et de constantes comme des "programmes", ou bien une preuve. La sémantique de la langue doit prévoir f comme une primitive de la règle d'inférence, ou de montrer comment f est une preuve qui peut être construit à partir de ces règles et des locaux.

Ces règles sont souvent spécifiées en termes de général paramétré par des axiomes qui définissent la base de membres d'un type et les règles qui vous permettent de prouver ce que d'autres programmes d'habiter ce type. Par exemple, le passage d' Int de Nat (nombres naturels de 0 vers l'avant), nous avons pu avoir ces règles:

• Axiome: 0 :: Nat (0 est une primitive de la preuve de l' Nat)
• Règle: x :: Nat ==> Succ x :: Nat
• Règle: x :: Nat, y :: Nat ==> x + y :: Nat
• Règle: x + Zero :: Nat ==> x :: Nat
• Règle: Succ x + y ==> Succ (x + y)

Ces règles sont assez pour prouver de nombreux théorèmes sur plus de nombres naturels. Ces épreuves seront également les programmes.