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

Теорема Кнастера — Тарского (теорема Тарского) — теорема в теории решёток, впервые сформулированная в частном случае Брониславом Кнастером и обобщенная Альфредом Тарским. Утверждает, что для любого монотонного отображения $f:L\to L$ полной решётки $⟨L,⊑⟩$ (то есть такого, что $l_1⊑l_2\Rightarrow f(l_1)⊑f(l_2)$) множество всех неподвижных точек $\mathrm{F}\mathrm{i}\mathrm{x}(f)=\{l\in L\mid f(l)=l\}$ также является полной решёткой.

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

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

Литература

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