ВЫЧИСЛИТЕЛЬНЫЕ ИСЧИСЛЕНИЯ ЧАСТЬ 3: RHO-ИСЧИСЛЕНИЯ

RChain Home_RU
Sep 5, 2018 · 11 min read

Обзор

В предыдущем посте мы рассмотрели, что π-исчисление — это исчисление процесса, которое зависит от теории имен; поэтому говорят, что это не замкнутая теория. Rho-исчисление представляет собой асинхронное исчисление передачи сообщений, основанное на понятии цитирования; это замкнутая теория, так как теория имен целиком определяется теорией процессов. Имя ρ-исчисление или Rho-исчисление является акронимом для рефлексивного исчисления высшего порядка. Под рефлексивным мы подразумеваем механизм переключения между именами и процессами (цитата / разыменование, см. ниже). Под более высоким порядком мы имеем в виду, что результирующий язык очень выразителен.

Это последний пост в серии праймеров. Последующие посты будут посвящены лекциям DoCC.

ρ-исчисление

Исходя из π-исчисления, ρ-исчисление может показаться немного похожим на переход в зону сумерек. В π-исчислении имена и процесс были двумя различными дихотомиями. Однако в p-исчислении мы имеем конструкторы для превращения процесса в имя и наоборот. Основная идея состоит в том, что процессы — это программы, а так как имена называются процессами, имена представляют собой код процесса. Таким образом, можно запустить процесс, то есть выполнить программу, процитировать процесс для объединения своего кода, отправить код на другой канал и разыменовать код, чтобы получить исполняемый экземпляр программы.

Как и в π-исчислении, в ρ-исчислении мы представляем взаимодействие между агентами путем передачи сообщений.

ГРАММАТИКА

Представление BNF грамматики для ρ-исчисления, написанное в стиле Rholang,

