1989 Fiscal Year Annual Research Report
| Project/Area Number |
62460220
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000)
|
|---|
| Keywords | 構成的数学 / 関数型プログラム言語 / 直観主義論理 / 証明 / プログラムの検証 / プログラムの合成 |
|---|
| Research Abstract |
構成的プログラミングは、構成的数学を形式化した論理体系をプログラム理論に応用したプログラミングの考え方である。本年度の研究では、この構成的プログラミングの考えの理論的、実際的有効性を示すため以下の研究を行った。
基礎となる論理体系SSTは、これまで述語の帰納的定義において、ハロップ論理式のみを許していたが、それを一般の論理式を許すような拡張を行った。これにより、SSTは更に強力な体系となった。新しいSSTに対してモデルを構成することにより、無矛盾性を示し、また、従来難しいとされてきた、一般的な帰納的述語定義に対する実現可能解釈を定義し、その健全性定理を証明した。
SSTに含まれるプログラム言語Λに大幅な変更を加えた。この変更は、昨年度の研究で作成した従来のΛの処理系による証明、合成システムの経験をふまえ、それらのシステムをより簡潔に自然に記述できるようにするためのものである。大きな変更点は、パタ-ン照合機能を強化したこと、表現をLISPのS式風に改めたこと、デ-タ型の概念を部分的に取り入れたこと、論理体系を表現するためのquoteの機構を整備したことなどである。この新しいΛをSSTの項として表現する変更を加え、その処理系をワ-クステ-ション上に実現した。
新しいΛにより、SSTの証明システム、プログラム抽出システムをワ-クステ-ション上に実現した。これらのシステムにより、計算機の上でSSTの証明を作成し、それを検証し、更に、そこから計算の情報を抽出して誤りのないプログラムを合成することに成功した。実際に、いくつかの例を作成して、この手順によるプログラム合成が有効であることを実証した。また、例を通して、証明と抽出されたプログラムの関係についての研究を行った。
|
