将约束 TRS 的依赖链转换为有界整数单调序列
计算机科学中的逻辑
2018-02-20 v1
摘要
在用于证明重写系统终止性的依赖对框架中，多项式解释被用于将对依赖链转换为有界递减整数序列，它们对证明终止成功起着重要作用，尤其对约束重写系统。在本文中，我们展示线性多项式解释将依赖链转换为有界单调（即递减或递增）整数序列的充分条件。此类多项式解释将原始系统的重写序列独立于依赖链的转换而转换为递减或递增序列。当我们将重写序列转换为递增序列时，多项式解释对标记函数符号的可归约位置具有非正系数。我们提出四个 DP 处理器，分别参数化地将依赖链和重写序列转换为递减或递增的整数序列。我们展示此类多项式解释使我们成功证明整数上 McCarthy 91 函数的终止性。
引用
@article{arxiv.1802.06497,
title = {Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers},
author = {Tomohiro Sasano and Naoki Nishida and Masahiko Sakai and Tomoya Ueyama},
journal= {arXiv preprint arXiv:1802.06497},
year = {2018}
}
备注
In Proceedings WPTE 2017, arXiv:1802.05862