リントンの定理： æ¦‚è¦ã€å®Ÿä¾‹ã€æ³¨æ„äº‹é …

最近の記事「リントンの定理」で述べた、リントン〈Fred Linton〉による（と思われる）代数-モデル対応定理〈algebra-model correspondence theorem〉を単に「リントンの定理」と呼ぶことにします。

リントンの定理の具体化のなかで一番簡単だと思われる“半群に対するリントンの定理”を実例として、リントンの定理の概要を述べます。

リントンの定理周辺には、誤解を招く〈misleading | error-prone〉ことがたくさんたくさん在ります。落とし穴だらけと言っていいでしょう。なので、落とし穴に落ちないための注意事項も述べます。$`
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\o}[1]{ \overline{#1} }
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\id}{ \mathrm{id} }
\newcommand{\In}{ \text{ in }}
%\newcommand{\On}{ \text{ on }}
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\op}{ \mathrm{op}}
\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\EQV}{\mathrel{\overset{\sim}{\equiv}} }
\newcommand{\T}[1]{\text{#1} }
\require{color}
\newcommand{\NX}[1]{ \textcolor{orange}{ {#1}} } % New Expression
\newcommand{\KX}[1]{ \textcolor{blue}{#1} } % Known EXpression
`$

内容：

半群の指標

半群の指標は次のように書けます。

$`\T{signature }\NX{\mrm{Semigroup}}\: \{\\
\quad \T{sort }\NX{U}\\
\quad \T{operation }\NX{m}: U \KX{\times} U \to U\\
\quad \T{equation }\NX{\T{assoc}} :: (m \KX{\times} \KX{\id}_U) \KX{;} m \twoto (\KX{\id}_U \KX{\times} m) \KX{;} m : U \KX{\times} U \KX{\times} U \to U\\
\}
`$

文字色の約束は「構造記述のための指標と名前 1/n 基本」と同じで； オレンジ色は初出の名前、青色は既知の名前です。一回オレンジ色で導入した名前は、その後は黒で書いてます。

$`(U\times U)\times U`$ と $`U\times (U\times U)`$ のあいだの変換である結合律子〈associator〉$`\alpha_{U,U,U}`$ も律儀に書くなら次のようです。

$`\T{signature }\NX{\mrm{Semigroup}}\: \{\\
\quad \T{sort }\NX{U}\\
\quad \T{operation }\NX{m}: U \KX{\times} U \to U\\
\quad \T{equation }\NX{\T{assoc}} :: (m \KX{\times} \KX{\id}_U) \KX{;} m \twoto \KX{\alpha}_{U,U,U} \KX{;} (\KX{\id}_U \KX{\times} m) \KX{;} m : (U \KX{\times} U) \KX{\times} U \to U\\
\}
`$

これらの指標は、直積〈デカルト積〉 $`\times`$ を持つ圏（典型例は集合圏）で解釈することを前提にしています。圏ではなくて複圏〈multicategory | オペラッド | operad〉で解釈する前提なら、次のような指標になります。

$`\T{signature }\NX{\mrm{Semigroup}}\: \{\\
\quad \T{sort }\NX{U}\\
\quad \T{operation }\NX{m}: (U, U) \to U\\
\quad \T{equation }\NX{\T{assoc}} :: m \mathop{\KX{;_1}} m \twoto m \mathop{\KX{;_2}} m : (U, U, U) \to U\\
\}
`$

プロファイル $`(U, U)\to U`$ を持ったオペレーション $`m`$ を絵に描くならワイ字形 Y になります。3本の脚〈半ワイヤー | ポート〉を持ったボックス〈ノード〉ですが、上の2本が入力、下の1本が出力です。

結合法則 $`\T{assoc}`$ の言っていることを絵に描きましょう。ちゃんと描くの面倒だから、象形文字を使ったアスキーアートで図示します。

Y  　  Y 
 Y ⇒ Y

上段の Y（象形文字）を、下段の一番目（左）の入力に“接ぎ木〈grafting〉”する操作が $`;_1`$ です。下段のニ番目（右）の入力に“接ぎ木〈grafting〉”する操作は $`;_2`$ です。$`m \mathop{;_1} m`$ を $`m \mathop{;_2} m`$ に変形〈書き換え | 描き換え〉してもよいというのが結合法則です。逆向きの変形が明示的に宣言されてませんが、「すべての変形は可逆である」ことが暗黙に仮定されています*1。

