はじめに
はじめまして。記事を開いていただきありがとうございます。
いくつかの引数で未定義となる関数を部分関数といい、すべての引数で値が定義されている関数を全域関数と言います。
ところで、計算可能性理論においては1つの関数は1つのアルゴリズムに対応しており、停止しないアルゴリズムの表現として部分関数が自然な形で登場します。
しかし、領域理論はこのような「部分関数と"全域的な"引数」という構図と真逆のアプローチを取ります。
領域理論には未定義を表す最小元\botが存在し、関数自体は常に全域的です。
つまり、領域理論では「全域関数と"部分的な"引数」という一見不思議な構図が生まれます。
一般の領域において引数が"部分的"、また"全域的"とは何を意味するのでしょうか。
この記事では"全域的"な元を一般に定義することを目的に進めていきます。
よろしくお願いします。
前提知識
必要となる前提知識を証明無しで駆け足で説明します。領域理論をご存じの方は次の章までお進みください。
Scott領域
代数的cpoの関数空間に閉じる部分クラスとしてScott領域を導入します。
代数的dcpoまでの簡単な説明はこちらの記事を参照ください。
https://zenn.dev/mineel5/articles/d6bc627587b72b
まず、dcpo上の関数空間は次のように定義されます。
定義1: 関数空間
dcpo D, Eに対し、関数空間[D\rightarrow{E}]=([D\rightarrow{E}], \le)を次で定義する
- [D\rightarrow{E}]=\{f: D\rightarrow{E}\ |\ fは連続\}
-
f\le{g}\Leftrightarrow\forall{x}\in{D},\ f(x)\le{g}(x) (=各点順序)
有向集合F\in[D\rightarrow{E}]に対し、上限\sqcup{F}は各点毎の上限、すなわち(\sqcup{F})(x)=\sqcup_{f\in{F}}(f(x))と書けることが示されます。
また、ステップ関数を導入します。
定義2: ステップ関数
dcpo D, E及びd\in{D}, e\in{E}に対し、次の関数をステップ関数という
\begin{equation*}
<d; e>(x) =
\left\{
\begin{array}{ll}
e & if\ d\leq{x} \\
\bot_E & otherwise
\end{array}
\right.
:D\rightarrow{E}
\end{equation*}
ただし、\bot_Eはdcpo Eの最小元を表す
普通の意味でのステップ関数です。ステップ関数はdが有限なら連続であり、またd, eが有限なら<d; e>も有限です。
ステップ関数に関して、以下の事実は呼吸のように使われます。
命題3: ステップ関数の性質
f\in[D\rightarrow{E}]、d\in{D},e\in{E}に対し次が成り立つ
<d; e>\le{f}\Leftrightarrow e\le f(d)
連続関数が単調であることに気をつければ証明は非常に容易です。
ところで、代数的dcpo上の連続関数全体は一般に代数的とはなりません。
代数的dcpo上の各連続関数fはf以下の有限ステップ関数全体の上限として書けるのですが、一般にf以下の有限関数全体が有向集合を成すと限らず、それゆえ代数的dcpoは関数空間に閉じません。(惜しい！)
そこで、冒頭に述べた通り代数的dcpoの関数空間に閉じる部分クラスとしてScott領域を導入します。
定義4: Scott領域
上に有界な集合が常に上限を持つ時そのdcpoを有界完備であるという
有界完備な代数的dcpoをScott領域という
集合が上に有界であるとは、領域理論的にはその集合が無矛盾、整合的であることを意味します。
(部分関数が包含関係により成すdcpoを考えてみれば、2つの部分関数f, gが上に有界とは、f, gは引数が同じなら出力も同じであることと同値になることを考えれば納得できます。)
そこで、dcpo Dの部分集合X\subseteq{D}が上に有界であることを\operatorname{Con}(X)と書き、Xは無矛盾であると呼ぶこととします。
事実として、Scott領域上の連続関数空間における有限関数は必ず有限個の無矛盾な有限ステップ関数の上限として書くことができ、逆も言えます。
また、Scott領域上の連続関数fは、有向集合F=(f以下の有限ステップ関数の有限個の組み合わせの上限全ての集合)の上限として記述することができ、Scott領域は関数空間に閉じることとなります。
Scott位相
dcpoにはScott位相と呼ばれる自然な位相を導入することができます。
まず位相空間から順序を得るための特殊化順序を導入します。
定義5: 特殊化順序
位相空間X=(X, \mathcal{O})に対し、次で定義される二項関係\leq_X \subseteq X\times{X}をXの特殊化順序という
x\leq_X{y}\Leftrightarrow 「\forall{U}\in\mathcal{O}.\ x\in{U}\Rightarrow y\in{U}」
特殊化順序は一般に前順序ですが、元の位相空間XがT_0なら半順序になり、T_1なら自明な順序、つまり等号になります。
そこで、dcpo Dに対し自然に次を満たすような位相が欲しくなります。
- 特殊化順序で元の順序に戻る
- dcpo上の連続関数と対応する位相空間上の連続関数が一致する
これを満たすようにDへの位相の導入を試みます。
任意の位相空間X=(X, \mathcal{O})において、Xからシエルピンスキ空間\mathbb{S}=(\{0, 1\}, \{\emptyset, \{1\}, \{0, 1\}\})への連続写像はXの開集合と一対一対応します。
(U\mapsto\chi_U、f\mapsto f^{-1}(\{1\})、ただし\chi_UはUの特徴関数)
つまり、位相空間の世界では、\mathbb{S}から位相空間上の連続関数fを用いてf^{-1}(\{1\})により開集合が得られます。
\mathbb{S}の特殊化によりこれをdcpoの世界に持ちこんで同じことをします。
すなわち、\mathbb{S}の特殊化順序は0\leq1であることよりDの位相\sigma(D)を次で定義します。
定義6: Scott位相
dcpo Dに対し、以下の\sigma(D)\subseteq 2^DをDのScott位相という
\sigma(D)=\{f^{-1}(\{1\})\ |\ f:D\rightarrow\mathbb{S}は(cpoの意味で)連続 \}
ただし、
\mathbb{S} = (\{0, 1\}, \leq)、順序は0\leq0, 0\leq1, 1\leq1
\sigma(D)は実際にD上の位相になり、次のように特徴づけされます。
命題7: Scott位相の特徴付け
dcpo D及びU\subseteq{D}に対し、次の(1)、(2)は同値である
\begin{array}{ll}
(1) & U\in\sigma(D)\\
(2) & U\ is\ upward\ closed\ \&\ inaccessible\ by\ directed\ sup
\end{array}
ただし、
\begin{array}{ll}
(2)の前半 & \Leftrightarrow & \forall x, y\in{D}.\ x\in{U}\ \&\ x\leq{y}\Rightarrow y\in{U}\\
(2)の後半 & \Leftrightarrow & \forall{A}: directed.\ A\cap{U}=\emptyset\Rightarrow\sqcup{A}\not\in{U}
\end{array}
(2)の前半をAlexandrov条件といい、これより得られる位相をAlexandrov位相といいます。
また、(2)の後半をScott条件といいます。
Scott位相は期待通りの性質を持っています。すなわち、次が成り立ちます。
命題8:
(1) dcpoで連続\LeftrightarrowScott位相で連続
(2) dcpo上のScott位相から得られる特殊化順序は元のdcpoの順序に一致する
有限な元は、それより真に小さい元の上限として得られないため、dcpo Dの有限な元c\in\mathcal{K}(D)に対し、\operatorname{B}^D_c=\{y\in{D}\ |\ c\leq{y}\}は開集合となります。
(\mathcal{K}(D)でD上の有限な元全体の集合を表します。)
特に、有限な元cによるB_c全体の族はScott位相の開基底を成します。
全域的な元
平坦領域及び関数空間における全域性
領域理論においては、自然数上の部分関数は\mathbb{N}_\bot上のストリクトな連続関数として表現されます。
定義9: 平坦領域
集合Aに対し、平坦領域A_\botを次で定義する(ただし、\bot\not\in{A})
順序は、x, y\in{A_\bot}に対し、
x\leq{y}\Leftrightarrow x=\bot\ or\ x=y
dcpo D, E間のストリクトな(=最小元を保存する)連続関数全体を[D\Rightarrow{E}]と書きます。
また、集合A, B間の部分関数全体を(A\rightharpoonup{B})と書きます。
すると、明らかに次の事実が成り立ちます。
命題10: 部分関数空間
[\mathbb{N}_\bot\Rightarrow\mathbb{N}_\bot]\cong(\mathbb{N}\rightharpoonup\mathbb{N})
Proof:
f\in[\mathbb{N}_\bot\Rightarrow\mathbb{N}_\bot]に対し、
\begin{equation*}
g(x) =
\left\{
\begin{array}{ll}
f(x) & if\ f(x)\not=\bot \\
undefined & otherwise
\end{array}
\right.
\end{equation*}
g\in(\mathbb{N}\rightharpoonup\mathbb{N})に対し、
\begin{equation*}
f(x) =
\left\{
\begin{array}{ll}
g(x) & if\ x\in\operatorname{dom}(g) \\
\bot & otherwise
\end{array}
\right.
\end{equation*}
とすればよい
すなわち、平坦領域における最小元\botは対応する部分関数の未定義を表します。
なので、平坦領域においては\bot以外を"全域的な"元といって良さそうです。
これより一般の領域に極大元として"全域的な"元を一般化することができそうですが、果たしてそれでよいのでしょうか？
実は、関数空間においてはこの定義が怪しいことがわかります。
(後に「極大\Rightarrow"全域的"」は示せるのですが、逆は成り立ちません)
今、[\mathbb{N}_\bot\rightarrow\mathbb{N}_\bot]においては、fが\mathbb{N}の元を(\botではなく)\mathbb{N}に写す、つまりf(\mathbb{N})\subseteq\mathbb{N}を満たすときfを"全域"関数と言えそうです。
これを一般化して、領域D, Eの"全域的"な元全体M\subseteq{D}, N\subseteq{E}が定まっているとしたら、次に含まれる関数は"全域"関数になっていてほしいです。
<M, N> = \{f\in[D\rightarrow{E}]\ |\ f(M)\subseteq{N}\}
その時、f\in<\mathbb{N}, \mathbb{N}>が必ずしも極大元ではないことが言えます。
例11: "全域的"だが極大でない元
\begin{equation*}
f(x) =
\left\{
\begin{array}{ll}
0 & if\ x\not=\bot \\
\bot & otherwise
\end{array}
\right.
\in<\mathbb{N}, \mathbb{N}>
\end{equation*}
は定数関数0より真に小さい
一般の領域における全域性
関数空間の元の全域性を調べるために部分性テストを考えます。
定義12: 部分性テスト
次のp^{D, E}_{x, y}:[D\rightarrow{E}]\rightarrow\mathbb{T}_\botを[D\rightarrow{E}]上の部分性テストという
p^{D, E}_{x, y}(f) = \left\{
\begin{array}{ll}
true & if\ f(x)=y\ \&\ f(x)\not=\bot \\
false & if\ f(x)\not=y\ \&\ f(x)\not=\bot \\
\bot & if\ f(x)=\bot
\end{array}
\right.
f\in[\mathbb{N}_\bot\rightarrow\mathbb{N}_\bot]において言えば、全てのx, y\in\mathbb{N}で部分性テストをパスする、つまり\botを返さないことをfの全域性と言えそうです。
一般の元xに対しても、直感的にはxの全域性を「xがパスする部分性テストが"十分に多く"あること」として定義できないか考えていきたいです。
つまり、以下のことを考えていきます。
- 関数空間と限らない一般の領域Dの元x\in{D}に対して部分性テストをどのように定義するか
- 部分性テストが"十分に多く"あるとはどういうことか
部分性テストとしての開集合
位相空間論における開集合は、x\in{U}という言明を考えることで論理学的な言明を表すと考えられます。
特に、無限の和(=任意の存在量化)に閉じており、かつ有限の積(=有界な全称量化)に閉じていることから開集合は半決定可能な性質や観測可能な性質と言われることがあります。
今、論理学的な言明としての開集合Uは元xに対して、x\in{U}のとき言明U(x)を絶対的に真であるといい、Uと交わりを持たない異なる開集合Vに対してx\in{V}となるとき言明U(x)を絶対的に偽であるといいます。
さらに、U(x)が絶対的に真であるか絶対的に偽であるとき、つまりx\not\in\partial{U}のときU(x)を決定可能であるといい、xはUを決定するといいます。
(ただし、\partial{U}をUの境界とした。)
また、開集合の族\mathcal{F}\subseteq\sigma(D)に対しても、xが各U\in\mathcal{F}を決定するとき、xは\mathcal{F}を決定するといいます。
すると、一般の領域の元xに対しても、開集合を用いることで部分性テストを実現できるのではないかということに気が付きます。
そこで、次の命題を示します。
命題13:
\forall x, y\in\mathbb{N},\ p^{\mathbb{N}_\bot, \mathbb{N}_\bot}_{x, y}(f)\not=\bot\Leftrightarrow f\not\in\partial{B}^{[\mathbb{N}_\bot\rightarrow\mathbb{N}_\bot]}_{<x; y>}
Proof:
まず、一般に有限な元c\in\mathcal{K}(D)に対し、B^D_c=\{y\in{D}\ |\ c\leq{y}\}はScott位相\sigma(D)における開集合であることに注意する。
その時、x, y\in\mathbb{N}に対して、
\begin{array}{llll}
p_{x, y}(f)\not=\bot & \Leftrightarrow & f(x)=y & or & \exists{z}\in\mathbb{N},\ f(x)=z\not=y \\
& \Leftrightarrow & <x; y>\leq{f} & or & \lnot\operatorname{Con}(<x; y>, f) \\
& \Leftrightarrow & f\in{B}_{<x; y>} & or & \exists{V}:open,\ (f\in{V}\ \&\ V\cap{B}_{<x; y>}=\emptyset) \\
& \Leftrightarrow & f\not\in\partial{B}_{<x; y>}
\end{array}
\square
この結果をそのまま一般化して、各有限な元c\in\mathcal{K}(D)が生成する開集合B_cを部分性テストとすることができそうです。
そこで、xが決定する開集合が"十分に多く"あるということを定義していきます。
分離的な族
位相空間においては、分離性が各位相空間を特徴づける重要な性質を担います。
定義14: (位相的)分離性
位相空間X=(X, \mathcal{O})上の2点x, y\in{X}に対し、次のときx, yは(位相的に)分離可能という
\exists U, V\in\mathcal{O}:disjoint,\ x\in{U}\ \&\ y\in{V}
定義より、位相空間がハウスドルフなら任意の異なる2点は分離可能です。
Scott位相においては、位相的分離性を無矛盾性によって特徴づけることが可能です。
命題15: Scott位相における分離性の特徴づけ
領域D上の元x, y\in{D}に対し、次が成り立つ
\operatorname{Con}(x, y)\Leftrightarrow x, yは\sigma(D)において分離不能
Proof:
\Rightarrowについて:
Scott開集合は上方集合だった(=Alexandrov条件)ため、x, yに上界が存在したらx, yの開近傍は必ずその上界において交わりを持つ。
\Leftarrowについて:
一般に、x\in{D}に対し、\operatorname{app}(x)=\{c\in\mathcal{K}(D)\ |\ c\le{x}\}とする。
今、x, y\in{D}に対し、c_0\in\operatorname{app}(x), c_1\in\operatorname{app}(y)を取る。
B_{c_0}, B_{c_1}はそれぞれx, yの開近傍より交わりを持つ。
すなわち、c_0, c_1は無矛盾ゆえ、領域の有界完備性よりc_0\sqcup{c_1}がDに存在。
A=\{c_0\sqcup{c_1}\ |\ c_0\in\operatorname{app}(x), c_1\in\operatorname{app}(y)\}\subseteq{D}
とすると、Aは有向。
(\because\ 「c_0, c_0'\in\operatorname{app}(x)のときc_0\sqcup{c_0'}\in\operatorname{app}(x)」(※)より、(c_0\sqcup{c_1})\sqcup(c_0'\sqcup{c_1'})=(c_0\sqcup{c_0'})\sqcup(c_1\sqcup{c_1'})\in{A})
\bot\in\operatorname{app}(y)ゆえ、Aにおいてc_1=\botとすることで\operatorname{app}(x)\subseteq{A}が言え、\operatorname{app}(y)\subseteq{A}も同様。
よって、x, y\le\sqcup{A}より\operatorname{Con}(x, y)
\square
(※)の証明:
xによりc_0, c_0'は無矛盾よりc_0\sqcup{c_0'}がDに存在。
c_0\sqcup{c_0'}\le\sqcup{A}ならc_0, c_0'\le\sqcup{A}であり、c_0, c_0'の有限性より\exists a, a'\in{A},\ c_0\le{a}\ \&\ c_0'\le{a'}である。
A:有向より、a, a'の上界をa''\in{A}とすれば、c_0\sqcup{c_0'}\le{a''}\in{A}ゆえ、c_0\sqcup{c_0'}\in\mathcal{K}(D)
今、c_0\sqcup{c_0}'\le{x}は明らかより、c_0\sqcup{c_0}'\in\operatorname{app}(x)
そこで、開集合族\mathcal{F}\subseteq\mathcal{O}における開集合の"豊富さ"を点を分離する能力により特徴付けることとします。
定義16: 分離的な族
位相空間X=(X, \mathcal{O})上の開集合族\mathcal{F}\subseteq\mathcal{O}は次を満たすとき分離的であるという
\forall x, y\in{X}: separable,\ \exists U, V\in\mathcal{F}: disjoint,\ x\in{U}\ \&\ y\in{V}
つまり、点を分離する能力が開集合すべてを用いる場合と比べても十分であることを保証する定義です。
容易に、開基底は常に分離的であることが従います。
(逆は成り立たなそうな気がしているのですが、当方位相空間論に疎いため反例を思いついていません。分かる方がいましたらお教えいただけると幸いです。)
そこで、一般の領域の元の全域性を次のように定義します。
x\in{D}が決定する開集合全体を\mathcal{F}_x\subseteq\sigma(D)とし、M\subseteq{D}の全ての元により決定される開集合全体を\mathcal{F}_Mとします。
(つまり、\mathcal{F}_M=\{U\in\sigma(D)\ |\ \forall{x}\in{M},\ xはUを決定する\}とします。)
定義17: 全域性
領域D上の元x\in{D}は、\mathcal{F}_xが\sigma(D)において分離的であるとき、全域的であるという
また、集合M\subseteq{D}は、\mathcal{F}_Mが\sigma(D)において分離的であるとき、全域的であるという
全域的な元の集合が必ず全域的とは限りませんが、全域的な集合の元は必ず全域的となります。
極大元と全域元
最後に、極大元の集合が全域集合であることを示します。
命題20: 極大元と全域元の関係
領域Dに対し、次が成り立つ
x\in{D}_m\Leftrightarrow xは\{B_c\ |\ c\in\mathcal{K}(D)\}を決定する
ただし、D上の極大元全体の集合をD_mとした
Proof:
\Rightarrowについて:
\forall x\in{D}_m,\ \forall c\in\mathcal{K}(D),\ x\not\in\partial{B}_cを示す。次を示せば十分。
\forall x\in{D}_m,\ \forall c\in\mathcal{K}(D),\ x\not\in B_c\Rightarrow\exists c'\in\mathcal{K}(D),\ x\in B_{c'}\land B_c\cap B_{c`}=\emptyset
まず、x:極大より、x\not\in{B}_cから\lnot\operatorname{Con}(x, c)が言える。
命題15より、x, cは分離可能より、x, cを分離する交わりのない開集合をそれぞれU, Vとする。
まず、c\in{V}:openより開集合のAlexandrov条件(=上方性)よりB_c\subseteq{V}となる。
また、各\{B_c\ |\ c\in\mathcal{K}(D)\}は開基底より、\exists c'\in\mathcal{K}(D),\ x\in{B}_{c'}\subseteq{U}となる。
U\cap{V}=\emptysetより、B_{c'}\cap{B}_c=\emptyset
\Leftarrowについて:
x\not\in{D}_mとし、対偶を示す。
y\gt xに対しc\in\operatorname{app}(y)\backslash\operatorname{app}(x)\not=\emptysetを取ると、y\in{B}_c, x\not\in{B}_cである。
次を示せば、x\in\partial{B}_cゆえ題意は示せる。
\forall x\le y\in{D}, \forall{U}\in\sigma(D),\ y\in{U}\Rightarrow x\in{U}\cup\partial{U}
実際、D\backslash(U\cup\partial{U}):開集合より、x\not\in{U}\cup\partial{U}とするとAlexandrov条件からy\not\in{U}\cup\partial{U}となり矛盾。
\square
つまり、\mathcal{F}_{D_m}=\{B_c\ |\ c\in\mathcal{K}(D)\}は開基底ゆえ分離的より、D_mは全域的。
おわりに
お疲れ様でした。ここまで読んでいただきありがとうございました。
当初はもう少し先の内容まで書こうとしていたのですが、基本的にここでの記事は濃すぎる内容よりは気軽に雰囲気を感じられる記事を想定していたため、定義だけして終わるという少し中途半端なオチとなってしまいました。
(気力が保てなかったことも大きな要因です、、)
ここで記事は終わりですが、以下で少しだけ先の話を続けます。
興味のある方だけ読んでくださると嬉しいです。
改めて本当にありがとうございました。
稠密性定理
ここまでで全域集合を定義しましたが、実際にはこの先では(通常の意味での)稠密性も考慮して、全域稠密集合を考え、稠密性定理なる定理まで示す予定でした。
全域稠密集合は、積の構成に閉じていることが示されますが、稠密性定理は全域稠密集合が関数の構成にも閉じていることを保証する定理で、証明自体は難しいものではありません。
また、元々の一般の領域における全域集合を定義するモチベーションは、一般計算可能性理論(?)におけるKreisel-KleeneのContinuous functionalsの領域理論版を考えることでした。
私は計算可能性理論に詳しくないため領域理論の文脈で初めて出会ったのですが、既に整備された理論らしく参考文献に教科書[3]を載せておきます。
実は、稠密性定理はContinuous functionalsの文脈でも示されており、上述の稠密性定理はその領域理論版とも言える定理となっておりました。
領域理論と計算理論の対比
以下はただの感想です。
計算のモデル化の違い
この繋がりを通して、ますます領域理論と計算理論の関係の深さを思い知らされました。
領域理論も計算理論もともに「計算」の数学的モデル化という目的は共通しています。
その際に、計算理論はある種「定量的に」計算概念をモデル化しているのに対し、領域理論は半順序を通して計算の進行を「x\le{y}」により「定性的に」モデル化しているとみなせます。
(定量的領域理論(quantative domain theory)も存在するのですが、不勉強のためどういう分野なのかは存じ上げておりません。)
停止しない計算の扱い
また、計算のモデル化の際には停止しない計算をどのように扱うのかを考える必要があり、その対比こそがタイトルの通り本記事のメインテーマでした。
通常の集合論的な関数を計算のモデルとして採用してしまうと、型無しλ計算において集合論的なモデルが存在しないようにRussellのパラドックスのような現象が発生してしまいます。
そこで、計算可能性理論においては、計算が停止しない入力を未定義とする部分関数により計算をモデル化しているのに対し、領域理論では未定義を表す元\botを導入することにより数学的には全域関数のみを用いて計算をモデル化していたのでした。
改めて標語的に言い換えると、「部分関数と全域引数の計算理論」と「全域関数と部分引数の領域理論」という対比が見えてきます。
computability vs continuity
また、computability vs continuityのような対比も随所で見られ、領域理論に計算可能性を導入しようとする試みはよく見られます。
しかし、結局は自然数を経由した"間接的な"定義しか見られず、個人的にはあまり満足がいっておりません。
原始帰納関数や部分帰納関数は適当な初期関数を用いて有限文字列上でも"直接的に"(=自然数を経由せず)定義されることは知られていますが、そのような計算可能性の直接的定義を\omega-代数的cpo、またはそのCCCな極大fullsubの1つであるbifinite domain(SFP-対象)で扱えないかなとずっと考えておりました。
今、\omega-代数的cpoを持ち出したのにも領域理論と計算可能性理論の対比による理由があります。
自然数と実数を統一的に扱う
代数的cpoにおいては、有限な元全体からイデアル完備化により全体を復元できるという定理がありますが、その際連続関数は有限な元での出力が定まっていれば他の元の出力も一意に定まるという定理があります。
特に、無限文字列上の連続関数の値が有限文字列、つまりその近似のみで決まるという事実はまさに実数上の計算可能性のアイデアそのものです。
その際、有限な元全体が\omega以下のとき\omega-代数的cpoといい、まさに有限及び無限文字列全体の空間の一般化となっています。
そのため、\omega-代数的cpoの有限な元上の"直接的な"定義もどうにか自然に与えることはできないかと思っていたわけです。
また、計算可能性理論においては自然数上の計算理論と実数上の計算理論がそれぞれ存在する形となっているのに対して、領域理論は自然数上の計算と実数上の計算を1つの領域上でイデアル完備化により統一的に扱えていると考えることもできると思っています。
不動点の扱い
まだ領域理論と計算可能性理論の対比の話はあります。
計算可能性理論における基本的な定理にKleeneの再帰定理が存在します。
停止性問題で見られるように部分再帰関数は直接的な不動点を常に持つとは限りませんが、再帰定理により意味上では常に不動点を持つことが言えます。
常に不動点を持つというのは、ある種任意の方程式が解を持つような事を言っておりありえないのですが、不動点の意味をある種弱めることで直感的ありえなさを回避しつつスムーズな理論を構築しております。
領域理論にも同様の定理が存在し、連続関数は常に不動点を持つことが言えます。
これも、不動点を直感的に持たない関数については未定義を表す\botを不動点とすることで、計算可能性理論と同様に不動点の意味をある種弱めることで直感的ありえなさをうまいこと回避しつつスムーズな理論を構築しております。
ただの感想
これらの話は本当にただの感想を話しているだけで、どれもだから何という話かもしれません。
そもそも私のリサーチ不足なだけで色々と既に研究されている可能性もありますし、どうでもいい視点過ぎて考えられてないだけかもしれません。
ただ、考えてることを書き留めたかったのみです。
最後に、Viggo, Ingrid, Edward[2]のp.222の演習問題14を載せて終わることにします。
演習問題:
\mu\in[[\mathbb{N}_\bot\rightarrow\mathbb{N}_\bot]\rightarrow\mathbb{N}_\bot]を次で定義する
\mu(g)=\left\{
\begin{array}{ll}
n & if\ g(n)>0\ \&\ \forall m<n,\ g(m)=0 \\
\bot & if\ no\ such\ n\in\mathbb{N}\ exists
\end{array}
\right.
また、F:[\mathbb{N}_\bot\rightarrow\mathbb{N}_\bot]\rightarrow\mathbb{N}_\botと次で定義する
F(g)=\left\{
\begin{array}{ll}
\bot & if\ g(\bot)=0 \\
\mu(g) & otherwise
\end{array}
\right.
-
Fは連続だが全域的でないことを示せ
-
Fは[[\mathbb{N}_\bot\rightarrow\mathbb{N}_\bot]\rightarrow\mathbb{N}_\bot]の極大元であることを示せ
参考文献
[1]: Berger, U., Total sets and objects in domain theory, Annals of Pure and Applied Logic 60 (1993), pp. 91–117.
[2]: Stoltenberg-Hansen, V., Lindström, I., Griffor, E.: Mathematical theory of domains. Cambridge: Cambridge University Press 1994
[3]: Normann, Dag: Recursion on the countable functionals. Lecture notes in mathematics (Springer-Verlag) ; 811. 1980
Discussion