|
本研究の目的は、関数型言語や定理証明システムに対して有用でありながらも、研究成果がほとんどなかった「非決定的な」（非直交な）項書き換えシステムの理論を構築することである。本年度は前年度に引き続いて、(1)合流性、(2)完備化に基づく定理証明、(3)正規化戦略の3つの課題を研究を行った。
(1)については合流性ツールSaigawaにChurch-Rosser モジュロ (Jouannaud & Kirchner 1986) の手法を実装、また逆方向危険対による合流性反証手法を開発し、ツールの証明・反証能力を格段に向上させた。ツールはオープンソースとして公開されている。
(2)については、前々年度に得られた極大完備化をもとに、（帰納的）定理自動証明へ適用できる制約付き等式へと理論体系を発展させ、実験評価を行った。
(3)については、root normalization strategy (Middeldorp 1997) が減少合流性のクラスで正規化戦略になるか研究を行った。前年度までに見つかった証明のギャップについてはついに期間内に埋まらなかった。平成25年度採択の研究課題「項書換えの合流性解析とその応用」(No. 25730004)へ引き継ぐ。
上記３研究に加え本研究分野のコミュニティ形成のため、合流性に関する第1回国際ワークショップ(IWC 2012)を５月にインスブルック大学の研究協力者と共催、また合流性ツールの国際競技会(CoCo 2012)を東北大学・インスブルック大学とともに共催した。それにともない競技会のためのデータベースおよびインフラシステムの開発を行った。
|
