Papers › Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
Todd Waugh Ambridge
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
The real numbers are important in both mathematics and computation theory. Computationally, real numbers can be represented in several ways; most commonly using inexact floating-point data-types, but also using exact arbitrary-precision data-types which satisfy the expected mathematical properties of the reals. This thesis is concerned with formalising properties of certain types for exact real arithmetic, as well as utilising them computationally for the purposes of search, optimisation and regression. We develop, in a constructive and univalent type-theoretic foundation of mathematics, a formalised framework for performing search, optimisation and regression on a wide class of types. This framework utilises Mart\'in Escard\'o's prior work on searchable types, along with a convenient version of ultrametric spaces -- which we call closeness spaces -- in order to consistently search certain infinite types using the functional programming language and proof assistant Agda. We formally define and prove the convergence properties of type-theoretic variants of global optimisation and parametric regression, problems related to search from the literature of analysis. As we work in a constructive setting, these convergence theorems yield computational algorithms for correct optimisation and regression on the types of our framework. Importantly, we can instantiate our framework on data-types from the literature of exact real arithmetic, allowing us to perform our variants of search, optimisation and regression on ternary signed-digit encodings of the real numbers, as well as a simplified version of Hans-J. Boehm's functional encodings of real numbers. Furthermore, we contribute to the extensive work on ternary signed-digits by formally verifying the definition of certain exact real arithmetic operations using the Escard\'o-Simpson interval object specification of compact intervals.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections