{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T04:35:49Z","timestamp":1716957349213},"reference-count":82,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2009,8]]},"abstract":"<jats:p>Abstract Stone Duality (ASD) is a direct axiomatisation of general topology, in contrast to the traditional and all other contemporary approaches, which rely on a prior notion of discrete set, type or object of a topos.<\/jats:p><jats:p>ASD reconciles mathematical and computational viewpoints, providing an inherently computable calculus that does not sacrifice key properties of real analysis such as compactness of the closed interval. Previous theories of recursive analysis failed to do this because they were based on points; ASD succeeds because, like locale theory and formal topology, it is founded on the algebra of open subspaces.<\/jats:p><jats:p>ASD is presented as a lambda calculus, of which we provide a self-contained summary, as the foundational background has been investigated in earlier work.<\/jats:p><jats:p>The core of the paper constructs the real line using two-sided Dedekind cuts. We show that the closed interval is compact and overt, where these concepts are defined using quantifiers. Further topics, such as the Intermediate Value Theorem, are presented in a separate paper that builds on this one.<\/jats:p><jats:p>The interval domain plays an important foundational role. However, we see intervals as generalised Dedekind cuts, which <jats:italic>underly<\/jats:italic> the construction of the real line, not as sets or pairs of real numbers.<\/jats:p><jats:p>We make a thorough study of arithmetic, in which our operations are more complicated than Moore's, because we work constructively, and we also consider back-to-front (Kaucher) intervals.<\/jats:p><jats:p>Finally, we compare ASD with other systems of constructive and computable topology and analysis.<\/jats:p>","DOI":"10.1017\/s0960129509007695","type":"journal-article","created":{"date-parts":[[2009,6,8]],"date-time":"2009-06-08T10:07:18Z","timestamp":1244455638000},"page":"757-838","source":"Crossref","is-referenced-by-count":8,"title":["The Dedekind reals in abstract Stone duality"],"prefix":"10.1017","volume":"19","author":[{"given":"ANDREJ","family":"BAUER","sequence":"first","affiliation":[]},{"given":"PAUL","family":"TAYLOR","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,8,1]]},"reference":[{"key":"S0960129509007695_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-67678-9"},{"key":"S0960129509007695_ref21","first-page":"852","article-title":"Un contre-example relatif aux fonctionnelles r\u00e9cursives","volume":"247","author":"Friedberg","year":"1958","journal-title":"Comptes rendus hebdomadaires des sc\u00e9ances de l'Acad\u00e9mie des Sciences (Paris)"},{"key":"S0960129509007695_ref19","first-page":"21","article-title":"Synthetic topology of data types and classical spaces","volume":"87","author":"Escard\u00f3","year":"2004","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0960129509007695_ref16","volume-title":"Essays on the theory of numbers","author":"Dedekind","year":"1901"},{"key":"S0960129509007695_ref12","volume-title":"Types for Proofs and Programs","author":"Cederquist","year":"1996"},{"key":"S0960129509007695_ref17","volume-title":"Gesammelte mathematische Werke","author":"Dedekind","year":"1932"},{"key":"S0960129509007695_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00285-0"},{"key":"S0960129509007695_ref15","unstructured":"Dedekind Richard (1872). Stetigkeit und irrationale Zahlen. Braunschweig. Reprinted in (Dedekind 1932), pages 315\u2013334; English translation, Continuity and Irrational Numbers, in (Dedekind 1901)."},{"key":"S0960129509007695_ref69","unstructured":"[F] Taylor Paul (2002) Scott domains in abstract Stone duality."},{"key":"S0960129509007695_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.03.027"},{"key":"S0960129509007695_ref13","first-page":"125","article-title":"Logical arithmetic","volume":"2","author":"Cleary","year":"1987","journal-title":"Future Computing Systems"},{"key":"S0960129509007695_ref2","volume-title":"Fifth International Conference on Computability and Complexity in Analysis","author":"Bauer","year":"2008"},{"key":"S0960129509007695_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61667-9"},{"key":"S0960129509007695_ref53","first-page":"2076","article-title":"What is continuity, constructively?","volume":"11","author":"Schuster","year":"2005","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129509007695_ref7","volume-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"S0960129509007695_ref26","volume-title":"Intuitionism, an Introduction","author":"Heyting","year":"1956"},{"key":"S0960129509007695_ref14","volume-title":"On Numbers and Games","author":"Conway","year":"1976"},{"key":"S0960129509007695_ref23","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S0960129509007695_ref51","unstructured":"Rosolini Giuseppe (1986). Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford."},{"key":"S0960129509007695_ref65","first-page":"300","article-title":"Subspaces in abstract Stone duality","volume":"10","author":"Taylor","year":"2002","journal-title":"Theory and Applications of Categories"},{"key":"S0960129509007695_ref30","volume-title":"Topos Theory","author":"Johnstone","year":"1977"},{"key":"S0960129509007695_ref63","volume-title":"Foundational Theories of Mathematics","author":"Taylor","year":"2009"},{"key":"S0960129509007695_ref71","unstructured":"[H] Taylor Paul (2004) An elementary theory of various categories of spaces and locales."},{"key":"S0960129509007695_ref9","volume-title":"Topologie G\u00e9n\u00e9rale","author":"Bourbaki","year":"1966"},{"key":"S0960129509007695_ref1","unstructured":"Bauer Andrej (2000). The Realizability Approach to Computable Analysis and Topology. PhD thesis, Carnegie Mellon University. Technical report CMU-CS-00-164."},{"key":"S0960129509007695_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00097-8"},{"key":"S0960129509007695_ref28","volume-title":"Category Theory","author":"Hyland","year":"1991"},{"key":"S0960129509007695_ref73","unstructured":"[K] Taylor Paul (2006) Interval analysis without intervals. In Real Numbers and Computers, Guillaume Hanrot and Zimmermann Paul , editors, Nancy."},{"key":"S0960129509007695_ref49","volume-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","year":"1992"},{"key":"S0960129509007695_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S0960129509007695_ref56","unstructured":"Spitters Bas (2007). Located and overt sublocales. arxiv.org\/abs\/math\/0703561."},{"key":"S0960129509007695_ref50","volume-title":"Reuniting the Antipodes: Constructive and Nonstandard Views of the Continuum","author":"Rosemeier","year":"2001"},{"key":"S0960129509007695_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061811"},{"key":"S0960129509007695_ref25","unstructured":"Hanrot Guillaume , Lef\u00e8vre Vincent , P\u00e9lissier Patrick , and Zimmermann Paul . The MPFR Library. INRIA. www.mpfr.org."},{"key":"S0960129509007695_ref32","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/030\/749770"},{"key":"S0960129509007695_ref29","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-60.1.1"},{"key":"S0960129509007695_ref55","volume-title":"Formal Semantics of Programming Languages","author":"Scott","year":"1972"},{"key":"S0960129509007695_ref31","volume-title":"Stone Spaces","author":"Johnstone","year":"1982"},{"key":"S0960129509007695_ref33","doi-asserted-by":"crossref","DOI":"10.1090\/memo\/0309","volume-title":"An Extension of the Galois Theory of Grothendieck","author":"Joyal","year":"1984"},{"key":"S0960129509007695_ref81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56999-9"},{"key":"S0960129509007695_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565663"},{"key":"S0960129509007695_ref35","volume-title":"Fundamentals of Numerical Computation","author":"Kaucher","year":"1980"},{"key":"S0960129509007695_ref36","first-page":"95","article-title":"Interval computations: Introduction, uses and resources","volume":"2","author":"Kearfott","year":"1996","journal-title":"Euromath Bulletin"},{"key":"S0960129509007695_ref37","first-page":"109","article-title":"A survey of totality in ordinary and enriched categories","volume":"27","author":"Kelly","year":"1986","journal-title":"Cahiers de G\u00e9ometrie et Topologie Differentielle"},{"key":"S0960129509007695_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005822"},{"key":"S0960129509007695_ref38","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"key":"S0960129509007695_ref6","first-page":"129","article-title":"The fan theorem and positive-valued uniformly continuous functions on compact intervals","volume":"38","author":"Berger","year":"2008","journal-title":"New Zealand Journal of Mathematics"},{"key":"S0960129509007695_ref39","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511550812"},{"key":"S0960129509007695_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/BF02425913"},{"key":"S0960129509007695_ref41","unstructured":"Lakeyev Anatoly (1995). Linear algebraic equations in Kaucher arithmetic. In Applications of Interval Computations (APIC'95), Vladik Kreinovich , editor. supplement to Reliable Computing."},{"key":"S0960129509007695_ref45","volume-title":"From Sets and Types to Topology and Analysis: Towards Practicable Foundations of Constructive Mathematics","author":"Palmgren","year":"2005"},{"key":"S0960129509007695_ref34","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1984.111.333"},{"key":"S0960129509007695_ref46","first-page":"565","article-title":"Studii di logica matematica","volume":"32","author":"Peano","year":"1897","journal-title":"Atti della Reale Accademia di Torino"},{"key":"S0960129509007695_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129509007695_ref48","volume-title":"Non-standard Analysis","author":"Robinson","year":"1966"},{"key":"S0960129509007695_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00707-7"},{"key":"S0960129509007695_ref57","article-title":"Binary floating-point arithmetic","volume":"754","author":"Stevenson","year":"1985","journal-title":"ANSI\/IEEE Standard"},{"key":"S0960129509007695_ref54","volume-title":"Toposes, Algebraic Geometry and Logic","author":"Scott","year":"1972"},{"key":"S0960129509007695_ref60","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(78)90160-6"},{"key":"S0960129509007695_ref27","volume-title":"The L.E.J. Brouwer Centenary Symposium","author":"Hyland","year":"1982"},{"key":"S0960129509007695_ref58","doi-asserted-by":"publisher","DOI":"10.1007\/BF01443264"},{"key":"S0960129509007695_ref59","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1980-0558176-3"},{"key":"S0960129509007695_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-007-0063-1"},{"key":"S0960129509007695_ref44","volume-title":"Computability and Complexity in Analysis: 4th International Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers","author":"M\u00fcller","year":"2001"},{"key":"S0960129509007695_ref61","volume-title":"Logic in Computer Science 6","author":"Taylor","year":"1991"},{"key":"S0960129509007695_ref62","volume-title":"Practical Foundations of Mathematics","author":"Taylor","year":"1999"},{"key":"S0960129509007695_ref64","first-page":"248","article-title":"Sober spaces and continuations","volume":"10","author":"Taylor","year":"2002","journal-title":"Theory and Applications of Categories"},{"key":"S0960129509007695_ref67","unstructured":"[D] Taylor Paul (2000) Non-Artin gluing in recursion theory and lifting in abstract Stone duality."},{"key":"S0960129509007695_ref68","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.059"},{"key":"S0960129509007695_ref70","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(1:1)2006"},{"key":"S0960129509007695_ref43","volume-title":"Interval Analysis","author":"Moore","year":"1966"},{"key":"S0960129509007695_ref72","unstructured":"[J] Taylor Paul (2005) A lambda calculus for real analysis. In Computability and Complexity in Analysis, Tanja Grubba , editors, volume 326 of Informatik Berichte, FernUniversit\u00e4t in Hagen."},{"key":"S0960129509007695_ref74","unstructured":"[L] Taylor Paul (2004) Tychonov's theorem in abstract Stone duality."},{"key":"S0960129509007695_ref75","unstructured":"[M] Taylor Paul (2009) Cartesian closed categories with subspaces."},{"key":"S0960129509007695_ref76","unstructured":"Thielecke Hayo (1997). Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh. ECS-LFCS-97-376."},{"key":"S0960129509007695_ref77","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700005992"},{"key":"S0960129509007695_ref78","volume-title":"Constructivism in Mathematics, an Introduction","author":"Troelstra","year":"1988"},{"key":"S0960129509007695_ref79","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)90047-7"},{"key":"S0960129509007695_ref80","doi-asserted-by":"publisher","DOI":"10.1007\/s10699-004-3065-z"},{"key":"S0960129509007695_ref82","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(82)90055-2"},{"key":"S0960129509007695_ref4","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn026"},{"key":"S0960129509007695_ref66","first-page":"284","article-title":"Geometric and higher order logic using abstract Stone duality","volume":"7","author":"Taylor","year":"2000","journal-title":"Theory and Applications of Categories"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129509007695","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T19:37:26Z","timestamp":1553974646000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129509007695\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":82,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["S0960129509007695"],"URL":"https:\/\/doi.org\/10.1017\/s0960129509007695","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8]]}}}