1998 Fiscal Year Annual Research Report
| Project/Area Number |
09640248
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
寳来 正子 東京工業大学, 大学院・情報理工学研究科, 教授 (00015588)
|
|---|
| Keywords | 型理論 / 証明論 / 高階理論 / ラムダ計算 / 原始帰納法 / 自由代数 |
|---|
| Research Abstract |
図書“Theories of Types and Proofs"は,1997年9月に東京工業大学で行われた同名の国際研究集会(日本数学会第2回リージョナルワークショップ)におけるいくつかの連続講義の講義録と,この分野の専門家でない読者のために用意された入門的な章から成る単行本であり,全体として型理論と証明論の関係について基礎から最新の結果までを丁寧に解説している.
研究論文 ′A primer on proofs and types′は,上記図書の最初の章として,型理論と証明論のエッセンスを,この分野の専門家でない数学者にも理解できるよう分かり易くまとめ,いくつかの新たな知見を加えて発表した論文である.はじめに, 19世紀後半に始まる数理論理学(数学の一分野としての論理学)の歩みを振り返り, 「論理体系」の仕組みとその数学的な意味と重要性について論じ,次いで「計算体系」の仕組みとその性質,および前二者の拡張としての「型理論」の仕組みとその性質について述べ,三者の間の関係を明らかにしている.特に,高階論理体系と高階型理論の関係については,これまで不自然な部分が残されていたが,従来のものとは異なる(自然な)高階論理体系を新たに導入することにより,両者の関係を明瞭にすることができた.
研究論文 ′Lambda-representable functions over free structures revisited′は,多くの型理論の中で最も基本的かつ重要な体系である「単純型理論」を取り上げ,その表現力を考察している.具体的には,この体系で表現可能な自由代数上の関数全体のクラスに対する二つの(帰納関数論的な)特徴付けを与えている.この種の研究はこれまでにも二三知られているが,本論文の特徴は,議論の対象をまず自由代数上の関数から項代数(open term algebra)上の関数に拡張し,後者に対する特徴付けを得た後,その結果をもとに,自由代数上の関数に関する上記の結果を得たことで,そのために全体の議論を見通しよく進めることができた.
|
-
[Publications] Masako Takahashi: "A primer on proofs and types" Thcories of Types and Proofs(MSJ-Memoirs). Vol.2. 1-44 (1998)
-
[Publications] Masako Takahashi--: "Lambda-representable functions over free structures revisited" Proc.3rd Fuji Int.Symp.on Functional and Logic Programming. 1-19 (1998)
-
[Publications] Masako Takahashi, et al.(eds.): "Theories of Types and Proofs(MSJ-Memorirs)" 日本数学会, 259 (1998)
