同期と非同期：セリンガーとBagnol／Guatto
次の論文をチラ見した。
- Title: Synchronous Machines: a Traced Category
- Authors: Marc Bagnol & Adrien Guatto
- URL:http://iml.univ-mrs.fr/~bagnol/drafts/synchronous-machines.pdf
Marc BagnolとAdrien Guatto（以下、BG）は二人とも博士課程の学生さんのようだ。
これを読んで、随分と前にやはりチラ見したセリンガーの論文を思い出した。セリンガーの論文ページ http://www.mathstat.dal.ca/~selinger/papers.html に2UPのPDFが用意されていて印刷に便利だ。
- Title: Categorical structure of asynchrony
- Author: Peter Selinger
- URL: http://www.mathstat.dal.ca/~selinger/papers/catasynch-2up.pdf
BGの論文は新しい視点を提供するものだが、なんかもの足りない。既存の知識の解説が大部分で「それで終わり？」という感じ。興味深いのは、同期を扱っていながら、非同期の定式化であるセリンガーとほとんど同じ話になっていることだ。
セリンガーの書くものはよく整理されていて鋭い。asynchronyもよくできた論文だと思ったのだが、今読み返してみると、用語法がミスリードだな、と思った。実際、僕も誤解があった。とりあえず、BGとセリンガーの用語の対応表を示す。
| 遷移系一般 | セリンガー | BG |
|---|---|---|
| 状態 | state | state |
| ラベル | action | - |
| 始状態 | initial state | initial state |
| 遷移 | transition relation | transition relation |
| 合同 | weak bisimulation | graph isomorphism |
| 入力 | input action | input signal |
| 出力 | output action | output signal |
| 無音遷移 | silent transition | - |
| バッファ性 | in/out-buffered | - |
合同（congruence）とは、どういう基準で遷移系を「同じ」とみなすか？ということ。BGの「graph isomorphismがあるとき同じとみなす」ってのは、何を言っているかイマイチわからない。遷移系を、入出力のペアでラベルされた辺ラベル付き有向グラフとみなす、ってことか？ 双模倣に比べて強い（狭い）し根拠もハッキリしない。
| 圏論一般 | セリンガー | BG | |
|---|---|---|---|
| 圏の結合 | sequential composition | composition | |
| モノイド積 | parallel compositon | tensor product | |
| トレース | feedback | trace | |
| GOI構成 | - | G construction |
以下、次の記号を用いる。
- 状態空間 S
- アクション記号の集合 A
- 入力の集合 X
- 出力の集合 Y
- 圏の結合 ;
- モノイド積
セリンガーとBGの違い：
- BGは、入出力と別にラベル（アクション記号）を考えない。入力信号（記号）と出力信号（記号）の組がラベルになる。
- セリンガーでは、入出力データ（BGは信号と呼ぶ）が、アクション記号に埋め込まれる。アクションに、入力アクション、出力アクション、無音（silent）アクションの別がある。無音アクションは入出力を伴わない遷移（無音遷移）を引き起こすアクションで、一種類（τ）しか考えない。
- セリンガーの遷移は、S×A×S の部分集合。
- セリンガーの遷移は、A×S→Pow(S) とも書ける。
- BGの遷移は、S×Pow(X)×Pow(Y)×S の部分集合。
- BGの遷移は、Pow(X)×S → Pow(S×Pow(Y)) とも書ける。
- BGが言っていることは、結合とテンソル積から作ったトレース付き圏からGOI構成したらコンパクト閉圏ができて、そこの結合がオートマトンの同期積（synchronous product）だ、ということ。
セリンガーの定式化は、意図もわかるし、好き嫌いを置いておけば納得できる。BGの遷移 S×Pow(X)×Pow(Y)×S は何なんだろう？ Pow(X), Pow(Y) を X', Y' とすると、X'×S → Pow(S×Y') だから、遷移は非決定性で状態を持つ関数と言える。しかし、最初から Pow(X) を取るのはなぜだろう？
A := X'×Y' とすると、BGの遷移は S×A×S の部分集合だから、ラベルとして入力と出力のペアを取っていることが分かる。一方、セリンガーは、{in}×X + {out}×Y + {τ} という直和を使っている。直積と直和の違いがあるのは、BGは最初から並列実行が前提なのに、セリンガーは、ひとつのプロセス（エージェントと呼んでいるが）の内部はあくまで順次実行なのである。2個のCPUを必要とするペアリングは禁止している。
セリンガーは、sequential, parallelを対比的に使っているが、この用語法は良くない。sequential結合は順次実行のように思えるが、実際は並列実行なのである。それが証拠には状態空間は直積を使っている。IOを通じて並行プロセスを複合している。IOチャネルで方向付きで繋ぐので自由には動けない。パイプライン並列だ。一方のparallel結合は無関係に独立して動く並列。
時間方向に繋ぐという意味のsequentialなら、セリンガーもBGも定義してない。二重圏で定式化するものだ。
セリンガーは非同期を扱っているが、sequential compositionは同期結合になっている。無限バッファを入れて非同期の圏を作っている。無限バッファBが、B;B B という性質を持つことを利用している。セリンガーの非同期圏（asynchronous agentの圏）とBGの同期圏（synchronous machineの圏）が同じになってしまうのは、セリンガーも基本は同期結合だからだ。
セリンガーのparallel composition、BGのtensor productの定義をよく見ると、これはタイムシェアリング、シャフル積に対応するわけで、むしろ逐次実行になっている。デマルチプレクサを使って複数のCPUに分配すると並列処理もできる。
セリンガーは時間の観点を入れてないが、それは時間概念をなくすことが目的で、そのために無限バッファを導入している。それに対してBGは、グローバルに同期した時間を入れているが、その割に時間による影響をちゃんと考えてない。
なんか足りない。どこか歪んでいる。どうも痒いことになっている。
