Русская Википедия:Пи-исчисление
<math>\pi</math>-исчисление в теоретической информатике — исчисление процессов, изначально разработанное Робином Милнером, Иоахимом Пэрроу и Дэвидом Уокером как продолжение работы над исчислением общающихся систем. Целью <math>\pi</math>-исчисления является возможность описать параллельные вычисления, конфигурация которых может меняться на протяжении вычисления.
Неформальное определение
<math>\pi</math>-исчисление принадлежит к семейству исчислений процессов. Фактически <math>\pi</math>-исчисление как λ-исчисление настолько минимально, что не содержит примитивов, таких как числа, булевы выражения, структуры данных, переменные, функции или операторы управления потоком (например, if-then-else, while).
<math>\pi</math>-исчисление определяет динамически взаимодействующие друг с другом параллельные процессы. Каждый процесс может состоять из одного или нескольких действий, расположенных последовательно или параллельно, а также альтернативно или рекурсивно. Действием может быть отправка или получение данных по каналу. Сообщение от одного процесса другому включает имя канала, который может быть использован для ответа. Имя является переменнойШаблон:Sfn.
Можно также сказать, что <math>\pi</math>-исчисление — это открытая теория, которая зависит от некоторой теории имен. Например, с операционной точки зрения π-исчислении можно представить как процедуру, которая для данной теории имен даёт теорию процессов над этими именами[1].
Конструкции процесса
Центральным для <math>\pi</math>-исчисления является понятие имени. Простота исчисления заключается в двойной роли имён, которые выступают и как каналы связи и как переменные. В исчислении доступны следующие конструкции процесса (точные определения даны в следующих секциях):
- конкуренция, обозначается <math>P \mid Q</math>, где <math>P</math> и <math>Q</math> — два процесса или потока, выполняемых конкурентно.
- связь, где
- префикс ввода <math>c\left(x\right).P</math> — процесс, ожидающий сообщение, отправленное по каналу связи <math>c</math>, перед тем как продолжаться как Шаблон:Nowrap, привязывающий полученное имя к имени Шаблон:Nowrap. Как правило, это моделирует процесс ожидания связи из сети, или метку
c, которую можно использовать с помощью операцииgoto c. - префикс вывода <math>\overline{c} \langle y \rangle.P</math> описывает, что имя <math>y</math> передаётся через канал <math>c</math>, перед тем как продолжаться как Шаблон:Nowrap. Как правило, это моделирует отправку сообщения через сеть или операцию
goto c.
- префикс ввода <math>c\left(x\right).P</math> — процесс, ожидающий сообщение, отправленное по каналу связи <math>c</math>, перед тем как продолжаться как Шаблон:Nowrap, привязывающий полученное имя к имени Шаблон:Nowrap. Как правило, это моделирует процесс ожидания связи из сети, или метку
- репликация, обозначается <math>!\,P</math>, которая может быть рассмотрена как процесс, который может всегда создавать новую копию Шаблон:Nowrap. Как правило, эти модели или сетевой сервис или метка
c, ожидающая любое числоgoto cопераций. - создание нового имени, обозначается <math>\left(\nu x\right)P</math>, которое может быть рассмотрено как процесс, размещающий новую константу <math>x</math> внутри Шаблон:Nowrap. Константы Шаблон:Nowrap определяются только через своё имя и всегда являются каналами связи.
- ноль процесс, обозначается 0, процесс, выполнение которого завершено и остановлено.
Минимализм Шаблон:Nowrap не позволяет писать программы в обычном смысле этого слова, но исчисление можно легко расширить. В частности, просто определить структуры управления (такие как рекурсия, циклы и последовательная композиция) и типы данных (такие как функции первого порядка, значения истинности, списки и целые числа). Кроме того, были предложены расширения Шаблон:Nowrap для криптографии с публичным ключом. Прикладное π-исчисление, разработанное Абади и Фурне, даёт этим различным расширениям π-исчисления формальную основу с помощью произвольных типов данных.
Небольшой пример
Ниже приведён пример процесса из трёх параллельных компонент. Канал <math>x</math> известен только в двух первых компонентах.
- <math>
\begin{align}
& \begin{align}
(\nu x) \; & ( \; \overline{x} \langle z \rangle . \; 0 \\
& | \; x(y). \; \overline{y}\langle x \rangle . \; x(y). \; 0 \; )
\end{align} \\
| \; & z(v) . \; \overline{v}\langle v \rangle . 0
\end{align} </math>
Первые две компоненты способны связываться через канал <math>x</math>, при этом <math>y</math> связывается с <math>z</math>. Следующий шаг процесса:
- <math>
\begin{align}
& \begin{align}
( \nu x) \; ( \; & 0 \\
| \; & \overline{z} \langle x \rangle . \; x(y). \; 0 \; )
\end{align}
\\
| \; & z(v). \; \overline{v}\langle v \rangle . \; 0
\end{align} </math>
В этом примере <math>y</math> не затрагивается, так как он определён во внутренней области видимости. Теперь вторая и третья параллельные компоненты могут связаться через канал <math>z</math>, при этом <math>v</math> связывается с <math>x</math>. Следующий шаг процесса:
- <math>
\begin{align}
(\nu x) ( \; & 0 \\
| \; & x(y). \; 0 \\
| \; & \overline{x}\langle x \rangle . \; 0 \; )
\end{align} </math> Обратите внимание, что, поскольку локальное имя <math>x</math> было выведено, область действия <math>x</math> расширена, чтобы охватить также третью компоненту. Наконец, канал <math>x</math> можно использовать для отправки имени <math>x</math>. После чего все процессы останавливаются.
- <math>
\begin{align}
(\nu x) ( \; & 0 \\
| \; & 0 \\
| \; & 0 )
\end{align} </math>
Формальное определение
Применение
Шаблон:Заготовка раздела <math>\pi</math>-исчисление — один из наиболее популярных формализмов в сообществе управления бизнес-процессами (BPM). Например, популярная литература утверждает (и подвергается критике[2]Шаблон:Sfn), что XLANG, WSCI, BPML, BPEL и WS-CDL основаны на этом исчислении. По крайней мере, свойства <math>\pi</math>-исчисления — порядок вычисления, связи на основе сообщений, мобильность (Шаблон:Lang-en) — могут служить основой для языков BPMШаблон:Sfn.
Другим неожиданным направлением использования <math>\pi</math>-исчисления является моделирование биомолекулярных систем[3].
Пример бизнес-процесса
Следующий пример может дать представление об описании бизнес-процесса при помощи пи-исчисления (перефразирован из Шаблон:Sfn):
- Клиент(заказ,клиент)=
- Шаблон:Overline<клиент>.клиент(блюдо)
- ОфициантПринимаетЗаказ(заказ,заказГотов,заказНеГотов,кухня)=
- заказ(клиент).Шаблон:Overline<заказГотов,заказНеГотов>
- .ОфициантПриноситЕду(заказГотов,заказНеГотов,клиент)
- ОфициантПриноситЕду(заказГотов,заказНеГотов,клиент)=
- заказГотов(блюдо).Шаблон:Overline<блюдо>
- + заказНеГотов(извинения).Шаблон:Overline<извинения>
- Кухня(кухня,заказГотов,заказНеГотов)=
- кухня(заказГотов,заказНеГотов).Шаблон:Overline<"борщ">
- Ресторан=
- (ν зкз,клнт,готов,неГотов,кух)
- Клиент(зкз,клнт)
- | ОфициантПринимаетЗаказ(зкз,готов,неГотов,кух)
- | Кухня(кух,готов,неГотов)
Для данного примера исчисление было расширено оператором выбора (P + Q).
Примечания
Литература
