computer-science - ミルナーの円周率計算では、複数のプロセスが同じチャネルから読み取るときの評価セマンティクスは何ですか?

Question

ミルナーの円周率計算では、複数のプロセスが同じチャネルから読み取るときの評価セマンティクスは何ですか?

ルールはそう言っている

!x(a). P | ?x(b) Q ~> P | Q[a/b]

しかし、次のような状況はどうですか

!x(a). P | ?x(b) Q | ?x(c) R

?

Answer 1

この質問がやや古いことは承知していますが、次の人が答えを探しに来るために、私は答えを試してみます。

答えは、非決定論的です。円周率計算プロセス:

?x(b).Q | ?x(c).R

「x で入力を受け入れてから Q として続行するか、x で入力を受け入れて R として続行するかのいずれか」と言います。このプロセスに関しては、どちらの実行も有効です。これらのプロセスに関連付けられたラベル付けされた遷移システムを考えることができます --- ご想像のとおり、分岐します。

プロセス計算 (円周率計算やその仲間のような) を「特別な」ものにするのはまさにこの種の非決定性であり、物事を評価する順序が問題にならないラムダ計算のようなものとは異なります (同じ結果に到達します)。 ）。円周率計算には、バイシミュレーションや遷移システムのセマンティクスなどのすべての機械が正確に含まれているため、このような状況を捉えて分析に適したものにすることができます。