
ВЫЧИСЛИТЕЛЬНЫЕ ИСЧИСЛЕНИЯ ЧАСТЬ 2: π-исчисления
ОБЗОР
В первом серии статей мы рассмотрели грамматику и оперативную семантику для λ-исчисления.
Наш интерес к π-исчислению заключается в том, что он является предшественником ρ-исчисления. Это модель параллельных вычислений, или, более конкретно, исчисление процесса, основанное на понятии именования. В исчислении процесса мы представляем взаимодействия между независимыми агентами или процессами как передачу сообщений, в отличие от модификаций общих переменных (как в λ-исчислении).
π-исчисление отличается от λ-исчисления различием между именами и процессами и добавлением терминов-конструкторов, включая параллельную композицию, которая отвечает за параллелизм. Таким образом, в π-исчислении, процессах и именах есть два разных объекта и различные взаимодействия между процессами и именами. Однако, как и λ-члены, процессы в π-исчислении строятся из имен.
Параллельная композиция позволяет вычислить в процессах: либо-либо параллельно, либо самостоятельно или же использовать обмен данными по общему каналу. Это применимо для смарт-контрактов, которые используются в приложении, и хранения переходов состояний виртуальной машины.
В этой статье мы обсудим грамматику, структурную конгруэнтность и оперативную семантику π-исчисления.
Πi-исчисление
Здесь мы обсудим упрощенную версию π-исчисления, предложенную Робин Милнер [1].
Грамматика
Представление BNF грамматики для π-исчисления
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (𝜈x)P | P|Q | !P (1.1)
Аналогично λ-исчислению, π-исчисление является параметрическим в наборе имен X. Даже не зная, что означают эти операторы, мы уже знаем, что мы можем написать
P[X] ::= 0 | X(X).P[X] | X̅⟨X⟩.P[X] | (𝜈X)P[X] | P[X]|P[X] | !P[X]
чтобы выразить эту зависимость от X явно.
Возвращаясь к (1.1), допустимые члены этой грамматики, т. е. выражения в правой части этого представления, также называются конструкторами термов. Ниже мы обсудим эти терм конструкторы.
Остановленный процесс: 0
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
Этот процесс означает «ничего не делать», т. е. выполнение завершено, и оно прекратилось.
Ввод-сохранение продолжения или префикса ввода: x (y) .P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
Данный процесс ожидает имя, отправленное по каналу x, чтобы заменить имя y в процессе P. Это аналогично, как в абстракции имени y, λy.P в λ-исчислении, где привязывают имя y в процессе P ,
Отправить на канал и выполнить или вывести префикс: x̅⟨y⟩.P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
(νx)P — читает “новый x в P” — определяет x как новое имя и связывает его в процессе P.
Параллельная композиция: P | Q
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
P | Q — чтение «P par Q» — означает, что процессы P и Q одновременно активны; они могут действовать независимо, или они могут общаться друг с другом.
Копирование: !P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
! P — читать «bang P» — означает P | P | …; столько копий, сколько пожелаете. Этот процесс всегда может создать новую копию P. Правила сокращения делают так, что нет риска бесконечной параллельной деятельности.
Каждый процесс в π-исчислении построен из остановленного процесса 0. Давайте построим несколько простых процессов.
Несколько простых процессов
- 0
Это самый простой процесс, из которого создаются все остальные процессы.
- x(y).0
Этот процесс ожидает сообщения y на канале x, а затем останавливается.
- x̅⟨y⟩.0
Этот процесс отправляет сообщение y по каналу x, а затем останавливается.
- (𝜈x)0
Этот процесс объявляет новое имя x в остановленном процессе.
Считаете ли вы, что это должно соответствовать процессу, который у нас уже есть?
- 0 | 0
Остановленный процесс выполняется одновременно с остановленным процессом.
Считаете ли вы, что это должно соответствовать процессу, который у нас уже есть?
- x̅⟨y⟩.0 | x(z).0
Этот процесс одновременно отправляет и получает сообщение на канале x. Так происходит общение!
Одновременная отправка и прием сообщений на одном канале позволяет осуществлять связь на этом канале. В общем случае процесс x̅⟨y⟩.P | x (z) .Q соответствует сообщению на канале x. Говорят, что x и x̅ находятся в отношениях имени / со-имени.
Структурная конгруэнтность
Интуитивно мы ожидаем эквивалентность между некоторыми процессами. Например, P | 0, 0 | P и P должны быть эквивалентными. Подумайте об этом.
Процесс P | 0 означает, что мы выполняем процесс P одновременно с остановленным процессом 0. Это не может быть иначе, чем выполнение процесса P само по себе. Вообще говоря, мы обозначаем структурную конгруэнтность процессов P и Q через P ≡ Q. Наши интуиции кодируются следующими аксиомами структурной конгруэнтности.
a-эквивалентность:
P ≡ Q, если Q можно получить из P, переименовав одно или несколько имен, связанных в P (мы обсудим свободные и связанные имена более подробно позже в серии статей). Это аналогично α-превращению в λ-исчислении. Это означает, что две программы эквивалентны, если они отличаются только именами переменных, используемых внутри. Они выполняют один и тот же код, но могут называть вещи разными именами согласованным образом
Аксиомы для параллельной композиции:
- P | Q ≡ Q | п
Порядок, в котором мы перечисляем параллельные процессы, не имеет значения, поскольку они выполняются одновременно. Поэтому процессы P | Q и Q | P эквивалентны.
- (P | Q) | R ≡ P | (Q | R)
Пар оператор должен быть ассоциативным. Мы только говорим о «совместном» двух процессах, поэтому, если мы хотим выпустить третий процесс в микс, есть два разных способа сделать это. Эта эквивалентность говорит, что эти два способа одинаковы, потому что мы одновременно выполняем эти процессы.
- P | 0 ≡ P
Запуск остановленного процесса вместе с другим процессом P не должен отличаться от того, что работает только один процесс. Эта эквивалентность говорит именно об этом. Параллельный процесс с остановленным процессом аналогичен добавлению числа 0.
Аксиомы для ограничения:
- (νx) (νy) P ≡ (νy) (νx) P
При объявлении новых имен в процессе сам порядок не имеет значения. Данная эквивалентность отражает это понятие.
- (νx) 0 ≡ 0
Объявление нового имени в остановленном процессе не должно ничего делать. Поэтому он должен быть эквивалентен остановленному процессу.
Аксиома для репликации:
-! P ≡ P | !П
С репликацией процесса мы всегда можем создать новую копию процесса. Следовательно, процессы! P и P | ! P эквивалентны.
Аксиома, связанная с ограничением и параллелью:
Если имя x связано в Q, то (νx) (P | Q) ≡ (νx) P | Q.
Это свойства структурной конгруэнтности в π-исчислении. Структурная конгруэнтность отражает понятие вычислительной неразличимости. То есть два структурно конгруэнтных процесса идентичны с точки зрения вычислений.
Структурная конгруэнтность является примером того, что называется отношением эквивалентности в математике. Мы рассматриваем его как вычислительную эквивалентность процессов.
Теперь мы будем точно понимать понятие связи в π-исчислении и обсуждать оперативную семантику.
ОПЕРАЦИОННАЯ СЕМАНТИКА, В ТОМ ЧИСЛЕ ПРАВИЛА СОКРАЩЕНИЯ
Напомним, что префикс представляет отправку сообщения y по каналу x, а префикс x (z) представляет прием сообщения z на канале x. Мысль заключается в том, что когда передача и прием по одному и тому же каналу происходят одновременно, происходит обмен данными, и получатель затем использует переданную информацию. В символах это написано
x̅⟨y⟩.P | x (z) .Q → P | В {г / г}
Символ → означает «сокращается до», и мы называем это comm сокращение или comm правило. Это означает, что если мы найдем два процесса x̅⟨y⟩.P и x (z) .Q, выполняющиеся одновременно, то y отправляется по каналу x, y заменяет z в процессе Q, а процессы P и Q (y / z } выполняются одновременно. Это аналогично β-редукции в λ-исчислении. Это так важно, я напишу его дважды
Правило Comm:
x̅⟨y⟩.P | x (z) .Q → P | В {г / г}
Правило comm взаимодействует с параллельным составом, ограничением и структурной конгруэнцией:
Параллельная композиция:
Если P → Q, то P | R → Q | Р.
Ограничение:
Если P → Q, то (νx) P → (νx) Q.
Структурная конгруэнтность:
Если P ≡ P ‘, Q ≡ Q’ и P ‘→ Q’, то P → Q.
На некоторых примерах мы должны намочить ноги.
Примеры
(i) x̅⟨y⟩.0 | x (z) .P | Q → P {y / z} | Q
Доказательство. Первые два процесса, x̅⟨y⟩.0 и x (z) .P, сообщают нам
x̅⟨y⟩.0 | x (z) .P → 0 | Р {г / г}
и имеем что 0 | P {y / z} ≡ P {y / z}. Кстати, правило связи взаимодействует с параллельным составом, и теперь мы получаем
x̅⟨y⟩.0 | x (z) .P | Q → P {y / z} | Q
(ii) x̅⟨y⟩.0 | x (u) .P | x (v) .Q не редуцирует однозначно
У нас есть два допустимых сокращения, так как возможны два comms сообщения. Одна редукция возникает из сообщения между первым и вторым членами, т. е. сводится к
P {y / u} | X (V) .Q
и другие результаты от comms между первым и третьим членами, т. е. сводятся к
x (u) .P | В {у / V}
(iii) (νx) (x̅⟨y⟩0 | x (z) .P) | x (u) .Q → P {y / z} | х (и) .Q
Доказательство. Ограничение имени x на первые два члена в параллельной композиции приводит к единственному уменьшению в этом случае, в отличие от предыдущего примера. Здесь имя x, ограниченное (νx), отличается от имени x, входящего в член x (u) .Q. Следовательно, только первые два члена comm, приводящие к уменьшению
P {y / z} | х (и) .Q
(iv) ! x̅⟨y⟩.0 | x (u) .P →! x̅⟨y⟩.0 | Р {у / и}
Доказательство. Мы знаем, что! X̅⟨y⟩.0 ≡! X̅⟨y⟩.0 | x̅⟨y⟩.0, потому что репликация всегда позволяет создать другую копию. Теперь мы имеем связь между x̅⟨y⟩.0 и x (u) .P, которые мы видели, сводится к P {y / u}. Таким образом, мы остались c
! x̅⟨y⟩.0 | Р {у / и}
Подводя итог, π-исчисление является параллельной моделью вычисления, основанной на понятии именования, в котором мы представляем взаимодействия между агентами как передачу сообщений. Эта передача сообщений происходит, когда у нас есть параллельные процессы отправки и получения на одном канале. В π-исчислении мы проводим различие между именами и процессами, и у нас есть возможность одновременно выполнять вычисления. Это основные отличия от λ-исчисления.
Чтобы увидеть полную версию π-исчисления, см. [1]. Мы не обсуждали оператор выбора и нормальные процессы, потому что наше намерение ввести π-исчисление состояло в том, чтобы исследовать параллелизм и как это рассматривается в грамматике.
Целями этой серии статей является ввести читателя в π-исчисления и установить основу для лекций DoCC. Мы достигнем обеих целей со следующей статьей.
РЕКОМЕНДАЦИИ
Милнер, Р. (1991). Полядическое π-исчисление: учебник, 18 августа 2018 г.