久馬栄道の数学のホームページへようこそ

ホームに戻ります

さてラムダ計算に「型」の理論を付けたものの型の部分は、「直観主義論理」と 呼ばれるものと同等であることがわかっている。 直観主義論理というのは、普通に数学を展開する論理から「背理法」に 相当する部分を除いたものである。
このようにすると、数学の中で存在を証明する定理は本当に具体的に 存在するものを作ってやらなければならなくなる。 このようなものを「構成的数学」という。 構成的数学はコンピュータなどの上に数学を展開するのにはたいへん 適しているので、現在では広く研究されている。
論理を普通の論理から直観主義論理に変更すると「背理法」が 使えないわけであるから随分と弱い体系になるように思われるが、 普通の公理的集合論において論理だけ直観主義論理にしたものは、 普通の公理的集合論と相対的無矛盾性(つまり片一方が無矛盾ならもう 片一方も無矛盾)がいえることがわかっている。 しかしながら普通の公理的集合論の公理の中には「構成的」とはいえないものも あるので、それらを構成的な公理に変えてやると相対的無矛盾性はいえなくなる。 このような集合論を「構成的集合論」という。

さて私の修士論文の

さて構成的数学には「マルコフ原理」といわれるものを認めるか 認めないか２つの立場があるが、私の

型付きラムダ計算の型を拡張して直観主義論理を普通の背理法のある論理に することができる。

最近の研究テーマはラムダ計算を「計算量の理論」と結び付けることである。 計算量の理論というのは、コンピュータで何か計算するときに、 単にアルゴリズムがあれば計算できるとはせずに、その計算時間やメモリーの 量も考慮に入れて計算できるとはどういうことかを考える理論である。

計算量の理論において重要なものにブール回路というものがあるが、

さて計算量の理論でもっとも重要な多項式時間計算可能な決定問題という ものは Bounded Arithmetic というもので表現できることが広く知られているが、 その場合に limited iteration の使用が何回も許された。

計算量の理論では自然数を２進展開した長さが本質的である。