| 研究課題/領域番号 |
09780264
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
龍田 真 京都大学, 大学院理学研究科, 助教授 (80216994)
|
|---|
| 研究期間 (年度) |
1997 – 1998
|
| 研究課題ステータス |
完了 (1998年度)
|
| 配分額 *注記 |
2,400千円 (直接経費: 2,400千円)
1998年度: 1,100千円 (直接経費: 1,100千円)
1997年度: 1,300千円 (直接経費: 1,300千円)
|
|---|
| キーワード | プログラム合成 / プログラム理論 / 帰納的定義 / 実現可能性解釈 |
|---|
| 研究概要 |
本研究の目的は、プログラムの性質を形式化して論じる事のできる論理体系TIDを構成する事と、この論理体系の証明環境を計算機上に実現する事の2点である。
プログラムの性質を自然な形で表現するためには、帰納的定義および余帰納的定義が不可欠である。自然数、リスト、木などのデータおよびプログラムの繰り返しは、帰納的定義により自然に形式化でき、また、ストリームに関する性質は余帰納的定義により自然に形式化できるからである。本研究では、帰納的定義をもつ論理体系EON_<+μ>,TIDOおよび余帰納的定義をもつ論理体系TID_<+v>の性質に関する研究をいっそう進め、帰納的定義を用いたプログラム合成の基礎理論を進展させた。特に、構成的集合の実現可能性解釈の研究を深め、無限論理を用いず、また、集合完備化プログラムと実現可能性解釈の再帰的定義を用いない解釈を与え、また、集合帰納法の原理を用いない健全性証明を与えた。また、単調余帰納的定義の実現可能性解釈について考察した。また、構成的集合と帰納的定義および余帰納的定義を含む論理体系を提案しその実現可能性解釈を与えた。また、合成されるプログラムの計算量を調べるため、有界算術についてその表現可能関数の基本性質を考察した。
|
