From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Florian Frohn, Jürgen Giesl
TL;DR
The paper addresses when innermost almost-sure termination ($iAST$) implies full almost-sure termination ($fAST$) for probabilistic term rewriting systems, and extends the dependency-pair framework to the probabilistic setting. It develops automatic, sufficient criteria that relate $iAST$ to $fAST$ (and analogues for PA$ST$ and SAST), and introduces concepts such as simultaneous rewriting and sparseness to relax left-/right-linearity assumptions, enabling modular, automated proofs. The authors implement these criteria in AProVE and evaluate them on FLOPS benchmarks, showing substantial automation: AProVE can prove $iAST$ for many PTRSs and, in favorable cases, deduce $fAST$ for basic terms or all terms. Overall, the work provides a principled, automated pathway to certify full termination properties for PTRSs by leveraging restricted, automatable variants of AST and extending existing DP-based techniques to the probabilistic realm.
Abstract
There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems (PTRSs). These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE.