👻

【コンピュータサイエンス】領域理論を紹介する【part1】

2023/07/25に公開

math

part2はこちらになります。(未完成)

はじめに

はじめまして。記事を開いていただきありがとうございます。
これから領域理論という数学分野について紹介したいと思います。

領域理論とは順序理論や位相空間論、圏論等の数学理論を用いて、コンピュータにおける「計算」概念を数学的にモデル化することを目的とした抽象数学理論です。

純粋な数学理論でありながらコンピュータサイエンス的な直感も通用するという点が他の分野にない魅力だと感じています。
プログラム意味論における応用が有名ですが、実はそれ以外にも様々なトピックがあり非常に興味深い分野です。

この記事について

想定読者：
- 順序理論や位相空間論などの数学に興味がある人
- プログラミング言語やデータ構造に背後にある数学構造に興味がある人
- 最低限の数学的素養は前提としています
記事の目的：領域理論を知らない人に興味を持ってもらうこと
解説内容：領域理論とは、領域理論の古典的なトピック等

領域理論とは

数学的側面と計算の抽象化としての側面について、それぞれの視点から領域理論を紹介します。

数学的特徴1: 不動点

領域理論とは有向完備半順序集合(dcpo)という(数学的)空間と、その間の連続写像により展開される数学理論です。
dcpoとは任意の有向集合^[1]が上限を持つような最小元を持つ半順序集合のことであり、連続写像とはその上限を保存する関数のことを指します。

なぜこの構造が重要とされるのでしょうか。
それは任意の関数が不動点を簡単な形で持つという定理が成り立つためです。

定理1: (不動点定理)

dcpo $D, E$ 及び連続関数 $f:D\rightarrow{E}$ に対し、 $D$ の最小元を $\bot$ とすれば次が成り立つ

f(\operatorname{fix}f) = \operatorname{fix}f

ただし、

\sqcup

を上限を表す記号^[2]として

\operatorname{fix}f = \sqcup_{n\in\mathbb{N}}{f^n(\bot)}

(つまり、

\operatorname{fix}

は最小不動点^[3]を与える関数)

この定理こそが領域理論を特徴づける最大の要素であり、最も重要な性質だと言えます。
この事実についてもう少し考察してみましょう。

実は、不動点を求めることはある種方程式の解を求めることに対応します。
例えば、関数 $f(x)=x^2+3x+1$ の不動点とは、 $a^2+3a+1=a$ を満たす $a$ のことであり、これは二次方程式 $a^2+2a+1=0$ を解くことに対応します。

この考察を踏まえて定理1を見直すと、これは以下のように(誇張気味に)言い換えることができます。

領域理論では任意の方程式の解が秒でわかる

この異常すぎる事実は実は再帰的定義を持つプログラミング言語と非常に相性が良いことがわかります。
例えば、階乗関数factの再帰的定義はOCamlでは以下のように行われます。

階乗関数 in Ocaml

let rec fact = fun x -> if x > 0 then x * fact (x - 1) else 1;;

これは見方を変えれば、関数factの関数方程式とみなせます。
すると、(色々と都合よく解釈すると)上記の事実より、この方程式はちゃんと解を持ち、関数factが容易に得られるわけです。

まとめると、領域理論は再帰的定義をサポートしているということが言えたことになります。

数学的特徴2: CCC

これはdcpoに限った構造ではありませんが、dcpo及び連続関数からなる圏がCCCをなすことも重要な特徴の一つです。

詳しく説明をします。
これは、dcpo同士の(適切に定められた)有限直積はdcpoになり、またdcpo $D, E$ 間の連続関数全体 $[D\rightarrow{E}]$ もまたdcpoになるということです。

特に後者の関数空間に閉じているという事実が重要で、これは領域理論が高階関数をサポートしているという事実を表します。

関数空間もまたdcpoになることで、関数自体も空間の点とみなすことができ、つまり関数もまたある関数の引数となり得ることになります。

領域がCCCをなすことはプログラミング言語の意味領域としての基本的な要請であり、それを調べることは主要なトピックの一つです。
このトピックについてはまた後に詳しく解説をします。

数学的特徴3: Scott位相

領域理論を話す上で絶対に外せない要素にScott位相の話があります。

ここまでの話はすべて順序理論としての側面しか見ていないのですが、領域理論では順序集合の話は必ずある種パラレルワールド的に位相空間の話として解釈することができます。

各dcpoからはScott開集合を導入することにより位相空間が得られます。
こうして得られる位相空間は $T_0$ になっており、幾何的な位相空間論とは風味が異なるためまた別の面白さがあると思われます。

