{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:12Z","timestamp":1747173432540,"version":"3.40.5"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T00:00:00Z","timestamp":1599004800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map from the reals to the integers is constant, as is well known. We overcome this by considering real numbers equipped with additional structure, which we call a locator. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy sequence, and conversely, these intensional representations give rise to a locator. Although the constructions are reminiscent of computable analysis, instead of working with a notion of computability, we simply work constructively to extract observable information, and instead of working with representations, we consider a certain locatedness structure on real numbers.<\/jats:p>","DOI":"10.1017\/s0960129520000171","type":"journal-article","created":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T08:49:11Z","timestamp":1599036551000},"page":"64-88","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Extensional constructive real analysis via locators"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3324-3167","authenticated-orcid":false,"given":"Auke B.","family":"Booij","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2020,9,2]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Taylor, P. (2010). A lambda calculus for real analysis. Journal of Logic and Analysis 2. http:\/\/logicandanalysis.org\/index.php\/jla\/article\/view\/63\/25.","key":"S0960129520000171_ref21","DOI":"10.4115\/jla.2010.2.5"},{"unstructured":"Booij, A. B. (2020b). Analysis in Univalent Type Theory. PhD thesis, University of Birmingham.","key":"S0960129520000171_ref4"},{"unstructured":"Bridges, D. and Richman, F. (1987). Varieties of Constructive Mathematics, London Mathematical Society Lecture Notes, vol. 97, Cambridge, Cambridge University Press.","key":"S0960129520000171_ref5"},{"doi-asserted-by":"crossref","unstructured":"Turing, A. M. (1937). On computable numbers, with an application to the Entscheidungsproblem. A correction. Proceedings of the London Mathematical Society. Second Series 43, 544\u2013546. See Turning (1936).","key":"S0960129520000171_ref25","DOI":"10.1112\/plms\/s2-43.6.544"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref10","DOI":"10.4230\/LIPIcs.TLCA.2015.153"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref2","DOI":"10.1007\/978-3-642-61667-9"},{"unstructured":"Booij, A. B. (2020a). Coq development of locators. https:\/\/github.com\/abooij\/HoTT\/tree\/locators (accessed February 2020).","key":"S0960129520000171_ref3"},{"volume-title":"Techniques of Constructive Analysis","year":"2006","author":"Bridges","key":"S0960129520000171_ref6"},{"unstructured":"Hofmann, M. (1995). Extensional Concepts in Intensional Type theory. PhD thesis, University of Edinburgh.","key":"S0960129520000171_ref13"},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013","author":"Univalent Foundations Program","key":"S0960129520000171_ref22"},{"unstructured":"Wiedmer, E. (1977). Exaktes Rechnen mit reellen Zahlen und anderen unendlichen Objekten. PhD thesis, ETH Zurich.","key":"S0960129520000171_ref26"},{"unstructured":"O\u2019Connor, R. (2009). Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory. PhD thesis, Radboud Universiteit Nijmegen.","key":"S0960129520000171_ref18"},{"volume-title":"Studies in Logic and the Foundations of Mathematics","year":"1988","author":"Troelstra","key":"S0960129520000171_ref23"},{"unstructured":"Frank, M. (2017). Interpolating between choices for the approximate intermediate value theorem. ArXiv e-prints, January 2017. arXiv:1701.02227.","key":"S0960129520000171_ref11"},{"unstructured":"Schwichtenberg, H. (2017). Constructive analysis with witnesses. http:\/\/www.math.lmu.de\/~schwicht\/seminars\/semws16\/constr16.pdf.","key":"S0960129520000171_ref20"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref14","DOI":"10.1007\/978-1-4471-0717-0_2"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref17","DOI":"10.1007\/978-3-319-43144-4_17"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref12","DOI":"10.1016\/j.apal.2011.12.026"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref19","DOI":"10.1515\/9783110199680.227"},{"unstructured":"Escard\u00f3, M. H. (2013). Message to the Univalent Foundations mailing list. https:\/\/groups.google.com\/d\/msg\/univalent-foundations\/SA0dzenV1G4\/d5iIGdKKNxMJ.","key":"S0960129520000171_ref9"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref7","DOI":"10.1007\/BF01458382"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref16","DOI":"10.1016\/j.entcs.2006.09.012"},{"doi-asserted-by":"publisher","key":"S0960129520000171_ref1","DOI":"10.1145\/3018610.3018615"},{"key":"S0960129520000171_ref15","article-title":"Notions of anonymous existence in Martin-L\u00f6f type theory","volume":"13","author":"Kraus","year":"2017","journal-title":"Logical Methods in Computer Science"},{"unstructured":"Cruz-Filipe, L. (2004). Constructive Real Analysis: A Type-Theoretical Formalization and Applications. PhD thesis, University of Nijmegen.","key":"S0960129520000171_ref8"},{"doi-asserted-by":"crossref","unstructured":"Turing, A. M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. Second Series 42, 230\u2013265. See correction Turning (1937).","key":"S0960129520000171_ref24","DOI":"10.1112\/plms\/s2-42.1.230"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129520000171","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,8]],"date-time":"2021-09-08T14:18:01Z","timestamp":1631110681000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129520000171\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,2]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["S0960129520000171"],"URL":"https:\/\/doi.org\/10.1017\/s0960129520000171","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2020,9,2]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}