1999 Fiscal Year Final Research Report Summary
Studies on logical structures of arithmetic and computation
| 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)
|
|---|
| Project Period (FY) |
1997 – 1999
|
| 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.
|
