宣言的プログラミングにおけるソフトウェア発展の研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14019084
• Research Institution: National Institute of Informatics
• Principal Investigator: 佐藤 健 国立情報学研究所, 情報学基礎研究系, 教授 (00271635)
• Co-Investigator(Kenkyū-buntansha): 照井 一成 国立情報学研究所, 情報学基礎研究系, 助手 (70353422) ; 新井 紀子 国立情報学研究所, 情報学基礎研究系, 助教授 (40264931) ; 龍田 真 国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
• Keywords: ソフトウェア発展 / 宣言的プログラミング / デフォルト論理 / 関数型プログラミング

Research Abstract

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

Research Products

• [Publications] 佐藤 健: "極小性チェックを必要としない極小変更ソフトウェア仕様の導出"Proc. of FOSE02. 143-150 (2002)
• [Publications] K.Nakazawa, M.Tatsuta: "Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction"Journal of Symbolic Logic. (掲載予定). (2003)
• [Publications] Ken Satoh: "Constructing a Critical Casebase to Represent a Lattice-Based Relation"Progress in Discovery Science 2002, LNAI. 2281. 214-223 (2002)
• [Publications] Shi-Kuo Chang(編者), Ken Satoh(分担執筆): "Handbook of Software Engineering and Knowledge Engineering, Vol.2の中のNonmonotonic Reasoning and Consistency Management in Software Engineering(pp.629-644)"World Scientific. 794 (2002)