| 研究課題/領域番号 |
21K11750
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 新潟大学 |
|---|
研究代表者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| キーワード | 正規形 / 項書き換えシステム / UNC性 / NFP性 / UNR性 / 合流性 |
|---|
| 研究成果の概要 |
本研究は，項書き換えシステムとよばれる論理と計算を融合した計算モデルに関する研究になります．項書き換えシステムにおいては，論理と計算の両方の面から等式変形を捉えるために，非決定的な計算が採用されています．このため，計算の解がどのような場合に一意的に得られるかという問題は，さまざまな項書き換えシステムの検証技術等において基本的な問題として立ち表われます．本研究の主な成果の1つは，計算解の一意性を保証する性質の1つである，簡約に関する一意正規形性(UNR性)について，決定不能クラスや検証手法を与えたことです．
|
| 自由記述の分野 |
プログラム理論
|
| 研究成果の学術的意義や社会的意義 |
本研究は，項書き換えシステムとよばれる論理と計算を融合した計算モデルに関する研究になります．項書き換えシステムにおいては，論理と計算の両方の面から等式変形を捉えるために，非決定的な計算が採用されています．このため，計算の解がどのような場合に一意的に得られるかという問題は，さまざまな項書き換えシステムの検証技術等において基本的な問題として立ち表われます．本研究の主な成果の1つは，計算解の一意性を保証する性質の1つである，簡約に関する一意正規形性(UNR性)について，決定不能クラスや検証手法を与えたことです．
|