ワイ字形 Y （脚付きボックス）の脚は適当に伸ばして描いてもいいので、結合法則は次のように描いてもかまいません。

Y I 　 I Y 
 Y  ⇒  Y

これなら、$`(m \times \id_U) ; m \twoto (\id_U \times m) ; m`$ との関係が明白でしょう。

$`m:U\times U\to U`$ と $`m:(U, U)\to U`$ の違いは、タプル1変数関数と2変数関数の違いと同様なのですが、「タプル1変数関数と2変数関数の違い」はなかなかに理解が難しいようです。以下の過去記事が参考になるでしょう。

• タプル1変数関数と多変数関数

タプル1変数関数（デカルト圏の射）と多変数関数（複圏〈オペラッド〉の複射）は相互に変換は出来ますが、それぞれにメリット・デメリットがあるので、用途に応じて使い分けます。この記事では、多変数関数の一般化・抽象化である複圏〈オペラッド〉の複射〈multimorphism〉を主に使います。

半群の指標のモデル

前節の指標のなかで、複射のプロファイル $`m:(U, U) \to U`$ を使った指標を考えます。指標は、ソート、オペレーション、等式的法則を宣言しているだけで、実際の半群を定義しているわけではありません。

実際の半群とは、具体的・個別特定な代数系です。具体的・個別特定な代数系を定義するには、まず、ソート記号〈ソート名〉 $`U`$ に具体的・個別特定な集合を割り当てる必要があります。一例として次のように割り当てましょう。

$`\quad U \mapsto \mbf{N}_{\ge 10} = \{n\in \mbf{N} \mid n \ge 10\}`$

この割り当てのもとで、$`(U, U)`$ は $`(\mbf{N}_{\ge 10}, \mbf{N}_{\ge 10})`$ となります。この“集合のリスト”の解釈は、2変数関数の引数の仕様です。第一引数の型が $`\mbf{N}_{\ge 10}`$ で、第二引数の型も同じく $`\mbf{N}_{\ge 10}`$ です。

オペレーション記号〈オペレーション名〉 $`m`$ には、具体的・個別特定な関数〈写像〉を割り当てます。引数の型は $`(\mbf{N}_{\ge 10}, \mbf{N}_{\ge 10})`$ で、戻り値の型は $`\mbf{N}_{\ge 10}`$ です。2変数関数ですが、最終的にはタプル1変数関数に帰着するので、$`m`$ に割り当てる関数は例えば次だとします。

$`\quad m \mapsto \mrm{addNat}_{\ge 10}\\
\quad \text{where }\mrm{addNat}_{\ge 10} : \mbf{N}_{\ge 10}\times\mbf{N}_{\ge 10} \to \mbf{N}_{\ge 10} \In \mbf{Set}
`$

ここで出てきた $`\mrm{addNat}_{\ge 10}`$ は、具体的・個別特定な関数で、通常の自然数の足し算を10以上の自然数達に制限した関数です。

半群の結合法則を表す記号〈名前〉$`\T{assoc}`$ には、実際に等式が成立するという事実を割り当てます。神様なら、等式の成立を一瞬で確認できるでしょうが、我々人間は無限集合に関する事実をシラミ潰しでは確認できないので、事実の証拠となる証明を提示します。つまり、記号〈名前〉$`\T{assoc}`$ に割り当てるべきモノは証明です。今は、そういう証明はあるものだとします。

$`\quad \T{assoc} \mapsto \T{👌}`$

OKマーク 👌 は、例えば「名前が指すモノ： 単射を例として」で使っているもので、「証明があると思ってね」という意味のマークです。最初にOKマークを使ったのは「曖昧性を減らす： Diag構成を事例として」です。

3つの割り当ての組
$`\quad (U \mapsto \mbf{N}_{\ge 10}, m \mapsto \mrm{addNat}_{\ge 10}, \T{assoc} \mapsto \T{👌})`$
により、具体的・個別特定な代数系としての半群が定義されます。半群の指標（それ自体で半群ではない）から見たとき、具体的・個別特定な半群はモデル〈model〉といいます。つまり、次のように言えます。

• 半群とは、半群の指標のモデルである。

具体的・個別特定な半群 $`(U \mapsto \mbf{N}_{\ge 10}, m \mapsto \mrm{addNat}_{\ge 10}, \T{assoc} \mapsto \T{👌})`$ を $`(\mbf{N}_{\ge 10}, \mrm{addNat}_{\ge 10})`$ のように略記するのが普通です。

