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

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

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