从最内到完全的随机项重写几乎必然终止
计算机科学中的逻辑
2024-02-13 v3
摘要
项重写系统有多种求值策略，但自动证明终止通常对最内重写最为容易。存在一些句法判据说明最内终止蕴含完全终止。我们将这些判据适配到概率设定，例如，我们展示了何时只需分析概率项重写系统（PTRSs）关于最内重写的几乎必然终止（AST）即可证明完全 AST。这些判据也适用于其他终止概念，如正 AST。我们在 AProVE 工具中实现并评估了我们的新贡献。
引用
@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}
}