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

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

• 批准号: 15017203
• 负责人: 外山 芳人
• 金额: $ 1.34万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2003
• 资助国家: 日本
• 起止时间: 2003 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15017203/
• 关键词: 情報基礎; ソフトウェア検証; プログラム変換; 定理自動証明; 項書き換えシステム; 情報基礎; ソフトウェア検証; プログラム変換; 定理自動証明; 項書き換えシステム

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

为了基于完成的程序融合转换的想法，必须实现高阶重写系统的完成。但是，完成高阶重写系统的大多数程序只是建议，尚未实施。这是因为不能轻易确定高阶重写系统的悬停性，这对于实施完成过程至关重要。在这项研究中，我们注意到，通过设置术语宽度的上限，固定顺序函数符号的简化顺序的定义对于可变级函数符号也有效，并且我们表明，使用词典路由顺序可以轻松确定S形莫拉重写系统的可伸缩性。许多实际的高阶重写系统都可以使用S型重写系统表示，并且可以使用此处提出的停止性确定方法完成。我们已经通过实验证明，可以在计算机上轻松实现S型重写系统的完成过程以及高阶重写系统的完成和融合转换。此外，为了扩大基于完成的程序转型的应用范围，该研究的目的是针对诱导定理的自动证明方法，包括高阶功能在内，并提出了高阶重写系统中潜在诱导的框架，并明确提出了对足够的脉动施用，可以确定足够的独立性。我们还根据重写分配提出了二阶模式匹配，并通过推杆匹配改进了程序的转换过程，并根据基于重写感应的融合进行了融合转换高阶程序的融合转换。