「方式」のあいだの同値性
プログラムの同値性ではなくて、プログラミング方式と実行方式のあいだのマクロな同値性を考える。例えば、時分割方式とマルチCPU方式。
時分割方式のプログラムの圏とマルチCPU方式のプログラムの圏がなんらかの意味で同値となる。「なんらかの意味」は、ある種の森田同値だろう。
時分割方式のプログラムの圏をC、マルチCPU方式のプログラムの圏をDとする。それぞれが小さな厳密モノイド圏となる。つまり、小さな厳密モノイド圏の森田同値が問題となる。
- C→(Set, ×, 1) というタイト（強）モノイド関手が右加群に相当する。
- Cop→(Set, ×, 1) というタイト（強）モノイド関手が左加群に相当する。
- Cop×D→(Set, ×, 1) というタイト（強）モノイド関手が双加群に相当する。
右加群は、プログラムの実行系または実行モデルとして解釈できる。が、左加群は順序が逆転するので分かりにくい。逆プログラムまたは反プログラムの実行系で、逆実行モデルまたは反実行モデル。双加群はさらに分かりにくい。
右加群の圏の同値を森田同値と定義すれば、「実行モデルの圏が圏同値になる」ことだから、これは自然な同値性になる。実行モデルのあいだに対応が付くことになるから、プログラミング方式／実行方式が同値だと言っていいだろう。
上記の枠組で、時分割方式とマルチCPU方式が森田同値であることを示したい。それほど簡単ではなくて、時分割方式のときは非決定がはいるので、シャフル積は非決定の積となる。マルチCPU方式は決定性の圏で、時分割方式は非決定性の圏だから、直接に比較はできない。単なる森田同値ではなくて、随伴と組合せないとダメなんだと思う。
状態遷移系は、モノイドが作用する集合として定義できる。Mをモノイド、Sを状態空間とすると、M→End(S) で状態遷移系が決まるから、これは右加群だといってよい。しかし、Mを単対象圏と考えるとモノイド積がない。次のようにしてMをモノイド圏にする。
- Cの対象集合はN = {0, 1, 2, ...} である。
- C(0, 0)はidだけの単元集合。
- C(n, n) := Mn として、Mの直積モノイドの構造を入れる。
- n≠m のときは、C(n, m) := 空集合
これは分断圏になる。モノイド積は、C(n, n)×C(m, m)→C(n+m, n+m) だけを定義すればよいが、これはタプルの連接で定義すればよい。
モノイドMが単一CPU上の機械語プログラムの全体のモデルになる。CがマルチCPUのプログラム全体のモデルとなる。圏の結合がプログラムの順次結合、モノイド積が並列結合。この圏CからSetへのモノイド関手は、プログラムの実行モデルとなり、拡張された状態遷移系を定義する。
時分割方式を同様に定義するには、非決定を考慮する必要がある。Mの直積（累乗）ではなくて、自由積に関する累乗を考える必要があるし、クライスリ圏も必要そうだ。
