论文标题
通过全球优化的一种建设性的，类型的理论方法回归
A Constructive, Type-Theoretic Approach to Regression via Global Optimisation
论文作者
论文摘要
我们通过“可搜索性”的概念从建设性类型理论的角度来研究了连续函数的确定性，完整和一般全局优化与回归的一般概念之间的联系。我们看到全局优化的收敛性属性是可搜索性的直接结果。抽象设置使我们能够将可搜索性和连续性概括为高阶函数，因此我们可以制定回归的新型收敛标准，这些标准源自全局优化的收敛性。在证明助理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.
