Knaster-Tarskiの不動点定理
参考文献
モチベーション
Def: 一般の不動点
半順序集合$ Xと，$ X上の関数$ f:X \to X 前不動点，後不動点，不動点
$ x \in Xが$ f(x) \leq xを満たすとき，$ xは$ fの前不動点(pre-fixed point) 前不動点の集合を$ \mathrm{Pre}(f)とする．
$ x \in Xが$ x \leq f(x)を満たすとき，$ xは$ fの後不動点(post-fixed point) 後不動点の集合を$ \mathrm{Pos}(f)とする．
$ xが$ fの前不動点かつ後不動点であるとき，$ xは不動点(fixed point) すなわち$ x \in Xが$ f(x) = xを満たす
最小不動点，最大不動点
$ \leqの意味で
最小の$ fの不動点を最小不動点$ \mathrm{LFP}(f)(least fixed point) 最大の$ fの不動点を最大不動点$ \mathrm{GFP}(f)(greatest fixed point) Def: 冪集合上の不動点
非空集合$ S．$ f:2^S \to 2^Sは$ \subeとして要件を満たす．
$ \mathrm{Pre}(f) \coloneqq \{ A \in 2^S \mid f(A) \sube A \}
$ \mathrm{Pos}(f) \coloneqq \{ A \in 2^S \mid f(A) \supe A \}
注意
少なくとも$ Sは前不動点て，$ \emptysetは後不動点．
注意
$ f: 2^S \to 2^Sが$ X \sube Y \implies f(X) \sube f(Y)のとき$ fが単調(Monotone)と呼ぶ．
非空集合$ Sと単調な関数$ f:2^X \to 2^Xについて
I. $ \mathrm{LFP}(f) \coloneqq \bigcap \mathrm{Pre}(f)
II. $ \mathrm{GFP}(f) \coloneqq \bigcup \mathrm{Pos}(f)
証明
Iについて証明する．IIについても同様に．
$ P = \bigcap \mathrm{Pre}(f)とする．
1~6より$ Pは最小の前不動点．
1. 任意の前不動点$ Aに対して$ P = \bigcap \mathrm{Pre}(f) \sube A
2. $ fの単調性より$ f(P) \sube f(A)
3. $ Aは前不動点であるので$ f(A) \sube A
4. 2,3より$ f(P) \sube A
5. $ A \in \mathrm{Pre}(f)であるので$ f(P) \sube \bigcap \mathrm{Pre}(f) = P．すなわち$ f(P) \sube P
6. $ Pは全ての前不動点の共通集合であるので最小．
7~9より$ Pは後不動点である
7. $ Pが前不動点かつ$ fが単調なので，$ f(f(P)) \sube f(P)
8. 7より$ f(P)は前不動点．
9. $ Pが最小の不動点であるので，$ P \sube f(P)が成立する．
よって$ Pは不動点である．
任意の不動点は前不動点であるので，最小の不動点は最小の前不動点でもある．