Difference between revisions of "Probabilistic Rewriting"
(some additional information on the probabilistic rewriting site) |
|||
| Line 9: | Line 9: | ||
</pre> | </pre> | ||
| − | + | Some examples of valid PTRSs are shown below. | |
| + | |||
| + | <pre> | ||
| + | ===== P1 ===== | ||
| + | (format PTRS) | ||
| + | (fun f 0) | ||
| + | (fun stop 0) | ||
| + | (prule f (( f :prob 1 ) (stop :prob 1 ))) | ||
| + | </pre> | ||
| + | * P1 models a coin flip that stops once it flips heads and keeps on going if it flips tails. | ||
| + | <pre> | ||
| + | ===== P2 ===== | ||
| + | (format PTRS) | ||
| + | (fun g 1) | ||
| + | (prule (g x) (( (g (g x)) :prob 1 ) (x :prob 1 ))) | ||
| + | </pre> | ||
| + | * P2 models a symmetric random walk on the numbers of f symbols in a term. | ||
| + | <pre> | ||
| + | ===== P3 ===== | ||
| + | (format PTRS) | ||
| + | (fun h 1) | ||
| + | (prule (h x) (( (h (h x)) :prob 2 ) (x :prob 1 ))) | ||
| + | </pre> | ||
| + | * P3 models a biased random walk on the numbers of h symbols in a term which is biased towards nontermination. | ||
== Probabilistic Termination == | == Probabilistic Termination == | ||
| − | + | There are several notions of ``termination'' in the probabilistic setting. | |
| + | As in ordinary term rewriting, we consider universal termination, i.e., we have no fixed start term, but consider every possible reduction. | ||
| + | For the formal definitions of all notions of termination, see [https://www.sciencedirect.com/science/article/pii/S0167642319301339 here]. | ||
| + | |||
| + | ===== Certain Termination ===== | ||
| + | |||
| + | A PTRS is certainly terminating if every possible reduction eventuelly terminates. | ||
| + | As this boils down to termination of TRSs, we usually try to omit certainly terminating examples in the following category, | ||
| + | and hence, have no allowed answer for a certainly terminating PTRS. | ||
| + | |||
| + | Example: None of the PTRSs P1, P2, or P3 are certainly terminating. | ||
| + | |||
| + | ===== Almost-Sure Termination (AST) ===== | ||
| + | |||
| + | A PTRS is almost-surely terminating if every non-terminating reduction occurs with probability 0. | ||
| + | |||
| + | Example: While P1 and P2 are AST, P3 is not AST. | ||
| + | |||
| + | ===== Positive Almost-Sure Termination (PAST) ===== | ||
| + | |||
| + | A PTRS is positive almost-surely terminating if the expected derivation length of every possible reduction is finite. | ||
| + | |||
| + | Example: Only P1 is PAST, but P2 and P3 are not PAST. | ||
| + | |||
| + | ===== Strong Almost-Sure Termination (SAST) ===== | ||
| + | |||
| + | A PTRS is strong almost-surely terminating if for every start term t there exists a bound C_t such that | ||
| + | the expected derivation length of every possible reduction starting in t is at most C_t. | ||
| + | |||
| + | Example: Again only P1 is PAST, but P2 and P3 are not PAST. | ||
| + | |||
| + | == Categories == | ||
=== PTRS Standard === | === 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: | The tools can give the following answers: | ||
| Line 24: | Line 79: | ||
=== PTRS Innermost === | === 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: | The tools can give the following answers: | ||
<pre>MAYBE, AST, PAST, SAST</pre> | <pre>MAYBE, AST, PAST, SAST</pre> | ||
Revision as of 11:19, 15 January 2026
Contents
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
Some examples of valid PTRSs are shown below.
===== P1 ===== (format PTRS) (fun f 0) (fun stop 0) (prule f (( f :prob 1 ) (stop :prob 1 )))
- P1 models a coin flip that stops once it flips heads and keeps on going if it flips tails.
===== P2 ===== (format PTRS) (fun g 1) (prule (g x) (( (g (g x)) :prob 1 ) (x :prob 1 )))
- P2 models a symmetric random walk on the numbers of f symbols in a term.
===== P3 ===== (format PTRS) (fun h 1) (prule (h x) (( (h (h x)) :prob 2 ) (x :prob 1 )))
- P3 models a biased random walk on the numbers of h symbols in a term which is biased towards nontermination.
Probabilistic Termination
There are several notions of ``termination in the probabilistic setting. As in ordinary term rewriting, we consider universal termination, i.e., we have no fixed start term, but consider every possible reduction. For the formal definitions of all notions of termination, see here.
Certain Termination
A PTRS is certainly terminating if every possible reduction eventuelly terminates. As this boils down to termination of TRSs, we usually try to omit certainly terminating examples in the following category, and hence, have no allowed answer for a certainly terminating PTRS.
Example: None of the PTRSs P1, P2, or P3 are certainly terminating.
Almost-Sure Termination (AST)
A PTRS is almost-surely terminating if every non-terminating reduction occurs with probability 0.
Example: While P1 and P2 are AST, P3 is not AST.
Positive Almost-Sure Termination (PAST)
A PTRS is positive almost-surely terminating if the expected derivation length of every possible reduction is finite.
Example: Only P1 is PAST, but P2 and P3 are not PAST.
Strong Almost-Sure Termination (SAST)
A PTRS is strong almost-surely terminating if for every start term t there exists a bound C_t such that the expected derivation length of every possible reduction starting in t is at most C_t.
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:
MAYBE, AST, PAST, SAST
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:
MAYBE, AST, PAST, SAST
