Feasibleな計算量クラスの数理論理学的手法による研究

本研究の主な目的は,極めて少ない計算資源で計算できる関数族についての性質を,数理論理学,特に機能的関数論あるいは算術の証明論やモデル論の手法を用いて解析することであった.これについて主に次の2点において研究成果を得た.計算の複雑さを測る尺度として論理回路がしばしば用いられる.ここでは特にある関数を計算する回路の素子の数が入力の多項式程度で押さえられるものを現実的に計算可能なものとする.通常,このような回路に更に制限を加えて新たな計算量クラスを作るわけであるが,特に回路の深さ,すなわち入力から出力に至る経路に現れる阻止の数の最大値を制限すると,より強い意味で計算可能な関数族が得られる.これまでは特にこれが入力の長さの対数多項式で押さえられるものについての研究が主であったが,本研究ではこれをより強く制限し,iterated logarithmの多項式で押さえられるものを考えた.これに関して,このような計算量クラスの再帰的定義による特徴づけを与え,更にこれらのクラスはすでに知られているグラフ到達可能性問題の計算量の下限についての結果を用いると分離が可能なことが明らかになった.一方,計算量クラスと密接な関係がある限定算術と呼ばれる弱い算術の理論では,ある命題がそこで証明可能かどうかが,主要な問題となる.これに関して多項式時間計算可能なクラスに対応するある種の2階算術理論においては,除算を定義する論理式が証明可能でないことを示した.これは従来これに関して知られているいくつかの結果の改良であり,またここで用いた手法は更に弱い算術のモデルに関する新たな問題を示唆している.

本研究の主な目的は,極めて少ない計算資源で計算できる関数族についての性質を,数理論理学,特に機能的関数論あるいは算術の証明論やモデル論の手法を用いて解析することであった.これについて主に次の2点において研究成果を得た.計算の複雑さを測る尺度として論理回路がしばしば用いられる.ここでは特にある関数を計算する回路の素子の数が入力の多項式程度で押さえられるものを現実的に計算可能なものとする.通常,このような回路に更に制限を加えて新たな計算量クラスを作るわけであるが,特に回路の深さ,すなわち入力から出力に至る経路に現れる阻止の数の最大値を制限すると,より強い意味で計算可能な関数族が得られる.これまでは特にこれが入力の長さの対数多項式で押さえられるものについての研究が主であったが,本研究ではこれをより強く制限し,iterated logarithmの多項式で押さえられるものを考えた.これに関して,このような計算量クラスの再帰的定義による特徴づけを与え,更にこれらのクラスはすでに知られているグラフ到達可能性問題の計算量の下限についての結果を用いると分離が可能なことが明らかになった.一方,計算量クラスと密接な関係がある限定算術と呼ばれる弱い算術の理論では,ある命題がそこで証明可能かどうかが,主要な問題となる.これに関して多項式時間計算可能なクラスに対応するある種の2階算術理論においては,除算を定義する論理式が証明可能でないことを示した.これは従来これに関して知られているいくつかの結果の改良であり,またここで用いた手法は更に弱い算術のモデルに関する新たな問題を示唆している.