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

Теорема Кнастера — Тарского (теорема Тарского) — теорема в теории решёток, впервые сформулированная в частном случае Брониславом Кнастером и обобщенная Альфредом Тарским. Утверждает, что для любого монотонного отображения $f:L\to L$ полной решётки $\langle L,\sqsubseteq \rangle$ (то есть такого, что $l_{1}\sqsubseteq l_{2}\Rightarrow f(l_{1})\sqsubseteq f(l_{2})$) множество всех неподвижных точек $\mathrm {Fix} (f)=\{l\in L\mid f(l)=l\}$ также является полной решёткой.

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

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

Литература

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