最近、『プログラム意味論』（著・横内寛文）をのんびり読み進めている。 3章2節の練習問題で少し悩んだので備忘録変わりに残しておく。

用語

用語は基本的に上述の『プログラム意味論』のものに従う。 ただ、参照するのが面倒なので基本的な定義をここに書き写しておく¹。

dcpo

\((D, \leq)\) を半順序集合とする。

\(X \subset D\) が有向であるとは、任意の \(a, b \in X\) に対して適当な元 \(x \in X\) が存在して \(a \leq x\) かつ \(b \leq x\) を満たすときをいう。

\(D\) の任意の有向部分集合 \(X \subset D\) について、上限 \(\sup X \in D\) が存在するとき、\(D\) を dcpo (directed-complete poset) という。

半順序集合 \(D\) の部分集合 \(A\) に対し、 \[ \uparrow A \coloneqq \{ d \in D | \exists a \in A \text{ s.t. } a \leq d \} \] および \[ \downarrow A \coloneqq \{ d \in D | \exists a \in A \text{ s.t. } d \leq a \} \] と書く。 特に一点集合 \(A = \{a\} \) に対して \(\uparrow a = \uparrow \{a\}\) のように略記する。

Scott 位相

\(D\) を dcpo とする。 \(D\) に次のように位相を定める。すなわち \(U \subset D\) が開集合であるのは次の条件を満たすときとする:

1. \(\uparrow U = U\)²,
2. 任意の有向部分集合 \(X \subset D\) について、\(\sup X \in U\) ならば \(X \cap U \neq \emptyset\)

実際、このように定義すると \(\{U\}\) は位相空間の公理を満たす³。 このような位相を Scott 位相という。

補題

\(D\) を dcpo とする。 任意の \(d \in D\) について、\(U_{d} \coloneqq D \setminus \downarrow d\) は Scott open である。

Proof.

まず \(\uparrow U_d = U_d\) を示す。 任意に \(u \in \uparrow U_d\) を取る。 このとき、適当な \(t \in U_d\) が存在して \(t \leq u\) である。 \(t \notin \downarrow x\) より \(u \notin \downarrow x\) でなければならず、したがって \(u \in U_d\) である。

\(X \subset D\) を有向部分集合であって \(\sup X \in U_d\) であるものとする。 このとき \(X \not\subset \downarrow d\) である（ 実際 \(X \subset \downarrow d\) とすると \(\sup X \leq d\) となり、\(\sup X \in U_d\) と矛盾してしまう）。 したがって適当な \(x \in X\) が取れて \(x \notin \downarrow d\) となり、 すなわち \(x \in X \cap U_d \neq \emptyset\) がわかる。

以上より \(U_d\) は Scott open である。

問題

dcpo の間の写像 \(f \colon D \to D’\) について、以下は同値:

1. \(f\) は（Scott 位相について）連続写像
2. 任意の有向部分集合 \(X\) について \(f(\sup X) = \sup f(X)\) が成り立つ

Proof.

\(2. \implies 1.\) は簡単なので、\(1. \implies 2.\) のみ示す。

まず \(f\) の単調性を示す。 \(a, b \in D\) で \(a \leq b\) なる元を任意に取る。 \(f(a) \not\leq f(b)\) を仮定して矛盾を導く。 いま \[ f(a) \not\leq f(b) \iff f(a) \in V_b \coloneqq D’ \setminus \downarrow f(b) \iff a \in U_b \coloneqq f^{-1}(V_b) \] である。 仮定より \(f\) は連続であるから \(U_b\) は Scott open で、特に \(\uparrow U_b = U_b\) となる。 ここで \(a \leq b\) より \(b \in U_b\) であるが、\(f(b) \in V_b\) となり矛盾。 したがって \(f\) は単調である。

さて \(X \subset D\) を有向部分集合としよう。 \(f\) は単調であるので \(\sup f(X) \leq f(\sup X)\) は明らか。 逆向きの不等号を示す。 \(f(\sup X) \not\leq \sup f(X)\) を仮定すると \[ f(\sup X) \in V \coloneqq D’ \setminus \downarrow \sup f(X) \] となり、したがって \(\sup X \in U \coloneqq f^{-1}(V)\) となる。 仮定より \(f\) は連続であるから \(U\) は Scott open である。 いま \(X \cap U \neq \emptyset\) であるから元 \(x \in X \cap U\) を任意に一つとる。 このとき \[ f(x) \in f(X) \cap f(U) \subset V \] であり、したがって \(f(x) \notin \downarrow \sup f(X)\) となる。 これは上限の定義に矛盾する。 証明終わり