多項式サイズ正規形を保証する項書き換えシステムの経路順序

摘要

項書き換えシステムを用いて記述したプログラムが，多項式時間で計算可能であることを示す様々な手法が知られている．Marion (2003)は多項式サイズ正規形を保証する軽多重集合経路順序を提案し，この順序により方向付け可能な項書き換えシステムにおいては，任意の項は多項式時間で評価可能であることを示した．また，多項式時間で計算可能な任意の関数は，この軽多重集合経路順序によって方向付けが可能であるような項書き換えシステムによって記述できることも示されている．しかしながら，一般に項書き換えシステムを与えたとき，多項式サイズ正規形が保証される場合でも，軽多重集合経路順序で方向付けができないことがある．このため，より一般的な経路順序によって多項式サイズ正規形を保証できることが望ましい．本論文では，軽多重集合経路順序を拡張し，より一般的な項書き換えシステムに対して多項式サイズ正規形を保証する新しい経路順序を提案する．