項書き換え
項書き換え（こうかきかえ、英: term rewriting）とは、数学・計算機科学・論理学において、式（数式、論理式）の項を別の項に置換する手法を総称する用語である。項書き換え系（英: term rewriting system、TRS）とは、項の集合とその置換規則から構成される。
項書き換えは非決定論的になることがありうる。ある規則で書き換え可能な項が他の規則でも書き換え可能な場合がありえて、その場合は複数の規則が適用可能と言うことになる。項書き換え系では、項書き換えのためのアルゴリズムは提供されず、書き換え規則の集合のみが提供される。しかし、適当なアルゴリズムと組み合わせれば、項書き換え系はプログラムのような働きをし、実際いくつかの宣言型プログラミング言語は項書き換えに基づいている。
例
算術
一般的な算術の規則は、以下のような規則を含む項書き換え系とみなすことができる:
- [math] \mathrm{plus}(a, b) \rightarrow a + b[/math]
- [math] \mathrm{times}(a, b) \rightarrow a \times b[/math]
ここで a+b は a と b の加算を意味し、a × b は a と b の乗算を意味する。
以下では、plus(a, b) を a+b と記述し、times(a, b) を a × b と記述する。次のような式があるとする。
- [math] (11 + 9) \times (2 + 4)[/math]
この式を書き換える方法は2種類ある。最初の括弧の中を単純化するか、2番目の括弧の中を単純化するかである。最初の括弧の中を先に項書き換えで単純化すると、次のようになる。
- [math] 20 \times (2 + 4) = 20 \times 6 = 120[/math]
2番目の括弧の中を先に単純化すると、次のようになる。
- [math] (11 + 9) \times 6 = 20 \times 6 = 120.[/math]
初等代数学
項書き換え系は自動定理証明にとっても便利な手法である。いくつかの等式からなる仮説があったとき、それらが一種の項書き換え規則群として利用できる。簡単な代数学での項書き換え手法として「類似の項を一方の辺に集める」というやり方がある。その進め方は何通りもある。
- P(x) = Q(x)
ここで、P と Q は多項式である。これに通常の規則を何度か適用すると次のような形の等式が得られる。
- R(x) = 0.
これは一種の標準形であるが、書き換えの経路が違うと R の内容が異なることもある。R が正規形であると言った場合、R(x)は x の次数の大きい項から順に次数が小さくなるように項が並んでいる。
論理学
論理学では、ある論理式が連言標準形(CNF)であるかどうかを決定する手続きが項書き換え系として使われる。その系の規則は以下の通りである:
- [math]\neg\neg A \to A[/math] （二重否定の消去）
- [math]\neg(A \land B) \to \neg A \lor \neg B[/math] （ド・モルガンの法則）
- [math]\neg(A \lor B) \to \neg A \land\neg B[/math]
- [math] (A \land B) \lor C \to (A \lor C) \land (B \lor C)[/math] （分配法則）
- [math] A \lor (B \land C) \to (A \lor B) \land (A \lor C)[/math]
ここで、矢印（[math]\to[/math]）は規則の左辺が右辺に書き換え可能であることを示す（つまり「～ならば～」という条件文ではない）。
合流性と停止性
合流性
以上、例示した項書き換え系をみてみると、項を最も単純な項へと書き換えることができ、最終的に得られる項はその項書き換え系内では書き換えることができない。それ以上書き換えられない項の並び（式）を標準形と呼ぶ。標準形の存在可能性と一意性の観点で項書き換え系を分類することもできる。標準形のない項書き換え系もある。例えば、2つの項 a と b があって、a → b と b → a という規則がある場合である。
どういう置換規則を適用しても最終的に同じ標準形になる項書き換え系の性質を「合流性」と呼ぶ。これは、標準形の一意性と結びついた特性である。
停止性
2つの項 a と b があって、a → b と b → a という規則がある場合、a を書き換えると a と b を行ったり来たりし、収束しなくなる。全ての項に対して収束する項書き換え系の性質を「停止性」と呼ぶ。
抽象項書き換え系
抽象的な項書き換え系もある。この場合、項の集合と置換規則を用意しなければならない。
項の集合 T = {a, b, c} と、置換規則 a → b、b → a、a → c、b → c があるとする。これをよくみると a も b も最終的に c に書き換えられることがわかる。このような特性が重要である。この場合、c はその系において最も基本的な項と考えられ、c を他の何かに書き換えることができない。
関連項目
参考文献
- Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems (1990). Chapter 6 of Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp.243–320.
- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003
- Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998