2000 Fiscal Year Final Research Report Summary
Subrecursive Realizability Interpretation for Intuitionistic Arithmetic
| Project/Area Number |
09640253
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
ISHIHARA Hajime Japan Advanced Institute of Science and Technology, School of Information Science, Associate Professor, 情報科学研究科, 助教授 (10211046)
|
|---|
| Project Period (FY) |
1997 – 2000
|
| Keywords | constructive arithmetic / subrecursive functions / realizability interpretation |
|---|
| Research Abstract |
Investigating computability and complexity in mathematics has been forming an interdisciplinary research area involving computer science and mathematics, and will be an important research area within a century since mathematics provides science and engineering with basics and rapid progress of information technology in our society will force computer science to make the basics computable. Especially constructive mathematics will play an important role in the area, as the Curry-Howard correspondence, that is "Proofs as Programs", holds in constructive logic.
The project started with the aim of clarifying problems on
analyzing computational complexity of extracted programs by realizability interpretation for constructive (intuitionistic) arithmetic ;
characterizing arithmetical systems from which we can extract programs in certain complexity class, for example the class of polytime computable functions,
and then finding solutions for the problems. Although during the period of the project, we could have some important results on the subject, including a nice characterization of polytime functions, we have left a difficult problems of how to integrate these results spreading over varieties of fields, for examples constructive mathematics, mathematical logic, computability theory, computational complexity and so on, into a systematic theory.
|
