Теорема Клини о неподвижной точке

Вычисление наименьшей фиксированной точки функции f ( x ) =1/10x ² + atan ( x ) +1, используя теорему Клини в вещественном интервале [0,7] с обычным порядком

В математических областях порядка и решетка теории , то теорема Клини о неподвижной точке , названной в честь американского математика Клини , утверждает следующее:

Теорема Клини о неподвижной точке. Предположим, что это направленно-полный частичный порядок (dcpo) с наименьшим элементом, и пусть будет непрерывной по Скотту (и, следовательно, монотонной ) функцией . Тогда имеет наименьшую неподвижную точку , которая является супремумом восходящей цепочки Клини${\ displaystyle (L, \ sqsubseteq)}$${\ displaystyle f: L \ to L}$${\ displaystyle f}$${\ displaystyle f.}$

По возрастанию клиниевская цепь из F представляет собой цепь

${\ Displaystyle \ бот \ sqsubseteq е (\ бот) \ sqsubseteq е (е (\ бот)) \ sqsubseteq \ cdots \ sqsubseteq f ^ {n} (\ бот) \ sqsubseteq \ cdots}$

полученный переборе е на наименьшего элемента ⊥ из L . Выраженная формулой, теорема утверждает, что

${\displaystyle {\textrm {lfp}}(f)=\sup \left(\left\{f^{n}(\bot )\mid n\in \mathbb {N} \right\}\right)}$

где обозначает наименьшую неподвижную точку.${\displaystyle {\textrm {lfp}}}$

Хотя теорема Тарского о неподвижной точке не рассматривает, как неподвижные точки могут быть вычислены путем итерации f из некоторого начального числа (также это относится к монотонным функциям на полных решетках ), этот результат часто приписывается Альфреду Тарски, который доказывает его для аддитивных функций ^[1] Более того, теорема Клини о неподвижной точке может быть расширена до монотонных функций с помощью трансфинитных итераций. ^[2]

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

Сначала мы должны показать, что восходящая цепочка Клини существует в . Чтобы показать это, мы докажем следующее:${\displaystyle f}$${\displaystyle L}$

Лемма. Если это DCPO с наименьшим элементом и непрерывно по Скотту, то${\displaystyle L}$${\displaystyle f:L\to L}$${\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot ),n\in \mathbb {N} _{0}}$

Доказательство. Воспользуемся индукцией:

• Предположим, что n = 0. Тогда, поскольку - наименьший элемент.${\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot ),}$${\displaystyle \bot }$
• Предположим, что n> 0. Тогда мы должны это показать . Путем перестановки получаем . По предположению индукции мы знаем, что это верно, и поскольку f монотонен (свойство непрерывных по Скотту функций), результат также верен.${\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )}$${\displaystyle f(f^{n-1}(\bot ))\sqsubseteq f(f^{n}(\bot ))}$${\displaystyle f^{n-1}(\bot )\sqsubseteq f^{n}(\bot )}$

Следствием леммы является следующая направленная ω-цепь:

${\displaystyle \mathbb {M} =\{\bot ,f(\bot ),f(f(\bot )),\ldots \}.}$

Из определения dcpo следует, что он имеет супремум, назовите его. Теперь остается показать, что это наименьшая неподвижная точка.${\displaystyle \mathbb {M} }$${\displaystyle m.}$${\displaystyle m}$

Во- первых, мы покажем , что является фиксированной точкой, т.е. . Потому что это Скотт-непрерывен , , то есть . Кроме того , так и потому , что не имеет никакого влияния в определении супремуму мы имеем: . Отсюда следует, что , делая фиксированную точку .${\displaystyle m}$${\displaystyle f(m)=m}$${\displaystyle f}$${\displaystyle f(\sup(\mathbb {M} ))=\sup(f(\mathbb {M} ))}$${\displaystyle f(m)=\sup(f(\mathbb {M} ))}$${\displaystyle \mathbb {M} =f(\mathbb {M} )\cup \{\bot \}}$${\displaystyle \bot }$${\displaystyle \sup(f(\mathbb {M} ))=\sup(\mathbb {M} )}$${\displaystyle f(m)=m}$${\displaystyle m}$${\displaystyle f}$

Доказательство того, что на самом деле наименьшая фиксированная точка, может быть выполнено путем демонстрации того, что любой элемент в меньше, чем любая фиксированная точка (потому что по свойству супремума , если все элементы набора меньше, чем элемент, то также меньше чем тот же элемент ). Это делается по индукции: Предположим, что это некоторая неподвижная точка . Докажем теперь индукцией по этому . База индукции, очевидно, верна: так как является наименьшим элементом . В качестве предположения индукции мы можем предположить, что . Теперь сделаем шаг индукции: исходя из предположения индукции и монотонности${\displaystyle m}$${\displaystyle \mathbb {M} }$${\displaystyle f}$${\displaystyle D\subseteq L}$${\displaystyle L}$${\displaystyle \sup(D)}$${\displaystyle L}$${\displaystyle k}$${\displaystyle f}$${\displaystyle i}$${\displaystyle \forall i\in \mathbb {N} :f^{i}(\bot )\sqsubseteq k}$${\displaystyle (i=0)}$${\displaystyle f^{0}(\bot )=\bot \sqsubseteq k,}$${\displaystyle \bot }$${\displaystyle L}$${\displaystyle f^{i}(\bot )\sqsubseteq k}$${\displaystyle f}$(опять же, что подразумевается непрерывностью Скотта ), мы можем заключить следующее: теперь, исходя из предположения, что это фиксированная точка, мы знаем это и отсюда получаем${\displaystyle f}$${\displaystyle f^{i}(\bot )\sqsubseteq k~\implies ~f^{i+1}(\bot )\sqsubseteq f(k).}$${\displaystyle k}$${\displaystyle f,}$${\displaystyle f(k)=k,}$${\displaystyle f^{i+1}(\bot )\sqsubseteq k.}$

См. Также [ править ]

• Другие теоремы о неподвижной точке

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