×

A constructive theory of continuous domains suitable for implementation. (English) Zbl 1169.06005

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.

MSC:

06B35 Continuous lattices and posets, applications
03D65 Higher-type and set recursion theory
03F60 Constructive and recursive analysis
03B70 Logic in computer science

Software:

RZ; iRRAM; gmp; RealLib; MPFR; OCaml
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, Samson; Jung, Achim, Domain theory, (Abramsky, S.; Gabbay, D.; Maibaum, T. S.E., Handbook of Logic in Computer Science Vol. 3 (1994), Oxford University Press)
[2] Andrej Bauer, The Realizability Approach to Computable Analysis and Topology, Available as CMU technical report; Andrej Bauer, The Realizability Approach to Computable Analysis and Topology, Available as CMU technical report
[3] Bauer, Andrej; Kavkler, Iztok, Implementing real numbers with RZ, (Weihrauch, Klaus; Zhong, Ning, Fourth International Conference on Computability and Complexity in Analysis. Fourth International Conference on Computability and Complexity in Analysis, Electronic Notes in Theoretical Computer Science (2007)) · Zbl 1262.03076
[4] Bauer, Andrej; Stone, Christopher A., RZ: A tool for bringing constructive and computable mathematics closer to programming practice, Journal of Logic and Computation, exn026 (2008), Advance access published on August 2, 2008
[5] Berger, Ulrich, Total sets and objects in domain theory, Annals of Pure and Applied Logic, 60, 91-117 (1993) · Zbl 0776.03031
[6] Bishop, Errett; Bridges, Douglas, Constructive Analysis (1985), Springer-Verlag · Zbl 0656.03042
[7] Bridges, Douglas; Richman, Fred, Varieties of constructive mathematics, Number 97 in London Mathematical Society Lecture Notes Series (1987), Cambridge University Press · Zbl 0618.03032
[8] Torbjörn Granlund, et al. GNU Multiple Precision Arithmetic Library. Free Software Foundation. http://gmplib.org/; Torbjörn Granlund, et al. GNU Multiple Precision Arithmetic Library. Free Software Foundation. http://gmplib.org/
[9] Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, Paul Zimmermann, The MPFR Library. INRIA. http://www.mpfr.org/; Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, Paul Zimmermann, The MPFR Library. INRIA. http://www.mpfr.org/
[10] Hyland, J. Martin E., The effective topos, (Troelstra, A. S.; Van Dalen, D., The L.E.J. Brouwer Centenary Symposium (1982), North Holland Publishing Company) · Zbl 0721.03048
[11] Branimir Lambov, Topics in the Theory and Practice of Computable Analysis, Ph.D. Thesis, Department of Computer Science, University of Aarhus, Denmark, December 2005; Branimir Lambov, Topics in the Theory and Practice of Computable Analysis, Ph.D. Thesis, Department of Computer Science, University of Aarhus, Denmark, December 2005 · Zbl 1136.03325
[12] Lambov, Branimir, RealLib: An efficient implementation of exact real arithmetic, Mathematical Structures in Computer Science, 17, 81-98 (2007) · Zbl 1112.65137
[13] Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, Jérôme Vouillon, The Objective Caml system, documentation and user’s manual — release 3.08, Technical report, INRIA, July 2004; Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, Jérôme Vouillon, The Objective Caml system, documentation and user’s manual — release 3.08, Technical report, INRIA, July 2004
[14] Müller, Norbert, The iRRAM: Exact arithmetic in C++, (Blanck, Jens; Brattka, Vasco; Hertling, Peter, Computability and Complexity in Analysis: 4th International Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers. Computability and Complexity in Analysis: 4th International Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers, Lecture Notes in Computer Science, vol. 2064 (2001), Springer), 222-252 · Zbl 0985.65523
[15] Michel Quercia, Numerix: Big Integer Library, version 0.22, INRIA. http://pauillac.inria.fr/ quercia/; Michel Quercia, Numerix: Big Integer Library, version 0.22, INRIA. http://pauillac.inria.fr/ quercia/
[16] Stoltenberg-Hansen, Viggo; Lindström, Ingrid; Griffor, Edward R., Mathematical theory of domains, Cambridge Tracts in Computer Science, vol. 22 (1994), Cambridge University Press · Zbl 0828.06001
[17] Troelstra, Anne S.; van Dalen, Dirk, Constructivism in Mathematics, An Introduction, Vol. 1, Studies in Logic and the Foundations of Mathematics, vol. 121 (1988), North-Holland · Zbl 0653.03040
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.