Probabilistic Rewriting

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 )
dist ::= ( ( term prob? )+ )
prob ::= :prob POSNAT

POSNAT is a positive natural number. If :prob is omitted, the weight is 1. The probabilities of a rule's outcomes are its weights divided by the sum of all its weights.

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 categories for PTRSs.

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.