| Project/Area Number |
18650003
|
|---|
| Research Category |
Grant-in-Aid for Exploratory Research
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
八杉 満利子 Kyoto Sangyo University, 理学部, 教授 (90022277)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 聡 京都産業大学, 理学部, 教授 (70234820)
林 晋 京都大学, 大学院・文学研究科, 教授 (40156443)
|
|---|
| Project Period (FY) |
2006 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2007: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2006: ¥1,500,000 (Direct Cost: ¥1,500,000)
|
|---|
| Keywords | 極限再帰性 / 実効的一様位相 / セミ古典論理 / ゲーム意味論 / バックトラック / 必勝法 / 変換意味論 / 有限基底定理 / 極限再帰関数 / ゲームセマンティックス / ゲームサイトセマンティックス / 構成的論理体系 / カット・三段論法 / バックトラッキング / ゲーム・ソフトウェア |
|---|
| Research Abstract |
当研究は、極限再帰関数を計算アルゴリズムとして許容する数学の実装とその応用を最終目標とし、その目的に都合のよいセミ古典論理(構成的論理に極限操作に対応する排中律を加えた体系)のゲーム意味論の完成およびその実装を目指した。実際には実現子による解釈も目的達成に有効であることが分かった。昨年度に1-バックトラック・ゲームの実装を二通りの方法で、教育的配慮も含めて行った(小林、林)。今年度はその改良および応用のための裏づけになる理論の改良と、実際の数学における極限再帰関数の使用例の詳細な分析を行った。理論的には、1、解析学における計算可能性問題で極限再帰性と実効的一様位相が同値な役割を果たす自然な条件を求め(八杉)、2、実効的一様位相の典型例であるFine位相上の解析学(収束、積分など)の展開(森・辻井(研究協力者)、八杉)、3、ゲーム意味論の整備(小林、林)、4、セミ古典論理の新しい変換意味論の開発(小林)が行われた。実装については昨年度の実装の手直しと応用実験が行われた。実際の数学で極限再帰性の原理を用いている典型例として、Hilbertの有限基底定理の最初の証明の詳細な分析を行った(林、八杉)。以上で研究目的はほぼ達成した。今後の課題としてゲーム意味論の実装の改良と論理学の教育現場への応用、変換意味論の実装、解析学における計算可能性の計算機上での実現などがあるが、当研究成果の基盤の上に逐次実現してゆくことが予期される。
|
