Study of Program Inversion for Functional Programs Defining Injective Functions

定义内射函数的函数程序的程序反演研究

• 批准号: 21700011
• 负责人: NISHIDA Naoki
• 金额: $ 2.58万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2009
• 资助国家: 日本
• 起止时间: 2009 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21700011/
• 关键词: プログラム逆化; プログラム変換; 項書換え系; 関数型言語; 情報基礎; 逆関数; 単射性; ログラム変換

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.

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

项目成果

More Specific Term Rewriting Systems ∗

更具体的术语重写系统*

• 发表时间: 2012
• 作者: Naoki Nishida

Proving Injectivity of Functions via Program Inversion in Term Rewriting

通过项重写中的程序反演证明函数的内射性

• 发表时间: 2010
• 作者: Naoki Nishida;German Vidal;Naoki Nishida and Masahiko Sakai
• 通讯作者: Naoki Nishida and Masahiko Sakai

Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems

改进左线性构造器系统中窄化的终止分析

• 发表时间: 2009
• 期刊: Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation
• 作者: Jose Iborra;Naoki Nishida;German Vidal
• 通讯作者: German Vidal

プログラム逆化ツールREPIUSのwebページ

程序反转工具REPIUS网页

Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

通过与线性相关的超性质解开条件项重写系统的可靠性

• 发表时间: 2012
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Naoki Nishida;Masahiko Sakai;and Toshiki Sakabe
• 通讯作者: and Toshiki Sakabe