同じものを異なる視点で見ることは新たな発見に繋がり、とても有用な見方です。
ここもまた所謂「点なし位相空間(pointless topology)」と繋がる非常に深遠なトピックであるため、後にまた文献案内及び解説をします。

位相空間論好きだけど幾何はなんか違うなと感じる人には特におすすめできます。

計算の抽象化としての側面

ここからはガラッと視点を変えて、領域理論の「アルゴリズムとデータ構造」的な側面を紹介したいと思います。

領域理論は一言で言うならば有限近似の理論と表現できます。

まず、dcpoとは直感的にはデータの集合を表しており、データの持つ情報量(=データの精度)によって半順序をなしていると説明されます。
その視点で見ると、 $x\leq{y}$ は $y$ の方がより精度の良いデータであることを表し、この関係はデータに対する計算の進行を表すと解釈できます。

すると、有向集合は合流性が保証された(つまり矛盾のない)計算の列と見なすことができ、有向集合が上限を持つという条件は矛盾のない計算は必ず収束するという条件と解釈できます。

そこで、この章では有向集合を計算過程(or 単に計算)と呼び、dcpoの元を単にデータと呼ぶことにします。

この直感のもとで、近似関係を導入します。
まず、より情報量が多いデータが計算できたら当然情報量がそれ以下のデータについてもわかることになるので、自然に以下の定義が得られます。

定義2: (計算)

dcpo $D$ 上のデータ $x$ 及び計算 $A$ に対し、次が成り立つとき $A$ はデータ $x$ を計算するという

x\leq\sqcup{A}

また、次が成り立つとき

A

はデータ

x

を有限的に計算するという

\exists{a}\in{A},\ x\leq{a}

(明らかに有限的に計算する

\Rightarrow

計算するは成り立つ)

そこで、近似関係は次のように得られます。

定義3: (近似関係)

dcpo $D$ 上のデータ $x, y$ に対し、次が成り立つとき $x$ は $y$ を有限近似すると言い、 $x\ll{y}$ と書く^[4]

yを計算する任意の計算過程でxは有限的に計算される

(一応、式で書くと $\forall{A}:有向, y\leq{\sqcup{A}} \Rightarrow \exists{a}\in{A},\ x\leq{a}$ となる)

このとき、 $x$ は $y$ に対して相対的に有限であるともいい、つまり有限近似というのは単に $y$ から見て $y$ より情報量の少なく有限的なデータのことを指すことになります。

ところで、 $x\ll{x}$ は成り立つのでしょうか？
日本語に直すと、「 $x$ は $x$ を有限近似する」と言えるのでまあ自身は自身を近似するでしょって感じがするのですが、実は「有限」近似であるという点が重要となってきます。

例えば無理数 $\pi$ を近似したいとして、「 $\pi$ は $\pi$ を近似しているのでこれが求めているものです！」なんて言われたら意味がわかりません。
我々が近似と言ったときに求めているのは有理数とかそういう有限的なデータによる近似なわけで、無理数で無理数を近似されても困ります。
しかし、 $3$ は $3$ を近似しているか？となれば、これは疑いようのない事実となります。

以上の観察から、「有限」という性質が以下のように定義されるのは明らかだと思います。

定義4: (有限)

dcpo $D$ 上のデータ $x$ に対し、 $x\ll{x}$ が成り立つとき $x$ を有限データ(or コンパクトなデータ)という

これは $\ll$ の元の定義に戻って「 $x$ を計算する任意の計算過程で $x$ は有限的に得られる」と言い換えれば $x$ が有限データであるということは更に納得できると思われます。

ここまでで有限近似という概念の形式化を行ってきました。
完全に抽象数学的な概念なのにどれほど直感が通じるのかはある程度感じ取れたかと思われます。

ここから、さらにdcpoについて2つのレベルの近似可能性を考え、連続dcpo及び代数的dcpoへと定義を拡張していきます。

定義5: (連続dcpo)

dcpo $D$ の各データ $x$ に対して、次が成り立つとき $D$ を連続dcpoという

x = \sqcup\{y\in{D}\ |\ y\ll{x}\}

これはつまり、「各データは相対的に有限なデータの近似として得られる」ということを意味します。
これはとても素晴らしい性質で、どのデータもある程度は有限的に表現できることを保証する性質です。

また、連続dcpoは全てのデータが有限データか極限データのどちらかであることを保証します。

定義6: (極限データ)

