Program verification method based on reduction approximations

为了提出基于约简近似的程序验证技术，我们进行了研究。归一化归约策略中的重写理论，模板程序转换，高阶重写系统的终止，高阶归纳定理的自动证明，可达性问题的可判断性。通过深入的理论分析和实验，我们得到了以下结果：(1)提出了基于均衡弱合流的归一化策略的概念。结果表明，如果每个临界对都是根平衡可合的，则外部约化是左线性重写系统的一种归一化策略。这一结果扩展了需要减少的归一化策略。我们还提出了外部约简是一种可计算的约简策略，如果存在规则保持近似的话。(2)提出了一种基于重写系统的基于模板的程序转换框架。在没有显式使用数据结构归纳法的情况下，证明了程序转换方法的正确性。因此，我们的程序转换系统可以很容易地与自动定理证明器结合。(3)引入了增长逼近的概念，它是强序列逼近、NV序列逼近和右线性增长逼近的推广。我们证明了增长逼近推广了一类具有可判定正规化策略的项重写系统。此外，还给出了增长系统的汇合与终止的可判性。

To propose program verification techniques based on reduction approximations, we have studied. rewriting theories among normalization reduction strategies, program transformation by template, termination of higher-order rewriting systems, automated proving for higher-order inductive theorems, decidability of reachability problem. Thorough theoretical analysis and experiments, we have obtained the following results.(1)We proposed the notion of normalizing strategy based on balanced weak confluence. It was shown that external reduction is a normalizing strategy for left-linear term rewriting systems if every critical pair is root balanced joinable. This results expands normalizing strategy of needed reduction. We also presented that external reduction is a computable reduction strategy if regular preserving approximation if it exits.(2)We developed a framework of program transformation by template based on rewriting systems. The correctness of our program transformation method is proven without explicit use of induction on data structures. Thus our program transformation system can easily incorporate with automated theorem provers.(3)We introduce the notion of growing approximation, which is a generalization of strong sequential approximation, NV-sequential approximation and right-linear growing approximation. We have shown that the growing approximation extends the class of term rewriting systems having a decidable normalizing strategy. Moreover, the decidability of confluence and termination for growing systems is presented.