トップ «前の日記(2007-04-24) 最新 次の日記(2007-04-27)» 月表示 編集

日々の流転


2007-04-25 [長年日記]

λ. 初給料日

というわけで、初給料。 さて、何に使うか。

λ. 2/3 SFP と algebraicity

Topology via Logic では 2/3 SFP を以下のように定義している。

For each finite set S of compact points there is another such M (a complete set of upper bounds for S) such that
  • each m∈M is an upper bound for S, and
  • if m´ is any compact upper bound for S, then m´ ⊒ m for some m∈M.

この定義はm´はcompactであることを要求しているが、対象となる半順序集合が algebraic dcpo であれば、この条件は外せる。

証明

m´ を S の upper bound とする。 対象となる半順序集合 P が algebraic dcpo なので、T = {c∈KP | c⊑m´} とおいて、 ∀x∈S. x ⊑ m´ = ⨆T 。 xのコンパクト性より、 ∀x∈S. ∃cx∈T. x ⊑ cx

C = {cx | x∈S} とおくと、CはTの有限部分集合なので、Cのupper bound c∈T が存在する。

  1. c∈Tなので m´ ⊒ c 。
  2. 一方、c は Sの compact upper bound なので、2/3 SFP を適用して、ある m∈M について c ⊒ m 。

よって、m´ ⊒ c ⊒ m 。