クリーネ代数への批判と賞賛：プログラムのモデル色々 - 檜山正幸のキマイラ飼育記 (はてなBlog)

僕は、クリーネ代数に批判的なことを言ったりしています。例えば、古く（2005年）は「実はKleene代数は好きじゃない」、最近（2014年）では「クリーニ代数と圏論」とか。批判の対象にするということは、それに興味を持っているということです。興味がないものは批判さえしません。

僕はもちろん、クリーネ代数に興味を持ち続けています。でも、「これじゃ足りない」感があるのです。その感じを記します。不足を補う方針にも言及します。過去の記事への参照をたくさん入れますが、それにより、僕がこの話題の周辺を長年ウロウロしていることが分かるでしょう。

内容：

プログラムの代数としてのクリーネ代数
クリーネ代数では表せない現象
トレース付きデカルト圏とデカルト半加法圏
並列実行と同期通信
条件付き実行はどこに行った？
時分割実行と待ち合わせ
クリーネ代数は足りないけど素晴らしい

プログラムの代数としてのクリーネ代数

クリーネ代数が素晴らしいのは、プログラムの代数的取り扱いを可能としたことです。プログラムの組み合わせや制御方法には次のものがあります。

順次実行
選択的実行
繰り返し実行
条件付き実行

クリーネ代数による定式化では、これらの実行制御を代数演算で表します。

プログラム	クリーネ代数
順次実行	掛け算
何もしないプログラム	掛け算の単位元
選択的実行	足し算
ハングするプログラム	足し算の単位元（零元）
繰り返し実行	クリーネスター

