Study of Program Inversion for Functional Programs Defining Injective Functions

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

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.