Extensional constructive real analysis via locators

TL;DR

This paper introduces locators, a structure on real numbers that enables extensional observation of discrete information, bridging constructive analysis with observable representations like signed-digit expansions.

Contribution

It proposes locators as a new structure on real numbers, allowing extensional access to discrete data, and connects this with classical representations in constructive analysis.

Findings

Locators enable construction of signed-digit representations.

Locators allow extracting discrete information constructively.

The approach bridges computable analysis and constructive real analysis.

Abstract

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.