Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Almost-Sure Termination by Guarded Refinement

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

TL;DR

This paper proposes an approach based on proving refinement between a higher-order program and a simpler probabilistic model, in such a way that the refinement preserves termination behavior, and presents Caliper, a higher-order separation logic for proving terminationpreserving refinements.

Abstract

Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logics have mostly been developed for first-order programs written in languages with specific syntactic patterns for looping. In this paper, we consider almost-sure termination for higher-order probabilistic programs with general references. This combination of features allows for recursion and looping to be encoded through a variety of patterns. Therefore, rather than developing proof rules for reasoning about particular recursion patterns, we instead propose an approach based on proving refinement between a higher-order program and a simpler probabilistic model, in such a way that the refinement preserves termination behavior. By proving a refinement, almost-sure termination behavior of the program can then be established by analyzing the simpler model. We present this approach in the form of Caliper, a higher-order separation logic for proving termination-preserving refinements. Caliper uses probabilistic couplings to carry out relational reasoning between a program and a model. To handle the range of recursion patterns found in higher-order programs, Caliper uses guarded recursion, in particular the principle of Löb induction. A technical novelty is that Caliper does not require the use of transfinite step indexing or other technical restrictions found in prior work on guarded recursion for termination-preservation refinement. We demonstrate the flexibility of this approach by proving almost-sure termination of several examples, including first-order loop constructs, a random list generator, treaps, and a sampler for Galton-Watson trees that uses higher-order store. All the results have been mechanized in the Coq proof assistant.

Almost-Sure Termination by Guarded Refinement

TL;DR

This paper proposes an approach based on proving refinement between a higher-order program and a simpler probabilistic model, in such a way that the refinement preserves termination behavior, and presents Caliper, a higher-order separation logic for proving terminationpreserving refinements.

Abstract

Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logics have mostly been developed for first-order programs written in languages with specific syntactic patterns for looping. In this paper, we consider almost-sure termination for higher-order probabilistic programs with general references. This combination of features allows for recursion and looping to be encoded through a variety of patterns. Therefore, rather than developing proof rules for reasoning about particular recursion patterns, we instead propose an approach based on proving refinement between a higher-order program and a simpler probabilistic model, in such a way that the refinement preserves termination behavior. By proving a refinement, almost-sure termination behavior of the program can then be established by analyzing the simpler model. We present this approach in the form of Caliper, a higher-order separation logic for proving termination-preserving refinements. Caliper uses probabilistic couplings to carry out relational reasoning between a program and a model. To handle the range of recursion patterns found in higher-order programs, Caliper uses guarded recursion, in particular the principle of Löb induction. A technical novelty is that Caliper does not require the use of transfinite step indexing or other technical restrictions found in prior work on guarded recursion for termination-preservation refinement. We demonstrate the flexibility of this approach by proving almost-sure termination of several examples, including first-order loop constructs, a random list generator, treaps, and a sampler for Galton-Watson trees that uses higher-order store. All the results have been mechanized in the Coq proof assistant.
Paper Structure (8 sections, 5 theorems, 6 equations)

This paper contains 8 sections, 5 theorems, 6 equations.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Background and Preliminaries
  4. Probabilistic Semantics
  5. ProbLang.
  6. Probabilistic Couplings
  7. A Probabilistic Termination-Preserving Refinement Logic
  8. Separation Logic Connectives and Basic Unary Rules

Key Result

Lemma 2.3

Let $\mu \in \mathcal{D}(A)$, $a \in A$, and $f : A \to \mathcal{D}(B)$. Then gives monadic structure to $\mathcal{D}$. We write $\mu \mathbin{ \raisebox{0.3ex}{$\gg\mkern-6mu=$} } f$ for $\mathop{\mathrm{bind}}\nolimits(f, \mu)$.

Theorems & Definitions (9)

  • Definition 2.1
  • Definition 2.2
  • Lemma 2.3
  • Definition 2.4
  • Lemma 2.5
  • Definition 2.6: Left-partial coupling clutch
  • Lemma 2.7
  • Lemma 2.8
  • Theorem 3.1: Soundness