| 研究概要 |
1.型理論の表現力を帰納的関数論の立場から考察する問題について以下の結果を得た. (1)はじめに,自由代数上の1階述語論理の項に対する関数に注目し,そのような関数のうち単純型理論で表現可能なものを,原始帰納法を制限する形で特徴付けることができた. (2)次にこの結果を用いて自由代数の(変数を含まない)項に対する関数に対する二つの表現定理を得た.なお,この研究の過程で, (2)の問題に対するこれまで正しいと思われていた結果の証明に重大な誤りがあることに気付き,そのことを反例をもって示した.
2.上の結果と比較する意味で,型なしラムダ計算による関数の表現可能性を,語を対象とする関数の場合について帰納的関数論の立場から考察した.すなわち,通常の(自然数を対象とする)帰納的関数の概念を,語を対象とする関数の場合に拡張し,それが,自然数によるコード化を経由して素朴な意味で「計算できる」関数の全体と一致することを示し,更に,型なしラムダ計算で表現可能な(語に対する)関数の全体とも一致することを示した.なお,この考え方をいろいろな木構造に拡張することについても検討中であり,良い見通しを得ている.
3.研究代表者は,1997年9月に"Theories of Types and Proofs"と題する国際研究集会を,日本数学会第2回リージョナルワークショップとして開催し,そこで行われたいくつかの連続講義の講義録を同名の図書として出版した.そしてその図書の最初の章として,型理論と証明論のエッセンスを,この分野の専門家でない数学者にも理解できるよう分かり易くまとめると共に,いくつかの新たな知見を加えて発表した.特に,高階論理体系と高階型理論の関係についてこれまで不自然な部分が残されていたが,従来とは異なる(自然な)高階理論体系を新たに導入することにより,両者の関係を明確にすることができた.
|
