完全偏序
模板参数错误!(代码36)
|
在数学中,有向完全偏序和完全偏序是特殊种类的偏序集合。分别简写为 dcpo 和 cpo,它们特征化自特定特定完备性性质。dcpos 和 cpos 在序理论中考虑并主要应用于理论计算机科学和指称语义。
定义
一个偏序集合是有向完全偏序(dcpo),如果它的每个有向子集都有上确界。完全偏序(cpo)是带有最小元素的 dcpo。在文献中,dcpos 有时分类为sup-完全偏序集合,或混淆为“cpo”。带有最小元素的 dcpo 有时叫做尖角(pointed) dcpo 或尖角 cpo。
Requiring the existence of directed suprema can be motivated by viewing directed sets as generalized approximation sequences and suprema as limits of the respective (approximative) computations. Details on this intuition in the context of denotational semantics are to be found in the introductory article on domain theory.
The dual notion of a directed complete poset is called a filtered complete partial order. However, this concept occurs far less frequently in practice, since one usually can work on the dual order explicitly.
性质和有关文章
Directed completeness relates in various ways to other completeness notions. This is documented in the article on completeness (order theory). Directed completeness alone is quite a basic property that occurs often in other order theoretic investigations. For instance, theorems involving directed completeness (and characterizations thereof) are to be found in the articles on continuous posets, algebraic posets, and the Scott topology. Functions between dcpos are often required to be monotone or even Scott continuous.
例子
- For any poset, the set of all non-empty filters, ordered by subset inclusion, is a dcpo, even a cpo if the poset has a greatest element. Together with the empty filter it is also guaranteed to be a cpo. If the order is a meet-semilattice (or even a lattice), then this construction (including the empty filter) actually yields a complete lattice.
- Consider the set of all partial functions on some set S, i.e. functions defined only on some subset (its domain) of S. For two such functions f and g, define f ≤ g iff the domain of f is a subset of the domain of g and the values of f and g agree on all inputs for which both functions are defined. In this case, we say that g extends f. This order is a cpo, where the least element is the nowhere defined function (with empty domain). In fact, ≤ is also bounded complete. This example also demonstrates why it is not always natural to have a greatest element.
- The specialization order of any sober space is a dcpo.
- Every finite poset is directed complete, every finite poset with a least element is a cpo.
- All complete lattices are of course also directed complete and thus provide numerous (though not particularly instructive) examples for dcpos.