4 Matching Annotations
  1. Mar 2022
    1. 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\)
  2. Aug 2020
  3. Apr 2020
  4. Feb 2020
    1. Compute the mean of every column in mtcars.
      output <- vector("double", ncol(mtcars))  # 1. output
      for (i in seq_along(mtcars)) {            # 2. sequence
        output[[i]] <- mean(mtcars[[i]])      # 3. body
      }