Advancing the Theory of Quantitative Universal Algebra

• Applicants: Professor Dr. Stefan Milius; Dr. Henning Urbat
• Subject Area: Theoretical Computer Science
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 569130867

Program equations, expressing behavioural equality between syntactically different programs, are ubiquitous in computer science. They are at the heart of program semantic definitions, transformations, optimizations, 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 influential work, 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 work, 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 / DFG project have both contributed, separately, with a number of technical advancements presented at top conferences. The main goal of this project is to advance the theory and applications of quantitative universal algebra towards a comprehensive body of results, constructions, and tools for the mechanizable deductive and algorithmic treatment of specifications with quantitative aspects. A particular emphasis will be directed to the specification of well-behaved programming languages with quantitative structure and to the development of efficient reasoning methods for upper and lower bounds for the distance of the behaviour of programs. Another key benefit of the project is to stimulate a sustained synergy between the two research groups at ENS Lyon and FAU. We expect that this will continue well beyond the duration of the project. Moreover, the systematic and close scientific collaboration of the two research groups during the course of the project will help the funded researchers (two postdocs at ENS Lyon and a doctoral researcher at FAU) to start building a scientific network and international contacts and collaborations.

• DFG Programme: Research Grants
• International Connection: France
• Cooperation Partner: Dr. Matteo Mio