On sufficient-completeness and related properties of term rewriting systems
On sufficient-completeness and related properties of term rewriting systems
复制标题
术语重写系统的充分完备性及相关性质
DOI：
10.1007/bf00292110
复制
发表时间：
1987
期刊：
影响因子：
0.6
通讯作者：
Hantao Zhang
中科院分区：
文献类型：
--
作者：
D. Kapur;P. Narendran;Hantao Zhang
摘要证明了满足一定条件的方程规格的充分完整性的可判定性。此外，还证明了项的拟约化的相关概念关于规则集的可判定性。关于不可约地面条款的长期重写系统的其他结果也遵循这些可判定性证明中使用的一个关键技术引理;这个技术引理指出，有一个有限的范围内的地面条款，需要考虑的替代，以检查一个给定的长期，是否得到的结果由任何替代地面条款到长期是不可约的。这些结果首先显示为非类型化系统，随后扩展到类型化系统。
SummaryThe decidability of the sufficient completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible. These results are first shown for untyped systems and are subsequently extended to typed systems.