🔢 mathematics

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability

This paper introduces an affine higher-order quantitative logic equipped with novel induction and guarded recursion principles for $1$-bounded complete metric spaces and probability measures, demonstrating its utility in verifying probabilistic programs and processes through case studies on bisimilarity distances, temporal learning convergence, and random walks.

Original authors: Giorgio Bacci, Rasmus Ejlers Møgelberg

Published 2026-05-21

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Giorgio Bacci, Rasmus Ejlers Møgelberg

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to judge how similar two things are. In the old days of computer science, logic was like a strict judge who only cared about "Yes" or "No." Two programs were either exactly the same, or they were completely different. There was no middle ground.

But in the modern world of probabilistic programming (where computers make random choices, like rolling dice), things aren't so black and white. Sometimes Program A is almost the same as Program B, or maybe it's only slightly different. This paper introduces a new kind of "logic" that can measure these shades of gray.

Here is a breakdown of the paper's ideas using simple analogies:

1. The World of "Fuzzy" Equality (Metric Spaces)

Think of a standard computer program as a point on a map. In traditional logic, if you have two points, they are either the same spot or they aren't.

In this paper, the authors treat programs like points on a rubber sheet.

Distance: The "distance" between two points isn't just physical space; it's a measure of how different their behavior is. If two programs behave almost the same, they are close together on the sheet. If they behave very differently, they are far apart.
The Goal: Instead of asking "Are they equal?", the logic asks, "How far apart are they?" and tries to prove that the distance is small enough to be acceptable.

2. The "Sensitivity" Tag (The Affine Calculus)

Imagine you are a chef following a recipe. Some ingredients are very sensitive: if you change the amount of salt by a tiny bit, the whole dish tastes ruined. Other ingredients are robust: adding a little more water doesn't change much.

The authors created a programming language (a "calculus") where every variable comes with a sensitivity tag.

If a variable is tagged with a high sensitivity, the logic knows that small changes in that input will cause big changes in the output.
If it's tagged with low sensitivity, the output is stable.
Why it matters: This allows the computer to mathematically track how errors or random choices ripple through a program. It's like having a built-in "error meter" that tells you exactly how much a mistake in the input will mess up the result.

3. The "Safe Loop" (Guarded Recursion)

Usually, when you write a computer program that repeats itself (a loop or recursion), it can get stuck in an infinite loop that never finishes.

The authors use a concept called Banach's Fixed Point Theorem (a famous math rule) to create a "safe loop."

The Analogy: Imagine a mirror reflecting a mirror. If the mirrors are perfectly parallel, you see an infinite tunnel. But if you angle them slightly so that the image gets smaller and smaller with every reflection, the image eventually shrinks to a single point and stops.
The Logic: The authors ensure that every time their program loops, it "shrinks" the problem slightly (by a factor less than 1). This guarantees the loop will eventually finish and settle on a single, stable answer. This is crucial for defining things like "geometric distributions" (randomly picking numbers) or simulating processes that run forever but settle into a pattern.

4. The "Coupling" Trick (Induction and Probability)

One of the hardest things to prove in probability is that two random processes are similar.

The Problem: You can't just compare the final results of two dice rolls because they are random.
The Solution (Coupling): The paper introduces a principle called Coupling. Imagine you have two people rolling dice. Instead of rolling them separately, you force them to roll the same dice at the same time. If you can show that, under this "shared" scenario, their results are always close, then you know the two processes are close, even if they usually roll separately.
The paper provides a logical rule that lets you prove things about probability distributions by "coupling" them together in your proof.

5. What They Actually Did (Case Studies)

The paper doesn't just talk theory; they used their new logic to solve three specific puzzles:

Markov Processes: They proved upper limits on how different two "random walk" systems (like a drunk person wandering a city) can be.
Learning Algorithms: They showed that a specific type of machine learning algorithm (Temporal Difference learning) actually converges to a stable answer, rather than going crazy.
Random Walks on a Hypercube: They used the "coupling" trick to prove that a random walker on a multi-dimensional cube (a complex shape) will eventually reach a state of balance.

Summary

This paper builds a new mathematical toolkit for reasoning about computer programs that involve randomness and uncertainty.

It replaces "Yes/No" with "How far apart?"
It tags variables with "sensitivity" to track how errors spread.
It uses "shrinking loops" to ensure programs don't get stuck.
It uses "shared scenarios" (coupling) to prove that random processes behave similarly.

The result is a system that can rigorously prove that probabilistic programs are safe, stable, and behave as expected, even when they involve complex random choices.

Technical Summary: Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability

Problem Statement

Traditional program logics are designed for qualitative properties, such as exact program equality or termination. However, modern applications in probabilistic programming, differential privacy, security, and machine learning require reasoning about quantitative properties. These include upper bounds on program distances, sensitivity of outputs to inputs, and the convergence of sequences of programs. While specific logics exist for these domains (e.g., Fuzz for differential privacy), there has been a lack of a general notion of quantitative logic capable of expressing these diverse applications as special cases. Specifically, there is a need for a framework that unifies reasoning about metric spaces, probability distributions, and guarded recursion within a higher-order setting.

Methodology

The authors develop a foundational framework consisting of a programming calculus and a corresponding higher-order logic, both grounded in the category of 1-bounded complete metric spaces (CMet).

