糖心TV

Prakash Panangaden
McGill University, CA and the Alan Turing Institute

Quantitative equational reasoning and its applications

Abstract:
Reasoning with equations is a central part of mathematics. Typically we
think of solving equations but another role they play is to define
algebraic structures like groups or vector spaces. Equational logic was
formalized and developed by Birkhoff in the 1930s and led to a subject
called universal algebra. Universal algebra was used in formalizing
concepts of data types in computer science. In this talk I will present a
quantitative analogue of equational logic. It turns out that
the metatheory of equational logic can be redeveloped in this
setting.

What could perhaps be considered sterile theory comes alive are some
striking examples. A notion of distance between probability distributions
called the Kantorovich metric (frequently called the Wasserstein metric)
has become important in the theory of probabilistic systems and in parts of
machine learning. It turns out that this metric emerges naturally as the
"free algebra" of some simple equational axioms in our extended sense.

This is joint work with Radu Mardare and Gordon Plotkin. Prakash is a
distinguished researcher in semantics and logics for
probabilistic systems and languages, machine learning and
quantum information theory. He is the founding Chair of the ACM
Special Interest Group on Logic and Computation.