構造化されたリフレクションをもつ型理論と知識表現への応用

Research Project

Project/Area Number	07780331
Research Category	Grant-in-Aid for Encouragement of Young Scientists (A)
Allocation Type	Single-year Grants
Research Field	Intelligent informatics
Research Institution	Okayama University
Principal Investigator	西崎真也岡山大学, 大学院・自然科学研究科, 助手 (90263615)
Project Period (FY)	1995
Project Status	Completed (Fiscal Year 1995)
Budget Amount *help	¥900,000 (Direct Cost: ¥900,000) Fiscal Year 1995: ¥900,000 (Direct Cost: ¥900,000)
Keywords	リフレクション / ラムダ計算 / 型理論 / 型推論
Research Abstract	本研究では、リフレクションのうちで、よい数学的構造をもつものに着目し、「構造化されたリフレクション」というものを考察し、それを備える型理論を設計することを本研究の目的とした。そしてさらに、リフレクションを備える型理論の知識表現、例えば、自然言語意味論、エキスパートシステム、ルールベースの離散シミュレーションなどの実践的なソフトウェアへの応用も考察しインプリメンテーションを試みることを計画した。研究発表や印刷公表された実績としての第一のものとしては、「シャド-イング機構をもつ環境λ計算の型推論」があげられる。これは、束縛変数のスコープをシャド-する(さえぎる)場合に対応するための機構を拡張した環境λ計算についての型体系および型推論アルゴリズムの研究である。この成果により、「構造化されたリフレクション」の代表的なものであるファーストクラスな環境の実用化へ大幅に近付けたものといえる。他に、「構造化されたリフレクション」の周辺分野である研究についても前進があった。具体的には「平面グラフの形式化」、「図的対象に関する証明検証システムのためのグラフィカル・ユーザー・インターフェース」、そして「ウイルスの遺伝子機構の計算機シミュレーション」などがあった。これらの周辺分野の研究により「構造化されたリフレクション」の研究活動に関して、さまざまな洞察を得ることができ、一層、研究を前進した。また、ソフトウェアのインプリメンテーションについても、いくつかのプロトタイプシステムをインプリメントし、多様な知見を得ることに成功した。