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

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

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

(L,\sqsubseteq )

представляет собой направленно-полный частичный порядок (dcpo) с наименьшим элементом, и пусть

f:L\to L

— непрерывная по Скотту (и, следовательно, монотонная ) функция . Затем

f

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

f.

Восходящая цепочка Клини функции f — это цепочка

\bot \sqsubseteq f(\bot )\sqsubseteq f(f(\bot ))\sqsubseteq \cdots \sqsubseteq f^{n}(\bot )\sqsubseteq \cdots

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

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

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

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

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

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

Лемма. Если

L

представляет собой dcpo с наименьшим элементом, и

f:L\to L

является непрерывным по Скотту, то

f^{n}(\bot )\sqsubseteq f^{n+1}(\bot ),n\in \mathbb {N} _{0}

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

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

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

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

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

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

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