2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 неподвижная точка монотонного преобразователя
Сообщение10.05.2010, 20:44 
Что-то не получается доказать такой факт, с которым я столкнулся в теории верификации программ.
Есть $\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\}.$$ Подскажите, как это сделать?

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение10.05.2010, 23:47 
Насколько я понял, в правой части равенства у вас стоит пустое множество.

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

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

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение10.05.2010, 23:49 
Аватара пользователя
malin в сообщении #317822 писал(а):
Насколько я понял, в правой части равенства у вас стоит пустое множество.

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

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

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение11.05.2010, 00:05 
Аватара пользователя
malin в сообщении #317822 писал(а):
Действительно, т.к. $\tau$ - монотонная функция, то
$\tau(\varnothing) \subseteq \varnothing$.

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

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение11.05.2010, 00:05 
Аватара пользователя
А доказывается это так.
Во-первых, т.к. $\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$-минимальная неподвижная точка. Для этого заметим, что любая неподвижная точка входит в пересечение.

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение11.05.2010, 00:09 
Да, ерунду написал.

-- Вт май 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\}$ будет пусто

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение11.05.2010, 08:50 
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, спасибо.

 
 
 
 Re: неподвижная точка монотонного преобразователя
Сообщение11.05.2010, 20:25 
Аватара пользователя
topic23747.html

 
 
 [ Сообщений: 8 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group