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.

翻译：概率量逻辑研究公式被满足的程度。本文研究高阶概率量逻辑的基本推理原理及其在概率程序与过程推理中的应用。我们为$1$边界完备度量空间和装备康德罗维奇距离的概率测度单子构造了一个仿射演算。该演算包含一种通过巴拿赫不动点定理解释的守护递归形式，这对过程递归编程尤为有用。随后我们定义了一个仿射高阶概率量逻辑，用于推理该演算中的项。该逻辑包含守护递归的新颖原理，以及关于概率测度和自然数的归纳原理。通过一系列案例研究，我们展示了该逻辑的表达能力：证明马尔可夫过程互模拟距离的上界，利用耦合论证展示时序学习算法和随机游走的收敛性。