dcpo $D$ 上のデータ $x$ に対し、次が成り立つときデータ $x$ を極限データという

xに収束するある計算過程でxが有限的に得られない

命題7:

連続dcpoにおいては各データは有限データか極限データのいずれかである

これによりいかにも有限っぽいのに有限じゃない変なデータが存在しないことが保証されます。
(本当は例を示したいのですが図が書けないのでお許しください。Hansen [4]のp.55とかにあります)

他にも、連続性は各データに対する計算は本質的に一つしかない^[5]ことを保証するという特徴もあります。
また、連続性は基底を持つことと同値であるという性質もあるのですが、基底周りは後に触れたいと思います。

ところで、連続dcpoは「相対的に」有限なデータによる近似可能性を保証するわけですが、我々が本当にやりたいのは真に有限なデータによる近似なわけです。
それを保証するより強い性質を定義します。

定義8: (代数的dcpo)

dcpo $D$ の各データ $x$ に対して、次が成り立つとき $D$ を代数的dcpoという

x = \sqcup\{y\in{D}\ |\ y\ll{y}\leq{x}\}

(明らかに代数性から連続性が従う)

$y\ll{y}$ というのは $y$ が有限データであることの定義だったので、これは全てのデータが真に有限近似可能であることを保証している定義となります。

これぞ我々がほしいデータ領域であり、領域理論は主にこの代数的dcpoを基本的なデータ領域とします。^[6]

代数的dcpoの例と反例

代数的dcpoの例と反例をいくつかあげます。

例9: べき集合

冪集合は包含関係により代数的dcpoをなし、有限データは有限濃度の集合に対応する
(有限集合の冪集合はすべての元が有限な代数的dcpoをなす)

例10: 部分代数 ("代数的"の由来)

ある代数の部分代数全体は包含関係により代数的dcpoをなし、有限データは有限生成な部分代数に対応する

例11: 部分関数空間

自然数間の部分関数全体 $[\mathbb{N}\rightharpoonup\mathbb{N}]$ は包含関係により代数的dcpoをなし、定義域が有限の部分関数が有限データに対応する

例12: カントール空間

あるアルファベット $\Sigma$ (=記号の集合)上の文字列全体(有限無限問わず)はprefix関係により代数的dcpoをなし、有限データは有限文字列に対応する
ただし、prefix関係は次のように定義される

\sigma\leq\tau\Leftrightarrow\tauの先頭に\sigmaが現れる

当然、無限文字列同士で

\sigma\leq\tau

となったらそれは

\sigma=\tau

を意味する

例13: $\mathbb{N}_\infty$

自然数に無限大元 $\infty$ を加えたものは代数的dcpoになり、有限データは自然数に対応する

反例14: $\mathbb{R}_\infty$ (連続だが代数的でない例)

実数に無限大元 $\infty$ を加えたものは全てのデータが極限データとなる連続dcpoになるが、代数的dcpoをなさない

反例15: $\mathbb{Q}_\infty$ (dcpoにならない例)

有理数には無限大元 $\infty$ を加えてもdcpoをなさない。例えば、次の集合は有向だが上限を持たない

\{x\ |\ x<\sqrt{2}\}

おまけ1: 無限列上の計算可能性

カントール空間に関連して無限列上の(=実数上の)関数の計算可能性の定義について軽く触れます。
この章は少しテクニカルな話が多くなるので、あまり知らなかったら読まなくても支障はありません

まずイデアル完備化を導入します。イデアルの定義やイデアル完備化のモチベについてはpart2で詳しく説明します。

定義16: (下方集合, イデアル)

poset (半順序集合; partially ordered set) $P$ の部分集合 $X$ ( $\not=\emptyset$ )が下方集合(or 下に閉, 順序イデアル)であるとは、 $X\ =\ \downarrow{X}$ が成り立つことを言う

ただし、 $\downarrow{X}$ は次のように定義される

\downarrow{X}\ =\ \{y\in{P}\ |\ \exists{x}\in{X},\ y\leq{x}\}

用語を濫用して

\downarrow{X}

を「

X

が生成する下方集合」と呼ぶこととする

また、 $P$ 上の有向下方集合をイデアル^[7]^[8]といい、特に一点集合から生成されるイデアル^[9]を主イデアル(or 単項イデアル)という

定義17: (イデアル完備化)

poset $P$ に対し、 $P$ のイデアル完備化^[10] $\overline{P}$ とは $P$ 上のイデアル全体を包含関係で順序付けたposetである

するとposetのイデアル完備化は代数的dcpoをなすことが言えます。

