Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Correspondences between codensity and coupling-based liftings, a practical approach

Samuel Humeau, Daniela Petrisan, Jurriaan Rot

TL;DR

The paper addresses generalising Kantorovich–Rubinstein dualities beyond distributions to arbitrary endofunctors on Set by comparing coupling-based liftings with codensity liftings in 𝔙-PMet. It develops a compositional, modality-driven approach showing correspondences are closed under coproducts and products, and provides explicit constructions for polynomial functors, including DFA and other automata-like systems, via a grammar of functors built from constants, identities, products, coproducts, powerset, and distribution. It also derives dualities for the powerset and distribution functors and demonstrates a counterexample (CTS) where a codensity lifting cannot be captured by a coupling-based lifting, delineating the limits of the framework. Collectively, these results yield a practical, modular toolkit to obtain and reason about behavioral metrics in a wide range of coalgebraic systems, with explicit modalities per component to achieve correspondences and, in some cases, dualities. The work thus unifies two prominent lifting notions into a constructive, scalable theory for quantitative coalgebraic semantics, with direct implications for systems like streams, DFA, labeled Markov processes, and automata metrics.

Abstract

The Kantorovich distance is a widely used metric between probability distributions. The Kantorovich-Rubinstein duality states that it can be defined in two equivalent ways: as a supremum, based on non-expansive functions into [0, 1], and as an infimum, based on probabilistic couplings. Orthogonally, there are categorical generalisations of both presentations proposed in the literature, in the form of codensity liftings and what we refer to as coupling-based liftings. Both lift endofunctors on the category Set of sets and functions to that of pseudometric spaces, and both are parameterised by modalities from coalgebraic modal logic. A generalisation of the Kantorovich-Rubinstein duality has been more nebulous-it is known not to work in some cases. In this paper we propose a compositional approach for obtaining such generalised dualities for a class of functors, which is closed under coproducts and products. Our approach is based on an explicit construction of modalities and also applies to and extends known cases such as that of the powerset functor.

Correspondences between codensity and coupling-based liftings, a practical approach

TL;DR

The paper addresses generalising Kantorovich–Rubinstein dualities beyond distributions to arbitrary endofunctors on Set by comparing coupling-based liftings with codensity liftings in 𝔙-PMet. It develops a compositional, modality-driven approach showing correspondences are closed under coproducts and products, and provides explicit constructions for polynomial functors, including DFA and other automata-like systems, via a grammar of functors built from constants, identities, products, coproducts, powerset, and distribution. It also derives dualities for the powerset and distribution functors and demonstrates a counterexample (CTS) where a codensity lifting cannot be captured by a coupling-based lifting, delineating the limits of the framework. Collectively, these results yield a practical, modular toolkit to obtain and reason about behavioral metrics in a wide range of coalgebraic systems, with explicit modalities per component to achieve correspondences and, in some cases, dualities. The work thus unifies two prominent lifting notions into a constructive, scalable theory for quantitative coalgebraic semantics, with direct implications for systems like streams, DFA, labeled Markov processes, and automata metrics.

Abstract

The Kantorovich distance is a widely used metric between probability distributions. The Kantorovich-Rubinstein duality states that it can be defined in two equivalent ways: as a supremum, based on non-expansive functions into [0, 1], and as an infimum, based on probabilistic couplings. Orthogonally, there are categorical generalisations of both presentations proposed in the literature, in the form of codensity liftings and what we refer to as coupling-based liftings. Both lift endofunctors on the category Set of sets and functions to that of pseudometric spaces, and both are parameterised by modalities from coalgebraic modal logic. A generalisation of the Kantorovich-Rubinstein duality has been more nebulous-it is known not to work in some cases. In this paper we propose a compositional approach for obtaining such generalised dualities for a class of functors, which is closed under coproducts and products. Our approach is based on an explicit construction of modalities and also applies to and extends known cases such as that of the powerset functor.

Paper Structure

This paper contains 16 sections, 5 theorems, 29 equations.

Table of Contents

  1. Introduction
  2. Codensity and coupling-based liftings: correspondences by example
  3. Preliminaries: "quantales" and "pseudometrics"
  4. "Liftings", "dualities", and "correspondences"
  5. "Well-behaved" "modalities"
  6. "Liftings" and "correspondences"
  7. "Kantorovich-Rubinstein dualities" and tools to get them
  8. "Correspondences" through coproducts and products
  9. Coproduct functors
  10. Product functors
  11. [constant]Constant and "identity functors"
  12. Putting it together: "correspondences" for polynomial functors
  13. "Dualities" for the "powerset" and "probability distribution functors"
  14. "Correspondences" for grammars of functors
  15. A counter-example: "conditional transition systems"
  16. ...and 1 more sections

Key Result

Proposition 16

The triple $\kl[correspondence]{\left(\text{\normalfont1},"\tau",\Gamma\right)}$ with the functor $\text{\normalfont1}$ sending any set to a fixed singleton is a "correspondence" if and only if $\Gamma=\{"\tau"\}$ and $"\tau"$ is the constant to $\top$ "modality".

Theorems & Definitions (27)

  • Definition 1
  • Example 2
  • Definition 3
  • Example 4
  • Remark 5
  • Definition 6
  • Example 7
  • Example 8
  • Definition 9
  • Example 10
  • ...and 17 more