A formal context for metric semantics

Add to your list(s) Download to your calendar using vCal

• Radu Mardare, University of Strathclyde
• Friday 05 November 2021, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Jamie Vicary.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.