Quantitative Algebraic Reasoning
summary
Defines a quantitative equational logic where equations are s =ε t (distance ε) and replaces congruence by nonexpansiveness, builds term pseudometrics and quotients to get free quantitative algebras, and proves universal mapping theorems that yield monads on Set, Met (metric spaces) and on complete separable (Polish) spaces. Shows finitely supported probability measures complete to all measures and identifies total variation distance and the p‑Wasserstein metric (and Hausdorff on closed sets) as canonical instances via isomorphism/completion theorems; some duality and unbounded‑metric extensions remain open.
AI-written summary · about
chapters (19)
- 0:00Intro
- 3:34Historical Perspective
- 6:28An Example
- 9:36Quantitative Equational Theory
- 11:48Quantitative Deductibility Relation
- 13:12Quantitative Equational Theories
- 13:52Quantitative Algebra
- 14:26Algebraic Semantics
- 16:32Term Algebra
- 18:04Generated Model -- from a Set
- 20:24Universality
- 21:17Left-invariant Barycentrie Algebra
- 23:56Generated Model - from a Metric Space
- 26:20Generated Models - from Complete Metric Spaces
- 29:59Interpolative Barycentric Algebra: Finitary Case
- 31:47Interpolative Barycentric Algebra: Continuous Case
- 36:09Example 3: Quantitative Semilattices with Zero
- 37:30Quantitative Semilattices with Zero: Continuous Case
- 39:03Related work
related talks
22mReasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence
01h 03mInside Every Calculus Is A Little Algebra Waiting To Get Out
14mA Unifying Approach to Product Constructions for Quantitative Temporal Inference
13mFormalizing a First-order Differentiable Logic with MathComp
01h 52mIsomorphic Reasoning: Counting with Types Part 3
52mPrinciples of Mathematical Thinking
20mWhat do posterior distributions of probabilistic programs look like?
01h 39mIsomorphic Reasoning: Counting with Types Part 1