P, Q :: = 0 | для (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

имеет несколько сходств с π-исчислением. Остановленный процесс, отправка, получение и параллельная композиция имеют аналоги в ρ-исчислении. Тем не менее, это отличительный признак, которые отличают его. Возможность процитировать процесс в имени и различие имени в процессе повышает выразительность ρ-исчисления.

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

P, Q :: = 0 | для (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

Это атомный процесс, который означает «ничего не делать». Все члены в ρ-исчислении построены из этого специального процесса аналогично тому, как термины в λ-исчислении и π-исчислении построены из имен. Главное отличие состоит в том, что нам больше не требуется набор имен, чтобы заставить мяч катиться с нашими попытками сформировать термины. Остановленного процесса достаточно, чтобы выполнить эту работу.

  • Для понимания: for (y ← x) P

P, Q :: = 0 | for (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

Этот процесс похож на восстановление, которое защищено входными данными, x(y).P, в π-исчислении. Этот процесс ожидает получения сообщения на канале x, тогда процесс P будет запускаться с полученным именем, которое будет заменено именем y. см. comm правило ниже.

  • Отправить по каналу x: x! (P)

P, Q :: = 0 | для (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

Цитируемый процесс @P отправляется по каналу x. Это аналогично префиксу вывода, x̅⟨y⟩.P, в π-исчислении, за исключением того, что теперь мы можем восстановить наши сообщения как процессы с использованием разыменования.

  • Параллельный состав процессов: P | Q

P, Q :: = 0 | для (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

Процессы P и Q выполняются одновременно, точно так же, как и в π-исчислении.

  • Разница («падение имени») или выражение: * x

P, Q :: = 0 | для (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

* x — читать «drop x» — позволяет нам превратить имя обратно в его основной процесс (поскольку каждое имя — это цитируемый процесс). Чтобы превратить имя @P в его основной процесс, разыменуйте его.

  • Имена называются процессами: @P

P, Q :: = 0 | для (y ← x) P | x! (P) | P | Q | *x

x, y :: = @P

Каждое имя — это цитируемый процесс. Идея состоит в том, что имена — это компьютерный код, а процессы — это компьютерные программы; код статический, программы выполняются. Учитывая программу (процесс), мы можем записать ее код (цитата), и как только у нас будет код (имя — это цитируемый процесс), мы можем выполнить программу (разыменовать ее). Поэтому мы будем считать процесс *@P таким же, как процесс P. Это является следствием семантической подстановки.

Нам дается остановленный процесс, 0, для начала. Из этого процесса мы строим все имена и процессы в ρ-исчислении. Построим несколько простых процессов ρ-исчисления, прежде чем перейти к структурной конгруэнтности, другим понятиям эквивалентности, синтаксическим и семантическим заменам и оперативной семантике.

  • 0

Это самый простой процесс. Ничего не произошло.

  • * 0

Это не верный синтаксис — только имена могут быть разыменованы, а 0 — процесс, а не имя. Это не является корректным процессом p-исчисления!

  • 0 | 0

Это, возможно, второй простейший процесс; он одновременно запускает остановленный процесс сам с собой. Должны ли мы быть в состоянии упростить этот процесс?

  • * @ 0

Поскольку 0 — простейший процесс, @0 — простейшее имя. Этот процесс разделяет имя @0. Должны ли мы упростить этот процесс?

  • @ (0 | 0)! (0)

Так как 0 | 0 — процесс, @(0 | 0) — это имя, которое предоставляет канал для отправки сообщений. Этот процесс отправляет сообщение @0 на канал @(0 | 0).

  • для (@ (0 | 0) ← @ 0) 0

Этот процесс ожидает сообщения на канале @0. Когда он получен, он заменяет полученное имя для @(0 | 0) в процессе 0.

  • @ 0! (0) | для (@ 0 ← @ 0) 0

Этот процесс одновременно отправляет и получает сообщение @0 на канале @0. Как и в π-исчислении, это приведет к общению!

  • @ (@ 0! (0))! (0)

Поскольку @0! (0) — процесс, мы можем процитировать его, чтобы сформировать имя @(@0!(0)), которое дает нам еще один канал для отправки сообщений. Этот процесс отправляет имя @0 на канал @(@ 0! (0)).

  • для (@ 0 ← @ (0 | 0)) @ 0! (0)

Этот процесс ожидает сообщения на канале @(0 | 0), чтобы заменить имя @0 в процессе @0! (0).

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

ПРЕДЛОЖЕНИЯ ЭКВИВАЛЕНТНОСТИ

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

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

P | 0 ≡ P

P | Q ≡ Q | п

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

Структурная конгруэнтность относится к процессам, а не к именам.

Обозначение эквивалентности

Обозначение эквивалентности, обозначаемое ≡N, имеет два экземпляра, относящихся к (i) одному имени и (ii) структурно конгруэнтным процессам:

(i) @ (* x) ≡N x

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

(ii) Если P ≡ Q, то @P ≡N @Q.

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

α-эквивалентности

Напомним понятие α-преобразования в λ-исчислении. Сказано, что два члена эквивалентны, если они отличаются только их связанными именами, т. е. они отличаются только тем, что мы называем переменными в этом члене. Существует аналогичное понятие, называемое α-эквивалентностью, обозначаемое ≡α, в ρ-исчислении (а также π-исчисление). Два процесса ρ-исчисления называются α-эквивалентными, если они отличаются только тем, что они называют именами, на которые они ссылаются. То есть P ≡α Q, если P и Q отличаются только именами, используемыми для построения этих процессов. Несколько примеров α-эквивалентных процессов:

x! (0) ≡α y! (0),

P | для (y ← x) 0 ≡α P | для (w ← u) 0.

Два α-эквивалентных процесса имеют один и тот же код, поэтому оба они представляют одну и ту же программу

ЗАМЕЩЕНИЯ И ОПЕРАЦИОННАЯ СЕМАНТИКА

Как и в других вычислительных исчислениях, мы имеем правила для подстановок и что эти подстановки означают в терминах вычисления, т. е. правила comm. Мы будем обозначать замену имени y для имени x в процессе P на (P) {y / x}.

Синтаксическая замена

Правила синтаксических подстановок (замен) определяют, что подстановка имен переводится как замена процессов (поскольку процессы построены из 0 и имен). На уровне имен замена выполняется прямо, но мы должны построить концепцию замещения имени в процессе. Таким образом, у нас есть правило для каждого конструктора термов. Правила замены имен в процессах построены из:

  • (0) {@ Q / @ P} = 0

Любая замена имен в остановленном процессе не изменяет остановленный процесс;

  • (! R) {@ Q / @ P} =! (R) {@ Q / @ P}

Существует только один процесс для замещения в репликации, и это происходит очевидным образом, мы реплицируем замещенный процесс;

  • (R | S) {@ Q / @ P} = (R) {@ Q / @ P} | (S) {@ Q / @ Р}

Подстановка в параллельных процессах — это просто замена в каждом процессе отдельно, затем замещенные процессы запускаются параллельно;

  • (x) (R)) {@ Q / @ P} = (x) {@ Q / @ P}! ((R) {@ Q / @ P})

Замещение в отправке работает так, как ожидалось. Во-первых, мы делаем соответствующую подстановку с именем канала x; это объясняет появление (x) {@ Q / @ P}, нового канала для отправки сообщения. Затем мы выполняем соответствующую замену процессом R; это объясняет появление (R) {@ Q / @ P}, нового сообщения для отправки по каналу;

  • (для (y ← x) R) {@ Q / @ P} = для (z ← (x) {@ Q / @ P}) ((R) {z / y}) {@ Q / @ P}

Это правило выглядит очень сложным, поэтому давайте рассмотрим его. Во-первых, мы заменяем имя принимающим каналом x; это объясняет появление (x) {@ Q / @ P} внутри выражения. Затем мы вызываем сообщение, которое мы ожидаем, y, под другим именем, z. Поскольку мы заменили эту метку, мы должны подставить z для каждого вида y в процессе R, следовательно, появляется (R) {z / y}. В конечном счете, нам нужно сделать замену имен внутри процесса (R) {z / y}; это объясняет появление ((R) {z / y}) {@ Q / @ P};

  • (* x) {@ Q / @ P} = * @ Q, если x ≡N @P, * x в противном случае

Замена с разыменованным именем выполняется прямо. Если имя x является именем, эквивалентным @P, то мы ожидаем подстановку, т. е. @Q заменяется на x. Если x не является именем, эквивалентным @P, ничего не меняется;

Обычная замена имени происходит по правилу

(x) {@ Q / @ P} = @Q, если x ≡N @P, x в противном случае.

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

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

Семантическая замена

Настоящий особый вкус исходит из понятия семантической замены. Мы обсуждали процессы цитирования и разыменования имен, что цитирование процесса приводит к имени, и как разыменование имени приводит к процессу, но мы явно не связывали эти две идеи.

Формально мы имеем правило

(* x) {@ Q / @ P} = Q, если x ≡N @P, * x в противном случае,

в котором говорится, что если мы заменим имя @Q на имя @P в процессе разыменования *x, то мы получим процесс Q, если x является именем, эквивалентным @P, и просто игнорируем подстановку вообще, если x не является эквивалентом имени .

Это именно то, что нам нужно, чтобы мы могли думать о процессах как о программах и именах как о коде. Мы хотим иметь возможность принять программу (процесс), записать ее код (указать процесс), затем запустить код в виде программы (разыменовать цитируемый процесс) и вернуть исходную программу (процесс). Семантическая подстановка объединяет все это.

Операционная семантика

У нас также есть понятие comm-события в ρ-исчислении. Идея заключается в том, что у нас есть связь, когда мы одновременно отправляем и получаем по одному каналу данные. Коммуникация — это сокращение процесса формы

x! (Q) | для (z ← x) P → (P) {@ Q / z}.

Мы распространяем это понятие коммуникации с использованием эквивалентности имен. Это сводится к тому, что сообщение обобщается на одновременную отправку и получение сообщений по эквивалентным каналам имен.

  • Comm правило: Если x ≡N y, то мы имеем правило сокращения

x! (Q) | для (z ← y) P → (P) {@ Q / z}

В этом правиле говорится, что параллельная передача x0! (Q) и принимает для (z ← y) P по эквивалентным каналам имен x и y сводится к замещенному процессу (P) {@ Q / z}. Правило связи позволяет агентам синхронизировать и связывать процессы, упакованные как имена.

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

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

Это правило гласит, что если процесс P сводится к процессу P ‘, то процесс P | Q будет уменьшаться до процесса P ‘| Q.

  • Структурная конгруэнтность: если P ≡ P ‘, Q ≡ Q’ и P ‘→ Q’, то P → Q.

Это правило гласит, что если у нас есть процесс P, который структурно конгруэнтен процессу P’, то процесс Q, структурно конгруэнтный процессу Q’, и процесс P’ сводится к процессу Q’, то процесс P уменьшает к процессу Q.

Пришло время для нескольких примеров сокращения.

Примеры

@ 0! (0) | для (@ (@ 0! (0)) ← @ 0) 0 → 0

Отправьте @ 0! (0) и получите, для (@ 0 ← @ 0) 0, процессы запускаются одновременно на одном канале, @ 0. Таким образом, возникает comm-событие, и этот процесс сводится к замене

(0) {@ 0 / @ (@ 0! (0))}.

Напомним, что (0) {z / y} = 0 для любых имен y, z, поэтому процесс в конечном счете упрощает остановленный процесс 0.

для (@ 0 ← x) @ 0! (0) | x! (@ 0! (0)) → @ (@ 0! (0))! (0)

Во-первых, мы замечаем, что мы отправляем и получаем сообщения на одном канале х, поэтому происходит общение. Чтобы упростить ситуацию, сделаем B, поэтому процесс, с которым мы имеем дело, можно переписать как

для (@ 0 ← x) P | х! (Q).

Используя правило comm (здесь z = @ 0), это сводится к

(Р) {@ Q / @ 0}.

Используя определения Р и Q, имеем

(@ 0! (0)) {@ (@ 0! (0)) / @ 0}

и используя синтаксическое правило замены для процесса отправки, мы подставляем имя и процесс, чтобы получить

(@ 0) {@ (@ 0! (0)) / @ 0}! ((0) {@ (@ 0! (0)) / @ 0}).

Опять же, используя правила синтаксической подстановки, это выражение можно упростить

@ (@ 0! (0))! (0).

Поэтому исходный процесс в конечном итоге сводится к отправке @0 на канал @(@0!(0)).

for (@ 0 ← @ (@ 0! (0))) * (@ 0) | @ (@ 0! (0))! (! (@ 0! (0))) →! (@ 0! (0)))

Во-первых, давайте точно определим, что здесь происходит. Существует два процесса, выполняемых одновременно: процесс получения для (@ 0 ← @ (@ 0! (0))) * (@ 0) и процесс отправки @ (@ 0! (0))! (! ( @ 0! (0))). Для упрощения мы будем называть y = @ 0, P = * y, Q = y! (0), x = @Q и R =! Q. Теперь мы переписываем исходный процесс

для (y ← x) P | х! (R).

В этом формате мы ясно видим, что происходит comm-событие и, следовательно, сводится к

(Р) {@ Р / у}

Возвращаясь к определениям P и Q, мы имеем

(* У) {@ Р / у}.

По правилу семантической замены для разыменования эта подстановка упрощает процесс R, который является просто

! (@ 0! (0)),

репликация процесса, который отправляет сообщение @0 на канал @0.

На этом заканчивается серия статей вычислительных исчислений. Следующий статьи будут посвещены лекциям DoCC.

Рекомендации

Мередит, Радешок (2005). Отражающие исчисления высших порядков, 16 июня 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