2020 Fiscal Year Annual Research Report
Quantitative analysis of existential theorems of reduction systems
| Project/Area Number |
17K05343
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | ラムダ計算 / チャーチ・ロッサーの定理 / 合流性 / 並行変換 / 簡約グラフ / 隣接行列 / 簡約列 / 計算の複雑さ |
|---|
| Outline of Annual Research Achievements |
ラムダ計算や書換え系に代表される簡約システムの合流性や停止性なのど存在定理の複雑さを定量的に評価する一般的な枠組みを構築することを目指して研究を遂行した．そして，並行簡約の計算の道を帰納的に生成する圏論的なシステムを箙の観点から導入した．また，計算の道はテンソル積によりシステマチックに行列表現でコード化できた．これにより，計算の道の本数を隣接行列の計算で機械的に評価できた．この結果は，京都大学数理解析研究所講究録から出版した．加えて，計算の道をグラフとして表現した簡約グラフに関する基礎研究も行なった．V. Zilliは，Theoretical Computer Science (1984)の論文で，無限に多くのボトルネックを持つ簡約グラフに関する定理を示したが，これには反例があることを発見した．さらに，この定理の逆向きの成立も予想されていたが，これについても反例があることがわかった．この成果は，京都大学数理解析研究所講究録から富岡との共著論文として出版した．さらに，合流性を示す証明手法として知られていたZ定理を拡張した分割統治的な新手法により，ラムダ・ミュー計算の名前呼びの体系・値呼びの体系の合流性を統一的に証明することができた．この結果は，本田，中澤との共著論文としてStudia Logica(Springer)から出版された．一方では，Raymond Smullyan流の論理パズルの形式化についての研究も行った．これは，論理式を活用して数理的な対象を形式化する際に有効であると考えられる．これについては，日本数学会2020年度秋季総合分科会（熊本大学），京都大学数理解析研究所RIMS共同研究「Logic, Language, Algebraic System and Related Areas in Computer Science」において，それぞれ研究発表を行なった．
|
Research Products
(6 results)
