Knaster-Tarski theorem
準備
半順序集合$ Xについて、$ f: X \to Xを$ \leq について単調な関数とする。
$ x \in Xが $ f(x) \leq x を満たすとき、$ xを$ fの前不動点 (pre-fixed point)と言う。
$ x \in Xが $ f(x) = x を満たすとき、$ xを$ fの不動点(fixed point)と言う。
$ x \in Xが $ x \leq f(x) を満たすとき、$ xを$ fの後不動点 (post-fixed point)と言う。
TaPLの21章では、以下の議論を含め$ Xを普遍集合$ \mathcal Uの冪集合$ \mathcal P(\mathcal U)、順序$ \leqを包含関係$ \subseteqとしている。このとき$ Xは完備束。また、pre-fixed pointであるような$ xを$ fについて閉じている (closed)、post-fixed pointであるような$ xを$ fについて整合的である (coherent) と表現している。
主張
$ Xを順序$ \leqによる完備束とする。$ f: X \to Xを$ \leq について単調な関数とする。以下の主張が成り立つ。
(1) $ fのすべてのpre-fixed pointからなる集合の交わりは$ fの最小不動点。
(2) $ fのすべてのpost-fixed pointからなる集合の結びは$ fの最大不動点。
(3) $ fのすべてのfixed pointからなる集合は完備束。
(1)および(2)は、$ fの最小不動点を$ \mu f、最大不動点を$ \nu fとして$ \mu f = \bigwedge\left\{x \mid f(x) \leq x\right\}、$ \nu f = \bigvee\left\{x \mid x \leq f(x)\right\}と書ける。元のTarskiの論文の主張は(3)だが、TaPLは主要な結果である(1)、(2)だけを使っている。 証明
(1) $ C=\left\{x \mid f(x) \leq x\right\}とする。
$ \wedge Cが$ fの不動点であることを示す。$ Cの任意の$ x\in Cについて、
交わりの定義から$ \wedge C \leq xであり、さらに$ fの単調性から$ f(\wedge C) \leq f(x)
また、$ Cの定義から$ f(x) \leq x
以上より任意の$ x\in Cについて$ f(\wedge C)\leq xであるから、$ f(\wedge C)\leq \wedge Cである。
さらに$ fの単調性から$ f(f(\wedge C))\leq f(\wedge C)。よって$ f(\wedge C)は$ fのpre-fixed point、すなわち$ f(\wedge C) \in Cである。よって交わりの定義から$ \wedge C \leq f(\wedge C)。
したがって$ f(\wedge C)=\wedge C、すなわち$ \wedge Cは不動点である。
ここで、$ fのすべてのfixed pointはpre-fixed pointであり、$ \wedge Cはすべてのpre-fixed pointのうち最小のものであるから、$ \wedge Cは最小不動点である。
(2) (1)と同様
(3) 省略
その他
(1) 対象をposet$ Xの要素、対象$ x, y間の射を$ x \leq yのときに$ x\to yであるとした圏において、単調な関数$ fは自己関手$ Fに相当する。集合$ C = \{x\mid f(x)\leq x\}に交わり$ \mu f = \wedge Cが存在することは、$ Fに始代数$ F\mu F\to \mu Fが存在することに相当し、このときLambek's theorem から$ F\mu Fと$ \mu Fは同型である（Knaster-Tarskiと同様な議論）。よって$ \mu Fは$ Fの最小不動点。 参考
TaPLの定理21.1.4 (222ページ)
プログラム意味論（横内）練習問題3.4.2