| 研究概要 |
本研究の目的は,等式を用いた自動証明技術として広い応用範囲をもつ完備化と呼ばれる手続きの高速な実装技術を提案することである。本研究では,等式を解くための手続きであるナローイングと完備化手続きとの類似性に着目し,ナローイングに基づく関数論理型言語処理系の実装で提案されているコンパイル技術を完備化手続きに応用することで完備化手続きの高速化をはかる。
今年度は,ナローイングに基づく関数論理型言語の実装方式について調査を行い,それを基にして完備化手続きを高速に実装するための等式のコンパイル技術を提案した。この中で関数論理型言語処理系の実装で提案されている抽象機械を調査した。関数論理型言語処理系の抽象機械として,関数型言語処理系の抽象機械を拡張したものと,論理型言語処理系の抽象機械を拡張したものとがこれまでに提案されている。今回の調査で,後者の抽象機械を応用することで,完備化の対象となる等式のコンパイルを行えることがわかった。また,完備化の場合,関数論理型言語と異なり,コンパイルの対象となる等式が動的に生成されるという問題がある。そこで,等式の内部表現をコンパイルされたコードに近い形式にすることで,等式の動的な生成がそのまま等式のコンパイルの大部分を兼ねるような方式を提案した。これにより,完備化のようにコンパイルの対象が動的に生成される場合でも高速にコンパイルを行えることがわかった。現在,提案した方式に基づいた完備化手続きの計算機上への実装と評価を進めている段階である。
また,高階の完備化の理論的研究と関連して,高階ナローイングに関する理論的研究を行った。高階ナローイングでは,一階の場合に比べて解の探索空間が爆発的に増えるという問題がある。そこで,解の探索空間が小さくなるように既存の高階ナローイング計算系を改良していき,そこで得られた知見に基づき新たな高階ナローイング計算系を提案した。
|
