自然変換のためのラムダ計算 (2) - 檜山正幸のキマイラ飼育記 (はてなBlog)

「自然変換のためのラムダ計算」の続きです。$`%
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\id}{\mathrm{id} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in } }
%\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\Map}{\mathrm{Map}}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
%\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Reserve}{\Keyword{Reserve } }%
\newcommand{\Release}{\Keyword{Release } }%
%`$

内容：

設定と約束
縦方向演算と横方向演算
束縛変数の予約
実例：基本公式

設定と約束

集合圏 $`{\bf Set}`$ に値を取るような関手と、そのような関手のあいだの自然変換を扱います。$`{\bf CAT}`$ を大きな圏も含む“圏の2-圏”として、そのなかに居る次のようなモノ達〈things〉が我々の主題です。

$`\quad \cat{C} \in |{\bf CAT}|\\
\quad F, G : \cat{C} \to {\bf Set} \In {\bf CAT}\\
\quad \alpha :: F \twoto G : \cat{C} \to {\bf Set} \In {\bf CAT}
`$

$`\cat{C}`$ を固定すれば、“圏の2-圏”のなかの関手圏内で話ができます。関手圏は通常 $`[\cat{C}, {\bf Set}]`$ と書きます。これは $`\cat{C}`$ の余前層の圏です。我々は主に、余前層の圏での計算を扱います。

縦方向演算と横方向演算

僕は、自然変換の計算はストリング図で行うのが望ましいと思っています。しかし、諸般の事情でそうもいかないので代わりにラムダ計算をしよう、ということです。頭にはストリング図を思い浮かべながらテキストで書くので、できるだけストリング図をイメージしやすい、つまり象形文字的記法にしたいのです。

テキスト記法が辛いのは、2次元の情報がバイダイレクショナル1次元文字列に潰れているからです。そこで、縦方向の演算と横方向の演算を明確に区別することにします。ここでの“演算”とは、評価〈適用 | 引数渡し〉と結合です。

原則は図式順演算子記号として、反図式順演算子記号も許容します。演算子記号は次の表のとおりです。

	図式順	反図式順
縦評価	`	()
縦結合	;	∘
横評価	.	[]
横結合	*	・

使用例は次のようです。

関数
- 評価 $`x`f = f(x)`$
- 結合 $`f;g = g\circ f`$
関手
- 評価 $`X.F = F[X],\, f.F = F[f]`$
- 結合 $`F* G = G \cdot F`$
自然変換
- 評価 $`X.\alpha = \alpha[X]`$
- 縦結合 $`\alpha;\beta = \beta \circ \alpha`$
- 横結合 $`\alpha * \beta = \beta \cdot \alpha`$
関手と自然変換
- ヒゲ結合 $`\alpha * G = G \cdot \alpha`$
- ヒゲ結合 $`F * \beta = \beta \cdot F`$

束縛変数の予約

「自然変換のためのラムダ計算」で述べたように、ラムダ抽象は次の形に書きます。

$`\quad \lambda\, x\in X\{\mathscr{E}\;\in Y\}`$

$`X, Y`$ は“型”ですが、$`Y`$ は適宜省略していいとします。ラムダ束縛変数の型 $`X`$ も省略したいのですが、無闇に省略すると型が不明になることもあります。そこで、束縛変数の型を前もって宣言する構文を導入します。次の形です。

$`\Reserve x\in X\\
\quad \lambda\, x\{\mathscr{E} \}\\
\quad \cdots\\
\Release
`$

$`\Reserve`$で束縛変数を宣言し、$`\Release`$で予約を解除します。予約したスコープの終わりが明らかなら $`\Release`$は省略してかまいません。

実例：基本公式

自然変換の縦結合と横結合の明示的公式〈explicit formula〉を書き下してみます。縦結合の状況設定は次のようです。

$`\quad \cat{C} \in |{\bf CAT}|\\
\quad F, G, H : \cat{C} \to {\bf Set} \In {\bf CAT}\\
\quad \alpha :: F \twoto G : \cat{C} \to {\bf Set} \In {\bf CAT}\\
\quad \beta :: G \twoto H : \cat{C} \to {\bf Set} \In {\bf CAT}
`$

