Теорема Кнастера — Тарского
Теорема Кнастера — Тарского (теорема Тарского) — теорема в теории решёток, впервые сформулированная в частном случае Брониславом Кнастером и обобщенная Альфредом Тарским[1]. Утверждает, что для любого монотонного отображения [math]\displaystyle{ f: L \to L }[/math] полной решётки [math]\displaystyle{ \langle L, \sqsubseteq \rangle }[/math] (то есть такого, что [math]\displaystyle{ l_1 \sqsubseteq l_2 \Rightarrow f(l_1) \sqsubseteq f(l_2) }[/math]) множество всех неподвижных точек [math]\displaystyle{ \mathrm{Fix}(f) = \{l \in L \mid f(l) = l\} }[/math] также является полной решёткой.
Результат используется в теоретической информатике, в частности, в работах по семантике языков программирования.
Из теоремы Кнастера — Тарского следует, что монотонное отображение полной решётки на себя имеет хотя бы одну неподвижную точку (так как полная решётка не может быть пустой). Более того, такое отображение имеет наименьшую и наибольшую неподвижные точки[2]. Теорема Клини о неподвижной точке утверждает, что для непрерывных по Скотту отображений (которые, как следствие непрерывности, являются монотонными) существует наименьшая неподвижная точка. Кроме того, теорема Клини выполнена также для любых полных частичных порядков.
Примечания
- ↑ Tarski, A. A Lattice-Theoretical Fixpoint Theorem and Its Applications // Pacific J. Math.. — 1955. — № 5. — С. 285—309.
- ↑ 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