個々の半群が何であるかはハッキリしたので、それらを寄せ集めてすべての半群のクラス（大きい集合）が定義できます。そればかりではなくて、半群のあいだの準同型射〈homomorphism〉という概念が自動的に定義できるので（これが関手意味論のミソ）、半群の圏〈category of semigroups〉が自動的に定義できます。半群の圏とは、半群の指標 $`\mrm{Semigroup}`$ のモデルの圏〈category of models〉なので、次のように書きます。

$`\quad \mrm{Model}(\mrm{Semigroup}) \;\in |\mbf{CAT}|`$

正確に言えば、モデルを構成しているターゲット圏が集合圏なので：

$`\quad \mrm{Model}(\mrm{Semigroup}, \mbf{Set})\;\in |\mbf{CAT}|`$

この記事ではターゲット圏を集合圏に固定するので、ターゲット圏は省略します。

半群の指標に限らず、なんらかの指標 $`\Sigma`$ があるとき、指標 $`\Sigma`$ のモデルの圏は次のように書きます。

$`\quad \mrm{Model}(\Sigma)\;\in |\mbf{CAT}|`$

半群の指標のリントン／ローヴェア・モナド

リントンの定理にはモナドが登場します。このモナドが、リントンの定理の主役です。が、名前が付いてないようです。ここでは、リントン／ローヴェア・モナド〈Linton-Lawvere monad〉と呼ぶことにします。Linton も Lawvere も頭文字は L なので、リントン／ローヴェア・モナドは黒板文字エル $`\mathbb{L}`$ で表します*2。

リントン／ローヴェア・モナドは、指標 $`\Sigma`$ に対して決まるので、次のように書けます。

$`\quad \mathbb{L}_\Sigma = (\mathbb{L}_\Sigma, \mu, \eta)/\mbf{Set}`$

ここで、モナド自体とモナドの台関手〈underlying functor〉を同じ記号で表す“記号の乱用”を使ってます。$`\mu`$ はモナド乗法、$`\eta`$ はモナド単位です。$`\mbf{Set}`$ はモナドの基礎圏〈ground category〉です。つまり、リントン／ローヴェア・モナドは、集合圏上のモナドです。

指標 $`\Sigma`$ として、半群の指標 $`\mrm{Semigroup}`$ を取ったとき、そのリントン／ローヴェア・モナドは、非空リスト・モナドになります。と言っても唐突過ぎるでしょうが、唐突さを埋めるのがリントンの定理です。とりあえず今は、謎のマシナリーによって、半群の指標 $`\mrm{Semigroup}`$ から非空リスト・モナドが生み出されると思ってください。

$`\quad \mathbb{L}_{\mrm{Semigroup}} = (\mrm{List}_+, \mrm{flatten}, \mrm{singl})/\mbf{Set}`$

右辺の非空リスト・モナドについて説明します。

1. 集合 $`X`$ に対して $`\mrm{List}_+(X)`$ は、空リストは除いたリストの集合。
2. 関数〈写像〉 $`f:X \to Y`$ に対して $`\mrm{List}_+(f):\mrm{List}_+(X) \to \mrm{List}_+(Y)`$ は、リストの“マップ関数”。
3. 集合 $`X`$ に対する $`\mrm{flatten}_X :\mrm{List}_+(\mrm{List}_+(X)) \to \mrm{List}_+(X)`$ は、入れ子のリストを平坦化〈flatten〉する関数。
4. 集合 $`X`$ に対する $`\mrm{singl}_X : X \to \mrm{List}_+(X)`$ は、$`X`$ の要素ひとつだけからなる単項リスト〈singleton list〉を対応させる関数。

リントンの定理

リントンの定理は、指標 $`\Sigma`$ に対して、次の圏同値を主張します。

$`\quad \mrm{EM}(\mathbb{L}_\Sigma) \EQV \mrm{Model}(\Sigma) \In \mbf{CAT}`$

ここで、$`\mrm{EM}(\hyp)`$ はモナドのアイレンベルク／ムーア圏で、$`\EQV`$ は圏同値（圏同型とは限らない）の記号だとします。

$`\Sigma := \mrm{Semigroup}`$ と具体化すると：

$`\quad \mrm{EM}(\mathbb{L}_\mrm{Semigroup}) \EQV \mrm{Model}(\rm{Semigroup}) \In \mbf{CAT}`$

