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


ホームに戻ります


私の研究テーマは一貫して「ラムダ計算」というものである。 ラムダ計算というのは、アルゴリズムの記述のために考えられたものであるが、 同じくアルゴリズムの記述のために考えられたチューリング機械や 帰納的関数と比べると、はるかに単純な2つのルール(abstruct と application) だけからなる構成である。 その単純さゆえにいろいろな応用が考えられており、現在の人工知能の研究では 標準的な言語である LISP の祖先ともなっている。

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

さて私の修士論文の

Constructive Set Theory, 昭和60年3月, 静岡大学修士論文第124号
は構成的集合論の論理を普通の論理と直観主義的論理の間の論理 (このようなものは「中間論理」といい無限個あることが知られている) に変えた場合に相対的無矛盾性はどのようになるのかいろいろな場合に 調べたものである。

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

Constructive Set Theory with Markov's Principle
平成1年12月, KOBE JOURNAL of MATHEMATICS, vol.6 No.2
ではマルコフ原理をもつ構成的集合論のモデルが、普通の公理的集合論よりも かなり弱い集合論(Kripke-Platek 集合論)の上でラムダ計算を用いて 構成できることを証明した。

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

古典命題論理における Curry-Haward の対応と強停止性
平成6年, 愛知学院大学教養部紀要第41巻第3号
では、そのような型付きラムダ項の計算をどの順番で行っても必ず停止する (これを強停止性という)という非常に強い性質を証明した。

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

新しい二進木リストの処理について
平成1年3月, ソニー懸賞論文
「21世紀のコンピュータ」特別賞
においては、ラムダ計算の新しい表現方法を考案しそれをコンピュータの 上において高速で計算する方法を考案した。

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

ブール回路を表現する λ-calculus の ω-rule について
平成3年12月, 豊田工業高等専門学校研究紀要第24号
においては、ブール回路をそのサイズと ω-rule と呼ばれる性質をそのまま 保存したまま λ-calculus で表現することに成功した。

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

多項式時間計算可能な決定問題の新しい特徴付けについて
平成3年12月, 豊田工業高等専門学校研究紀要第24号
においては limited iteration の使用を1回に制限しても本質的には 同じ事を証明した。

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

型付きラムダ計算, 自然数の2進表現, 計算量の理論
平成7年, 愛知学院大学教養部紀要第43巻第1号
では型付きラムダ計算での自然数の2進数を表現する方法を考案し、 その上で多項式時間計算可能なものが計算できることを示した。
E-mail: kyuma@dpc.aichi-gakuin.ac.jp updated March 29, 1996