| 研究概要 |
本研究の成果は大きく5つに分けられている.以下に概要を述べる.
1.等式言語の枠組みにおけるメタ機能を研究した.メタ機能は学習の結果を自己に反映させてシステムを成長させる基本的メカニズムであり,最近ではリフレクションと呼ばれて,盛んに研究されている.本研究では等式言語の枠組みでその可能性を実証しており,本研究遂行のための理論的な保証を提供している.
2.等式言語の枠組みにおけるモジュール性について研究した.モジュール性は大規模なシステムを開発するための最も重要な概念であり,扱いやすい小さな部分システムの合成により最終的なシステムを完成させ得る技術である.本研究では特に,システムの検証や合成に重要な役割を果たす単純停止性のモジュール性を証明した.
3.以上の2つの基礎の上に,EBLに基づくプログラムの検証,特に停止性の検証,について研究した.停止性検証はすべての先行順序からなる空間上での探索問題に帰着される.本研究では,その探索の過程でシステムが学習した知識を真偽維持システムで管理し,検証を効率化する手法を開発した.
4.プログラムの合成へのEBL応用手法について研究した.この枠組みにおいては,プログラムの合成は等式理論の完備化と呼ばれている.この研究においても、探索の過程でシステムが学習した知識を真偽維持システムで管理することにより,効率の良い完備化手続きを開発することができた.
5.プログラム変換についてEBLの考え方の利用を研究した.特に,停止性を保存する変換を考察の対象とした.本研究では合成可能(composable)な系の停止性について,混合系の非停止性を示す無限簡約列を純粋系の無限簡約列に変換する手法の一般化においてEBLの考え方を参考にしている.
|
