【研究分野】情報学基礎

【研究領域課題番号】19500008 (KAKENデータベースで見る）

【研究キーワード】

ラムダ計算 / 圏論 / 型理論 / ソフトウェア学

【研究成果の概要】

圏論に基づいた新しい計算体系の研究を行った。プログラミング言語の基礎となる計算体系であるラムダ計算と、数学の基礎理論である圏論との関連は古くから知られている。当研究は、圏論を計算体系として再構成することで、数学的に確たる基盤をもった計算体系を構築することを目的とした研究の一環である。特に古典的リニア・カテゴリ上に計算規則を導入した体系を考案し、その性質の研究を行った。

【研究種目】基盤研究(C)

【研究期間】2007 - 2008

【配分額】1,690千円 (直接経費: 1,300千円、間接経費: 390千円)

【研究分野】数学一般(含確率論・統計数学)

【研究領域課題番号】09440072 (KAKENデータベースで見る）

【研究キーワード】

論理構造 / 計算論 / 型理論 / 形式算術 / 2階算術 / 逆数学 / 限定算術 / ラムダ計算 / ロジック / 証明論 / 算術のモデル / 数学基礎論

【研究成果の概要】

本研究の実施計画に従って,研究代表者と研究分担者は相互に緊密な連絡を取り合い,また研究集会での発表や討論を通して,算術と計算の論理構造に関する研究を行った.主な研究成果を研究者毎にまとめると、以下の通りである。
田中一之は,数学の定理を証明するのにどれくらい複雑な集合が必要かという問題(逆数学)を研究した.逆数学においてとくに重要とされる2階算術の体系WKL_0に対して,その可算モデルの性質を分析することで,山崎武らと共に新しいメタ定理を得た.赤間陽二は,計算の停止性の概念に興味を持ち,関数型言語から派生する値呼びλ計算,名前呼びλ計算,Turnerのλ計算などにおいて,停止性を持つ項の特徴づけを行った.また,組合せ論理に対する型理論を導入し,組合せ論理の停止性を持つ項を特徴づけた.宝来(高橋)正子は,高階論理体系と高階型理論の関係を研究した.また,自由構造上の計算可能性とλ表現可能性について考察した.安本雅洋は,限定算術(Bounded arithmetic)の超準モデルMのブール値拡大M^B,およびgeneric拡大M[G]の構造に関する研究を行った.龍田真は,D-正規証明の概念を提案し,この概念を用いて構成的命題論理における正規証明の唯一性に関して次の結果を示した.(1)βηD-正規証明は唯一である.(2)PNN条件を満たす論理式のβη-正規証明は唯一である.(3)BCK論理における極小論理式のβη-正規証明の唯一性の別証明を与える.長谷川立は,解析関手の理論計算機科学への応用を研究した.鹿島亮は,含意のみを論理記号とするrelevant logicの証明論および意味論の研究でいくつかの重要な成果を得た.

【研究種目】基盤研究(B)

【研究期間】1997 - 1999

【配分額】13,900千円 (直接経費: 13,900千円)

【研究分野】知能情報学

【研究領域課題番号】07780331 (KAKENデータベースで見る）

【研究キーワード】

リフレクション / ラムダ計算 / 型理論 / 型推論

【研究成果の概要】

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

【研究種目】奨励研究(A)

【研究期間】1995

【配分額】900千円 (直接経費: 900千円)