クリーネの不動点定理

数学の順序理論や束論におけるクリーネの不動点定理（クリーネのふどうてんていり、Kleene fixed-point theorem）とは、スティーヴン・コール・クリーネによって導入された以下の定理である。

最小元を持つ ω-完備半順序 $(L,\sqsubseteq )$ 上のスコット連続関数 $f:L\to L$ は最小不動点を持ち、それは $f$ のクリーネ鎖の上限に一致する。

ここで、$f$ のクリーネ鎖とは、$L$ の最小元 $\bot$ に $f$ を繰り返し適用することで得られる以下の鎖のことである。

$\bot \sqsubseteq f(\bot )\sqsubseteq f(f(\bot ))\sqsubseteq \cdots \sqsubseteq f^{n}(\bot )\sqsubseteq \cdots$

最小不動点を ${\textrm {lfp}}$ と書くことにすると、本定理は次式で表すことができる。

${\textrm {lfp}}(f)=\sup \left(\left\{f^{n}(\bot )\mid n\in \mathbb {N} \right\}\right)$

本定理はしばしばアルフレト・タルスキによるものと誤解されるが、本定理は不動点の具体的な構成方法を与えているという点でタルスキの不動点定理（こちらは完備束上の単調関数に関する定理である）とは異なるものである。

証明

はじめに、$L$ における $f$ のクリーネ鎖の存在性を示す。 $\bot$ の最小性より $\bot \sqsubseteq f(\bot )$ が成り立つので、この両辺に単調関数 $f$ （スコット連続関数はすなわち単調である）を繰り返し適用することで以下の通りクリーネ鎖 $\mathbb {M}$ が得られる。

$\bot \sqsubseteq f(\bot )\sqsubseteq f(f(\bot ))\sqsubseteq \cdots \sqsubseteq f^{n}(\bot )\sqsubseteq \cdots$

これは ω-完備半順序上の ω-鎖であるから、上限 $\sup(\mathbb {M} )$ を持つ。

続いて、$\sup(\mathbb {M} )$ が $f$ の不動点であることを示す。 これは $f$ のスコット連続性より次式の通り示される。（この式の最後の等号は $\bot \sqsubseteq f(\bot )$ より成り立つ）

$f(\sup(\mathbb {M} ))=f(\sup(\{\bot ,f(\bot ),f(f(\bot )),\ldots \}))=\sup(\{f(\bot ),f(f(\bot )),f(f(f(\bot ))),\ldots \})=\sup(\mathbb {M} )$

最後に、$\sup(\mathbb {M} )$ が $f$ の最小不動点であることを示す。 $f$ の任意の不動点 $k$ を取ると、$\bot$ の最小性より $\bot \sqsubseteq k$ が成り立つ。 この両辺に単調関数 $f$ を繰り返し適用すると $f^{n}(\bot )\sqsubseteq f^{n}(k)$ ($n\in \mathbb {N}$) が得られるが、$k$ は $f$ の不動点であるからすなわち $f^{n}(\bot )\sqsubseteq k$ が成り立つ。 よって $\mathbb {M}$ は $k$ 以下の元からなる鎖であり、$\sup(\mathbb {M} )$ はその上限であるから、$\sup(\mathbb {M} )$ もまた $k$ 以下である。 斯くして $\mathbb {M}$ が $f$ の最小不動点であることが示された。

関連項目

• タルスキの不動点定理
• その他の不動点定理