項書き換え
一般的な算術の規則は、以下のような規則を含む項書き換え系とみなすことができる:
p l u s ( a , b ) → a + b {\displaystyle \mathrm {plus} (a,b)\rightarrow a+b}
t i m e s ( a , b ) → a × b {\displaystyle \mathrm {times} (a,b)\rightarrow a\times b}
ここで a+b は a と b の加算を意味し、a × b は a と b の乗算を意味する。
以下では、plus(a, b) を a+b と記述し、times(a, b) を a × b と記述する。次のような式があるとする。
( 11 + 9 ) × ( 2 + 4 ) {\displaystyle (11+9)\times (2+4)}
この式を書き換える方法は2種類ある。最初の括弧の中を単純化するか、2番目の括弧の中を単純化するかである。最初の括弧の中を先に項書き換えで単純化すると、次のようになる。
20 × ( 2 + 4 ) = 20 × 6 = 120 {\displaystyle 20\times (2+4)=20\times 6=120}
2番目の括弧の中を先に単純化すると、次のようになる。
( 11 + 9 ) × 6 = 20 × 6 = 120. {\displaystyle (11+9)\times 6=20\times 6=120.}