Пи-исчисление

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

\pi-исчисление в теоретической информатике  — исчисление процессов, изначально разработанное Робином Милнером, Иоахимом Парровом и Дэвидом Уолкером как продолжение работы над исчислением общающихся систем. Целью \pi-исчисления является возможность описать параллельные вычисления, конфигурация которых может меняться на протяжении вычисления.

Неформальное определение[править | править исходный текст]

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

Конструкции процесса[править | править исходный текст]

Центральным для \pi-исчисления является понятие имени. Простота исчисления заключается в двойной роли имён, которые выступают и как каналы связи и как переменные. В исчислении доступны следующие конструкции процесса (точные определения даны в следующих секциях):

  • конкуренция, обозначается 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. Константы \pi-исчисления определяются только через своё имя и всегда являются каналами связи.
  • ноль процесс, обозначается 0, процесс выполнение которого завершено и остановлено.

Однако минимализм \pi-исчисления не позволяет писать программы в обычном смысле слова, но исчисление может легко расширяться. В частности, просто определить структуры управления (такие как рекурсия, циклы и секвенциальная композиция) и типы данных (такие как функции первого порядка, значения истинности, списки и целые числа). Кроме того, были предложены расширения \pi-исчисления, которые принимают во внимание распределение и криптографию с публичным ключом. Применяется \pi-исчисление благодаря Абади и Фурнье внёсших эти различные дополнения на формальной основе, посредством расширения \pi-исчисления с произвольными типами данных.

Небольшой пример[править | править исходный текст]

Ниже расположен пример процесса, который состоит из трёх параллельных компонент. Канал x известен только из двух первых компонент.


\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}

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


\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}

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


\begin{align}

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

Формальное определение[править | править исходный текст]