New completeness results for lazy conditional narrowing

New completeness results for lazy conditional narrowing
复制标题

惰性条件缩小的新完整性结果

DOI:
10.1145/1013963.1013979
复制
发表时间:
2004
期刊:
--
影响因子:
--
通讯作者:
A. Middeldorp
A. Middeldorp
中科院分区:
--
文献类型:
--
作者:
M. Marin;A. Middeldorp

文献摘要

被引文献

相似文献

对于一类确定性条件重写系统(CTRS),我们证明了具有最左选择的延迟条件窄化演算(LCNC)的完备性。确定性CTR允许在其重写规则的右侧和条件中有额外的变量。从完备性证明中,我们得到了使微积分更具确定性的几点见解。此外,与为无条件情况开发的精化类似,我们通过对参与的CTR施加进一步的语法条件并限制需要建立完备性的解集,成功地消除了由于LCNC推理规则的选择而导致的所有不确定性。
We show the completeness of the lazy conditional narrowing calculus (LCNC) with leftmost selection for the class of deterministic conditional rewrite systems (CTRSs). Deterministic CTRSs permit extra variables in the right-hand sides and conditions of their rewrite rules. From the completeness proof we obtain several insights to make the calculus more deterministic. Furthermore, and similar to the refinements developed for the unconditional case, we succeeded in removing all nondeterminism due to the choice of the inference rule of LCNC by imposing further syntactic conditions on the participating CTRSs and restricting the set of solutions for which completeness needs to be established.