帰納的定義を用いたプログラム合成

点击翻译按钮获取中文摘要

本研究の目的は、プログラムの性質を形式化して論じる事のできる論理体系TIDを構成する事と、この論理体系の証明環境を計算機上に実現する事の2点である。プログラムの性質を自然な形で表現するためには、帰納的定義および余帰納的定義が不可欠である。自然数、リスト、木などのデータおよびプログラムの繰り返しは、帰納的定義により自然に形式化でき、また、ストリームに関する性質は余帰納的定義により自然に形式化できるからである。本研究では、帰納的定義をもつ論理体系EON_<+μ>,TIDOおよび余帰納的定義をもつ論理体系TID_<+v>の性質に関する研究をいっそう進め、帰納的定義を用いたプログラム合成の基礎理論を進展させた。特に、構成的集合の実現可能性解釈の研究を深め、無限論理を用いず、また、集合完備化プログラムと実現可能性解釈の再帰的定義を用いない解釈を与え、また、集合帰納法の原理を用いない健全性証明を与えた。また、単調余帰納的定義の実現可能性解釈について考察した。また、構成的集合と帰納的定義および余帰納的定義を含む論理体系を提案しその実現可能性解釈を与えた。また、合成されるプログラムの計算量を調べるため、有界算術についてその表現可能関数の基本性質を考察した。