書き換え順序

理論計算機科学、特に形式方程式の自動推論では、無限ループを防ぐために縮約順序が使用されます。書き換え順序、そして書き換え関係は、この概念を一般化したものであり、理論的調査に役立つことが判明しています。

直感的には、 t が何らかの意味で sよりも適切に「単純」である場合、簡約順序R は2 つの項 sとt を関連付けます。

たとえば、項の簡略化はコンピュータ代数プログラムの一部であり、ルール セット { x +0 → x、 0+ x → x、x *0 → 0、 0* x → 0 、x *1 → x、 1* x → x } が使用されている場合があります。これらのルールを使用して項を簡略化するときに無限ループが不可能であることを証明するために、「項tが項sよりも適切に短い場合はsRt」で定義される削減順序を使用できます。セットの任意のルールを適用すると、項は常に適切に短縮されます。

対照的に、x *( y + z ) → x * y + x * zという規則を使用して「配布」の終了を確立するには、 xの重複により項のサイズが爆発する可能性があるため、より複雑な削減順序が必要になります。書き換え順序の理論は、このような場合に適切な順序を提供することを目的としています。

正式には、項の集合上の二項関係(→) は、文脈的埋め込みとインスタンス化の下で閉じている場合、書き換え関係と呼ばれます。正式には、l → r が、すべての項l、r、u 、 uの各パスp、および各置換σに対して u [ l σ ] _p → u [ r σ] _pを意味する場合です。 (→) が非反射的かつ推移的でもある場合、それは書き換え順序付け^[1]または書き換え前順序と呼ばれます。後者の (→) がさらに整基礎である場合、それは簡約順序付け[ ^2]または簡約前順序と呼ばれます。二項関係Rが与えられた場合、その書き換え閉包はR を含む最小の書き換え関係です。^[3]部分項順序を含む推移的かつ反射的な書き換え関係は、単純化順序付けと呼ばれます。^[4]

• 書き換え関係の逆閉包、対称閉包、反射閉包、推移閉包は、書き換え関係であり、2つの書き換え関係の和集合や積集合も同様である。^[1]
• 書き換え命令の逆もまた書き換え命令です。
• 基底項の集合上で全となる書き換え順序（略して「基底全」）は存在するが、すべての項の集合上で全となる書き換え順序は存在しない。^{[注 3] [5]}
• 項書き換えシステム { l ₁ ::= r ₁ ,..., l _n ::= r _n , ...}は、その規則が簡約順序のサブセットである場合に終了する。^{[注4] [2]}
• 逆に、すべての停止項書き換えシステムに対して、 (::=) の推移閉包は縮小順序であるが^[2]、これは必ずしも基底全項書き換えシステムに拡張可能である必要はない。例えば、基底項書き換えシステム { f ( a )::= f ( b ), g ( b )::= g ( a ) } は停止しているが、定数aとbが比較不可能な場合にのみ縮小順序を使用して停止していることが示される。^{[注 5] [6]}
• 基底全体と十分に根拠のある書き換え順序付け^{[注6]には、基底項に関する}適切な部分項関係が必ず含まれる。^[注7]
• ^{逆に、関数記号の集合が有限であるとき、部分項関係[注8]}を含む書き換え順序は必然的に整基礎となる。^{[5] [注9]}
• 有限項書き換えシステム{ l ₁ ::= r ₁ ,..., l _n ::= r _n , ...}は、その規則が簡略化順序の厳密な部分のサブセットである場合に終了するという。^{[4] [8]}

Nachum Dershowitz、Jean-Pierre Jouannaud (1990)。 「 Rewrite Systems」。Jan van Leeuwen (編) 著。形式モデルとセマンティクス。理論計算機科学ハンドブック。第 B 巻。Elsevier。pp. 243–320。doi :10.1016/ B978-0-444-88074-1.50011-1。ISBN 9780444880741。