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

1998 Fiscal Year Annual Research Report

• Project/Area Number: 09780264
• Research Institution: Kyoto University
• Principal Investigator: 龍田 真 京都大学, 大学院理学研究科, 助教授 (80216994)
• Keywords: プログラム合成 / プログラム理論 / 帰納的定義 / 実現可能性解釈

Research Abstract

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

Research Products

• [Publications] M.Tada and M.Tatsuta: "The Fuction [a/m] in Sharply Bounded Arithmetic" Archive for Mathematical Logic. 37. 51-57 (1997)
• [Publications] M.Tatsuta: "Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis" Lecture Notes in Computer Science. (1998)
• [Publications] M.Tatsuta: "Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis" Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science. (1998)
• [Publications] 龍田 真: "構成的集合の実現可能性解釈" 日本ソフトウェア科学会第15回大会論文集. 189-192 (1998)
• [Publications] 龍田 真: "構成的理論とプログラム理論" 1998年度日本数学会秋季総合分科会総合講演企画特別講演アブストラクト. 13-24 (1998)
• [Publications] 龍田 真: "構成的集合論の実現可能性とそのプログラム合成への応用" 第1回プログラミングおよびプログラミング言語ワークショップ. (1999)