Probabilistic Rewriting - Revision history

JCKassing: Removed Categories from this page

2026-03-11T10:05:58Z

Removed Categories from this page

JCKassing: Added to the category group

2026-01-15T12:36:09Z

Added to the category group

JCKassing: some additional information on the probabilistic rewriting site

2026-01-15T11:19:07Z

some additional information on the probabilistic rewriting site

JCKassing at 13:17, 13 May 2024

2024-05-13T13:17:02Z

JCKassing: JCKassing moved page Prob Rewriting to Probabilistic Rewriting: Change of title

2024-05-13T08:14:37Z

JCKassing moved page Prob Rewriting to Probabilistic Rewriting: Change of title

JCKassing at 10:15, 10 May 2024

2024-05-10T10:15:44Z

JCKassing: Created page with "== General == As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented..."

2024-05-10T10:14:53Z

Created page with "== General == As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented..."

New page

== General ==

As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). The format of TRSs is explained [[Term Rewriting|here]]. To extend this format with probabilistic rules, we extend the reserved words by <pre>prule, prob</pre>. Furthermore, probabilistic rules are defined as follows:
<pre>
prule ::= ( prule term dist cost? )
cost ::= :cost number
dist ::= ( ( term prob? )* )
prob ::= :prob number
</pre>

The goal of the analysis is implicitly specified by the category.

== Probabilistic Termination ==

All probabilistic termination categories consider termination w.r.t. arbitrary start terms.

=== PTRS Standard ===

* full rewriting
The tools can give the following answers:

<pre>MAYBE, AST, PAST, SAST</pre>

=== PTRS Innermost ===

* innermost rewriting
The tools can give the following answers:

<pre>MAYBE, AST, PAST, SAST</pre>

← Older revision		Revision as of 10:05, 11 March 2026
Line 66:		Line 66:

	Example: Again only P1 is PAST, but P2 and P3 are not PAST.		Example: Again only P1 is PAST, but P2 and P3 are not PAST.
−
−	~~== Categories ==~~
−
−	~~=== PTRS Standard ===~~
−
−	~~In this category, we have to prove termination for the given PTRS with relation to an arbitrary rewrite strategy.~~
−
−	~~The tools can give the following answers:~~
−
−	~~<pre>MAYBE, AST, PAST, SAST</pre>~~
−
−	~~=== PTRS Innermost ===~~
−
−
−	~~In this category, we have to prove termination for the given PTRS with relation to an innermost rewrite strategy.~~
−
−	~~The tools can give the following answers:~~
−
−	~~<pre>MAYBE, AST, PAST, SAST</pre>~~
−
−	~~[[Category:Categories]]~~

← Older revision		Revision as of 12:36, 15 January 2026
Line 85:		Line 85:

	<pre>MAYBE, AST, PAST, SAST</pre>		<pre>MAYBE, AST, PAST, SAST</pre>
		+
		+	[[Category:Categories]]

@@ Line 1: / Line 1: @@
 == General ==
-As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). The format of TRSs is explained [[Term Rewriting|here]]. To extend this format with probabilistic rules, we extend the reserved words by  <pre>prule, prob</pre>. Furthermore, rules are replaced by probabilistic rules that are defined as follows:
+As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). The format of TRSs is explained [[Term Rewriting|here]]. To extend this format for PTRSs, rules are replaced by probabilistic rules that are defined as follows:
 <pre>
 prule ::= ( prule term dist cost? )

@@ Line 9: / Line 9: @@
 </pre>
-The goal of the analysis is implicitly specified by the category.
+Some examples of valid PTRSs are shown below.
 == Probabilistic Termination ==
-All probabilistic termination categories consider termination w.r.t. arbitrary start terms.
+There are several notions of ``termination'' in the probabilistic setting.
 === PTRS Standard ===
-* full rewriting
+In this category, we have to prove termination for the given PTRS with relation to an arbitrary rewrite strategy.
 The tools can give the following answers:
@@ Line 24: / Line 79: @@
 === PTRS Innermost ===
-* innermost rewriting
 The tools can give the following answers:
 <pre>MAYBE, AST, PAST, SAST</pre>

← Older revision	Revision as of 08:14, 13 May 2024
(No difference)