Budget Amount *help 
¥1,500,000 (Direct Cost : ¥1,500,000)
Fiscal Year 2000 : ¥500,000 (Direct Cost : ¥500,000)
Fiscal Year 1999 : ¥500,000 (Direct Cost : ¥500,000)
Fiscal Year 1998 : ¥500,000 (Direct Cost : ¥500,000)

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 CurryHoward 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. 平成9年度から平成12年度にわたる4年間でいくつか重要な成果・知見を得ることができたが、一方目標を実現するために多くの分野(構成的数学・数理論理学・計算可能性理論・計算の複雑さ理論など)にまたがる成果・知見をどのような視点からどのように統合し、体系的な理論としてまとめあげるかという難しい問題が今後の課題として残されてしまった。
