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

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

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

Формулировка

Частично упорядоченное множество $\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 — частичные функции, а Φ_i — правильно построенные термы соответствующего языка программирования. Если предполагать Φ_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