Universal Algebraic Datatypes: Theory and Practice on Datatypes based on Higher-Order Rewriting

通用代数数据类型：基于高阶重写的数据类型理论与实践

• 批准号: 20H04164
• 负责人: 浜名 誠
• 金额: $ 11.23万
• 依托单位: Gunma University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20H04164/
• 关键词: ソフトウェア科学; 書換え系; 代数仕様; プログラム理論; 関数プログラミング; 書替え系; 関数プログラム; 合流性; 停止性; Haskell; ラムダ計算; ソフトウェア科学; 書換え系; 代数仕様; プログラム理論; 関数プログラミング; 書替え系; 関数プログラム; 合流性; 停止性; Haskell; ラムダ計算

本年度は学術論文誌論文2本出版の良好な成果を得た。学術論文誌Logical Methods in Computer Science誌で発表した論文では、二階書換えの停止性に関する新しいモジュラーな証明法を確立した。これは意味ラベリング手法を拡張した新規な証明方法によるものである。さらに応用として、代数的効果、エフェクトハンドラ、 エフェクト理論を持つCall-by-Push-Value計算系の停止性を証明した。これは現実の関数型言語への有用な応用である。論文誌コンピュータソフトウェア誌で発表した論文は、関数型言語Haskellのための合流性検証ツールを提案したものである。Glasgow Haskell Compiler (GHC)では、プログラマが Haskellプログラムを最適化するために書換え規則を使用することができる。これまで、GHCはユーザが定義した書換え規則の合流をチェックする方法がなかったが、本研究成果でこれを検証することができる。

今年，我们通过发表两篇学术期刊论文获得了良好的结果。计算机科学逻辑方法上发表的一篇论文建立了一种新的模块化证明方法，用于终止双阶重写。这是由于一种扩展语义标记技术的新颖证明方法。此外，作为一种应用，我们已经证明了具有代数效应，效应处理程序和效应理论的逐个呼叫计算系统的垂直性。这是对现实世界功能语言的有用应用。该论文发表在《 Journal Computer》软件上的论文提出了功能语言Haskell的Confluence验证工具。格拉斯哥Haskell编译器（GHC）允许程序员使用重写规则来优化Haskell程序。到目前为止，GHC还没有办法检查用户定义的重写规则的汇合，但是可以通过本研究的结果来验证。