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

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

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

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

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

Пусть  — полная решётка, а отображение  — монотонно, то есть сохраняет отношение порядка: , то множество всех неподвижных точек:

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

Следствия[править | править вики-текст]

Из теоремы Кнастера — Тарского следует, что монотонное отображение полной решётки на себя имеет хотя бы одну неподвижную точку (так как полная решётка не может быть пустой). Более того, такое отображение имеет наименьшую и наибольшую неподвижные точки[2].

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

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

Примечания[править | править вики-текст]

  1. Tarski, A. A Lattice-Theoretical Fixpoint Theorem and Its Applications // Pacific J. Math.. — 1955. — № 5. — С. 285-309.
  2. Roland Uhl. Tarski's Fixed Point Theorem (англ.) на сайте Wolfram MathWorld.

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

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