項書き換え系

項の定義

述語論理で使う項と同じもの。

1. 変数は項である。
2. $f$が$n$引数の関数記号、$t_1,t_2,·,t_n$が項の時、$f(t_1,t_2,·,t_n)$は項である。

項書き換え系の定義

項書き換え系は書き換え規則の集合である。書き換え規則は、$A,B$を項とすると、$A\to B$の形をしている。

項$T$が与えられた時、ある規則$A\to B$と適当な代入$\sigma$があって、$T$の部分項が$A\sigma$と一致すれば、その部分項を$B\sigma$で置き換える。これをリダクションと言う。

例えば、リストを逆順にする項書き換え系は次のようになる。

    reverse([]) → []
    reverse([X|Y]) → append(reverse(Y), [X])
    append([], X) → X
    append([X|Y], Z) → [X|append(Y, Z)]

停止性

すべてのリダクション列は、有限の長さで既約形（それ以上リダクションできない形）に到達する。

合流性

ある項から出発する二種類のリダクション列がある時、うまくその先を続けていくと、同じ項に到達することができる。

項書き換え系と文法との違い

• 書き換える対象が文字列ではなくて、構造を持った項である。
• 終端記号／非終端記号の区別がない。与えられた項をどんどん書き換えていって、それ以上書き換えられなくなったら終り。
• プログラムのモデル化や理論的研究に使われる。