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浏览器提供了反转的服务。

项目成果

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网页

制約付き等式の定理自動証明器の試作

约束等式自动定理证明器原型

• 发表时间: 2009
• 作者: 西田直樹;中林直生;酒井正彦;草刈圭一朗;坂部俊樹
• 通讯作者: 坂部俊樹

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