高階関数を用いたプログラム検証および変換技術の高度化に関する研究

利用高阶函数改进程序验证和转换技术的研究

基本信息

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

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17700002/
关键词：
項書き換えシステム高階関数単純型付き項書き換えシステムプログラム検証書き換え帰納法プログラム変換パターン基づくプログラム変換補題自動発見法項群き換えシステム帰納的定理証明高階書き換えシステム単純型付き書き換えシステム変換パターン補題自動発見停止性

项目摘要

単純型付き項書き換えシステムの停止性検証手法の高度化を以下の点について試みた。(1)依存対手法における引数フィルタリングおよび使用可能規則を高階の場合への拡張を行った。(2)実験システムについての検討を進めた。特に、効率的な実装を実現するためのSAT検証器を用いた実装法についての検討を行い、その基本となる経路順序の符号化法について改良を行った。また停止性にもとづく帰納的定理の自動証明法である書き換え帰納法についての検討を進めた。特に反証付き書き換え帰納法に適した補題自動導入法について検討を行った。発散鑑定法を改良し、健全性を持つ発散鑑定法を提案した。実験システムを実装するとともに証明システムのベンチマークとなる例題集を抽出し、他の書き換え帰納法に基づく定理証明器との比較実験を行った。また、反証付き書き換え帰納法を利用するために必要な合流性を保障する方法について検討を進めた。停止性の検証器は多数提案されているのに対して、合流性の検証器の提案はあまりなされていないため、合流性の自動検証法について実験システムを構築し検討を行った。合流性の十分条件を満たさない項書き換えシステムについて分解手法を用いる判定法を利用することの検討を行い、分解手法を利用した合流性検証器の提案を行った。変換パターンに基づくプログラム変換のための変換パターンの抽出法について検討をすすめた。2階の一般化アルゴリズムを提案し、それに基づいて具体的なプログラム変換から変換パターンを抽出する実験を行った。変換に利用可能なパターンの抽出を容易にするためのヒューリスティクスについて検討を行い、いくつかの変換パターンの抽出に成功した。

我们试图在以下几点中改善简单键入术语重写系统的可耐验证验证方法。（1）依赖关系对方法中的参数过滤和可用规则已扩展到高阶情况。（2）我们已经进行了实验系统的研究。特别是，我们使用SAT验证符检查了实现方法以实现有效的实现，并改进了为路线顺序编码的基本方法。我们还讨论了改写诱导，这是一种基于停止性的自动归纳定理方法。我们已经检查了一种自动引理介绍方法，该方法特别适合通过反驳而重写归纳。我们提出了一种分歧评估方法，该方法改善了声音的分歧评估方法。实施了实验系统，并提取了一个示例集合，该集合将作为证明系统的基准，并根据其他重写诱导方法进行了比较实验。我们还讨论了确保使用改写归纳所需的汇合处的方法。尽管已经提出了许多停止能力验证者，但汇合验证者的建议很少，因此对自动汇合验证方法进行了构建并检查了实验系统。我们使用判断方法使用分解方法进行了调查，以实现不满足汇合的足够条件的术语重写系统，并建议使用分解方法进行汇合验证设备。我们建议采用一种根据转换模式提取程序转换的转换模式的方法。我们在第二阶提出了一种概括算法，并基于此，我们进行了一个实验，以从具体程序转换中提取转换模式。我们研究了启发式方法，以促进提取可用于转化的模式，并成功提取了几种转换模式。