Quantitative Equational Logic and the Kantorovich Metric

Quantitative equational logic is an extension of ordinary equational logic where one allows the equality symbol to be annotated by a (small) real number; one can write "equations" of the form s =_e t where s and t are terms and e is a real number.  The intended interpretation is that "s is within e of t".  I will briefly sketch the rules of inference and the general theory, but I will spend most of my time discussing a particular example.  This is the example of probability distributions on a metric space and how a simple set of quantitative equations axiomatizes the Kantorovich-Wasserstein metric.  

This is joint work with Gordon Plotkin, who came up with the idea, and Radu Mardare.  Radu will discuss the theory in his upcoming talk at the Uncertainty Workshop.