| 研究課題/領域番号 |
15K00015
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2019年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2018年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2017年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2016年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2015年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | プログラム抽出 / 非決定性 / 実数計算 / 並列計算 / 実現可能性解釈 / 余帰納法 / グレイコード / IFP / CFP / Amb / シェルピンスキー四面体 / Coq / Program Extraction / nondeterminism / totality / Fixed Point Logic / Adequacy / Gray code / Lattice Puzzle / コンパクト集合 / T^omega / 計算可能解析学 / 表現空間 / ボトム入り文字列 / コンパクト集合の表現 / タイリング / full-folding map / 不定元 / 余代数 |
|---|
| 研究成果の概要 |
空間の近似のなす組み合わせ的な構造と，それを用いた計算について研究を行った。特に，実数のグレイコードという未定義を含むコードの論理的な扱いに関連して，IFP (Intuitionistic Fixed Point Logic) および CFP (Concurrent Fixed Point Logic) という論理体系を共同研究者とともに構築し，そこにおける証明から，グレイコードを入出力する並列プログラムを抽出した。
|
| 研究成果の学術的意義や社会的意義 |
実数のグレイコード表現は，不定元を利用することにより離散的な構造を介さずに一意的に実数を表現したものであり，その上の計算には，非全域性や並列計算による非決定性といった実数計算の特徴的な性質が表れている。IFP / CFPは，非全域性や並列計算による非決定性について，実現可能性解釈を介して論理的に考察することを可能にしたものであり，実現可能性解釈の適用範囲を広げるとともに，並列計算の理解を深めている。
|
