权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

関数型プログラムの逆計算プログラム生成に関する研究

函数程序逆计算程序生成研究

基本信息

批准号：
17700009
负责人：
西田直樹
金额：
$ 1.47万
依托单位：
Nagoya University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2005
资助国家：
日本
起止时间：
2005 至 2007
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17700009/
关键词：
情報基礎項書換え系関数型言語プログラム変換

项目摘要

本研究では,項書換え系(TRS)からの逆計算プログラムの生成に取り組んでおり,バグのないプログラムによる効率的な逆計算をめざしている.本年度も前年度に引続き,単射関数に注目し,決定的な計算を行う逆関数プログラムの生成に取り組んだ.逆計算コンパイラが生成するプログラムは一般に停止性や合流性を持つとは限らない.また,紐解き変換がCTRSを近似したTRSを生成するという欠点から,逆計算の計算結果の集合に解ではない項が含まれるという問題があった.これを解決するために,変換で得られたTRSが停止性を持つ場合には,完備化手続きを適用することで合流性を持つTRSを得られることを示した.完備化手続きは合流性を持つTRSを生成する手続きであるが,必ずしも成功するわけではない.しかし,逆計算コンパイラで得られたTRSが停止性を持つ実用的な例で実験を行なったところ,実験した例すべてで完備化手続きが成功した.さらに,これまでの逆計算コンパイラの実装とインタフェースを整備した.実験では従来の完備化システムを実装して用いた.しかし,ほとんどの例では再帰経路順序では等式の方向付けに失敗した.そこで,停止性証明ツールを利用した完備化システムを実現することで,完備化に成功した.等価関係を利用して定義されるような関数を扱うTRSでは,項を最内戦略で評価する必要がある.従来の完備化ではそのようなTRSについては正しい結果が得られない.そこで,最内戦略で評価されるTRSに対する従来の完備化の枠組の正当性を保存するための十分条件も示した.今年度の研究結果は年度内の発表は間に合わなかったが,すでに論文にまとめるまでに至っている.また,本成果は条件付きTRSからTRSへの紐解き変換の改善に相当し,今後,条件付きTRSの研究に役立つことが期待できる.

In this study, the inverse calculation of the TRS (Term Transformation System) was performed. This year and the previous year, the number of shots, the number of decisions, the calculation of the inverse number of shots, the generation of the selection group. The inverse calculation is based on the general stopping property and the convergence property. The solution of CTRS is approximate, TRS is generated, and the set of inverse calculation results is solved. The solution is to change the TRS to stop the situation, complete the manual, and apply the TRS to the convergence. Complete the manual to meet the nature of TRS generation, manual to meet, must be successful. The inverse calculation of TRS was successful in obtaining TRS and stopping TRS. In this case, the inverse calculation of the inverse calculation is carried out. In order to improve the quality of the products, we should improve the quality of the products. In this case, the order of the path is reversed, and the direction of the equation is reversed. The proof of stopping property is used to complete the system. The relationship between TRS and the relationship between TRS. The result of the completion of TRS is that the TRS is not perfect. Therefore, the most internal evaluation strategy demonstrates that there are very conditions for preserving the legitimacy of the recent comprehensive organization of TRS. The results of this year's research show that the research results of this year are consistent with those of the previous year. The results of this study are expected to improve TRS performance.

项目成果

期刊论文数量（0）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Transformation for Refining Unraveled Conditional Term Rewriting Sys-tems

改进已解开的条件术语重写系统的转型

DOI：
发表时间：
2006
期刊：
Proc. of 6th International Workshop on Reduc-tion Strategies in Rewriting and Programming(WRS2006)
影响因子：
0
作者：
Naoki Nishida;Tomohiro Mizu-tarsi;and Masahiko Sakai
通讯作者：
and Masahiko Sakai

Convergent Term Rewriting Systems for Inverse Compu-tation of Injective Functions

单射函数逆计算的收敛项重写系统