「カリー/ハワード/ランベック対応の辞書」を皮切りにカリー/ハワード/ランベック対応に関して幾つかの記事を書きました。
- カリー/ハワード/ランベック対応の辞書(最初の記事)
- 続・カリー/ハワード/ランベック対応の辞書
- 論理と圏論: 導入規則と除去規則のあいだの等式的法則
- まだある、カリー/ハワード/ランベック対応の辞書
- タプル・コタプルとVΣ計算
- 矢印の混乱に対処する: デカルト閉圏のための記法
- 矢印のオーバーロードがひどい件: 所感
- カリー/ハワード/ランベック対応の辞書: 推論規則再論
短くまとめたチートシートを作りました。$`\newcommand{\Imp}{\Rightarrow}
\newcommand{\Hom}[2]{ \{ #1 \to #2\}}
`$
内容:
用語法・記号法
用語は、通常使われているものは無視します。慣習・伝統より合理性・一貫性・効率性を重視します。それにより、カリー/ハワード/ランベック対応が明瞭になります。通常使われているメジャーな用語法は別途調べてください。
- 双対概念には一律に "co"〈余〉を付ける。
- 逆写像には一律に(今回はカリー化しか登場しないが) "un"〈反〉を付ける。
- 依存性がある場合は一律に "dependent"〈依存〉を付ける。
- 限量子に関係する場合は一律に "quantified"〈限量〉を付ける。
型理論、論理では違う用語を使いますが、次の対応を守ります。
型理論 | 論理 |
---|---|
型定数 | 命題定数 |
型構成子 | 命題結合子 |
依存型構成子 | 限量子 |
多相関数 | 推論規則 |
コンビネータ | リーズニング規則 |
単純型理論 | 命題論理 |
依存型理論 | 述語論理 |
記号は次の対応を守ります。
$`{\bf 型理論/圏論}`$ | $`{\bf 論理}`$ |
---|---|
$`{\bf 1}`$ | $`\top`$ |
$`{\bf 0}`$ | $`\bot`$ |
$`\times`$ | $`\land`$ |
$`+`$ | $`\lor`$ |
$`[\:\to\:]`$ | $`(\:\Imp\:)`$ |
$`\prod`$ | $`\forall`$ |
$`\sum`$ | $`\exists`$ |
上記以外の記号は共通にします。「矢印の混乱に対処する: デカルト閉圏のための記法」で導入した記法を使います。
依存型構成子/限量子で使う添字に関して、次はすべて同じ意味です(書き方の差異はどうでもいい)。
- $`\prod_{i\in I}A_i`$
- $`\prod i\in I. A_i`$
- $`\prod (i\in I). A_i`$
- $`\prod_I A_\bullet`$ (黒丸は添字〈引数〉が入る場所を示す)
$`A_i\; A[i]\; A(i)`$ も特に区別しません(書き方の差異はどうでもいい)。
型理論と圏論
単純型理論
型定数:
$`\text{terminal }{\bf 1}`$ | $`\text{coterminal }{\bf 0}`$ |
型構成子:
$`\text{product }A\times B`$ | $`\text{coproduct } A + B`$ |
多相関数:
$`\text{terminal }A \to {\bf 1}`$ | $`\text{coterminal }{\bf 0}\to A`$ |
$`\text{projection left }A\times B\to A`$ | $`\text{coprojection left }A\to A + B`$ |
$`\text{projection right }A\times B\to B`$ | $`\text{coprojection right }B\to A + B`$ |
コンビネータ:
$`\text{pairing}\\
\quad \Hom{X}{A} \times \Hom{X}{B}\\
\to \Hom{X}{A\times B}
`$
$`\text{copairing}\\
\quad \Hom{A}{Y} \times \Hom{B}{Y}\\
\to \Hom{A + B}{Y}
`$
型構成子:
$`\text{exponential } [A \to B]`$
多相関数:
$`\text{evaluation right }[A \to B]\times A \to B`$
コンビネータ:
$`\text{currying}\\
\quad \Hom{A\times X}{B}\\
\to \Hom{A}{[X \to B]}
`$
$`\text{uncurrying}\\
\quad \Hom{A}{[X \to B]}\\
\to \Hom{A\times X}{B}
`$
依存型理論
依存型構成子:
$`\text{dependent product }\prod_I A_\bullet`$ | $`\text{dependent coproduct }\sum_I A_\bullet`$ |
多相関数:
$`\text{denpendent evaluation right }(\prod_I A_\bullet) \times I \to \sum_I A_\bullet`$
コンビネータ:
$`\text{dependent currying}\\
\quad {\bf Set}\{I \to \sum_{i\in I}\Hom{X}{A_i} \mid \text{section} \}\\
\to \Hom{X}{ \prod_I A_\bullet}
`$
$`\text{dependent uncurrying}\\
\quad \Hom{X}{ \prod_I A_\bullet}\\
\to {\bf Set}\{I \to \sum_{i\in I}\Hom{X}{A_i} \mid \text{section} \}
`$
論理
命題論理
命題定数:
$`\text{true }\top`$ | $`\text{cotrue }\bot`$ |
命題結合子:
$`\text{conjunction }A\land B`$ | $`\text{coconjunction } A \lor B`$ |
推論規則:
$`\text{trivial }A \to \top`$ | $`\text{cotrivial }\bot \to A`$ |
$`\text{projection left }A\land B\to A`$ | $`\text{coprojection left }A\to A \lor B`$ |
$`\text{projection right }A\land B\to B`$ | $`\text{coprojection right }B\to A \lor B`$ |
リーズニング規則:
$`\text{pairing}\\
\quad \Hom{X}{A} \times \Hom{X}{B}\\
\to \Hom{X}{A\land B}
`$
$`\text{copairing}\\
\quad \Hom{A}{Y} \times \Hom{B}{Y}\\
\to \Hom{A \lor B}{Y}
`$
命題構成子:
$`\text{implication } (A \Imp B)`$
推論規則:
$`\text{modus ponens right }(A \Imp B) \land A \to B`$
リーズニング規則:
$`\text{deductive currying}\\
\quad \Hom{A\land X}{B}\\
\to \Hom{A}{(X \Imp B)}
`$
$`\text{deductive uncurrying}\\
\quad \Hom{A}{(X \Imp B)}\\
\to \Hom{A\land X}{B}
`$
述語論理
限量子:
$`\text{universal }\forall_I A_\bullet`$ | $`\text{couniversal }\exists_I A_\bullet`$ |
推論規則:
$`\text{quantified modus ponens right }(\forall_I A_\bullet) \land I \to \exists_I A_\bullet`$
リーズニング規則:
$`\text{quantified currying}\\
\quad {\bf Set}\{I \to \sum_{i\in I} \Hom{X}{A_i} \mid \text{section} \}\\
\to \Hom{X}{ \forall_I A_\bullet}
`$
$`\text{quantified uncurrying}\\
\quad \Hom{X}{ \forall_I A_\bullet}\\
\to {\bf Set}\{I \to \sum_{i\in I} \Hom{X}{A_i} \mid \text{section} \}
`$