PTRS Innermost

The PTRS Standard category is concerned with the question "Will every innermost 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 innermost 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. It restricts the analysis of probabilistic algorithms to a call-by-value evaluation strategy, which is one of the most used evaluation strategies in probabilistic programming languages.

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].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.

Problem

Input: A probabilistic term rewrite system R.

Question: Is R innermost AST or innermost SAST?

Possible Outputs:

• "iAST" followed by a termination proof, e.g., a ranking function proving innermost almost-sure termination (iAST) of R.
• "iSAST" followed by a termination proof, e.g., a ranking function proving innermost strong almost-sure termination (iSAST) of R.
• "MAYBE" (indicating that the solver can neither prove iAST nor iSAST 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.