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

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

π - исчисление имеет мало терминов и является небольшим, но выразительным языком (см. § Синтаксис). Функциональные программы могут быть закодированы в π -исчислении, и кодирование подчеркивает диалоговую природу вычислений, проводя связи с игровой семантикой . Расширения π -исчисления, такие как spi-исчисление и прикладное π , были успешными в рассуждениях о криптографических протоколах . Помимо первоначального использования для описания параллельных систем, π -исчисление также использовалось для рассуждений о бизнес-процессах ^[1] и молекулярной биологии . ^[2]

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

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

Конструкции процессов, доступные в исчислении, следующие ^[3] (точное определение дано в следующем разделе):

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

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

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

${\displaystyle {\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 . Поэтому следующим шагом в процессе является

${\displaystyle {\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 . Теперь следующим шагом в процессе является

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

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

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

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

${\displaystyle {\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}}}$

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

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

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

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

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

Альфа-преобразование :

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

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

• ${\displaystyle P|Q\equiv Q|P}$
• ${\displaystyle (P|Q)|R\equiv P|(Q|R)}$
• ${\displaystyle P|0\equiv P}$

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

• ${\displaystyle (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\displaystyle (\nu x)0\equiv 0}$

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

• ${\displaystyle !P\equiv P|!P}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle (\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}$

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

${\displaystyle (\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}$

Обратите внимание, что, применяя аксиому замены-редукции, свободные вхождения теперь помечаются как .${\displaystyle y}$${\displaystyle z}$

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

${\displaystyle (\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 расширяется, чтобы охватить и третий компонент. Это было зафиксировано с помощью аксиомы расширения области действия.

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

${\displaystyle (\nu x)(0|0|0)}$

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

${\displaystyle 0}$

В качестве альтернативы можно дать исчислению числа Пи маркированную семантику перехода (как это было сделано с исчислением коммуникационных систем ).
В этой семантике переход из состояния в некоторое другое состояние после действия обозначается как: ${\displaystyle P}$${\displaystyle P'}$${\displaystyle \alpha }$

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

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

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

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

В синтаксис можно добавить оператор недетерминированного выбора . ${\displaystyle P+Q}$

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

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

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

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

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

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

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

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

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

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

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

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

π - исчисление является универсальной моделью вычислений . Это впервые было отмечено Милнером в его статье «Функции как процессы» ^[10] , в которой он представляет две кодировки лямбда-исчисления в π -исчислении. Одна кодировка имитирует стратегию оценки «eager» (вызов по значению) , другая кодировка имитирует стратегию «normal-order» (вызов по имени). В обеих из них решающим пониманием является моделирование привязок среды — например, « x привязан к терму » — как реплицирующихся агентов, которые отвечают на запросы своих привязок, отправляя обратно соединение к терму .${\textstyle M}$${\displaystyle M}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

и

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

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

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

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

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

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

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

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

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

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

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

• Милнер, Робин (1999). Коммуникационные и мобильные системы: π-исчисление . Кембридж, Великобритания: Cambridge University Press. ISBN 0-521-65869-1.
• Милнер, Робин (1993). «Полиадическое π-исчисление: Учебное пособие». В FL Hamer; W. Brauer; H. Schwichtenberg (ред.). Логика и алгебра спецификации . Springer-Verlag.
• Sangiorgi, Davide ; Walker, David (2001). π-исчисление: теория мобильных процессов . Кембридж, Великобритания: Cambridge University Press. ISBN 0-521-78177-9.