Probabilistic Rewriting

From Termination-Portal.org
Revision as of 13:17, 13 May 2024 by JCKassing (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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