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

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

本研究の目的は、プログラムの性質を形式化して論じる事のできる論理体系TIDを構成する事と、この論理体系の証明環境を計算機上に実現する事の2点である。プログラムの性質を自然な形で表現するためには、帰納的定義および余帰納的定義(coinductive definition)が不可欠である。自然数、リスト、木などのデータおよびプログラムの繰り返しは、帰納的定義により自然に形式化でき、また、ストリームに関する性質は余帰納的定義により自然に形式化できるからである。本研究では、帰納的定義をもつ論理体系EON+mu,TID_0および余帰納的定義をもつ論理体系TID_<0nu>の性質に関する研究をいっそう進め、帰納的定義を用いたプログラム合成の基礎論理を進退させた。特に、帰納的定義および余帰納的定義両方に対して、単調条件の下での実現可能性解釈を与えた。非可述的原理を用いた帰納的定義および余帰納的定義に対する実現可能性解釈を与えた。また、初等的集合に対するプログラム合成に適した実現可能性解釈を与えた。合成システムを計算機上に実現するための準備として、基礎論理である論理体系の整備を行なった。また、国内、国外の証明システムの研究を調査することにより、帰納的定義を用いたプログラム合成のための証明システムを既存の証明システム上に構築する場合の問題点について考察し、新しい知見を得た。