| 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
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2023: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2022: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2021: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 正規形 / 項書き換えシステム / UNC性 / NFP性 / UNR性 / 合流性 / 項書換えシステム / 一意正規形性 / 自動検証 / 計算モデル |
|---|
| Outline of Research at the Start |
論理学と計算機科学に基づいて，ソフトウェアやその計算を厳密に取り扱うことを目指して，項書き換えシステムとよばれる等式推論に基づく計算モデルについて研究を行います． 等式推論は人が馴染みやすい推論方法であるばかりでなく，場合によっては，リダクションによって効率的な推論が可能です． 等式推論とリダクションの対応をとるためには非決定的な計算を考える必要あります．非決定的な計算においては答えが1つとなるとは限らないので，計算解の一意性を保証することが重要になります．本研究計画では項書き換えシステムが，(どのような意味で)計算解の一意性を保証するかを自動的に検証する手法を研究します．
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は，項書き換えシステムとよばれる論理と計算を融合した計算モデルに関する研究になります．項書き換えシステムにおいては，論理と計算の両方の面から等式変形を捉えるために，非決定的な計算が採用されています．このため，計算の解がどのような場合に一意的に得られるかという問題は，さまざまな項書き換えシステムの検証技術等において基本的な問題として立ち表われます．本研究の主な成果の1つは，計算解の一意性を保証する性質の1つである，簡約に関する一意正規形性(UNR性)について，決定不能クラスや検証手法を与えたことです．
|
