このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

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

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

  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} \}
`$