|
本研究の目的は、関数型言語や定理証明システムに対して有用でありながらも、研究成果がほとんどなかった「非決定的な」(非直交な)項書き換えシステムの理論を構築することである。本年度は、(1)計算の答え(正規形)の一意性を保証する合流性と、(2)答えに辿り着く書き換えの仕方(正規化戦略)の研究を行った。また来年度予定の、(3)定理証明への応用へ向けた研究を一部前倒しして行った。
まず合流性の研究について。無限列において衝突する規則(危険対ステップ)が無限に現れない左線形局所合流システム(減少合流システム)が合流性を持つことを示した。これは左線形システムに対する二大合流性定理(Knuth-Bendix条件・直交性)を一般化する定理である。さらに弱直交性を包含する合流性条件への拡張にも成功した。前者の成果は国際会議IJCARで発表を行った。Development Closure Theoremを包含する定理への拡張は来年度に行う。
戦略について。直交システムの正規化戦略であるfull-substitudonと並列最外戦略が、共に減少合流システムでも正規化戦略になることが示された。関数型言語の実行時最適化などへの応用が期待できる。また完備で変数複製なしのオーバレイシステムでは、最内書き換え戦略が最悪の計算量を持つと判明した。これらは国際ワークショップと国際論文誌へ投稿中である。Root Needed戦略の研究は来年度に持ち越す。
最後に定理証明については著しい進捗を得た。現在の定理証明の自動化理論は「Knuth-Bendix完備化」と呼ばれる1970年から1980年にかけて確立した枠組みを基盤にしている。本研究では「極大完備化」と名付けた既存の手法と全く異なる、シンプルかつ柔軟でしかも高効率な理論体系を開発することに成功した。この成果は国際会議RTAに受理された。
|
