Теорема Клини о неподвижной точке - Kleene fixed-point theorem

Эта статья посвящена теореме Клини о неподвижной точке в теории решеток. По поводу теоремы о неподвижной точке в теории вычислимости см. Теорема Клини о рекурсии.

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

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

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

В восходящая цепь Клини из ж это цепь

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

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

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

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

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

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

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

Лемма. Если ${\displaystyle L}$ является DCPO с наименьшим элементом, и ${\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. Тогда мы должны показать, что ${\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 )}$ справедливо, и поскольку f монотонна (свойство непрерывных по Скотту функций), результат также верен.

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

${\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). "Теорема о неподвижной точке в теории решеток и ее приложения". Тихоокеанский математический журнал. 5:2: 285–309., стр.305.
2. Патрик Кузо и Радия Кузо (1979). «Конструктивные версии теорем Тарского о неподвижной точке». Тихоокеанский математический журнал. 82:1: 43–57.
3. Stoltenberg-Hansen, V .; Lindstrom, I .; Гриффор, Э. Р. (1994). Математическая теория областей В. Столтенберг-Хансен. Издательство Кембриджского университета. стр.24. Дои:10.1017 / cbo9781139166386. ISBN  0521383447.