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

Теорема в теории порядка и теории решеток

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

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

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

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

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

полученный путем итерации f по наименьшему элементу ⊥ из 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.}$

Смотрите также

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

Ссылки

1. Альфред Тарский (1955). «Теорема о неподвижной точке в теории решеток и ее приложения». Pacific Journal of Mathematics . 5:2 : 285–309., стр. 305.
2. Патрик Кусо и Радхия Кусо (1979). «Конструктивные версии теорем Тарского о неподвижной точке». Pacific Journal of Mathematics . 82:1 : 43–57.
3. Столтенберг-Хансен, В.; Линдстром, И.; Гриффор, Э. Р. (1994). Математическая теория доменов В. Столтенберга-Хансена. Cambridge University Press. стр. 24. doi :10.1017/cbo9781139166386. ISBN 0521383447.