Каковы семантики оценки в Pi Calculus Милнера, когда несколько процессов читают из одного канала?

Question

Каковы семантики оценки в Pi Calculus Милнера, когда несколько процессов читают из одного канала?

Правила говорят, что

!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". Оба исполнения действительны в отношении этого процесса. Вы можете рассмотреть помеченную переходную систему, связанную с этим процессом - она ​​будет ветвиться, как и следовало ожидать.

Именно этот вид недетерминизма делает исчисление процесса (например, исчисление Пи и его друзей) "особенным" и отличается от таких вещей, как лямбда-исчисление, где не имеет значения, в каком порядке вы оцениваете вещи (вы достигнете того же результата). Исчисление Пи имеет весь этот механизм, такой как бисимуляция и семантика системы переходов, именно для того, чтобы он мог фиксировать подобные ситуации и делать их доступными для анализа.