構成的論理体系における仕様記述と証明作成に関する研究

1993 Fiscal Year Annual Research Report

• Project/Area Number: 05780221
• Research Institution: Tohoku University
• Principal Investigator: 亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000)
• Keywords: 構成的プログラミング / 証明 / 帰納的述語定義 / 仕様記述

Research Abstract

構成的プログラミングは、構成的な論理体系において、仕様を表す論理式を証明することにより、プログラムを作成するプログラミング・パラダイムである。この手法は、プログラムの正当性が保証される反面、仕様記述が容易でないという欠点もある。人間の仕様記述は曖昧さを持つものであるため、これを機械的に仕様を表す論理式に変換することはできない。そして、本研究は、人間にとって書きやすい形式の仕様記述から、構成的プログラミングをおこなう手法を確率することを目的とした。
最初に、仕様記述のための論理体系を設計した。この体系は、構成的に1階述語論理の拡張になっており、「プログラムがある型を持つ」あるいは「項がある命題の証明になっている」という関係を自然に表現できるものである。なお、本研究代表者が昨年まで研究してきたRPTシステムとの違いは、RPTにおいては、それらの関係が組み込みであることに対して、本研究で提案した新しい体系では、新たに定義できる仕組みを導入した、ということである。従って、「項がある命題の証明である」という関係をrefineした関係も定義できるようになった。
次に、この体系の無矛盾性と実現可能性解釈の健全性を証明した。この実現可能性解釈は若干の制限はあるものの、上記の関係を自然に定義できるものである。自然数、リスト、二分木などのデータ型を自然な帰納的述語定義を用いて記述すると、論理記号として論理和や存在記号を多く含んだ形式になる。この論理式に対する証明(プログラム)は無駄なコードを多く含み、プログラムが効率的でない、という問題点があった。そこで、上記の仕組みを使ってプログラムとその型の関係を、無駄なコードを含まないような関係に定義しなおすことによって、プログラムの効率化をはかることができるようになった。

Research Products

• [Publications] M.Sato: "Conservativeness of LAMBDA over lambdasigma-calculus" Lecture Notes in Computer Science,Springer.
• [Publications] 亀山幸義: "負の出現を持つ帰納的述語定義とそのプログラム導出への応用" 記号論理学と情報科学研究集会. (1993)