WikiSort.ru - Не сортированное

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

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

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

Пусть ${\displaystyle \langle L,\sqsubseteq \rangle }$  — полная решётка, а отображение ${\displaystyle f:L\to L}$  — монотонно, то есть сохраняет отношение порядка: ${\displaystyle l_{1}\sqsubseteq l_{2}\Rightarrow f(l_{1})\sqsubseteq f(l_{2})}$ , то множество всех неподвижных точек:

${\displaystyle \mathrm {Fix} (f)=\{l\in L\mid f(l)=l\}}$

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

Следствия

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

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

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

Примечания

Литература

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

Для улучшения этой статьи желательно: Проставить для статьи более точные категории.