Extensional constructive real analysis via locators

This is an announcement of a paper in the areas of constructive mathematics, (univalent) type theory, and exact real arithmetic.

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.

To appear in the MSCS Special Issue on Homotopy Type Theory and Univalent Foundations (preprint on the arXiv). This work is also discussed in some more generality in my PhD thesis.

Comments

  1. Nice. What's new or different in the paper compared to the thesis?
    t. Nikolaj-K

    ReplyDelete
  2. @Nikolaj: The main difference with the thesis is that this paper works with the Dedekind reals specifically, rather than with a general Cauchy complete Archimedean ordered field. Additionally, the thesis contains much more background (such as the definition of Cauchy complete Archimedean ordered fields), and stretches the theory of locators a bit further.

    ReplyDelete

Post a Comment