CH対応橋
命題 ↔ 型・証明 ↔ プログラム。Curry-Howard 同型対応をマッチングで体得する。
Curry-Howard 同型対応: 直観主義論理の 命題 と単純型付き λ 計算の 型 は同一構造。命題の証明 はその 型を持つプログラム に対応する。
左の論理側カードと右の計算側カードを 同じ構造のもの同士 で結べ。
左の論理側カードと右の計算側カードを 同じ構造のもの同士 で結べ。
Stage 1/5
Matched 0/0
Mistakes 0
論理側 (命題・証明)
計算側 (型・項)
| 論理 | 計算 | 意味 |
|---|---|---|
| 命題 P | 型 P | 素朴対応 |
| 含意 A → B | 関数型 A → B | 「A から B」 |
| 連言 A ∧ B | 直積型 A × B | ペア |
| 選言 A ∨ B | 直和型 A + B | Either |
| 偽 ⊥ | 空型 0 | 無 |
| Modus Ponens | 関数適用 f x | 除去則 →E |
| 含意導入 | λ抽象 λx.t | 導入則 →I |
| ∀x.P(x) | Π型 ∀x.P x | 多相 |
操作
左のカードをクリックして選択 → 右の対応カードをクリックで結ぶ。間違うと 赤 で点滅し再選択可。全マッチで次ステージ。
ヒント: 構造的に同じものを探す。A→B は関数型、∧ は直積、∨ は直和、⊥ は空型 (要素なし)。証明＝項、適用＝MP、抽象＝→導入。