π -исчисление

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

В π -исчислении мало терминов, и это небольшой, но выразительный язык (см. § Синтаксис ). Функциональные программы могут быть закодированы в π -исчислении, причем кодирование подчеркивает диалоговый характер вычислений, прорисовывая связи с игровой семантикой . Расширения π -исчисления, такие как SPI-исчисление и прикладное π , оказались успешными в рассуждениях о криптографических протоколах . Помимо первоначального использования при описании параллельных систем, π -исчисление также использовалось для рассуждений о бизнес-процессах. и молекулярная биология .

Неофициальное определение

- исчисление π принадлежит к семейству исчислений процессов , математических формализмов для описания и анализа свойств параллельных вычислений. Фактически, π -исчисление, как и λ-исчисление , настолько минимально, что не содержит примитивов, таких как числа, логические значения, структуры данных, переменные, функции или даже обычные операторы потока управления (такие как if-then-else, while).

Конструкции процесса

Центральное место в π -исчислении занимает понятие имени . Простота исчисления заключается в двойной роли, которую имена играют как каналы связи и переменные .

В исчислении доступны следующие конструкции процесса: (точное определение дано в следующем разделе):

• параллельность , написано $P\mid Q$, где $P$ и $Q$ два процесса или потока выполняются одновременно.
• общение , где
  • входной префикс $c\left(x\right).P$ это процесс, ожидающий сообщения, отправленного по каналу связи с именем $c$ прежде чем продолжить, как $P$, привязывая полученное имя к имени x . Обычно это моделирует либо процесс, ожидающий связи из сети, либо метку. c можно использовать только один раз goto c операция.
  • префикс вывода ${\overline {c}}\langle y\rangle .P$ описывает, что имя $y$ излучается на канале $c$ прежде чем продолжить, как $P$. Обычно это моделирует либо отправку сообщения по сети, либо goto c операция.
• репликация , написанное $!\,P$, который можно рассматривать как процесс, который всегда может создать новую копию $P$. Обычно это моделирует либо сетевую службу, либо метку. c ждем любое количество goto c операции.
• создание нового имени , написанного $\left(\nu x\right)P$, который можно рассматривать как процесс выделения новой константы x внутри $P$. Константы π -исчисления определяются только своими именами и всегда являются каналами связи. Создание нового имени в процессе также называется ограничением .
• нулевой процесс, написанный $0$, — это процесс, выполнение которого завершено и остановлено.

Хотя минимализм π -исчисления не позволяет нам писать программы в обычном смысле этого слова, его легко расширить. В частности, легко определить как структуры управления, такие как рекурсия, циклы и последовательная композиция, так и типы данных, такие как функции первого порядка, значения истинности , списки и целые числа. Более того, были предложены расширения π -исчисления , учитывающие распределение или криптографию с открытым ключом. Прикладное предложенное π -исчисление, Абади и Фурне [1], поставило эти различные расширения на формальную основу, расширив π -исчисление произвольными типами данных.

Небольшой пример

Ниже приведен небольшой пример процесса, состоящего из трех параллельных компонентов. Имя канала x известно только первым двум компонентам.

