Введение
Процессовое исчисление
В теоретической информатике исчисление (или π-исчисление) является процессовым исчислением. Оно позволяет передавать имена каналов по самим каналам, и таким образом способно описывать конкурентные вычисления, сетевая конфигурация которых может изменяться в процессе вычислений. В исчислении немного базовых элементов, и оно представляет собой небольшой, но выразительный язык (см.). Функциональные программы могут быть закодированы в это исчисление, и кодирование подчеркивает диалоговый характер вычислений, устанавливая связь с семантикой игр. Расширения исчисления, такие как spi-исчисление и прикладное π-исчисление, успешно применяются для рассуждений о криптографических протоколах. Помимо первоначального использования в описании конкурентных систем, исчисление также используется для анализа бизнес-процессов и молекулярной биологии. (Точное определение приводится в следующем разделе):
конкурентность, записываемая , где и – два процесса или потока, выполняющиеся одновременно. коммуникация, где префикс ввода – это процесс, ожидающий сообщения, отправленного по каналу связи с именем , прежде чем продолжить работу как , связывая полученное имя с именем . Обычно это моделирует либо процесс, ожидающий коммуникации из сети, либо метку c, используемую только один раз операцией goto c. Префикс вывода описывает, что имя передается по каналу , прежде чем продолжить работу как . Обычно это моделирует либо отправку сообщения в сеть, либо операцию goto c. репликация, записываемая , которую можно рассматривать как процесс, способный всегда создавать новую копию . Обычно это моделирует либо сетевую службу, либо метку c, ожидающую любое количество операций goto c. создание нового имени, записываемое , которое можно рассматривать как процесс выделения новой константы x в пределах . Константы определяются только своими именами и всегда являются каналами связи. Создание нового имени в процессе также называется ограничением. нулевой процесс, записываемый , – это процесс, чье выполнение завершено и остановлено. Хотя минимализм исчисления не позволяет писать программы в обычном смысле, его легко расширить. В частности, легко определить как структуры управления, такие как рекурсия, циклы и последовательное композирование, так и типы данных, такие как функции первого порядка, булевы значения, списки и целые числа. Кроме того, были предложены расширения, учитывающие распределенные вычисления или криптографию с открытым ключом. Прикладное π-исчисление, разработанное Абади и Фурне, формализовало эти различные расширения, расширив исчисление произвольными типами данных.
input prefixing is a process waiting for a message that was sent on a communication channel named before proceeding as , binding the name received to the name Typically, this models either a process expecting a communication from the network or a label c usable only once by a goto c operation. output prefixing describes that the name is emitted on channel before proceeding as Typically, this models either sending a message on the network or a goto c operation. replication, written , which may be seen as a process which can always create a new copy of Typically, this models either a network service or a label c waiting for any number of goto c operations. creation of a new name, written , which may be seen as a process allocating a new constant x within The constants of are defined by their names only and are always communication channels. Creation of a new name in a process is also called restriction. the nil process, written , is a process whose execution is complete and has stopped. Although the minimalism of the calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first order functions, truth values, lists and integers. Moreover, extensions of the have been proposed which take into account distribution or public key cryptography. The applied due to Abadi and Fournet put these various extensions on a formal footing by extending the with arbitrary datatypes.
Маленький пример.
Ниже приведен небольшой пример процесса, состоящего из трех параллельных компонентов. Имя канала x известно только первым двум компонентам. Первые два компонента могут обмениваться сообщениями по каналу x, и имя y связывается со значением z. Следующий шаг процесса заключается в том, что оставшееся y не изменяется, поскольку оно определено во внутренней области видимости. Второй и третий параллельные компоненты теперь могут обмениваться сообщениями по каналу z, и имя v связывается со значением x. Следующий шаг процесса выглядит следующим образом. Обратите внимание, что поскольку локальное имя x было передано по каналу, область видимости x расширяется и охватывает третий компонент. Наконец, канал x может быть использован для отправки имени x. После этого все одновременно выполняющиеся процессы завершаются.
Note that the remaining y is not affected because it is defined in an inner scope. The second and third parallel components can now communicate on the channel name z, and the name v becomes bound to x. The next step in the process is now
Note that since the local name x has been output, the scope of x is extended to cover the third component as well. Finally, the channel x can be used for sending the name x. After that all concurrently executing processes have stopped
Полная версия Тьюринга
Калькуль - это универсальная модель вычислений. Это впервые было замечено Милнером в его статье "Функции как процессы", в которой он представляет два кодирования лямбда-исчисления в калькуле. Одно кодирование имитирует стратегию нетерпеливого (передача по значению) вычисления, а другое – стратегию нормального порядка (передача по имени). В обоих случаях ключевым является моделирование связей окружения – например, "x связано с термом " – как реплицирующих агентов, которые отвечают на запросы о своих связях, отправляя обратно соединение с термом. Особенности калькуля, делающие эти кодирования возможными, – это передача имен и репликация (или, эквивалентно, рекурсивно определенные агенты). Без репликации/рекурсии калькуль перестает быть Тьюринг-полным. Это можно увидеть из того факта, что эквивалентность бисимуляции становится разрешимой для калькуля без рекурсии и даже для калькуля с конечным управлением, где число параллельных компонентов в любом процессе ограничено константой.
The features of the calculus that make these encodings possible are name passing and replication (or, equivalently, recursively defined agents). In the absence of replication/recursion, the calculus ceases to be Turing complete. This can be seen by the fact that bisimulation equivalence becomes decidable for the recursion free calculus and even for the finite control calculus where the number of parallel components in any process is bounded by a constant.
Бисумиляции в калькуле
Что касается исчислений процессов, то данное исчисление позволяет определить эквивалентность бисимуляции. В этом исчислении определение бисимуляционной эквивалентности (также известное как бисимилярность) может основываться либо на редукционной семантике, либо на семантике помеченных переходов. Существует (как минимум) три различных способа определения помеченной бисимуляционной эквивалентности в этом исчислении: ранняя, поздняя и открытая бисимилярность. Это обусловлено тем, что исчисление является исчислением процессов с передачей значений. В остальной части этого раздела будем обозначать и процессами, а – бинарными отношениями над процессами.
Открытая бисимилярность
К счастью, существует третье определение, позволяющее избежать этой проблемы, а именно открытое бисходство, предложенное Сангиорги. Бинарное отношение над процессами является открытой бисимуляцией, если для каждой пары элементов и для каждой подстановки имен и каждого действия, всякий раз, когда , то существует такое , что и . Процессы и называются открыто бисходными, что обозначается как , если пара для некоторой открытой бисимуляции.
Processes and are said to be open bisimilar, written if the pair for some open bisimulation .
Рановая, поздняя и открытая бисимилярия различаются
Раннее, позднее и открытое бисходство различны. Включения строгие, поэтому в некоторых подвычислениях, таких как асинхронный π-исчисление, позднее, раннее и открытое бисходство совпадают. Однако в этом контексте более подходящим понятием является асинхронное бисходство. В литературе термин "открытая бисимуляция" обычно относится к более сложному понятию, где процессы и отношения индексируются отношениями различимости; подробности можно найти в вышеупомянутой статье Сангиорги.
In certain subcalculi such as the asynchronous pi calculus, late, early and open bisimilarity are known to coincide. However, in this setting a more appropriate notion is that of asynchronous bisimilarity. In the literature, the term open bisimulation usually refers to a more sophisticated notion, where processes and relations are indexed by distinction relations; details are in Sangiorgi's paper cited above.
Приложения
Калькуль используется для описания многих различных типов конкурентных систем. Фактически, некоторые из последних применений лежат за пределами традиционной информатики. В 1997 году Мартин Абади и Эндрю Гордон предложили расширение калькуля, исчисление Spi, как формальную нотацию для описания и рассуждений о криптографических протоколах. Spi-калькуль расширяет калькуль примитивами для шифрования и дешифрования. В 2001 году Мартин Абади и Седрик Фурне обобщили обработку криптографических протоколов, создав прикладной калькуль. В настоящее время существует большой объем работ, посвященных вариантам прикладного калькуля, включая ряд экспериментальных инструментов верификации. Одним из примеров является инструмент ProVerif, разработанный Бруно Бланше, основанный на переводе прикладного калькуля в логическую систему программирования Бланше. Другой пример – Cryptyc, разработанный Эндрю Гордоном и Аланом Джеффри, который использует метод соответствия утверждений Ву и Лама в качестве основы для систем типов, способных проверять свойства аутентификации криптографических протоколов. Около 2002 года Говард Смит и Питер Фингар заинтересовались возможностью использования калькуля в качестве инструмента описания для моделирования бизнес-процессов. К июлю 2006 года в сообществе велись дискуссии о потенциальной полезности этого подхода. В последнее время калькуль стал теоретической основой языка моделирования бизнес-процессов (BPML) и Microsoft XLANG. Калькуль также привлек внимание в области молекулярной биологии. В 1999 году Авив Регев и Эхуд Шапиро показали, что можно описать путь клеточной сигнализации (так называемый каскад RTK/MAPK) и, в частности, молекулярный "конструктор", реализующий эти задачи коммуникации, в расширении калькуля. После публикации этой основополагающей работы другие авторы описали всю метаболическую сеть минимальной клетки. В 2009 году Энтони Нэш и Сара Калвала предложили калькульную структуру для моделирования трансдукции сигнала, управляющей агрегацией Dictyostelium discoideum.
История
Рассчет был первоначально разработан Робином Мильнером, Йоахимом Парроу и Дэвидом Уолкером в 1992 году, основываясь на идеях Уффе Энгберга и Могенса Нильсена. Его можно рассматривать как продолжение работы Милнера над процессуальным исчислением CCS (Calculus of Communicating Systems). В своей Тьюринг-лекции Милнер описывает разработку исчисления как попытку отразить единообразие значений и процессов в акторах.