On proving inductive properties of abstract data types
On proving inductive properties of abstract data types
复制标题
关于证明抽象数据类型的归纳性质
DOI：
10.1145/567446.567461
复制
发表时间：
1980
期刊：
影响因子：
--
通讯作者：
D. Musser
中科院分区：
文献类型：
--
作者：
D. Musser
数据类型（例如有限序列）代数规范的方程公理通常可以形成一组收敛的重写规则。即，所有重写的序列都是有限的，并且唯一终止。如果添加了与数据类型属性相对应的重写规则，该规则的证明需要诱导（例如序列串联的关联性），则可能会破坏收敛性，但通常可以使用Knuth-Bendix算法来恢复收敛，以生成其他规则。因此获得的一组收敛规则可以用作公理的方程理论以及添加的属性的决策过程。这一事实与公理的“完整规范”属性相结合，导致了一种新的归纳特性证明方法 - 而不是需要明确调用归纳性推理规则。
The equational axioms of an algebraic specification of a data type (such as finite sequences) often can be formed into a convergent set of rewrite rules; i.e. such that all sequences of rewrites are finite and uniquely terminating. If one adds a rewrite rule corresponding to a data type property whose proof requires induction (such as associativity of sequence concatenation), convergence may be destroyed, but often can be restored by using the Knuth-Bendix algorithm to generate additional rules. A convergent set of rules thus obtained can be used as a decision procedure for the equational theory for the axioms plus the property added. This fact, combined with a "full specification" property of axiomatizations, leads to a new method of proof of inductive properties--not requiring the explicit invocation of an inductive rule of inference.