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

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

基本信息

批准号：
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行。此外，高地板计划的归纳性质和悬架条件的理论分析，这对于程序转换和验证至关重要，并建立了减少策略的基本理论，这对于计划执行机制的设计至关重要。