Difference between revisions of "Probabilistic Rewriting"
From Termination-Portal.org
Jump to navigationJump to search (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...") |
|||
| Line 1: | Line 1: | ||
== General == | == 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: | + | 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: |
<pre> | <pre> | ||
prule ::= ( prule term dist cost? ) | prule ::= ( prule term dist cost? ) | ||
Revision as of 10:15, 10 May 2024
General
As in the non-probabilistic setting, we use an adaption of the ARI format, so probabilistic TRSs (PTRSs) are represented as S-Expressions (see here, Sec. 3.1). The format of TRSs is explained here. To extend this format with probabilistic rules, we extend the reserved words by
prule, prob
. Furthermore, rules are replaced by probabilistic rules that are defined as follows:
prule ::= ( prule term dist cost? ) cost ::= :cost number dist ::= ( ( term prob? )* ) prob ::= :prob number
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:
MAYBE, AST, PAST, SAST
PTRS Innermost
- innermost rewriting
The tools can give the following answers:
MAYBE, AST, PAST, SAST
