先進的な高階書き換え理論に基づく遅延評価関数型プログラムの検証

基于先进高阶重写理论的惰性求值函数程序验证

基本信息

批准号：
19K11891
负责人：
菊池健太郎
金额：
$ 2.33万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2019
资助国家：
日本
起止时间：
2019-04-01 至 2024-03-31
项目状态：
已结题

项目摘要

研究期間の初年度に発表した論文により、帰納的定理の証明手法である潜在帰納法の適用のためには合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。(1) 前々年度に国内学会で発表した名目書き換えにおける合流性の成立条件について、未完成となっていた補題や定理の証明を完成させ、論文として国際会議で発表した。具体的な内容としては、アトム変数を用いる書き換え規則によって定義される名目書き換えシステムに対して、アルファ同値性を法とした強可換性の概念を導入し、それを利用して基底名目項上の書き換えが合流性を満たす条件を提示した。この条件は、書き換え規則の間に重なりがある場合にも適用可能であり、前々年度に国際会議で発表した条件よりも広い範囲をカバーするものとなっている。(2) 局所十分完全性については、前年度に国際会議で発表した判定手続きを変更して、第一階項書き換えシステムよりも実際の関数型プログラミング言語に近い体系における類似の性質を判定するための手続きとして利用できないか検討した。また、第一階項書き換えシステムや関数型プログラミング言語における生成性の判定法など、関連する既存研究の手法について調査を進めた。これらを通じて得られた知見は、型変数や高階関数を持つ関数型プログラミング言語のプログラムに対する検証手法を開発するために重要になると考えられる。

在研究期的第一年发表的一篇论文表明，汇合和局部足够的完美对于应用潜在诱导是必不可少的，这是归纳定理的证明方法。今年的研究提供了以下有关其特性的结果和发现：（1）关于未完成的引理和定理的证明，就名义重写建立汇合的条件完成了，该条件在过去两年中在日本学会上介绍，并在国际会议上作为论文介绍了这一点。具体而言，对于使用ATOM变量重写规则定义的标称重写系统，使用Alpha等效性引入了强可交换性的概念，并使用此条件根据名义子句重写标称的条款来满足汇合。即使重写规则之间存在重叠，并且涵盖比上一年在国际会议上宣布的条件更大的范围，这种情况也适用。（2）关于本地足够的完整性，我们检查了上一年在国际会议上提出的判断程序是否可以用作确定与第一个术语重写系统更接近实际功能编程语言的系统中的类似属性。我们还对现有研究方法进行了研究，例如一阶术语重写系统和用于确定功能编程语言产生的方法。通过这些发现获得的发现对于开发具有类型变量和高阶功能的功能编程语言编程程序的验证方法很重要。

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Polymorphic computation systems: Theory and practice of confluence with call-by-value

多态计算系统：按值调用融合的理论与实践

DOI：
10.1016/j.scico.2019.102322
发表时间：
2020
期刊：
Science of Computer Programming
影响因子：
1.3
作者：
Makoto Hamana;Tatsuya Abe;Kentaro Kikuchi
通讯作者：
Kentaro Kikuchi

A Proof Method for Local Sufficient Completeness of Term Rewriting Systems

术语重写系统局部充分完备性的证明方法

DOI：
10.1007/978-3-030-85315-0_22
发表时间：
2021
期刊：
Proceedings of the 18th International Colloquium on Theoretical Aspects of Computing (ICTAC 2021)
影响因子：
0
作者：
Tomoki Shiraishi;Kentaro Kikuchi;Takahito Aoto
通讯作者：
Takahito Aoto

Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting

标称重写中的接地合流和强换向模 Alpha 等价

DOI：
10.1007/978-3-031-17715-6_17
发表时间：
2022
期刊：
Proceedings of the 19th International Colloquium on Theoretical Aspects of Computing (ICTAC 2022)
影响因子：
0
作者：
可児冬弥;瀬戸信明;市原英行;岩垣剛;井上智生;Kentaro Kikuchi
通讯作者：
Kentaro Kikuchi

アトム変数を用いた名目単一化の実装

使用原子变量实现名义统一