右辺の $`\mrm{Model}(\rm{Semigroup})`$ については既に説明しました -- これは半群の指標のモデルの圏、つまりは半群の圏でした。左辺に出てくる $`\mathbb{L}_\mrm{Semigroup}`$ は（結果だけを言えば）非空リスト・モナド $`\mrm{List}_+`$ でした。したがって：

$`\quad \mrm{EM}(\mrm{List}_+) \EQV \mrm{Model}(\rm{Semigroup}) \In \mbf{CAT}`$

アイレンベルク／ムーア圏 $`\mrm{EM}(\mrm{List}_+)`$ の対象がどんなモノかと言うと； $`A = (\u{A}, \alpha_A)`$ のように書けるアイレンベルク／ムーア代数です。より具体的には：

1. $`\u{A}`$ は集合（アイレンベルク／ムーア代数の台集合）。
2. $`\alpha_{A}`$ は、$`\mrm{List}_+(\u{A}) \to \u{A}`$ という関数（アイレンベルク／ムーア代数の演算）。
3. 演算 $`\alpha_A`$ は、アイレンベルク／ムーア代数の法則（結合法則と単位法則）を満たす（簡単な説明は「一般化ハイパーグラフ 再論 // アイレンベルク／ムーア代数」参照）。

リントンの定理が与える圏同値を、特に $`\Sigma = \mrm{Semigroup}`$ の場合に考えるなら：

• 任意の半群（半群の指標のモデル） $`S = (\u{S}, m_S)`$ に、アイレンベルク／ムーア代数 $`A = (\u{A}, \alpha_A)`$ が対応する。
• 任意の半群の射 $`f:S \to T`$ に対して、アイレンベルク／ムーア代数の射 $`\varphi : A \to B`$ が対応する。
• この対応は関手である。
• アイレンベルク／ムーア代数に半群を対応させる逆向きの関手もある。
• これら、互いに逆向きの2つの関手は、半群の圏と（非空リスト・モナドの）アイレンベルク／ムーア代数の圏のあいだの圏同値を与える。

一般的なリントンの定理のメカニズムが分からなくても、半群の場合（特殊事例）なら、圏同値を具体的に構成することが出来るでしょう。半群の場合を観察することにより、一般的なリントンの定理のフィーリングを掴むことが出来ると思います。

注意事項への注意事項

過去記事「一般化ハイパーグラフ → P-バンドル、P-ファミリー」は、「一般化ハイパーグラフ」という呼び名を、「P-バンドル」または「P-ファミリー」に変更するよ、という内容でした。変更の理由は、「頂点」「辺」などの用語が誤認・誤解・混乱を招きそうだからです。次のように書いています。

実にまったく言霊の悪影響は恐ろしいものです。

リントンの定理周辺は、言霊の悪影響が猛威を振るう場所になっています。「セオリー」という言葉から余計な連想をしてしまったり、「オペレーション」という言葉のコンフリクト〈かち合い | バッティング〉で混乱したり、「代数」という言葉のオーバーロードに苦しんだりします。

また、「モノイドのような代数系の単位とモナド単位は関係があるのだろう」といった間違った推測をしたりします。推測の根拠は「単位」という言葉の一致だけです。まさに、言霊にたぶらかされています。代数系の単位がモナド単位と無関係なのは、前節の半群の例（半群に単位はない）から明らかでしょう。

ローヴェアの「セオリー」は“ある種の圏”という意味しかないし、「オペレーション」は文脈により、関数、複射、コンビネータ、それらを表す予定の名前〈記号〉などの意味で使われます。なんでもかんでも「代数〈algebra〉」と呼んでしまうことは、広く蔓延した悪習です。言葉の一致や類似で推測するなんてのは、言語道断です -- 絶対にやらないように。

ここから先は、落とし穴（主に言霊由来の陥穽）に落ちないための注意事項を述べます。

セオリー

ローヴェアは、代数系（半群、モノイド、環など）の定義のために指標を使っていません。その代わりに代数セオリー〈algebraic theory〉、あるいは略してセオリー〈theory〉と呼ばれる構造を使っています。セオリーはある種の圏なので、現在ではローヴェア圏〈Lawvere category〉と呼ばれることが多いです（「ローヴェア・セオリーとその周辺」参照）。他にも山のように別名があります。過去記事「用語のバリエーション記述のための正規表現 // ウンザリする例」で例に出しています。

