一句话：提出 Caliper：用保持终止的高阶程序—概率模型精化，经守卫递归与 Löb 归纳证明几乎必然终止。
几乎必然终止是概率程序的重要正确性性质，但已有程序逻辑大多针对一阶程序及特定循环语法。本文研究带一般引用的高阶概率程序的几乎必然终止：这类语言中递归与循环可编码为多种形式，因此难以给出针对具体递归模式的证明规则。作者提出 Caliper，一种用于证明“保持终止的精化”的高阶分离逻辑：通过证明高阶程序与更简单概率模型之间的精化，将程序的几乎必然终止性归约为对模型的分析。Caliper 使用概率耦合进行程序与模型之间的关系推理，并用守卫递归特别是 Löb 归纳处理高阶程序中的各种递归模式。技术上不需要超限步索引或既有守卫递归工作里的其他限制。作者验证了一阶循环构造、随机链表生成器、treap 以及使用高阶存储的 Galton-Watson 树采样器等例子，所有结果均在 Coq 中机器化。
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 terminationpreserving 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Gregersen0HTB24,
title = {Almost-Sure Termination by Guarded Refinement},
author = {Simon Oddershede Gregersen and Alejandro Aguirre and Philipp G. Haselwarter and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674632}
}