权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

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

基本信息

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

项目摘要

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

During the period of the study, the annual report table of the study shows that there is a clear explanation of the potential method of application of the information system, which is very complete in the current situation of the research period. In this year's research, we have learned about the results of the following research. (1) in the previous year, the table of the Institute of domestic Studies, the list of terms, the conditions for the establishment of confluence, the conditions for the establishment of confluence, the Theorem for the completion of the National Institute of International Studies, and the International Conference for International Cooperation. The specific content and number of messages are defined in the following rules: definition, consistency, convergence, convergence and convergence. The conditions and rules do not require any additional information. The previous year, the International Conference of the United Nations (ICC) issued a list of conditions and conditions. (2) the Bureau is very complete. In the previous year, the International Conference of the people's Republic of China (ICC) has made a decision. The first item is the first item. The number of data is very close to that of the system. It is similar to the system that determines the nature of the system. The first item, the first item, is the method of determining the generative nature of the disease, and the method of existing research. You can get the information that you need to know, and the number of people you know, the number of people you know, the number of people, the number of people.

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

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

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

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

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