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

Research Project

Project/Area Number	13224088
Research Category	Grant-in-Aid for Scientific Research on Priority Areas (C)
Allocation Type	Single-year Grants
Review Section	Science and Engineering
Research Institution	National Institute of Informatics
Principal Investigator	佐藤健国立情報学研究所, 情報学基礎研究系, 教授 (00271635)
Co-Investigator(Kenkyū-buntansha)	新井紀子国立情報学研究所, 情報学基礎研究系, 助教授 (40264931) 龍田真国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
Project Period (FY)	2001
Project Status	Completed (Fiscal Year 2001)
Keywords	ソフトウェア発展 / 極小更新 / 仮説論理プログラム / 宣言的プログラミング
Research Abstract	ソフトェア発展はソフトウェア科学およびソフトウェア工学における重要なテーマである。佐藤は、以前、特定領域研究「発展機構を備えたソフトウェアの構成原理の研究」において極小変更の考えを用いたソフトウェア仕様の変更の研究を行い、仮説論理プログラミングによるプロトタイプシステムの開発も行った。本研究は、その研究をさらに発展させ、論理型プログラミングや関数型プログラミングのような宣言的なプログラミングに通用する,より一般的なソフトウェア発展の理論を構築することを目的とするものである.今年度では,このための基礎的な準備として以下の研究を行った.佐藤は,関数のない論理仕様に対する極小変更の自動化に向けて論理仕様を仮説論理型プログラムに変換し,その上での処理系で極小変更が自動的に行えるクラスの同定を行った.さらに,論理仕様に矛盾が生じたときに,その矛盾の一般化を用いて,より適切な更新ができるように,PAC learningの枠組みに基づいた極大矛盾除去の手法の検討を行った.龍田は,直観主義論理に基づく構成的なプログラム合成の研究において,二階古典自然演繹の強正規化性に関してCPS変換を用いたParigotの証明の誤りを指摘し,その原因であるCPS変換の継続消滅について論じ,オグメンテーションの概念を用いて証明を完成させた.新井は,命題論理の証明の複雑さについて,自動証明で頻繁に用いられるresolutionシステムとtableauxシステムの効率比較を理論的に行い,さらに、両システムを融合し新しい推論規則(symmetry rule)を導入したシステムの実装を行い,ここで初等的な組み合わせ論の問題を短時間で解くことに成功した.