2022 Fiscal Year Annual Research Report
Combinatorial and computational structures of approximations of spaces
| Project/Area Number |
15K00015
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| Project Period (FY) |
2015-04-01 – 2023-03-31
|
| Keywords | プログラム抽出 / 並列計算 / 実現可能性解釈 / 余帰納法 / グレイコード |
|---|
| Outline of Annual Research Achievements |
今年度のはじめに，ESOP で，CFP (Concurrent Fixed Point Logic) に関する研究発表を行った。また，CFP の数学的な問題への応用，IFP を拡張した体系のCoq 上での実装，および，induction/coinduction とフラクタルの関係について研究を行った。CFP は，並列処理プログラムの抽出が可能な準構成的な論理である。CFPの証明から，ガウス消去法に基づき，並列的に逆行列を求めるプログラムを抽出する手法に関して論文にまとめた。フラクタルは最大不動点を用いて定義されるため余帰納法と密接な関係があり，また，その性質を証明するのに帰納法がよく使われる。シェルピンスキー四面体，および，それと関係したフラクタル立体 Fractal H および Fractal T に対して，それらの射影が正の面積を持つ方向を特定し，その証明の中で整礎帰納法を用いた部分を， IFP を拡張した体系で形式化し，その Coq 上での実験的な実装を用いて，面積を持たない有理的な方向に対し，面積を持たないことの理由になる重複場所を出力するプログラムの抽出を行った。
期間を通して，共同研究者らとともに，グレイコードという実数の近似のもつ組み合わせ的な構造を利用した部分的な表現を足がかりにして，準構成的論理体系における証明から非決定的な計算を行うプログラムを抽出する研究を主に行ってきた。その結果，IFP および CFP という体系と，それらにおいて実現可能性解釈を用いて証明からプログラムを抽出する枠組みを構成することができ，それらを論文にまとめ，また，その一部を実装した。
|
