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

构造性逻辑系统的规范描述与证明创建研究

基本信息

批准号：
05780221
负责人：
亀山幸義
金额：
$ 0.58万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1993
资助国家：
日本
起止时间：
1993 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-05780221/
关键词：
構成的プログラミング証明帰納的述語定義仕様記述

项目摘要

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

本构编程是一个编程范式，其中通过证明代表本构逻辑系统规范的逻辑表达式来创建程序。该方法还具有保证程序的合法性的缺点，但也很难描述规范。人类规范是模棱两可的，因此不能将其转换为机械代表规范的逻辑表达。这项研究的目的是使从人类易于编写的规格中实施组成编程的方法加固方法。首先，我们设计了用于规范说明的逻辑系统。该系统是对一阶谓词逻辑的构型扩展，并且自然可以表达关系“具有类型”或“具有术语”或“具有术语的证明”的关系。直到去年，研究人员研究人员研究的RPT系统之间的差异是，尽管这些系统之间的关系嵌入了RPT中，但本研究中提出的新系统介绍了可以定义的新机制。因此，已经有可能定义一种完善关系的关系“术语是命题的证明”。接下来，我们证明了该系统的一致性以及可行性解释的健全性。这种可行性解释是上述关系的自然定义，尽管存在一些局限性。当数据类型（例如自然数，列表）使用自然归纳谓词定义编写二进制树时，它们成为包括许多逻辑符号，包括逻辑总和和存在符号的格式。此逻辑表达式的证明（程序）包含许多不必要的代码，并且该程序效率低下。因此，通过使用上述机制重新定义程序及其类型与不包括不必要的代码的关系之间的关系，可以提高程序的效率。