A correct-by-construction approach to approximate computation

按构造更正程序开发使用高级类型系统来描述通过计算操作的数据以及这些计算的正确性。在软件中嵌入正确性有许多优点，英国和其他地方几十年的开创性工作证明了这一点，这些优点最终形成了AGDA、Idris、CoQ、Lean、HOL、Isabelle等系统，这些系统强大到足以实现这一愿景，现在在学术界和工业界都产生了重大影响。推动这项研究的主要问题是：通过构造修正的编程能否扩展到具有近似值的计算，例如在：i)需要处理固有/模拟随机性的随机系统；ii)资源有限的环境，其中准确的计算代价高得令人望而却步；iii)具有不完全/部分回忆的系统，其中一个人只有关于所发生的事情或每个代理的意图/可信度的有限信息；以及iv)非精确计算，其中原始数据(例如来自传感器)是不准确的并且提供了误差条。例如，这些场景出现在网络物理系统、机器学习、机器人、汽车工程、航空航天和能源系统中。衡量度量与其真实值的接近程度自然会导致度量的使用，但尽管取得了一些成功，它们的使用仍存在一些缺点，例如：i)在一个问题领域中定义的度量通常不会延续到其他问题领域；ii)基于系统结构的度量通常不反映行为相似性，反之亦然；iii)系统结构的日益精确的模型并不能保证具有与建模系统的行为越来越准确的行为。我们推测，这些问题是更深层次问题的表现，即支撑计算的所有数学都以精确相等为原始，因此近似建立在精确的元理论之上。然而，在最近的一项突破中，马代尔和他的合作者引入了数量代数(QA)，它概括了现代数学的核心支柱之一，即普适代数(UA)，允许在形式推理中使用近似公式。这一新思想的普遍性--在数学结构中用更精细的近似推理取代经典推理--给我们提供了一种新的范例，它为适当的近似理论提供了一个严格的逻辑框架，其中界限可以处理，证明可以收敛，极限可以近似。这个项目将通过设计、实现和部署一种新的可信近似计算语言来改变近似计算的理论和应用。它涉及：i)数学研究：我们通过开发支持精确计算的常见数学结构的新的定量概括，复制从UA到QA的转变，以及类似的革命性的从精确计算到近似计算的转变。然后，近似计算将由驱动精确计算的关键结构的这些新的近似版本来驱动。ii)类型理论和编程语言研究：我们开发了一个核心依赖类型理论，结合了近似等式和类型检查，以确保遵守近似界限；我们通过开发高级功能将我们的类型理论转换为可用的编程语言。iii)应用程序和影响生成：我们创建系统生物学和数字双胞胎的案例研究，以验证我们的研究，并与共同创建该提案的学术/行业合作者创造影响。这涉及到近似博弈论的发展，因为这两个案例研究都涉及到需要在存在不确定性的情况下做出最优决策的自主代理。

Correct-by-construction program development uses advanced type systems to describe both the data manipulated by computation, and the correctness of those computations. Embedding correctness within software has many advantages, as certified by several decades of pioneering work in the UK and elsewhere, which have culminated in systems such as Agda, Idris, Coq, Lean, HOL, Isabelle, etc., which are powerful enough to implement this vision and which are now having significant impact in both academia and industry. The main question that motivates this research is: can correct-by-construction programming be extended to computation with approximate values, e.g. in: i) stochastic systems where one needs to handle inherent/simulated randomness; ii) resource limited environments, where exact computation is prohibitively expensive; iii) systems with imperfect/partial recall, where one only has limited information about what has happened or the intentions/trustworthiness of each agent; and iv) non-exact computation where primitive data (e.g. from sensors) is inexact and supplied with error bars. These scenarios arise in e.g. cyber-physical systems, machine learning, robotics, automotive engineering, aerospace, and energy systems. Measuring how close measurements might be from their true values naturally leads to the use of metrics but, despite some successes, their use suffers from a number of drawbacks, e.g. i) metrics defined in one problem domain often do not carry over to others; ii) metrics based upon system structure often do not reflect behavioural similarity and vice-versa; and iii) increasingly accurate models of a system's structure are not guaranteed to have increasingly accurate behaviours to that of the modelled system.We conjecture that these problems are manifestations of the deeper problem that all of the mathematics underpinning computation takes exact equality as primitive, so approximation is built over an exact meta-theory. However, in a recent breakthrough, Mardare and his collaborators introduced Quantitative Algebra (QA) which generalises one of the central pillars of modern mathematics, namely universal algebra (UA), to allow approximate equations in formal reasoning. The generality of this new idea - replacing classical reasoning with a more refined approximate reasoning in the very fabric of mathematics - gives us a new paradigm which supports a rigorous logical framework for a proper approximation theory, where bounds can be handled, convergences proven and limits approximated.This project will transform the theory and applications of approximate computation by designing, implementing and deploying a new language for trusted approximate computation. It involves:i) Mathematical Research: We replicate the shift from UA to QA with a similarly revolutionary one from exact computation to approximate computation by developing new quantitative generalisations of the common mathematical structures underpinning exact computation. Approximate computation will then be driven by these new approximate versions of the key structures that drive exact computation.ii) Type Theory & Programming Languages Research: We develop a core dependent type theory incorporating equality-up-to-approximation and type checking to ensure approximation bounds are adhered to; and we convert our type theory into a usable programming language by developing high level features.iii) Applications and Impact Generation: We create case studies in systems biology and digital twins to validate our research and create impact with academic/industrial collaborators who have co-created this proposal. This involves the development of approximate game theory as both these case studies involve autonomous agents that need to make optimal decisions in the presence of uncertainty.