Subrecursive Realizability Interpretation for Intuitionistic Arithmetic

点击翻译按钮获取中文摘要

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 onanalyzing 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.