Confluence of Non-Left-Linear TRSs via Relative Termination

Confluence of Non-Left-Linear TRSs via Relative Termination
复制标题

通过相对终止实现非线性 TRS 的汇合

DOI：
10.1007/978-3-642-28717-6_21
复制
发表时间：
2012
期刊：
--
影响因子：
--
通讯作者：
Nao Hirokawa
Nao Hirokawa
中科院分区：
--
文献类型：
--
作者：
Dominik Klein;Nao Hirokawa

文献摘要

被引文献

相似文献

通过放宽Knuth和Benzmann的合流准则的终止性要求，利用扩展临界对的可连接性，提出了一个词项重写系统的合流准则。由于扩展临界对的计算需要方程的统一，而方程的统一是不可判定的，因此我们给出了一个自动判定可连接性的充分条件。
We present a confluence criterion for term rewrite systems by relaxing termination requirements of Knuth and Bendix’ confluence criterion, using joinability of extended critical pairs. Because computation of extended critical pairs requires equational unification, which is undecidable, we give a sufficient condition for testing joinability automatically.