Изменения

Перейти к: навигация, поиск

Согласованный интервал

1690 байт добавлено, 19:13, 11 февраля 2019
Добавил доказательство наличия согласованного среза
[[Категория: Параллельное программирование]]
Рассмотрим Назовем пару [[Срез, согласованный срез|срезысрезов]] ''<tex>[G'' и '', H'']</tex>, <tex>G \subset H</tex>. Назовем эту пару , интервалом.<br>Интервал '''согласованный''', если <tex>\forall e, g: g \in G, \land e \rightarrow g \Rightarrow e \in H</tex>.
Это значит, что нет сообщений через согласованный интервал в обратную сторону. Отсюда следует, что в согласованном интервале есть согласованный срез. Более того, в обратную сторону тоже верно. В самом деле: рассмотрим произвольный согласованный интервал <tex>[G, H]</tex>.В доказательстве ниже будем считать, что $a \to a$ для простоты (но можно переписать доказательство и без рефлексивности). <tex>G</tex> может не быть срезом (если есть стрелочка из <tex>H \setminus G</tex> в <tex>G</tex>), что печально.Но можно попробовать пойти по стрелочкам в обратную сторону.Придумаем формальное "замыкание" <tex>G</tex>: возьмём множество <tex>X = \{ e \mid \exists g \in G \colon e \rightarrow g \}</tex>.* $G \subseteq X$ по построению (тут пользуемся тем, что $a \to a$).* $X \subseteq H$, иначе есть стрелочка, пересекающая согласованный интервал в обратную сторону.* $X$ является срезом, так как если есть $a < b$ и $b \in X$, есть $g \in G$ такое, что $b \rightarrow g$. По транзитивности имеем $a \rightarrow g$, что и требуется.* $X$ является согласованным срезом. Пусть есть события $a \rightarrow b$, причём $b \in X$. Тогда есть такое $g \in G$, что $b \rightarrow g$. Следовательно, $a \rightarrow g$. Значит, $a \in X$, что и требовалось.
292
правки

Навигация