日々の流転

λ. cpoとか

らくがきえんじん(2004-11-13) でcpoの話を見かけて、cpoという単語は複数の意味で使われていて紛らわしかったのを思い出した。私の知ってるのだとこんな感じだったかな。

有向集合 (directed set)

≦を集合X上の擬順序(preorder)とする。部分集合S⊆Xは、任意の有限部分集合T⊆SがS内に上限を持つ(∨T ∈ S)とき有向集合。(空集合の上限が存在するのでSは空集合ではない)

dcpo (directed complete poset)

任意の有向な部分集合が上限を持つ半順序集合。この上限は ∨^↑ S 等と書かれる事もある。

cpo (complete poset), ipo (inductive partial order)

最小元⊥を持つdcpo。下のcpoと区別するためにipoと呼ばれることも。

cpo (complete poset), pointed cpo

最小元⊥を持ち、任意の無限上昇列(ω-chain)が上限を持つ半順序集合。ω-chainの上限は ∨_i=0^∞x_i 等と書かれる事もある。下の最小元⊥を持たないやつをcpoと呼ぶ場合にはこっちは pointed cpo と呼ぶ。

cpo (complete poset)

任意の無限上昇列(ω-chain)が上限を持つ半順序集合。最小元⊥は持たなくてもよい。

ω-algebraic dcpo

任意の有向な部分集合がω-chainを含んでいて、有向集合の上限とω-chainの上限が一致する algebraic dcpo。