証明コンパイラにおける拡張射影手法

概要

論文の詳細を見る
構成的証明から実現可能性解釈(realisability interpretation)を使って実行可能コードが抽出できることは古くから知られているが,その原理を応用して数学の証明からプログラム生成を行うのが証明コンパイラである.しかしながら実現可能性解釈だけではプログラムとして意味の無いコードまでも生成されてしまい,生成されたプログラム全体の実行効率を大きく下げてしまうことが多い.本論文では,証明の中のアルゴリズムに関係しない部分を解析・判別して冗長性の無いプログラムを生成する手法「拡張射影手法」を提案する.すなわち,人間が定理の部分に簡単な宣言を行ってプログラムとして取り出したいものを指定すると,その情報が自動的に証明木の各ノードに伝搬される.証明コンパイラは付加情報が付いた証明本から冗長性の無いプログラムを生成する.この方法によって一つの証明から複数のアルゴリズムを抽出することもできる.この方法は,簡単な型構造,数学的帰納法,およびq-実現可能性解釈が定義された簡単な構成的一階述語論理の上で展開される.例題として,素数判定プログラムを示す.
1990-10-15