Теорема Кнастера — Тарского

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Теорема Кнастера — Тарского — теорема в теории множеств, впервые сформулированная в частном случае Брониславом Кнастером, и обобщённая Альфредом Тарским.

Формулировка[править | править исходный текст]

Частично упорядоченное множество \langle M,\sqsubseteq\rangle называется полным, если оно содержит наименьший элемент, и каждая цепь C\subseteq M в нём имеет наименьшую верхнюю грань. Функция f:M\to N, где M и N — полные частично упорядоченные множества, называется непрерывной, если для всех цепей C из M   \bigsqcup f(C) существует и равно f(\bigsqcup C). В частности, непрерывная функция будет также монотонной. Элемент a полного частично упорядоченного множества \langle M,\sqsubseteq\rangle называется неподвижной точкой отображения f:M\to M, если f(a) = a. Элемент a\in M называется наименьшей неподвижной точкой, если он является наименьшей нижней гранью множества всех неподвижных точек в M.

(Ниже дана Теорема Канторовича! Теорема Кнастера — Тарского для монотонных, возможно прерывных, отображений. См. на английскую версию.)

Теорема Кнастера — Тарского утверждает, что любое непрерывное отображение f полного частично упорядоченного множества в себя имеет наименьшую неподвижную точку.

Применение[править | править исходный текст]

Теорема Кнастера — Тарского имеет большое значение в теоретической информатике и является мощным инструментом для описания денотационной семантики языков программирования. Например, не ограничивая общности, в большинстве случаев можно считать, что функциональная программа может быть представлена в виде системы рекурсивных уравнений:



\begin{array}{lcr} 
f_1 &=& \Phi_1(f_1,\cdots, f_n)\\
f_2 &=& \Phi_2(f_1,\cdots, f_n)\\
\vdots &&\\ 
f_n &=& \Phi_n(f_1,\cdots, f_n)
\end{array}


где f_i — частичные функции, а \Phi_i — правильно построенные термы соответствующего языка программирования. Если предполагать \Phi_i непрерывными, теорема Кнастера — Тарского гарантирует существование и единственность наименьшего решения, то есть функций f_1, f_2,\ldots,f_n. Наименьшесть в этом случае означает, что f_i имеют самую широкую область определения по сравнению с другими решениями. Дальнейшее развитие эта идея получает в теории доменов.

Литература[править | править исходный текст]

  • S. Abramsky, Dov M. Gabbay, T. S. E. Maibaum, Handbook of Logic in Computer Science: Volume 1: Background: Mathematical Structures