Extensional constructive real analysis via locators

摘要

Real numbers do not admit an extensional procedure for observing discrete information, such as the firstdigit of its decimal expansion, because every extensional, computable map from the reals to the integersis constant, as is well known. We overcome this by considering real numbers equipped with additionalstructure, which we call a locator. With this structure, it is possible, for instance, to construct a signeddigitrepresentation or a Cauchy sequence, and conversely, these intensional representations give rise toa locator. Although the constructions are reminiscent of computable analysis, instead of working with anotion of computability, we simply work constructively to extract observable information, and instead ofworking with representations, we consider a certain locatedness structure on real numbers.