2005 Fiscal Year Annual Research Report
| Project/Area Number |
16700020
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
照井 一成 国立情報学研究所, 情報学基礎研究系, 助手 (70353422)
|
|---|
| Keywords | 線型論理 / 関数型プログラミング / 計算量 / ラムダ計算 / 型推論 / 相意味論 / シークエント計算 / カット除去定理 |
|---|
| Research Abstract |
本研究は、関数型プログラムの実行時間を検証するためのフレームワークを線形論理のアイデアに基づいて実現することを最終目標としている。そのための具体的な課題の一つとして次のものを挙げていた。
●線型論理の部分体系であり、多項式時間関数を特徴付ける論理として知られている軽論理を、ラムダ計算や既存の関数型プログラミング言語に対する型システムとして見る見方を確立する。
前年度の研究において、(1)軽論理を大きく単純化し、ラムダ計算とより精密に対応する論理体系を考案した(双対軽論理)。(2)また軽論理と密接に関係する初等命題論理について多項式時間で型推論を行うことができるアルゴリズムを考案した。本年度は当初の予定通り、
●(1)の型推論アルゴリズムを拡張し、(2)の双対軽論理についても多項式時間で型推論を行うことができるアルゴリズムを開発した。また試験的実装を行った。
結果として、次のことが言える:
●ラムダ計算のプログラムが与えられたとき、もしもそれに双対軽論理の型がつけられるならば、そのプログラムが多項式時間で実行可能であることが数学的に保証される。しかも型がつけられるかどうかは、多項式時間で判定可能である。
これにより、(未だ実用段階ではないとはいえ)与えられたプログラムがリーズナブルな時間で実行可能であることを検証するための一つの理論的フレームワークが得られたといえるだろう。上記結果をまとめた論文は現在投稿中である。
その他に、(1)我々のアプローチの源泉である線型論理について、直感主義相意味論が古典的相意味論と「ほとんど同じ」であることを示す研究を行った。また、(2)論理学の計算機科学への応用の根底にあるカット除去定理について、さまざまなシークエント計算においてそれが成り立つための必要十分条件を与えた。両者は雑誌論文として発表された。
|
