Теорема Кнастера

Бронислав Кнастер

Альфред Тарский

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

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

Частично упорядоченное множество $\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