完備半順序
数学の特に順序理論関連分野における有向完備半順序（ゆうこうかんびはんじゅんじょ、英: directed-complete partial order; dcpo）および ω-完備半順序（オメガかんびはんじゅんじょ、英: ω-complete partial order; ωcpo）あるいは単に cpoとは、半順序集合の特別なクラスで、完備性によって特徴づけられる。完備半順序は理論計算機科学、表示的意味論、領域理論において中心的な役割を果たす。
定義
[編集]半順序集合が有向完備半順序集合 (dcpo) であるとは、その任意の有向部分集合が上限を持つことを言う。半順序集合の部分集合が有向であるとは、それが空でなく、その任意の二元の上界がその部分集合内にとれることを言うのであった。言葉づかいとして、有向完備半順序集合のことを上完備半順序集合 (up-complete poset) と言ったり、単に cpo と言ったりする。
ω-完備 (あるいは単に cpo) は任意の ω-鎖 (x1 ≤ x2 ≤ x3 ≤ x4 ≤ …) が上限を持つような半順序集合を表すのに用いられる。任意の ω-鎖は有向ゆえ、任意の有向完備半順序は ω-有向完備半順序だが、逆は真でない。
最小元を持つ有向完備半順序集合は重要であり、しばしば点付き有向完備半順序や cppo あるいは単に cpo と呼ばれる。
有向上限の存在を要求することは、有向集合および上限を（近似的）計算における近似およびその極限をそれぞれ一般化するものと見做すことを考えれば自然である。この直観は、表示的意味論において、領域理論の発展を背景としてもたらされたものであった。
有向完備順序集合の双対概念はフィルター付き完備半順序 (filtered complete partial order) と呼ばれるが、双対順序を明示的に用いて扱う方がふつうであるから、実利上はこの概念を直接扱うことはそれほど多くない。
例
[編集]- 任意の有限半順序集合は有向完備である。
- 任意の完備束もやはり有向完備である。
- 任意の半順序集合に対して、その空でないフィルター全体の成す集合は、包含関係の定める順序に関して有向完備半順序集合である。空フィルターも含めれば点付きになる。順序が二項演算として交わりを持つならば、この点付き有向完備半順序集合は実際には完備束になる。
- 与えられた集合 S 上の部分写像全体の成す集合は、写像 f, g が f ≤ g であることを、g が f の延長である（つまり f の定義域は g の定義域の部分集合で、両方の写像が定義されるところでは f の値と g の値は一致する）ことと定めると順序集合になる（あるいは同じことだが、写像をグラフとして定義する立場ならば f ≤ g ⇔ f ⊆ g と定義することもできる）。この順序集合は点付き有向完備半順序集合になる。最小元は至る所定義されていない（つまり定義域が空の）部分写像である。実はこの場合の ≤ は有界完備にもなる。この例からは、最大元を持つことが常に自然とは言えない理由も示されている。
- 任意のsoberな空間の特殊化順序は有向完備半順序集合である。
- 因果関係 (consequence) で閉じているような文の集合として「演繹系」と言う言葉を用いることにする（ここで用いる意味の consequence の定義は例えば Tarski's algebraic approach[1][2]）。有向完備半順序集合となるような演繹系の集合に注目した重要な定理がいくつも存在する[3]。また、演繹系の集合には自然な仕方で最小元を選ぶことができる（だから完備半順序集合にもなる）。これは空集合の因果関係全体の成す集合（つまり、論理的に証明可能 / 論理的に意味を持つ文全体の成す集合）が演繹系であり、任意の演繹系に含まれることによる。
性質
[編集]順序集合 P が有向完備半順序集合となる必要十分条件は、その任意の鎖が P に上限を持つことである。同様に、順序集合 P が点付き有向完備半順序集合となる必要十分条件は、その任意の順序を保つ自己写像が最小の不動点を持つことである。任意の集合 S は、最小元 ⊥ (bottom) を付け加えて、平坦順序（S の各元 s に対して ⊥ ≤ s かつ s ≤ s およびそれ以外には関係を持たない）をいれることによって有向完備半順序集合にすることができる。
連続写像と不動点
[編集]二つの有向完備半順序集合 P, Q の間の写像が（スコット）連続であるとは、それが有向集合を有向集合へ写し、かつそれらの上限を保つことをいう。つまり、
- D ⊂ P が有向ならば f(D) は Q の有向集合で、
- 任意の有向集合 D ⊂ P に対して f(sup D) = sup f(D) が成り立つ。
有向完備半順序集合の間の任意の連続写像は単調となることに注意。この連続性の概念は、スコット位相によって誘導される位相的な連続性と同値である。
二つの有向完備半順序集合 P, Q の間の連続写像全体の成す集合 [P → Q] は、点ごとの順序を入れて再び有向完備半順序集合となり、またさらに Q が点付きならば点付き有向完備半順序集合になる。従って完備半順序集合とスコット連続写像の全体はデカルト閉圏を成す[4]。
点付き完備半順序集合 (P, ⊥) 上の任意の単調（順序を保つ）自己写像 f は最小不動点を持つ[5]。この f が連続ならば、この不動点は ⊥ の反復列 (⊥, f(⊥), f(f(⊥)), … fn(⊥), …) の上限に等しい（クリーネの不動点定理も参照）。
関連する概念
[編集]有向完備性は、ほかの完備性の概念（例えば鎖完備など）と様々な意味で関係がある。有向完備性自体は、ほかの例えば代数的順序集合やスコット位相を用いるような順序理論的研究においても生じてくるような極めて基本的な性質である。
注記
[編集]- ^ Tarski, Alfred: Bizonyítás és igazság / Válogatott tanulmányok. Gondolat, Budapest, 1990. (Title means: Proof and truth / Selected papers.)
- ^ Stanley N. Burris and H.P. Sankappanavar: A Course in Universal Algebra
- ^ See online in p. 24 exercises 5–6 of §5 in BurSan:UnivAlg. Or, on paper, see Tar:BizIg.
- ^ Barendregt, Henk, The lambda calculus, its syntax and semantics Archived 2004年8月23日, at the Wayback Machine., North-Holland (1984)
- ^ See Knaster–Tarski theorem; The foundations of program verification, 2nd edition, Jacques Loeckx and Kurt Sieber, John Wiley & Sons, ISBN 0-471-91282-4, Chapter 4; the Knaster-Tarski theorem, formulated over cpo's, is given to prove as exercise 4.3-5 on page 90.
参考文献
[編集]- Davey, B.A., and Priestley, H. A. (2002). Introduction to Lattices and Order (Second ed.). Cambridge University Press. ISBN 0-521-78451-4