日記 (2019 年 11 月 9 日)
計算体系の表示的意味論を構築するときに用いられる概念に領域というものがあるが、 最近これに触れる機会が多くなってきたので、 改めて復習というか整理をしておこうと思う。
主なリファレンスは Abramsky–Jung†1 である。
順序集合に関する基本的な用語の定義や性質は既知とする。
単に順序集合と言った場合、 半順序集合 (反射的かつ推移的かつ反対称な順序が定まった集合) を指す。
また、 出てくる順序集合の順序は、 何も断らなければ常に ⊑ で表す。
まず、 領域理論において主に扱う順序集合を定義する。
定義 1.
順序集合 D の部分集合 A を考える。
A が空でなく、 任意の A の 2 元集合が A に上界をもつとき、 A は有向 (directed) であるという。
定義 2.
順序集合 D に対し、 任意の D の有向部分集合が D に上限をもつとき、 D は有向完備 (directed-complete) もしくは単に完備 (complete) であるという。
定義 3.
順序集合 D に対し、 D の最小元が存在するとき、 D は点付き (pointed) であるという。
領域理論では、 完備順序集合や点付き完備順序集合 (もしくはここでは定義しないが ω-完備集合) を主な対象として扱う。
「領域理論」 という名前で理論を展開するわけなので、 これらの概念のいずれかを 「領域」 と呼びたくなるが、 どれをそう呼ぶかは文脈によってまちまちのようである。
そこで、 余計な混乱を避けるため、 この日記シリーズでは 「領域」 という言葉は用いないことにする。
いくつか記号を整理しておく。
順序集合 D の部分集合 A に対し、 その上限は ⨆A で表す。
A が有限集合で A=:{a1,⋯,an} と書ける場合は、
a1⊔⋯⊔an:=⨆{a1,⋯,an}
と書く。
また、 何らかの集合 X からの写像 f:X→D があるとき、
x∈Xf(x):=⨆{f(x)∈D∣x∈X}
と書く。
このとき、 添字に条件を加える場合もある。
最後に、 最小元は常に ⊥ で表す。
次に、 これらの順序集合の間の写像を定義する。
定義 4.
順序集合 D,E と写像 f:D→E をとる。
任意の 2 元 d,d∈D に対し、 d⊑d ならば f(d)⊑f(d) が成り立つとする。
このとき、 f は単調 (monotonic) であるという。
定義 5.
完備順序集合 D,E と写像 f:D→E をとる。
任意の D の有向部分集合 A に対し、 ⨆f(A) が存在して f(⨆A)=⨆f(A) が成り立つとする。
このとき、 f は連続 (continuous) であるという。
定義 6.
点付き順序集合 D,E と写像 f:D→E をとる。
f が最小元を保つとき、 f は厳密 (strict) であるという。
完備順序集合 D,E に対し、 その間の連続写像全体の集合は [D,E] で表す。
D,E がともに点付きであるとき、 その間の厳密連続写像全体の集合は [D,E]! で表す。
単調写像と連続写像に関してすぐに分かる性質を 2 つ証明しておく。
命題 7.
完備順序集合 D,E の間の写像 f:D→E をとる。
f が連続であれば、 f は単調である。
証明.
任意に 2 元 d,d∈D をとり、 d⊑d とする。
d=d⊔d であるから、 f の単調性によって、 f(d)=f(d)⊔f(d) が成り立つ。
これは f(d)⊑f(d) を意味する。
命題 8.
完備順序集合 D,E をとる。
[D,E] の順序を
f⊑f:⟺∀d∈Df(d)⊑f(d)
で定めると、 [D,E] は完備である。
さらに、 E が点付きであれば、 [D,E] も点付きである。
証明.
[D,E] の有向部分集合 S をとる。
各 d∈D に対して集合 {s(d)∣s∈S} は有向であるから、
f: D ⟶ E d ⟼ s∈Ss(d)
が定義できる。
任意の D の有向集合 A に対し、
f(a∈Aa(=s∈Ss(a∈Aa(=s∈Sa∈As(a)=a∈As∈Ss(a)=a∈Af(a)
が成り立つが、 これは f(⨆A)=⨆f(A) を意味するので、 f は連続である。
したがって、 f∈[D,E] であり、 これは明らかに S の上限を与える。
以上により、 [D,E] は完備である。
E が点付きであれば、 E の最小元への定値写像が [D,E] の最小元を与える。
命題 9.
点付き完備順序集合 D,E をとる。
[D,E]! の順序を [D,E] と同様に定めると、 [D,E]! は完備かつ点付きである。
これらの命題により、 [D,E] や [D,E]! の有向部分集合 S について、 任意の d∈D に対して、
(s∈Ss((d)=s∈Ss(d)
が成り立つことが分かる。
すなわち、 [D,E] や [D,E]! における上限は各点で計算できる。
さて、 完備順序集合の間の射としては、 基本的に連続写像だけを考える。
これは、 完備順序集合を特徴づける有向部分集合の上限という概念を保つ写像であるから、 この選択は非常に自然である。
考えている順序集合が点付きの場合は、 その間の射としてさらに最小元を保つ (すなわち厳密である) ものだけを考えるのが自然に思えるが、 これは計算体系の意味論として使う場合にしばしば不都合を生じる。
そのため、 点付き完備順序集合の間の射としては、 (厳密でないかもしれない) 連続写像を考えることもあれば、 厳密な連続写像のみを考えることもある。
以上のことを踏まえて、 完備順序集合とその間の連続写像が成す圏を Dcpo とする。
また、 点付き完備順序集合とその間の (厳密でないかもしれない) 連続写像が成す圏と、 点付き完備順序集合とその間の厳密な連続写像が成す圏を、 それぞれ明確に区別して PDcpo と PDcpo! とする。
参考文献
- S. Abramsky, A. Jung (1994) 「Domain theory」 『Handbook of Logic in Computer Science』 3:1–168