在Milner的Pi微積分中，當多個進程從同一個通道讀取時，什麼是評估語義？

Question

在Milner的Pi微積分中，當多個進程從同一個通道讀取時，什麼是評估語義？

規則說

!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」。這兩個執行都對這個過程有效。您可以考慮與這些流程相關的標籤轉換系統 - 它會像您期望的那樣分支。

恰恰是這種不確定性使得過程計算（如Pi微積分和朋友）「特殊」，與lambda微積分不同，它以什麼順序評估事物並不重要（你會達到相同的結果）。 Pi微積分具有所有這些機制，如互模擬和轉換系統語義，以便它可以捕捉這些類型的情況並使其適合於分析。