一句话：将最内层重写的终止与复杂度准则推广到概率项重写，证明几乎必然终止和复杂度可模块化分析。
项重写系统有多种求值策略，而终止性与复杂度分析通常在 innermost 重写下最容易进行。已有若干语法准则刻画何时 innermost 终止可推出完全终止，或何时运行时复杂度与 innermost 运行时复杂度一致。本文把这些准则推广到概率情形，给出在何种条件下只需分析概率项重写系统的 innermost 几乎必然终止，即可证明其完全几乎必然终止，并将准则用于概率设置下的终止与复杂度分析。作者在 AProVE 中实现并评估了新贡献，还利用这些结果考察概率终止性质的模块性。
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 to investigate the modularity of probabilistic termination properties.
@article{paperbot3341,
title = {From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity},
author = {Jan-Christoph Kassing and Jürgen Giesl},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:28)2025}
}