2002 Fiscal Year Annual Research Report
| Project/Area Number |
13480084
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
高橋 大輔 早稲田大学, 理工学部, 教授 (50188025)
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
山本 章博 北海道大学, 大学院・工学研究科, 助教授 (30230535)
|
|---|
| Keywords | 形式的証明 / 形式的技法 / 学習理論 / 極限計算 / 非構成的原理 |
|---|
| Research Abstract |
本年も数々の新知見を得たが、ここでは今年度の最大の成果はsublearning階層についてのべる。Π^0_1-LEM、Σ^0_1-LEMは学習の階層に対応する。これがLCMの基本的アイデアであり、これを形式的に上に伸ばしたΠ^0_n-LEM、Σ^0_n-LEMなどは考えていたものの、これらより下の階層、つまり、学習理論より下の階層(以下、sublearning階層)は考慮に入れなかった。
以前より、海外共同研究者、分担者のKohlenbach,石原は、これらより下、つまり、Π^0_1-LEMより下に、構成的数学でいうLLPO(Lesser Limited Principles of Ominiscience)に対応する原理があり、WKL(弱ケーニッヒの原理)と対応することを指摘してはいたが、それの計算論的・学習理論的意味は不明だった。
これがWKLのLCM階層における位置づけの研究を通して明らかになった。その結果として、1970年代末にV.Lifschitzによって発明され、後にvan Oostenによって拡張洗練された、Lifschitz-realizabilityという解釈と、この原理が対応し、しかも、この解釈は「有限個のプロセスの反証による非決定計算」という直感的で学習理論的な極限計算モデルになっていることが判明した。また、これらとKohlenbachの関数解釈、帰納関数論のLow basis theoremが密接に関係しており、sublearning階層が数理論理学の一分野である逆数学でいうWKL上の数学と、ほぼ一致することも判明した。このことにより、LCMによる証明アニメーションの適用範囲が極めて広いことが、判明し、しかも、Javaなどでアニメータが簡単に実装できる証明の範囲があり、しかも、それが述語論理の完全性定理などの多くの数学の定理の証明を含むことも判明した。また、これは同時に目的である、数学的に極めて重要な発見である。
|
Research Products
(2 results)
-
[Publications] S.Hayashi, Y.Akama: "Limit-Computable Mathematics and its Applications"Proceedings of Computer Science Logic '02. 2471. 7-21 (2002)
-
[Publications] S.Hayashi: "Mathematics based on Learning"Proceedings of Algorithmic Learning Theory '02. 2533. 1 (2002)