ローヴェアの代数セオリーは後で一般化されたので、オリジナルの代数セオリーは単純代数セオリー〈simple algebraic theory〉、またはローヴェア代数セオリー〈Lawvere algebraic theory〉と形容詞付きで呼ぶこともあります。さらに SAT または LAT という省略語も使われます。僕は、省略語の SAT （または LAT）を使うのがいいと思います。なぜなら、theory という誤認誘発性が高い言葉が T 一文字になって隠れるからです。という理由で、ここではローヴェアの代数セオリー（と呼ばれる圏）はSAT圏〈SAT category〉と呼びます。（[追記]「「セオリー」は使わざるをえないな」も参照。[/追記]）

ローヴェア自身は使ってませんが、SAT圏の生成系としてSAT指標〈SAT signature〉があります。色々なSAT指標から同一のSAT圏が生成できるという意味で、SAT指標には恣意的自由度があり過ぎます。ローヴェアは恣意的自由度を嫌ったのでしょう。しかし、現実的にはSAT指標を使わざるを得ないので、SAT指標を避ける態度は取りません。

ローヴェアはSAT圏を使いましたが、SAT複圏〈SATオペラッド | SAT {multicategory | operad}〉を使うアプローチもあります。SAT複圏の生成系はSAT複指標〈SAT multi-signature〉と呼べばいいでしょう。半群の例で出した $`m:(U, U)\to U`$ というプロファイルはSAT複圏〈SATオペラッド〉を想定しているので、あの指標はSAT複指標だったということになります。

SAT圏を使うか、SAT複圏〈SATオペラッド〉を使うかは、用途と好みにより決めればいいことですが、僕はSAT複圏〈SATオペラッド〉のほうが好みです（SAT複圏にこだわってはいませんが）。

なお、よく知られたSAT〈LAT〉の拡張・一般化として、GAT〈generalized algebraic theory〉、EAT〈essentially algebraic theory〉があります。

モデル

この記事で、SAT指標またはSAT複指標に対してモデルを定義しました。半群の指標のモデルが半群でした。指標／複指標を使わない場合は、SAT圏またはSAT複圏に対してモデルを定義します。

• SAT指標で生成されたSAT圏のモデルは、SAT指標のモデルと同じ。
• SAT複指標で生成されたSAT複圏〈SATオペラッド〉のモデルは、SAT複指標のモデルと同じ。

「モデル」が2つの意味で使われています。個人的には、SAT圏／SAT複圏に対して定義されるモデルは「表現〈representation〉」と呼んで区別しています。

• SAT指標で生成されたSAT圏の表現は、SAT指標のモデルと同じ。
• SAT複指標で生成されたSAT複圏〈SATオペラッド〉の表現は、SAT複指標のモデルと同じ。

この「表現」の用法は、「群の線形表現」などの「表現」と同じ意味・解釈なので、けっこう具合がいいと思います。

とはいえ、「モデル」「表現」「代数」の使い方・使い分けはグチャグチャなので、「指標／複指標のモデル」「圏／複圏の表現」という使い分けも個人的ローカルルールに過ぎません。

オペレーション

指標の宣言に、$`\T{operation }m:(U, U)\to U`$ のようにキーワード $`\T{operation}`$ を使いました。キーワードの選定は趣味的・恣意的なんで、$`\T{operation}`$ というワードを使ったからどうだ、ってのは無意味な話です。が、SAT複指標に関しては、キーワード $`\T{operation}`$ によりSAT複圏〈SATオペラッド〉の生成系〈system of generators〉となるオペレーションを宣言しています。

複圏〈オペラッド〉のオペレーションとは、圏の射と類似の概念で、複射〈multimorphism〉とも呼びます。「複射」を使ったほうが無難です。なぜなら、「オペレーション」は演算〈写像〉の意味でも普通に使うからです。

$`\cat{M}`$ を複圏〈オペラッド〉として、オペラッド結合の特定の成分は次のように書けます。

$`\quad (;_2) : \cat{M}( (A, B), A) \times \cat{M}((A, A), C) \to \cat{M}((A, A, B), C) \In \mbf{Set}`$

ここで、$`\cat{M}( \hyp , \hyp)`$ は圏のホムセットと同様で、特定のプロファイル〈複プロファイル〉を持つ複射の集合です。複射のオペラッド結合を与える写像 $`(;_2)`$ のことも、オペラッドのオペレーションと呼ぶことがあります。これは、なかなかに悲惨な結果をまねきます。次のような言い回しがまかり通るのです。

