A Constructive, Type-Theoretic Approach to Regression via Global Optimisation

TL;DR

This paper presents a constructive, type-theoretic framework linking global optimisation and regression, formalised in Agda, enabling new convergence criteria based on searchability and higher-order functions.

Contribution

It introduces a novel formalisation connecting global optimisation and regression using constructive type theory and searchability, extending to higher-order functions.

Findings

Convergence of global optimisation follows from searchability.

Generalised searchability and continuity for higher-order functions.

Formalisation of the theory in Agda.

Abstract

We examine the connections between deterministic, complete, and general global optimisation of continuous functions and a general concept of regression from the perspective of constructive type theory via the concept of 'searchability'. We see how the property of convergence of global optimisation is a straightforward consequence of searchability. The abstract setting allows us to generalise searchability and continuity to higher-order functions, so that we can formulate novel convergence criteria for regression, derived from the convergence of global optimisation. All the theory and the motivating examples are fully formalised in the proof assistant Agda.