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.

翻译：项重写系统存在多种求值策略，但自动证明终止性通常对内层重写最为简单。目前已存在若干语法判据，可判断内层终止性何时蕴含全终止性。我们将这些判据适配到概率设置中，例如，我们证明了何时只需分析相对于内层重写的几乎必然终止性（AST）即可验证概率项重写系统（PTRSs）的全AST性。这些判据同样适用于其他终止性概念，如正几乎必然终止性。我们已在工具AProVE中实现并评估了这些新贡献。