| 研究概要 |
本研究の目的は,等式を用いた自動証明技術として広い応用範囲をもつ完備化と呼ばれる手続きの高速な実装技術を提案することである.本研究では,等式を解くための手続きであるナローイングと完備化手続きとの類似性に着目し,ナローイングに基づく関数論理型言語処理系の実装で提案されているコンパイル技術を完備化手続きに応用することで完備化手続きの高速化をはかることを目的とした.
今年度は,前年度提案した完備化手続きを高速に実装するための等式のコンパイル技術を用いて,実際にUNIX環境上に完備化手続きを実装した.具体的には,コンパイルされた等式からの危険対の生成と,実行時での動的な等式コンパイルのための命令セットをもつ抽象機械を実装し,完備化手続きの中に組み込んだ.これにより従来のものに比べてある程度の高速化を図ることができたが,期待したほどの効果は得られなかった.これは等式を簡約化する部分が従来の完備化手続きと同様に実装されていたためであった.この問題点を解決するために,今年度は等式のコンパイルされた表現をデータとみなして簡約を行う方法について検討を行い,実装を試みた.
また,高階の完備化の理論的研究と関連して,前年度につづいて高階ナローイングに関する理論的研究を行った.前年度で提案した高階ナローイング計算系を出発点とし,その計算系が生成する解の探索空間をさらに縮小できるいくつかの改良点を発見した.それらを組み合わせることで,いくつかの新たな高階ナローイング計算系を提案した.
|
