RChain Home_RU
Sep 5, 2018 · 7 min read

ВЫЧИСЛИТЕЛЬНЫЕ ИСЧИСЛЕНИЯ ЧАСТЬ 2: π-исчисления

ОБЗОР

В первом серии статей мы рассмотрели грамматику и оперативную семантику для λ-исчисления.

Наш интерес к π-исчислению заключается в том, что он является предшественником ρ-исчисления. Это модель параллельных вычислений, или, более конкретно, исчисление процесса, основанное на понятии именования. В исчислении процесса мы представляем взаимодействия между независимыми агентами или процессами как передачу сообщений, в отличие от модификаций общих переменных (как в λ-исчислении).

π-исчисление отличается от λ-исчисления различием между именами и процессами и добавлением терминов-конструкторов, включая параллельную композицию, которая отвечает за параллелизм. Таким образом, в π-исчислении, процессах и именах есть два разных объекта и различные взаимодействия между процессами и именами. Однако, как и λ-члены, процессы в π-исчислении строятся из имен.

Параллельная композиция позволяет вычислить в процессах: либо-либо параллельно, либо самостоятельно или же использовать обмен данными по общему каналу. Это применимо для смарт-контрактов, которые используются в приложении, и хранения переходов состояний виртуальной машины.

В этой статье мы обсудим грамматику, структурную конгруэнтность и оперативную семантику π-исчисления.

Πi-исчисление

Здесь мы обсудим упрощенную версию π-исчисления, предложенную Робин Милнер [1].

Грамматика

Представление BNF грамматики для π-исчисления

P,Q ::= 0 | x(y).P | y⟩.P | (𝜈x)P | P|Q | !P (1.1)

Аналогично λ-исчислению, π-исчисление является параметрическим в наборе имен X. Даже не зная, что означают эти операторы, мы уже знаем, что мы можем написать

P[X] ::= 0 | X(X).P[X] | X.P[X] | (𝜈X)P[X] | P[X]|P[X] | !P[X]

чтобы выразить эту зависимость от X явно.

Возвращаясь к (1.1), допустимые члены этой грамматики, т. е. выражения в правой части этого представления, также называются конструкторами термов. Ниже мы обсудим эти терм конструкторы.

Остановленный процесс: 0

P,Q ::= 0 | x(y).P | y.P | (νx)P | P|Q | !P

Этот процесс означает «ничего не делать», т. е. выполнение завершено, и оно прекратилось.
Ввод-сохранение продолжения или префикса ввода: x (y) .P

P,Q ::= 0 | x(y).P | 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

(νx)P — читает “новый x в P” — определяет x как новое имя и связывает его в процессе P.

Параллельная композиция: P | Q

P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P

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 | …; столько копий, сколько пожелаете. Этот процесс всегда может создать новую копию P. Правила сокращения делают так, что нет риска бесконечной параллельной деятельности.

Каждый процесс в π-исчислении построен из остановленного процесса 0. Давайте построим несколько простых процессов.

Несколько простых процессов

  • 0

Это самый простой процесс, из которого создаются все остальные процессы.

  • x(y).0

Этот процесс ожидает сообщения y на канале x, а затем останавливается.

  • y.0

Этот процесс отправляет сообщение y по каналу x, а затем останавливается.

  • (𝜈x)0

Этот процесс объявляет новое имя x в остановленном процессе.

Считаете ли вы, что это должно соответствовать процессу, который у нас уже есть?

  • 0 | 0

Остановленный процесс выполняется одновременно с остановленным процессом.

Считаете ли вы, что это должно соответствовать процессу, который у нас уже есть?

  • y⟩.0 | x(z).0

Этот процесс одновременно отправляет и получает сообщение на канале x. Так происходит общение!

Одновременная отправка и прием сообщений на одном канале позволяет осуществлять связь на этом канале. В общем случае процесс x̅⟨y⟩.P | x (z) .Q соответствует сообщению на канале x. Говорят, что x и x̅ находятся в отношениях имени / со-имени.

Структурная конгруэнтность

Интуитивно мы ожидаем эквивалентность между некоторыми процессами. Например, P | 0, 0 | P и P должны быть эквивалентными. Подумайте об этом.

Процесс P | 0 означает, что мы выполняем процесс P одновременно с остановленным процессом 0. Это не может быть иначе, чем выполнение процесса P само по себе. Вообще говоря, мы обозначаем структурную конгруэнтность процессов P и Q через P ≡ Q. Наши интуиции кодируются следующими аксиомами структурной конгруэнтности.

a-эквивалентность:
P ≡ Q, если Q можно получить из P, переименовав одно или несколько имен, связанных в P (мы обсудим свободные и связанные имена более подробно позже в серии статей). Это аналогично α-превращению в λ-исчислении. Это означает, что две программы эквивалентны, если они отличаются только именами переменных, используемых внутри. Они выполняют один и тот же код, но могут называть вещи разными именами согласованным образом

Аксиомы для параллельной композиции:
- P | Q ≡ Q | п

Порядок, в котором мы перечисляем параллельные процессы, не имеет значения, поскольку они выполняются одновременно. Поэтому процессы P | Q и Q | P эквивалентны.

