Study of Unique Normal Form Properties of Term Rewriting Systems

2023 Fiscal Year Final Research Report

• Project/Area Number: 21K11750
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Niigata University
• Principal Investigator: Aoto Takahito 新潟大学, 自然科学系, 教授 (00293390)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: 正規形 / 項書き換えシステム / UNC性 / NFP性 / UNR性 / 合流性

Outline of Final Research Achievements

This project concerns a computational model called term rewriting systems, which combines logic and computation. In term rewriting systems, in order to capture the logical aspect and the computational aspect of equational transformations, non-deterministic computation is employed in this computational model. Because of this fact, the problem of guaranteeing uniqueness of results of computation appears as a fundamental problem in various verification techniques based on term rewriting. One of main outcomes of this research project is about such a property called UNR (uniqueness of normal forms w.r.t. reduction) which guarantees uniqueness of results of computation; we have shown an undecidable class and new verification methods.

Free Research Field

プログラム理論

Academic Significance and Societal Importance of the Research Achievements

本研究は，項書き換えシステムとよばれる論理と計算を融合した計算モデルに関する研究になります．項書き換えシステムにおいては，論理と計算の両方の面から等式変形を捉えるために，非決定的な計算が採用されています．このため，計算の解がどのような場合に一意的に得られるかという問題は，さまざまな項書き換えシステムの検証技術等において基本的な問題として立ち表われます．本研究の主な成果の1つは，計算解の一意性を保証する性質の1つである，簡約に関する一意正規形性(UNR性)について，決定不能クラスや検証手法を与えたことです．