PTRS Standard - Revision history

JCKassing: Add new Output Syntax for Competition

2026-10-28T15:56:25Z

Add new Output Syntax for Competition

← Older revision		Revision as of 15:56, 28 October 2026
Line 29:		Line 29:
	<b>Question</b>: Is R AST or SAST?		<b>Question</b>: Is R AST or 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:
	* "<b>~~AST~~</b>" followed by a ~~termination~~ proof, e.g., a ranking function ~~proving~~ almost-~~sure termination~~ (AST~~) of R~~.		* <i>g</i> ∈ {<b>?</b> < <b>AST</b> < <b>SAST</b>}: "<b>AST</b>" claims that R is almost-surely terminating (AST), e.g., proven by a ranking function. "<b>SAST</b>" claims that R is strongly almost-surely terminating (SAST), and thus also AST. "<b>?</b>" makes no claim.
	* "<b>SAST</b>" ~~followed by a termination proof, e.g~~., ~~a ranking function proving strong almost-sure termination (~~SAST~~) of R~~.		* <i>f</i> ∈ {<b>?</b> < <b>Non-SAST</b> < <b>Non-AST</b>}: "<b>Non-SAST</b>" claims that R is not SAST. "<b>Non-AST</b>" claims that R is not AST, and thus also not SAST. "<b>?</b>" makes no claim.
	* "<b>~~MAYBE~~</b>" ~~(indicating~~ that the solver can neither ~~prove~~ AST ~~nor~~ SAST ~~termination)~~.		* "<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 ==

JCKassing: Small fixes

2026-06-09T12:25:39Z

Small fixes

← Older revision		Revision as of 12:25, 9 June 2026
Line 1:		Line 1:
	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 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 have 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 [[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 19:		Line 19:
	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 ~~more than~~ 2 arguments).		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].

JCKassing: Added missing reference

2026-03-11T10:08:02Z

Added missing reference

← Older revision		Revision as of 10:08, 11 March 2026
Line 30:		Line 30:

	<b>Possible Outputs</b>:		<b>Possible Outputs</b>:
	* "<b>AST</b>" followed by a termination proof, e.g., a ranking function proving ~~outermost~~ termination of R.		* "<b>AST</b>" followed by a termination proof, e.g., a ranking function proving almost-sure termination (AST) of R.
	* "<b>SAST</b>" followed by a termination proof, e.g., a ranking function proving ~~outermost~~ termination of R.		* "<b>SAST</b>" followed by a termination proof, e.g., a ranking function proving strong almost-sure termination (SAST) of R.
	* "<b>MAYBE</b>" (indicating that the solver ~~cannot~~ prove ~~outermost~~ termination).		* "<b>MAYBE</b>" (indicating that the solver can neither prove AST nor SAST termination).

	== 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. Logical Methods in Computer Science, 2026.

	[[Category:Categories]]		[[Category:Categories]]

JCKassing: Added PTRS Standard category

2026-03-11T09:57:07Z

Added PTRS Standard category

New page

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 [[19th_International_Workshop_on_Termination | 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(n2).
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 [[Probabilistic_Rewriting | 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 = {l1 → r1,...,ln → rn} 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 outermost termination of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "MAYBE" (indicating that the solver cannot prove outermost termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.

[[Category:Categories]]