Think Proof, Count Two

and look for a red shoe

Scott 位相についての連続性の練習問題

Posted on — Feb 19, 2023

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

用語

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

dcpo

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

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

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

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

Scott 位相

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

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

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

補題

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

Proof.

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

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

以上より UdU_d は Scott open である。

問題

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

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

Proof.

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

まず ff の単調性を示す。 a,bDa, b \in Daba \leq b なる元を任意に取る。 f(a)≰f(b)f(a) \not\leq f(b) を仮定して矛盾を導く。 いま f(a)≰f(b)    f(a)VbDf(b)    aUbf1(Vb) 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) である。 仮定より ff は連続であるから UbU_b は Scott open で、特に Ub=Ub\uparrow U_b = U_b となる。 ここで aba \leq b より bUbb \in U_b であるが、f(b)Vbf(b) \in V_b となり矛盾。 したがって ff は単調である。

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


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

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

  3. これは簡単。 ↩︎