Sharp elements and apartness in domains

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Downloads (Pure)

Abstract


Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of sharp elements. Being apart is a positive formulation of being unequal, similar to how inhabitedness is a positive formulation of nonemptiness. To exemplify sharpness, we note that a lower real is sharp if and only if it is located. Our first main result is that for a large class of continuous dcpos, the Bridges-Vita apartness topology and the Scott topology coincide. Although we cannot expect a tight or cotransitive apartness on nontrivial dcpos, we prove that the intrinsic apartness is both tight and cotransitive when restricted to the sharp elements of a continuous dcpo. These include the strongly maximal elements, as studied by Smyth and Heckmann. We develop the theory of strongly maximal elements highlighting its connection to sharpness and the Lawson topology. Finally, we illustrate the intrinsic apartness, sharpness and strong maximality by considering several natural examples of continuous dcpos: the Cantor and Baire domains, the partial Dedekind reals and the lower reals.
Original languageEnglish
Title of host publicationProceedings 37th Conference on Mathematical Foundations of Programming Semantics
PublisherElectronic Proceedings in Theoretical Computer Science
Pages134–151
Publication statusPublished - 29 Dec 2021
Event37th Conference on Mathematical Foundations of Programming Semantics - Salzburg, Austria
Duration: 30 Aug 20212 Sep 2021
https://easychair.org/cfp/MFPS37

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Number351

Conference

Conference37th Conference on Mathematical Foundations of Programming Semantics
Abbreviated titleMFPS37
Country/TerritoryAustria
CitySalzburg
Period30/08/212/09/21
Internet address

Fingerprint

Dive into the research topics of 'Sharp elements and apartness in domains'. Together they form a unique fingerprint.

Cite this