極限計算可能数学の計算機上の実行

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

当研究は、極限再帰関数を計算アルゴリズムとして許容する数学の実装とその応用を最終目標とし、その目的に都合のよいセミ古典論理(構成的論理に極限操作に対応する排中律を加えた体系)のゲーム意味論の完成およびその実装を目指した。実際には実現子による解釈も目的達成に有効であることが分かった。昨年度に1-バックトラック・ゲームの実装を二通りの方法で、教育的配慮も含めて行った(小林、林)。今年度はその改良および応用のための裏づけになる理論の改良と、実際の数学における極限再帰関数の使用例の詳細な分析を行った。理論的には、1、解析学における計算可能性問題で極限再帰性と実効的一様位相が同値な役割を果たす自然な条件を求め(八杉)、2、実効的一様位相の典型例であるFine位相上の解析学(収束、積分など)の展開(森・辻井(研究協力者)、八杉)、3、ゲーム意味論の整備(小林、林)、4、セミ古典論理の新しい変換意味論の開発(小林)が行われた。実装については昨年度の実装の手直しと応用実験が行われた。実際の数学で極限再帰性の原理を用いている典型例として、Hilbertの有限基底定理の最初の証明の詳細な分析を行った(林、八杉)。以上で研究目的はほぼ達成した。今後の課題としてゲーム意味論の実装の改良と論理学の教育現場への応用、変換意味論の実装、解析学における計算可能性の計算機上での実現などがあるが、当研究成果の基盤の上に逐次実現してゆくことが予期される。