PTRS Innermost: Difference between revisions
Added PTRS Innermost category |
Add new Output Syntax for Competition |
||
| (2 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
The PTRS | The PTRS Innermost category is concerned with the question "Will every <i>innermost</i> rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t have a finite upper bound on the expected runtime of all <i>innermost</i> 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 [[19th_International_Workshop_on_Termination | termination workshop 2023]]. | The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]]. | ||
| Line 13: | Line 13: | ||
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool. | 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. | 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 | 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 at least 2 arguments). | ||
Formally, a probabilistic term rewrite system R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} is a finite set of probabilistic rewrite rules, see [1]. | Formally, a probabilistic term rewrite system R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} is a finite set of probabilistic rewrite rules, see [1]. | ||
| Line 25: | Line 25: | ||
<b>Question</b>: Is R innermost AST or innermost SAST? | <b>Question</b>: Is R innermost AST or innermost SAST? | ||
<b>Possible Outputs</b>: | <b>Possible Outputs</b>: The first line of the output must be "<b>WORST_CASE(</b><i>f</i><b>,</b><i>g</i><b>)</b>", followed by a proof of the claimed bounds. Here <i>f</i> is a lower bound and <i>g</i> is an upper bound: | ||
* <i>g</i> ∈ {<b>?</b> < <b>AST</b> < <b>SAST</b>}: "<b>AST</b>" claims that R is innermost almost-surely terminating (iAST), e.g., proven by a ranking function. "<b>SAST</b>" claims that R is innermost strongly almost-surely terminating (iSAST), and thus also iAST. "<b>?</b>" makes no claim. | |||
* "<b>iSAST</b>" | * <i>f</i> ∈ {<b>?</b> < <b>Non-SAST</b> < <b>Non-AST</b>}: "<b>Non-SAST</b>" claims that R is not iSAST. "<b>Non-AST</b>" claims that R is not iAST, and thus also not iSAST. "<b>?</b>" makes no claim. | ||
* "<b> | * "<b>WORST_CASE(?,?)</b>" means that the solver can prove neither bound. | ||
The conflicting answers are <b>Non-SAST</b> with <b>SAST</b>, <b>Non-AST</b> with <b>SAST</b>, and <b>Non-AST</b> with <b>AST</b>. | |||
== References == | == References == | ||
* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. <i>Science of Computer Programming</i>, 2020. | * [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. <i>Science of Computer Programming</i>, 2020. | ||
* [ | * [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. <i>Logical Methods in Computer Science</i>, 2026. | ||
[[Category:Categories]] | [[Category:Categories]] | ||
Latest revision as of 15:55, 28 October 2026
The PTRS Innermost 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 have 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 at least 2 arguments).
Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} 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: The first line of the output must be "WORST_CASE(f,g)", followed by a proof of the claimed bounds. Here f is a lower bound and g is an upper bound:
- g ∈ {? < AST < SAST}: "AST" claims that R is innermost almost-surely terminating (iAST), e.g., proven by a ranking function. "SAST" claims that R is innermost strongly almost-surely terminating (iSAST), and thus also iAST. "?" makes no claim.
- f ∈ {? < Non-SAST < Non-AST}: "Non-SAST" claims that R is not iSAST. "Non-AST" claims that R is not iAST, and thus also not iSAST. "?" makes no claim.
- "WORST_CASE(?,?)" means that the solver can prove neither bound.
The conflicting answers are Non-SAST with SAST, Non-AST with SAST, and Non-AST with AST.
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.