A Constructive, Type-Theoretic Approach to Regression via Global Optimisation
This work provides a theoretical foundation for regression using constructive methods, which is incremental in applying type theory to optimization problems.
The paper connects deterministic global optimization of continuous functions to regression through constructive type theory and searchability, showing that convergence in global optimization implies convergence criteria for regression, with all theory formalized in Agda.
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.