極限計算の論理とその応用
【研究分野】計算機科学
【研究キーワード】
inductive inference / 数理論理学 / 古典論理証明実行 / 形式的証明 / 形式的技法 / 学習理論 / 極限計算 / 非構成的論理 / 非構成的原理
【研究成果の概要】
本プロジェクトでは、極限計算可能数学の基礎理論について、数多くの新知見が多く得られた。その内で大きなものは次のとおりである。
1.LCMの実現可能性解釈の完成
2.subleaning階層の発見
3.LCMゲームの発見
4.算術階層の決定
5.LCMの圏の構成
6.極限計算の概念による計算可能解析学の再検討。特に不連続関数の計算理論
7.並行計算概念に基づくDelta-0-2_写像のモデル(Berardi)。
これらの内、特に注目すべきは、sublearnig階層の発見である。LEMより下に、構成的数学でいうLLPOに対応する原理があり、弱ケーニッヒの原理と対応することが指摘されてはいたが、それの計算論的・学習理論的意味は不明だった。これがWKLのLCM階層における位置づけの研究を通して明らかになった。その結果として、「有限個のプロセスの反証による非決定計算」という直感的で学習理論的な極限計算モデルPopperian gameの存在が明らかになった。
また、このsubleaning階層も含めて、LCMの全算術階層の構造が解明されたのも特筆に値する。この決定は、多くの数理論理学的手法を使って行われており、数学的にも価値の高いものである。また、組織外の研究者の協力で、この階層によるcalibration理論の研究も進んだ。
さらに、Coquandのゲーム理論のゲームのバックトラックを、ゲーム理論的により自然なものにすると、LCMに対応するという発見も、非常に重要である。
【研究代表者】