項書き換えのソースを表示

'''項書き換え'''（こうかきかえ、{{lang-en-short|term rewriting}}）とは、[[数学]]・[[計算機科学]]・[[論理学]]において、式（数式、論理式）の[[項]]を別の項に置換する手法を総称する用語である。'''項書き換え系'''（{{lang-en-short|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'' &times; ''b'' は ''a'' と ''b'' の乗算を意味する。

以下では、plus(''a'', ''b'') を ''a''+''b'' と記述し、times(''a'', ''b'') を ''a'' &times; ''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>）は規則の左辺が右辺に書き換え可能であることを示す（つまり「～ならば～」という[[論理包含|条件文]]ではない）。

==合流性と停止性==
{{see also|クヌース・ベンディックス完備化アルゴリズム}}
===合流性===
{{main|合流性}}
以上、例示した項書き換え系をみてみると、項を最も単純な項へと書き換えることができ、最終的に得られる項はその項書き換え系内では書き換えることができない。それ以上書き換えられない項の並び（式）を[[標準形]]と呼ぶ。標準形の存在可能性と一意性の観点で項書き換え系を分類することもできる。標準形のない項書き換え系もある。例えば、2つの項 ''a'' と ''b'' があって、''a'' &rarr; ''b'' と ''b'' &rarr; ''a'' という規則がある場合である。

どういう置換規則を適用しても最終的に同じ標準形になる項書き換え系の性質を「'''[[合流性]]'''」と呼ぶ。これは、標準形の一意性と結びついた特性である。

===停止性===
2つの項 ''a'' と ''b'' があって、''a'' &rarr; ''b'' と ''b'' &rarr; ''a'' という規則がある場合、a を書き換えると a と b を行ったり来たりし、収束しなくなる。全ての項に対して収束する項書き換え系の性質を「'''停止性'''」と呼ぶ。

==抽象項書き換え系==
抽象的な項書き換え系もある。この場合、項の集合と置換規則を用意しなければならない。

項の集合 ''T'' = {''a'', ''b'', ''c''} と、置換規則 ''a'' &rarr; ''b''、''b'' &rarr; ''a''、''a'' &rarr; ''c''、''b'' &rarr; ''c'' があるとする。これをよくみると ''a'' も ''b'' も最終的に ''c'' に書き換えられることがわかる。このような特性が重要である。この場合、''c'' はその系において最も基本的な項と考えられ、''c'' を他の何かに書き換えることができない。

==関連項目==
*[[クヌース・ベンディックス完備化アルゴリズム#危険対|危険対]]
*[[合流性]]
*[[グラフ書き換え]]
*[[クヌース・ベンディックス完備化アルゴリズム]]
*[[ラムダ計算]]
*[[リンデンマイヤーシステム]]
*[[Mathematica]]
*[[Q_(プログラミング言語)|Q言語]]
*[[文字列書き換え系]]

==参考文献==
{{参照方法|date=2023年8月}}
*Nachum Dershowitz and Jean-Pierre Jouannaud. [http://citeseer.ist.psu.edu/dershowitz90rewrite.html Rewrite Systems] (1990). Chapter 6 of ''Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)'', pp.243&ndash;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

{{Normdaten}}
{{DEFAULTSORT:こうかきかえ}}
[[Category:形式言語]]
[[Category:形式手法]]
[[Category:数理論理学]]
[[Category:計算理論]]
[[Category:数学に関する記事]]