Study on Rewriting Theory for Analysis, Verification and Efficient Execution of Functional Programs

这项研究旨在消除阻碍术语重写系统(TRS)的结果应用于功能语言的空白。得到了以下结果：(1)以前提出的证明高阶重写系统终止性的依赖对方法不适用于含有右侧嵌套变量和包含复制规则的重写系统。(2)利用树自动机技术和De Bruijn记号证明了关于强序列逼近或NV逼近所需的修正是可判定的。(3)证明了高阶重写系统中隐式归纳可证明的定理是归纳定理的子类。某些归纳定理被判定为非归纳性的情况发生。我们给出了保证重叠TRSS的最外层约简策略完全的条件，并给出了生成满足该条件的TRSS的变换。(5)给出了TRSS的一种变换，其输出定义了输入构造子TRSS的逆计算。在计算中，对于含有额外变量的线性TRSS，最里面的缩小是有效的，以获得所有的结果。

This research is toward removing gaps that prevent from applying results of term rewriting systems (TRS for short) to fuctional languages. The following results were obtained ;(1) The previously proposed dependency pair method for proving termination of higher-order rewrite systems cannot be applied for ones containing nested variable in a right-hand side and containing copy rules. We succeeded to remove the strong restriction from it for proving termination of simple-typed rewriting systems.(2) We showed that the needed redexes with respect to strong sequential or NV approximation are decidable by using tree-automata technique and the de Bruijn notations.(3) It appeared that theorems provable by implicit induction in higher-order rewrite systems are the subclass of the inductive theorems. The case happens that some inductive theorems are judged to be not inductive. We gave a condition to prevent this situation.(4) We gave a condition that guarantees the outer-most reduction strategy to be complete for overlapping TRSs, and showed a transformation of TRSs that produce TRSs that satisfy the condition.(5) We developed a transformation of TRSs whose outputs define the inverse computation of the input constructor TRSs. In the computation, innermost narrowing is effective for obtaining all results in case of linear TRSs with extra variables.