Quantitative Equational Logic

We develop a quantitative analogue of equational reasoning, which we call quantitative equational logic. The quantitative equations use, instead of classical equality, quantitative equalities, which are equalities indexed with nonnegative reals. Thus, s = εt means that “s and t are points in a metric space and their distance is less than ε”. Quantitative equalities will be used to encode behavioural distances, with ε being an upper bound on the measure of dissimilarity between two terms. We develop the metatheory of this subject. We define a notion of quantitative algebra, which is the quantitative analogue of universal algebra. We prove a completeness theorem for quantitative equational logic, and we show that we obtain monads on suitable categories of metric spaces. We present a set of examples where the free algebra of a quantitative equational theory corresponds to some well-known structure. These examples are: Hausdorff metrics from quantitative semilattices; p-Wasserstein metrics (hence also the Kantorovich metric), and the total variation metric.