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

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

基本信息

批准号：
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的缺点，我们能够计算反向计算。存在一个问题，因为一组计算结果包括不是解决方案的术语。为了解决这个问题，我们表明，如果转换获得的TR具有停止能力，则可以通过应用完整的程序获得具有汇合的TR。完整的过程是生成Confluence TRS的过程，但不一定是成功。但是，当我们进行了一个实践实验时，在该实验中，逆编译器获得的TR具有停止能力时，我们发现实验是使用一个实际示例进行的，其中逆编译器获得的TR具有停止能力，并进行了实验。所有完整的程序都是成功的。此外，还建立了以前的反编译器的实现和界面。在实验中，实施并使用了常规的完整系统。但是，在大多数情况下，方程的方向在递归路径顺序中失败。因此，通过使用防止性能工具实现完整的系统，完成了完成。在处理使用等效关系定义的函数的TR中，必须使用最内向的策略评估该术语。本财政年度的结果未获得常规完整性，因此无法获得此类TR的结果。因此，还证明了足够的条件可以保留传统框架对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

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