研究課題
今年度のはじめに，ESOP で，CFP (Concurrent Fixed Point Logic) に関する研究発表を行った。また，CFP の数学的な問題への応用，IFP を拡張した体系のCoq 上での実装，および，induction/coinduction とフラクタルの関係について研究を行った。CFP は，並列処理プログラムの抽出が可能な準構成的な論理である。CFPの証明から，ガウス消去法に基づき，並列的に逆行列を求めるプログラムを抽出する手法に関して論文にまとめた。フラクタルは最大不動点を用いて定義されるため余帰納法と密接な関係があり，また，その性質を証明するのに帰納法がよく使われる。シェルピンスキー四面体，および，それと関係したフラクタル立体 Fractal H および Fractal T に対して，それらの射影が正の面積を持つ方向を特定し，その証明の中で整礎帰納法を用いた部分を， IFP を拡張した体系で形式化し，その Coq 上での実験的な実装を用いて，面積を持たない有理的な方向に対し，面積を持たないことの理由になる重複場所を出力するプログラムの抽出を行った。期間を通して，共同研究者らとともに，グレイコードという実数の近似のもつ組み合わせ的な構造を利用した部分的な表現を足がかりにして，準構成的論理体系における証明から非決定的な計算を行うプログラムを抽出する研究を主に行ってきた。その結果，IFP および CFP という体系と，それらにおいて実現可能性解釈を用いて証明からプログラムを抽出する枠組みを構成することができ，それらを論文にまとめ，また，その一部を実装した。
すべて 2023 2022 その他
すべて 国際共同研究 (1件) 雑誌論文 (1件) (うち国際共著 1件、 査読あり 1件) 学会発表 (3件) (うち国際学会 3件)
M. Benini, O. Beyersdorff, M. Rathjen, P. Schuster (eds), Mathematics for Computation
巻: - ページ: 223～250
10.1142/9789811245220_0009
