Study of Program Inversion for Functional Programs Defining Injective Functions

在这项研究中，我们旨在将自动生成逆计算程序的程序逆方法应用到实际的函数式程序中，并开发了一种程序逆方法，该方法将给定的程序逆到关于函数应用的确定性的函数定义集，即程序。为了将这种方法应用到几种函数式语言中，作为目标程序，我们处理了术语重写系统，其中的类被称为函数式程序的计算模型。首先，我们提出了一种新的专门处理尾递归函数的逆变换，并将其融入到我们以前工作中开发的程序逆变换中。接下来，我们提出了一种确定重写规则的方法，这些规则在规则的应用方面是不确定的。更准确地说，在保留所需计算的情况下，该方法通过缩小计算范围来分析右侧来实例化每个规则。通过将该方法作为反演法的后处理，成功地改进了现有的反演法。最后，我们实现了检索方法，并通过浏览器提供了检索服务。

In this research, we aimed at applying program inversion methods that automatically generate inverse computation programs, into practical functional programs, and we developed a program inversion method that inverts a given program to a function-definition set which is deterministic with respect to function application, namely a program. To apply the method into several functional languages, as target programs, we dealt with term rewriting systems of which the class is known as a computation model of functional programs. First, we proposed a new inversion transformation that specializes in tail recursive functions, and then incorporated it into the program inversion method developed at our previous work. Next, we proposed a method for determinizing rewrite rules that are indeterministic with respect to application of rules. More precisely, with preserving desired computation, the method instantiates each of the rules by analyzing the right-hand side by means of narrowing computation. By using the method as a postprocess of the inversion method, we succeeded in improving the existing inversion method. Finally, we implemented the inversion method and provided a service of inversion via web browsers.