| 研究課題/領域番号 |
16700020
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
照井 一成 国立情報学研究所, 情報学プリンシプル研究系, 助教授 (70353422)
|
|---|
| 研究期間 (年度) |
2004 – 2006
|
| 研究課題ステータス |
完了 (2006年度)
|
| 配分額 *注記 |
2,500千円 (直接経費: 2,500千円)
2006年度: 700千円 (直接経費: 700千円)
2005年度: 800千円 (直接経費: 800千円)
2004年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | 線型論理 / 関数型プログラミング / 計算量 / ラムダ計算 / 型推論 / 相意味論 / シークエント計算 / カット除去定理 / 線形論理 / プール回路 |
|---|
| 研究概要 |
申請者は、関数型プログラムの計算量制御のための一般的フレームワーク(与えられた計算資源の中で実行可能なソフトウェアを開発するためのプログラミング方法論、計算量解析法、検証理論)を実現することを最終目的として研究を進めている。
そのための第一歩として、本研究では特に線形論理の部分体系である軽論理(多項式時間関数を特徴付ける論理)をとりあげ、ラムダ計算や既存の関数型プログラミング言語(ML, Scheme等)に対する型システムとして見る立場を確立した。具体的には、前年度までの研究により、軽論理を大きく単純化し、ラムダ計算とより精密に対応する論理体系(双対軽論理)を考案した。また、双対形論理における型推論を行う多項式時間アルゴリズムを開発・試験的実装を行った。
これにより次のことが実現された。
●ラムダ計算のプログラムが与えられたとき、もしもそれに双対軽論理の型がつけられれば、そのプログラムが多項式時間で実行可能であることが数学的に保証されるしかも型がつけられるかどうかは、多項式時間で判定可能である。
本年度は、まずアルゴリズムと実装をより現実的な状況へあわせて改良し、さまざまなプログラム具体例を用いて検証試験、ベンチマークテストを行った。結果は、ある種の単純なプログラムについては高速な計算量検証が行えるというものである。適用範囲の狭さに難点があるが、それでも予備的なクイックチェックとしてはある程度の有用性が期待できる。成果は国際会議論文1件、雑誌論文1件(受理済み)の形でまとめられた。
また関連研究として、論理学の計算機科学への応用の根底にあるカット除去定理について、その成立の必要十分条件を与える前年度研究を継続し、より広範囲の論理へと拡張する研究を行った(国際会議論文1件、受理済み雑誌論文1件)。その他、論理学の普遍代数学への応用、ならびに計算量理論の論理的基礎付けのための一連の研究を行った。これらについては現在投稿準備中である。
|
