PTRS Standard

The PTRS Standard category is concerned with the question "Will every rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the termination workshop 2023.

Category Motivation

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.

Many algorithms can be made more robust by introducing probabilistic choices. For example, in probabilistic quicksort the pivot element is chosen uniformly at random. This variant is more robust than the standard quicksort algorithm because it achieves an expected runtime of O(n * log(⁡n)) for every input and avoids the deterministic worst-case runtime of O(n²). However, when probabilities are introduced, programmers often quickly lose intuition about expected runtime and termination. Therefore, automatic techniques for proving termination and establishing upper bounds on the expected runtime are needed.

Syntax & Semantic

The syntax and the semantics of term rewrite systems are described here including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST). Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool. However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST. In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

Formally, a probabilistic term rewrite system R = {l₁ → r₁,...,l_n → r_n} is a finite set of probabilistic rewrite rules, see [1].

Problem

Input: A probabilistic term rewrite system R.

Question: Is R AST or SAST?

Possible Outputs:

• "AST" followed by a termination proof, e.g., a ranking function proving almost-sure termination (AST) of R.
• "SAST" followed by a termination proof, e.g., a ranking function proving strong almost-sure termination (SAST) of R.
• "MAYBE" (indicating that the solver can neither prove AST nor SAST termination).

References

• [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
• [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.