неподвижная точка монотонного преобразователя

[cyb12]

Что-то не получается доказать такой факт, с которым я столкнулся в теории верификации программ.
Есть $\tau \colon \mathcal P(S) \to \mathcal P(S)$ -- функция, отображающая множество $\mathcal P(S)$ всех подмножеств $S$ в себя. При этом она монотонна (если $P\subseteq Q,$ то $\tau(P)\subseteq \tau(Q)$). Определим на $\mathcal P(S)$ отношение частичного порядка как теоретико-множественное включение. Нужно доказать, что минимальная неподвижная точка отображения $\tau(Z)$ определяется как

$$\mu Z.\tau(Z) = \bigcap\limits_{Z\in\mathcal P(S)}\{Z|\tau(Z)\subseteq Z\}.$$

Подскажите, как это сделать?

[malin]

Насколько я понял, в правой части равенства у вас стоит пустое множество.

Действительно, т.к. $\tau$ - монотонная функция, то
$\tau(\varnothing) \subseteq \varnothing$. Ну и поэтому пересечение пусто.

Да и на самом деле, т.к. $\tau(\varnothing) = \varnothing$, то $\varnothing$ - минимальная неподвижная точка

[Xaositect]

malin в сообщении #317822 писал(а):

Насколько я понял, в правой части равенства у вас стоит пустое множество.

Действительно, т.к. $\tau$ - монотонная функция, то
$\tau(\varnothing) \subseteq \varnothing$. Ну и поэтому пересечение пусто.

Это неверно. Например, постоянная функция является монотонной.

[paha]

malin в сообщении #317822 писал(а):

Действительно, т.к. $\tau$ - монотонная функция, то
$\tau(\varnothing) \subseteq \varnothing$.

Правильно так: $\forall A\in\cal{P}(S)$ $\tau(\varnothing)\subseteq\tau(A)$

[Xaositect]

А доказывается это так.
Во-первых, т.к. $\tau$ монотонна, $\tau(\cap_i A_i)\subseteq \cap_i \tau(A_i)$.
Дальше распишем по этой формуле $\tau$ от нашего большого пересечения (обозначим его $M$) и убедимся, что $\tau(M)\subseteq M$. Потом докажем, что вариант $\tau(M)\subset M$ невозможен: $\tau(M)\subseteq M\Rightarrow \tau(\tau(M))\subseteq \tau(M)\Rightarrow M\subseteq\tau(M)$ (последнее - по определению M)

Осталось доказать, что $M$-минимальная неподвижная точка. Для этого заметим, что любая неподвижная точка входит в пересечение.

[malin]

Да, ерунду написал.

-- Вт май 11, 2010 01:20:30 --

Кстати, всё равно что-то тут не то. Например, если $S = \{0,1\}$, то $\mathcal P(S) = \{\varnothing, \{0\},\{1\},\{0,1\}\}$
Если отображение $\tau$ задать таким образом:
$\tau(\varnothing) = \{0\}$, а остальные элементы отобразить в себя, то минимальными неподвижными точками будут множества $\{0\}$ и $\{1\}$.
А вот пересечение множеств $\{0\},\{1\},\{0,1\}$ будет пусто

[cyb12]

malin в сообщении #317831 писал(а):

Кстати, всё равно что-то тут не то. Например, если $S = \{0,1\}$, то $\mathcal P(S) = \{\varnothing, \{0\},\{1\},\{0,1\}\}$
Если отображение $\tau$ задать таким образом:
$\tau(\varnothing) = \{0\}$, а остальные элементы отобразить в себя, то минимальными неподвижными точками будут множества $\{0\}$ и $\{1\}$.
А вот пересечение множеств $\{0\},\{1\},\{0,1\}$ будет пусто

Тогда ваше отображение не монотонно: $\varnothing \subseteq \{1\}$, но при этом $\tau(\varnothing)=\{0\} \nsubseteq \tau(\{1\})=\{1\}$.

Xaositect, спасибо.

[Профессор Снэйп]

topic23747.html