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中实现并评估了这些新成果。