EPSRC Reference: 
EP/Y000455/1 
Title: 
A correctbyconstruction approach to approximate computation 
Principal Investigator: 
Mardare, Professor R 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer and Information Sciences 
Organisation: 
University of Strathclyde 
Scheme: 
Standard Research 
Starts: 
01 November 2023 
Ends: 
31 October 2027 
Value (£): 
692,875

EPSRC Research Topic Classifications: 
Fundamentals of Computing 
Logic & Combinatorics 

EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
03 Jul 2023

EPSRC ICT Prioritisation Panel July 2023

Announced


Summary on Grant Application Form 
Correctbyconstruction 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 correctbyconstruction 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) nonexact computation where primitive data (e.g. from sensors) is inexact and supplied with error bars. These scenarios arise in e.g. cyberphysical 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 viceversa; 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 metatheory. 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 equalityuptoapproximation 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 cocreated 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.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.strath.ac.uk 