博士

ロボ子、今日のITニュースは非決定性セマンティクスじゃ！

ロボ子

非決定性セマンティクスですか。それはまた難しそうな...

博士

難しくないぞ！簡単に言うと、プログラムが複数の結果を持つ可能性があるってことじゃ。「プログラムは複数の結果を持つ可能性があるため、セマンティックドメインの自然な選択肢は、初期状態から可能な結果の空でない集合への関数である」って書いてある。

ロボ子

なるほど、一つの入力に対して複数の出力があり得るということですね。

博士

そうそう！そこで、モナドを使うんじゃ。\(\mathcal {M}(X) = mathcal {P}(X_ot) setminus emptyset\)というモナドに対して、\(\eta\)と\(\mu\)演算を提供するらしい。

ロボ子

\(\eta\)と\(\mu\)演算、ですか。具体的にはどういうものなんですか？

博士

\(\eta(x) = \{ x \}\)で、\(\mu(S) = (\bigcup_{X \neq \bot \in S} X) \cup (S \cap \{ \bot \})\)じゃ！

ロボ子

うーん、ちょっと難しいですね...。

博士

大丈夫！要は、非決定的な選択演算子を和の形で簡単に追加できるってことじゃ。「\(\llbracket c_1 + c_2 \rrbracket_mathcal {C} = \lambda \sigma. \llbracket c_1 \rrbracket_mathcal {C} \sigma \cup \llbracket c_2 \rrbracket_mathcal {C} \sigma\)」って書いてある。

ロボ子

なるほど、選択肢が増えるごとに、結果の集合が広がっていくイメージですね。

博士

そういうことじゃ！でも、ここで問題があるんじゃ。\(\mathcal {P}(X_ot) setminus emptyset\)の要素をどう順序付けるか、明確じゃないらしい。

ロボ子

順序付けですか。部分集合包含関係\(\subseteq\)を使うのはどうでしょう？

博士

それが、\(\emptyset\)がないから、最小要素がないんじゃ。しかも、それだと「単一の状態 \(\{ \sigma \}\) を返す決定的な終了プログラムは、発散する可能性のあるプログラム \(\{ \bot, \sigma \}\) よりも情報量が多いと見なされる」ことになって、ほとんどの操作が連続的でなくなるらしい。

ロボ子

なるほど...色々な順序付けを検討する必要があるんですね。

博士

そうじゃ！冪集合演算子\(\mathcal {P}\)と同様の構成をセマンティックドメインに対して考えたいらしい。そのためには、algebraic CPOというものが必要になるらしいぞ。

ロボ子

CPO...奥が深いですね。

博士

まあ、簡単に言うと、非決定性セマンティクスを扱うには、集合の順序付けとか、色々な数学的な知識が必要になるってことじゃ！

ロボ子

勉強になります！

博士

ところでロボ子、非決定的なプログラムって、まるで私みたいじゃない？

ロボ子

え？どういうことですか？

博士

だって、私の行動も予測不可能で、いつも複数の結果を生み出すじゃん？

ロボ子

それは...否定できませんね（苦笑）。

博士

アハハ！