| 研究概要 |
本研究では、構成的プログラミングの基礎となる論理体系として,RPTを設計,改良し,その性質について研究を行った.RPTは,証明を項として直接取り扱うことのできる論理体系であり,「メタな概念」を体系内で表現できるという特徴を持っているため,構成的プログラミングを実現する基礎となるものまである.本研究では,意味論理的体系として与えられたRPTの1つの形式化を与え,その理論的性質を解明した.また,プログラム言語Λの設計を完成させた.Λは,手続き型プログラム言語における代入文や繰り返し文に相当する機構を持ちながら,関数型プログラム言語としての理論的性質を保持していることを示した.
次に,Aの処理系(インタープリタ,コンパイラ)をワークステーション上に実装した.Aの遅延評価機構と代入文の並存は,実行効率を著しく落とす要因となる問題点を指摘し,この問題に対し,プログラム変換の方法による解決方法を提案した.実装した処理系では,この手続きを組みこんでいるため,プログラムに負担をかけずに,高効率の実行が可能な処理系となっている。
さらに,Λを用いて,理論体系RPTの形式化に対応する証明システムをワークステーション上に実現した.このRPTの証明システムを用いて、Λのプログラムを検証することができるようになり,Church-Rosserの定理など,いくつかの例を作成した.また,証明した定理から,プログラムを抽出するシステムも作成し,それを利用してappendなどのプログラム例を作成し、構成的プログラミングの有用性を実証した。
|
