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

TL;DR

This paper develops a higher-order quantitative logic with induction and recursion principles for probabilistic reasoning, enabling formal analysis of probabilistic programs and processes.

Contribution

It introduces a new affine higher-order logic with guarded recursion and induction principles tailored for probabilistic reasoning and metric spaces.

Findings

Proved upper bounds on bisimilarity distances of Markov processes

Demonstrated convergence of a temporal learning algorithm

Analyzed random walk convergence using coupling arguments

Abstract

Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes. We construct an affine calculus for $1$-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach's fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion, and induction over probability measures and natural numbers. We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.