日々の流転

λ. 初給料日

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

λ. 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. ∃c_x∈T. x ⊑ c_x 。

C = {c_x | 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 。