ジャズ・マイヤース〈David Jaz Myers〉が、Categorical Systems Theory のなかで、「アリーナの二重圏」という概念を定義しているのですが、なんだかピンとこない。実例を考えてみました。具体的な状態遷移系をタイト射とする二重圏です。この具体的な状態遷移系達の二重圏を、できるだけ大道具を使わずに直接的に定義してみます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\In}{\text{ in }}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\newcommand{\Bun}[2]{ \begin{bmatrix} {#1}\\ \downarrow\\{#2}\end{bmatrix} }
\newcommand{\BunM}[2]{ \begin{bmatrix} {#1}\\{}\\{#2}\end{bmatrix} }
\newcommand{\BunF}[2]{ \begin{pmatrix} {#1}\\{}\\{#2}\end{pmatrix} }
\newcommand{\LensM}[2]{ \begin{pmatrix} {#1}\\{\leftarrow}\\{#2}\end{pmatrix} }
\newcommand{\DM}[4]{ #1 \underset{#4}{\overset{#3}{\Box}} #2} % Double Morphism
\newcommand{\DO}[4]{ {^{#1}_{#3}\Box^{#2}_{#4}} } % Double Objects
\newcommand{\tr}{\mathrm{t} }
`$
内容：
- マイヤース本との違い
- 古典的状態遷移系
- バンドルとバンドル射
- バンドル射のベース・ファイバー表示
- バンドルのあいだのレンズ射
- レンズ射の結合
- レンズ射は状態遷移系である
- 単純レンズ射
- バックエンドとラッパー
- 状態遷移系のあいだの準同型射
- 準同型射の整合性条件
- 二重圏との関係
- おわりに
続きの記事：
マイヤース本との違い
マイヤースの教科書は以下のものです。
- [Mye23-]
- Title: Categorical Systems Theory
- Author: David Jaz Myers
- Date: September 3, 2023
- Pages: 311p
- URL: https://www.davidjaz.com/Papers/DynamicalBook.pdf
マイヤース本におけるアリーナ〈arena〉達の二重圏は、抽象的一般的概念ですが、ここでは具体例を作ります。具体例は状態遷移系をタイト射とする二重圏です。集合と関数〈写像〉だけを使って二重圏を組み立てます。素材はすべて集合圏 $`\mbf{Set}`$ から持ってくるので、抽象的圏はまったく出てきません。すべて具体的です。
具体例では、一般論の用語は使いません。一般論と具体例での用語の対応は以下のとおりです。
| マイヤース本 | この記事（具体例） |
|---|---|
| アリーナ達の二重圏 | 状態遷移系達の二重圏 |
| アリーナ | バンドル |
| レンズ | 状態遷移系 |
| チャート | バンドル射 |
| expose射 | 状態露出関数 |
| update射 | 状態更新関数 |
| 状態空間 | 内部状態空間 |
| 出力 | 外部状態空間 |
| ？ | 内部移動空間 |
| 入力 | 外部制御空間 |
マイヤース本の流儀では、インデックス付き圏からグロタンディーク二重構成〈the Grothendieck double construction〉を使ってアリーナ達の二重圏を作ります。ここでの具体例では、集合圏のインデックス付きスライス圏 $`\mbf{Set}/\hyp`$ が、“もとになるインデックス付き圏”です。
グロタンディーク二重構成は、1つのインデックス付き圏 $`\msc{A}`$ に対する2つのグロタンディーク構成の組み合わせです。
- 通常のグロタンディーク構成 $`\int \msc{A}(\hyp)`$
- ファイバー反転のグロタンディーク構成 $`\int \msc{A}(\hyp)^\op`$
通常のグロタンディーク構成の代わりにアロー圏構成も使えます。$`\mbf{Set}/\hyp`$ のグロタンディーク構成 $`\int (\mbf{Set}/\hyp)`$ とアロー圏構成 $`\mrm{Arr}(\mbf{Set})`$ は同じことです。$`\mrm{Arr}(\mbf{Set})`$ は、集合のバンドル達の圏 $`\mbf{Bun}`$ です。この記事では、$`\mbf{Bun}`$ を直接的に定義します（アロー圏構成さえ使わない）。
ファイバー反転のグロタンディーク構成は、スピヴァック〈David I. Spivak〉が一般化レンズ構成〈generalized lens construction〉として導入したものです（以下の論文）。
- [Spi19-22]
- Title: Generalized Lens Categories via functors $`\cat{C}^\op\to \mbf{CAT}`$
- Author: David I. Spivak
- Submitted: 6 Aug 2019 (v1), 17 Mar 2022 (v4)
- Pages: 10p
- URL: https://arxiv.org/abs/1908.02202
ファイバー反転のグロタンディーク構成で作られた一般化レンズは、今はグロタンディーク・レンズとかスピヴァック・レンズと呼ばれます。ここでのグロタンディーク・レンズの導入は、反転グロタンディーク構成を経由せずに、単なる図式として定義します。
インデックス付き圏 $`\mbf{Set}/\hyp`$ から作られたグロタンディーク・レンズは状態遷移系と解釈できます。状態遷移系は、ブラックボックス内にある内部バンドルと、インターフェイスを提供する外部バンドルを持ちます。バンドル射のペア（内部側と外部側）が状態遷移系の準同型射を与えます。この具体例は、マイヤースのアリーナの二重圏に対する直感的な理解を促します。
古典的状態遷移系
古典的状態遷移系〈classical state transition system〉は次の構成素からなります。
- 内部状態空間〈internal state space〉 $`S \In \mbf{Set}`$
- 外部状態空間〈external state space〉 $`A\In \mbf{Set}`$
- 状態露出関数〈state expose function〉 $`\mrm{expose} : S \to A\In \mbf{Set}`$
- ラベル達の集合〈set of labels〉 $`B\In \mbf{Set}`$
- 状態遷移関数〈state transition function〉 $`\mrm{trans}: S\times B \to S\In \mbf{Set}`$
集合 $`S`$ の要素を、内部状態〈internal state〉、隠蔽状態〈hidden state〉、不可視状態〈invisible state〉、あるいは単に状態〈state〉と呼びます。集合 $`A`$ の要素を、外部状態〈external state〉、可視状態〈visible state〉、観測可能状態〈observable state〉などと呼びます。状態露出関数は、内部状態の情報の一部を外部状態に露出させます。
外部状態空間が単元集合で、状態露出関数が $`!_S: S \to \mbf{1}`$ のとき、内部状態を知るすべはありません。一方、外部状態空間が $`S`$ で、状態露出関数が $`\id_S: S \to S`$ なら、内部状態は完全に可視（内部がダダ漏れ）です。外部状態空間が二値真偽値集合 $`\mbf{B}`$ のとき、状態露出関数 $`\mrm{fin}: S \to \mbf{B}`$ は、状態が終状態〈{final | terminal} state〉かどうかを調べる述語と解釈できます。
集合 $`B`$ の要素を、ラベル〈label〉、アクションラベル〈action label〉、アクション〈action〉、コマンド〈command〉、刺激〈stimulus〉などと呼びます。形式言語理論の文脈なら、記号〈symbol〉とか語〈word〉と呼ばれるでしょう。
状態遷移関数 $`\mrm{trans}`$ は、現在の状態とアクションを受け取って、次の状態を返します。状態遷移系の“実行”を担うのが状態遷移関数です。
古典的状態遷移系は、マイヤースが採用している抽象的構造であるグロタンディーク・レンズでまーまーうまく定式化できます。しかし、状態遷移系に関する直感と抽象的構造が100%一致するわけではありません。僕は、なんか違和感／ズレを感じます。後で、違和感／ズレの正体についても述べます。
バンドルとバンドル射
写像〈関数〉を“（集合の）バンドル”〈bundle〉とも呼びます。単に気分の問題に過ぎませんが、「バンドル」と呼んだほうがシックリ来ることがあります。用語の対応は以下のとおり。
| 写像 | バンドル |
|---|---|
| 写像の域 | バンドルのトータル空間〈全空間 | total space〉 |
| 写像の余域 | バンドルのベース空間〈底空間 | base space〉 |
| 写像そのもの | バンドルの射影（ここでは使わない） |
バンドルと呼ぶからと言って「全射である」のような仮定は付けません。単なる写像〈関数〉です。
バンドルをギリシャ文字小文字 $`\alpha, \beta`$ などで書くことにします。次の記法の約束をします。
$`\quad \o{\alpha} := \mrm{dom}(\alpha)\\
\quad \base{\alpha} := \mrm{cod}(\alpha)
`$
したがって、バンドル $`\alpha`$ は次のように書けます。
$`\quad \alpha : \o{\alpha} \to \base{\alpha}\In \mbf{Set}`$
もし、バンドルの余域〈ベース空間 | 底空間〉が $`A`$ であれば、次のようです。
$`\quad \alpha : \o{\alpha} \to A\In \mbf{Set}`$
$`\alpha,\beta`$ がバンドルのとき、バンドル射 $`F`$ は、以下の2つの写像 $`\o{F}, \base{F}`$ のペアで与えられます。
$`\quad \xymatrix{
\o{\alpha} \ar[d]_\alpha \ar[r]^{\o{F}}
\ar@{}[dr]|{\text{comm.}}
&{\o{\beta}} \ar[d]^\beta
\\
\base{\alpha} \ar[r]_{\base{F}}
&\base{\beta}
}\\
\quad \In \mbf{Set}
`$
四角形内の $`\text{comm.}`$ は可換性〈commutativity〉を示します。
集合のバンドルを対象として、バンドル射を射とする圏が形成されます。この圏を $`\mbf{Bun}`$ とします。バンドル射は次の形で書きます。
$`\quad F = \BunM{\o{F}}{\base{F}} : \Bun{\o{\alpha}}{\base{\alpha}}
\to \Bun{\o{\beta}}{\base{\beta}}
\In \mbf{Bun}
`$
$`\o{F}`$ を $`F`$ のトータルパート〈total part〉、$`\base{F}`$ を $`F`$ のベースパート〈base part〉と呼びます。
バンドル射のベース・ファイバー表示
前節のバンドル射のパート分け〈成分表示〉はベースとトータルでした。別なパート分けを考えます。ちょっと天下りなのですが、2つのバンドル $`\alpha, \beta`$ に対して次の形の図式を考えます。
$`\quad \xymatrix{
\o{\alpha} \ar[d]_\alpha \ar[r]^{g}
\ar@{}[dr]|{\text{comm.}}
&\cdot \ar[d] \ar[r]^{f^\uparrow}
\ar@{}[dr]|{\text{p.b.}}
&\o{\beta} \ar[d]^\beta
\\
\base{\alpha} \ar@{=}[r]
&\base{\alpha} \ar[r]_{f}
&\base{\beta}
}\\
\quad \In \mbf{Set}
`$
右側の四角形内部に $`\text{p.b.}`$ と書き込まれていますが、これはプルバック四角形〈デカルト四角形〉のことです。$`f`$ と $`\beta`$ に対して、プルバック四角形はup-to-isoで一意的に決まります。ここでは、“標準的な”プルバック四角形をほんとに一意に選ぶルール（分裂〈splitting〉と呼ぶ、「ファイブレーションの亀裂と分裂」参照）が存在するとします。以下、プルバック四角形は常に標準的なプルバック四角形が選ばれるとします。
以上のような状況で、$`f^\uparrow`$ は $`f`$ と $`\beta`$ から一意に決まります。それに対して、$`g`$ は勝手に選んだ写像です。$`f`$ と $`g`$ のペアは、バンドル射 $`F`$ を次のように決めます。
$`\quad \o{F} := g;f^\uparrow \;: \o{\alpha} \to \o{\beta} \In \mbf{Set}\\
\quad \base{F} := f \;: \base{\alpha} \to \base{\beta} \In \mbf{Set}
`$
このことから、$`f`$ と $`g`$ のペアをバンドル射の表示とみなして、次のように書きます。
$`\quad F = \BunF{F_\flat}{\base{F}} = \BunF{g}{f} : \Bun{\o{\alpha}}{\base{\alpha}}
\to \Bun{\o{\beta}}{\base{\beta}}
\In \mbf{Bun}
`$
$`F_\flat`$ を $`F`$ のファイバーパート〈fiber part〉と呼びます。実際、インデックス付きスライス圏 $`\mbf{Set}/\hyp`$ のグロタンディーク構成のファイバーパートになっているのですが、そこは各自で確認してください（ここには書きません）。
前節のベース・トータル表示と、今定義したベース・ファイバー表示〈base-fiber presentation〉は、角括弧と丸括弧の違いしかないので注意してください。
さて、バンドル射 $`F`$ が与えられたとき、そのベース・ファイバー表示は一意的に決まるでしょうか？ 大丈夫です。下の図を考えましょう。
$`\quad \xymatrix{
{\o{\alpha}} \ar@/^/[drr]^{\o{F}}
\ar@{.>}[dr]^{?}
\ar@/_/[ddr]_{ {\alpha} }
&{}
&{}
\\
{}
&{\cdot} \ar[d] \ar[r]
\ar@{}[dr]|{\text{p.b.} }
&{\o{\beta}} \ar[d]^\beta
\\
{}
&{\base{\alpha}} \ar[r]_{\base{F}}
&{\base{\beta}}
}\\
\quad \text{commutative }\In \mbf{Set}
`$
プルバック四角形の性質から、点線・疑問符の射は一意的に決まります。それを $`F_\flat`$ と置けばいいのです。
バンドル射 $`F`$ のベースパート、トータルパート、ファイバーバートをひとつの図式内に描けば次のようになります。
$`\quad \xymatrix{
\o{\alpha} \ar[d]_\alpha \ar[r]_{F_\flat}
\ar@/^1.2pc/[rr]^{\o{F}}
\ar@{}@/^/[rr]|{\text{comm.}}
\ar@{}[dr]|{\text{comm.}}
&\cdot \ar[d] \ar[r]
\ar@{}[dr]|{\text{p.b.}}
&\o{\beta} \ar[d]^\beta
\\
\base{\alpha} \ar@{=}[r]
&\base{\alpha} \ar[r]_{\base{F}}
&\base{\beta}
}\\
\quad \In \mbf{Set}
`$
バンドルのあいだのレンズ射
2つのバンドル $`\alpha, \beta`$ に対して、そのあいだの“ある種の射”を考えます。それはバンドル射とは異なります。異なりますが似ています。“ある種の射” $`\varphi`$ は次の図式で与えられます。
$`\quad \xymatrix{
\o{\alpha} \ar[d]_\alpha
\ar@{}[dr]|{\text{comm.}}
&\cdot \ar[d] \ar[r] \ar[l]_{\varphi^\sharp}
\ar@{}[dr]|{\text{p.b.}}
&\o{\beta} \ar[d]^\beta
\\
\base{\alpha} \ar@{=}[r]
&\base{\alpha} \ar[r]_{\base{\varphi}}
&\base{\beta}
}\\
\quad \In \mbf{Set}
`$
右側の四角形はプルバック四角形なので（しかも分裂も固定されているので）ラベルがない頂点〈対象〉と辺〈射〉は自動的に一意的に決まります。したがって、$`\base{\varphi}`$ と $`\varphi^\sharp`$ だけで図式全体が決まります。
この形の“射”を、バンドル $`\alpha`$ から $`\beta`$ へのレンズ射〈lens morphism〉と呼びます。$`\base{\varphi}`$ をレンズ射 $`\varphi`$ のベースパート〈base part | 底パート〉、$`\varphi^\sharp`$ を逆行ファイバーバート〈backward fiber part〉と呼びます。
レンズ射は、インデックス付きスライス圏 $`\mbf{Set}/\hyp`$ のファイバー反転グロタンディーク構成により作られたグロタンディーク・レンズになっているのですが、そこは各自で確認してください（ここには書きません）。ここでの「レンズ射」と「グロタンディーク・レンズ」は同義語です。
レンズ射の結合〈合成〉や恒等レンズ射は、バンドル射のときのように自明ではありません。が、それがうまく定義できたとして（後述）、形成される圏を $`\mbf{Lens}`$ とします。圏 $`\mbf{Lens}`$ の対象はバンドルです。つまり、次が成立します。
$`\quad |\mbf{Lens}| = |\mbf{Bun}| \In \mbf{SET}`$
これは二重圏を構成するうえで絶対必須事項です。例えば、タイト方向に関数、プロ方向に関係として二重圏を作れるのは次が成立しているからです。
$`\quad |\mbf{Set}| = |\mbf{Rel}| \In \mbf{SET}`$
バンドル $`\alpha, \beta`$ のあいだのレンズ射 $`\varphi`$ は次のように書きます。
$`\quad \varphi = \LensM{\varphi^\sharp}{\base{\varphi}} : \Bun{\o{\alpha}}{\base{\alpha}}
\to \Bun{\o{\beta}}{\base{\beta}}
\In \mbf{Lens}
`$
左向き矢印は、上段の $`\varphi^\sharp`$ が逆行していることを暗示しています。
さて、バンドルのあいだのレンズ射の結合〈composition〉ですが、これは、ファイバー反転グロタンディーク構成〈スピヴァック／グロタンディーク構成〉における射の結合をなぞる形で定義します。直接的に定義すると、トリッキーな印象をまぬがれません。しかし、レンズ射を状態遷移系として解釈すると、比較的自然なセマンティクスを持ちます。
レンズ射の結合の定義は次節で。
レンズ射の結合
結合の定義をしてないので、まだ「圏 $`\mbf{Lens}`$」とは呼べないのですが、先走って圏の用語・記法を使ってしまいます。バンドルのあいだのレンズ射 $`\varphi: \alpha \to \beta \In \mbf{Lens}`$ があると、その図式の右側の四角形はプルバック四角形でした。
$`\quad \xymatrix{
\cdot \ar[d] \ar[r]
\ar@{}[dr]|{\text{p.b.}}
&{\o{\beta}} \ar[d]^\beta
\\
{\base{\alpha} } \ar[r]_{\base{\varphi}}
&{\base{\beta}}
}\\
\quad \In \mbf{Set}
`$
記号を簡潔にするために、ベースパートを $`f:A\to B`$ と置いたうえで、無名だった頂点・辺に次のようにラベルします。
$`\quad \xymatrix{
{f^*\o{\beta}} \ar[d]_{f^*\beta} \ar[r]^{f^\uparrow}
\ar@{}[dr]|{\text{p.b.}}
&{\o{\beta}} \ar[d]^\beta
\\
{A } \ar[r]_{f}
&{B }
}\\
\quad \In \mbf{Set}
`$
左の辺 $`f^*\beta : f^*\o{\beta} \to A`$ を、バンドル $`\beta`$ の写像 $`f`$ によるファイバー引き戻し〈fiber pullback〉といいます。集合 $`f^*\o{\beta}`$ も、トータル空間 $`\o{\beta}`$ の写像 $`f`$ によるファイバー引き戻し〈fiber pullback〉といいます。集合のファイバー引き戻しは、$`f`$ と $`\beta`$ のファイバー積〈fibered product〉と同じです。ファイバー積の書き方は色々ありますが、例えば次のように書けます。
$`\quad f^*\o{\beta} = (A, f) \times_B (\o{\beta}, \beta)`$
$`f^*`$ は、実際に $`f`$ から決まる関手です。今は踏み込みませんが、$`f^*`$ は、インデックス付きスライス圏 $`\mbf{Set}/\hyp`$ の再インデキシング関手〈reindexing functor〉です。
$`\quad f^* : (\mbf{Set}/B) \to (\mbf{Set}/A) \In \mbf{CAT}`$
$`f^\uparrow`$ は、$`f`$ だけから決まるわけではなくて、$`f`$ と $`\beta`$ から決まります。その意味で $`f^{\uparrow \beta}`$ と書いたほうが正確です。$`f^\uparrow`$ は、図式のレイアウト上も“持ち上げ”に見えるし、デカルト持ち上げ〈Cartesian {lift | lifting}〉と関係しますが、デカルト持ち上げそのものではありません（プルバック四角形全体が $`f`$ のデカルト持ち上げ）。
さて、次のような2つのレンズ射を考えます。
$`\quad \varphi : \alpha \to \beta \In \mbf{Lens} \text{ where }\base{\varphi} = (f: A \to B)\\
\quad \psi : \beta \to \gamma \In \mbf{Lens} \text{ where }\base{\psi} = (g: B \to C)
`$
$`\varphi`$ の一部である $`f^\uparrow`$ と、$`\psi`$ の一部である $`\psi^\sharp`$ を取り出して、次のようなプルバック四角形を考えます。
$`\quad\xymatrix{
{f^{\uparrow *}(g^*\o{\gamma}) } \ar[r] \ar[d]_{f^{\uparrow *}(\psi^\sharp) }
\ar@{}[dr]|{\text{p.b.}}
&{g^*\o{\gamma}} \ar[d]^{\psi^\sharp}
\\
{f^* \o{\beta}} \ar[r]_{f^\uparrow}
&\o{\beta}
}\\
\quad \In \mbf{Set}
`$
このプルバック四角形により、$`\psi`$ の逆行ファイバーパート $`\psi^\sharp`$ を $`f^\uparrow`$ に沿って（むしろ抗して）引き戻すことができます。引き戻した $`f^{\uparrow *}(\psi^\sharp)`$ は、$`\varphi`$ の逆行ファイバーパート $`\varphi^\sharp`$ と普通に結合できます。
$`\quad\xymatrix{
{f^{\uparrow *}(g^*\o{\gamma}) } \ar[d]_{f^{\uparrow *}(\psi^\sharp) }
\ar@/^1.3pc/[dd]^{f^{\uparrow *}(\psi^\sharp)\, ; \, \varphi^\sharp}
\\
{f^* \o{\beta}} \ar[d]_{\varphi^\sharp}
\\
\o{\alpha}
}\\
\quad \In \mbf{Set}
`$
以上で、2つのレンズ射の結合 $`\varphi ; \psi`$ の逆行ファイバーパートが作れます。$`\varphi ; \psi`$ のベースパートとうまくまとまりが付くには次の等式がキモになります。
$`\quad f^{\uparrow *}(g^*\o{\gamma}) = (f;g)^* (\o\gamma)`$
これは、標準プルバック四角形が分裂により選ばれていることの帰結です。上記等式を仮定すれば（分裂を仮定すれば）、逆行ファイバーパートとベースパートは以下の図式にまとめ上げることができます。
$`\quad \xymatrix@C+1.5pc{
{\o{\alpha}} \ar[d]_{\alpha}
\ar@{}[dr]|{\text{comm.}}
&{(f;g)^* (\o\gamma)} \ar[l]_-{f^{\uparrow *}(\psi^\sharp)\, ; \, \varphi^\sharp}
\ar[d] \ar[r]^-{(f;g)^\uparrow}
\ar@{}[dr]|{\text{p.b.}}
&{\o{\gamma}} \ar[d]^{\gamma}
\\
{A} \ar@{=}[r]
&{A} \ar[r]_{f;g}
&{C}
}\\
\quad \In \mbf{Set}
`$
ここまでに説明した、レンズ射の結合は、プルバック四角形をいじくり回す手法で、なんかトリッキーでゴチャゴチャした感じがしますが、状態遷移系の具体例では、直感的な意味を持ちます。
恒等レンズ射は、自明に定義できます。レンズ射の結合と恒等レンズ射のあいだに、結合律、右単位律、左単位律が要求されます。プルバック四角形をいじくり回しても証明できますが、大道具であるスピヴァック／グロタンディーク構成のマシナリーを稼働させたほうが楽ちんです*1。圏の結合律、右単位律、左単位律については割愛します。
レンズ射は状態遷移系である
レンズ射は状態遷移系のひとつの定式化となります。とりあえず、「レンズ射」と「状態遷移系」は同義語だと思ってかまいません。ただし、ここでの状態遷移系は古典的状態遷移系に限りません。
レンズ射 $`\varphi:\alpha \to \beta \In \mbf{Lens}`$ があるとき、$`\varphi`$ を状態遷移系と同一視しますが、域であるバンドル $`\alpha`$ を内部バンドル〈internal bundle〉、余域であるバンドル $`\beta`$ を外部バンドル〈external bundle〉と呼びます。
状態遷移系＝レンズ射 をもう少し詳しく書きましょう。$`\base{\varphi} = f`$ と置いています。
$`\quad \xymatrix@C+1.3pc{
\o{\alpha} \ar[d]_\alpha
\ar@{}[dr]|{\text{comm.}}
&{f^*\o{\beta}} \ar[l]_{\varphi^\sharp} \ar[r]^{f^\uparrow} \ar[d]|{f^*\beta}
\ar@{}[dr]|{\text{p.b.}}
&{\o{\beta}} \ar[d]^\beta
\\
{A} \ar@{=}[r]
&{A} \ar[r]_f
&{B}
}\\
\quad \In \mbf{Set}
`$
上記図式の各部を、状態遷移系の言葉では次のように呼びます。
- 集合 $`A`$ を、内部状態空間〈internal state space〉と呼ぶ。
- 集合 $`B`$ を、外部状態空間〈external state space〉と呼ぶ。
- 関数 $`f`$ を、状態露出関数〈state expose function〉と呼ぶ。
- 集合 $`\o{\alpha}`$ を、内部移動空間〈internal move space〉と呼ぶ。
- バンドル $`\alpha`$ を、内部バンドル〈internal bundle〉と呼ぶ。
- 集合 $`\o{\beta}`$ を、外部制御空間〈external control space〉と呼ぶ。
- バンドル $`\beta`$ を、外部バンドル〈external bundle〉と呼ぶ。
- 集合 $`f^*\o{\beta}`$ を、中間制御空間〈middle control space〉と呼ぶ。
- バンドル $`f^*\beta`$ を、中間バンドル〈middle bundle〉と呼ぶ。
- 関数 $`\varphi^\sharp`$ を、状態更新関数〈state update function〉と呼ぶ
- 外部バンドル $`\beta`$ を、インターフェイス・バンドル〈interface bundle〉とも呼ぶ。
状態更新関数は、状態遷移関数とは微妙に異なります。この微妙な差が先に述べた違和感／ズレの1つ目の原因です。「制御空間」と「移動空間」という言葉を使いましたが、理論上は「制御」と「移動」を区別する必要はありません。が、直感としては区別するのが自然です。これが、違和感／ズレの2つ目の原因です。違和感／ズレについては、また適宜触れます。
一例として、ランプやインジケータが表示されていて、メニューからコマンド〈アクション〉を選んで操作する対話的ソフトウェアを想定しましょう。
外部状態空間 $`B`$ は、ランプやインジケータの状態です -- これはユーザーから可視〈ビジブル〉です。インターフェイス・バンドルの外部制御空間は次のように書けます。
$`\quad \o{\beta}\cong \sum_{b\in B}\beta^{-1}(b)`$
これは、外部状態〈可視状態〉$`b\in B`$ ごとにコマンドセット $`\beta^{-1}(b)`$ があることで、外部状態が変わればそれに応じて使える〈イネーブルな〉コマンド達も変化します。外部状態は、内部状態〈隠蔽状態〉が状態露出関数で露出されたものなので、間接的には内部状態に応じて使えるコマンド達が変わります。
中間バンドルの中間制御空間は次のように書けます。
$`\quad f^*\o{\beta} \cong \sum_{a\in A}\beta^{-1}( f(a) )`$
内部状態〈隠蔽状態〉$`a\in A`$ ごとに、外部に露出している（ユーザーが利用可能な）コマンドセット $`\beta^{-1}( f(a) )`$ が生えているバンドル（集合のたば）になっています。中間バンドルは、ベース空間が内部状態空間で、各ファイバーは外部インターフェイスを反映しているので、文字通り内部（隠蔽部分）と外部（公開インターフェイス部分）の中間に位置します。
内部バンドルとその内部移動空間は、マイヤースの定式化に違和感／ズレを感じるところです。内部移動空間は、状態遷移の情報（遷移の前と遷移の後）を保持できます。（一般に、「移動」と「遷移」は同義語ですが、別概念とするほうがいいかも知れません（後の節参照）。状態遷移の結果である「遷移〈移動〉した後の内部状態」を取り出す関数がレンズ射には備わっていません。グロタンディーク二重構成は「何か足りてない」ように思えます*2。
多くの場合、内部移動空間は $`A\times A`$ として、内部バンドルを $`\pi_1^{A, A}\to A`$ としてうまくいきます。とりあえずは、この場合を想定して考えます。
内部移動空間は次のように書けます。
$`\quad \o{\alpha} \cong \sum_{a\in A}\alpha^{-1}( a )`$
内部状態 $`a\in A`$ に対するファイバー $`\alpha^{-1}( a )`$ は、$`a`$ から移動〈遷移〉可能な行き先達の空間です。内部移動空間が $`A\times A`$ なら、ペア $`(a, a')`$ の $`a'`$ が移動先〈遷移先〉になります。
状態更新関数 $`\varphi^\sharp`$ をファイバーごとに見ると、次のような関数です。
$`\text{For }a\in A\\
\quad \varphi^\sharp_a : \beta^{-1}(f(a)) \to \alpha^{-1}(a)
`$
これは、内部状態 $`a\in A`$ で利用可能なコマンドを受け取って、$`a`$ の移動先を返す関数です。確かに、外部からの制御により内部状態を変更する関数です。
第ニ節で述べた古典的状態遷移系では、以下のようになります。使っている文字 $`S, A, B`$ は第ニ節の意味です。$`e`$ はexpose関数〈状態露出関数〉、$`u`$ はupdate関数〈状態更新関数〉です（図のすぐ後に説明あり）。
$`\quad \xymatrix@C+1.3pc{
{S\times S} \ar[d]_{\pi_1^{S, S}}
\ar@{}[dr]|{\text{comm.}}
&{S \times B } \ar[l]_{\mrm{u} } \ar[r]^{e\times \id_B} \ar[d]|{\pi_1^{S, B}}
\ar@{}[dr]|{\text{p.b.}}
&{A\times B} \ar[d]^{\pi_1^{A, B}}
\\
{S} \ar@{=}[r]
&{S} \ar[r]_e
&{A}
}\\
\quad \In \mbf{Set}
`$
図中の関数 $`u`$ は、状態遷移関数を $`t`$ として次のように定義されます。
$`\text{For }s\in S, b\in B\\
\quad u(s, b) := (s, t(s, b))\; \in S\times S
`$
レンズ射のファイバーパートである状態更新関数は、古典的な意味での状態遷移関数そのものではありません。状態更新関数は、状態遷移関数を包みこんだ関数です。これは、先述した1つ目の違和感／ズレです。
古典的ケースでは、3つのバンドルがすべて、直積と第一射影で構成される自明バンドルです。一般的には、自明バンドルとは限らないバンドルになります。
単純レンズ射
前節の例は3つのバンドルがすべて自明バンドルでした。外部バンドル（レンズ射の余域）が自明バンドルなら中間バンドルも自明になるので、域と余域が自明バンドルなら3つのバンドルがすべて自明バンドルになります。このようなレンズ射を単純レンズ射〈simple lens morphism〉と呼ぶことにします。
単純レンズ射は、表示や計算が楽です。古典的状態遷移系は、単純レンズ射で表現可能です。この節では、単純レンズ射だけを扱うので、今までの記法を完全にリセットして、新しい記法を定義します。
集合をラテン文字大文字、関数〈写像〉はラテン文字小文字で書きます。単純レンズ射は2つの関数のペアですが、記号の乱用により次のように書きます。
$`\quad f = \LensM{f^\sharp}{f}`$
レンズ射とそのベースパートを同じ名前でオーバーロードします。$`f`$ がどちらの意味かは毎回判断が必要です。
ひとつの単純レンズ射に関わる集合は4つ（例えば、$`A, B, P, Q`$）です。次のように書けます。$`\mbf{SimpLens}`$ は単純レンズ射達の圏（対象はバンドル）です。
$`\quad f = \LensM{f^\sharp}{f}: \Bun{A\times P}{A} \to \Bun{B\times Q}{B}
\In \mbf{SimpLens}
`$
単純レンズ射の域と余域のバンドルは、必ず直積の第一射影（自明なバンドル）です。
単純レンズ射の図式は、次のレイアウトで描くことにします。
$`\quad \xymatrix{
{A\times P} \ar[d]
&{A\times Q} \ar[dl] \ar[l]_{f^\sharp} \ar[r]^{f\times \id_Q}
\ar@{}[dr]|{\text{p.b.} }
&{B\times Q} \ar[d]
\\
A \ar[rr]_f
&{}
&B
}\\
\quad \In \mbf{Set}
`$
- ラベルがない矢印は直積の第一射影と暗黙に仮定
- ラベルがない左の三角形は可換だと暗黙に仮定
単純レンズ射の場合、そのファイバーパート〈状態更新関数〉をデカルトペアに分解できます。
$`\quad f^\sharp = \langle (f^\sharp)_1, (f^\sharp)_2 \rangle :
A\times Q \to A\times P \In \mbf{Set}\\
\text{where }\\
\quad (f^\sharp)_1 : A\times Q \to A \In \mbf{Set}\\
\quad (f^\sharp)_2 : A\times Q \to P \In \mbf{Set}
`$
図式の三角形の可換性から、第一成分 $`(f^\sharp)_1`$ は $`\pi_1^{A, Q}`$ となります。第ニ成分 $`(f^\sharp)_2`$ が古典的状態遷移系の状態遷移関数です。単純レンズ射 $`f`$ の状態遷移関数 $`(f^\sharp)_2`$ は $`f^\tr`$ と書くことにします。右肩の $`\tr`$ は transition からで transpose ではありません。
単純レンズ射 $`f`$ を、状態更新関数 $`f^\sharp`$ ではなくて状態遷移関数 $`f^\tr`$ により表示するときは、状態遷移関数をブラケットで囲むことにします。
$`\quad f = \LensM{f^\sharp}{f} = \LensM{[f^\tr]}{f}: \Bun{A\times P}{A} \to \Bun{B\times Q}{B} \In \mbf{SimpLens}\\
\text{where}\\
\quad f^\tr : A\times Q \to P \In \mbf{Set}
`$
さて、もう一つの単純レンズ射 $`g`$ があったとします。
$`\quad g = \LensM{g^\sharp}{g} = \LensM{[g^\tr]}{g}: \Bun{B\times Q}{B} \to \Bun{C\times R}{C} \In \mbf{SimpLens}
`$
$`f`$ と $`g`$ の結合の状態更新関数を計算するには、次のプルバック四角形を使います。
$`\quad \xymatrix{
\cdot \ar[r] \ar[d]_{(f\times \id_B)^* g^\sharp}
\ar@{}[dr]|{\text{p.b.}}
& {B\times R} \ar[d]^{g^\sharp}
\\
{A\times Q} \ar[r]_{f\times \id_Q}
&{B\times Q}
}\\
\quad \In\mbf{Set}
`$
具体的な計算をゴニョゴニョ・ガチャガチャとやると、次のプルバック四角形に帰着することが分かります。
$`\quad \xymatrix{
{A\times B\times R} \ar[r]^-{\pi_{2,3}^{A, B, R}} \ar[d]_{\widehat{g}}
\ar@{}[dr]|{\text{p.b.}}
& {B\times R} \ar[d]^{g^\sharp}
\\
{A\times Q} \ar[r]_{f\times \id_Q}
&{B\times Q}
}\\
\text{where}\\
\quad \widehat{g} =
\lambda\,(a, b, r)\in A\times B\times R.\, (a, g^\tr(b, r) ) \\
\quad \In\mbf{Set}
`$
これを使って、状態遷移関数の結合公式が出ます。
$`\quad (f;g)^\tr = \lambda\, (a, b, r).f^\tr(a, g^\tr(b, r) )
`$
$`\quad \LensM{[f^\tr]}{f} ;\LensM{[g^\tr]}{g} =
\LensM{[(f;g)^\tr]}{f;g }
`$
この結合公式を使えば、単純レンズ射（＝古典的状態遷移系）のレンズ結合を具体的に計算できます。
バックエンドとラッパー
この節では、何度か触れた違和感／ズレの話をします。古典的状態遷移系は単純レンズ射で定式化されるので、古典的状態遷移系と単純レンズ射は原則的に同一視できます。が、同一視し切れない部分が残ります。
古典的状態遷移系 $`f`$ と $`g`$ をレンズ結合〈lens composition〉（レンズ射として結合）することは、新しい古典的状態遷移系 $`f; g`$ を作り出すことです。新しい古典的状態遷移系 $`f;g`$ において、$`f`$ はバックエンド・コンポネント（ユーザーから見えない部分）となり、$`g`$ はフロントエンド・コンポネントになります。
$`f;g;h;`$ のような繋ぎ方をすると、$`g`$ は中継ぎのコンポネントになります。$`f`$ のインターフェイスを $`h`$ に理解可能な形に変換しているので、インターフェイスの「変換子 or フィルター or ラッパー」などと呼べます。ここでは「ラッパー〈wrapper〉」としましょう。
現実では、バックエンド〈backend〉とラッパーは区別できます。しかし、単純レンズ射（一般のレンズ射でも）、そういう区別はありません。もし、バックエンドとラッパーという役割りを区別したいなら：
- 内部バンドルが $`A\times A \to A`$ の形の単純レンズ射 $`f`$ だけがバックエンドの役割りを担える。
- バックエンド $`f`$ に対して、ポスト結合可能な単純レンズ射は $`f`$ のラッパーとなり得る。
バックエンドの内部移動空間は、$`A\times A`$ の形で、その要素 $`(a, a')`$ は実際に「$`a`$ から $`a'`$ への移動」を表します。
一方、ラッパーの内部バンドルはバックエンドの外部バンドルに一致するので、$`B\times Q\to B`$ のような形をしています。これは、バックエンド $`f`$ が露出している外部状態とコマンドのペアです。したがって、ラッパー $`g`$ の内部バンドルは移動ではなくて制御を表しています。ここでの「移動」と「制御」の使い分けは：
- 移動は、遷移前の状態 $`a`$ と遷移後の状態 $`a'`$ のペア $`(a, a')`$
- 制御は、遷移前の状態 $`b`$ とコマンド $`q`$ のペア $`(b, q)`$
移動も制御もペアですが、遷移後の状態の取り出し方が違います。
- 移動 $`(a, a')`$ から遷移後の状態を取り出すには、第ニ成分 $`a'`$ を取る。
- 制御 $`(b, q)`$ から遷移後の状態を取り出すには、状態遷移関数を適用して $`\mrm{trans}(b, q)`$ とする。
つまり、バックエンドとラッパーでは内部メカニズムにも違いがあります。一律に、「古典的状態遷移系＝単純レンズ射」と定式化してしまうと、この違いが反映されないのです。これが（少なくとも僕にとっては）違和感／ズレを感じさせます。
バックエンドとラッパーを（心のなかで）区別するなら、単純レンズ射のレンズ結合は、バックエンドにラッパーを結合してインターフェイス変換をすること、あるいはラッパーとラッパーを結合して多段階のインターフェイス変換をすることだと解釈できます。
なお、マイヤースは、二重圏上の二重インデックス付き圏〈doubly indexed category〉という概念も提示しています。二重インデックス付き圏が、違和感／ズレを解消してくれるかも知れません。
状態遷移系のあいだの準同型射
レンズ射は状態遷移系であるとすると、当然に状態遷移系のあいだの準同型射が問題になります。つまり、レンズ射（＝状態遷移系）を対象として、そのあいだの準同型射を射とする圏を考えたいのです。
今までの記法のハイブリッド方式として； $`\alpha, \beta`$ などがバンドル、$`f, g`$ などが状態遷移系（バンドルのあいだのレンズ射）とします。状態遷移系のあいだの準同型射は、ギリシャ文字大文字 $`\Phi,\Psi`$ などで書くことにします。
状態遷移系の図式のレイアウトと記号の乱用と暗黙の約束は、単純レンズ射のときと同様とします。
$`\quad \xymatrix{
{\o{\sigma} } \ar[d]
&{f^* \o{\alpha} } \ar[dl] \ar[l]_{f^\sharp} \ar[r]^{f^\uparrow }
\ar@{}[dr]|{\text{p.b.} }
&{\o{\alpha} } \ar[d]
\\
S \ar[rr]_f
&{}
&A
}\\
\quad \In \mbf{Set}
`$
ラベルのない矢印は、内部バンドル $`\sigma`$ 、中間バンドル $`f^*\alpha`$ 、外部バンドル $`\alpha`$ です。
$`f:\sigma \to \alpha`$ と $`g: \tau \to \beta`$ を状態遷移系〈レンズ射〉とします。状態遷移系の準同型射〈homomorphism of state transition system〉 $`\Phi`$ は、次の形だと想定するのはまー妥当でしょう。
$`\quad \xymatrix{
\sigma \ar[d]_f \ar[r]^U
\ar@{}[dr]|{\Phi\,\twoto}
&\tau \ar[d]^g
\\
\alpha \ar[r]_F
&\beta
}
`$
ここで、$`U,F`$ は、バンドル射です。$`U`$ は内部バンドルのあいだの変換で、$`F`$ は外部バンドル〈インターフェイス・バンドル〉のあいだの変換です。$`\Phi`$ は、4つの射 $`f, g, U, F`$ のあいだの整合性条件〈compatibility condition〉を記述していると言えます。
4つの射を関数に分解すると8つになります。
- $`\base{f} : S \to A \In \mbf{Set}`$
- $`{f^\sharp} : f^*\o{\alpha} \to \o{\sigma} \In \mbf{Set}`$
- $`\base{g} : T \to B \In \mbf{Set}`$
- $`{g^\sharp} : g^*\o{\beta} \to \o{\tau} \In \mbf{Set}`$
- $`\base{U} : S \to T \In \mbf{Set}`$
- $`\o{U} : \o{\sigma}\to \o{\tau} \In \mbf{Set}`$
- $`\base{F} : A \to B \In \mbf{Set}`$
- $`\o{F} : \o{\alpha}\to \o{\beta} \In \mbf{Set}`$
$`U,F`$ をベース・ファイバー表示で書くなら、ファイバーパートとして次の関数も現れます。
- $`U_\flat : \o{\sigma} \to U^*\o{\tau}`$
- $`F_\flat : \o{\alpha} \to F^*\o{\beta}`$
関与する関数が多くなるので、どうしても話がややこしくなります。ある程度複雑な構造を扱うときはこうなるもんなので、まーしょうがないですね。
まだ定義が完了してないですが、状態遷移系達の圏を $`\mbf{STS}`$ とします。上の図式のように、圏 $`\mbf{STS}`$ の射は2次元的なので、次のように書くことにします。
$`\quad \Phi :: f \twoto g \In \mbf{STS}`$
圏 $`\mbf{STS}`$ の背後には二重圏があり、射 $`\Phi`$ は二重圏の二重射をプロ方向〈ルーズ方向〉に見たものです。「構造を持つ概念的事物の記述と参照： コンパニオンを例に // コンパニオン系の記述」で導入した記法で書くなら：
$`\quad \Phi :: \DM{f}{g}{U}{F} : \DO{\sigma}{\tau }{\alpha}{\beta} \In \mbf{STS}
`$
四角形 $`\Phi`$ が表現する整合性条件が問題なのですが、節を改めましょう。
準同型射の整合性条件
状態遷移系 $`f, g`$ のあいだの準同型射 $`\Phi`$ は内部バンドルのあいだのバンドル射 $`U:\sigma \to \tau`$ と、外部バンドルのあいだのバンドル射 $`F:\alpha\to \beta`$ のペアです。が、$`\Phi`$ の本質的部分は構成素のあいだの相互関係／法則性 -- 整合性条件です。
整合性条件をテキストで書き下すのはもはや現実的ではありません。図式を使います。プルバック四角形／可換四角形／可換三角形以外に、持ち上げ四角形〈lift square〉を使います。持ち上げ四角形は、関手の値割り当て〈value assignment〉の記述です。関手 $`F:\cat{C}\to \cat{D}`$ に対して、以下の四角形は $`F(f) = g`$ を意味します。
$`\quad \xymatrix{
A \ar[r]^f \ar@{|->}[d]_F
\ar@{}[dr]|{\text{lift}}
&B \ar@{|->}[d]^F
\\
X \ar[r]_g
&Y
}\\
\quad \In F:\cat{C}\to\cat{D}
`$
老婆心で言うと、上の図式で出現した $`A, B, f, F`$ は、一時的な名前で、話の本筋で出現している名前 $`A, B, f, F`$ とは無関係です。
関手の値割り当てのように、複数の圏にまたがる矢印・多角形も含む図式については以下の過去記事達を参照してください。
状態遷移系〈レンズ射〉において、記号の乱用により、$`f = \base{f}`$ としましたが、バンドル射においても同様な記号の乱用をして、$`F = \base{F}`$ とします。オーバーロード解決の負担が増えますが、記述は簡潔になります。
状態遷移系のあいだの準同型射の整合性を表わす3つの図式を挙げます。まずはベースにおける整合性です。
$`\quad \xymatrix{
S \ar[r]^{U } \ar[d]_{f}
\ar@{}[dr]|{(1)}
&T \ar[d]^{g}
\\
A \ar[r]_{F }
&B
}\\
\quad \text{commutative }\In \mbf{Set}
`$
集合圏における可換図式で、可換四角形に $`(1)`$ と名前を付けます。
今まで、インデックス付きスライス圏 $`\mbf{Set}/\hyp`$ は出来るだけ使わないようにしてきたのですが、もはや避けられないので使います。集合圏内の可換四角形 $`(1)`$ を、集合圏上のインデックス付き圏であるインデックス付きスライス圏 $`\mbf{Set}/\hyp`$ により $`\mbf{CAT}`$ に移すと、次の可換四角形が得られます。
$`\quad \xymatrix{
{\mbf{Set}/S }
\ar@{}[dr]|{(2)}
&{\mbf{Set}/T } \ar[l]_{U^*}
\\
{\mbf{Set}/A } \ar[u]^{f^*}
&{\mbf{Set}/B } \ar[l]^{F^*} \ar[u]_{g^*}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
可換四角形 $`(2)`$ は、次の等式的命題を導きます。
$`\text{For }\beta \in |\mbf{Set}/B|\\
\quad f^*(F^*\beta) = U^*(g^*\beta)
`$
$`\beta`$ の域（バンドルのトータル空間）を取ると、集合のあいだの等式が出ます。
$`\quad f^*(F^*)\o{\beta} = U^*(g^*\o{\beta}) \In \mbf{Set}`$
この等式はすぐ下で使います。
最後に、ファイバーにおける整合性です。可換四角形と持ち上げ四角形（関手の値割り当て）が混じった図式になります。
$`\quad \xymatrix{
{\o{\alpha} } \ar@{|->}[d]_{f^*} \ar[r]^{F_\flat}
\ar@{}[dr]|{\text{lift}}
&{F^*\o{\beta} } \ar@{|->}[d]^{f^*}
&{}
\\
{f^*\o{\alpha} } \ar[r]^{f^* F_\flat} \ar@{=}[d] \ar[r]
\ar@{}[dr]|{(3)}
&{f^*(F^*\o{\beta}) } \ar@{=}[d]^{(2)}
&{}
\\
{f^*\o{\alpha} } \ar[d]_{f^\sharp} \ar[r]^{f^* F_\flat}
\ar@{}[dr]|{(4)}
&{U^*(g^* \o{\beta})} \ar[d]|{U^*(g^\sharp)}
\ar@{}[dr]|{\text{lift}}
&{g^* \o{\beta}} \ar@{|->}[l]_{U^*} \ar[d]^{g^\sharp}
\\
\o{\sigma} \ar[r]_{U_\flat}
&{U^*\o{\tau} }
&{\o{\tau}} \ar@{|->}[l]^{U^*}
}\\
\quad \In f^* : (\mbf{Set}/A)\to (\mbf{Set}/S)\\
\quad \In U^* : (\mbf{Set}/T)\to (\mbf{Set}/S)\\
\quad \text{commutative }\In \mbf{Set}
`$
中心となるのは $`(4)`$ の可換四角形です。可換四角形 $`(4)`$ を構成するための補助に、2つの持ち上げ四角形と可換四角形 $`(3)`$ が必要です。可換四角形 $`(3)`$ では、先の可換四角形 $`(2)`$ から導かれた等式を使っています。
以上が、状態遷移系のあいだの準同型射の整合性です。整合性を記述する図式（それは準同型射の主要部）を出しただけなので、次の課題があります。
- 準同型射の整合性のココロ（状態遷移系におけるセマンティクス）は何なのか？
- 2つの準同型射 $`\Phi, \Psi`$ の結合はどうやるのか？
- 結合の定義が与えられたとして、それは圏の公理を満たすのか？
これらの課題に応えるにはけっこうな手間がかかるので、今回は扱いません。結果を言えば、状態遷移系を対象として準同型射を射とする圏は構成可能です。
二重圏との関係
今までの話の流れとしては、圏 $`\mbf{STS}`$ は、状態遷移系を対象として準同型射を射とする圏です。が、圏 $`\mbf{STS}`$ の定義のなかに二重圏が織り込まれています。
状態遷移系のあいだの準同型射の概要を表わす図式は次でした。
$`\quad \xymatrix{
\sigma \ar[d]_f \ar[r]^U
\ar@{}[dr]|{\Phi\,\twoto}
&\tau \ar[d]^g
\\
\alpha \ar[r]_F
&\beta
}
`$
$`\Phi`$ はそのまま二重圏の二重射とみなせます。念の為、二重圏の構成素を列挙すると：
- 二重圏の対象はバンドル
- 二重圏のタイト射は状態遷移系（バンドルのあいだのレンズ射）
- 二重圏のプロ射はバンドルのあいだのバンドル射
- 二重圏の二重射は状態遷移系のあいだの準同型射
おわりに
この記事は、状態遷移系の準同型射の整合性条件の記述が雑だったり、ほんとに具体的な状態遷移系の個別事例が無かったりしますが、状態遷移系としてのレンズ射〈グロタンディーク・レンズ〉と、それらが形成する圏／二重圏についてザッと眺めました。
マイヤース流の定式化が、どの程度の表現力と妥当性を持つのかはまだよく分かりませんが、二重圏を使う手法が有効なのは間違いないでしょう。型理論や論理との関係も興味あるところです。