プレーンテキストで次のような“アスキーアート”を書いておくと間違いが少ないです。

 x  F
 x (α)
 x  G
 x (β)
 x  H

縦結合の定義を書き下します。

$`\quad \alpha ; \beta \\
\Reserve x\in |\cat{C}|\\
= \lambda\, x\{x.\alpha \;\in \Map(x.F, x.G)\} \,;
\lambda\, x\{x.\beta \;\in\Map(x.G, x.H)\} \\
= \lambda\, x\{x.\alpha \,; x.\beta \;\in \Map(x.F, x.H)\}\\
= \lambda\, x\{(x.\alpha, x.\beta).\mrm{comp}[x.F,x.G, x.H] \;\in \Map(x.F, x.H)\}
%`$

最後の行の $`\mrm{comp}[x.F,x.G, x.H]`$ は集合圏の結合を内部化した関数です。

$`\quad \mrm{comp}[x.F,x.G, x.H] : \\
\qquad \Map(x.F, x.G)\times \Map(x.G, x.H) \to \Map(x.F, x.H)
\In {\bf Set}
`$

横結合は自己関手圏の場合に計算します。縦結合とは状況設定が違います。

$`\quad F, G, H, K : {\bf Set} \to {\bf Set} \In {\bf CAT}\\
\quad \alpha :: F \twoto G : {\bf Set} \to {\bf Set} \In {\bf CAT}\\
\quad \beta :: H \twoto K : {\bf Set} \to {\bf Set} \In {\bf CAT}
`$

“アスキーアート”は次のようです。

 X  F  H
 X (α) H
 X  G  H
 X  G (β)
 X  G  K

まず、ヒゲ結合 $`\alpha * H`$ と $`G * \beta`$ を書き下します。

$`\quad \alpha * H \\
\Reserve X \in |{\bf Set}|, f \in \Map(X.F, X.G)\\
= \lambda\, X\{X.\alpha \;\in \Map(X.F, X.G)\} * \lambda\, f\{ f.H \;\in \Map(X.F.H, X.G.H)\}\\
= \lambda\, X\{ X.\alpha.H \;\in \Map(X.F.H, X.G.H)\}\\
\:\\
\quad G * \beta \\
\Reserve Y \in |{\bf Set}|\\
= \lambda\, X \{X.G \in |{\bf Set}| \} * \lambda\,Y \{Y.\beta \;\in \Map(Y.H, Y.K) \}\\
= \lambda\, X \{ X.G.\beta \; \in\Map(X.G.H, X.G.K) \}
`$

ヒゲ結合を使って、自己関手の横結合を書き下します。

$`\quad \alpha \,; \beta \\
= (\alpha * H)\,; (G*\beta) \\
\Reserve X \in |{\bf Set}|\\
= \lambda\, X \{ X.\alpha.H \;\in \Map(X.F.H, X.G.H) \} \,;\\
\qquad \lambda\, X \{ X.G.\beta \;\in \Map(X.G.H, X.G.K) \}\\
= \lambda\, X\{ X.\alpha.H \,; X.G.\beta \in \Map(X.F.H, X.G.K) \}\\
\Reserve a \in X.F.H\\
= \lambda\, X\{ \lambda\,a \{ a`(X.\alpha.H \,; X.G.\beta) \in X.G.K \} \}\\
= \lambda\, X\{ \lambda\,a \{ a`(X.\alpha.H)`(X.G.\beta) \in X.G.K \} \}\\
= \lambda\, X, \lambda\, a \{ a`(X.\alpha.H)`(X.G.\beta) \in X.G.K \}
%`$

最後のラムダ抽象本体内を、通常の反図式順で書くなら次のようです。

$`\quad
\beta_{G(X)}( H( \alpha_X )(a) )
\in K( G(X) )
`$

見慣れた形式で安心する人が多いでしょうが、僕は右から左への書字方向とボコボコしたフォルムが気持ち悪くてダメです。

自然変換の自然性から、横結合は次のようにも定義できます。

$`\quad \alpha \,; \beta = (F*\beta) \,; (\alpha * K)`$

この場合の明示的な公式も同様に計算できます。

設定と約束

縦方向演算と横方向演算

束縛変数の予約

実例： 基本公式

実例：基本公式