カリー／ハワード／ランベック対応： チートシート

「カリー／ハワード／ランベック対応の辞書」を皮切りにカリー／ハワード／ランベック対応に関して幾つかの記事を書きました。

1. カリー／ハワード／ランベック対応の辞書（最初の記事）
2. 続・カリー／ハワード／ランベック対応の辞書
3. 論理と圏論： 導入規則と除去規則のあいだの等式的法則
4. まだある、カリー／ハワード／ランベック対応の辞書
5. タプル・コタプルとVΣ計算
6. 矢印の混乱に対処する： デカルト閉圏のための記法
7. 矢印のオーバーロードがひどい件： 所感
8. カリー／ハワード／ランベック対応の辞書： 推論規則再論

短くまとめたチートシートを作りました。$`\newcommand{\Imp}{\Rightarrow}
\newcommand{\Hom}[2]{ \{ #1 \to #2\}}
`$

内容：

用語法・記号法

用語は、通常使われているものは無視します。慣習・伝統より合理性・一貫性・効率性を重視します。それにより、カリー／ハワード／ランベック対応が明瞭になります。通常使われているメジャーな用語法は別途調べてください。

1. 双対概念には一律に "co"〈余〉を付ける。
2. 逆写像には一律に（今回はカリー化しか登場しないが） "un"〈反〉を付ける。
3. 依存性がある場合は一律に "dependent"〈依存〉を付ける。
4. 限量子に関係する場合は一律に "quantified"〈限量〉を付ける。

型理論、論理では違う用語を使いますが、次の対応を守ります。

型理論	論理
型定数	命題定数
型構成子	命題結合子
依存型構成子	限量子
多相関数	推論規則
コンビネータ	リーズニング規則
単純型理論	命題論理
依存型理論	述語論理

記号は次の対応を守ります。

$`{\bf 型理論／圏論}`$	$`{\bf 論理}`$
$`{\bf 1}`$	$`\top`$
$`{\bf 0}`$	$`\bot`$
$`\times`$	$`\land`$
$`+`$	$`\lor`$
$`[\:\to\:]`$	$`(\:\Imp\:)`$
$`\prod`$	$`\forall`$
$`\sum`$	$`\exists`$

上記以外の記号は共通にします。「矢印の混乱に対処する： デカルト閉圏のための記法」で導入した記法を使います。

依存型構成子／限量子で使う添字に関して、次はすべて同じ意味です（書き方の差異はどうでもいい）。

1. $`\prod_{i\in I}A_i`$
2. $`\prod i\in I. A_i`$
3. $`\prod (i\in I). A_i`$
4. $`\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} \}
`$