項書き換え

項書き換えとは

項書き換え（英: term rewriting）は、数学、計算機科学、論理学において、式（数式、論理式）の項を別の項に置換する手法を総称する用語です。項書き換え系（英: term rewriting system、TRS）は、項の集合とその置換規則から構成されます。

特徴

項書き換えは、一つの項が複数の規則によって書き換え可能である場合があり、非決定的になることがあります。項書き換え系は、項を書き換えるための具体的なアルゴリズムを提供するのではなく、書き換え規則の集合のみを提供します。しかし、適切なアルゴリズムと組み合わせることで、項書き換え系はプログラムのように機能し、一部の宣言型プログラミング言語は項書き換えに基づいています。

例

算術

一般的な算術の規則は、以下のような規則を含む項書き換え系とみなすことができます。

`plus(a, b) → a + b`
`times(a, b) → a × b`

ここで、`a + b` は `a` と `b` の加算を、`a × b` は `a` と `b` の乗算を意味します。

例えば、`(11 + 9) × (2 + 4)` という式があるとき、以下の2通りの書き換えが可能です。

最初の括弧の中を先に単純化する: `20 × (2 + 4) = 20 × 6 = 120`
2番目の括弧の中を先に単純化する: `(11 + 9) × 6 = 20 × 6 = 120`

初等代数学

項書き換え系は、自動定理証明にも応用できます。等式からなる仮説があるとき、それらを項書き換え規則として利用できます。例えば、「類似の項を一方の辺に集める」という手法は、代数学における項書き換えの一例です。

`P(x) = Q(x)` (P と Q は多項式) に対して、通常の規則を適用することで、`R(x) = 0` という形の等式が得られます。ここで、R が正規形であるとは、R(x) の項が x の次数の大きいものから順に並んでいることを意味します。

論理学

論理学では、論理式から連言標準形(CNF)を得る手続きを項書き換え系として表現できます。例えば、以下の規則が適用されます。

`¬¬A → A` (二重否定の除去)
`¬(A ∧ B) → ¬A ∨ ¬B` (ド・モルガンの法則)
`¬(A ∨ B) → ¬A ∧ ¬B`
`(A ∧ B) ∨ C → (A ∨ C) ∧ (B ∨ C)` (分配法則)
`A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)`

合流性と停止性

合流性

項書き換え系において、どのような置換規則を適用しても最終的に同じ標準形になる性質を「合流性」と呼びます。これは、標準形の一意性と関連する重要な特性です。

停止性

全ての項に対して、書き換えが有限ステップで終了する（収束する）項書き換え系の性質を「停止性」と呼びます。

抽象項書き換え系

抽象的な項書き換え系では、項の集合と置換規則を定義します。例えば、項の集合 T = {a, b, c} と、置換規則 a → b、b → a、a → c、b → c がある場合、a も b も最終的に c に書き換えられます。この特性は、系の基本的な項を特定する上で重要です。

関連項目

危険対
合流性
グラフ書き換え
クヌース・ベンディックス完備化アルゴリズム
ラムダ計算
リンデンマイヤーシステム
Mathematica
Q言語
文字列書き換え系

参考文献

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

もう一度検索