Experiments for ``Simulating Dependency Pairs by Semantic Labeling''

Note

• 1-dimensional linear interpretation is of the form f_A(x₁,...,x_n) = a₀ + a₁ x₁ + ... + a_n x_n with a₀ in ℕ and a_i in {0,1}
• 2-dimensional linear interpretation is of the form f_A((x₁,y₁),...,(x_n,y_n)) = (a₀ + a₁ x₁ + ... + a_n x_n, b₀ + b₁ y₁ + ... + b_n y_n) with a₀, b₀ in ℕ and a_i, b_i in {0,1}. Such an interpretation is weakly monotone if a_i > 0 whenever b_i > 0.
• 3-dimensional is analogously defined.
• Example 21 uses ordinal interpretations B on ω². Such interpretations f_B(ω x₁ + y₁,..., ω x_n + y_n) = ω · (a₀ + a₁ x₁ + ... + a_n x_n) + b₀ + b₁ y₁ + ... + b_n y_n with x_i, y_i in ℕ can be simulated by 2-dimensional linear interpretations of the above form. For instance, rand_B(z) = z + ω (z in ω²) is identical to rand_B(ω x + y) = (ω x + y) + ω = ω · (x + 1) with x, y in ℕ, and thus it is simulated by the 2-dimensional linear interpretation rand_A((x,y)) = (x+1,0).
• As usual, our tool uses reduction pairs based on linear interpretations to remove strictly oriented dependency pairs. If all dependency pairs can be removed, relative termination is concluded. See Hirokawa and Middeldorp (I&C 2005) and Giesl, Thiemann and Schneider-Kamp (LPAR 2005) for details.
• NaTT 2.3.3 (participated in termCOMP 2023) is not available for proving relative termination; see termCOMP 2023.