• オペラッドのオペレーションは、オペラッドのオペレーションを引数に取るオペレーションである。

さすがにひどい。混乱を緩和するために、次のような言い回しを使います。

• オペラッドのコンビネータは、オペラッドのオペレーションを引数に取る写像である。
• オペラッドのオペレーションは、オペラッドの複射を引数に取る関数である。

コンフリクトしている言葉「オペレーション」を、「コンビネータ」「写像」「複射」「関数」などに置き換えています。「コンビネータ」「複射」「写像〈関数〉」を使い分ければ混乱は起きないでしょうし、一時は僕もそうしていました。最近また横着になって、「コンビネータ」は「オペレーション」で済ませています。横着だけではなくて、「コンビネータ」が「コンビネーション」と似てる（誤認のリスクがある）ので避けてるってこともあります（次節参照）。

コンビネーション

ここでのコンビネーションは linear combination と同じ用法の combination です。linear は vector space のことを表すので、vector-space combination と言っても同じです。

"linear combination" は、「線形結合」と翻訳されますが、「結合」は "composition" とかぶります。直訳の「組み合わせ」も他の意味（例えばタプル）に解釈されそうです。それでカタカナ書き「コンビネーション」とします。

vector-space combination〈ベクトル空間コンビネーション〉の vector-space の所を他の代数系に置き換えると、semigroup combination〈半群コンビネーション〉、 ring combination〈環コンビネーション〉 monoidal-category combination〈モノイド圏コンビネーション〉 などと言えます。これは、それぞれの代数系において許される（解釈可能な）式〈expression〉のことです。例えば：

• ベクトル空間コンビネーションは、定数・変数をもとに、足し算とスカラー倍で組み立てられた式
• 半群コンビネーションは、定数・変数をもとに、掛け算（と呼ぶ二項演算）だけで組み立てられた式
• 環コンビネーションは、定数・変数をもとに、足し算と掛け算で組み立てられた式
• モノイド圏コンビネーションは、定数・変数をもとに、射の結合とモノイド積で組み立てられた式

「式」を使わずに「コンビネーション」としているのは、テキスト表現に限らず、ストリング図などによる絵図表現も考えるからです。スケマティックな状況（「スケマティック」参照）では、テキスト表現は出てこないで絵図表現だけを相手にします。絵図的なコンビネーションは、ストリング図やストリング図類似の図〈string-diagram-like diagram〉です。

入れ子コンビネーションと平坦コンビネーション

「ストリング図、ストリング図動画が“使える”とは？」の最後で「みんな、ストリング図を使おうぜ」と推奨してます。その理由には、テキスト表現ではうまく表現できなかったり、無駄に煩雑になってしまうことがある、ということもあります。

入れ子コンビネーション〈nested combination〉と平坦コンビネーション〈flat combination〉の区別も、テキスト表現では難しいです。例えば、
$`\quad (2x + 1) + (3y -2)`$
というテキストの式が入れ子か平坦かの区別は難しい、というか原理的に区別できないです。括弧があるから入れ子だとも言えないのです*3。

絵図表現（例えばストリング図）においては、入れ子を明白に示す幾つかの手段があります。例えば、シーム〈seam〉（「穴、スポット、エリア、シーム」参照）を使って入れ子を表現できます。入れ子コンビネーションと平坦コンビネーションの区別は極めて重要です。逆に言うと、入れ子コンビネーションと平坦コンビネーションの区別が出来ない状況は致命的にマズイのです。

リントン／ローヴェア・モナドのモナド乗法とは、詰まるところ、入れ子コンビネーションの入れ子を平坦化〈flatten〉する操作です。アイレンベルク／ムーア代数の演算は、平坦コンビネーションに対して一気に計算結果を求める操作です。入れ子コンビネーションと平坦コンビネーションのあいだを行ったり来たりすることが、実は、リントン／ローヴェア・モナド構成のキモになります。

穴、変数