定理18: (posetのイデアル完備化)

posetのイデアル完備化は主イデアルを有限データに持つ代数的dcpoである

Proof: (Sketch)

有向完備性は、イデアル族の有向性がその和集合の(イデアルとしての)有向性を直接導くことより分かる。(下方性は明らか)
また、主イデアルが有限なことは和集合の定義から容易に分かり、逆は有限データ $I\in\overline{P}$ に対し、 $\{\downarrow{p}\ |\ p\in{I}\}$ という計算を与えてやれば有限性から $I$ が主イデアルであることは示せる。
最後に、各イデアルがその各元が生成する主イデアルらの和集合で表せることは明らかより代数性も言える。
$\square$

Remark:
posetが最小元を持つとき、かつそのときに限り生成されるdcpoも最小元を持つ

この事実を用いて以下の事実が容易に示せます。

定理19: (単調関数の連続拡張)

poset $P$ , dcpo $E$ 間の単調関数 $f: P\rightarrow{E}$ は $P$ のイデアル完備化 $\overline{P}$ に対して連続な拡張 $\overline{f}: \overline{P}\rightarrow{E}$ を一意に持つ

Proof: (Sketch)

$\overline{P}$ の代数性を利用して $\overline{f}(I)$ の $I$ を有限近似に置き換えれば、あとは有限データが主イデアルであること及び関数の連続性からすぐに $\overline{f}$ の自然な定義が一意に導かれる。すなわち、

