カリー=ハワード同型対応

type-theorylogiccomputer-science

論理の命題と型、論理の証明とプログラムが一対一に対応するという発見。

プログラマ向けの一言

型を書くこと = 命題を書くこと。コンパイルが通るプログラムを書くこと = 証明を書くこと。 型チェッカーは実は定理の証明チェッカーでもある。

対応表

// 論理              ↔  プログラミング
// ─────────────────────────────────
// 命題              ↔  型
// 証明              ↔  プログラム（その型の値）
// A ∧ B（かつ）      ↔  [A, B]（タプル / 直積型）
// A ∨ B（または）    ↔  A | B（直和型 / union）
// A → B（ならば）    ↔  (a: A) => B（関数）
// ⊤（真）           ↔  void / unit（常に作れる値）
// ⊥（偽）           ↔  never（作れない値）
// ¬A（否定）        ↔  (a: A) => never（A があると矛盾）
// ∀x. P(x)         ↔  <T>(x: T) => P<T>（ジェネリクス）

コードで理解する

// --- 「A かつ B ならば A」の証明 ---
// 命題: A ∧ B → A
// 型:   ([A, B]) => A
function proof1<A, B>(pair: [A, B]): A {
  return pair[0]; // タプルの1つ目を取り出すだけ
}
// この関数が書けた = この命題が証明された

// --- 「A ならば A または B」の証明 ---
// 命題: A → A ∨ B
// 型:   (a: A) => A | B
function proof2<A, B>(a: A): A | B {
  return a; // A はそのまま A | B の一員
}

// --- 「A → B かつ B → C ならば A → C」の証明 ---
// 命題: (A → B) ∧ (B → C) → (A → C)
// 型:   三段論法 = 関数合成
function proof3<A, B, C>(f: (a: A) => B, g: (b: B) => C): (a: A) => C {
  return (a) => g(f(a)); // 合成するだけ
}

// --- never（偽 / ⊥）からは何でも証明できる ---
// 命題: ⊥ → A（爆発原理 / ex falso quodlibet）
function absurd<A>(x: never): A {
  return x; // never 型の値は存在しないので、この関数は呼ばれない
}

なぜ重要か

// 1. 型チェッカー = 証明チェッカー
//    コンパイルが通る → 型（= 命題）に対する値（= 証明）が存在する → 命題が正しい

// 2. 定理証明系の基盤
//    Coq, Agda, Lean は「プログラムを書く = 定理を証明する」をそのまま実現
//    カリー=ハワード対応があるからこそ可能

// 3. 型を見れば性質がわかる
//    (a: A) => A  ← これを満たす関数は恒等関数しかない（パラメトリシティ）
//    <A, B>(f: (a: A) => B, xs: A[]) => B[]  ← map しかない

// 4. 「型で考える」ことの正当化
//    型設計 = 仕様設計。型が通るプログラムを書く = 仕様を満たす実装を書く。

押さえどころ（カード化候補）

関連

Graph

Backlinks