カリー／ハワード／ランベック対応の辞書： 推論規則再論

• 続・カリー／ハワード／ランベック対応の辞書
• 矢印の混乱に対処する： デカルト閉圏のための記法

上記2つの記事で述べた内容を組み合わせて、記述を追加します。

論理でいう「推論規則」は種類が違うものをゴッチャにしています。導入規則〈introduction rule〉と除去規則〈elimination rule〉のあいだに対称性はありません。対称といえる部分でも、その対称性が「双対性か可逆性か随伴性か」の区別を付けてなくて曖昧です。このへんのこと（自然演繹への悪口）は次の過去記事に書いています。

• 自然演繹はちっとも自然じゃない -- 圏論による再考

カリー／ハワード／ランベック対応を通して見れば、自然演繹が対称的でもないし綺麗でもない（歪んでいる）ことがわかります。まず、以下に対応表。$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\hyp}{\text{-}}
\newcommand{\T}[1]{\text{#1}}
\newcommand{\Hom}[2]{ \{ #1 \to #2\}}
\newcommand{\In}{\text{ in }}
\newcommand{\mrm}[1]{ \mathrm{#1} }
`$

小文字始まりの名前は圏の射で、大文字始まりの名前は射に働く圏論的オペレーター〈コンビネータ〉（「圏論的コンストラクタと圏論的オペレータ〈コンビネータ〉 再論」参照）です。射とオペレーターは別な種類のモノです。表の後に、射／オペレーターの記述をします。

圏論	論理
基本操作
Compose
Exchange
終対象と始対象	真と偽
terminal	trivial
initial	cotrivial
デカルト・ペア	論理AND
MakePair	AndIntroduction
projectionLeft	andEliminationLeft
projectionRight	andEliminationRight
swapProduct
余デカルト・コペア	論理OR
MakeCopair
injectionLeft	orIntroductionLeft
injectionRight	orIntroductionRight
swapSum
不要 1	OrElimination
カリー同型	含意
MakeCurry	ImplicationIntroduction
MakeUncurry
evalLeft	implicationEliminationLeft
evalRight	implicationEliminationRight
デカルト・タプル	全称限量子
MakeTuple	UniversalIntroduction
projection
dependentEvalLeft
dependentEvalRight
不要 2	UniversalElimination
余デカルト・コタプル	存在限量子
MakeCotuple
injection	existentialIntroduction
不要 3	ExistentialElimination

圏 $`\cat{C}`$ はデカルト閉圏で直和も持つとします。さらに、パイ構成とシグマ構成もできるとします -- これは、圏 $`\cat{C}`$ が完備性・余完備性を持つということです。型理論的な見方をすれば、$`\cat{C}`$ で依存型理論を展開できることになります。

$`A, B, X, Y`$ などは圏 $`\cat{C}`$ の対象を表します。$`I, J`$ なども $`\cat{C}`$ の対象ですが、これらを“集合とみなす方法”〈dereification〉があるとします*1。特に記号を変えずに、$`I \in |\cat{C}|`$ かつ $`I \in |{\bf Set}|`$ だとします。$`\cat{C} = {\bf Set}`$ なら何の仕掛けも要りません。

以下、「矢印の混乱に対処する： デカルト閉圏のための記法」で導入した記法を全面的に使って記述します。集合圏では、$`\Hom{X}{Y} = [X \to Y]`$ であることに注意してください。視認性の観点から、ブレイスとブラケットどっちでもいいならブラケットを優先します。

論理の場合、どこがどう歪んでいるか（主に上の表の「不要」の部分）については別な機会（あれば）に説明します。

内容：

射とオペレーターの組み合わせのあいだの等式的法則については以下の記事に書いてあります。

• 論理と圏論： 導入規則と除去規則のあいだの等式的法則

基本操作

Compose

$`\T{Compose} :\\
X, Y, Z \mapsto [\Hom{X}{Y} \times \Hom{Y}{Z}\\
\quad \to \Hom{X}{Z}]
`$

説明します； $`\T{Compose}`$ は3つの引数（圏 $`\cat{C}`$ の対象達）を取りますが、それを下付き添字で書くと：

$`\quad\T{Compose}_{X, Y, Z} \in [\Hom{X}{Y} \times \Hom{Y}{Z} \to \Hom{X}{Z}]`$

つまり、

$`\quad\T{Compose}_{X, Y, Z} \in {\bf Set}(\cat{C}(X, Y) \times \cat{C}(Y, Z), \cat{C}(X, Z) )`$

さらに書き換えれば：

$`\quad\T{Compose}_{X, Y, Z} : \cat{C}(X, Y) \times \cat{C}(Y, Z) \to \cat{C}(X, Z) \In {\bf Set}`$

$`\T{Compose}`$ は、圏 $`\cat{C}`$ が備える結合〈composition〉演算のことです。

Exchange

$`\T{Exchange} \\
A, X, B, Y \mapsto [ \Hom{A}{X}\times \Hom{B}{Y} \\
\quad \to \Hom{B}{Y} \times \Hom{A}{X}]
`$

射のペアを入れ替える操作ですが、具体的に書けば：

$`\quad \T{Exchange}_{A, X, B, Y}(f, g) := (g, f)`$

終対象と始対象

terminal

$`\T{terminal} :\\
X \mapsto \Hom{X}{\bf 1}
`$

説明します； $`\T{terminal}`$ は1つの引数（圏 $`\cat{C}`$ の対象）を取りますが、それを下付き添字で書くと：

$`\quad \T{terminal}_X \in \Hom{X}{\bf 1} `$

つまり、

$`\quad \T{terminal}_X \in \cat{C}(X , {\bf 1})`$

さらに書き換えれば：

$`\quad \T{terminal}_X : X \to {\bf 1} \In {C}`$

$`\T{terminal}`$ は、圏の終対象への唯一の射を与えます。

initial

$`\T{initial} :\\
X \mapsto \Hom{\bf 1}{X}
`$

デカルト・ペア

MakePair

$`\T{MakePair} : \\
X, A, B \mapsto [\Hom{X}{A} \times \Hom{X}{B} \\
\quad \to \Hom{X}{A \times B}]
`$

projectionLeft

$`\T{projectionLeft} :\\
A, B \mapsto \Hom{A\times B}{A}`$

projectionRight

$`\T{projectionRight} :\\
A, B \mapsto \Hom{A\times B}{B}`$

swapProduct

$`\T{swapProduct} : \\
A, B \mapsto \Hom{A\times B}{ B \times A}
`$

これは、しばしば $`\sigma_{A, B}`$ と書かれます。

余デカルト・コペア

MakeCopair

$`\T{MakeCopair} : \\
A, B, Y \mapsto [\Hom{A}{Y} \times \Hom{B}{Y} \\
\quad \to \Hom{A + B}{Y}]
`$

injectionLeft

$`\T{injectionLeft} :\\
A, B \mapsto \Hom{A}{A + B}`$

injectionRight

$`\T{injectionRight} :\\
A, B \mapsto \Hom{B}{A + B}`$

swapSum

$`\T{swapSum} : \\
A, B \mapsto \Hom{A + B}{ B + A}
`$

カリー同型

MakeCurry

$`\T{MakeCurry} :\\
X, A, Y \mapsto [ \Hom{X\times A}{Y}\\
\quad \to \Hom{X}{[A \to Y]}]
`$

左カリー化と右カリー化の区別はしてません。一般論では、左右の区別をしたほうが望ましいです。左右を区別するときは、$`[A \to Y]`$ と $`[Y \leftarrow A]`$ も使い分けます。

MakeUncurry

$`\T{MakeUncurry} :\\
X, A, Y \mapsto [ \Hom{X}{[A \to Y]}\\
\quad \to \Hom{X\times A}{Y}]
`$

evalLeft

$`\T{evalLeft} :\\
A, B \mapsto \Hom{A \times [A \to B]}{B}
`$

evalRight

$`\T{evalRight} :\\
A, B \mapsto \Hom{[A \to B] \times A }{B}
`$

デカルト・タプル

MakeTuple

$`\T{MakeTuple} :\\
I, (A_\bullet: I \to |\cat{C}|) \mapsto
{\displaystyle
\prod_{ |\mrm{Cone}(A_\bullet, \cat{C})| }
\cat{C}\Hom{\mrm{top}(\hyp)}{\Pi_I A_\bullet}
}`$

これはちょっと複雑です。$`\T{MakeTuple}`$ に渡されるモノは、圏 $`\cat{C}`$ の対象であり、同時に集合ともみなせる $`I`$ 、それと $`A_\bullet`$ です。$`A_\bullet`$ は、黒丸のところにインデックスが入る族〈ファミリー〉です。$`\mrm{top}(\hyp)`$ は錐の頂点を取り出す写像です。大きな総積記号は、無名変数 $`\hyp`$ が表す“すべての錐”に渡って掛け合わせる記号です。大きな総積記号は大規模〈ラージ〉な演算を表します。

$`I, A_\bullet`$ が決まると、$`A_\bullet`$ を底面とする錐の圏 $`\mrm{Cone}(A_\bullet, \cat{C})`$ の対象 $`F_\bullet`$ からタプル構成をして、$`\cat{C}`$ の射
$`\quad \langle F_\bullet \rangle_I = \langle F_i \rangle_{i\in I} : \mrm{top}(F_\bullet) \to \Pi_I A_\bullet`$ （これがタプル）
が得られます。$`\Pi_I A_\bullet`$ は極限 $`\mrm{lim}_I A_\bullet`$ と同じです。

projection

$`\T{projection} :\\
I, (A_\bullet: I \to |\cat{C}|), a \in I \mapsto \Hom{\Pi_I A_\bullet }{A_a}
`$

dependentEvalLeft

$`\T{dependentEvalLeft} : \\
I, (A_\bullet: I \to |\cat{C}|) \mapsto \Hom{I \times \Pi_I A_\bullet}{\Sigma_I A_\bullet}
`$

これは、$`i, \langle F_\bullet\rangle_I \mapsto F_i`$ という写像を定義します。次の図式が可換になります。

$`\require{AMScd}\\
\begin{CD}
I \times \Pi_I A_\bullet @>{\T{dependentEvalLeft}}>> \Sigma_I A_\bullet \\
@V{\pi_1}VV @VV{\pi}V\\
I @= I
\end{CD}\\
\text{commutative in }\cat{C}`$

dependentEvalRight

$`\T{dependentEvalRight} : \\
I, (A_\bullet: I \to |\cat{C}|) \mapsto \Hom{\Pi_I A_\bullet \times I }{\Sigma_I A_\bullet}
`$

余デカルト・コタプル

MakeCotuple

$`\T{MakeCotuple} :\\
J, (B_\bullet: J \to |\cat{C}|) \mapsto
{\displaystyle
\prod_{ |\mrm{Cocone}(B_\bullet, \cat{C})| }
\cat{C}\Hom{\Pi_J B_\bullet}{\mrm{cotop}(\hyp) }
}`$

$`\mrm{cotop}(\hyp)`$ は余錐の余頂点を取り出す写像です。

injection

$`\T{injection} :\\
J, (B_\bullet: J \to |\cat{C}|), b \in J \mapsto \Hom{B_b}{\Sigma_j B_\bullet }
`$

*1:この仮定は、パワーリング／テンソリングを使って取り除くことができるかも知れません。現状、よくわからない。