Main Page: Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
← Older edit
No edit summary
No edit summary
 
(476 intermediate revisions by more than 100 users not shown)
Line 1: Line 1:
In [[mathematics]], '''directed-complete partial orders''' (abbreviated to '''dcpo''' or sometimes just '''cpo''') are special classes of [[partially ordered set]]s, characterized by particular [[completeness (order theory)|completeness properties]]. Complete partial orders play a central role in [[theoretical computer science]], in [[denotational semantics]] and [[domain theory]].
This is a preview for the new '''MathML rendering mode''' (with SVG fallback), which is availble in production for registered users.


== Definitions ==
If you would like use the '''MathML''' rendering mode, you need a wikipedia user account that can be registered here [[https://en.wikipedia.org/wiki/Special:UserLogin/signup]]
* Only registered users will be able to execute this rendering mode.
* Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere.


A partially ordered set is a '''directed-complete partial order''' ('''dcpo''') if each of its [[directed set|directed subsets]] has a [[supremum]]. Recall that a subset of a partial order is directed if it is non-empty and every pair of elements has an upper bound in the set. In the literature, dcpos sometimes also appear under the label '''up-complete poset''' or simply '''cpo'''.
Registered users will be able to choose between the following three rendering modes:


In some contexts, the phrase [[chain complete|ω-cpo]] (or just '''cpo''') is used to describe a poset in which every ω-chain (''x''<sub>1</sub>≤''x''<sub>2</sub>≤''x''<sub>3</sub>≤''x''<sub>4</sub>≤...) has a supremum. Every dcpo is an ω-cpo.
'''MathML'''
:<math forcemathmode="mathml">E=mc^2</math>


An important role is played by dcpo's with a least element. They are sometimes called '''pointed dcpo'''s, or '''cppo'''s, or just '''cpo'''s.
<!--'''PNG''' (currently default in production)
:<math forcemathmode="png">E=mc^2</math>


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. This intuition, in the context of denotational semantics, was the motivation behind the development of [[domain theory]].
'''source'''
:<math forcemathmode="source">E=mc^2</math> -->


The [[duality (order theory)|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.
<span style="color: red">Follow this [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering link] to change your Math rendering settings.</span> You can also add a [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering-skin Custom CSS] to force the MathML/SVG rendering or select different font families. See [https://www.mediawiki.org/wiki/Extension:Math#CSS_for_the_MathML_with_SVG_fallback_mode these examples].


== Examples ==
==Demos==


* Every finite poset is directed complete.
Here are some [https://commons.wikimedia.org/w/index.php?title=Special:ListFiles/Frederic.wang demos]:
* All [[complete lattice]]s are also directed complete.
* For any poset, the set of all [[non-empty]] [[filter (mathematics)|filters]], ordered by subset inclusion, is a dcpo. Together with the empty filter it is also pointed. If the order has binary [[join and meet|meets]], then this construction (including the empty filter) actually yields a [[complete lattice]].
* The set of all [[partial function]]s on some given set ''S'' can be ordered by defining ''f''&nbsp;≤&nbsp;''g'' for functions ''f'' and ''g'' if and only if ''g'' extends ''f'', i.e. if 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. (Equivalently, ''f''&nbsp;≤&nbsp;''g'' if and only if ''f''&nbsp;⊆&nbsp;''g'' where ''f'' and ''g'' are identified with their respective [[graph of a function|graphs]].) This order is a pointed dcpo, 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.
* Let us use the term “[[deductive system]]” as a set of sentences closed under consequence (for defining notion of consequence, let us use e.g. Tarski's algebraic approach<ref name=Tar-BizIg>Tarski, Alfred: Bizonyítás és igazság / Válogatott tanulmányok. Gondolat, Budapest, 1990. (Title means: Proof and truth / Selected papers.)</ref><ref name=BurSan-UnivAlg>[http://www.math.uwaterloo.ca/~snburris/index.html Stanley N. Burris] and H.P. Sankappanavar: [http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html A Course in Universal Algebra]</ref>). There are interesting theorems which concern a set of deductive systems being a directed complete partial ordering.<ref name=seqdcpo>See online in p. 24 exercises 5–6 of §5 in [[#_note-BurSan-UnivAlg|BurSan:UnivAlg]]. Or, on paper, see [[#_note-Tar-BizIg|Tar:BizIg]].</ref> Also, a set of deductive systems can be chosen to have a least element in a natural way (so that it can be also a complete partial ordering), because the set of all consequences of the empty set (i.e. “the set of the logically provable / logically valid sentences”) is (1) a deductive system (2) contained by all deductive systems.


== Properties ==


An ordered set ''P'' is a pointed dcpo if and only if every [[chain (order theory)|chain]] has a supremum in ''P''. Alternatively, an ordered set ''P'' is a pointed dcpo if and only if every [[order-preserving]] self-map of ''P'' has a least [[fixpoint]]. Every set ''S'' can be turned into a pointed dcpo by adding a least element ⊥ and introducing a flat order with ⊥&nbsp;≤&nbsp;''s'' and s&nbsp;≤&nbsp;''s'' for every ''s''&nbsp;∈&nbsp;''S'' and no other order relations.
* accessibility:
** Safari + VoiceOver: [https://commons.wikimedia.org/wiki/File:VoiceOver-Mac-Safari.ogv video only], [[File:Voiceover-mathml-example-1.wav|thumb|Voiceover-mathml-example-1]], [[File:Voiceover-mathml-example-2.wav|thumb|Voiceover-mathml-example-2]], [[File:Voiceover-mathml-example-3.wav|thumb|Voiceover-mathml-example-3]], [[File:Voiceover-mathml-example-4.wav|thumb|Voiceover-mathml-example-4]], [[File:Voiceover-mathml-example-5.wav|thumb|Voiceover-mathml-example-5]], [[File:Voiceover-mathml-example-6.wav|thumb|Voiceover-mathml-example-6]], [[File:Voiceover-mathml-example-7.wav|thumb|Voiceover-mathml-example-7]]
** [https://commons.wikimedia.org/wiki/File:MathPlayer-Audio-Windows7-InternetExplorer.ogg Internet Explorer + MathPlayer (audio)]
** [https://commons.wikimedia.org/wiki/File:MathPlayer-SynchronizedHighlighting-WIndows7-InternetExplorer.png Internet Explorer + MathPlayer (synchronized highlighting)]
** [https://commons.wikimedia.org/wiki/File:MathPlayer-Braille-Windows7-InternetExplorer.png Internet Explorer + MathPlayer (braille)]
** NVDA+MathPlayer: [[File:Nvda-mathml-example-1.wav|thumb|Nvda-mathml-example-1]], [[File:Nvda-mathml-example-2.wav|thumb|Nvda-mathml-example-2]], [[File:Nvda-mathml-example-3.wav|thumb|Nvda-mathml-example-3]], [[File:Nvda-mathml-example-4.wav|thumb|Nvda-mathml-example-4]], [[File:Nvda-mathml-example-5.wav|thumb|Nvda-mathml-example-5]], [[File:Nvda-mathml-example-6.wav|thumb|Nvda-mathml-example-6]], [[File:Nvda-mathml-example-7.wav|thumb|Nvda-mathml-example-7]].
** Orca: There is ongoing work, but no support at all at the moment [[File:Orca-mathml-example-1.wav|thumb|Orca-mathml-example-1]], [[File:Orca-mathml-example-2.wav|thumb|Orca-mathml-example-2]], [[File:Orca-mathml-example-3.wav|thumb|Orca-mathml-example-3]], [[File:Orca-mathml-example-4.wav|thumb|Orca-mathml-example-4]], [[File:Orca-mathml-example-5.wav|thumb|Orca-mathml-example-5]], [[File:Orca-mathml-example-6.wav|thumb|Orca-mathml-example-6]], [[File:Orca-mathml-example-7.wav|thumb|Orca-mathml-example-7]].
** From our testing, ChromeVox and JAWS are not able to read the formulas generated by the MathML mode.


== Continuous functions and fixpoints ==
==Test pages ==


A function ''f'' between two dcpos ''P'' and ''Q'' is called [[Scott continuity|'''(Scott) continuous''']] if it maps directed sets to directed sets while preserving their suprema:
To test the '''MathML''', '''PNG''', and '''source''' rendering modes, please go to one of the following test pages:
* <math>f(D) \subseteq Q</math> is directed for every directed <math>D \subseteq P</math>.
*[[Displaystyle]]
* <math>f(\sup D) = \sup f(D)</math> for every directed <math>D \subseteq P</math>.
*[[MathAxisAlignment]]
Note that every continuous function between dcpos is a [[monotone|monotone function]].
*[[Styling]]
This notion of continuity is equivalent to the topological continuity induced by the [[Scott topology]].
*[[Linebreaking]]
*[[Unique Ids]]
*[[Help:Formula]]


The set of all continuous functions between two dcpos ''P'' and ''Q'' is denoted <nowiki>[</nowiki>''P''&nbsp;→&nbsp;''Q''<nowiki>]</nowiki>. Equipped with the pointwise order, this is again a dcpo, and a cpo whenever ''Q'' is a cpo.
*[[Inputtypes|Inputtypes (private Wikis only)]]
Thus the complete partial orders with Scott continuous maps form a [[cartesian closed category]].<ref name="barendregt1984">[[Henk Barendregt|Barendregt, Henk]], [http://www.elsevier.com/wps/find/bookdescription.cws_home/501727/description#description ''The lambda calculus, its syntax and semantics''], [[North-Holland]] (1984)</ref>
*[[Url2Image|Url2Image (private Wikis only)]]
 
==Bug reporting==
Every order-preserving self-map ''f'' of a cpo (''P'', ⊥) has a least fixpoint.<ref>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.</ref> If ''f'' is continuous then this fixpoint is equal to the supremum of the [[Iterated function|iterates]] (⊥, ''f''(⊥), ''f''(''f''(⊥)), … ''f''<sup>''n''</sup>(⊥), …) of ⊥ (see also the [[Kleene fixpoint theorem]]).
If you find any bugs, please report them at [https://bugzilla.wikimedia.org/enter_bug.cgi?product=MediaWiki%20extensions&component=Math&version=master&short_desc=Math-preview%20rendering%20problem Bugzilla], or write an email to math_bugs (at) ckurs (dot) de .
 
== See also ==
 
Directed completeness relates in various ways to other [[completeness (order theory)|completeness]] notions. Directed completeness alone is quite a basic property that occurs often in other order theoretic investigations, using for instance [[algebraic poset]]s and the [[Scott topology]].
 
== Notes ==
 
<references/>
 
== References ==
* {{cite book
| author = Davey, B.A., and Priestley, H. A.
| year = 2002
| title = '''Introduction to Lattices and Order'''
| edition = Second
| publisher = Cambridge University Press
| isbn = 0-521-78451-4
}}
 
{{DEFAULTSORT:Complete Partial Order}}
[[Category:Order theory]]
 
[[fr:Ordre partiel complet (informatique)]]
[[pl:Porządek zupełny]]
[[ru:Частично упорядоченное множество#Полное частично упорядоченное множество]]
[[zh:完全偏序]]

Latest revision as of 22:52, 15 September 2019

This is a preview for the new MathML rendering mode (with SVG fallback), which is availble in production for registered users.

If you would like use the MathML rendering mode, you need a wikipedia user account that can be registered here [[1]]

  • Only registered users will be able to execute this rendering mode.
  • Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere.

Registered users will be able to choose between the following three rendering modes:

MathML

E=mc2


Follow this link to change your Math rendering settings. You can also add a Custom CSS to force the MathML/SVG rendering or select different font families. See these examples.

Demos

Here are some demos:


Test pages

To test the MathML, PNG, and source rendering modes, please go to one of the following test pages:

Bug reporting

If you find any bugs, please report them at Bugzilla, or write an email to math_bugs (at) ckurs (dot) de .

Retrieved from "https://en.formulasearchengine.com/index.php?title=Main_Page&oldid=329754"