アルファベットも圏であることと、ステージ付き遷移系
アルファベットも圏(の生成系)と言ったが、実例を出す。
以前から僕は、状態遷移におけるステージ(フェーズとかモードと言ってもよい)という概念を使ってきた。次の例では、4つのステージを持つ。(ネーミングは、created/disposed とか born/dead のほうがよかった。
- beBorn
- ready
- working
- disposed
アクション記号は
- init : beBorn→ready
- begin : ready→working
- end, cancel : working→ready
- put(0), put(1), ..., unput : working→working
- dispose : working→disposed
実は間違っている。 disposeは、ready→disposedのはずだ。これは、書き込みバッファを持ったストリームを表すオブジェクトのライフサイクルを表す。図を見れば明らかなように、ラベル付き有向グラフで、辺ラベルがアクション記号になっている。そして、頂点ラベルがステージの名前。
この有向グラフから自由圏(道の圏)を作れば圏になるから、ラベル付き有向グラフと圏はほぼ同一視してもよい。それで、ラベル付き有向グラフがアルファベットだから、アルファベットも圏となる。
アルファベット=ラベル付き有向グラフをAとする。A→Setという関手が決定性オートマトン(遷移系とオートマトンは今は区別しない)。A→Relという関手が非決定性オートマトン。値を取る圏をCとすると、CA がアルファベットAのオートマトンの圏。オートマトンの圏の射は関手のあいだの自然変換になる。
アルファベット達の圏(有向グラフの圏)をDiagとすると(図式だからDiag)、A∈|Diag|に対して圏CAが対応しているからインデックス付き圏となる。
Diagの対象であるグラフは構文的な存在物とみなされる。よって、Diag内の射は構文的な変換とみなされる。Diagにいろいろな結合を入れるとマンダラ圏の構造を持つようになるだろう。つまり、Diagはプログラム図式の圏とも考えられる。
上の図で注意すべきは、ステージは単なるラベル付き頂点だが、ステージに対応するのはSetまたはRelの対象なので、要素(点)を持つ状態空間である。beBornやreadyなどの状態空間は単元集合となる。ステージ(の記号)、単元の状態空間、状態点をシッカリ区別せよ。
アルファベットを圏(の生成系であるグラフ)と捉えただけでかなり自由度が上がるし、現実の表現にも便利、そしてマンダラ圏の構成にも近づく。