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

这项研究旨在消除阻碍术语重写系统（简称TRS）结果应用于函数式语言的差距。得到以下结果：(1)先前提出的用于证明高阶重写系统终止的依赖对方法不适用于右侧包含嵌套变量和包含复制规则的系统。我们成功地去掉了证明简单类型重写系统终止的强约束。(2)利用树-自动机技术和de Bruijn符号证明了强序列近似或NV近似所需的矩阵是可确定的。(3)证明了高阶重写系统中的隐式归纳法可证明定理是归纳定理的子类。在这种情况下，一些归纳定理被判定为不归纳。我们提出了一个防止这种情况发生的条件。(4)给出了保证重叠trs最外层约简策略完备的条件，并给出了trs的变换，生成满足条件的trs。(5)我们开发了trs的变换，其输出定义了输入构造函数trs的逆计算。在计算中，对于具有额外变量的线性trs，最内层窄化对于获得所有结果都是有效的。

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.