| 研究課題/領域番号 |
25K07097
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 東京電機大学 |
|---|
研究代表者 |
藤田 憲悦 東京電機大学, 理工学研究科, 特別専任教授 (30228994)
|
|---|
| 研究期間 (年度) |
2025-04-01 – 2029-03-31
|
| 研究課題ステータス |
交付 (2025年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2028年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2027年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2026年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2025年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | カリー・ハワード同型 / 証明 / 計算 / 型 / Girard's Paradox |
|---|
| 研究開始時の研究の概要 |
カリー・ハワード同型を深化させて，証明と計算の相互作用の解析にフィードバックさせる．研究の核心は，計算可能性・計算量を本質的に特徴付けている基本概念は何か？という根本問題である．そのために，証明と形式化された計算の関係からこの問題を追求する．まず，型理論，論理体系，そして意味論の関係を俯瞰して，健全かつ完全な意味論を精査して計算的複雑さを解析する．並行して，カリー・ハワード同型を掘り下げて，ラムダ計算におけるプログラム変換と論理的埋め込みとの対応関係を，双対性と決定可能性の観点から分析する．これらにより証明と計算の関係の深化を図り，可解性・計算量の基本問題を一層深く追求する基礎の構築を目指す．
|
