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

使用归纳定义进行程序综合

• 批准号: 06780224
• 负责人: 龍田 真
• 金额: $ 0.58万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1994
• 资助国家: 日本
• 起止时间: 1994 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-06780224/
• 关键词: プログラム合成; プログラム理論; 帰納的定義; 実現可能性解釈

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

The purpose of this study is to formalize the nature of the logic system, discuss the logic system TID, construct the logic system TID, prove the logic system TID, and realize the logic system TID on the computer. The nature of the plant is natural, and the definition of the plant and the coinductive definition of the plant are indispensable. Natural numbers, numbers, numbers. In this paper, the definition of the logic system EON+μ,TID_O and the definition of the logic system TID_γ are studied. To deepen the understanding of the possibility of realization under special and special conditions. The principle of non-description is to use the definition of inclusion and the definition of residual inclusion to deepen the solution of realization possibility. To deepen the understanding of the possibility of realization of a set of elementary problems Parallel logic synthesis, π computation, linear logic, logic system expansion, etc. The preparation and implementation of the logic system of the synthesis system on the computer The research on the proof system at home and abroad is carried out in the field of investigation, definition, application, synthesis and construction of the proof system.

项目成果

M.Tatsuta: "Two reulizability interpretations of monotone inductive definitioms" International Journal of Foundations of Computer Sciense. 5. 1-21 (1994)

M.Tatsuta：“单调归纳定义的两种可重构性解释”国际计算机科学基础杂志。