Strategies on functional languages

这项研究旨在消除阻碍术语重写系统(简称TRSS)的结果应用于派系语言的空白。得到了以下结果：(1)在实际执行时间内，只有规则较少的TRSS才能判断它们是否为NV序列。(2)将TRSS的根索引的概念推广到具有优先级的TRSS，并构造了一个原型系统，有效地计算了强序列优先级TRSS的头部范式的索引。(3)减少所需Redex的策略是规范化的。(4)证明了一类高阶TRSS的依赖对方法是有效的。(5)最左边的归约策略是对终止、右线性和根重叠的TRSS进行归一化。

This research is toward removing gaps that prevent from applying results of term rewriting systems (TRSs for short) to factional languages. The following results were obtained ;(1) Only TRSs having few rules can be decided whether they are NV-sequential in realistic execution time. The execution time of the calculating an index of a given term and a TRS is similar to the decision problem.(2) We extended the notion of root indexes of TRSs to TRSs with priorities and construct a prototype system that efficiently caliculate indexes for head normal forms of strongly sequential priority TRSs.(3) The strategy that reduce needed redex is normalizing.(4) We showd a class of higher-order TRSs in which the dependency pair method, a mecanized proof technique of termination, is effective.(5) The leftmost innermost reduction strategy is normalizing for terminating, right-linear and root over-lapping TRSs.