Нехай D —
ω
{\displaystyle \omega }
φ
:
D
→
D
{\displaystyle \varphi :D\to D}
нерухома точка
φ
{\displaystyle \varphi }
l
f
p
φ
{\displaystyle lfp\ \varphi }
l
f
p
φ
=
⨆
i
∈
ω
φ
(
i
)
(
⊥
)
{\displaystyle lfp\ \varphi =\bigsqcup _{i\in \omega }\varphi ^{(i)}(\perp )}
де
φ
(
0
)
(
⊥
)
=⊥
φ
(
i
+
1
)
(
⊥
)
=
φ
(
φ
(
i
)
(
⊥
)
)
,
i
∈
ω
{\displaystyle \varphi ^{(0)}(\perp )=\perp \ \varphi ^{(i+1)}(\perp )=\varphi (\varphi ^{(i)}(\perp )),\,i\in \omega }
Альфред Тарський сформулював теорему в її найзагальнішій формі[ 1]
Доведення складається з трьох частин:
Доведення факту, що множина
{
φ
(
i
)
(
⊥
)
}
i
∈
ω
{\displaystyle \{\varphi ^{(i)}(\perp )\}i\in \omega }
⨆
i
∈
ω
φ
(
i
)
(
⊥
)
{\displaystyle \bigsqcup _{i\in \omega }\varphi ^{(i)}(\perp )}
Доведення того, що
⨆
i
∈
ω
φ
(
i
)
(
⊥
)
{\displaystyle \bigsqcup _{i\in \omega }\varphi ^{(i)}(\perp )}
φ
{\displaystyle \varphi }
Доведення, що
⨆
i
∈
ω
φ
(
i
)
(
⊥
)
{\displaystyle \bigsqcup _{i\in \omega }\varphi ^{(i)}(\perp )}
φ
{\displaystyle \varphi }
Множина D —
ω
{\displaystyle \omega }
ω
{\displaystyle \omega }
↑ Tarski, Alfred (1 червня 1955). A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics . 5 (2): 285—309. doi :http://dx.doi.org/10.2140/pjm.1955.5.285 .
Нікітченко, М.С. (2010). ТЕОРІЯ ПРОГРАМУВАННЯ . Ніжин: Видавництво НДУ імені Миколи Гоголя. Weisstein, Eric W. Tarski's Fixed Point Theorem . mathworld.wolfram.com (англ.) . Процитовано 31 березня 2024 .
