| Project/Area Number |
09440072
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | TOHOKU UNIVERSITY |
|---|
Principal Investigator |
TANAKA Kazuyuki Grad. School of Science, Tohoku Univ., Prof., 大学院・理学研究科, 教授 (70188291)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KASHIMA Ryo Grad. Sc. of Info. Sci. and Eng., Tokyo Inst. Tech., Lec., 大学院・情報理工学研究科, 講師 (10240756)
HORAI Masako Grad. Sc. of Info. Sci. and Eng., Tokyo Inst. Tech., Prof., 大学院・情報理工学研究科, 教授 (00015588)
AKAMA Yohji Grad. School of Science, Tohoku Univ., Assoc. Prof., 大学院・理学研究科, 助教授 (30272454)
HASEGAWA Ryu Grad. School of Math. Sci., Univ. of Tokyo, Assoc. Prof, 大学院・数理科学研究科, 助教授 (20243107)
TATSUTA Makoto Grad. School of Science, Kyoto Univ., Assoc. Prof, 大学院・理学研究科, 助教授 (80216994)
廣川 佐千男 九州大学, 大型計算機センター, 教授 (40126785)
安本 雅洋 名古屋大学, 大学院・多元数理科学研究科, 助教授 (10144114)
菊池 誠 神戸大学, 大学院・自然科学研究科, 助手 (60273801)
|
|---|
| Project Period (FY) |
1997 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥13,900,000 (Direct Cost: ¥13,900,000)
Fiscal Year 1999: ¥3,800,000 (Direct Cost: ¥3,800,000)
Fiscal Year 1998: ¥4,200,000 (Direct Cost: ¥4,200,000)
Fiscal Year 1997: ¥5,900,000 (Direct Cost: ¥5,900,000)
|
|---|
| Keywords | logical structures / theory of computation / type theory / formal arithmetic / second order arithmetic / reverse mathematics / bounded arithmetic / lambda calculus / ロジック / 証明論 / 算術のモデル / 数学基礎論 |
|---|
| Research Abstract |
K. Tanaka studied along the program of reverse mathematics how much of set theory is needed to prove a theorem of ordinary mathematics. By observing properties of countable models of WKL_0, he proved (jointly with T. Yamazaki and S. Simpson) new conservation results of WKL_0 over RCA_0. Y. Akama introduced an intersection typing system for combinatory logic, and showed that it is sound and complete for the class of partial combinatory algebras. M. Horai has shown that the Curry-Howard isomorphism between higher-order intuitionistic logic and calculus of constructions can be better formulated when a modified version of higher-order type theory is introduced. She also studied the lambda-representability of functions over free structures with respect to the simple type system, as well as the notion of recursive functions over free-structures. M. Tatsuta investigated realizability interpretations of monotone coinductive definition. He proved, among others, that full monotone coinductive definitions are not sound while restricted ones are. R. Hasegawa studied applications of analytic functions to theoretical computer science. R. Kashima obtained several important results on relevant logic.
|
