とある自然変換の計算をしていて、通常のラムダ計算の構文はどうも具合が悪い気がしました。視力がいい人なら問題ないでしょうが、老眼近視の僕には視認性が良い構文が必要です。また、ラムダ計算に図式順記法を取り入れます。$`
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in } }
\newcommand{\Subs}[2]{
{\scriptsize \begin{bmatrix} #1 \\ #2\end{bmatrix} } }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
%\newcommand{\Define}{\Keyword{Define } }%
%\newcommand{\Holds}{\Keyword{Holds } }%
\newcommand{\Using}{\quad \Keyword{Using } }%
`$
内容:
小さい字は使わない
下付き・上付きの添字は色々な場面で使われます。
- 自然変換の成分: $`\alpha_X:F(X) \to G(X)`$
- 関手のホムセット部: $`F_{A, B}:\cat{C}(A, B) \to \cat{D}(F(A), F(B))`$
- トレース・オペレーター: $`\mrm{Tr}^X_{A, B}:\cat{C}(A\otimes X, B\otimes X) \to \cat{C}(A, B)`$
- カリー化オペレーター: $`\mrm{Curry}_{A, B,C} : {\bf Set}(A\times B, C) \to {\bf Set}(A, [B, C])`$
視認性の観点から、添字はやめてブラケットにします。
- 自然変換の成分: $`\alpha[X]:F(X) \to G(X)`$
- 関手のホムセット部: $`F[A, B]:\cat{C}(A, B) \to \cat{D}(F(A), F(B))`$
- トレース・オペレーター: $`\mrm{Tr}[X][A, B]:\cat{C}(A\otimes X, B\otimes X) \to \cat{C}(A, B)`$
- カリー化オペレーター: $`\mrm{Curry}[A, B,C] : {\bf Set}(A\times B, C) \to {\bf Set}(A, [B, C])`$
ペアやタプルの成分添字は、後置の番号にします。
- $`A = (A_1, A_2, A_2) = (A1, A2, A3)`$
- $`f = \langle f_1, f_2 \rangle = \langle f1, f2 \rangle`$
指数はMapを使う
集合の指数〈内部ホム | 関数集合〉を $`[A, B]`$ と書くのは一般的で、僕もよく使っています。ブラケット以外にも、集合の指数の書き方は色々あります。
- $`[A, B]`$
- $`B^A`$
- $`\mrm{Map}(A, B)`$
- $`{\bf Set}(A, B)`$
添字をブラケットにすると、指数のブラケットが埋もれてしまい見つけにくいです。ブラケットの代わりに $`\mrm{Map}(A, B)`$ を使うことにします。$`\mrm{Map}(- , -)`$ は二項関手〈双関手〉として使うので、次の表現も有効です。
- $`\mrm{Map}(f, g) : \mrm{Map}(B, C) \to \mrm{Map}(A, D)`$
- $`\mrm{Map}(f, \id_C) : \mrm{Map}(B, C) \to \mrm{Map}(A, D)`$
- $`\mrm{Map}(\id_A, g) : \mrm{Map}(A, C) \to \mrm{Map}(A, D)`$
$`\id_A`$ を単に $`A`$ と略記するのを許します。例えば:
- $`\mrm{Map}(f, C) = \mrm{Map}(f, \id_C)`$
- $`\mrm{Map}(A, g) = \mrm{Map}(\id_A, g)`$
射が出現すべき文脈に対象が現れたら恒等射と解釈します。
それでも肩の添字を使う場合
小さい字は使いたくない、と言いました。指数には Map を使うと言いました。それでも、右肩の小さい字を使う場合もあります。
成り行き上、指数をべき乗形式で書いたほうがいいことがあります。そのときはべき乗で書きます。
- $`B^A = \mrm{Map}(A, B)`$
- $`g^f = \mrm{Map}(f, g)`$
- $`g^A = \mrm{Map}(A, g)`$
- $`C^f = \mrm{Map}(f, C)`$
もうひとつのケースは、関数、関手、自然変換などに作用するオペレーターを右肩の小さい字で表すことがあります。例えば、カリー化オペレーターは右肩にキャップで表します。
- $`f^\cap = \mrm{Curry}(f) = \mrm{Curry}[A, B, C](f) = \mrm{Curry}_{A,B,C}(f)`$
オペレーターがたくさん出てくるときは、番号または名前をブラケットで囲んで右肩に乗せることにします。次がその例です。
- $`f^{[a]}`$
- $`f^{[1]}`$
- $`f^{[1, 2]} = f^{[1][2]} = (f^{[1]})^{[2]}`$
番号や一時的な名前で識別されるオペレーターは、局所的に定義されるもので、長期間使う気はない使い捨てオペレーターです。
ラムダ抽象のピリオドと括弧
関数/関手/自然変換の評価〈適用 | 引数渡し〉の図式順記法としてピリオドを使うことにします。
- $`x.f = f(x)`$
- $`X.F = F(X)`$
- $`f.F = F(f)`$
- $`X.\alpha = \alpha[X] = \alpha_X`$
そうすると、ラムダ抽象のピリオドが混乱をまねく邪魔者になります。なので、ピリオドはやめます。また、ラムダ抽象の本体部を囲む括弧は波括弧〈ブレイス〉にします。
- $`\lambda\, x\in X\{ \cdots \} = \lambda\, x\in X.(\, \cdots \,)`$
ラムダ抽象が入れ子になるときは、区切り記号にピリオドではなくてカンマを使うことにします。
- $`\lambda\, y\in Y, \lambda\, x\in X\{ \cdots \} = \lambda\,y\in Y. \lambda\, x\in X.(\, \cdots \,)`$
ラムダ式に現れる変数を置換することを示すメタ記号として次の形を使います。
$`\quad \mathscr{F}.(\lambda\, x\in A\{ \mathscr{E} \}) = \mathscr{E}\Subs{\mathscr{F}}{x}`$
これは、式 $`\mathscr{E}`$ のなかに出現する変数 $`x`$ を式 $`\mathscr{F}`$ で置き換えることを示しています。簡単な例は:
$`\quad a.(\lambda\, x\in A\{ f(x) \; \in B\} ) = \{f(x) \; \in B\}\Subs{a}{x}
= \{f(a) \; \in B\}`$
事例:基本公式
今まで述べた記法で、関数の評価、結合、直積、指数を書いてみます。
$`\For f:A \to B \In {\bf Set}\\
\For a \in A\\
\quad a.f = a.\lambda\, x\in A\{f(x) \; \in B\} \\
\quad = \{f(a) \;\in B\}\\
%
\For f:A \to B, g:B \to C \In {\bf Set}\\
\quad f; g = \lambda\, x\in A\{x.f \; \in B\} ; \lambda\, y\in B\{y.g \; \in C\} \\
\quad = \lambda\, x\in A\{ (x.f).g \;\in C\}\\
\quad \text{i.e. }x.(f;g) = (x.f).g\\
%
\For f:A \to B, h:D \to E \In {\bf Set}\\
\quad f\times g = \lambda\, x\in A\{x.f \; \in B\} \times \lambda\, z\in D\{z.h \; \in E\}\\
\quad = \lambda\, (x, z)\in A\times D\{ (x.f, z.h) \;\in B\times E\}\\
\quad \text{i.e. } (x, z).(f\times g) = (x.f, z.h)\\
%
\For f:A \to B, h:D \to E \In {\bf Set}\\
\quad h^f = \mrm{Map}(\lambda\, x\in A\{x.f \; \in B\} , \lambda\, z\in D\{z.h \; \in E\}) \\
\quad = \lambda\, u\in D^B\{ f;u;h \;\in E^A \}\\
\quad \text{i.e. } u.(h^f) = f;u;h
`$
これらは、頻繁に使うラムダ計算の公式です。
式で表現されるモノ
概念的事物 $`x`$ が式 $`\mathscr{E}`$ で表現されることを、
$`\quad \mrm{HasExpression}(x, \mathscr{E})`$
と書くことにします。等式 で $`x = \mathscr{E}`$ で書いてもさほど問題ありませんが、$`\mrm{HasExpression}`$ を短く書くために特別な記号 $`:=:`$ を使うことにします。
$`\quad x :=: \mathscr{E} \Iff \mrm{HasExpression}(x, \mathscr{E})`$
例えば次のように使います。
$`\For F, G :{\bf Set} \to {\bf Set} \In {\bf CAT}\\
\quad \alpha \in \mrm{Nat}(F, G)\\
\Imp \alpha :=: \lambda\, X\in |{\bf Set}|\{ X.\alpha \:\in \mrm{Map}(F(X), G(X))\}
`$
これは次のことを意味します。
集合圏から集合圏への関手 $`F, G`$ に対して、
$`\alpha`$ が $`F`$ から $`G`$ への自然変換ならば、
$`\alpha`$ はラムダ式による表示 $`\lambda\, X\in |{\bf Set}|\{ X.\alpha \:\in \mrm{Map}(F(X), G(X))\}`$ を持つ。
$`\alpha`$ がラムダ式による表示を持つだけでは自然変換とは言えません。表示以外に自然性の条件が別途要求されるからです。$`\alpha`$ が自然性の条件を満たすことを短く $`\alpha \text{ is-nat}`$ と書くとすれば:
$`\For F, G :{\bf Set} \to {\bf Set} \In {\bf CAT}\\
\quad \alpha \in \mrm{Nat}(F, G)\\
\Iff \alpha :=: \lambda\, X\in |{\bf Set}|\{ X.\alpha \:\in \mrm{Map}(F(X), G(X))\} \land \alpha \text{ is-nat}
`$
$`\alpha`$ が上記のようなラムダ式で表現されることは、次のように書いてもかまいません。
$`\quad \alpha \in \mrm{Sect}(\sum_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X)) \to |{\bf Set}|)`$
ここで、$`\sum_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X))`$ は大きな直和です。この直和は、インデックス集合である $`|{\bf Set}|`$ への自然な射影を持ちます。この射影に関するセクションの全体が $`\mrm{Sect}(\cdots)`$ です。セクションについては「セクションとタプル」に書いています。セクションの全体は、得体の知れない大きな集合ですが、条件 $`\alpha \text{ is-nat}`$ で絞り込むとよく知られた集合になります。
$`\quad \alpha \in \mrm{Sect}(\sum_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X)) \to |{\bf Set}|)
\land \alpha \text{ is-nat}\\
\Iff \alpha \in \overline{\prod}_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X))
`$
上記の $`\overline{\prod}`$ はエンドのことで、「自然変換の集合のエンド表示」で述べた内容です。今までのことをまとめて書けば:
$`\For F, G :{\bf Set} \to {\bf Set} \In {\bf CAT}\\
\quad \alpha \in \mrm{Nat}(F, G)\\
\Iff \alpha :=: \lambda\, X\in |{\bf Set}|\{ X.\alpha \:\in \mrm{Map}(F(X), G(X))\} \land \alpha \text{ is-nat}\\
\Iff \alpha \in \mrm{Sect}(\sum_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X)) \to |{\bf Set}|)
\land \alpha \text{ is-nat}\\
\Iff \alpha \in {\prod}_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X)) \land \alpha \text{ is-nat}\\
\Iff \alpha \in \overline{\prod}_{X\in |{\bf Set}|} \mrm{Map}(F(X), G(X))
`$
自然変換の計算例
実際の計算をやってみましょう。
$`A, B`$ は集合圏上の単項式関手とします。スピヴァック〈David I. Spivak〉の記法を使って、次のように書きます。
$`\quad A = A1\, y^{A2} = A1\times y^{A2}\\
\quad B = B1\, y^{B2} = B1 \times y^{B2}
`$
スピヴァックの $`y^-`$ については、「米田テンソル計算 3: 米田の「よ」、米田の星、ディラックのブラケット 再論 // スピヴァックの指数記法」を参照してください。
計算に使う基本的な事項は以下のようなものがあります。
- カリー同型:
$`\mrm{Map}(A\times B, C) \cong \mrm{Map}(A, \mrm{Map}(B, C) )`$ - ラムダ抽象:
$`f\in \mrm{Map}(A, B) \Iff f :=: \lambda\, x\in A\{f(x)\;\in B\}`$ - 入れ子のラムダ抽象:
$`\lambda\, y\in B,\lambda\, x\in A\{f(x, y)\;\in C\} = \lambda\, y\in B\{ \lambda\, x\in A\{f(x, y)\;\in C\} \}`$ - ラムダ抽象の順序入れ替え:
$`\lambda\, y\in B,\lambda\, x\in A\{f(x, y)\;\in C\} = \lambda\, x\in A, \lambda\, y\in B\{f(x, y)\;\in C\}`$
単項式関手のあいだの自然変換を変形して、別な表示を求めます。
$`\quad \alpha \in \mrm{Nat}(A, B)\\
\Using \text{HasExpression}\\
%
\Iff \alpha :=: \lambda\, X\in |{\bf Set}|\{ X.\alpha \;\in \mrm{Map}(A(X), B(X)) \} \land \alpha \text{ is-nat}\\
%
\Using A\: の定義\\
\Iff \alpha :=: \lambda\, X\in |{\bf Set}|\{ X.\alpha \;\in \mrm{Map}(A1\times X^{A2}, B(X)) \} \land \alpha \text{ is-nat}\\
%
\Using カリー同型\\
\Iff \alpha^{[1]} :=: \lambda\, X\in |{\bf Set}|\{ (X.\alpha)^\cap \;\in \mrm{Map}(A1, \mrm{Map}( X^{A2}, B(X)) ) \} \\
\quad \land \alpha \text{ is-nat}\\
%
\Using ラムダ抽象\\
\Iff \alpha^{[1]} :=: \lambda\, X\in |{\bf Set}|\{
\lambda\, a\in A1\{ (X.\alpha)^\cap(a) \; \in \mrm{Map}( X^{A2}, B(X)) \} \} \\
\quad \land \alpha \text{ is-nat}\\
%
\Using 入れ子のラムダ抽象\\
\Iff \alpha^{[1]} :=: \lambda\, X\in |{\bf Set}|,
\lambda\, a\in A1 \{ (X.\alpha)^\cap(a) \; \in \mrm{Map}( X^{A2}, B(X)) \} \\
\quad \land \alpha \text{ is-nat}\\
%
\Using ラムダ抽象の順序入れ替え\\
\Iff \alpha^{[1, 2]} :=: \lambda\, a\in A1,
\lambda\, X\in |{\bf Set}| \{ (X.\alpha)^\cap(a) \; \in \mrm{Map}( X^{A2}, B(X)) \} \\
\quad \land \alpha \text{ is-nat}\\
%
\Using 命題の証明(別途)\\
\Iff \alpha^{[1, 2]} :=: \lambda\, a\in A1,
\lambda\, X\in |{\bf Set}| \{ (X.\alpha)^\cap(a) \; \in \mrm{Map}( X^{A2}, B(X)) \}
\quad \land
\forall a\in A1.\; \alpha^{[1, 2]}(a) \text{ is-nat }\\
%
\Using 自然変換であること\\
\Iff \alpha^{[1, 2]} :=: \lambda\, a\in A1 \{ \alpha^{[1, 2]}(a) \;\in \mrm{Nat}(y^{A2}, B) \} \\
\quad \text{where }\alpha^{[1, 2]}(a) = \lambda\, X\in |{\bf Set}| \{ (X.\alpha)^\cap(a) \; \in \mrm{Map}( X^{A2}, B(X)) \}\\
%
\Using ラムダ抽象\\
\Iff \alpha^{[1, 2]} \in \mrm{Map}(A1, \mrm{Nat}(y^{A2}, B))
`$
ここで、$`\alpha \mapsto \alpha^{[1]}`$ というオペレーターはカリー化から誘導されるオペレーターです。$`\alpha^{[1]} \mapsto \alpha^{[1][2]}`$ は、ラムダ束縛の順序を入れ替えることから誘導されるオペレーターです。中間で次の命題を使っていますが、これは別に証明が必要です。
$`\quad
\alpha \text{ is-nat} \Imp \forall a\in A1.\; \alpha^{[1, 2]}(a) \text{ is-nat }
`$
細部をちゃんと埋めれば次が言えます*1。
$`\quad \mrm{Nat}(A, B) \cong \mrm{Map}(A1, \mrm{Nat}(y^{A2}, B) )`$
同時に、この同型を与える写像も得られます。
$`\quad \mrm{Nat}(A, B) \ni \alpha \mapsto \alpha^{[1, 2]} \in \mrm{Map}(A1, \mrm{Nat}(y^{A2}, B) )`$
こんなことして何を計算しているかは、また語る機会があるでしょう、たぶん。
*1:この同型は、具体的な計算によらずにホムセット関手の連続性(極限・余極限の保存)から出ます。が、実際の計算に使うには具体的な表示が有利です。