2020 Fiscal Year Annual Research Report
Universal Algebraic Datatypes: Theory and Practice on Datatypes based on Higher-Order Rewriting
| Project/Area Number |
20H04164
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 大学院理工学府, 准教授 (90334135)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | 書換え系 / 関数プログラム / 合流性 / 停止性 / Haskell / ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
本年度は国際学術論文誌論文1本の出版、国際会議の招待講演、コンペティション優勝の良好な成果を得た。
プログラミング言語分野の著名論文誌Science of Computer Programming誌で発表した論文では、多相型と型推論を書換系に初めて導入した多相書換系の理論を構築した。合流性検証のための危険対解析、モジュラ性といった性質の理論的証明をした。これを用いて、計算効果のある関数型言語の基礎体系である 計算的λ計算(Computational lambda-calculus)の合流性を初めて形式的に証明した。
国際会議FLOPS 2020では、二階書換え系の理論と実践についての招待講演を行なった。二階書換え系は、論理プログラミング、代数的エフェクト、量子計算などのプログラミング言語の重要な概念に適用できる有用な手法である。このような二階書換え系のフレームワークを提示し、その基礎と進化を説明した。様々なプログラミング言語の例を通して有効性を示した。
さらにツールSOLにて、国際コンペティション International Confluence Competitoin に参加した。これは参加ツールがどれだけ多くの既存問題の自動証明に成功するかの数を競うものである。ツールSOLは高階書換システム部門で優勝した。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
ツールSOLの合流性自動検証手法の改良により、国際コンペティションで優勝したことは顕著な進歩である。SOLは他の書換え系ツールでは扱えない多相型も扱えるため、関数型プログラミング言語への適用範囲が広いという特徴も持つ。またFLOPS2020における二階書換え系についての招待講演により、申請者オリジナルの体系と形式化、意味論、実装という広範囲な知見を周知できた。
|
| Strategy for Future Research Activity |
高階書換え系のモジュラ性といった基礎理論の拡充を行ない、多相高階関数型プログラミング言語への書換え手法の応用を積極的に進める。
|
