コボルディズム的プログラム意味論
グラフのコボルディズムに期待すること - 檜山正幸のキマイラ飼育記 メモ編 の繰り返しになるが、特に強調したい所：
- 並列実行と同期通信を表現できる（IO結合）。
- 時分割・直列化実行を定式化できる。
- プログラムの実行時間とメモリ使用量を定式化できる。
- プログラムの同値性（振る舞い同値、観測的に識別不能、機能仕様として同じ）が定式化できる。
- イプシロン遷移εと無音遷移τを区別する。
それを使って：
- ファイルやキューなどの広義のバッファを定式化できる。
- 無限キューのベキ等性を示せる。
- 並列パイプと直列化パイプの同値性を示せる
ポイントは広義のバッファ（ミュータブルコレクション）の扱いだと思う。write-mode新規ファイル、read-modeファイル（初期値はいろいろ）、既存ファイルをread-wrieモードで開けた場合、複数のファイル、名前付きパイプなどを定式化する。
Erlangのようなマイクロプロセスにメールボックス（キューバッファ）が付いたモノも容易に扱えると思う。
決定性コンパイルのほうが分かりやすいな。IOオートマトンからをグラフと見てパス圏を作る。このとき、非空パスに付くラベルを X*×Y*にする。ラベルが、(X_×Y_)* とはまったく違う。
X_×Y_ をラベルとするグラフから、Pow(X*×Y*)またはBag(X*×Y*)をラベルとする反射的推移的グラフを作る。ラベル付きグラフの圏におけるモナドになるが、モナドの作り方がかなり特殊だ。
