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

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

基本信息

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

项目摘要

プログラム変換の手法である融合変換と、定理自動証明の手法である完備化を組み合わせた新しいプログラム変換手法を提案することを目的として、プログラム変換の実験と解析を行った。とくに、帰納的定理の強力な自動証明手法である書き換え帰納法と組み合わせることによって、プログラム変換に必要な性質を自動証明しながら、その結果を利用してプログラム変換を進めていくので、従来よりも強力な変換が可能となる。また、変換に必要な性質を自動的に発見することを可能とする補題発見機構を組み入れることにより、高度なプログラム自動変換を実現することができることを実証することができた。さらに、パターンをもちいたプログラム変換システムRAPTを開発した。これまでの研究から、プログラムの効率化にはいくつかの定石があることが明らかになっている。そこで、これらの定石を高階の変換パターンで表現し、パターンマッチングによるプログラム変換で効率を改良する方法を提案した。変換の正当性を検証するためには、プログラムのさまざまな帰納的性質を証明する必要がある。そこで、プログラムを書き換えシステムでモデル化し、定理自動証明の手法である潜在帰納法を適用することにより、プログラム変換とその正当性の検証を完全に自動化することに成功した。RAPTは入力プログラムを自動変換して出力プログラムを得るまでの手続きを6段階に分けて実現している。実装は関数型言語SMLをもちいて行い、ソースコードのサイズは約5000行である。また、プログラムの変換や検証に不可欠な基礎技術である高階プログラムの帰納的性質や停止条件に関する理論的な解析を進めるとともに、プログラムの実行メカニズムの設計に不可欠なリダクションの戦略に関する基礎理論の確立を行った。

我们对程序转换进行了实验和分析，目的是提出一种新的程序转换技术，该技术结合了融合转换，程序转换技术和完整性，即一种自动定理的方法。特别是，通过将其与归纳定理的强大自动证明方法相结合，它会自动证明程序转换所需的属性，然后使用结果进行程序转换，从而实现比以前更强大的转换。此外，通过合并一种允许自动发现转换的引理发现机制，已经证明可以实现高级自动程序转换。此外，我们已经开发了一个带有模式的程序转换系统。先前的研究表明，有几种提高计划效率的标准策略。因此，我们提出了一种使用高阶转换模式来表达这些标准策略的方法，并通过使用模式匹配来提高程序转换效率。为了验证转换的有效性，有必要证明程序的各种电感特性。因此，通过使用重写系统对程序进行建模并应用潜在诱导，这是一种自动定理证明技术，我们成功地完全自动化了程序转换和其有效性的验证。 RAPT是一个六步过程，涉及自动转换输入程序并获得输出程序。实现使用功能语言SML完成，源代码大小约为5,000行。此外，对较高计划的归纳特性和停止条件进行了理论分析，这是对程序转换和验证必不可少的基本技术，并建立了有关减少策略的基本理论，这对于设计程序执行机制至关重要。