はじめに
はじめまして。記事を開いていただきありがとうございます。
一般に、方程式は不動点を求める事ができれば解を求めることができます。
例：二次方程式
実数上の関数に対して、その（最小）不動点を求める部分関数を\mathrm{fix}\colon(\mathbb R\to\mathbb R)\rightharpoonup\mathbb Rとする。
（\rightharpoonupで部分関数を表すとし、\mathrm{fix}は不動点を持つ関数のみを定義域に持つとする。）
そのとき、f\colon\mathbb R\to\mathbb Rをf(x)=x^2+4x-1とすれば、\mathrm{fix}(f)は二次方程式x^2+3x-1=0の解の一つである。
実際、a=\mathrm{fix}(f)はfの（最小）不動点であるため、a^2+4a-3=a、すなわち、a^2+3a-3=0を満たします。
すると、関数の再帰的定義も関数方程式であるとみなすことで、不動点により解が得られます。
例：関数の再帰的定義
自然数上の関数\mathrm{fact}\colon\mathbb N\to\mathbb Nを次で定める。
\mathrm{fact}(n)=\left\{\begin{array}{ll}
1 & \text{ if }n=0 \\
n\times\mathrm{fact}(n-1) & \text{ otherwise}
\end{array}\right.
これは関数\mathrm{fact}\colon\mathbb N\to\mathbb Nの関数方程式と見なすことで、不動点として\mathrm{fact}が得られるのでは無いかと考えられます。
条件分岐があるのに関数方程式？
条件分岐が気になる方は、次のように考えてください。
まず、関数\mathrm{isZero}\colon\mathbb N\to\mathbb Nを\mathrm{isZero}(n)\coloneqq\frac{1-n+|1-n|}{2}で定義します。
そうすると、\mathrm{isZero}(n)は次のようになります。
\mathrm{isZero}(n)=\left\{\begin{array}{ll}
1 & \text{ if }n=0 \\
0 & \text{ otherwise}
\end{array}\right.
この関数\mathrm{isZero}を用いることで、先ほどの式は次のように書き直すことができ、条件分岐を取り除くことができます。
\mathrm{fact}(n)=\mathrm{isZero}(n)\times 1\quad+\quad(1-\mathrm{isZero}(n))\times n\times\mathrm{fact}(n-1)
実際、再帰的定義を持つ言語の意味論や関数の再帰的定義において、この不動点の考え方が用いられております。
しかし、不動点と言っても一つとは限りません。どの不動点を採用するかは個人の自由なはずです。
なのに、何故か最小の不動点が採用されることが一般的となっております。
確かに、最小性は非常に便利です。実際、再帰的定義の一意性の証明において、最小性が非常に重要な役割を果たしています。
また、領域理論においてx\le yというのはyの方がより多くの情報を保持することを意味します。
その観点で言えば、数学においてはできる限り最小の情報を用いた定義が好まれるという共通認識が存在するため、最小不動点を採用するのは合理的に思えます。
さらに、最小不動点を取る関数\mathrm{fix}_D\colon[D\to D]\to Dは\mathrm{fix}_D(f)=\sqcup_{n\in\mathbb N}f^n(\bot_D)という非常に簡単な表示を持つため、とても扱いやすいです。
しかし、どうしても今ひとつ数学的な根拠付けが足りないように思えます。
つまり、最小不動点だけが満たしてくれる何らかのキレイな数学的性質がない限りは「それってただの好みだよね？」に反論できなくなってしまいます。
そこで、この記事ではGunter, ScottによるSemantic Domainsにおいて紹介されている、最小不動点を取る関数のみが満たすuniformityという性質を紹介し、その証明を行っていこうと思います。
よろしくお願いします。
定義1: 不動点演算子
各dcpo Dに対し、次を満たすF_D\colon[D\to D]\to Dを返すFを不動点演算子という。
（ただし、[D\to D]\coloneqq\{f\colon D\to D\mid f\text{ is continuous}\}とした。）
\forall f\in[D\to D], F_D(f)=f(F_D(f))
不動点演算子について、uniformityという性質を定義します。
不動点演算子Fが次を満たすとき、Fはuniformであるという。
下の図式を可換にするような任意のf\in[D\to D], g\in[E\to E], h\in[D\Rightarrow E]に対して、次を満たす。
（[D\Rightarrow E]でストリクトな連続関数、すなわち、最小元を必ず最小元に移す連続関数の集合を表すとする。）
f, g, hが満たす図式：
\begin{matrix}
D & \xrightarrow{f} & D \\
\mathop\downarrow{h} & & \mathop\downarrow{h} \\
E & \xrightarrow{g} & E
\end{matrix}
（結局uniformityとは何なのかについては、「おわりに」で私個人の感想を述べております。）
このとき、不動点演算子\mathrm{fix}はuniformとなります。
\mathrm{fix}を最小不動点を取る不動点演算子とする。そのとき、\mathrm{fix}はuniformである。
証明
uniformityの条件を満たすf\in[D\to D], g\in[E\to E], h\in[D\Rightarrow E]を取る。
\begin{array}{rcl}
h(\mathrm{fix}_D(f)) & = & h(\sqcup_{n\in\mathbb N}f^n(\bot_D)) \\
& = & \sqcup_{n\in\mathbb N}h(f^n(\bot_D)) \\
& = & \sqcup_{n\in\mathbb N}g(h(f^{n-1}(\bot_D))) \\
& \vdots & \\
& = & \sqcup_{n\in\mathbb N}g^n(h(\bot_D)) \\
& = & \sqcup_{n\in\mathbb N}g^n(\bot_E) \\
& = & \mathrm{fix}_E(g)
\end{array}
（一応厳密には、h(f^n(\bot_D))=g^n(h(\bot_D))\text{ for all }n\in\Nは数学的帰納法で示す必要があります。）
\square
さらに重要なことに、uniformityを満たす不動点演算子は\mathrm{fix}のみであることが示せます。
uniformityを満たす不動点演算子は\mathrm{fix}のみである。
証明
dcpo Dと連続関数f\in[D\to D]を固定し、D'=\{x\in D\mid x\le\mathrm{fix}_D(f)\}\subseteq Dとする。
すると、明らかにD'はDの順序においてdcpoをなす。さらに、f'=f|_{D'}\in[D'\to D']、つまり、fのD'への制限をf'とする。
そのとき、f'は\mathrm{fix}_D(f)のみを不動点に持つ。なぜなら、f'の不動点は常にfの不動点にもなるため、f'が他に不動点を持っていたら\mathrm{fix}_D(f)の最小性に反する。
今、包含写像i\colon D'\to Dはストリクトな連続関数であり、さらに次を可換にする。
\begin{matrix}
D' & \xrightarrow{f'} & D' \\
\mathop\downarrow{i} & & \mathop\downarrow{i} \\
D & \xrightarrow{f} & D
\end{matrix}
今、Fをuniformな不動点演算子とすれば、uniformityの定義よりF_D(f)=F_{D'}(f')だが、f'の不動点は\mathrm{fix}_D(f)しかないことより、F_D(f)=\mathrm{fix}_D(f)が言える。
\square
おわりに
お疲れ様でした。ここまで読んでいただきありがとうございました。
今回は、不動点意味論でなぜ最小の不動点を取るのかという疑問について、uniformityという観点から解説を行いました。
最後に、uniformityとは結局何なのかについて、私個人の感想を述べてみることにします。
ストリクトな連続関数h\in[D\Rightarrow E]は、dcpoとしてのDの構造をすべて保存します。
すなわち、dcpoを (D, \le_D, \bot_D, \sqcup_D)という構造付きの集合だとみなしたとき、すべての構造を保存することになります。
さらに、不動点演算子Fに対して、関係R^D\subseteq D\times[D\to D]を
(x, f)\in R^D\iff x=F_D(f)
と定義すれば、uniformityは次のような条件だと考えることができそうです。
(x, f)\in R^D\implies (hx, hf)\in R^E
これは、代数における準同型と同じ形をしていますね。
群における準同型
群Gにおける関係R_1^G, R_2^G, R_3^Gを次で定義する。
\begin{array}{rcl}
(a, b, c)\in R_1^G & \iff & a = b\cdot_Gc \\
(a, b)\in R_2^G & \iff & a=b^{{-1}_G} \\
a\in R_3^G & \iff & a=e_G
\end{array}
そのとき、h\colon G\to Hが準同型であるとは、群のすべての構造R_1, R_2, R_3を保存することである。すなわち、次をすべて満たすことである。
\begin{array}{rcr}
(a, b, c)\in R_1^G & \implies & (ha, hb, hc)\in R_1^H \\
(a, b)\in R_2^G & \implies & (ha, hb)\in R_2^H \\
a\in R_3^G & \implies & ha\in R_3^H
\end{array}
つまり、uniformityは、「不動点演算子もストリクトな連続関数に保存される構造の一つである」ということを要請する性質です。
言い換えれば、uniformityの要請というのは、不動点演算子もdcpo固有の構造の一つではないだろうかという領域理論に対する提唱だとも考えられます。
このような観点から考えれば、dcpoとは(D, \le_D, \bot_D, \sqcup_D, \mathrm{fix}_D)という構造付き集合であると見なす事もできます。
私は、「領域理論の基本定理とは何か？」と聞かれれば、迷うことなく連続関数の不動点定理を挙げます。
しかし、これはdcpoの定理ではなくdcpoの定義なのではないかと考えてみると面白いかもしれませんね。
改めて、本当にありがとうございました。
Discussion