始祖学習によるソフトウェア発展プロセスの統一的構成技術の開発

Research Project

Project/Area Number	15017201
Research Category	Grant-in-Aid for Scientific Research on Priority Areas
Allocation Type	Single-year Grants
Review Section	Science and Engineering
Research Institution	Kyoto University
Principal Investigator	山本章博京都大学, 情報学研究科, 教授 (30230535)
Co-Investigator(Kenkyū-buntansha)	林晋神戸大学, 工学部, 教授 (40156443) 中戸川孝治北海道大学, 文学研究科, 教授 (20237316) 立木秀樹京都大学, 人間環境学研究科, 助教授 (10211377)
Project Period (FY)	2003
Project Status	Completed (Fiscal Year 2003)
Budget Amount *help	¥4,600,000 (Direct Cost: ¥4,600,000) Fiscal Year 2003: ¥4,600,000 (Direct Cost: ¥4,600,000)
Keywords	始祖学習 / 極限同定 / 帰納推論 / 帰納論理 / メタ論理プログラミング
Research Abstract	本研究では正データからの極限同定による帰納推論を論理の視点から再検討し,始祖学習と名づけた上で,ソフトウェア発展の理論的基盤とすることにある.本年度は論理の手続き的意味論と始祖学習の接続を中心に研究を行った. 帰納推論を特別なクラスの論理式で表現する手法に付いては,本研究の分担者である林と協力者であるオーストラリア・ニュー・サウス・ウェールズ大のMartin氏が独立に発見していた.さらに,この手法は論理の手続き的意味論の拡張であることも示されている.一方,ソフトウェア発展はプログラムを発展させること,すなわち,プログラムをデータとして扱わなければならない.そこで,本研究では,メタ論理プログラミングを始祖学習に利用することにした.従来もメタ論理プログラミングを帰納論理へ応用する研究は提案されてはいたが,上述の特別なクラスの論理式を用いないため,始祖学習とみなすには問題を含んでいた.本研究では,特別なクラスの論理式とメタ論理プログラミングとの組合せがソフトウェア発展を表現することを示した.また「発展とは現状を否定することにある」との観点から,論理における否定の手続き的意味論と始祖学習との関係を検討し,論理プログラムのあるクラスを対象にすると,始祖学習と否定が結合できるということを確認した. さらに,始祖学習と現実のソフトウェア開発技法との関係の検討,実数などのデータのコード化と始祖学習の関係を検討を行った.