（２３）プログラム生成システム：ＰＡＰＹＲＵＳ


	マ シ ン：PSI
	環　　境：SIMPOS
	言　　語：ESP
	ソース量：4 MB
	文　　書：マニュアル (日本語／英文)

概要

論理式の構成的証明から、その論理式の仕様を満たすプログラムを取り出すための支援環境である。

ＰＡＰＹＲＵＳは以下の２つのモジュールから構成される。

ＰＡＰＹＲＵＳはCurry-Howard Isomorphismに基づき構成的論理の証明からプログラムの生成を行うためのシステムである。その主な機能として、

論理定義をCalculus of Constractionsのデータ型として管理する。よって、このデータを変更することでプログラム生成のための様々な論理を使用できる。
Calculus of Constractionsで表現された論理データにより証明のチェックを行う機構を内蔵し、部分証明が構成される毎に自動的にチェックを行う。
プログラム生成規則を項書き換えルールとして管理する。よって、このデータを変更することで様々な実現可能性解釈を使用できる。また、完成した証明からそのルールに従ったプログラム生成が行える。
項書き換え系をベースとしたマクロ定義機構を利用することにより様々な記述形式が使用できる。
プルーバを自由に呼び出すことができるため、対話的に証明を構成してゆくことができる。
未証明部へのジャンプ機能など、構造エディタによる様々な支援機能を備える。

といったものが用意されている。