優先順位と二分決定グラフに基づく複数経路順序下の項書換え系完備化手続き

摘要

関数型プロダラミング，代数的仕様記述，定理自動証明，記号処理など，等式によって表現されたシステムが数多く研究されている．項書換え系［二木83，Dershowitz 90，外山01，Terese 03］は与えられた等式仕様から導かれる項の書換え規則の集合として定義され，項を書換え規則に従って順次書換えることで計算を行う．項書換え系に要求される重要な性質として，停止性（書換えが停止すること）および合流性（書換えの結果が一意であること）があり，これらを共に満たすとき，書換え系は完備であるいう．停止性は簡約順序とよばれる項の集合上の順序を適切に定めることによって保証され，停止性を満たす項書換え系は，さらに弱合流性（あるいは局所合流性）とよばれる性質が保証されることによって完備となることが知られている．