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

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

Теорема Кнастера — Тарского — теорема в теории решёток, впервые сформулированная в частном случае Брониславом Кнастером (польск. Bronisław Knaster) и обобщенная Альфредом Тарским. Утверждает, что множество всех неподвижных точек любого монотонного отображения полной решётки на себя также является полной решёткой.

Результат используется в теоретической информатике, в частности, в работах по семантике языков программирования.

Формулировка[править | править вики-текст]

Пусть \langle L, \sqsubseteq \rangle — полная решётка, а отображение f: L \to L — монотонно, то есть сохраняет отношение порядка: l_1 \sqsubseteq l_2 \Rightarrow f(l_1) \sqsubseteq f(l_2), то множество всех неподвижных точек:

\mathrm{Fix}(f) = \{l \in L \mid f(l) = l\}

также является полной решёткой.

Связанные результаты[править | править вики-текст]

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

Литература[править | править вики-текст]

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