最近、『プログラム意味論』(著・横内寛文)をのんびり読み進めている。
3章2節の練習問題で少し悩んだので備忘録変わりに残しておく。
用語
用語は基本的に上述の『プログラム意味論』のものに従う。
ただ、参照するのが面倒なので基本的な定義をここに書き写しておく。
dcpo
(D,≤) を半順序集合とする。
X⊂D が有向であるとは、任意の a,b∈X に対して適当な元 x∈X が存在して a≤x かつ b≤x を満たすときをいう。
D の任意の有向部分集合 X⊂D について、上限 supX∈D が存在するとき、D を dcpo (directed-complete poset) という。
半順序集合 D の部分集合 A に対し、
↑A:={d∈D∣∃a∈A s.t. a≤d}
および
↓A:={d∈D∣∃a∈A s.t. d≤a}
と書く。
特に一点集合 A={a} に対して ↑a=↑{a} のように略記する。
Scott 位相
D を dcpo とする。
D に次のように位相を定める。すなわち U⊂D が開集合であるのは次の条件を満たすときとする:
- ↑U=U,
- 任意の有向部分集合 X⊂D について、supX∈U ならば X∩U=∅
実際、このように定義すると {U} は位相空間の公理を満たす。
このような位相を Scott 位相という。
補題
D を dcpo とする。
任意の d∈D について、Ud:=D∖↓d は Scott open である。
Proof.
まず ↑Ud=Ud を示す。
任意に u∈↑Ud を取る。
このとき、適当な t∈Ud が存在して t≤u である。
t∈/↓x より u∈/↓x でなければならず、したがって u∈Ud である。
X⊂D を有向部分集合であって supX∈Ud であるものとする。
このとき X⊂↓d である(
実際 X⊂↓d とすると supX≤d となり、supX∈Ud と矛盾してしまう)。
したがって適当な x∈X が取れて x∈/↓d となり、
すなわち x∈X∩Ud=∅ がわかる。
以上より Ud は Scott open である。
問題
dcpo の間の写像 f:D→D’ について、以下は同値:
- f は(Scott 位相について)連続写像
- 任意の有向部分集合 X について f(supX)=supf(X) が成り立つ
Proof.
2.⟹1. は簡単なので、1.⟹2. のみ示す。
まず f の単調性を示す。
a,b∈D で a≤b なる元を任意に取る。
f(a)≤f(b) を仮定して矛盾を導く。
いま
f(a)≤f(b)⟺f(a)∈Vb:=D’∖↓f(b)⟺a∈Ub:=f−1(Vb)
である。
仮定より f は連続であるから Ub は Scott open で、特に ↑Ub=Ub となる。
ここで a≤b より b∈Ub であるが、f(b)∈Vb となり矛盾。
したがって f は単調である。
さて X⊂D を有向部分集合としよう。
f は単調であるので supf(X)≤f(supX) は明らか。
逆向きの不等号を示す。
f(supX)≤supf(X) を仮定すると
f(supX)∈V:=D’∖↓supf(X)
となり、したがって supX∈U:=f−1(V) となる。
仮定より f は連続であるから U は Scott open である。
いま X∩U=∅ であるから元 x∈X∩U を任意に一つとる。
このとき
f(x)∈f(X)∩f(U)⊂V
であり、したがって f(x)∈/↓supf(X) となる。
これは上限の定義に矛盾する。
証明終わり