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

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

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

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

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

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

Следствия

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

Связанные результаты

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

Примечания

  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
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.