研究課題/領域番号 |
17K05343
|
研究機関 | 群馬大学 |
研究代表者 |
藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
|
研究分担者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
研究期間 (年度) |
2017-04-01 – 2021-03-31
|
キーワード | ラムダ計算 / チャーチ・ロッサーの定理 / グルジェゴルチック階層 / 並行変換 / 簡約列 / 隣接行列 / 箙 / 計算の複雑さ |
研究実績の概要 |
ラムダ計算や書き換え系に代表される簡約システムの停止性や合流性などの存在定理の複雑さを定量的に評価する一般的な枠組みを構築することを目指して研究を行った.そして,箙から計算の道を帰納的に生成する形式的体系を与えることができた.この体型に基づくと,生成される計算の道は転置とテンソル積を使うことでシステマティックに行列表現に落とし込むことができる.これにより,計算の道の本数を隣接行列の行列計算で機械的に数えることができた.この結果は,Theoretical Computer Science (Elsevier)から研究論文として出版された.なお,この論文は今後オープンアクセスを予定している. さらに,高階の計算モデルと束論的意味論に関して大きな進展があり,完全な意味論を構築することに成功した.この結果を研究分担者との共著による研究論文にまとめて,Fundamenta Informaticae (IOS Press)からオープンアクセスとして出版した. これらの研究成果と関連する結果については,日本数学会2019年度秋季総合分科会(金沢大学),京都大学数理解析研究所 RIMS共同研究 「証明論とその周辺」,第52回項書換え系研究集会,日本数学会2020年度年会(日本大学理工学部,但し社会情勢のために開催は中止されたがアブストラクトは出版された)においてそれぞれ研究発表を行った. また,研究実績の概要は次のWebページ http://www.cs.gunma-u.ac.jp/~fujita/ からも公開して最新の情報を発信している.
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
簡約システムの存在定理に関する定量的性質の解明のために,これまでにチャーチ・ロッサーの定理の観点から,簡約列の長さとその道の本数を評価することができた. そして,雑誌論文6件(その内,査読付き3件),国際会議発表4件,国内学会・研究会等の発表8件を行い研究を実施してきた.
|
今後の研究の推進方策 |
本研究で得られた結果の最適性についても引き続き検証を重ねていく.そして,ゲーデルの体型など他の計算体系に対しても本手法を適用してその汎用性を確認していく. この方策により,計算と論理の意味論的観点,証明論的観点から研究を俯瞰的に推進していく.
|
次年度使用額が生じた理由 |
研究目的を精緻に達成するために,日本数学会,研究集会への参加,および研究発表を予定していた.しかし,社会情勢によりこれらの学会と研究会が中止に追い込まれた.今後の学会,研究会において当初に予定されていた研究発表を行っていく計画である.
|