π -числение

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

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

Неофициальное определение [ править ]

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

Конструкции процесса [ править ]

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

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

• concurrency , записанный , где и - два процесса или потока, выполняемые одновременно.${\ displaystyle P \ mid Q}$${\ displaystyle P}$${\ displaystyle Q}$
• общение , где
  • префикс ввода - это процесс, ожидающий сообщения, которое было отправлено по каналу связи с именем, прежде чем продолжить как , связывая полученное имя с именем x . Как правило, это моделирует либо процесс, ожидающий связи от сети, либо метку, используемую операцией только один раз .${\ Displaystyle с \ влево (х \ вправо) .P}$${\ displaystyle c}$${\ displaystyle P}$cgoto c
  • префикс output описывает, что имя передается по каналу перед продолжением как . Как правило, это модели отправки сообщения по сети или операции.${\ displaystyle {\ overline {c}} \ langle y \ rangle .P}$${\ displaystyle y}$${\ displaystyle c}$${\ displaystyle P}$goto c
• репликация , записанная , которую можно рассматривать как процесс, который всегда может создать новую копию . Обычно это моделирует либо сетевой сервис, либо метку, ожидающую любого количества операций.${\ Displaystyle! \, P}$${\ displaystyle P}$cgoto c
• создание нового записанного имени , которое можно рассматривать как процесс, выделяющий внутри новую константу x . Константы π -исчисления определяются только своими именами и всегда являются каналами связи. Создание нового имени в процессе также называется ограничением .${\ Displaystyle \ влево (\ ню х \ вправо) P}$${\ displaystyle P}$
• записанный процесс nil - это процесс, выполнение которого завершено и остановлено.${\ 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 (где х и у являются любыми имена из Й): ^[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}$	а ; х ; все свободные имена 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}$if можно получить из , переименовав одно или несколько связанных имен в .${\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 }$

Стандартный результат в отношении помеченной семантики состоит в том, что она согласуется с семантикой редукции в том смысле, что тогда и только тогда, когда для некоторого действия ^{[ необходима ссылка ]} .${\displaystyle P\rightarrow P'}$${\displaystyle P\,{\xrightarrow {\overset {}{\alpha }}}P'}$${\displaystyle \alpha }$

Расширения и варианты [ править ]

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

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

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

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

Полиадические π -исчисление позволяет общаться более чем одно именем в одном действии: (полиадический выход) и (полиадическую вход) . Это полиадическое расширение, которое полезно, особенно при изучении типов для процессов передачи имен, может быть закодировано в монадическом исчислении путем передачи имени частного канала, через который затем последовательно передаются несколько аргументов. Кодировка определяется рекурсивно с помощью предложений${\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}$

Свойства [ править ]

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

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

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

Бисимуляции в π- исчислении [ править ]

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

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

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

Раннее и позднее двойное сходство [ править ]

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

Бинарное отношение над процессами является ранней бисимуляцией , если для каждой пары процессов ,${\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}}$

Открытое двойное сходство [ править ]

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

Бинарное отношение над процессами - это открытая двойная симуляция, если для каждой пары элементов и для каждой подстановки имени и каждого действия всякий раз, когда существует такое, что и .${\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}$

Мы говорим , что и являются колючей bisimilar , если существует колючая бисимуляцию где .${\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) и Microsoft XLANG. ^[13]

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

История [ править ]

Π -исчисления первоначально была разработана Робин Милнер , Joachim Parrow и Дэвид Уокер в 1992 году, основываясь на идеях по Uffe Энгберга и Могенс Nielsen. ^[16] Его можно рассматривать как продолжение работы Милнера по исчислению процессов CCS ( Calculus of Communicating Systems ). В своей лекции Тьюринга Милнер описывает развитие π- исчисления как попытку уловить единообразие ценностей и процессов в акторах. ^[17]

Реализации [ править ]

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

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

Заметки [ править ]

Ссылки [ править ]

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

Внешние ссылки [ править ]

• PiCalculus в вики по C2
• FAQ по я-исчислению от Жаннет М. Крыло