Теорема Фишера-Линча-Патерсона (FLP) — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
 
(не показано 19 промежуточных версий этого же участника)
Строка 1: Строка 1:
Теорема Фишера, Линча и Патерсона (FLP, 1985 год) невозможно достичь даже необоснованного [[Консенсус в распределённой системе|консенсуса]] $N>2$ процессами даже на одном бите при следующих условиях:
+
[[Категория:Параллельное программирование]]
 +
Теорема Фишера, Линча и Патерсона (FLP, 1985 год): невозможно достичь даже необоснованного [[Консенсус в распределённой системе|консенсуса]] $N>2$ процессами даже на одном бите при следующих условиях:
 
* Алгоритм должен завершиться за конечное время.
 
* Алгоритм должен завершиться за конечное время.
 
* Один из узлов [[Иерархия ошибок в распределённых системах|может отказать]]
 
* Один из узлов [[Иерархия ошибок в распределённых системах|может отказать]]
Строка 5: Строка 6:
 
* Алгоритм должен быть детерминирован.
 
* Алгоритм должен быть детерминирован.
  
 +
Если разрешаем незавершаемость в случае отказов, есть [[Paxos]] и [[Raft]].
 
Если отказов нет, есть [[Консенсус в распределённой системе#Решение при отсутствии отказов|простой алгоритм]].
 
Если отказов нет, есть [[Консенсус в распределённой системе#Решение при отсутствии отказов|простой алгоритм]].
 
Если система синхронна, то есть [[консенсус в синхронных системах]].
 
Если система синхронна, то есть [[консенсус в синхронных системах]].
 
Если разрешаем недетерминизм, то есть [[алгоритм Бен-Ора]].
 
Если разрешаем недетерминизм, то есть [[алгоритм Бен-Ора]].
  
* TODO: доказательство из презентации Елизарова.
+
При этом даже если разрешить одновременную посылку сообщения сразу нескольким процессам (как в [[Общий порядок сообщений|общем порядке сообщений]]) и тем самым запретить процессу падать при массовой рассылке сообщений, лучше не станет: нет гарантии, в каком порядке и как скоро эти сообщения будут получены и обработаны получателями.
* Инфо: http://bailonga.es/tpmtp/lecture09.pdf + презентация Р.Елизарова
+
А вот если какую-нибудь гарантию дадим, то получаем [[Переформулировки консенсуса в распределённой системе#Terminating Reliable Broadcast (TRB)|TLB]], из которого сразу выводится консенсус.
* Инфо: https://github.com/volhovm/study-notes/blob/master/parallel_programming/parallel_programming.org
+
 
 +
== Доказательство ==
 +
Из презентации Р. Елизарова.
 +
 
 +
От противного: пусть есть такой алгоритм, тогда мы проанализируем варианты его исполнения, подстроим порядок доставки сообщений (без откладывания сообщений бесконечно далеко), получим бесконечную цепочку выполнения и противоречие с конечностью алгоритма.
 +
 
 +
=== Модель ===
 +
{{Определение
 +
|definition=
 +
'''Процесс''' — это детерминированный автомат, который может выполнять три операции:
 +
* <code>receive() : msg</code> — бесконечная блокировка до получения ближайшего сообщения. Так как система асинхронна, возможности "посмотреть следующее сообщение" или ''таймаутов нет''.
 +
* <code>send(msg)</code> — отправка сообщения другому процессу. Гарантируется, что сообщение дойдёт получателю за конечное время, но это время может быть сколь угодно большим.
 +
* <code>decided(value)</code> — процесс принял решение <code>value</code>. Решение процесс может принять только один раз, но после этого он ''может продолжить выполняться'' и помогать остальным процессам.
 +
Заметим, что так как нет "времени", можно считать все переходы в процессе мгновенными.
 +
}}
 +
Для доказательства от противного у нас есть такой алгоритм для процессов, что все они вызывают <code>decided(value)</code> с одинаковым значением через конечное время, независимо от того, как система задерживает сообщения.
 +
{{Определение
 +
|definition=
 +
'''Конфигурация''' — это состояния всех процессов плюс все сообщения в пути (которые отправили, но ещё не доставили).
 +
}}
 +
В начальной конфигурация у каждого процесса может быть сколько угодно входных данных и даже своя программа.
 +
Начальных конфигураций может быть несколько, они могут отличаться, например, предложениями процессов.
 +
{{Определение
 +
|definition=
 +
'''Шаг''' из одной конфигурации в другую — это приём какого-то сообщения процессом (событие) и последовавшие за этим внутренние действия процесса до следующего <code>receive()</code>. Эти действия ''однозначно'' определяются предыдущей конфигурацией и событием.
 +
}}
 +
{{Определение
 +
|definition=
 +
'''Исполнение''' — это ''бесконечная'' цепочка шагов из какой-нибудь начальной конфигурации. Бесконечная, потому что процессы могут выполняться и после принятия решений.
 +
}}
 +
{{Определение
 +
|definition=
 +
'''Отказавший процесс''' — это процесс, который делает только конечное количество шагов в исполнении. Такой в системе может быть максимум один (это более сильное условие, чем если может много процессов отказывать).
 +
}}
 +
 
 +
Также гарантируется, что в любом исполнении любое сообщение, предназначенное не отказавшему процессу, обрабатывается через конечное число шагов.
 +
Другими словами, ''сообщения не теряются''.
 +
 
 +
=== Валентность ===
 +
Заметим, что в любом исполнении всегда принимается решение.
 +
Даже если один процесс отказал, то все остальные должны прийти к решению за конечное число шагов.
 +
{{Определение
 +
|definition=
 +
Конфигурация называется '''$i$-валентной''' и '''одновалентной''', если все цепочки шагов из неё приводят к решению $i$.
 +
Таким образом, бывают 0-валентные и 1-валентные конфигурации.
 +
Если же из конфигурации есть цепочки, приводящие к каждому из решений, то такая конфигурация называется '''бивалентной'''.
 +
}}
 +
'''Наблюдение''': пусть из конфигурации $X$ есть цепочка шагов, обрабатывающая сообщения из $X$ в подмножестве процессов $A$, за которой идёт цепочка процессов, обрабатывающая сообщения из $X$ в подмножестве процессов $B$, и в конце мы получили конфигурацию $Y$. Тогда эти цепочки коммутируют: можно сначала обработать сообщения подмножеством процессов $B$, а потом — $A$ (так как мы обрабатываем только сообщения из $X$, а не новые).
 +
 
 +
'''Наблюдение''': за $i$-валентной конфигурацией могут следовать только $i$-валентные.
 +
 
 +
=== Начальная бивалентная конфигурация ===
 +
'''Лемма''': существует бивалентная начальная конфигурация.
 +
 
 +
Доказательство от противного: пусть все начальные конфигурации одновалентны.
 +
Из нетривиальности консенсуса мы знаем, что есть как 0-, так и 1-валентные начальные конфигурации.
 +
Тогда можно найти две начальные конфигурации разной валентности, которые отличаются только состоянием одного процесса:
 +
взяли две произвольные начальные конфигурации разной валентности, начали переводить одну в другую копированием исходных состояний процессов, по одному процессу за шаг.
 +
 
 +
А раз есть две такие конфигурации разной валентности, то пусть в каждой из них этот процесс (где они отличаются) откажет с самого начала, до отправки и приёма любых сообщений.
 +
Тогда мы всё ещё получим консенсус, но решение будет одинаковым, потому что внешняя система никак не может выявить состояние отказавшего процесса.
 +
А они исходно были разной валентности, противоречие.
 +
 
 +
=== Цепочка бивалентных конфигураций ===
 +
'''Лемма''': для любой бивалентной конфигурации можно найти следующую за ней бивалентную.
 +
 
 +
'''Следствие''': если лемма верна, то мы можем построить бесконечную цепочку бивалентных конфигураций и тем самым получим противоречие и докажем FLP: есть бесконечная цепочка, в которой не принято решение.
 +
 
 +
'''Доказательство''': от противного.
 +
Пусть все конфигурации после некотороый бивалентной конфигурации $G$ одновалентны.
 +
Введём определения:
 +
* $e$ — какое-то событие в $G$, скармливающее сообщение $m$ процессу $p$. Такое есть, иначе у нас в конфигурации ничего не происходит, она бивалентна, а решение должно быть детерминированным, противоречие.
 +
* $C$ — множество конфигураций, достижимых из $G$ без использования $e$. В частности, в $C$ по предположению отсутствуют бивалентные конфигурации.
 +
* $D=e(C)$, то есть все конфигурации, достижимые из $G$, где $e$ — последнее обработанное событие. В частности, в $D$ по предположению отсутствуют бивалентные конфигурации.
 +
Теперь докажем, что $D$ содержит бивалентную конфигурацию.
 +
То есть мы выбрали, насколько сильно отложить обработку произвольного события $e$ и показали, что это не порушит бивалентность.
 +
Надо ещё аккуратно, чтобы это не порушило конечность обработки каждого сообщения.
 +
Например, их можно обрабатывать по очереди, начиная с самых старых.
 +
Тогда каждое событие рано или поздно попадёт в наш шаг и будет обработано.
 +
 
 +
[[Файл:distributed-flp-proof-cd.png|500px]]
 +
 
 +
==== Шаг 1: существование $i$-валентных конфигураций в $D$ ====
 +
'''Подлемма''': для любого $i$ в $D$ существует $i$-валентная конфигурация.
 +
 
 +
В самом деле: так как $G$ бивалентна, то по какой-то цепочке шагов из неё можно дойти до $i$-валентной конфигурации $E_i$.
 +
Дальше разбором случаев находим искомую конфигурацию в $D$:
 +
* Если $E_i \in D$, то мы доказали подлемму.
 +
* Если $E_i \in C$, то $e(E_i) \in D$, у $e(E_i)$ такая же валентность и мы снова доказали подлемму.
 +
* Иначе ребро $e$ применялось в цепочке шагов для достижения $E_i$ из $G$. Найдём конфигурацию $F_i \in D$, которая была в этой цепочке шагов сразу после применения $e$. Так как в $D$ нет бивалентных конфигураций, то $F_i$ является $i$-валентной, что и требовалось.
 +
 
 +
==== Шаг 2: существование соседних разновалентных конфигураций ====
 +
 
 +
Теперь мы хотим найти такие две соседние конфигурации $C_0, C_1 \in C$ (отличающиеся переходом $e'(C_0)=C_1$), что $D_0=e(C_0) \in D$ является 0-валентной, а $D_1=e(C_1)$ — 1-валентной (или наоборот).
 +
Это можно сделать, если взять в $D$ конфигурацию $e(C_1)$, отличающуюся от валентности $e(G)$, а дальше посмотреть на цепочку конфигураций между $G$ и $e(C_1)$ и найти момент смены валентности.
 +
 
 +
Начнём искать, более строго. Не теряя общности можем сказать, что $e(G)\in D$ является 0-валентной (иначе повторим доказательство шага).
 +
По предыдущему шагу найдём в $D$ 1-валентную конфигурацию $D_1=e(C_1)\in D$.
 +
Конфигурация $C_1$ получена какой-то конечной непустой цепочкой сообщений $x_1, x_2, \dots, x_k$.
 +
Будем по очереди убирать по одному сообщения с конца и смотреть на валентность конфигураций $e(x_{k-1}(\dots(x_1(G))\dots))$, $e(x_{k-2}(\dots(x_1(G))\dots))$, \dots — в какой-то момент она сменится с единицы на ноль (например, при пустой цепочке, т.е. при рассмотрении $e(G)\in D$).
 +
Тогда мы как раз нашли искомую пару соседей $C_0$ и $C_1$ таких, что $e(C_0)$ и $e(C_1)$ разной валентности.
 +
 
 +
==== Шаг 3: разбор случаев ====
 +
Теперь у нас, помимо конфигурации $C$ и события $e$, есть некоторое событие $e'$ и конфигурации $C_0$ и $C_1$, причём:
 +
* $e(C_0)=D_0$ является 0-валентной, а $e(C_1)=D_1$ является 1-валентной (или наоборот, повторим доказательство)
 +
* $e'(C_0)=C_1$
 +
 
 +
Разберём два случая, в зависимости от того, одному процессу приходят $e$ и $e'$ или разным.
 +
 
 +
===== Разным =====
 +
Пусть $proc(e)\neq proc(e')$ (т.е. эти события в разных процессах).
 +
Тогда нам всё равно, в каком порядке их обрабатывать, т.е. $e'(e(C_0))=e(e'(C_0))=e(C_1)=D_1$:
 +
 
 +
[[Файл:Distributed-flp-proof-case1.png|300px]]
 +
 
 +
Мы знаем, что $D_1$ является 1-валентной. Но так как они достижима из $D_0$, то она также является и 0-валентной, противоречие.
 +
 
 +
===== Одному =====
 +
Пусть $proc(e) = proc(e') = p$ (т.е. это два сообщения одному и тому же процессу).
 +
Тогда рассмотрим цепочку шагов $\sigma$ от состояния $C_0$, в которой процесс $p$ вообще отказал вместо обработки сообщений.
 +
Тогда остальные процессы в этой цепочке пришли к какому-то решению в конфигурации $A=\sigma(C_0)$.
 +
Тогда эта конфигурация должна быть либо 0-, либо 1-валентной (в ней уже принято решение).
 +
 
 +
[[Файл:Distributed-flp-proof-case2.png|400px]]
 +
 
 +
Но теперь мы можем сказать, что процесс $p$ не отказал, а просто очень долго работал и теперь получает событие $e$.
 +
Так как $\sigma$ не обращается к $p$, то $E_0=e(\sigma(C_0)=\sigma(e(C_0))=\sigma(D_0)$ — конфигурация, достижимая из 0-валентной, т.е. тоже 0-валентная.
 +
 
 +
С другой стороны, можно аналогично сказать, что процесс $p$ теперь получает сообщение $e'$, а за ним — сообщение $e$.
 +
Тогда получается $E_1=e(e'(\sigma(C_0))$.
 +
Из-за коммутативности получаем $E_1=\sigma(e(e'(C_0)))=\sigma(e(C_1))=\sigma(D_1)$ — конфигурация, достижимая из 1-валентной, т.е. тоже 1-валентная.
 +
 
 +
Таким образом получаем, что из $A$ достижимы и 0-валентная, и 1-валентная конфигурация, противоречие.
 +
 
 +
== Ссылки ==
 +
* http://bailonga.es/tpmtp/lecture09.pdf  
 +
* https://github.com/volhovm/study-notes/blob/master/parallel_programming/parallel_programming.org

Текущая версия на 08:49, 4 июня 2019

Теорема Фишера, Линча и Патерсона (FLP, 1985 год): невозможно достичь даже необоснованного консенсуса $N>2$ процессами даже на одном бите при следующих условиях:

  • Алгоритм должен завершиться за конечное время.
  • Один из узлов может отказать
  • Система асинхронна
  • Алгоритм должен быть детерминирован.

Если разрешаем незавершаемость в случае отказов, есть Paxos и Raft. Если отказов нет, есть простой алгоритм. Если система синхронна, то есть консенсус в синхронных системах. Если разрешаем недетерминизм, то есть алгоритм Бен-Ора.

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

Доказательство[править]

Из презентации Р. Елизарова.

От противного: пусть есть такой алгоритм, тогда мы проанализируем варианты его исполнения, подстроим порядок доставки сообщений (без откладывания сообщений бесконечно далеко), получим бесконечную цепочку выполнения и противоречие с конечностью алгоритма.

Модель[править]

Определение:
Процесс — это детерминированный автомат, который может выполнять три операции:
  • receive() : msg — бесконечная блокировка до получения ближайшего сообщения. Так как система асинхронна, возможности "посмотреть следующее сообщение" или таймаутов нет.
  • send(msg) — отправка сообщения другому процессу. Гарантируется, что сообщение дойдёт получателю за конечное время, но это время может быть сколь угодно большим.
  • decided(value) — процесс принял решение value. Решение процесс может принять только один раз, но после этого он может продолжить выполняться и помогать остальным процессам.
Заметим, что так как нет "времени", можно считать все переходы в процессе мгновенными.

Для доказательства от противного у нас есть такой алгоритм для процессов, что все они вызывают decided(value) с одинаковым значением через конечное время, независимо от того, как система задерживает сообщения.

Определение:
Конфигурация — это состояния всех процессов плюс все сообщения в пути (которые отправили, но ещё не доставили).

В начальной конфигурация у каждого процесса может быть сколько угодно входных данных и даже своя программа. Начальных конфигураций может быть несколько, они могут отличаться, например, предложениями процессов.

Определение:
Шаг из одной конфигурации в другую — это приём какого-то сообщения процессом (событие) и последовавшие за этим внутренние действия процесса до следующего receive(). Эти действия однозначно определяются предыдущей конфигурацией и событием.


Определение:
Исполнение — это бесконечная цепочка шагов из какой-нибудь начальной конфигурации. Бесконечная, потому что процессы могут выполняться и после принятия решений.


Определение:
Отказавший процесс — это процесс, который делает только конечное количество шагов в исполнении. Такой в системе может быть максимум один (это более сильное условие, чем если может много процессов отказывать).


Также гарантируется, что в любом исполнении любое сообщение, предназначенное не отказавшему процессу, обрабатывается через конечное число шагов. Другими словами, сообщения не теряются.

Валентность[править]

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

Определение:
Конфигурация называется $i$-валентной и одновалентной, если все цепочки шагов из неё приводят к решению $i$.

Таким образом, бывают 0-валентные и 1-валентные конфигурации.

Если же из конфигурации есть цепочки, приводящие к каждому из решений, то такая конфигурация называется бивалентной.

Наблюдение: пусть из конфигурации $X$ есть цепочка шагов, обрабатывающая сообщения из $X$ в подмножестве процессов $A$, за которой идёт цепочка процессов, обрабатывающая сообщения из $X$ в подмножестве процессов $B$, и в конце мы получили конфигурацию $Y$. Тогда эти цепочки коммутируют: можно сначала обработать сообщения подмножеством процессов $B$, а потом — $A$ (так как мы обрабатываем только сообщения из $X$, а не новые).

Наблюдение: за $i$-валентной конфигурацией могут следовать только $i$-валентные.

Начальная бивалентная конфигурация[править]

Лемма: существует бивалентная начальная конфигурация.

Доказательство от противного: пусть все начальные конфигурации одновалентны. Из нетривиальности консенсуса мы знаем, что есть как 0-, так и 1-валентные начальные конфигурации. Тогда можно найти две начальные конфигурации разной валентности, которые отличаются только состоянием одного процесса: взяли две произвольные начальные конфигурации разной валентности, начали переводить одну в другую копированием исходных состояний процессов, по одному процессу за шаг.

А раз есть две такие конфигурации разной валентности, то пусть в каждой из них этот процесс (где они отличаются) откажет с самого начала, до отправки и приёма любых сообщений. Тогда мы всё ещё получим консенсус, но решение будет одинаковым, потому что внешняя система никак не может выявить состояние отказавшего процесса. А они исходно были разной валентности, противоречие.

Цепочка бивалентных конфигураций[править]

Лемма: для любой бивалентной конфигурации можно найти следующую за ней бивалентную.

Следствие: если лемма верна, то мы можем построить бесконечную цепочку бивалентных конфигураций и тем самым получим противоречие и докажем FLP: есть бесконечная цепочка, в которой не принято решение.

Доказательство: от противного. Пусть все конфигурации после некотороый бивалентной конфигурации $G$ одновалентны. Введём определения:

  • $e$ — какое-то событие в $G$, скармливающее сообщение $m$ процессу $p$. Такое есть, иначе у нас в конфигурации ничего не происходит, она бивалентна, а решение должно быть детерминированным, противоречие.
  • $C$ — множество конфигураций, достижимых из $G$ без использования $e$. В частности, в $C$ по предположению отсутствуют бивалентные конфигурации.
  • $D=e(C)$, то есть все конфигурации, достижимые из $G$, где $e$ — последнее обработанное событие. В частности, в $D$ по предположению отсутствуют бивалентные конфигурации.

Теперь докажем, что $D$ содержит бивалентную конфигурацию. То есть мы выбрали, насколько сильно отложить обработку произвольного события $e$ и показали, что это не порушит бивалентность. Надо ещё аккуратно, чтобы это не порушило конечность обработки каждого сообщения. Например, их можно обрабатывать по очереди, начиная с самых старых. Тогда каждое событие рано или поздно попадёт в наш шаг и будет обработано.

Distributed-flp-proof-cd.png

Шаг 1: существование $i$-валентных конфигураций в $D$[править]

Подлемма: для любого $i$ в $D$ существует $i$-валентная конфигурация.

В самом деле: так как $G$ бивалентна, то по какой-то цепочке шагов из неё можно дойти до $i$-валентной конфигурации $E_i$. Дальше разбором случаев находим искомую конфигурацию в $D$:

  • Если $E_i \in D$, то мы доказали подлемму.
  • Если $E_i \in C$, то $e(E_i) \in D$, у $e(E_i)$ такая же валентность и мы снова доказали подлемму.
  • Иначе ребро $e$ применялось в цепочке шагов для достижения $E_i$ из $G$. Найдём конфигурацию $F_i \in D$, которая была в этой цепочке шагов сразу после применения $e$. Так как в $D$ нет бивалентных конфигураций, то $F_i$ является $i$-валентной, что и требовалось.

Шаг 2: существование соседних разновалентных конфигураций[править]

Теперь мы хотим найти такие две соседние конфигурации $C_0, C_1 \in C$ (отличающиеся переходом $e'(C_0)=C_1$), что $D_0=e(C_0) \in D$ является 0-валентной, а $D_1=e(C_1)$ — 1-валентной (или наоборот). Это можно сделать, если взять в $D$ конфигурацию $e(C_1)$, отличающуюся от валентности $e(G)$, а дальше посмотреть на цепочку конфигураций между $G$ и $e(C_1)$ и найти момент смены валентности.

Начнём искать, более строго. Не теряя общности можем сказать, что $e(G)\in D$ является 0-валентной (иначе повторим доказательство шага). По предыдущему шагу найдём в $D$ 1-валентную конфигурацию $D_1=e(C_1)\in D$. Конфигурация $C_1$ получена какой-то конечной непустой цепочкой сообщений $x_1, x_2, \dots, x_k$. Будем по очереди убирать по одному сообщения с конца и смотреть на валентность конфигураций $e(x_{k-1}(\dots(x_1(G))\dots))$, $e(x_{k-2}(\dots(x_1(G))\dots))$, \dots — в какой-то момент она сменится с единицы на ноль (например, при пустой цепочке, т.е. при рассмотрении $e(G)\in D$). Тогда мы как раз нашли искомую пару соседей $C_0$ и $C_1$ таких, что $e(C_0)$ и $e(C_1)$ разной валентности.

Шаг 3: разбор случаев[править]

Теперь у нас, помимо конфигурации $C$ и события $e$, есть некоторое событие $e'$ и конфигурации $C_0$ и $C_1$, причём:

  • $e(C_0)=D_0$ является 0-валентной, а $e(C_1)=D_1$ является 1-валентной (или наоборот, повторим доказательство)
  • $e'(C_0)=C_1$

Разберём два случая, в зависимости от того, одному процессу приходят $e$ и $e'$ или разным.

Разным[править]

Пусть $proc(e)\neq proc(e')$ (т.е. эти события в разных процессах). Тогда нам всё равно, в каком порядке их обрабатывать, т.е. $e'(e(C_0))=e(e'(C_0))=e(C_1)=D_1$:

Distributed-flp-proof-case1.png

Мы знаем, что $D_1$ является 1-валентной. Но так как они достижима из $D_0$, то она также является и 0-валентной, противоречие.

Одному[править]

Пусть $proc(e) = proc(e') = p$ (т.е. это два сообщения одному и тому же процессу). Тогда рассмотрим цепочку шагов $\sigma$ от состояния $C_0$, в которой процесс $p$ вообще отказал вместо обработки сообщений. Тогда остальные процессы в этой цепочке пришли к какому-то решению в конфигурации $A=\sigma(C_0)$. Тогда эта конфигурация должна быть либо 0-, либо 1-валентной (в ней уже принято решение).

Distributed-flp-proof-case2.png

Но теперь мы можем сказать, что процесс $p$ не отказал, а просто очень долго работал и теперь получает событие $e$. Так как $\sigma$ не обращается к $p$, то $E_0=e(\sigma(C_0)=\sigma(e(C_0))=\sigma(D_0)$ — конфигурация, достижимая из 0-валентной, т.е. тоже 0-валентная.

С другой стороны, можно аналогично сказать, что процесс $p$ теперь получает сообщение $e'$, а за ним — сообщение $e$. Тогда получается $E_1=e(e'(\sigma(C_0))$. Из-за коммутативности получаем $E_1=\sigma(e(e'(C_0)))=\sigma(e(C_1))=\sigma(D_1)$ — конфигурация, достижимая из 1-валентной, т.е. тоже 1-валентная.

Таким образом получаем, что из $A$ достижимы и 0-валентная, и 1-валентная конфигурация, противоречие.

Ссылки[править]