Abstract

In the last decades the research in most of the fields in computer science, from programming paradigms to cyber-physical systems and from robotics to learning, has been challenged to integrate various concepts of continuous mathematics into semantics. This is because the interaction of computational systems with the real world brought real-valued parameters in computation (rates, probabilities, differential equations, time, resources, etc). And in this context, the classic semantics centred on concepts of congruence (bisimulation, behavioural equivalence) became inadequate. We are not interested anymore in understanding systems or their behaviours up to identity, but we need instead to work with approximations of systems and of their behaviours, which scale properly in the structure of a computational system and allow us to understand approximated computation.

To answer this challenge, we have introduced quantitative equational reasoning, an algebraic theory that generalizes universal algebras by extending the classic concept of equation of type s=t to equations of type s=_e t for some positive e, interpreted as an upper bound of the distance between the interpretations of the terms s and t. In this way, instead of axiomatizing congruences, we axiomatize algebraic structures on metric spaces. This provides the concepts we need to develop a metric semantics for systems where the similarity between non-equivalent systems can be properly measured and approximated.

This talk is a tutorial on quantitative equational reasoning and quantitative algebras. I plan to summarize a series of results that we have published in the last five years, joint work with Prakash Panangaden and Gordon Plotkin.