|
本研究は、関数型プログラミングにおける計算量制御のためのフレームワークを線形論理のアイデアに基づいて実現することを最終目標としている。そのための具体的な課題として、次の2点を挙げた。
1.形論理の乗法部分体系MLLとプール回路の正確な関係を確立する。
2.形論理の部分体系であり、多項式時間関数を特徴付ける論理として知られている軽論理を、ラムダ計算や既存の関数型プログラミング言語に対する型システムとして見る見方を確立する。
それぞれについての本年度の成果は以下の通りである。
1.LLにおける正規化手続(プログラム実行)をプール回路により効率的にシミュレートする方法を考した。またMLLにおける証明の深さと入力数制限なしのプール回路の深さが正確に対応することを示し、それによりMLL正規化手続の計算量に対する精密な特徴づけを得ることができた。
2.論理はあまりにも複雑であり、そのままの形ではラムダ計算に対する型システムとしては有用でないため、軽論理を大きく単純化し、ラムダ計算とより精密に対応する論理体系を考案した(対軽論理)。そして対軽論理により型がつけられるラムダ計算のプログラムは多項式時間で実行できることを証明した。これは軽論理についてはそのままでは成り立たない重要な性質である。また、軽論理に基づく型推論の第一歩として、軽論理を包含する初等(命題)論理についての型推論のアルゴリズムを考案した。初等論理の型推論についてはこれまでにも研究がなされてきたが、本研究で与えたアルゴリズムはそれらよりもはるかに単純であり、なおかつ多項式時間で実行可能である。ラムダ計算のプログラムに初等論理の型がつけられるならば、そのプログラムは初等時間(超指数関数時間)で実行可能である。しかも型がつけられるかどうかは、本研究の成果により、いまや多項式時間で判定可能である。これは型推論に基づく計算量の制御という当初の目的の実現へ向けた第一歩であるといえる。
|