- (P | Q) | R ≡ P | (Q | R)

Пар оператор должен быть ассоциативным. Мы только говорим о «совместном» двух процессах, поэтому, если мы хотим выпустить третий процесс в микс, есть два разных способа сделать это. Эта эквивалентность говорит, что эти два способа одинаковы, потому что мы одновременно выполняем эти процессы.

- P | 0 ≡ P

Запуск остановленного процесса вместе с другим процессом P не должен отличаться от того, что работает только один процесс. Эта эквивалентность говорит именно об этом. Параллельный процесс с остановленным процессом аналогичен добавлению числа 0.

Аксиомы для ограничения:
- (νx) (νy) P ≡ (νy) (νx) P

При объявлении новых имен в процессе сам порядок не имеет значения. Данная эквивалентность отражает это понятие.

- (νx) 0 ≡ 0

Объявление нового имени в остановленном процессе не должно ничего делать. Поэтому он должен быть эквивалентен остановленному процессу.

Аксиома для репликации:
-! P ≡ P | !П

С репликацией процесса мы всегда можем создать новую копию процесса. Следовательно, процессы! P и P | ! P эквивалентны.

Аксиома, связанная с ограничением и параллелью:

Если имя x связано в Q, то (νx) (P | Q) ≡ (νx) P | Q.

Это свойства структурной конгруэнтности в π-исчислении. Структурная конгруэнтность отражает понятие вычислительной неразличимости. То есть два структурно конгруэнтных процесса идентичны с точки зрения вычислений.

Структурная конгруэнтность является примером того, что называется отношением эквивалентности в математике. Мы рассматриваем его как вычислительную эквивалентность процессов.

Теперь мы будем точно понимать понятие связи в π-исчислении и обсуждать оперативную семантику.

ОПЕРАЦИОННАЯ СЕМАНТИКА, В ТОМ ЧИСЛЕ ПРАВИЛА СОКРАЩЕНИЯ

Напомним, что префикс представляет отправку сообщения y по каналу x, а префикс x (z) представляет прием сообщения z на канале x. Мысль заключается в том, что когда передача и прием по одному и тому же каналу происходят одновременно, происходит обмен данными, и получатель затем использует переданную информацию. В символах это написано

x̅⟨y⟩.P | x (z) .Q → P | В {г / г}

Символ → означает «сокращается до», и мы называем это comm сокращение или comm правило. Это означает, что если мы найдем два процесса x̅⟨y⟩.P и x (z) .Q, выполняющиеся одновременно, то y отправляется по каналу x, y заменяет z в процессе Q, а процессы P и Q (y / z } выполняются одновременно. Это аналогично β-редукции в λ-исчислении. Это так важно, я напишу его дважды

Правило Comm:
x̅⟨y⟩.P | x (z) .Q → P | В {г / г}

Правило comm взаимодействует с параллельным составом, ограничением и структурной конгруэнцией:

Параллельная композиция:
Если P → Q, то P | R → Q | Р.

Ограничение:
Если 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 | Р {г / г}

и имеем что 0 | P {y / z} ≡ P {y / z}. Кстати, правило связи взаимодействует с параллельным составом, и теперь мы получаем

x̅⟨y⟩.0 | x (z) .P | Q → P {y / z} | Q

(ii) x̅⟨y⟩.0 | x (u) .P | x (v) .Q не редуцирует однозначно

У нас есть два допустимых сокращения, так как возможны два comms сообщения. Одна редукция возникает из сообщения между первым и вторым членами, т. е. сводится к

P {y / u} | X (V) .Q

и другие результаты от comms между первым и третьим членами, т. е. сводятся к

x (u) .P | В {у / 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} | х (и) .Q

(iv) ! x̅⟨y⟩.0 | x (u) .P →! x̅⟨y⟩.0 | Р {у / и}

Доказательство. Мы знаем, что! X̅⟨y⟩.0 ≡! X̅⟨y⟩.0 | x̅⟨y⟩.0, потому что репликация всегда позволяет создать другую копию. Теперь мы имеем связь между x̅⟨y⟩.0 и x (u) .P, которые мы видели, сводится к P {y / u}. Таким образом, мы остались c

! x̅⟨y⟩.0 | Р {у / и}

Подводя итог, π-исчисление является параллельной моделью вычисления, основанной на понятии именования, в котором мы представляем взаимодействия между агентами как передачу сообщений. Эта передача сообщений происходит, когда у нас есть параллельные процессы отправки и получения на одном канале. В π-исчислении мы проводим различие между именами и процессами, и у нас есть возможность одновременно выполнять вычисления. Это основные отличия от λ-исчисления.

Чтобы увидеть полную версию π-исчисления, см. [1]. Мы не обсуждали оператор выбора и нормальные процессы, потому что наше намерение ввести π-исчисление состояло в том, чтобы исследовать параллелизм и как это рассматривается в грамматике.

Целями этой серии статей является ввести читателя в π-исчисления и установить основу для лекций DoCC. Мы достигнем обеих целей со следующей статьей.

РЕКОМЕНДАЦИИ
Милнер, Р. (1991). Полядическое π-исчисление: учебник, 18 августа 2018 г.

    RChain Home_RU

    Written by

    Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
    Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
    Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade