加群とオートマトンとインデックス付き圏の転置

コンピュータのハードウェアやソフトウェアは状態遷移系でモデル化できる場合が多いですよね（例えば、「状態遷移機械と非決定性遷移」）。多くの計算システムは、「状態遷移を引き起こすアクション記号の集合をアルファベットとするオートマトンなのだ」と言ってももいいでしょう。ここで、アルファベットや状態空間が有限であることは仮定しません。

オートマトンは多元環（可換とは限らない代数）上の加群だと思うのがいいんじゃないか、というのが僕の方針です（「メイヤー代数／メイヤー加群の圏」）。とはいえ、多元環や加群のことをよく知っているわけじゃないので、枠組みの設定から先に進んでないのが実情ですけどね。とりあえず、枠組みだけでも説明しておきます。共有メモリにちょっと触れますが、同期と排他、トランザクションなどは次の機会にします。

内容：

アーベル群のなかの加群

Abをアーベル群と準同型からなる圏とします。アーベル群は、整数の可換環Z上の加群なので、Z上のテンソル積を定義できます。このテンソル積をモノイド積として、Abを対称モノイド圏だとみなせます。モノイド単位はZで、対称はテンソル積の順番の入れ替えです。

対称モノイド圏Ab内のモノイドとモノイド準同型からなる圏 Monoid(Ab) を作れます。これは多元環（単にalgebraと呼ぶことが多いです）の圏です。A∈|Monoid(Ab)| を固定すると、多元環A上の加群の圏Module(A)を定義できます。そして、多元環の準同型 f:A→B in Monoid(Ab) があると、加群の圏のあいだの関手 f^*:Module(B)→Module(A) が誘導されます。

多元環と加群達は、全体としてインデックス付き圏を構成し、そのベースの圏は多元環（Ab内のモノイド）の圏です。

集合のなかの加群

足し算は忘れて、圏Abの代わりに圏Setを使いましょう。集合の直積に関してSetを対称モノイド圏と考えます。Setのなかで多元環とか加群に相当するものは次です。

• 多元環は、単なるモノイド
• 加群は、モノイドが作用する集合

モノイドが作用する集合の意味で「加群」という言葉を使い続けます。また、加群の台集合を状態空間とも呼びます。モノイドに作用される集合が状態空間です。

Σをなんらかの集合として、Σ^* := FreeMonoid(Σ) とします。Σ^*はモノイドなので、状態空間Sと作用 S×Σ^*→S があれば、これは加群となります。S×Σ^*→S はオートマトンの定義そのものなので、オートマトンは自由モノイド上の加群ということになります。Autom(Σ) = Module(Σ^*) ですね。

アルファベットΣはモノイドの生成系ですが、具体的な表示が必要なとき以外は特に考える必要もないので、オートマトンとは集合圏のなかの加群だと言ってもいいでしょう。もちろん、生成系の議論は重要ですが、いつでも生成系を引きずっているとかえって鬱陶しいです。

モノイドMに対するModule(M)や、f:M→N に対する f^*:Module(N)→Module(M) も、Ab内の加群のときと同じです。

加群のハードウェア的解釈

モノイドM、状態空間S、作用aからなる加群（＝オートマトン）を (M, S, a) と3つ組で書きましょう。MがアルファベットΣから自由生成されている場合は次のような解釈が可能です。

1. Σは、基本となる機械語命令の集合（インストラクションセット）である。
2. M = Σ^* は機械語命令の列なので、機械語プログラムである。
3. Mの単位元は、空（長さ0）な機械語プログラムである。
4. Mの乗法は、2つの機械語プログラムを時間的に順次実行すること。空間的には、コード領域に機械語プログラムを併置することである。
5. Sは、メモリの状態全体からなる集合。
6. aは、機械語命令（の記号）がメモリ状態をどう変更するかを実際に規定するハードウェアアーキテクチャとなる。

2つの加群 (M, S, a) と (M, T, b) は、同じインストラクションセット（モノイドM）を持ちますが、異なる状態空間（SとT）と異なる挙動（aとb）を持つでしょう。状態空間が同じでも、(M, S, a) と (M, S, b) は異なるかもしれません。コード領域にまったく同じ機械語プログラムを載せ、データ領域も揃えたのに、実行結果（の状態）が違うことがある、ということです。その原因は、機械語命令に対する解釈（意味論）が違うからです。aやb、つまり加群のスカラー乗法が、機械語命令の“状態遷移による意味論”を与えているのです。

圏論的インデックス付け

3つ組 (M, S, a) が加群であることを強調して、Module(M, S, a) と書くことにします。インデックス付き圏のファイバーと紛らわしい記法ですが、わざとそうしています。

モノイドMと状態空間Sは固定して、作用の仕方を色々と変えた全体を、ワイルドカードを使って Module(M, S, *) と書きましょう。Module(M, S, *) は、加群の集合です。圏にすることもできますが、とりあえずは単に集合と思ってもかまいません。

Module(M, S, *)のハードウェア的解釈は、インストラクションセットとデータメモリは固定して、インストラクションの解釈を変化させたもの全体です。CPU機能がプログラマブルなコンピュータキットのようなものです。

Module(M, *, *)は、インストラクションセットは固定だが、データメモリもCPU機能も自由に変えられるコンピュータキットです。データメモリ（の状態）をSに設定して、インストラクションの解釈をaと定義すると、具体的な加群（＝オートマトン）Module(M, S, a)が出来上がります。

Module(M, S) := Module(M, S, *)、Module(M) := Module(M, *, *) としましょう。単なる加群の集合ではなくて、射も一緒に考えて圏にしたものは、Module[M, S]、 Module[M] にします。ブラケットを使うと、インデックス付け（indexing）の感じがでます。

Module[M] がモノイドM上の加群の圏になり、M|→Module[M] がインデックス付き圏になることはわかります。AbでやったことをSet上でも再現できるからです。しかし、Module[M, S] ってのはなんだか分かりません。普通、こんなモノは出てこないと思います（僕が知らないだけかもしれませんが）。コンピュータとプログラミングの文脈なら、Module[M, S] に意味を与えることは割と自然に行えます。

EP圏とPE圏

Cを圏として、A, B∈|C| に対して、e:A→B と p:B→A で次の条件を満たすものをEPペアと呼びます。

• e;p = id_A

EPは embedding-projection の略記です。Cがなんらかの構造（例えば順序）で豊饒化されているときはもっと条件を付けますが、Cが単なる圏だと e;p = id_A という等式だけです。

EPペア(e, p)を A→B という向きの射と考えた圏を EP(C) とします。実際に圏になることは容易に確認できます。EP(C) の反対圏（opposite）を PE(C) としましょう； PE(C) := EP(C)^op 。

(e, p):A→B in EP(C) の意味は、だいたいはAがBの部分集合という感じです。eでAをBに埋め込んで、pでBからAを取り出せるのです。ですから、EP圏EP(C) の射は、ある種の包含関係を表しているとみなせます。もとの圏Cを型と計算処理の圏だとすると、EPペアは型階層（type hierarchy）を与えます。

EPペアでハッキリとした階層構造を作れるのですが、僕の印象では、EPペアは条件がきつすぎて使いにくいような。もう少しゆるい概念の候補がいくつかあります。

1. e:A→B は指定するが、pは指定しない。eは分裂モノ（split mono）ともいう。
2. p:B→A は指定するが、eは指定しない。pは分裂エピ（split epi）ともいう。
3. Cが順序集合の圏であるときは、ガロア対応を使う。
4. 観測概念、つまり余モノイド上の余加群構造を考えて、観測を保存する射を使う。

EP圏（またはPE圏）が扱いは楽なので、ここではEPペアを使うことにします。

状態空間の射に沿った圏の引き戻し

以下、加群のスカラー乗法は右加群の形で書きます。

(N, T, b)がモノイドN上の加群で、f:M→N がモノイド準同型のとき、(M, T, a)を、a:T×M→M, a := (id_T×f);b と定義して、加群の引き戻しが定義できます。この引き戻しは、モノイドの射に沿った（逆方向の）移動です。

(e, p):S→T がEPペアだとします。このとき、加群 (N, S, a) を、a:S×N→S, a := (e×id_N);b;p と定義します。(e, p)がEPペアであれば、スカラー乗法aはちゃんと定義できます。状態空間のあいだの射をEPペアだとすると、状態空間の射に沿った（逆方向）の移動（引き戻し）が定義できたことになります。

集合圏で考えることにして、Monoid := Monoid(Set)、State := EP(Set) と定義します。そして、圏の直積 Monoid×State を作ります。この圏の対象は、モノイドMと状態空間（と呼ぶ集合）Sのペア (M, S) で、射は、モノイド射 f:M→N とEPペア (e, p):S→T のペア (f, (e, p)):(M, S)→(N, T) です。

モノイドNと状態空間Tを固定して、(N, T)上の加群構造の全体を Module[N, T] とします。射を適切に定義すれば、Module[N, T] は圏になります。モノイド射に沿った引き戻しとEPペアに沿った引き戻しは定義できているので、それらを組み合わせれば、(f, (e, p)):(M, S)→(N, T) に沿って、Module[N, T]→Module[M, S] という引き戻し関手を定義できるでしょう。(N, S)|→Module[M, S] は2つのインデックスを持ったインデックス付き圏となります。

