Modularity of Termination in Probabilistic Term Rewriting
Authors: J.-C. Kassing, J. Giesl
We investigate the modularity of probabilistic notions of termination in term rewriting. In the probabilistic setting, there are several interesting termination properties: almost-sure termination (termination with probability 1), positive almost-sure termination (finite expected runtime of each rewrite sequence), and strong almost-sure termination (expected runtime is bounded by a constant for each start term). A property is called modular if it is preserved for certain unions of probabilistic term rewrite systems. We show that these three termination properties have different modularity behavior for innermost rewriting. Utilizing known relations between innermost and full probabilistic rewriting allows us to obtain modularity results for full probabilistic rewriting as well.