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

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

本研究の目的は、プログラムの性質を形式化して論じる事のできる論理体系TIDを構成する事と、この論理体系の証明環境を計算機上に実現する事の2点である。プログラムの性質を自然な形で表現するためには、帰納的定義および余帰納的定義(coinductive definition)が不可欠である。自然数、リスト、木などのデータおよびプログラムの繰り返しは、帰納的定義により自然に形式化でき、また、ストリームに関する性質は余帰納的定義により自然に形式化できるからである。本研究では、帰納的定義をもつ論理体系EON+μ,TID_0および余帰納的定義をもつ論理体系TID_νの性質に関する研究をいっそう進め、帰納的定義を用いたプログラム合成の基礎理論を進展させた。特に、対象となるプログラム言語を、catch/throw機構に拡張した場合のプログラムの公理的意味論および強正規化可能性について考察した。並行プログラムの合成を行なうため、π計算および線型論理含むような論理体系の拡張について考察した。また、線形論理の独立論理式など線形論理の基本的性質について考察した。合成されるプログラムの計算量を調べるため、有界算術についてその表現可能関数などの基本性質を考察した。合成システムを計算機上に実現するための準備として、基礎理論である論理体系の整備を行なった。また、国内、国外の証明システムの研究をひき続き調査することにより、帰納的定義を用いたプログラム合成のための証明システムを既存の証明システム上に構築する場合の問題点について考察した。