| 研究概要 |
本研究では,以前に佐藤が行っていた極小変更によるソフトウェア仕様の発展の研究を発展させ,論理型言語や関数型言語のような宣言型プログラミング一般に適用可能なより広範囲のソフトウェア発展の理論を構築し,プロトタイプシステムを開発して,実証を行う.今年度の成果はいかである。(1)は論理型言語でのソフトウェア発展の研究成果、(2),(3)は、関数型言語のソフトウェア発展に関連する基礎的考察の研究成果である。
(1)論理型言語での極小変更仕様の導出のために従来必要だった変更の極小性チェックを省略でき,かつ完全性を持つ手法を開発した。具体的には、論理仕様からデフォルト理論(default theory)への変換を用いることにより,デフォルト理論での拡張が極小変更プログラムに1対1対応することを示すことで、上記性質を持つ手法の提案を行った。さらに、佐藤が以前提案したデフォルト理論での証明系の単純化した手続きが極小変更プログラムの計算に使用できることを示した。
(2)多項式時間で実行可能なプログラムに正確に対応する素朴集合論(軽アフィン集合論)の考案および、その集合論における構成的証明から多項式時間プログラムを自動的に抽出するプログラム抽出法の考案、考察を行った.
(3)高階λμ計算の強正規化性がParigotによりCPS変換を用いて証明されていたが、この証明の誤りを主補題の反例により示し、それが継続消滅に起因していることを指摘し、augmentationの概念を用いてこの証明を完成させた。
|
