| 研究課題/領域番号 |
17K00011
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2020年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2019年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2018年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2017年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 項書換え / 正規化性 / 正規化戦略 / 定理自動証明 / 完備化 / 合流性 / 自動定理証明 / 情報基礎 |
|---|
| 研究成果の概要 |
実数や無限リストなどをコンピュータ上で扱う際に必要になる技術の基礎研究を行った。そのようなデータを扱うプログラムは潜在的に停止しない関数を用いることが多く、遅延評価と呼ばれる特殊な計算方法が必要となる。本研究はプログラムを変形することで、多くの場合、最左最外書換えと呼ばれる単純な計算方法で遅延評価が可能になることを示した。またプログラムの実行の安全性を保証するためには遅延評価が停止性を持つこと（有限ステップで計算を終えること）を証明する必要があるが、それを自動的に行う手法を開発した。
|
| 研究成果の学術的意義や社会的意義 |
本研究において遅延評価の実現方法とその停止性（正規化性）を解析する枠組み・手法を構築した。遅延評価は関数型プログラミング言語のみならず、数学的な定理を証明する定理証明支援システムにおいても採用されている。実数や無限列などの数学的構造を扱う上で必須の技術であり、本研究はそれらをより良く扱うための計算・演繹機構の理論基盤、より良い自動化の枠組みを与えるための技術基盤の確立に貢献する。
|
