Advancing the Theory of Quantitative Universal Algebra
Program equations, expressing behavioural equality between syntactically different programs, are ubiquitous in computer science. They are at the heart of program semantic definitions, transformations, optimisations, etc. The mathematical field of universal algebra (UA) constitutes a theoretical background for these topics. However, in many applications a more fine grained reasoning that allows to describe that two programs, while behaviourally different, have very similar behaviours is more desirable. Quantitative universal algebra (QUA), a generalization of UA recently proposed by Mardare, Panangaden and Plotkin in an influential LICS 2016 conference paper, provides the mathematical foundations for this reasoning via quantitative program equations. In QUA, informal similarity is captured quantitatively and numerically by the mathematical concept of metric distance. For example, one could take a program and start replacing some lines of code with different, but sufficiently near ones under an appropriate metric, and expect the final outcome to be sufficiently near to the original program in the metric. Quantitative algebraic methods also appear to be very promising in the context of AI or IoT. In these settings, it is desirable to expect reliable results even when inputs, parameters, sensor data, etc., could be affected by some small perturbations, e.g. due to noise. Since the initial LICS 2016 paper, QUA has received considerable attention and is now an active topic of research in theoretical computer science. The two research groups involved in this ANR PRCI have both contributed, separately, with a number of technical advancements presented at top conferences. The main goal of this ANR PRCI project is to stimulate a synergy between the two research groups and advance the theory and applications of quantitative universal algebra. Besides the activity of the permanent researchers, this will be enabled by postdocs and a PhD student funded by the grant.
3/6 complete
Imported from OpenAIRE Germany | Grant ANR-25-CE48-1428.
Open sourceOverview
Grant agreement ANR-25-CE48-1428 | ATQUA
Open sourceProgram equations, expressing behavioural equality between syntactically different programs, are ubiquitous in computer science. They are at the heart of program semantic definitions, transformations, optimisations, etc. The mathematical field of universal algebra (UA) constitutes a theoretical background for these topics. However, in many applications a more fine grained reasoning that allows to describe that two programs, while behaviourally different, have very similar behaviours is more desirable. Quantitative universal algebra (QUA), a generalization of UA recently proposed by Mardare, Panangaden and Plotkin in an influential LICS 2016 conference paper, provides the mathematical foundations for this reasoning via quantitative program equations. In QUA, informal similarity is captured quantitatively and numerically by the mathematical concept of metric distance. For example, one could take a program and start replacing some lines of code with different, but sufficiently near ones under an appropriate metric, and expect the final outcome to be sufficiently near to the original program in the metric. Quantitative algebraic methods also appear to be very promising in the context of AI or IoT. In these settings, it is desirable to expect reliable results even when inputs, parameters, sensor data, etc., could be affected by some small perturbations, e.g. due to noise. Since the initial LICS 2016 paper, QUA has received considerable attention and is now an active topic of research in theoretical computer science. The two research groups involved in this ANR PRCI have both contributed, separately, with a number of technical advancements presented at top conferences. The main goal of this ANR PRCI project is to stimulate a synergy between the two research groups and advance the theory and applications of quantitative universal algebra. Besides the activity of the permanent researchers, this will be enabled by postdocs and a PhD student funded by the grant.