Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
复制标题
终止具有浅右线性、折叠和右基规则的重写系统
DOI：
10.1007/11532231_12
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
A. Tiwari
中科院分区：
文献类型：
--
作者：
Guillem Godoy;A. Tiwari
我们表明，终止是可判定的重写系统，包含浅和右线性规则，崩溃的规则，右接地规则。这类重写系统的表达能力足以包含有趣的规则。我们的证明使用的事实，这类重写系统是已知的正则保持，因此可达性和可连接性问题是可判定的。通过对非终止导子的分析，得到了终止性的判定性。
We show that termination is decidable for rewrite systems that contain shallow and right-linear rules, collapsing rules, and right-ground rules. This class of rewrite systems is expressive enough to include interesting rules. Our proof uses the fact that this class of rewrite systems is known to be regularity-preserving and hence the reachability and joinability problems are decidable. Decidability of termination is obtained by analyzing the nonterminating derivations.