Think Proof, Count Two

最近、『プログラム意味論』（著・横内寛文）をのんびり読み進めている。 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)$ となる。 これは上限の定義に矛盾する。 証明終わり

Footnotes

1. 定義の細かい箇所が本とは異なるので注意。 ↩

2. 一般に $\uparrow U \supset U$ であることに注意。 ↩

3. これは簡単。 ↩