From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Logic in Computer Science
2024-02-13 v3
Abstract
There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems (PTRSs). These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE.
Keywords
Cite
@article{arxiv.2310.06121,
title = {From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting},
author = {Jan-Christoph Kassing and Florian Frohn and Jürgen Giesl},
journal= {arXiv preprint arXiv:2310.06121},
year = {2024}
}