Term Rewriting and All That


The errors marked with (p) are still present in the paperback edition.

1, line -7: replace s(s(s(0))+0) by s(s(s(0)+0)). (Sebastian Skalberg) (p)

15, line 9: replace "that" by "that if"" and "iff" by "then". (Aurelian Radoaca) (p)

25, line -10: replace $\gtrsim$ by $\gtrsim_{mul}$ (Aurelian Radoaca) (p)

27, line -14 and -18: replace "bool" by "order" in the type of the ML functions "rem1" and "mdiff". (Stephen Eldridge) (p)

29, line 1: replace "example" by "examples". (Markus Triska) (p)

29, penultimate line of the proof of Newman's Lemma: replace y1 by y and z1 by z. (Aurelian Radoaca) (p)

39, line 7: replace $\cal T$ by T. (Amine Chaieb) (p)

45, lines -7, and -8: replace $A$ by $\cal A$. (Aurelian Radoaca) (p)

51, line 6: replace T by $\cal T$ (in the range of the homomorphism). (Sebastian Skalberg) (p)

52, line -15: replace X by V. (Amine Chaieb) (p)

60, Exercise 4.2: add "finite" before E. (Martin Lange) (p)

77, line 9: replace V(t) by Var(t). (Dennis Pagano) (p)

96, line -8: replace left-arrow over l by right-arrow. (Hisashi Kondo)

98, line 21 and 22: replace s1 by s0 (in definition of $\stackrel{\rightarrow}{\Gamma}$ and $\stackrel{\leftarrow}{\Gamma}$).

101, Exercise 5.2: replace "ground" by "right-ground". (Robert McNaughton) (p)

103, Exercise 5.6: Two assumptions are missing. First, the set of ground terms must be non-empty. Under this assumption, the order defined on p.104 is a reduction order. To show that it is the largest order, one must additionally assume that the order > one starts with is total on ground terms. (Ralph Matthes) (p)

106, line -10: replace "2 > 1" by "3 > 2" and $\odot^A(1,2) = 1 = \odot^A(1,1)$ by $\odot^A(2,3) = 4 = \odot^A(2,2)$ (Aurelian Radoaca) (p)

111, Exercise 5.9: replace k|s|f by k(|s|f+1)

114, in the paragraph after (1): replace both occurrences of n by ni. (Aurelian Radoaca) (p)

115, line 4: replace "variable" by "variable or a constant"

115-116: In the proof of Theorem 5.4.8 replace every occurrence of V(.) by Var(.).

120, lines 2 and 3: replace l by n. (Martin Lange) (p)

120, lines -5: replace 1 ≥ i ≥ n by 1 ≤ i ≤ n. (Aurelian Radoaca) (p)

134-135, proof of Theorem 6.1.1: add the assumption "and neither l nor r is a variable" behind "Var(l) = Var(r)" (2 occurrences).

135: First sentence of section 6.2: insert "terminating" in front of "finite".

140, line 6: replace t1 by t1|p1 and t2 by t2|p2. (Aurelian Radoaca) (p)

142: In Exercise 6.7 (b) replace both occurrences of E by G. (p)

144, line 3, below Fig 6.3: replace "cps" by "innercps". (Yamatodani Kiyoshi) (p)

153, line -2: replace P1 by P1>. (Daniel Reiß) (p)

154: line 2: replace P1 by P1> and P0 by P0>; lines 3 and 4: replace P0 by P0<.

156, Exercise 6.18: replace h(p(x),q(x)) by h(p(x),q(y)). (Aurelian Radoaca) (p)

158, line -7: replace "canonical" by "convergent". (Philipp Lucas) (p)

175, line -13: replace si-1[sigma(u)] by si-1[sigma(u)]p. (Yamatodani Kiyoshi) (p)

178, lines -11,-12: replace Ri by Ri ∪ {l → r}. (Aurelian Radoaca) (p)

183, line -13 (second recursive call of simpl): replace E by E'. (Jaco van de Pol) (p)

190, line -2: replace the last f1 with fk. (Aurelian Radoaca) (p)

192, line 25 (penultimate line in proof of Theorem 8.2.7): replace fl by fs(l) (2 occurrences).

228, line -5: replace S1 by S (in exercise 10.3) (Sebastian Skalberg) (p)

233, Fig. 10.1: replace the last "Decompose" by "Delete" (Aurelian Radoaca) (p).

239 and 242, in the displayed equation marked with (*): replace the 3x1 zero-matrix by the 1x1 zero-matrix "(0)". (Sebastian Skalberg) (p)

240, line -12, the first line in the proof of Theorem 10.3.10: replace Mn,r(sigma) by Mn,r(sigmaW). (Yamatodani Kiyoshi) (p)

249, line 9: The sequence of inequalities in this line must be changed slightly. In addition, for the statement in line 10 to be true, the definition of the norm of a matrix must be changed. See here for details. (Markus Rosenkranz) (p)

253, line 18: replace $\models s \not\approx t$ by $\not\models s \approx t$. (Sebastian Skalberg) (p)

255, lines 6 and 11: replace (s+1)*σ(t)+s*σ(t) by (s+1)*σ1(t)+s*σ2(t). (Aurelian Radoaca) (p)

255, line -15 through -11: The tau introduced locally with "Let tau be..." clashes with the global tau that occurs in the definition of sigma. It needs to be renamed to, for example, delta. Thus on those 5 lines all occurrences of tau, except for the 4th, 9th and 12th, should be replaced by delta. (Sebastian Skalberg) (p)