There are many evaluation strategies for term rewrite systems, but automatically proving termination or analyzing complexity is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination or when runtime complexity and innermost runtime complexity coincide. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination w.r.t. innermost rewriting in order to prove full almost-sure termination of probabilistic term rewrite systems. These criteria can be applied for both termination and complexity analysis in the probabilistic setting. We implemented and evaluated our new contributions in the tool AProVE. Moreover, we also use our new results on innermost and full probabilistic rewriting to investigate the modularity of probabilistic termination properties.

翻译：项重写系统存在多种求值策略，但自动证明终止性或分析复杂度通常在最内层重写中最为简便。当最内层终止蕴含完全终止时，或当运行时复杂度与最内层运行时复杂度一致时，存在若干语法判定准则。我们将这些准则适配至概率场景，例如证明了在何种条件下，通过分析最内层重写下的几乎必然终止性即可证明概率项重写系统的完全几乎必然终止性。这些准则可同时应用于概率场景下的终止性分析与复杂度分析。我们在工具AProVE中实现并评估了这些新贡献。此外，我们还利用关于最内层与完全概率重写的新结果，探究了概率终止性质的模块性。