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.