| Project/Area Number |
23K28036
|
|---|
| Project/Area Number (Other) |
23H03346 (2023)
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund (2024)
Single-year Grants (2023) |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
Basic Section 60020:Mathematical informatics-related
Sections That Are Subject to Joint Review: Basic Section60010:Theory of informatics-related , Basic Section60020:Mathematical informatics-related
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
河村 彰星 京都大学, 数理解析研究所, 准教授 (20600117)
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
木原 貴行 名古屋大学, 情報学研究科, 准教授 (80722701)
|
|---|
| Project Period (FY) |
2024-04-01 – 2028-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥18,460,000 (Direct Cost: ¥14,200,000、Indirect Cost: ¥4,260,000)
Fiscal Year 2027: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2026: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2025: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2024: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2023: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
|
|---|
| Keywords | 計算可能解析学 / 厳密実数計算 / 計算複雑さ / プログラム抽出 |
|---|
| Outline of Research at the Start |
計算可能解析学に関して，内外の研究者との共同研究を通して，実数の表現，計算的構造を表す位相概念と複雑さの階層，連続性を扱う論理とその証明からのプログラム抽出，微分方程式の計算理論，実数プログラムの検証，連続な空間の近似が持つ組み合わせ的な構造，高階計算の計算複雑性など，様々な側面から研究を行い，連続な空間の計算的構造の解明と，それに基づく連続体上の厳密計算のシステムの構築を目指す。
|
| Outline of Annual Research Achievements |
・プログラム抽出を可能とする厳密実数計算ライブラリAERNを基に，実行効率の高いHaskellプログラムの抽出を特徴とする CAERNライブラリを開発した。また，Taylorモデルおよび冪級数の理論のCoqによる形式化を行い，常微分方程式の数値解に応用することにより，任意精度で解軌道を求めるプログラムの抽出を可能とした。さらに，物理シミュレーションへの応用に向けて厳密実数計算に基づく常微分方程式の数値解法を最適化し、加速器物理における粒子運動の高精度な追跡問題の誤差保証付きの解を効率的に計算できることを示した。
・表現空間の圏における算術的階層の研究を行い，古典Σ^0_2-完全集合の自然な例たちが，この文脈では多対一同値でないことを明かした．その具体例として，古典Σ^0_2-完全問題である，自然数列の収束性判定，有界性判定，グラフの不連結性判定，全順序の非稠密性判定が，表現空間の圏では，多対一還元の真上昇列を与えていることがあげられる。また，連続時間確率過程について距離時相論理の観点からの研究を行い，特に距離時相論理式によって定義可能な事象の可測性に対する貢献をした。
・恒常的な仕事のスケジューリング問題である「輪番割当」「竹叢伐採」について、仕事の頻度を離散値から連続値へ拡張する新たな論法などを用いて、従来よりも多くの場合に効率的な割当を行うアルゴリズムを得た。
・層構造を持つフラクタル・イマジナリーキューブの2次元射影に関して，射影像が正の面積を持つかどうかが，射影方向の代数的性質により特徴付けされることを示した。また，ある種のセル・オートマトンが極限でみせるフラクタル構造について，状態に定義される不変量の観点から考察をおこなった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
厳密実数計算のプログラム抽出，表現空間の圏における算術的階層などの分野で有意義な結果を出し，招待講演やチュートリアルを通じて多くの研究者と知見を共有することができた。
|
| Strategy for Future Research Activity |
来期は，9月に CCA2025 (Twenty-Second International Conference on Computability and Complexity in Analysis) を京都で開催する。また，Autumn School Proof and Computation 2025 での講演も予定されている。内外の研究者との交流を活発に行い，これからの研究の礎になるものにしたい。述語論理に基づくプログラム抽出体系である IFP やそれを並列プログラムに拡張した CFP についての研究を深め，これらが用いる余帰納法とフラクタル図形との関係について考察を深めたい。
|
