| 研究課題/領域番号 |
21K11750
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 新潟大学 |
|---|
研究代表者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2023年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2022年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2021年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | 正規形 / 項書き換えシステム / UNC性 / NFP性 / UNR性 / 合流性 / 項書換えシステム / 一意正規形性 / 自動検証 / 計算モデル |
|---|
| 研究開始時の研究の概要 |
論理学と計算機科学に基づいて，ソフトウェアやその計算を厳密に取り扱うことを目指して，項書き換えシステムとよばれる等式推論に基づく計算モデルについて研究を行います． 等式推論は人が馴染みやすい推論方法であるばかりでなく，場合によっては，リダクションによって効率的な推論が可能です． 等式推論とリダクションの対応をとるためには非決定的な計算を考える必要あります．非決定的な計算においては答えが1つとなるとは限らないので，計算解の一意性を保証することが重要になります．本研究計画では項書き換えシステムが，(どのような意味で)計算解の一意性を保証するかを自動的に検証する手法を研究します．
|
| 研究成果の概要 |
本研究は，項書き換えシステムとよばれる論理と計算を融合した計算モデルに関する研究になります．項書き換えシステムにおいては，論理と計算の両方の面から等式変形を捉えるために，非決定的な計算が採用されています．このため，計算の解がどのような場合に一意的に得られるかという問題は，さまざまな項書き換えシステムの検証技術等において基本的な問題として立ち表われます．本研究の主な成果の1つは，計算解の一意性を保証する性質の1つである，簡約に関する一意正規形性(UNR性)について，決定不能クラスや検証手法を与えたことです．
|
| 研究成果の学術的意義や社会的意義 |
本研究は，項書き換えシステムとよばれる論理と計算を融合した計算モデルに関する研究になります．項書き換えシステムにおいては，論理と計算の両方の面から等式変形を捉えるために，非決定的な計算が採用されています．このため，計算の解がどのような場合に一意的に得られるかという問題は，さまざまな項書き換えシステムの検証技術等において基本的な問題として立ち表われます．本研究の主な成果の1つは，計算解の一意性を保証する性質の1つである，簡約に関する一意正規形性(UNR性)について，決定不能クラスや検証手法を与えたことです．
|