「ストリング図、ストリング図動画が“使える”とは？ // 穴、境界、ストリング図テンプレート」において、ストリング図テンプレート〈string diagram template〉と穴〈hole〉について説明しました。キャンバスにあいた穴とは、テキストの式なら変数です。穴／変数の同義語として、ポジション〈position〉、プレースホルダー〈placeholder〉、スロット〈slot〉、不定元〈indeterminate〉などがあります。これらの言葉達は、多少のニュアンスはあるにしろ同義語です。国語辞書的（あるいは英語辞書的）ニュアンスに注意を向けてしまうと、言霊の悪さでドライな思考が邪魔されます。

穴に内容〈中身 | content〉を詰めて埋めることは、変数への代入〈substitution〉と同じです。充填〈filling〉、挿入〈insertion〉、はめ込み〈inset〉、具体化〈instantiation〉、割り当て〈assignment〉は、代入と同義語です -- 同じ操作を意味します。穴を、ストリング図やストリング図テンプレートで埋めるときは、結合〈composition〉、接ぎ木〈grafting〉、貼り合わせ〈gluing〉、溶接〈welding〉、裁縫〈sewing〉などともいいます。背後にあるメンタルモデル／メタファー／典型的具体例と歴史的経緯により、さまざまな用語が生み出されます。逆に言うと、メンタルモデル／メタファー／典型的具体例と歴史的経緯を除去してしまえば、フォーマルにはすべて同じことです。

名前や記号を見ただけでは、また雑に描いた絵を見ただけでは、穴〈変数〉と中身が詰まった〈ソリッドな〉ボックス〈定数〉の区別は難しいです。穴〈変数〉は充填可能〈fillable〉／置き換え可能〈replaceable〉で、ソリッドボックス〈定数〉に対しては充填／置き換えが出来ません。しかし、あたかもソリッドボックス〈定数〉として扱っていたボックスを「実は穴でした」とちゃぶ台返しをすることはしばしばあります。中学校でも、「$`ax + b`$ の $`x`$ は変数だが $`a, b`$ は定数」と言っておきながら、「$`a`$ に $`2`$ 、$`b`$ に $`1`$ を代入したら $`2x + 1`$」とかちゃぶ台返しをします。ほんとに定数なら代入できるわけないじゃん*4。

計算

代数系とは「計算を行うための仕掛け」です。そして、指標とリントン／ローヴェア・モナドは「代数系を定義するための仕掛け」です。指標はモデルとして代数系を定義し、リントン／ローヴェア・モナドはアイレンベルク／ムーア代数として代数系を定義します。リントンの定理が、「モデル ←→ 代数」対応を与えるので、2つの定義方法は同等な定義能力を持ちます。

モデルとして定義された代数系では、幾つかの基本演算〈primitive operation〉達が計算ツールとして提供されます。一方のアイレンベルク／ムーア代数では、最も一般的な単一の総演算〈collective operation〉だけが提供されます。モデルに代数を対応付けるときには、基本演算を組み合わせて総演算を構成して、「どのような組み合わせ方をしても同一の総演算が一意的に決まる」ことを示す必要があります。そのために、「代数系における計算とは何か？」という問〈とい〉に正面から向かい合うことになります。

総演算は、任意の平坦コンビネーションに対して一気に計算結果を出力します。しかし、総演算も基本演算の組み合わせのはずで、実際には計算過程〈computation process〉を遂行して結果が得られているはずです。平坦コンビネーションを入れ子コンビネーションに分解して、入れ子の内側からコツコツと基本演算の繰り返しをしているはずです。ひとつの平坦コンビネーションに対して、そのようなコツコツと遂行する計算過程は膨大な数〈かず〉存在するかも知れません。どんな計算過程で計算しても、最終結果は同じであること -- 一般結合法則〈general associative law〉は、リントンの定理のコーナーストーンです。

計算過程は、空間方向と時間方向に展開した組み合わせ幾何的対象物〈combinatorial geometric object〉として表現するのが適切だと思われるので、リントンの定理をスケマティックな状況で定式化して証明するのは自然〈オーガニック〉だと僕は考えています。

*1:変形〈書き換え | 基本遷移〉を集合圏内の2-射として解釈します。集合圏の2-射は常に可逆です。「任意の圏を等式により2-圏とみなす」参照。

*2:手書きのときは、'L' を重ね書きすればいいでしょう。

*3:計算の優先順〈precedence〉を示す括弧とは別に、入れ子を構成する括弧を導入すれば、テキストでも入れ子を表現できます。が、実際にそのような表現手法が使われているわけではありません。

*4:「定数」がほんとに個別特定の具体物を指すこともありますが、多くの場合はスコープが違う変数のことです。