В теоретической информатике , то π -исчисление (или пи-исчисление ) является процесс исчисления . Π -исчисление позволяет названия каналов , которые будут передаваться по каналам самих, и таким образом , он может описать параллельные вычисления которых конфигурация сети может изменяться в процессе вычислений.
В π- исчислении мало терминов, это небольшой, но выразительный язык (см. § Синтаксис ). Функциональные программы могут быть закодированы в π- исчисление, и кодирование подчеркивает диалоговую природу вычислений, устанавливая связи с семантикой игры . Расширения π- исчисления, такие как spi-исчисление и прикладное π , оказались успешными в рассуждении о криптографических протоколах . Помимо первоначального использования при описании параллельных систем, π- исчисление также использовалось для рассуждений о бизнес-процессах [1] и молекулярной биологии . [2]
Неформальное определение
Π -исчисление принадлежит к семейству процессов исчислений , математических формализмов для описания и анализа свойств параллельного вычисления. Фактически, π- исчисление, как и λ-исчисление , настолько минимально, что не содержит примитивов, таких как числа, логические значения, структуры данных, переменные, функции или даже обычные операторы потока управления (например if-then-else
, while
).
Конструкции процесса
Центральное место в π- исчислении занимает понятие имени . Простота исчисления заключается в двойной роли, которую играют имена как каналы связи и переменные .
В исчислении доступны следующие конструкции процессов [3] (точное определение дается в следующем разделе):
- параллелизм , письменный, где а также два процесса или потока, выполняемые одновременно.
- общение , где
- префикс ввода это процесс, ожидающий сообщения, которое было отправлено по каналу связи с именем прежде чем продолжить как , привязывая полученное имя к имени x . Как правило, это моделирует либо процесс, ожидающий связи от сети, либо метку,
c
используемуюgoto c
операцией только один раз . - префикс вывода описывает, что имя излучается на канале прежде чем продолжить как . Как правило, это модели отправки сообщения по сети или
goto c
операции.
- префикс ввода это процесс, ожидающий сообщения, которое было отправлено по каналу связи с именем прежде чем продолжить как , привязывая полученное имя к имени x . Как правило, это моделирует либо процесс, ожидающий связи от сети, либо метку,
- репликация , написанная, который можно рассматривать как процесс, который всегда может создать новую копию . Как правило, это моделирует либо сетевой сервис, либо метку,
c
ожидающую любого количестваgoto c
операций. - создание нового имени , написанного, который можно рассматривать как процесс, выделяющий новую константу x в. Константы π- исчисления определяются только своими именами и всегда являются каналами связи. Создание нового имени в процессе также называется ограничением .
- нулевой процесс, написанный , это процесс, выполнение которого завершено и остановлено.
Хотя минимализм π- исчисления не позволяет нам писать программы в обычном смысле, его легко расширить. В частности, легко определить как управляющие структуры, такие как рекурсия, циклы и последовательная композиция, так и типы данных, такие как функции первого порядка, значения истинности , списки и целые числа. Более того, были предложены расширения π- исчисления , которые учитывают распределение или криптографию с открытым ключом. Приложенное π -исчисления из - Абади и Ж.Фурнье [1] поместить эти различные расширения на формальной основе посредством расширения π -исчисления с произвольными типами данных.
Небольшой пример
Ниже приведен крошечный пример процесса, который состоит из трех параллельных компонентов. Имя канала x известно только первым двум компонентам.
Первые два компонента могут обмениваться данными по каналу x , и имя y становится привязанным к z . Поэтому следующим шагом в этом процессе является
Обратите внимание, что оставшийся y не изменяется, потому что он определен во внутренней области. Второй и третий параллельные компоненты теперь могут обмениваться данными по имени канала z , а имя v становится привязанным к x . Следующий шаг в этом процессе сейчас
Обратите внимание, что, поскольку локальное имя x было выведено, область действия x расширена, чтобы охватить также третий компонент. Наконец, канал x можно использовать для отправки имени x . После этого все одновременно выполняющиеся процессы остановились.
Формальное определение
Синтаксис
Пусть Χ будет набором объектов, называемых именами . Абстрактный синтаксис для π -исчисления построен из следующей грамматики BNF (где х и у являются любыми имена из Й): [4]
В конкретном синтаксисе ниже префиксы связываются более плотно, чем параллельная композиция (|), а скобки используются для устранения неоднозначности.
Имена связаны конструкциями ограничения и входного префикса. Формально, множество свободных имен процесса в π – исчислении индуктивно определяется таблицей ниже. Набор связанных имен процесса определяется как имена процесса, не входящие в набор свободных имен.
Построить | Бесплатные имена |
---|---|
Никто | |
а ; х ; все свободные имена P | |
а ; свободные имена P за исключением x | |
Все бесплатные имена P и Q | |
Свободные имена P, кроме x | |
Все бесплатные имена P |
Структурное соответствие
Центральным как для семантики редукции, так и для семантики помеченных переходов является понятие структурной конгруэнтности . Два процесса структурно конгруэнтны, если они идентичны по структуре. В частности, параллельная композиция коммутативна и ассоциативна.
Точнее, структурная конгруэнтность определяется как отношение наименьшей эквивалентности, сохраняемое конструкциями процесса и удовлетворяющее:
Альфа-преобразование :
- если можно получить из переименовав одно или несколько связанных имен в .
Аксиомы параллельной композиции :
Аксиомы для ограничения :
Аксиома для репликации :
Аксиома, связывающая ограничение и параллель :
- если x не свободное имя.
Эта последняя аксиома известна как аксиома «расширения области видимости». Эта аксиома является центральной, поскольку она описывает, как связанное имя x может быть вытеснено действием вывода, вызывая расширение области действия x . В случаях, когда x - свободное имя, альфа-преобразование может использоваться для продолжения расширения.
Семантика редукции
Мы пишем если может выполнить шаг вычисления, после которого он теперь . Это редукционное отношение определяется как наименьшее отношение, замкнутое по набору правил редукции.
Основное правило редукции, которое учитывает способность процессов взаимодействовать по каналам, следующее:
- где обозначает процесс в котором бесплатное имя был заменен на свободные вхождения . Если свободное появление происходит в месте, где не будет бесплатным, может потребоваться альфа-преобразование.
Есть три дополнительных правила:
- Если тогда также .
- Это правило гласит, что параллельная композиция не препятствует вычислениям.
- Если , то также .
- Это правило гарантирует, что вычисления могут выполняться без ограничений.
- Если а также а также , то также .
Последнее правило гласит, что структурно конгруэнтные процессы имеют одинаковые редукции.
Повторный пример
Рассмотрим еще раз процесс
Применяя определение семантики редукции, получаем редукцию
Обратите внимание, как, применяя аксиому подстановки редукции, свободное вхождение теперь помечены как .
Далее получаем сокращение
Обратите внимание, что, поскольку локальное имя x было выведено, область действия x расширена, чтобы охватить также третий компонент. Это было зафиксировано с помощью аксиомы расширения области действия.
Далее, используя аксиому подстановки редукции, получаем
Наконец, используя аксиомы параллельной композиции и ограничения, получаем
Помеченная семантика
В качестве альтернативы можно придать пи-исчислению помеченную семантику перехода (как это было сделано с исчислением коммуникационных систем ).
В этой семантике переход из состояния в какое-то другое государство после действия обозначается как:
Где говорится а также представляют процессы и является либо действием ввода , выходное действие , или бесшумное действие τ . [5]
Стандартный результат в отношении помеченной семантики состоит в том, что она согласуется с семантикой редукции в том смысле, что если и только если для какого-то действия [ необходима цитата ] .
Расширения и варианты
Приведенный выше синтаксис минимален. Однако синтаксис можно изменять по-разному.
Оператор недетерминирован выбор можно добавить в синтаксис.
Тест на равенство имен можно добавить в синтаксис. Этот оператор сопоставления может действовать кактогда и только тогда, когда x иодно и то же имя. Точно так же можно добавить оператор несовпадения для неравенства имен . Практические программы, которые могут передавать имена (URL-адреса или указатели), часто используют такую функциональность: для прямого моделирования такой функциональности внутри исчисления часто бывает полезно это и связанные с ним расширения.
Асинхронная π -исчисление [6] [7] допускает только выходы, без суффикса, то есть атомы вывода вида, что дает меньшее исчисление. Однако любой процесс в исходном исчислении может быть представлен меньшим асинхронным π- вычислением с использованием дополнительного канала для имитации явного подтверждения от принимающего процесса. Поскольку выходные данные без продолжения могут моделировать передаваемое сообщение, этот фрагмент показывает, что исходное π- исчисление, которое интуитивно основано на синхронной коммуникации, имеет выразительную асинхронную модель коммуникации внутри своего синтаксиса. Однако недетерминированный оператор выбора, определенный выше, не может быть выражен таким образом, поскольку неохраняемый выбор будет преобразован в защищенный; этот факт был использован для демонстрации того, что асинхронное исчисление строго менее выразительно, чем синхронное (с оператором выбора). [8]
Полиадических π -исчисления позволяет общаться более чем одно имя в одном действии: (полиадический вывод) и (полиадический ввод) . Это полиадическое расширение, которое полезно, особенно при изучении типов для процессов передачи имен, может быть закодировано в монадическом исчислении путем передачи имени частного канала, через который затем последовательно передаются несколько аргументов. Кодировка определяется рекурсивно с помощью предложений
кодируется как
кодируется как
Все остальные конструкции процесса не меняются кодировкой.
В приведенном выше описании обозначает кодировку всех префиксов в продолжении таким же образом.
Полная сила репликации не нужен. Часто рассматривается только дублированный ввод , аксиома структурной конгруэнтности которого .
Реплицированный процесс ввода, такой как можно понимать как серверы, ожидающие вызова на канале x клиентами. Вызов сервера порождает новую копию процесса, где a - это имя, переданное клиентом серверу во время его вызова.
Более высокий порядок π -исчисления может быть определен , где не только имена , но процессы , посылается через каналы. Ключевое правило редукции для случая более высокого порядка:
Здесь, обозначает переменную процесса, которая может быть представлена термином процесса. Санджорджи установил, что способность передавать процессы не увеличивает выразительность π- исчисления: прохождение процесса P можно смоделировать, просто передав вместо этого имя, указывающее на P.
Характеристики
Полнота по Тьюрингу
Π -исчисление является универсальной моделью вычислений . Это впервые заметил Милнер в своей статье «Функции как процессы» [9], в которой он представляет два кодирования лямбда-исчисления в π- исчислении. Одна кодировка имитирует стратегию стремительной оценки (вызов по значению) , другая - стратегию обычного порядка (вызов по имени). В обоих случаях ключевым моментом является моделирование привязок среды - например, « x привязан к термину"- как реплицирующие агенты, которые отвечают на запросы своих привязок, отправляя обратно соединение с термином .
Возможностями π- исчисления, которые делают возможным такое кодирование, являются передача имен и репликация (или, что то же самое, рекурсивно определенные агенты). В отсутствие репликации / рекурсии π- исчисление перестает быть мощным по Тьюрингу . Это можно увидеть по тому факту, что эквивалентность бимоделирования становится разрешимой для исчисления без рекурсии и даже для π- исчисления с конечным управлением, где количество параллельных компонентов в любом процессе ограничено константой. [10]
Бисимуляции в π- исчислении
Что касается исчислений процессов, π -исчисление позволяет определить эквивалентность бимоделирования. В π- исчислении определение эквивалентности бисимуляции (также известной как бисхожесть) может быть основано либо на семантике редукции, либо на семантике помеченного перехода.
Существует (по крайней мере) три различных способа определения меченой бисимуляционной эквивалентности в π- исчислении: раннее, позднее и открытое двусходство. Это проистекает из того факта, что π -вычисление является исчислением процесса передачи значений.
В оставшейся части этого раздела мы позволяем а также обозначают процессы и обозначают бинарные отношения над процессами.
Раннее и позднее двойное сходство
И раннее, и позднее двойное сходство были сформулированы Милнером, Парроу и Уокером в их оригинальной статье о π- исчислении. [11]
Бинарное отношение над процессами - это ранняя двойная симуляция, если для каждой пары процессов,
- в любое время затем для каждого имени есть некоторые такой, что а также ;
- для любого действия, не связанного с вводом , если тогда есть некоторые такой, что а также ;
- и симметричные требования с а также поменялись местами.
Процессы а также считаются ранними бисимилярами, написаны если пара для ранней бисимуляции .
При позднем двойном сходстве переходное совпадение не должно зависеть от передаваемого имени. Бинарное отношениенад процессами - это поздняя бисимуляция, если для каждой пары процессов,
- в любое время тогда для некоторых он считает, что а также для каждого имени y ;
- для любого действия, не связанного с вводом , если подразумевает, что существует некоторая такой, что а также ;
- и симметричные требования с а также поменялись местами.
Процессы а также говорят, что опаздывают, написаны если пара для некоторой поздней бисимуляции .
Оба а также страдают от проблемы, заключающейся в том, что они не являются отношениями конгруэнтности в том смысле, что они не сохраняются всеми конструкциями процесса. Точнее, существуют процессы а также такой, что но . Эту проблему можно решить, рассматривая отношения максимальной конгруэнтности, включенные в а также , известное как ранняя и поздняя конгруэнтность соответственно.
Открытое двойное сходство
К счастью, возможно и третье определение, позволяющее избежать этой проблемы, а именно определение открытого двойного сходства , созданное Санджорджи. [12]
Бинарное отношение над процессами является открытой бисимуляцией, если для каждой пары элементов и при каждой подмене имени и каждое действие , в любое время тогда есть некоторые такой, что а также .
Процессы а также называются открытыми бисквитными, написанными если пара для некоторой открытой бисимуляции .
Различают раннее, позднее и открытое двойное сходство.
Различают раннее, позднее и открытое двойное сходство. Условия содержания в порядке, так что.
Известно, что в некоторых субвычислениях, таких как асинхронное пи-исчисление, позднее, раннее и открытое двойное сходство совпадают. Однако в этом случае более подходящим является понятие асинхронного двойного сходства . В литературе термин открытая бисимуляция обычно относится к более сложному понятию, в котором процессы и отношения индексируются с помощью отношений различия; подробности можно найти в цитированной выше статье Санджорджи.
Колючая эквивалентность
В качестве альтернативы можно определить эквивалентность бисимуляции непосредственно из семантики редукции. Мы пишем если процесс сразу разрешает ввод или вывод по имени .
Бинарное отношение над процессами является бизимуляцией с зазубринами, если это симметричное отношение, удовлетворяющее тому, что для каждой пары элементов у нас есть это
- (1) если и только если для каждого имени
а также
- (2) для каждого сокращения существует редукция
такой, что .
Мы говорим что а также являются бисимиляры с зазубринами, если существует бисимуляция где .
Определяя контекст как π- член с дырой [], мы говорим, что два процесса P и 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
Заметки
- ^ Спецификация OMG (2011). «Модель и нотация бизнес-процессов (BPMN), версия 2.0» , Группа управления объектами . стр.21
- ^ a b Регев, Авив ; Уильям Сильверман; Эхуд Ю. Шапиро (2001). "Представление и моделирование биохимических процессов с использованием алгебры процессов пи-исчисления". Тихоокеанский симпозиум по биокомпьютингу : 459–470.
- ^ Крыло, Жаннетт М. (27 декабря 2002 г.). «FAQ по π-исчислению» (PDF) .
- ^ A Calculus of Mobile Processes part 1 page 10, R. Milner, J. Parrow и D. Walker, опубликованный в Information and Computing 100 (1) pp. 1-40, сентябрь 1992 г.
- ^ Робин Милнер, Коммуникационные и мобильные системы: вычисление числа Пи, Cambridge University Press, ISBN 0521643201 . 1999 г.
- ^ Будоль, Г. (1992). Асинхронность и π- исчисление. Технический отчет 1702, INRIA, София-Антиполис .
- ^ Honda, K .; Токоро, М. (1991). Объектное исчисление для асинхронной связи. ЕКООП 91 . Springer Verlag.
- ^ Паламидесси, Катуша (1997). «Сравнение выразительной силы синхронного и асинхронного пи-исчисления». Труды 24-го симпозиума ACM по принципам языков программирования : 256–265. arXiv : cs / 9809008 . Bibcode : 1998cs ........ 9008P .
- ^ Милнер, Робин (1992). «Функции как процессы» (PDF) . Математические структуры в компьютерных науках . 2 (2): 119–141. DOI : 10.1017 / s0960129500001407 .
- ^ Плотина, Мэдс (1997). «О разрешимости эквивалентностей процессов для пи-исчисления». Теоретическая информатика . 183 (2): 215–228. DOI : 10.1016 / S0304-3975 (96) 00325-8 .
- ^ Milner, R .; Дж. Парроу; Д. Уокер (1992). «Исчисление мобильных процессов» (PDF) . Информация и вычисления . 100 (1): 1–40. DOI : 10.1016 / 0890-5401 (92) 90008-4 .
- ^ Санджорджи, Д. (1996). «Теория бисимуляции для π-исчисления». Acta Informatica . 33 : 69–97. DOI : 10.1007 / s002360050036 .
- ^ «BPML | BPEL4WS: путь конвергенции к стандартному стеку BPM». Документ с изложением позиции BPMI.org. 15 августа 2002 г.
- ^ Кьяруги, Давиде; Пьерпаоло Дегано; Роберто Марангони (2007). «Вычислительный подход к функциональному скринингу геномов» . PLOS Вычислительная биология . 3 (9): 1801–1806. DOI : 10.1371 / journal.pcbi.0030174 . PMC 1994977 . PMID 17907794 .
- ^ Nash, A .; Калвала, С. (2009). «Основное предложение для клеточной локальности Dictyostelium, смоделированное в π-исчислении» (PDF) . CoSMoS 2009 .
- ^ Engberg, U .; Нильсен, М. (1986). "Расчет систем связи с передачей метки" . Серия отчетов DAIMI . 15 (208). DOI : 10,7146 / dpb.v15i208.7559 .
- ^ Робин Милнер (1993). «Элементы взаимодействия: лекция о премии Тьюринга» . Commun. ACM . 36 (1): 78–89. DOI : 10.1145 / 151233.151240 .
Рекомендации
- Милнер, Робин (1999). Коммуникационные и мобильные системы: π-исчисление . Кембридж, Великобритания: Издательство Кембриджского университета. ISBN 0-521-65869-1.
- Милнер, Робин (1993). "Полиадическое π-исчисление: Учебное пособие" . В FL Hamer; В. Брауэр; Х. Швихтенберг (ред.). Логика и алгебра спецификации . Springer-Verlag.
- Санджорджи, Давиде ; Уокер, Дэвид (2001). Π-исчисление: теория мобильных процессов . Кембридж, Великобритания: Издательство Кембриджского университета. ISBN 0-521-78177-9.
Внешние ссылки
- PiCalculus в вики по C2
- FAQ по я-исчислению от Жаннет М. Крыло