| 研究課題/領域番号 |
15K00015
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2023-03-31
|
| キーワード | プログラム抽出 / 非決定性 / 実数計算 / 並列計算 / 実現可能性解釈 |
|---|
| 研究成果の概要 |
空間の近似のなす組み合わせ的な構造と，それを用いた計算について研究を行った。特に，実数のグレイコードという未定義を含むコードの論理的な扱いに関連して，IFP (Intuitionistic Fixed Point Logic) および CFP (Concurrent Fixed Point Logic) という論理体系を共同研究者とともに構築し，そこにおける証明から，グレイコードを入出力する並列プログラムを抽出した。
|
| 自由記述の分野 |
理論計算機科学
|
| 研究成果の学術的意義や社会的意義 |
実数のグレイコード表現は，不定元を利用することにより離散的な構造を介さずに一意的に実数を表現したものであり，その上の計算には，非全域性や並列計算による非決定性といった実数計算の特徴的な性質が表れている。IFP / CFPは，非全域性や並列計算による非決定性について，実現可能性解釈を介して論理的に考察することを可能にしたものであり，実現可能性解釈の適用範囲を広げるとともに，並列計算の理解を深めている。
|
