Наш интерес к π-исчислению заключается в том, что оно является предшественником ρ-исчисления. Это модель параллельных вычислений или, точнее, исчисление процессов, основанное на понятии именования. В исчислении процессов мы представляем взаимодействие между независимыми агентами или процессами как передачу сообщений, а не модификации общих переменных (как в λ-исчислении).
π-исчисление отличается от λ-исчисления различием между именами и процессами и добавлением конструкторов терминов, включая параллельную композицию, которая отвечает за параллелизм. Итак, в π-исчислении есть две разные сущности, процессы и имена, а также разные взаимодействия между процессами и именами. Однако, как и λ-термы, процессы в π-исчислении строятся из имен.
Параллельная композиция позволяет вычислениям в процессах либо выполняться параллельно и независимо, либо обмениваться данными по общему каналу. Это полезно для приложений смарт-контрактов и хранения переходов состояний виртуальной машины.
В этом посте мы обсудим грамматику, структурную конгруэнтность и операционную семантику π-исчисления.
π-исчисление
Здесь мы обсудим упрощенную версию π-исчисления, предложенную Робином Милнером [1].
Грамматика
Представление BNF грамматики для π-исчисления
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (𝜈x)P | P|Q | !P (1.1)
очень похоже на λ-исчисление, является параметрическим в наборе имен X. Даже не зная, что означают эти операторы, мы уже знаем, что можем написать
P[X] ::= 0 | X(X).P[X] | X̅⟨X⟩.P[X] | (𝜈X)P[X] | P[X]|P[X] | !P[X]
чтобы явно выразить эту зависимость от X.
Возвращаясь к (1.1), допустимые термы в этой грамматике, т. е. выражения в правой части этого представления, также называются конструкторами термов. Мы обсудим эти конструкторы терминов ниже.
Остановленный процесс: 0
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
Этот процесс представляет собой «ничего не делать», т. е. выполнение завершено и остановлено.
Защищенное вводом продолжение или входной префикс: x(y).P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
Этот процесс ожидает, пока имя, отправленное по каналу x, заменит имя y в процессе P. Это играет аналогичную роль абстракции имени y, λy.P в λ-исчислении, связывая имя y в процессе P. .
Отправьте на канал и выполните или введите префикс вывода: x̅⟨y⟩.P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
Отправляет имя y на канал x в качестве подстановочного имени в процессе с защитой ввода, ожидающем на канале x, а затем запускает P.
Ограничение или создание нового имени: (νx)P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
(νx)P – читать «новый x в P» – определяет x как новое имя и связывает его в процессе P.
Параллельная композиция: P | Вопрос
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
П | Q — читать «P par Q» — означает, что процессы P и Q активны одновременно; они могут действовать независимо или общаться друг с другом.
Репликация: !P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
!P – читается как «bang P» – означает P | П | …; столько копий, сколько пожелаете. Этот процесс всегда может создать новую копию P. Правила сокращения позволяют избежать риска бесконечной параллельной активности.
Каждый процесс в π-исчислении строится из остановленного процесса 0. Давайте построим несколько простых процессов.
0
Это простейший процесс, из которого создаются все остальные процессы.
x(y).0
Этот процесс ожидает сообщения y на канале x и затем останавливается.
x̅⟨y⟩.0
Этот процесс отправляет сообщение y по каналу x и затем останавливается.
(𝜈x)0
Этот процесс объявляет новое имя x в остановленном процессе.
Как вы думаете, это должно соответствовать процессу, который у нас уже есть?
0 | 0
Остановленный процесс выполняется одновременно с остановленным процессом.
Как вы думаете, это должно соответствовать процессу, который у нас уже есть?
x̅⟨y⟩.0 | x(z).0
Этот процесс одновременно отправляет и получает сообщение по каналу x. Так происходит общение!
Одновременная отправка и получение сообщений по одному и тому же каналу позволяет осуществлять связь по этому каналу. В общем случае процесс x̅⟨y⟩.P | x(z).Qсоответствует связи по каналу x. Говорят, что x и x̅ находятся в отношениях имя/совместное имя.
Структурное соответствие
Интуитивно мы ожидаем эквивалентности между некоторыми процессами. Например, P | 0, 0 | P и P должны быть эквивалентны. Подумай об этом.
Процесс Р | 0 означает, что мы запускаем процесс P одновременно с остановленным процессом 0. Это ничем не отличается от запуска процесса P отдельно. Вообще говоря, мы обозначаем структурную конгруэнтность процессов P и Q как P ≡ Q. Наши интуитивные представления кодифицируются следующими аксиомами структурной конгруэнтности.
α-эквивалентность:
P ≡ Q , если Q можно получить из P переименованием одного или нескольких имен, связанных в P (мы более подробно обсудим свободные и связанные имена позже в этой серии). Это аналогично α-преобразованию в λ-исчислении. Это означает, что две программы эквивалентны, если они отличаются только именами переменных, используемых внутри. Они выполняют один и тот же код, но, возможно, последовательно называют вещи разными именами.
Аксиомы параллельной композиции:
– P | Q ≡ Q | P
Порядок, в котором мы перечисляем параллельные процессы, не должен иметь значения, потому что они выполняются одновременно. Следовательно, процессы P | Q и Q | P эквивалентны.
– (P | Q) | R ≡ P | (Q | R)
Оператор par должен быть ассоциативным. Мы всегда говорим только об «объединении» двух процессов вместе, поэтому, если мы хотим добавить в смесь третий процесс, есть два различных способа сделать это. Эта эквивалентность говорит, что эти два способа одинаковы, потому что мы запускаем эти процессы одновременно.
– P | 0 ≡ P
Запуск остановленного процесса вместе с другим процессом P не должен отличаться от запуска P в одиночку. Эта эквивалентность говорит именно об этом. Объединение процесса с остановленным процессом аналогично добавлению числа 0.
Аксиомы ограничения:
– (𝜈x)(𝜈y)P ≡ (𝜈y)(𝜈x)P
При объявлении новых имен в процессе порядок не должен иметь значения. Эта эквивалентность отражает это понятие.
– (𝜈x)0 ≡ 0
Объявление нового имени в остановленном процессе ничего не должно делать. Поэтому он должен быть эквивалентен остановленному процессу.
Аксиома репликации:
– !P ≡ P | !P
При репликации процесса мы всегда можем создать новую копию процесса. Следовательно, процессы !P и P | !P эквивалентны.
Аксиома, касающаяся ограничения и параллельности:
Если имя x связано в Q, то (νx)(P | Q) ≡ (νx)P | В.
Это свойства структурной конгруэнтности в π-исчислении. Структурная конгруэнтность отражает понятие вычислительной неразличимости. То есть два структурно конгруэнтных процесса идентичны с вычислительной точки зрения.
Структурная конгруэнтность является примером того, что в математике называется отношением эквивалентности. Мы рассматриваем это как вычислительную эквивалентность процессов.
Теперь мы уточним понятие коммуникации в π-исчислении и обсудим операционную семантику.
Операционная семантика, т.е. правила редукции
Напомним, что префикс представляет отправку сообщения y по каналу x, а префикс x(z) представляет получение сообщения z по каналу x. Идея заключается в том, что когда отправка и получение по одному и тому же каналу происходят одновременно, происходит связь, и получатель затем использует переданную информацию. Символами это написано
x̅⟨y⟩.P | x(z).Q → P | Q{y/z}
→ — это обозначение для «сводится к», и мы называем это сокращением связи или правилом связи. Это означает, что если мы обнаружим, что два процесса x̅⟨y⟩.P и x(z).Q выполняются одновременно, то y отправляется по каналу x, y заменяет z в процессе Q, а процессы P и Q{y/z } работать одновременно. Это аналогично β-редукции в λ-исчислении. Это так важно, я напишу это дважды
Правило связи:
x̅⟨y⟩.P | x(z).Q → P | Q{y/z}
Правило связи взаимодействует с параллельной композицией, ограничением и структурным соответствием:
Параллельная композиция:
Если P → Q, то P | Р → В | Р.
Ограничение:
Если P → Q, то (𝜈x)P → (𝜈x)Q.
Структурное соответствие:
Если P ≡ P’, Q ≡ Q’ и P’ → Q’, то P → Q.
Мы должны получить наши ноги с некоторыми примерами.
Примеры
(i) x̅⟨y⟩.0 | x(z).P | Q → P{y/z} | Q
Доказательство: первые два процесса, x̅⟨y⟩.0 и x(z).P, сообщатся, чтобы дать нам
x̅⟨y⟩.0 | x(z).P → 0 | P{y/z}
и у нас есть это 0 | P{y/z} ≡ P{y/z}. По тому, как правило comm взаимодействует с параллельной композицией, мы теперь получаем
x̅⟨y⟩.0 | x(z).P | Q → P{y/z} | Q
(ii) x̅⟨y⟩.0 | х(и).Р | x(v).Q не сводится однозначно
У нас есть два действительных сокращения, поскольку есть два возможных сообщения, которые могут произойти. Одна редукция получается в результате связи между первым и вторым членами, т. е. сводится к
P{y/u} | x(v).Q
а другой результат связи между первым и третьим членами, т.е. сводится к
x(u).P | Q{y/v}
(iii) (νx)(x̅⟨y⟩.0 | x(z).P) | x(u).Q → P{y/z} | х(и).Q
Доказательство. Ограничение имени x первыми двумя терминами в параллельной композиции приводит к уникальному сокращению в этом случае, в отличие от предыдущего примера. Здесь имя x, ограниченное (νx), отличается от имени x, входящего в терм x(u).Q. Следовательно, только первые два члена comm приводят к сокращению
P{y/z} | x(u).Q
(iv) !x̅⟨y⟩.0 | x(u).P→ !x̅⟨y⟩.0 | P{y/u}
Доказательство: мы знаем, что !x̅⟨y⟩.0 ≡ !x̅⟨y⟩.0 | x̅⟨y⟩.0, потому что репликация всегда позволяет создать другую копию. Теперь у нас есть связь между x̅⟨y⟩.0 и x(u).P, которая, как мы видели, сводится к P{y/u}. Таким образом, нам остается
!x̅⟨y⟩.0 | P{y/u}
Подводя итог, π-исчисление — это параллельная модель вычислений, основанная на понятии именования, в которой мы представляем взаимодействия между агентами как передачу сообщений. Эта передача сообщений происходит, когда у нас есть параллельные процессы отправки и получения на одном и том же канале. В π-исчислении мы делаем различие между именами и процессами, и у нас есть возможность выполнять вычисления одновременно. Это основные отличия λ-исчисления.
Полную версию π-исчисления см. в [1]. Мы не обсуждали оператор выбора и нормальные процессы, потому что при введении π-исчисления мы намеревались исследовать параллелизм и то, как он обрабатывается в грамматике.
Цели этой серии учебников по вычислительным исчислениям состоят в том, чтобы представить ρ-исчисление и заложить основу для лекций DoCC. Мы достигнем обеих целей в следующей статье.
