| 研究課題/領域番号 |
17K05343
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
|
|---|
| 研究分担者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | ラムダ計算 / チャーチ・ロッサーの定理 / 簡約列 / 非初等関数 / グルジェゴルチック階層 |
|---|
| 研究実績の概要 |
ラムダ計算や書換え系に代表される簡約システムに関する停止性，合流性などの存在定理の複雑さを定量的に評価可能とする枠組みを構築することを目指した．そのために，簡約システムにおける等式の組合わせパターンとチャーチ・ロッサーの定理の合流点との依存関係，ラムダ計算に対するチャーチ・ロッサーの定理が主張する合流点に至るまでの計算ステップ数，そして式の構成子および型の制限のもとで限定された計算体系の存在定理の定量的性質の解明に向けて計算量的観点から研究を行ってきた．
特に，チャーチ・ロッサーの定理に対して，等式の長さと合流点までの計算ステップ数の上限との関係を解明した．既存研究によると，この計算ステップ数の上限はグルジェゴルチック階層のレベル5に属する帰納的関数と予想されていた．しかし，本研究の証明手法ではこの階層のレベル4に属する帰納的関数で上から押さえられることが明らかになり，上限を大幅に改善することができた．
この結果と関連する成果については，６th International Workshop on Confluence（Oxford）, 日本数学会秋季総合分科会（山形大学），京都大学数理解析研究所研究集会（証明論と証明活動），第４８回書き換え系研究集会（秋保），Second Workshop on Mathematical Logic and its Application （JSPS Core-to-Coreプログラム，金沢），及び日本数学会年会 数学基礎論分科会（東京大学）でそれぞれ研究発表を行った．
さらに，ルートヴィヒ・マクシミリアン大学ミュンヘンのHelmut Schwichtenberg教授と数回にわたり研究討議を行って，定理証明システムMinlogの有効な活用方法についての知見を得ることができた．
また，これらの研究成果は論文にまとめて学会誌に現在投稿中である．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
チャーチ・ロッサーの定理に対して，等式の長さと合流点までの計算ステップ数の上限との関係を解明した．本研究の証明手法ではグルジェゴルチック階層のレベル4に属する帰納的関数で上から押さえられることが明らかになり，上限を大幅に改善することができた．
また，Helmut Schwichtenberg教授と数回にわたり研究討議を行って，定理証明システムMinlogの有効な活用方法についての知見を得ることができた．
現時点までの研究成果を研究論文にまとめて学会誌に投稿中である．
|
| 今後の研究の推進方策 |
本研究で得られた上限の最適性について引き続き調査検討をしていく．また，様々な計算体系に対しても本手法を適用してその有効性を検証していく．そして，特に，ソートにより制限された計算体型の存在定理に関する上限を明らかにしていく．このような方策により，計算と論理の意味論的・証明論的観点から研究を横断的に推進していく．
|
| 次年度使用額が生じた理由 |
国際共同研究のために複数の国に今年度滞在する計画であり，そのために有効に活用することができる．
|