二重インデックスとインデックスの転置

フビニ／グロタンディーク同値が適切に定式化できれば、おそらく、Module[M, S] を (Module[M])[S] とみなそうが、(Module[S])[M] とみなそうが、最終的にできる多重グロタンディーク構成は圏同値になるでしょう（ここらへん未確認）。

加群の係数域であるモノイドMを固定したファイバー Module[M] = Module[M, *] はお馴染みといえますが、状態空間（加群の台）のほうを固定したファイバー Module[*, S] は代数ではそれほど注目されない気がします。Module[*, S] のワイルドカード「*」はモノイドの上を走るので、同じ状態空間にたくさんのモノイドを取っ替え引っ替え作用させることになります。複数モノイドの自由積を作って作用させることもできます。共有メモリが、複数のCPUやプロセスからアクセスされる状況とは、まーこんなものでしょ。

S|→Module[*, S] というインデックス付き圏は、共有メモリの分析に役立つと期待されます。二重のインデックス付け (M, S)|→Module[M, S] があり、M側を固定するかS側を固定するかで、異なるインデックス付き圏が現れます。S|→Module[*, S] は、M|→Module[M, *] を転置した形になっています。

転置すると物の見方が代わりますが、M|→Module[M, *] だとCPU中心、S|→Module[*, S] だとメモリ中心の見方になります。どちらか一方では現象が見えにくいでしょうから、結局、二重インデックス付き圏全体を見渡しながら、必要に応じてインデキシングを切り替えることになるのでしょう。

状態空間をベースとするファイバーとインデキシング

状態空間Sを固定したファイバー Module[*, S] がどんな形かを見ておきましょう。集合圏のなかで考えれば、ファイバー Module[*, S] は具体的に記述できます。

Sは状態空間（と呼ばれる集合）で、これは固定されています。Mは集合圏のモノイド、つまり普通のモノイドです。3つ組 (M, S, a)が、ファイバー Module[*, S] に入ることは、(M, S, a) が加群であることですが、集合圏で加群はオートマトンのことです。Sは固定しているので、ファイバー Module[*, S] の射（垂直方向の射）は、f:(M, S, a)→(N, S, b) という加群準同型（オートマトン準同型）です。このfは、M→N というモノイド準同型で、作用（オートマトンの状態遷移）aをbに移すものです。

加群（オートマトン）(M, S, a)を右加群の形で書くのなら、作用aは、a:S×M→S in Set となります。集合圏Setはデカルト閉なので、a:M→[S, S] と書いても実質は同じです。ここで、[S, S] は指数です。[S, S] は外部ホムセット Set(S, S) = Hom_Set(S, S) = End_Set(S) を内部化したものなので、[S, S] = end(S) とも書くことにします。end(S) は、自己射の結合に関するモノイド構造を内部化したモノイド構造を持つので、end(S)∈|Monoid| と考えることができます。

以上のことから、加群のスカラー乗法（オートマトンの状態遷移）aは、a:M→end(S) in Monoid と同一視できます。Sは固定してますが、Mのほうを動かすので、スカラー乗法の全体はオーバー圏（スライス圏）Monoid/end(S) の対象類に一致します。スカラー乗法を保つモノイド準同型が Monoid/end(S) の射なのですが、これはファイバー Module[*, S] の射と同じです。

結局、状態空間Sを固定したファイバー Module[*, S] は、モノイドの圏Monoidから作ったオーバー圏Monoid/end(S) と同じ形をしています（圏同値）。さらにSを動かせば、S|→Monoid/end(S) となりますが、これはEP(Set)をベースの圏とするインデックス付き圏と考えると、二重インデックス付き圏 (M, S)|→Module[M, S] をS側でインデキシングしたものになります。

以上の記述は、S|→end(S) という「状態空間から標準的モノイドを作る」対応を利用しているので、指数を持たない圏ではそのままは使えないでしょう。

もう一言

Monoid×State は集合圏から具体的に作るので扱いやすいのですが、集合圏に依存した議論もあって、抽象度も一般性も不足しています。そもそも、プログラムがモノイドの要素としてモデル化されるのは単純すぎるので、モノイドより一般的な対象を持つ圏でないとモデル化に不十分です。より一般化したときに、状態空間、加群のスカラー乗法、状態空間の射（今はEP射）などがどう定義されるべきかはよくわかりません。

当面、Monoid×State を使うにしても、並行実行、同期と排他、通信、トランザクションなどを定式化するにはまだ作業が必要です。ある程度は分かっている所と全然分からないことがあるので、まーボチボチと書くつもりです。