Knaster-Tarskiの定理
[math] \newcommand{\mathsetextension}[1]{% \left\{ #1 \right\}% } \newcommand{\mathsetintension}[2]{% \left\{ #1 \left| #2 \right.\right\}% } \newcommand{\mathof}[2]{% \mathop{#1}\left(#2\right)% } \newcommand{\mathderiv}{\mathrel{\mathop{\Rightarrow}^{*}}} \newcommand{\mathgen}{\rightsquigarrow} \newcommand{\mathgenfun}[1]{\mathbf{#1}} \newcommand{\mirrorim}[1]{\overleftarrow{#1}} \newcommand{\emptyword}{\varepsilon} \newcommand{\kleenecl}[1]{{#1}^{*}} \newcommand{\inverse}[1]{{#1}^{-1}} \newcommand{\interpret}[1]{[\![#1]\!]} \newcommand{\mathautomaton}[1]{\mathcal{#1}} \newcommand{\mathnat}{\mathbb{N}} \newcommand{\mathcountfunc}{\mathop{\#}} \newcommand{\mathsup}{\mathop{\sqcup}} \newcommand{\mathinf}{\mathop{\sqcap}} \newcommand{\mathprefix}[1]{\mathop{\mathrm{PreFix}_{#1}}} \newcommand{\mathpostfix}[1]{\mathop{\mathrm{PostFix}_{#1}}} \newcommand{\mathlfp}[1]{\mathop{\mathrm{lfp}_{#1}}} \newcommand{\mathgfp}[1]{\mathop{\mathrm{gfp}_{#1}}} \newcommand{\qed}{\blacksquare} [/math]
Knaster-Tarskiの定理とは代表的な不動点定理の一つである。
Knaster-Tarskiの定理
定理 1 (Knaster-Tarskiの定理)
$\left(L, \leq \right)$ を完備束，$\varphi\colon L\to L$ を単調写像とする． このとき，$\left(L, \leq \right)$ についての最小不動点 $\mathlfp{\varphi}$，最大不動点 $\mathgfp{\varphi}$が存在し，次が成り立つ． \begin{align*} \mathlfp{\varphi}&=\mathinf\mathsetintension{x\in L}{\mathof{\varphi}{x}\leq x} \\ \mathgfp{\varphi}&=\mathsup\mathsetintension{x\in L}{x\leq \mathof{\varphi}{x}} \end{align*}
Proof.
$\mathlfp{\varphi}=\mathinf\mathsetintension{x\in L}{\mathof{\varphi}{x}\leq x}$ を示す． 以下 $\mathprefix{\varphi}=\mathsetintension{x\in L}{\mathof{\varphi}{x}\leq x}$，$p=\mathinf\mathsetintension{x\in L}{\mathof{\varphi}{x}\leq x}$ と書くことにする．
$\mathof{\varphi}{p}$ が $\mathprefix{\varphi}$ の下界になっていること，つまり，任意の $x\in\mathprefix{\varphi}$ について，$\mathof{\varphi}{p}\leq x$ を示す．
$x\in\mathprefix{\varphi}$ を固定する．定義から $p\leq x$ である．$\varphi$ は単調写像なので，$\mathof{\varphi}{p}\leq \mathof{\varphi}{x}$．$x\in\mathprefix{\varphi}$ より，$\mathof{\varphi}{p}\leq \mathof{\varphi}{x}\leq x$．
$\mathof{\varphi}{p}$ が $\mathprefix{\varphi}$ の下界になっていることから，$\mathof{\varphi}{p}\leq p$．よって，特に $p\in\mathprefix{\varphi}$．
$\mathof{\varphi}{p}\leq p$ と $\varphi$ が単調写像であることから $\mathof{\varphi}{\mathof{\varphi}{p}}\leq \mathof{\varphi}{p}$．よって $\mathof{\varphi}{p}\in\mathprefix{\varphi}$．$p$ の最小性から，$p=\mathof{\varphi}{p}$．ゆえに，$p$ は不動点． $p$ が最小不動点になることは，任意の不動点が $\mathprefix{\varphi}$ の元であることと $p$ の定義から明らかである．
$\mathgfp{\varphi}=\mathsup\mathsetintension{x\in L}{x\leq \mathof{\varphi}{x}}$ は同様に示すことができる．
□
