完備化に基づくプログラム自動変換の研究

基于完备性的程序自动转换研究

基本信息

批准号：
15017203
负责人：
外山芳人
金额：
$ 1.34万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
2003
资助国家：
日本
起止时间：
2003 至无数据
项目状态：
已结题

项目摘要

完備化に基づくプログラム融合変換のアイデアを,高階プログラムに適用するためには,高階書き換えシステムの完備化を実現する必要がある。しかし,高階書き換えシステムの完備化手続きの多くは机上の提案にとどまっており,実装にはいたっていない。これは,完備化手続きを実装するために不可欠な高階書き換えシステムの停止性が,簡単に判定できなかったからである。本研究では,項の幅の上界を設定することで,固定次数の関数記号に対する単純化順序の定義が,可変次数の関数記号に対してもそのまま有効に働くことに注目し,S式書き換えシステムの停止性が辞書式経路順序で簡単に判定できることを示した。実際に利用される高階書き換えシステムの多くは,S式書き換えシステムで表現できるため,ここで提案された停止性判定法をもちいて完備化可能である。我々は,S式書き換えシステムの完備化手続きを計算機上に実装し,高階書き換えシステムの完備化と融合変換が容易に実現できることを実験によって明らかにした。さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,高階関数を含む帰納的定理の自動証明法を検討し,高階書き換えシステムにおける潜在帰納法の枠組みを提案するとともに,潜在帰納法の適用に不可欠な十分完全性の判定が決定可能であることを明らかにした。また,書き換え代入に基づく2階のパターンマッチングを提案し,パターマッチングをもちいたプログラム変換手続きを改良するとともに,書き換え帰納法に基づく高階プログラムの融合変換の実験を行った。

为了基于对高层计划的实现来应用程序融合转换的想法，有必要完成高地板重写系统。但是，高楼重写系统的许多重写系统仅在桌子上建议，并且未实施。这是因为不容易确定高地板重写系统的悬挂是必不可少的。在这项研究中，请注意，固定数量的函数符号中简化顺序的定义将通过设置该部分的顶部世界有效。在字典路线顺序中轻松确定。许多实际使用的高地板重写系统可以在S类型重写系统中表达，因此可以通过建议的悬架判断方法可以完全增强它。我们已经在计算器上实现了S类型重写系统的完成过程，并揭示了该实验很容易得到充分增强，并且高地板重写系统的融合转换。此外，为了根据针对本研究的实现扩大程序转换的应用程序范围，我们将研究归纳定理的自动祝贺，包括高地板函数，并提出了潜在诱导方法的框架在高地板重写系统中，可以确定足够的探索判断，这对于应用潜在诱导方法至关重要。此外，我们根据重写分配提出了二楼的模式匹配，通过推杆匹配改进了程序的转换过程，并根据基于重写归纳方法进行了有关高地板程序融合转换的实验。