Exercises

2.1.b

Counterexample: \(\to := {(a, c), (b, c)}\)

2.3

\(a \to b\) iff \(a\) encodes Turing machine \(M_a\) and \(b\) encodes a valid terminating computation (sequence of states) of \(M_a\).

2.9

Let \(|w|_a := \varphi_a(w)\).

\(\varphi(w) := 3^{|w|_a} 2^{|w|_b}\)

Proof

1. Let \(u \to_1 v\). Then \(\varphi(v) = 3^{|v|_a} 2^{|v|_b} = 3^{|u|_a+1} 2^{|u|_b-2} = 3^{|u|_a} 2^{|u|_b} \frac{3}{4} = \varphi(u) \frac{3}{4} < \varphi(u)\).
2. Let \(u \to_2 v\). Then \(\varphi(v) = 3^{|v|_a} 2^{|v|_b} = 3^{|u|_a-1} 2^{|u|_b+1} = 3^{|u|_a} 2^{|u|_b} \frac{2}{3} = \varphi(u) \frac{2}{3} < \varphi(u)\).

2.17

No.

Let \(a > b\). Then \([b^n a | n \in [0, 1, \ldots]]\) is an infinite chain according to \(>_{Lex}\).

Note: This exercise completes the discussion of Lemma 2.4.3.

4.2

Let \(s, t\) be terms. Run BFS from \(s\) using \(\leftrightarrow^E\). If \(t\) is encountered, conclude that \(s \approx_E t\). If the BFS finishes enumerating the equivalence class without encountering \(t\), conclude that \(\lnot s \approx_E t\).

4.4

Let \(x \in Var(r) \setminus Var(l)\). Let \(p\) be a position of \(x\) in \(r\).

Infinite chain:

• \(t_0 = x\)
• \(t_{i+1} = r[t_i]_p\)

4.18

1. a
   • Unifier: \({x \to h(a), y \to h(a)}\)
   • Matcher: \({x \to h(a), y \to x}\)
2. b
   • Unifier: Unsolvable
   • Matcher: \({x \to h(x), y \to x}\)
3. c
   • Unifier: \({x \to h(y), z \to b}\)
   • Matcher: Unsolvable
4. d
   • Unifier: Unsolvable
   • Matcher: Unsolvable

5.2

Counterexample TRS \(R\):

1. \(a \to b\)
2. \(b \to b\)