Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Jürgen Giesl
TL;DR
The paper tackles automatic analysis of almost-sure termination for probabilistic term rewriting (PTRS) under full rewriting, extending prior work that handled only innermost AST. It introduces annotating dependency pairs (ADPs) for full rewriting and augments the framework with variable repositioning to preserve necessary annotations during non-innermost steps, enabling AST proofs for overlapping and non-left-linear PTRSs. A key contribution is a chain-criterion-based ADP framework that remains sound and complete under probabilistic semantics, along with basic-start-term specialization (bAST) and spareness concepts to widen applicability. The approach leverages modular processors—dependence graphs, usable rules, reduction pairs (multilinear polynomial interpretations), and reachability techniques—extending the DP framework to the probabilistic setting and demonstrating practicality via integration into AProVE with a benchmark suite including lists and trees. The results show automatic AST proofs for PTRSs that previous methods could not handle, highlighting improved automation for probabilistic programs with complex data structures and non-deterministic behavior.
Abstract
Dependency pairs (DPs) are one of the most powerful techniques for automated termination analysis of term rewrite systems. Recently, we adapted the DP framework to the probabilistic setting to prove almost-sure termination (AST) via annotated DPs (ADPs). However, this adaption only handled AST w.r.t. the innermost evaluation strategy. In this paper, we improve the ADP framework to prove AST for full rewriting. Moreover, we refine the framework for rewrite sequences that start with basic terms containing a single defined function symbol. We implemented and evaluated the new framework in our tool AProVE.