\begin{equation*} \overline{f}(I) = \left\{ \begin{array}{ll} f(p) & if\ I = \downarrow{p} \\ \sqcup_{p\in{I}}f(p) & otherwise \end{array} \right. \end{equation*}

は確かに連続で、この形でしか $f$ の拡張は存在しない。
( $f$ : 単調より $\{f(p)\}_{p\in{I}}$ は確かに有向)
$\square$

Remark:
ここでは $\overline{P}$ 内の( $P$ 上の)主イデアルらを $P$ と同一視している

つまり何が言えるかというと、代数的dcpoにおいては有限データに対しての出力さえ定まっていれば極限データに対しての出力も自動で定まるということです。

領域理論におけるこの有限と極限(無限)の対比は、離散と連続、ひいては始代数と終余代数の対比に言い換えることができ、それらを結ぶのがイデアル完備化というわけです。(Adamek [1], Balan [2])

今カントール空間について、無限列は有限列のイデアル完備化として得られるため、無限列上の関数の計算可能性は対応する有限列上の単調関数の計算可能性により記述することができ、近似の視点から見ると無限列上の計算可能性の定義はめちゃくちゃ自然な定義だったんだとわかります。

また、こういう視点で見ると実数とは終余代数なので、実数上の計算可能性は終余代数上の計算可能性へと一般化されるのではないかと想像が膨らみます。(Pattinson [3])

おまけ2: "domain"の定義はカオス

こっちはガチのおまけです。

領域理論の文献ではその名の通り"domain(領域)"という用語が必ず多用されています。
では、結局"domain"の定義ってなんなのでしょうか。

実はこれは「人による」が答えなのですが、面白いのがあまりにも"domain"の定義のバラエティが豊富すぎて人によるなんてレベルじゃない状況になっている点です。

例を挙げると、
cpo, 連続cpo, 代数的cpo, $\omega$ -代数的cpo、Scott領域
などが単に"domain"として呼ばれているのを見たことがあります。
(なんかどっかで完備束やら連続束がdomainと呼ばれてたような気もしなくもない)

そして更に状況をややこしくしているのが、今意図的に濁して書いた"cpo"の部分すら文献によってまちまちですという点です。

"cpo"の定義には「有向完備 vs $\omega$ 完備」と「最小限を持つ vs 持たない」で合計4通りあり、どれも単にcpoと呼ばれる可能性があります。
前半をdcpoや $\omega$ -cpo、後半をpointedの有無で区別されている場合もあり、この記事では混乱のないようdcpoと丁寧に呼んできました。

個人的に結構終わってるなと思ったのが、[5]ではdcpoはdcpoで呼び、pointed dcpoのことをcpoと呼ぶという区別をしており、何度cpoのことを(pointless) $\omega$ -cpoと勘違いしたかわかりません。

さらに、あまりにややこしすぎてか「"domain"という言葉は専門用語ではない」とまで言っている文献すら見たことあり本当にもうはちゃめちゃです。

しかし、これは実は的を射ており、実際"domain"という言葉は結局は「自分が理想と考えるプログラミング言語の意味領域」という程度の意味でみんな使っているように感じるので、当然人によってその辺の感覚はまちまちなわけですね。
(それでももう少し統一してほしいとは思いますが)

まあなので、領域理論の文献を読むときは必ずdomainの定義を確認してから読むように心がけましょう(n敗)

他にもこのレベルで定義がまちまちな数学用語があったらぜひ紹介してくださると嬉しいです。
以上、ガチのおまけパートでした。

この記事はpart2に続きます。

参考文献

文献については主にpart2で紹介しようと思っているので、ここでは最低限の文献をあげておきます。

[1]: J. Adámek. Final coalgebras are ideal completions of initial algebras. J. Logic Comput., 12 (2) (2002), pp. 217-242.
[2]: A. Balan and A. Kurz, “On Coalgebras over Algebras,” Electronic Notes in Theoretical Computer Science, vol. 264, no. 2, pp. 47–62, Aug. 2010.
[3]: Pattinson, D. (2003) Computable functions on final coalgebras. In: Proc. of 6th Workshop on Coalgebraic Methods in Computer Science, CMCS'03. Electronic Notes in Theoretical Computer Science 82 (1).
[4]: Stoltenberg-Hansen, V., Lindström, I., Griffor, E.: Mathematical theory of domains. Cambridge: Cambridge University Press 1994
[5]: R. Amadio and P.-L. Curien, Domains and Lambda-calculi, Cambridge University Press, 1998.
[6]: G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. Continuous Lattices and Domains. Cambridge University Press, 2002.
[7]: Carl A. Gunter, Semantics of Programming Languages: Structures and Techniques, 1992
[8]: S. Abramsky and A. Jung, "Domain Theory" in Handbook of Logic in Computer Science, Oxford University Press, vol. III, pp. 1-168, 1994.
[9]: C. A. Gunter, D. S. Scott. Semantic Domains. Handbook of Theoretical Computer Science, Volume B, 633-674, 1990, pp. 633-674.

脚注

空集合は有向ではありません。もしそうしないと、有向完備性が最小元の存在を常に含意してしまうためです。 ↩︎
$\sqcup$ で有向集合に対する上限を、 $\vee$ で有向と限らない集合に対する上限を表すとします。領域理論には様々な形で上限が登場するため、この区別は本質的です ↩︎
なぜ「最小」不動点を取るのが好ましいのかはGunter [9]に"Uniformity"という言葉で説明されていました ↩︎
wey-below relationとも言う ↩︎
$\sqcup{A}=\sqcup{B}=x$ ならば $A\cup{B}$ は有向で $\sqcup(A\cup{B})=x$ ↩︎
実際はもう少し条件の付いたScott領域というdcpoが基本となるデータ構造です ↩︎
ブール束におけるイデアルは、対応するブール環におけるイデアルと完全に一致します ↩︎
イデアルはフィルターの双対概念です。イデアルがupward-directed, downward-closedなのに対し、フィルターはdownward-directed, upward-closedとなっています ↩︎
一元生成下方集合は必ずイデアルになります ↩︎
実はイデアル完備化は繰り返しても元に戻ると限らず、closureの定義の一つ $\overline{\overline{P}}=\overline{P}$ に反します ↩︎

はじめに

この記事について

領域理論とは

数学的特徴1: 不動点

定理1: (不動点定理)

数学的特徴2: CCC

数学的特徴3: Scott位相

計算の抽象化としての側面

定義2: (計算)

定義3: (近似関係)

定義4: (有限)

定義5: (連続dcpo)

定義6: (極限データ)

命題7:

定義8: (代数的dcpo)

代数的dcpoの例と反例

例9: べき集合

例10: 部分代数 ("代数的"の由来)

例11: 部分関数空間

例12: カントール空間

例13: \mathbb{N}_\infty

反例14: \mathbb{R}_\infty (連続だが代数的でない例)

反例15: \mathbb{Q}_\infty (dcpoにならない例)

おまけ1: 無限列上の計算可能性

定義16: (下方集合, イデアル)

定義17: (イデアル完備化)

定理18: (posetのイデアル完備化)

Proof: (Sketch)

定理19: (単調関数の連続拡張)

Proof: (Sketch)

おまけ2: "domain"の定義はカオス

参考文献

Discussion

例13: $\mathbb{N}_\infty$

反例14: $\mathbb{R}_\infty$ (連続だが代数的でない例)

反例15: $\mathbb{Q}_\infty$ (dcpoにならない例)