某勉強会がコーヒーブレイクタイムに入って,ブレイクタイムから抜けたら何もかも忘れてそうだったので,数式レンダリングのテストも兼ねて CPO 関連の定義だけまとめておくことにした.
なお各定義は, SoPL (Semantics of Programming Languages) に則ってる.
Complete Partial Order
まあ,まずはおなじみのやつから.
- 定義. 半順序 (partially ordered set, poset, partial order)
集合 D と二項関係 (⊑)⊆D×D の組 ⟨D,⊑⟩ で,以下の制約を満たすもの:
- 反射律 (reflexive)
- ∀x∈D.x⊑x
- 反対称律 (anti-symmetric)
- ∀x,y∈D.(x⊑y∧y⊑x)⟹x=y
- 推移律 (transitive)
- ∀x,y,z∈D.(x⊑y∧y⊑z)⟹x⊑z
なお,二項関係が文脈から分かる場合単に集合を poset と呼んだり,逆に集合が分かる場合二項関係を半順序と呼んだりする.二項関係がどの poset のものか示すため, ⊑D と書いたりもする.total な関係になっていれば,全順序.
- 定義. (上に) 有界 (bounded (above), consistent)
poset D に対して,その部分集合 P⊆D が (上に) 有界とは,以下を満たすこと:
∃x∈D.∀y∈P.y⊆x
この時, x を P の上界 (an upper bound) と呼ぶ.
なお,普通 bounded は上下に有界な時使う気がするけど,この後は特に断りない限り, bounded above のことを有界と言っていく.後逆は, bounded below と lower bound .それと, {x1,…,xn} が有界な時, x1↑⋯↑xn と書く.組になってる時は, consistency pair と呼んだりもするっぽい.
- 定義. 上限 (least upper bound, lub, supremum, sup)
poset D ,その有界集合 P⊆D に対して,その上界 ⨆P∈P が上限とは,以下を満たすこと:
任意の上界 x について⨆P⊑x
supP=⨆P という記法や, pointwise に ⨆x∈Px=⨆P ,supx∈Px=supP という記法を使うこともある.また, x1⊔⋯⊔xn=⨆{x1,…,xn} と書くこともある.
上限の中で一番小さいやつ.全ての有界集合が sup 持つとは限らない (上界同士で上下関係がないことがあるので) ことに注意.存在すれば一意に決まる.逆は, greatest lower bound (glb) または infimum (inf) .
- 定義. 有向部分集合 (directed subset)
poset D に対して,その部分集合 M⊆D が有向とは,以下を満たすこと:
∀U∈Pfin(M).U は上界 x∈P を持つ
名前の意味的には,部分集合の上界を集めるとまたそれに上界があり,それにもやっぱり上界があってと言う感じで,最終的にある場所に対して上に上に順序が伸びていく感じ.なお,伸びていく場所が 2 点とか 3 点になってるような奴は, directed にならない.あと空集合にも上界の存在を求めてるので,空集合自体は directed じゃないことにも注意.また, directed subset は自身の内に上限を持つとは限らなくて, [0,1)⊆R を考えてみると,こいつは poset ⟨R,≤⟩ の directed subset になってて,上限は 1 だが,これは自身の内にはない.
- 定義. 完備半順序 (complete partial order, cpo)
poset D が,完備であるとは,以下を満たすこと:
任意の directed subset P⊆D は sup を持つ
directed subset は,有限の場合 sup を中に持つ.なので,有限 poset は cpo になる.cpo でない例としては,自然数の集合に通常の順序 ≤ をいれた poset ω={0,1,…} とか. ω は自身の directed subset になるが,その上限は存在しない.で, ω∞=ω∪{∞} に拡張して ∞ を最大要素となるよう順序も拡張すると,こいつは cpo になる.
- 定義. 点付き (pointed)
poset D が点付きであるとは,以下を満たすこと:
∃⊥∈D.∀x∈D.⊥⊑x
CPO の性質
こっちもおなじみのやつ.
- 定義. 単調 (monotone)
poset D から E への関数 f:D→E が単調とは,以下を満たすこと:
∀x,y∈D.x⊑y⟹f(x)⊑f(y)
順序を保存する関数.流石に順序ぐらいは保存してくれないとね.
- 定義. 連続 (continuous)
poset D から E への単調関数 f:D→E が連続とは,以下を満たすこと:
任意の directed subset P⊆D についてf(⨆P)=x∈P⨆f(x)
なお,有限だけ考える場合の連続性だけなら単調性だけから言えて,directed subset P={xi}1≤i≤n において, x=⨆P∈P となるものがあり, ∀i.xi⊑x より ∀i.f(xi)⊑f(x) なので, ⨆if(xi)=f(x)=f(⨆ixi) となる.なお, pointed cpo に対して連続関数から不動点を作れる (不動点定理).
- 定義. 正格 (strict)
pointed poset D から E への関数 f:D→E が正格とは,以下を満たすこと:
f(⊥)=⊥
pointed を保存する関数.
- 定義. ω-完備半順序 (ω-cpo)
poset D に対して,
- 単調関数 f:ω→D≃(xn∈D)n∈ω を ω-chain と呼ぶ.
- 任意の ω-chain (xn)n∈ω が sup を持つ時, D を ω-cpo と呼ぶ.
また, ω-cpo D から E への単調関数 f:D→E が ω-continuous とは,以下を満たすこと:
任意の ω-chain (xn)n∈ω についてf(n∈ω⨆xn)=n∈ω⨆f(xn)
ω-chain はつまり可算な増加列のこと.こいつは有限部分集合を取ると明らかに最大要素が一つ確定するため有界であり, directed subset になる.なので, cpo は ω-cpo になる.ただ,その逆は成り立たないらしい . ω-cpo でも不動点定理が成り立つ.
- 定理. cpo と連続関数による圏は,CCC
Cpo を cpo と連続関数から作られる圏とする.この時, Cpo は Cartesian Closed.
証明:
- terminal object
-
1 要素の cpo への関数は必ず連続になる.
- product
∀x1⊑x2∈D,y1⊑y2∈E.(x1,y1)⊑(x2,y2)∈D×E
product order が単純に直積になる.
- exponential object
DE={f∣連続関数 f:D→E}
pointwise order (f⊑g⟺∀x∈D.f(x)⊑g(x)) 入れた連続関数空間が冪になる.単純に apply(f,x)=f(x) / curry(f)(x)(y)=f(x,y) は連続関数になる.
ドメイン
こっからが本命みたいなとこがある.
- 定義. コンパクト (compact)
cpo D に対して, x∈D がコンパクトとは,以下を満たすこと:
任意の directed subset M⊆D についてx⊑⨆M⟹∃y∈M.x⊑y
なお, D の compact elements 全体を K(D) と書く.
cpo の場合のコンパクト性について. compact element は finite element とも呼ばれ,自身を近似するやつ.一般に,
x≪y⟺(∀M⊆D.M は directed∧y⊑⨆M⟹∃a∈M.x⊑a)
を近似関係と言って, x は y を近似すると読む.
- 定義. algebraic
cpo D が algebraic とは,以下を満たすこと:
∀x∈D,M={a∈K(D)∣a⊑x}.M は directed∧⨆M=x
algebraic cpo のことを domain と呼ぶことにする. domain 内の要素はそれ以下の compact elements の sup で表せる.これは色々便利な性質だけど,その圏は CCC にならない.具体的には,冪が作れない.
- 定義. 基底 (basis)
cpo D に対して, D0⊆K(D) が D の基底を成すとは,以下を満たすこと:
∀x∈D,M={a∈D0∣a⊆x}.M は directed∧⨆M=x
なお, D0 が D の基底を成す時, D は algebraic で K(D)=D0 となる. basis を持つ,つまり algebraic の範囲では cpo と ω-cpo は一致するらしい .
- 定義. 完備束 (complete lattice)
poset D が完備束とは,以下を満たすこと:
∀M⊆D.⨆M∈D
なお,この定義は完備半束と呼ばれるやつで,下限でもいい.通常の完備束は,上限下限どちらも要求する.ただ,完備半束は完備束と一致する.つまり,どちらかがあればどちらもある.
- 定理. 完備半束と完備束の一致
poset D において,以下は同値:
- 任意の部分集合 M⊆D は上限を持つ (完備束)
- 任意の部分集合 M⊆D は下限を持つ
- 任意の部分集合 M⊆D は上限下限を持つ
証明:
3 ⟹ 1 / 3 ⟹ 2 / 1 かつ 2 ⟹ 3 はいいので, 1 ⟹ 2 / 2 ⟹ 1 が示せればいい.どちらか片方が示せれば,もう片方は対称的に証明可能なので, 1 ⟹ 2 だけ示す.
まず,空集合を考えるとこいつにも上限があるはずで,そいつは最小元になる.
最小元は,全ての部分集合の下界になるため,少なくとも下界は一つは存在する.任意の部分集合 M の下界全体の集合を ↓M=∅ と書くとする.この時, M の要素は ↓M の上界になり,また ⨆(↓M) が存在するはずで,こいつは以下を満たす:
{∀x∈M.⨆(↓M)⊑x∀x∈↓M.↓M⊑⨆(↓M)
つまり, ⨆(↓M) は M の下界であり,かつ下界の最大要素であるため,下限となる.
以上より,定理が示せる.
一応束論ってタグつけたので,ちょっとは束論らしいことやらないとね? complete lattice は cpo になる.
- 定義. 有界完備 (bounded complete)
空でない cpo D が有界完備とは,以下を満たすこと:
任意の有界集合 M⊆D が ⨆M∈D を持つ
なお, cpo は directed complete な poset と呼ばれることがあり, directed + bounded complete な poset が, bounded complete cpo になる.bounded complete な domain を, bc-domain と呼ぶことにする. bc-domain による圏は CCC になる.
- 補題. 点付き有界完備 cpo の同値条件
pointed cpo D において,以下は同値:
- D は bounded complete
- 任意の x↑y について, x⊔y∈D
証明:
1 ⟹ 2 は,有界集合として M={x,y} を取れば自明に成り立つ.
2 ⟹ 1 は,以下のように示せる .
任意の有界部分集合 M⊆D について, M′∈Pfin(M) は有界で有限なので, ⊥ から各要素の sup 取りまくれば全体の sup が作れる.
ここで, N={⨆M′∣M′∈Pfin(M)} を考える.こいつは,任意の U∈Pfin(N) に対して, ⨆⋃{M′∣⨆M′∈U}∈U が上界となるので, U は directed set になる. D は cpo なので, ⨆U∈D が存在する.
⨆U は M の上界であり,他の任意の上界は U の上界にもなるので, ⨆M=⨆U となる.よって,題意は成り立つ.
2 の逆は sup があれば有界なことより自明なので, x↑y と x⊔y∈D は bc-domain では同値条件になる.
- 定義. 単項イデアル (principal ideal)
- poset P , x∈P について, x により生成される単項イデアルとは,集合 ↓x={y∈P∣y⊑x} のこと.
- 定義. property I
algebraic cpo D が property I を持つとは,以下を満たすこと:
∀a∈K(D).↓a は有限
property I + bounded complete な domain では,有限個で要素を近似できる.ただ, CCC は作れない.これはやっぱり冪が作れないから.単なる連続関数空間が property I を持たないため.
- 定義. 分配的 (distributive)
bc-domain D が分配的とは,以下を満たすこと:
∀x,y↑z∈D.x⊓(y⊔z)=(x⊓y)⊔(x⊓z)
distributive で property I を持つ bc-domain を dI-domain と呼ぶことにする.
- 定義. stable
dI-domain D から E への連続関数 f:D→E が, stable とは,以下を満たすこと:
∀x↑y.f(x⊓y)=f(x)⊓f(y)
dI-domain と stable function による圏は CCC になる.冪は,以下の stable order で作る:
f⊑sg⟺∀x⊑y.f(x)=f(y)⊓g(x)
まとめ
色々数式環境お試しのために書いた. KATEX では, \bigsqcap が書けないこととかが分かった.
これで,某勉強会のコーヒーブレイクタイムが終わっても,元の話題をちゃんと思い出せるといいな.