ここで、「ハングするプログラム」は「無限ループするプログラム」と同じです。「プログラムの算術的計算法 (続き＆完結）」に、while(true){;} が「ハングするプログラム」であり、それが足し算の単位元（零元）になることを説明しています。

掛け算・足し算・クリーネスターだけだと、条件付き実行（if文やwhile文）を表現できません。条件（テスト）を入れたクリーネ代数がテスト付きクリーネ代数です。テスト付きクリーネ代数については、「テスト付きクリーネ代数とその使い方」に書いてあります。絵による表現は「非決定性プログラミングだって絵を描いてみれば一目瞭然」を参照。

クリーネ代数では表せない現象

プログラムの代数的な表現を与えるクリーネ代数ですが、次の点では不足・不満を感じます。

異なる状態空間のあいだの遷移を表せない。
「型」の概念を表せない。
並列実行を表せない。

クリーネ代数がモデル化している現象は、単一の状態空間の上での非決定性状態遷移です。テスト付きクリーネ代数では、状態空間上の述語（ブール値関数）を一緒に考えます。

たくさんの状態空間、型付きのプログラム、並列走行するプログラム群などは、もともとスコープ外です。工夫をして、スコープ外の現象までモデル化する手段があるかも知れませんが、「無理してる」感が否めません。僕はそういった工夫は虚しい努力だと感じるのでやる気が起きません。

上記の問題点（機能不足）を克服するには、クリーネ代数を超える枠組みが必要でしょう。

トレース付きデカルト圏とデカルト半加法圏

クリーネ代数を超える枠組みの基本となるものが、トレース付きデカルト圏です。トレース付きデカルト圏は、トレース付き（対称）モノイド圏（「トレース付き対称モノイド圏とはこんなモノ」、「トレース付きモノイド圏の新しい定義」参照）のモノイド積がデカルト積となっているものです。

トレース付きデカルト圏では、再帰や不動点の議論ができます。この事実を明らかにしたのは長谷川真人さんです。長谷川さんの論文・スライドへの参照は「フローチャートをめぐる迷信と妄言と愚昧」の真ん中へん、「関数型言語では、フローチャートは書けない?!」のセクションにあります。長谷川（と先駆者達）の定理の簡単な紹介は「絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」」にあります。

クリーネ代数を再現するには、トレース付きデカルト圏では構造が不足で、追加の仮定が必要です。その仮定とは；デカルト積が双積になっており、始対象と終対象が一致する（零対象が存在する）ことです。零対象と双積を持つ圏を半加法圏と呼ぶので、この仮定があると、トレース付きデカルト半加法圏を考えることになります。

トレース付きデカルト半加法圏でクリーネ代数が再現できることは、「トレースを使ってクリーネスター（またはクリーネプラス）を計算する方法の概略」にだいたいは書きました。

トレース付きデカルト半加法圏の対象ごとに1つのクリーネ代数（正確にはコンウェイ代数と言うべきだけど）が構成できて、次の対応があります。

トレース付きデカルト半加法圏	クリーネ代数
対象 A	クリーネ代数 K = End(A)
自己射 f:A→A	クリーネ代数の要素 f∈K
結合 f;g	掛け算 fg
恒等射 id_A	単位元 1
Δ;(f×g);∇	足し算 f + g
零射 0_A	零元 0
Tr(∇;f;Δ)	クリーネプラス f⁺

クリーネスターf^*は、f^* = 1 + f⁺ と定義できます。

並列実行と同期通信

トレース付きデカルト半加法圏により、異なる状態空間のあいだを遷移する挙動は、自己射ではない射 f:A→B（A ≠ B）により表現できます。圏の対象を型と考えることもできます。しかし、並列実行は相変わらず表現できません。

トレース付きデカルト半加法圏のデカルト双積は、集合論的に解釈すると直和になっています。「直和が直積」となる状況は、「Alloyの矢印記法と、モノイド閉圏としての関係圏」に書いています。デカルト双積では集合の直積が出てこないので、並列実行の定式化は無理です。

デカルト双積とは別に、集合の直積に相当する“テンソル積”を入れた圏をテンソル半加法圏と呼ぶことにします。実際は、「テンソル積付きトレース付きデカルト半加法圏」を相手にするのですが、名前が長ったらし過ぎるので、トレースやデカルト双積の存在は暗黙に仮定します。

テンソル半加法圏については幾つかの記事で言及しています：

デカルト双積とは別にテンソル積を導入すると、fとgの同時並列実行を f $\otimes$ g で表現できます。しかし、f $\otimes$ g は、fとgがまったく無関係に、相互作用なしに実行されることを表しているだけなんです。

並列走行しているfとgが通信（相互作用）しないと面白くありません。同期通信に関してはIO結合という“結合”を導入すれば良さそうだと思っています。

ラベル付き遷移系のIO結合

非同期通信は、同期通信とバッファリングの組み合わせで定式化できるでしょう。その背景は「圏論番外：同期／非同期の結合」。

通信／相互作用を含めた並列実行を定式化するには、テンソル半加法圏とIO結合（同期通信）を一緒にする必要があるのですが、あんまり考えていません。

条件付き実行はどこに行った？

クリーネ代数に条件付き実行を追加したのがテスト付きクリーネ代数でした。そして、クリーネ代数の一般化としてトレース付きデカルト半加法圏やテンソル半加法圏を導入したのでした。となると、トレース付きデカルト半加法圏／テンソル半加法圏にもテスト（ガード条件）を追加したくなります。

これに関しては、以下の記事で扱ってますが、印象としては「意外に難しい」。

条件付き実行の「条件」が、古典二値の命題でいいのかは疑問です。ハング（無限ループ）するプログラムとか判断困難な状況を考えると、4値論理がいいような気がします。

時分割実行と待ち合わせ

複数のCPUを使う「ほんとの並列実行」は、時分割方式で単一CPUでもシミュレートできます。これはよく知られた事実で、現実にも使われています。でも僕は時分割シミュレーションが不思議でしょうがありません。シミュレートのメカニズムが目に見えるようになる定式化はないのでしょうか。

テンソル半加法圏のテンソル積は、「集合論的には直積で並列実行の定式化に使う」と言いました。このテンソル積＝集合論的直積は、「ほんとの並列実行」を意味し時分割実行ではありません。時分割実行を意味する別なモノイド積があるんじゃないかと思っています。そのモノイド積に関する目論見はあるのですが、まだ言及したことはありません。

時分割実行でほんとの並列実行をシミュレートは出来ても、実行時間は遅くなります。つまり、実行時間まで考えたら「同じ」には出来ないはずです。ここらへんのことは、「プログラムの実行時間を計る事と半環の代数」で書いたような時間計測で議論できるかも知れません。

並列実行に関してよく理解できないことがまだあります。複数のプログラム（プロセス）A₁, A₂, ..., A_n が並列に走っていて、それらの終了を待っているプログラムBがいるとします。A_i（i = 1, 2, ..., n）どれかひとつが終わるとすぐにBが走り出す場合と、すべての終了を待ってからBが走るのではまったく挙動が違います。

以上のことは、並列実行を記号「*」、順次実行を記号「;」で表すとして、(A₁*A₂* ... *A_n);B の意味が定まらないことです。「並列」が混じると「順次」の意味も考え直さないといけないのです。

これは、「call-by-value call-by-name, call-by-need」の話とか論理式の∀、∃の評価の話と関係あるでしょう。「今週見つけた圏」（今週＝2012年6月のとある週）がモデルになりそうです。

クリーネ代数は足りないけど素晴らしい

クリーネ代数は「ダメだ」と言ったり「素晴らしい」と言ったり、言動がメチャクチャと言われも仕方ないですが、「嫌い」ってことは「好き」なんだ、とか、そういう感情もありますからね。

さて、クリーネ代数はプログラムの代数であると同時に、形式言語の代数であり、また関係の代数でもあります。

プログラム	形式言語	関係
非決定性写像 f:S→S	部分集合 L⊆Σ^*	部分集合 R⊆A×A
写像の結合 f;g	部分集合の連接 L;M	部分集合の推移結合 R;S
恒等写像 id_S	単元集合 {ε}	対角集合 Δ_A
値の合併による和 f + g	集合の合併 L∪M	集合の合併 R∪S
まったく未定義な写像 0	空集合 $\emptyset$	空集合 $\emptyset$
不定回の繰り返し f^*	不定回の連接の和 L^*	反射的推移的閉包 R^*

さらに、プログラムと形式言語を繋ぐ存在としてオートマトンがあり、関係は有向グラフや行列として表現することも出来ます。

クリーネ代数は、一見かけ離れた対象物が持つ共通の構造をうまく抽象しているのです。クリーネ代数を拡張する場合は、クリーネ代数では定式化できなかった概念が取り込めている事と共に、クリーネ代数の多くの実例がどこまで再現されるのかに注意すべきでしょう。

クリーネ代数をひとつの「基準点」と考えるとき、そのバランスの良さを改めて感じたりします。頂きにはほど遠いけど信頼できるベースキャンプ -- そんな感じかな。