1. The Calculus: An Affine Lambda Calculus for CMet

The authors construct an affine $\lambda$ -calculus designed for programming in CMet. Key features include:

Sensitivity Annotations: The calculus tracks the Lipschitz constant (sensitivity) of variables. A typing context $\Gamma$ assigns sensitivity factors $r \in [0, \infty]$ to variables, indicating how much a term's output distance depends on the input distance.
Monoidal Structure: It utilizes the tensor product $\otimes$ (1-bounded truncated sum of distances) rather than the categorical product, allowing for currying and function application while respecting non-expansiveness.
Probability Monad: The calculus includes the Radon probability monad $D$ , mapping a metric space $X$ to the space of Radon probability measures $DX$ equipped with the Kantorovich metric.
Guarded Recursion: General recursion is not supported in metric spaces, but guarded recursion is modeled via the Banach Fixed Point Theorem. A term $fix\ x.t$ is well-typed if the recursive call occurs with a sensitivity factor $p < 1$ , ensuring the function is a contraction and thus has a unique fixed point.
Affine Logic: The calculus is affine (weakening is allowed, but contraction is not), reflecting the nature of metric spaces where duplicating a variable does not necessarily preserve distance properties without scaling.

2. The Logic: Higher-Order Quantitative Logic

The authors define a higher-order logic for reasoning about terms in the calculus.

Quantale Semantics: Propositions are valued in the unit interval $[0, 1]$ , where $0$ represents "true" and $1$ represents "false." The logic is interpreted over the commutative unital quantale $([0, 1], \ge, \oplus, \multimap, 0)$ , where $\oplus$ is truncated addition and $\multimap$ is truncated subtraction.
Equality as Distance: The equality predicate $t =_A u$ is interpreted as the metric distance $d_A(t, u)$ .
Novel Inference Rules:
- Guarded Recursion: A rule allowing the derivation of $\phi$ from $(1-p)\Psi, p\phi \vdash \phi$ (for $p < 1$ ), mirroring the fixed-point combinator.
- Induction over Natural Numbers: Standard induction adapted for the quantitative setting.
- Induction over Probability Measures: A novel principle stating that a property holds for all distributions if it holds for Dirac distributions and is preserved under convex combinations ( $\oplus_p$ ). This relies on the density of finitely supported distributions in the space of Radon measures.
- Equality Elimination: A rule incorporating sensitivity: if $x$ has sensitivity $r$ in $\phi$ , then $\phi[t/x], r(t=s) \vdash \phi[s/x]$ . This allows reasoning about how small changes in inputs affect predicates.

3. Internalization of the Kantorovich Distance

A significant technical achievement is the internalization of the Kantorovich distance within the logic. The authors define an equality-coupling and prove that two distributions are equal (distance 0) if and only if there exists a coupling between them that minimizes the expected distance. This allows the logic to reason about probabilistic couplings directly.

Key Contributions

Affine Calculus for CMet: A simply-typed $\lambda$ -calculus with sensitivity annotations for programming in the category of 1-bounded complete metric spaces, featuring a strong monad for probability measures and guarded recursion.
Higher-Order Quantitative Logic: The first (to the authors' knowledge) higher-order logic where equality is interpreted as metric distance. It includes new rules for induction over probability measures and guarded recursion.
Induction Principles: The formulation of an induction principle for the Radon monad $D$ , which enables reasoning about continuous distributions by leveraging the density of finite distributions and the continuity of predicates.
Coupling as a Logical Principle: The demonstration that the logic can internalize the Kantorovich distance, enabling "coupling proofs" to be conducted as logical derivations.

Results and Case Studies

The paper validates the expressivity of the logic through three case studies:

Markov Processes: The authors model Markov processes as coalgebras in CMet. They use the guarded recursion principle to define recursive processes and prove upper bounds on bisimilarity distances. They show that the internal bisimilarity relation is equivalent to equality in the final coalgebra when the discount factor $c < 1$ .
Temporal Learning: A temporal difference learning algorithm is modeled. The authors use natural number induction to prove the convergence of the value function refinement, demonstrating the logic's ability to handle iterative algorithms with probabilistic updates.
Random Walk on a Hypercube: The authors prove the convergence of a random walk on a hypercube. This case study specifically utilizes the coupling argument internalized in the logic. By constructing a specific coupling between two walks starting at different positions, they prove a bound on the distance between the resulting distributions, illustrating the power of the induction principle for distributions and the equality elimination rule.

Significance and Claims

The paper claims that the combination of affine logic, sensitivity annotations, guarded recursion, and induction over probability measures provides a powerful, unified foundation for quantitative reasoning.

Unification: It bridges the gap between metric space theory, probabilistic programming, and higher-order logic.
Natural Reasoning: The authors argue that standard concepts like coupling and bisimulation can be read and reasoned about "very naturally" within this logic, often reducing complex metric proofs to logical derivations.
Robustness: By treating equality as distance, the logic inherently handles small perturbations, making it suitable for applications like differential privacy and security where exact equality is too rigid.

The authors acknowledge limitations, such as the restriction to 1-bounded metric spaces (to ensure the Banach fixed point theorem holds) and the external quantification required for certain parameters (like the dimension of a hypercube) due to the lack of dependent types. They suggest that extending the framework to extended metric spaces or incorporating dependent types are directions for future work.