A constructive theory of continuous domains suitable for implementation (Q1023289): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2008.09.025 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2014504638 / rank | |||
Normal rank |
Revision as of 00:21, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A constructive theory of continuous domains suitable for implementation |
scientific article |
Statements
A constructive theory of continuous domains suitable for implementation (English)
0 references
11 June 2009
0 references
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.
0 references
domain theory
0 references
constructive mathematics
0 references
real number computation
0 references
realizability interpretation
0 references
modest sets
0 references
computable analysis
0 references