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

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

• 批准号: 19K11891
• 负责人: 菊池 健太郎
• 金额: $ 2.33万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19K11891/
• 关键词: 書き換えシステム; プログラム検証; 帰納的定理; 合流性; 局所十分完全性

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

在研究期的第一年发表的一篇论文表明，连接和局部足够的足够对于应用潜在诱导方法至关重要，这是诱导定理的证明。今年的研究获得了以下结果和有关这些特性的知识。 （1）两年前家庭协会宣布的名称改写的交界处的组成部分已经完成，并且完成了未完成的主题和定理的证明，并宣布将其作为论文宣布为论文。特定的内容是，使用Alpha等价的兼容性概念被介绍给使用原子变量的重写规则定义的名义重写系统，并且它用于使用它来使用它。交界处。当重写规则之间存在重叠时，这种情况是适用的，并且比两年来国际会议上宣布的条件更大的范围。 （2）关于当地的足够，以更改上一年国际会议上宣布的判断程序，并确定与实际功能编程语言更接近一楼的系统中的类似属性。用作程序。此外，我们对相关现有的研究方法进行了一项调查，例如基于一楼的替换系统以及确定功能编程语言的生动性的方法。通过这些知识获得的知识对于开发具有类型变量和高地板功能的编程语言程序的验证方法很重要。

项目成果

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)
• 作者: Tomoki Shiraishi;Kentaro Kikuchi;Takahito Aoto
• 通讯作者: Takahito Aoto

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

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)
• 作者: 可児冬弥;瀬戸信明;市原英行;岩垣剛;井上智生;Kentaro Kikuchi
• 通讯作者: Kentaro Kikuchi

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

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

• 发表时间: 2021
• 作者: 山上隼司;菊池健太郎;上野雄大;大堀淳
• 通讯作者: 大堀淳

名目書き換えにおける強可換性を用いた合流性証明

在名义重写中使用强交换性的汇合证明

• 发表时间: 2020
• 作者: 山上隼司;菊池健太郎;上野雄大;大堀淳;菊池健太郎
• 通讯作者: 菊池健太郎