Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics

TL;DR

This thesis develops, 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, and formally defines and proves the convergence properties of type-theoretic variants of global optimisation and parametric regression.

Abstract

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ín Escardó'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ó-Simpson interval object specification of compact intervals.

Figures (14)

• Figure 1: Commutative diagram illustrating \ref{['lem:truncate-commute']}.
• Figure 2: Example indices of countably-many extended naturals $c_i := c_{T_i}(\alpha_i,\beta_i)$ from countably-many closeness functions $\ty{c_{T_i}}{T_i \to T_i \to \Ni}$ using $\ty{\alpha,\beta}{\Pi T}$. The first four diagonals are coloured differently for emphasis.
• Figure 3: Graph of the function $f(x) = x^6 - x^4 + x^3 + x^2$ with $-1.1 \leq x \leq 1$.
• Figure 4: Illustration of the universal property \ref{['def:universal']}; the map $\ty{h}{A \to B}$maps points on the bipointed convex body $(A,\oplus_A,M_A,u,v)$to the relative point on the bipointed convex body $(B,\oplus_B,M_B,s,t)$. The colours used here are as in the illustration.
• Figure 5: Commutative diagram illustrating \ref{['def:representation-map']}.

Theorems & Definitions (531)

• definition 1
• lemma 1
• proof
• lemma 2
• proof
• definition 2
• definition 3
• lemma 3
• proof
• lemma 4