| 研究概要 |
最初に,型のない構成的論理体系を基礎として、従来の、単調オペレータによる帰納的述語定義を拡張した機構を加えた体系を提案した.従来の体系においては,Universeの概念は体系に備え付けのものであったが,この体系では,Universeに相当する概念をユーザが新たに定義することができるという特徴を持っている.この特徴により,Universeの定義を少し変更し,変更前と変更後のUniverseが一定の関係を持っていること等を推論することができるようになった.
次に,その体系に対してモデルの構成方法を与えた.さらに,この体系に実現可能生解釈を与え,その健全性を証明した.実現可能性解釈は,従来の単調オペレータによる帰納的述語定義を自然に拡張したものとなっている.また,健全性定理は,単調オペレータによる帰納的述語定義に対する条件と同様な条件のもとで成立することが示された.
最後に,本体系の構成的プログラミングへの応用について検討した.本体系では、Universeの概念を新たに定義することができるので,冗長な情報を持つ証明項から,冗長な情報を落とした効率のよい証明項を与える変換を得ることができる.詳しくいえば,効率の悪い項を与えるUniverse関係と,効率を改善した項を与えるUniverse関係の2つを定義し,両者の間の同等性を証明することができる。この原理に基づき,いくつか例となるUniverse定義を行い,実際に本体系の中での同等性を確かめた.
|
