A correct-by-construction approach to approximate computation

构造正确的程序开发使用高级类型系统来描述计算操作的数据和这些计算的正确性。在软件中嵌入正确性有许多优点，正如英国和其他地方几十年的开创性工作所证明的那样，这些工作在Agda，Idris，Coq，Lean，HOL，Isabelle等系统中达到了顶峰，这些技术足以实现这一愿景，并且现在在学术界和工业界都产生了重大影响。激励这项研究的主要问题是：可以通过构造正确的编程扩展到近似值的计算，例如：i）随机系统，其中需要处理固有的/模拟的随机性; ii）资源有限的环境，其中精确的计算是非常昂贵的; iii）具有不完美/部分回忆的系统，其中人们仅具有关于发生了什么或每个代理的意图/可信度的有限信息;以及iv）非精确计算，其中原始数据（例如来自传感器）是不精确的并且被提供有误差条。这些场景出现在例如网络物理系统、机器学习、机器人、汽车工程、航空航天和能源系统中。测量测量值与其真实值的接近程度自然会导致使用度量，但是，尽管取得了一些成功，但它们的使用受到许多缺点的影响，例如i）在一个问题域中定义的度量通常不会延续到其他问题域; ii）基于系统结构的度量通常不反映行为相似性，反之亦然;以及iii）系统结构的越来越精确的模型并不能保证具有越来越精确的行为。我们推测这些问题是更深层次问题的表现，即所有支持计算的数学都将精确相等作为原始，所以近似是建立在精确的元理论之上的。然而，在最近的一项突破中，Mardare和他的合作者引入了量化代数（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.