A Strong Restriction of the Inductive Completion Procedure
A Strong Restriction of the Inductive Completion Procedure
复制标题
归纳完成程序的严格限制
DOI：
10.1016/s0747-7171(89)80069-0
复制
发表时间：
1986
期刊：
影响因子：
--
通讯作者：
L. Fribourg
中科院分区：
文献类型：
--
作者：
L. Fribourg
Knuth & Benedict（In：Computational Problems in Abstract Algebras，Pergamon Press，1970，pp. 263-297）完成一个方程系统成为一个合流。当方程以不明确的方式叠加时，它通过添加临界对来进行。Huet & Hullot（Proc. 21st Symp. Foundations in Computer Science，1980，pp 96-107）已经表明，对于构造函数满足所谓定义原理的理论，Knuth-Benefit过程可以用来证明构造函数是给定理论的归纳定理（证明归纳完成）。在本文中，我们表明，这是情况下，即使该过程是限制在一个线性选择的方式：首先，临界对是由初始理论的一个方程叠加到由临界对导出的一个方程中而线性生成的（两个方程之间不叠加），其次，对于每一个临界对，与理论方程叠加的发生由选择函数唯一确定. p与Knuth-Benidians程序不同，我们的程序在成功终止时，一般不会产生汇合系统。然而，生成的系统保证具有地面汇流属性（汇流项没有变量）。这个结果足以保证猜想的有效性。我们的限制完成程序终止在许多情况下，归纳完成程序循环，产生无限多的关键对。该程序适用于没有构造函数的理论（Jouannaud & Kounalis，Proc. Symp.《计算机科学中的逻辑》，剑桥，MA，1986，pp. 358-366），并延伸到条件理论和条件假设。它还可以包含经典归纳法中使用的各种技术。然后，该过程结合了经典归纳法的效率与归纳完成的简单性。
The procedure of Knuth & Bendix (In:Computational Problems in Abstract Algebras,Pergamon Press, 1970, pp. 263–297) completes a system of equations into a confluent one. It proceeds by adding critical pairs when equations superpose themselves in an ambiguous way. Huet & Hullot (Proc. 21st Symp. Foundations in Computer Science, 1980, pp 96–107) have shown that, for theories with constructors satisfying a so-calledprinciple of definition, the Knuth-Bendix procedure can be used to prove that conjectures are inductive theorems of a given theory (proofs by inductive completion).In this paper, we show that this is the case even when the procedure is restricted in a linear selecting manner: first, critical pairs are generated in alinearmanner by superposition of one equation of the initial theory into one equation issued from critical pairs (no superposition between two equations both issued from critical pairs); second, for each critical pair, the occurrence of superposition with theory equations is uniquely determined by aselection function. p Unlike the Knuth-Bendix procedure, our procedure, when terminating with success, does not produce a confluent system in general. However, the generated system is guaranteed to have theground-confluenceproperty (confluence for terms without variables). This result suffices to guarantee the conjecture validity. Our restricted completion procedure terminates in many cases where the inductive completion procedure loops, generating infinitely many critical pairs. The procedure applies to theories without constructors (Jouannaud & Kounalis, Proc. Symp. on Logic in Computer Science, Cambridge, MA, 1986, pp. 358–366) and extends to conditional theories and conditional conjectures. It can also incorporate various techniques used in classical induction. The procedure then combines the efficiency of classical induction method with the simplicity of inductive completion.