| 研究課題/領域番号 |
18650003
|
|---|
| 研究機関 | 京都産業大学 |
|---|
研究代表者 |
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
|
|---|
| 研究分担者 |
小林 聡 京都産業大学, 理学部, 教授 (70234820)
林 晋 京都大学, 大学院文学研究科, 教授 (40156443)
|
|---|
| キーワード | 極限再帰関数 / ゲームセマンティックス / ゲームサイトセマンティックス / 構成的論理体系 / カット・三段論法 / バックトラッキング / 必勝法 / ゲーム・ソフトウェア |
|---|
| 研究概要 |
当研究は、極限再帰関数を収束率などに許容する数学の実装を目標とし、その目的に都合のよい、構成的論理に極限操作に対応する排中律を加えた体系のゲームセマンティックスの完成、およびその実装を目指した。また、実践の裏づけになる理論的考察も行った。今年度の目標はほぼ達成された。ここでゲームセマンティックスは1-バックトラックを認め、論理式の正しさと必勝法の存在が同値になることを要求する。今年度の成果は以下のとおりである。Berardiの体系を制限のない算術の体系に拡張し、その1-バックトラックゲームによるセマンティックスを与え、JavaScriptによって実装した(小林)。分かりやすい仕様になっていて、論理の教育用にも適している。また、"ゲームサイトセマンティックス"という着想を得て、2人ゲームでなく、ゲームサイトが必要に応じてプレーヤーをアサインしてくれるゲームとして定義し、そのプログラムを作成した(林)。このプログラムもゲームをしやすく、また論理を表に出さずに一般的なゲームの概念で説明できるために、教育的効果が期待される。限定された論理式についてのカットルールをもつ体系に対する必勝法の存在証明にも成功した(研究協力者 山形)。
この研究課題の理論的背景は、実数上の不連続関数の計算問題と、極限学習を必要とする証明のアニメーションであり、当課題と対になっている基盤研究B(16340028)によって基礎付けられている(林、八杉)。
上記の実装を基にこれらの問題を計算機上で実現すべく、その仕様を作成しつつある(林、八杉)。来年度はこの実現によって最終目標を達成する計画である。
|
