Difference between revisions of "Probabilistic Rewriting"
From Termination-Portal.org
Jump to navigationJump to searchm (JCKassing moved page Prob Rewriting to Probabilistic Rewriting: Change of title) |
|||
| 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 | + | 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> | <pre> | ||
prule ::= ( prule term dist cost? ) | prule ::= ( prule term dist cost? ) | ||
Latest revision as of 13:17, 13 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 for PTRSs, 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
