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

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

基本信息

批准号：
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の研究に役立つことが期待できる.

在这项研究中，我们正在致力于从术语重写系统（TRS）生成逆计算程序，旨在使用无错误的程序进行高效的逆计算。今年，与前一年一样，我们将重点关注单射函数，我们致力于生成执行确定性计算的逆函数程序。通过逆计算生成的程序，编译器通常不一定具有停止属性或合流。此外，分解变换会生成近似于 CTRS 的 TRS。不利的是存在一个问题，即计算结果集包含不是解的项。为了解决这个问题，如果通过变换获得的TRS具有停止性质，则可以通过应用完成过程来解决该问题。完成过程为。一个用confluence生成TRS的程序，但是并不总是成功。但是，逆向编译器得到的TRS可以我用一个实际的例子进行实验，我实验的例子在所有情况下完成过程都是成功的。此外，我们改进了以前的逆计算编译器的实现和接口。在实验中，我们实现并使用了传统的完成系统。但是，在大多数示例中，递归路径顺序是相等的。公式因此，我们通过使用停止证明工具创建一个完整的系统，成功地完成了该系统。在处理使用等价关系定义的函数的 TRS 中，术语需要使用 Moinai 策略进行评估。传统的完整性无法为这种TRS得出正确的结果。因此，我们还证明了保留最内层策略评估的TRS的传统完整性框架的有效性的充分条件。今年的研究结果是。虽然结果未能在本财年及时发表，但已被整理成一篇论文。此外，该结果对应于从条件TRS到TRS的分解转换的改进，预计对研究有用。以后有条件TRS就可以。

项目成果

期刊论文数量（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

Dependency Graph Method for Proving Termination of Narrowing

证明收缩终止的依赖图方法