Русская Википедия:Теорема Кнастера — Тарского
Теорема Кнастера — Тарского (теорема Тарского) — теорема в теории решёток, впервые сформулированная в частном случае Брониславом Кнастером и обобщенная Альфредом Тарским[1]. Утверждает, что для любого монотонного отображения <math>f: L \to L</math> полной решётки <math>\langle L, \sqsubseteq \rangle</math> (то есть такого, что <math>l_1 \sqsubseteq l_2 \Rightarrow f(l_1) \sqsubseteq f(l_2)</math>) множество всех неподвижных точек <math>\mathrm{Fix}(f) = \{l \in L \mid f(l) = l\}</math> также является полной решёткой.
Результат используется в теоретической информатике, в частности, в работах по семантике языков программирования.
Из теоремы Кнастера — Тарского следует, что монотонное отображение полной решётки на себя имеет хотя бы одну неподвижную точку (так как полная решётка не может быть пустой). Более того, такое отображение имеет наименьшую и наибольшую неподвижные точки[2]. Теорема Клини о неподвижной точке утверждает, что для непрерывных по Скотту отображений (которые, как следствие непрерывности, являются монотонными) существует Шаблон:Iw. Кроме того, теорема Клини выполнена также для любых полных частичных порядков.
Примечания
Литература
- S. Abramsky, Dov M. Gabbay, T. S. E. Maibaum, Handbook of Logic in Computer Science: Volume 1: Background: Mathematical Structures
