A constructive theory of continuous domains suitable for implementation (Q1023289): Difference between revisions

The paper presents a predicative, constructive approach to the theory of \(\omega\)-continuous domains. The main example the authors are interested in is the interval domain consisting of all closed real intervals and its application to exact real number computation. They show how to present the theory in such a way that its realizability interpretation in the category of modest sets directly corresponds to practical implementation. This interpretation validates first-order intuitionistic logic as well as the extra-logical principles number choice, dependent choice, and Markov principle. Powersets are not allowed because they cannot be represented as modest sets. Continuous domains allow to represent their elements as least upper bounds of directed sets of base elements. In the \(\omega\)-continuous case it suffices to consider only least upper bounds of increasing sequences of such elements. Sequences are more suited for the authors' practical needs than general directed sets. The authors reformulate essential domain-theoretic notions and constructions in such a way that only base elements and sequences of them are used.