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

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07780331
• Research Institution: Okayama University
• Principal Investigator: 西崎 真也 岡山大学, 大学院・自然科学研究科, 助手 (90263615)
• Keywords: リフレクション / ラムダ計算 / 型理論 / 型推論

Research Abstract

本研究では、リフレクションのうちで、よい数学的構造をもつものに着目し、「構造化されたリフレクション」というものを考察し、それを備える型理論を設計することを本研究の目的とした。そしてさらに、リフレクションを備える型理論の知識表現、例えば、自然言語意味論、エキスパートシステム、ルールベースの離散シミュレーションなどの実践的なソフトウェアへの応用も考察しインプリメンテーションを試みることを計画した。
研究発表や印刷公表された実績としての第一のものとしては、「シャド-イング機構をもつ環境λ計算の型推論」があげられる。これは、束縛変数のスコープをシャド-する(さえぎる)場合に対応するための機構を拡張した環境λ計算についての型体系および型推論アルゴリズムの研究である。この成果により、「構造化されたリフレクション」の代表的なものであるファーストクラスな環境の実用化へ大幅に近付けたものといえる。
他に、「構造化されたリフレクション」の周辺分野である研究についても前進があった。具体的には「平面グラフの形式化」、「図的対象に関する証明検証システムのためのグラフィカル・ユーザー・インターフェース」、そして「ウイルスの遺伝子機構の計算機シミュレーション」などがあった。これらの周辺分野の研究により「構造化されたリフレクション」の研究活動に関して、さまざまな洞察を得ることができ、一層、研究を前進した。
また、ソフトウェアのインプリメンテーションについても、いくつかのプロトタイプシステムをインプリメントし、多様な知見を得ることに成功した。

Research Products

• [Publications] Shin-ya Nishizaki et al.: "Formalization of Planar Graph" Lecture Notes in Computer Science. 971. 369-384 (1995)
• [Publications] 西崎真也 他3名: "図形対象を扱う証明チェッカのための視覚化ツール" インタラクティブシステムとソフトウェア. 83-92 (1995)