1999 Fiscal Year Annual Research Report
| Project/Area Number |
09440072
|
|---|
| Research Institution | TOHOKU UNIVERSITY |
|---|
Principal Investigator |
田中 一之 東北大学, 大学院・理学研究科, 教授 (70188291)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
鹿島 亮 東京工業大学, 大学院・情報理工学研究科, 講師 (10240756)
寶来 正子 (高橋 正子) 東京工業大学, 大学院・情報理工学研究科, 教授 (00015588)
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
長谷川 立 東京大学, 大学院・数理科学研究科, 助教授 (20243107)
龍田 真 京都大学, 大学院・理学研究科, 助教授 (80216994)
|
|---|
| Keywords | 論理構造 / 計算論 / 型理論 / 形式算術 / 2階算術 / 逆数学 / 限定算術 / ラムダ計算 |
|---|
| Research Abstract |
本研究の実施計画に従って,研究代表者と研究分担者は相互に緊密な連絡を取り合い,また研究集会での発表や討論を通して,算術と計算の論理構造に関する研究を行った.また,3年分の研究成果をまとめて報告集を作成した.本年度の主な研究を研究者毎にまとめると,以下の通りである.
田中一之は,数学の定理を証明するのにどれくらい複雑な集合が必要かという問題(逆数学)を研究した.また,山崎武らと協力して,逆数学の重要な体系であるWKL_0に対し,その可算モデルの性質を分析することで,新しいメタ定理を証明した.赤間陽二は,計算の停止性の概念に興味を持ち,関数型言語から派生する値呼びλ計算,名前呼びλ計算,Turnerのλ計算などにおいて,停止性を持つ項の特徴づけを行った.また,組合せ論理に対する型理論を導入し,組合せ論理の停止性を持つ項を特徴づけた.宝来(高橋)正子は,高階論理体系と高階型理論の関係を研究した.また,自由構造上の計算可能性とλ表現可能性についても考察した.龍田真はD-正規証明の概念を提案し,この概念を用いて構成的命題論理における正規証明の唯一性に関して次の結果を示した.(1)βηD-正規証明は唯一である.(2)PNN条件を満たす論理式のβη-正規証明は唯一である.(3)BCK論理における極小論理式のβη-正規証明の唯一性の別証明を与える.長谷川立は,解析関手の理論計算機科学への応用を研究した.鹿島亮は,含意のみを論理記号とするrelevant logicの証明論および意味論の研究でいくつかの重要な成果を得た.
|
-
[Publications] 田中 一之、山崎 武: "2階算術と有界選択公理"京大数理解析研 講究録. 1096. 84-88 (1999)
-
[Publications] M.Takahashi: "Lambda-representable functions over term algebras"J.Foundations of Computer Science. 印刷中. (2000)
-
[Publications] S.Hirokawa,Y.Komori,M.Nagayama: "An application of simply eyped λ-calculus to relevance logic P-W"J.Symbolic Logic. 印刷中. (2000)
-
[Publications] R.Kashima,N.Kamide: "Substructural implicational logic including the relevant logic E"Studia Logica. 63. 181-212 (1999)
-
[Publications] M.Tatsuta: "Uniqueness of D-normal proofs"Proc. Of 7th Asian Logic Conf.. 41-42 (1999)
-
[Publications] T.Yamazaki: "Some move conservation results on the Baire category theorem"Mathematical Logic Quarterly. 印刷中. (2000)
-
[Publications] 田中一之(編): "数学の基礎をめぐる論争"シュプリンガー フェアラーク東京. 24 (1999)
-
[Publications] 森田康夫: "整数論"東京大学出版会. 284 (1999)
