| 研究課題/領域番号 |
17K05343
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
|
|---|
| 研究分担者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | ラムダ計算 / チャーチ・ロッサーの定理 / グルジェゴルチック階層 / 並行変換 / 簡約列 / 計算の複雑さ |
|---|
| 研究実績の概要 |
ラムダ計算や書換え系に代表される簡約システムの停止性，合流性などの存在定理を定量的に評価する一般的枠組みを構築することを目指して研究を行なった．そして，並行簡約と逐次簡約との関係を明示的に与えることでグルジェゴルチック階層に基づく一般的枠組みを構築することができた．これは，型無しラムダ計算に限らず，ゲーデルのシステムTやジラルのシステムF，Pure Type Systemsなど型のある計算体系でも同様に有効な枠組みであることが明らかになった．
これらの研究成果の一部は，Information and Computation（Elsevier）から研究論文として出版して，オープンアクセスとした．また，Swansea大学（イギリス），Chalmers工科大学（スウェーデン）でもそれぞれ発表を行なった．
こららの結果と関連する研究成果については，第４９回書換え系研究集会（伊香保），第２１回プログラミングおよびプログラミング言語ワークショップPPL２０１９（花巻），ラムダ計算と論理の早春セミナー（草津），日本数学会２０１９年度年会（東京工業大学）においてそれぞれ研究発表を行なった．
また，Munchen大学，Swansea大学，Chalmers大学の海外研究協力者とそれぞれ複数回にわたり建設的な研究討議を行って，定理証明システム，計算量，計算体系に関する有益な知見を得ることができた．
さらに，１０年ほど前から継続して研究してきた計算モデルの束論的意味論に関して進展があり，その研究成果は研究分担者との共著論文にまとめて学会誌に現在投稿中である．また，研究実績の概要はWebページ http://www.cs.gunma-u.ac.jp/~fujita からも公開して情報発信している．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
チャーチ・ロッサーの定理に対して，簡約（reduction）と展開（expansion）の出現数の関数として合流点までの計算のステップ数の上限を一般的枠組みの中で与えることができた．
また，計算ステップ数の下限に関しては，海外研究協力者（Munchen大学）と研究討議を行って様々な知見を得ることができた．
さらに，計算モデルの束論的意味論に関しては大きな進展があり，その成果は研究分担者との共著論文としてまとめて現在投稿中である．
|
| 今後の研究の推進方策 |
本研究で得られた上限の一般的枠組みについては引き続き調査検討を重ねていく．また，計算のステップ数に限らず，計算の道の本数についてもその特徴を解析していく．
さらに，進展があった意味論的観点から計算量へのフィードバックを明らかにしていく．
これらの方策により，計算と論理の意味論的・証明論的視点から計算量を特徴付ける研究を推進していく．
|
| 次年度使用額が生じた理由 |
国際共同研究のために複数の国に滞在計画であり，そのために有効に使用できる．
|
