从线性项重写到保持终止性的图重写
计算机科学中的逻辑
2021-12-22 v2
摘要
项重写系统（TRSs）到图重写系统的编码通常会丧失全局终止性，即这些编码并非在所有图上都终止。例如，终止的 TRS 规则 a(b(x)) -> b(a(x)) 的典型编码可能沿着 a 与 b 的循环被无限次应用。最近，我们引入了 PBPO+，一种图重写形式体系，其中规则利用类型图来指定变换并控制规则的可应用性。在本文中，我们证明 PBPO+ 允许对线性 TRS 规则进行自然的编码，从而全局保持终止性。该结果是朝着以保留终止性与合流性等性质的方式，使用图重写对其他重写形式体系（如 lambda 演算与高阶重写）进行建模的一步。此外，我们期望该编码可作为将 TRS 终止方法提升到 PBPO+ 重写的指南。
引用
@article{arxiv.2106.13826,
title = {From Linear Term Rewriting to Graph Rewriting with Preservation of Termination},
author = {Roy Overbeek and Jörg Endrullis},
journal= {arXiv preprint arXiv:2106.13826},
year = {2021}
}
备注
In Proceedings GCM 2021, arXiv:2112.10217. arXiv admin note: text overlap with arXiv:2010.08230