${\begin{aligned}(\nu x)&\;(\;{\overline {x}}\langle z\rangle .\;0\\&\;|\;x(y).\;{\overline {y}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .0\end{aligned}}$

Первые два компонента могут взаимодействовать по каналу x , и имя y становится привязанным к z . Поэтому следующим шагом в этом процессе является

${\begin{aligned}(\nu x)&\;(\;0\\&\;|\;{\overline {z}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .\;0\end{aligned}}$

Обратите внимание, что оставшийся y не затрагивается, поскольку он определен во внутренней области видимости.Второй и третий параллельные компоненты теперь могут взаимодействовать по имени канала z , а имя v становится привязанным к x . Следующий шаг в этом процессе сейчас

${\begin{aligned}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x}}\langle x\rangle .\;0\;)\end{aligned}}$

локальное имя x Обратите внимание: поскольку выведено , область действия x расширяется и включает также третий компонент. Наконец, канал x можно использовать для отправки имени x . После этого все одновременно выполняющиеся процессы остановились

${\begin{aligned}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{aligned}}$

Формальное определение

Синтаксис

Пусть X — множество объектов, называемых именами . Абстрактный синтаксис - исчисления π построен на основе следующей грамматики BNF (где x и y — любые имена из Χ):

${\begin{aligned}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Receive on channel }}x{\text{, bind the result to }}y{\text{, then run }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,&{\text{Send the value }}y{\text{ over channel }}x{\text{, then run }}P\\&\;|\;P|Q\,\,\,\,\,\,\,\,\,&{\text{Run }}P{\text{ and }}Q{\text{ simultaneously}}\\&\;|\;(\nu x)P\,\,\,&{\text{Create a new channel }}x{\text{ and run }}P\\&\;|\;!P\,\,\,&{\text{Repeatedly spawn copies of }}P\\&\;|\;0&{\text{Terminate the process}}\end{aligned}}$

В конкретном синтаксисе, приведенном ниже, префиксы связаны более тесно, чем параллельная композиция (|), а для устранения неоднозначности используются круглые скобки.

Имена связаны конструкциями ограничения и входного префикса. Формально множество свободных имен процесса в π –исчислении определяется индуктивно с помощью таблицы ниже. Набор связанных имен процесса определяется как имена процесса, которых нет в наборе свободных имен.

Построить	Бесплатные имена
$0$	Никто
${\overline {a}}\langle x\rangle .P$	а ; х ; все свободные имена P
$a(x).P$	а ; свободные имена P, кроме x
$P|Q$	Все свободные имена P и Q
$(\nu x)P$	Свободные имена P, кроме x
$!P$	Все свободные имена P

Структурное соответствие

Центральным элементом как семантики редукции, так и семантики помеченных переходов является понятие структурной конгруэнтности . Два процесса структурно конгруэнтны, если они идентичны с точностью до структуры. В частности, параллельная композиция коммутативна и ассоциативна.

Точнее, структурная конгруэнтность определяется как наименьшее отношение эквивалентности, сохраняемое конструкциями процесса и удовлетворяющее:

Альфа-конверсия :

• $P\equiv Q$ если $Q$ можно получить из $P$ переименовав одно или несколько связанных имен в $P$.

Аксиомы параллельной композиции :

• $P|Q\equiv Q|P$
• $(P|Q)|R\equiv P|(Q|R)$
• $P|0\equiv P$

Аксиомы ограничения :

• $(\nu x)(\nu y)P\equiv (\nu y)(\nu x)P$
• $(\nu x)0\equiv 0$

Аксиома репликации :

• $!P\equiv P|!P$

Аксиома, связывающая ограничение и параллель :

• $(\nu x)(P|Q)\equiv (\nu x)P|Q$ если x не является свободным именем $Q$.

Эта последняя аксиома известна как аксиома «расширения области действия». Эта аксиома является центральной, поскольку она описывает, как связанное имя x может быть выдавлено действием вывода, что приведет к области действия x расширению . В тех случаях, когда x является свободным именем $Q$, альфа-преобразование может использоваться для продолжения расширения.

Семантика сокращения

Мы пишем $P\rightarrow P'$ если $P$ может выполнить шаг вычисления, после чего теперь $P'$.Это соотношение приведения $\rightarrow$ определяется как наименьшее отношение, замкнутое в соответствии с набором правил редукции.

Основное правило сокращения, которое фиксирует способность процессов взаимодействовать через каналы, следующее:

• ${\overline {x}}\langle z\rangle .P|x(y).Q\rightarrow P|Q[z/y]$

где $Q[z/y]$ обозначает процесс $Q$ в котором свободное имя $z$ было заменено свободными появлениями $y$. Если свободное возникновение $y$ происходит в месте, где $z$ не будет бесплатным, может потребоваться альфа-конверсия.

Есть три дополнительных правила:

• Если $P\rightarrow Q$ тогда также $P|R\rightarrow Q|R$.

Это правило гласит, что параллельная композиция не препятствует вычислениям.

• Если $P\rightarrow Q$, тогда также $(\nu x)P\rightarrow (\nu x)Q$.

Это правило гарантирует, что вычисления могут продолжаться с соблюдением ограничений.

• Если $P\equiv P'$ и $P'\rightarrow Q'$ и $Q'\equiv Q$, тогда также $P\rightarrow Q$.

Последнее правило гласит, что структурно конгруэнтные процессы имеют одинаковые сокращения.

Повторный пример

Рассмотрим еще раз процесс

$(\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0$

Применяя определение семантики редукции, получаем редукцию

$(\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0$

Обратите внимание, что, применяя аксиому редукционной замены, свободное появление $y$ теперь помечены как $z$.

Далее мы получаем сокращение

$(\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|x(y).0|{\overline {x}}\langle x\rangle .0)$

локальное имя x Обратите внимание: поскольку выведено , область действия x расширяется и включает также третий компонент. Это было зафиксировано с помощью аксиомы расширения области видимости.

Далее, используя аксиому редукционной замены, получаем

$(\nu x)(0|0|0)$

Наконец, используя аксиомы параллельной композиции и ограничения, мы получаем

$0$

Маркированная семантика

Альтернативно, можно придать пи-исчислению помеченную семантику перехода (как это было сделано с « Исчислением коммуникативных систем »).
В этой семантике переход из состояния $P$ в какое-то другое государство $P'$ после действия $\alpha$ обозначается как:

• $P\,{\xrightarrow {\overset {}{\alpha }}}P'$

Где говорится $P$ и $P'$ представляют процессы и $\alpha$ это либо входное действие $a(x)$, выходное действие ${\overline {a}}\langle x\rangle$, или молчаливое действие τ .

Стандартный результат помеченной семантики состоит в том, что она согласуется с семантикой редукции до структурного соответствия в том смысле, что $P\rightarrow P'$ тогда и только тогда, когда $P\,\xrightarrow {\overset {}{\tau }} \equiv P'$

Расширения и варианты

Синтаксис, приведенный выше, является минимальным. Однако синтаксис может быть изменен различными способами.

Оператор недетерминированного выбора $P+Q$ можно добавить в синтаксис.

Тест на равенство имен $[x=y]P$ можно добавить в синтаксис. Этот оператор сопоставления может действовать как $P$ тогда и только тогда, когда x и $y$ одно и то же имя.Аналогичным образом можно добавить оператор несоответствия для неравенства имен . Практические программы, которые могут передавать имена (URL-адреса или указатели), часто используют такую ​​функциональность: для непосредственного моделирования такой функциональности внутри исчисления это и связанные с ним расширения часто бывают полезны.

Асинхронное π - исчисление допускает только выходные данные без продолжения, т.е. выходные атомы формы ${\overline {x}}\langle y\rangle$, что дает меньшее исчисление. Однако любой процесс в исходном исчислении может быть представлен меньшим асинхронным π -исчислением, использующим дополнительный канал для имитации явного подтверждения от принимающего процесса. Поскольку вывод без продолжения может моделировать сообщение в пути, этот фрагмент показывает, что исходное π- исчисление, интуитивно основанное на синхронной коммуникации, имеет внутри своего синтаксиса выразительную модель асинхронной связи. Однако определенный выше оператор недетерминированного выбора не может быть выражен таким образом, поскольку незащищенный выбор будет преобразован в защищенный; этот факт был использован для демонстрации того, что асинхронное исчисление строго менее выразительно, чем синхронное (с оператором выбора).

Полиадическое π - исчисление позволяет сообщить более одного имени за одно действие: ${\overline {x}}\langle z_{1},...,z_{n}\rangle .P$ (полиадический выход) и $x(z_{1},...,z_{n}).P$ (полиадический вход) . Это полиадическое расширение, которое особенно полезно при изучении типов процессов передачи имен, может быть закодировано в монадическом исчислении путем передачи имени частного канала, через который затем последовательно передаются несколько аргументов. Кодировка определяется рекурсивно с помощью предложений

${\overline {x}}\langle y_{1},\cdots ,y_{n}\rangle .P$ кодируется как $(\nu w){\overline {x}}\langle w\rangle .{\overline {w}}\langle y_{1}\rangle .\cdots .{\overline {w}}\langle y_{n}\rangle .[P]$

$x(y_{1},\cdots ,y_{n}).P$ кодируется как $x(w).w(y_{1}).\cdots .w(y_{n}).[P]$

Все остальные конструкции процесса при кодировании остаются неизменными.

В приведенном выше $[P]$ обозначает кодировку всех префиксов в продолжении $P$ таким же образом.

Полная мощь репликации $!P$ не нужен. Часто учитывают только реплицируемый ввод. $!x(y).P$, аксиома структурного сравнения которого равна $!x(y).P\equiv x(y).P|!x(y).P$.

Реплицированный процесс ввода, такой как $!x(y).P$ можно понимать как серверы, ожидающие на канале x, который будет вызываться клиентами. Вызов сервера порождает новую копиюпроцесс $P[a/y]$, где a — имя, переданное клиентомсервер во время его вызова.

, более высокого порядка Можно определить π -исчисление в котором по каналам передаются не только имена, но и процессы.Ключевое правило приведения для случая более высокого порядка:

${\overline {x}}\langle R\rangle .P|x(Y).Q\rightarrow P|Q[R/Y]$

Здесь, $Y$ обозначает переменную процесса , экземпляр которой может быть создан термином процесса. Санджорджиустановлено, что возможность прохождения процессов неповысить выразительность π -исчисления: прохождение процесса P можномоделируется путем простой передачи имени, указывающего P. на

Свойства

Полнота по Тьюрингу

- исчисление π является универсальной моделью вычислений . Впервые это заметил Мильнер в своей статье «Функции как процессы». в котором он представляет две кодировки лямбда-исчисления в π -исчислении. Одна кодировка имитирует нетерпеливую стратегию оценки (вызов по значению) , другая кодировка имитирует стратегию нормального порядка (вызов по имени). В обоих случаях решающим моментом является моделирование привязок среды – например, « x привязан к терму». ${\textstyle M}$" – как реплицирующиеся агенты, которые отвечают на запросы своих привязок, отправляя обратно соединение с термином $M$.

Особенности π -исчисления, которые делают возможным такое кодирование, — это передача имен и репликация (или, что то же самое, рекурсивно определенные агенты). В отсутствие репликации/рекурсии π -исчисление перестает быть Тьюринг-полным. Об этом можно судить по тому факту, что эквивалентность бисимуляции становится разрешимой для безрекурсивного исчисления и даже для π -исчисления с конечным управлением, где число параллельных компонентов в любом процессе ограничено константой.

в π -

См. также: Бисимуляция

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

Существует (по крайней мере) три разных способа определения помеченной бисимуляционной эквивалентности в π -исчислении: раннее, позднее и открытое биподобие. Это связано с тем, что π -исчисление представляет собой исчисление процесса передачи значений.

В оставшейся части этого раздела мы позволяем $p$ и $q$ обозначают процессы и $R$ обозначают бинарные отношения над процессами.

Раннее и позднее бисходство

Раннее и позднее биподобие были сформулированы Милнером, Пэрроу и Уокером в их оригинальной статье о π -исчислении.

Бинарное отношение $R$ над процессами является ранней бисимуляцией , если для каждой пары процессов $(p,q)\in R$,

• в любое время $p\,{\xrightarrow {a(x)}}\,p'$ тогда для каждого имени $y$ существует какой-то $q'$ такой, что $q\,{\xrightarrow {a(x)}}\,q'$ и $(p'[y/x],q'[y/x])\in R$;
• для любого действия, не связанного с вводом данных $\alpha$, если ${p{\xrightarrow {\overset {}{\alpha }}}p'}$ тогда существует некоторый $q'$ такой, что $q{\xrightarrow {\overset {}{\alpha }}}q'$ и $(p',q')\in R$;
• и симметричные требования с $p$ и $q$ поменялись местами.

Процессы $p$ и $q$ считаются ранними бисходными, написанными $p\sim _{e}q$ если пара $(p,q)\in R$ для некоторой ранней бисимуляции $R$.

В позднем бисходстве совпадение перехода должно быть независимым от передаваемого имени.Бинарное отношение $R$ overprocesses — это поздняя бисимуляция , если для каждой пары процессов $(p,q)\in R$,

• в любое время $p{\xrightarrow {a(x)}}p'$ тогда для некоторых $q'$ он утверждает, что $q{\xrightarrow {a(x)}}q'$ и $(p'[y/x],q'[y/x])\in R$ для каждого имени y ;
• для любого действия, не связанного с вводом данных $\alpha$, если $p{\xrightarrow {\overset {}{\alpha }}}p'$ подразумевает, что существует некоторый $q'$ такой, что $q{\xrightarrow {\overset {}{\alpha }}}q'$и $(p',q')\in R$;
• и симметричные требования с $p$ и $q$ поменялись местами.

Процессы $p$ и $q$ называются поздними бисходными, написанными $p\sim _{l}q$ если пара $(p,q)\in R$ для какой-то поздней бисимуляции $R$.

Оба $\sim _{e}$ и $\sim _{l}$ страдают от проблемы, состоящей в том, что они не являются отношениями конгруэнтности в том смысле, что они не сохраняются всеми процессуальными конструкциями. Точнее, существуют процессы $p$ и $q$ такой, что $p\sim _{e}q$ но $a(x).p\not \sim _{e}a(x).q$. Эту проблему можно решить, рассмотрев отношения максимального сравнения, включенные в $\sim _{e}$ и $\sim _{l}$, известные как ранняя конгруэнтность и поздняя конгруэнтность соответственно.

Открытое бисходство

К счастью, возможно третье определение, которое позволяет избежать этой проблемы, а именно определение открытого биподобия , предложенное Санджорджи.

Бинарное отношение $R$ над процессами является открытой бисимуляцией , если для каждой пары элементов $(p,q)\in R$ и для каждой замены имени $\sigma$ и каждое действие $\alpha$, в любое время $p\sigma {\xrightarrow {\overset {}{\alpha }}}p'$ тогда существует некоторый $q'$ такой, что $q\sigma {\xrightarrow {\overset {}{\alpha }}}q'$ и $(p',q')\in R$.

Процессы $p$ и $q$ называются открытыми биподобными, написанными $p\sim _{o}q$ если пара $(p,q)\in R$ для некоторой открытой бисимуляции $R$.

Различают раннее, позднее и

Различают раннее, позднее и открытое бисходство. Условия содержания правильные, поэтому $\sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}$.

Известно, что в некоторых субисчислениях, таких как асинхронное пи-исчисление, позднее, раннее и открытое биподобие совпадают. Однако в данном случае более подходящим понятием является асинхронное биподобие .В литературе термин «открытая бисимуляция» обычно относится к более сложному понятию, в котором процессы и отношения индексируются отношениями различия; подробности можно найти в статье Санджорджи, цитированной выше.

эквивалентность

Альтернативно, можно определить эквивалентность бисимуляции непосредственно из семантики редукции. Мы пишем $p\Downarrow a$ если процесс $p$ немедленно разрешает ввод или вывод по имени $a$.

Бинарное отношение $R$ над процессами является колючей бисимуляцией, если это симметричное отношение, которое удовлетворяет тому, что для каждой пары элементов $(p,q)\in R$ у нас есть это

(1) $p\Downarrow a$ тогда и только тогда, когда $q\Downarrow a$ на каждое имя $a$

и

(2) для каждого сокращения $p\rightarrow p'$ существует сокращение $q\rightarrow q'$

такой, что $(p',q')\in R$.

Мы говорим, что $p$ и $q$ являются зазубренными биподобными, если существует зазубренная бисимуляция $R$ где $(p,q)\in R$.

Определяя контекст как π- термин с дыркой [], мы говорим, что два процесса P и Q конгруэнтны , записываются $P\sim _{b}Q\,\!$, если для каждого контекста $C[]$ у нас есть это $C[P]$ и $C[Q]$ колючие, разноподобные. Оказывается, колючая конгруэнтность совпадает с конгруэнтностью, вызванной ранним бисходством.

Приложения

π - исчисление использовалось для описания множества различных типов параллельных систем. Фактически, некоторые из новейших приложений выходят за рамки традиционной информатики.

В 1997 году Мартин Абади и Эндрю Гордон предложили расширение π -исчисления, Spi-исчисление, в качестве формальной записи для описания и рассуждений о криптографических протоколах. Спи-исчисление расширяет π -исчисление примитивами для шифрования и дешифрования. В 2001 году Мартин Абади и Седрик Фурне обобщили обработку криптографических протоколов для создания прикладного π- исчисления. В настоящее время существует большой объем работ, посвященных вариантам прикладного π -исчисления, включая ряд экспериментальных инструментов проверки. Одним из примеров является инструмент ProVerif [2] Бруно Бланше, основанный на переводе прикладного π -исчисления в структуру логического программирования Бланше. Другим примером является Cryptyc [3] , созданный Эндрю Гордоном и Аланом Джеффри, который использует метод утверждений соответствия Ву и Лама в качестве основы для систем типов, которые могут проверять свойства аутентификации криптографических протоколов.

Примерно в 2002 году Говард Смит и Питер Фингар заинтересовались тем, что π -исчисление станет инструментом описания для моделирования бизнес-процессов. К июлю 2006 года в сообществе началась дискуссия о том, насколько это будет полезно. Совсем недавно π -исчисление сформировало теоретическую основу языка моделирования бизнес-процессов (BPML) и Microsoft XLANG.

π - исчисление также вызвало интерес в молекулярной биологии. В 1999 году Авив Регев и Эхуд Шапиро показали, что можно описать клеточный сигнальный путь (так называемый каскад RTK / MAPK ) и, в частности, молекулярное «лего», которое реализует эти задачи коммуникации в расширении π -исчисления. После этой плодотворной статьи другие авторы описали всю метаболическую сеть минимальной клетки. В 2009 году Энтони Нэш и Сара Калвала предложили систему π -исчисления для моделирования передачи сигнала, которая управляет агрегацией Dictyostelium discoideum .

История

π - исчисление было первоначально разработано Робином Милнером , Иоахимом Пэрроу и Дэвидом Уокером в 1992 году на основе идей Уффе Энгберга и Могенса Нильсена. Его можно рассматривать как продолжение работы Милнера по исчислению процессов CCS ( Исчисление коммуникационных систем ). В своей лекции Тьюринга Милнер описывает развитие π -исчисления как попытку уловить единообразие ценностей и процессов у акторов.

Реализации

Следующие языки программирования реализуют π -исчисление или один из его вариантов:

• Язык моделирования бизнес-процессов (BPML)
• Оккам-π
• Пикт
• JoCaml (на основе Join-исчисления )
• РоЛанг

Ссылки

• Милнер, Робин (1999). Коммуникационные и мобильные системы: π-исчисление . Кембридж, Великобритания: Издательство Кембриджского университета. ISBN  0-521-65869-1 .
• Милнер, Робин (1993). «Полиадическое π-исчисление: Учебное пособие» . Во Флориде Хамер; В. Брауэр; Х. Швихтенберг (ред.). Логика и алгебра спецификации . Спрингер-Верлаг.
• Санджорджи, Давиде ; Уокер, Дэвид (2001). π-исчисление: теория мобильных процессов . Кембридж, Великобритания: Издательство Кембриджского университета. ISBN  0-521-78177-9 .