Experiments on termination problems

General Information

Our termination tool employs the dependency pair method with cycle analysis of dependency graphs, reduction pairs, and rule removal by monotone reduction pairs.

L

lexicographic path orders (LPO) with argument filtering

Ed

echelon-form matrix interpretations on N^d with 0,1-matrix coefficients, equipped with the lexicographic order (Section 5)

Sd

matrix interpretations on N^d with 0,1-matrix coefficients, equipped with the standard order (by Endrullis et al. 2008)

M

max/plus interpretations of the form f_A(x₁,....,x_n) = max{b₀, a₁(x₁ + b₁), ..., a_n(x₁ + b_n)} with a_i in {0,1} and b_i in N

WA

weighted path orders (WPO) with algebras A ∈ {Ed, Sd, M}

AProVE

AProVE 2024

NaTT

NaTT (termCOMP 2024 version)

For instance, E1L stands for the lexicographic combination of E1 and L. Note that E1 and S1 are identical. Concerning heterogeneous combinations, (e.g.) E1 ⊆ E1L does not hold in general, as weak orientation by E1 does not guarantee weak orientation by L. On the other hand, A ⊆ WA holds. Column A-B in the following table tries AA, BB, AB, and (then) BA Here AB stands for the lexicographic combination of A and B.

Note

• L ⊆ LL = LLL
• E1 ⊆ E1E1 ⊆ E2 ⊆ E3 ⊈ E4. The non-inclusion is due to timeouts. |E3 ∪ E4| = 568.
• S2 ⊈ S2S2 ⊇ S2S2S2; The non-inclusion and the reverse inclusion are simply due to timeouts. |S2 ∪ S2S2| = 623.
• |L ∪ E1| = 503 and |L ∪ E1 ∪ LE1 ∪ E1L| = |L ∪ E1 ∪ E1L| = 533.
• |L ∪ E1 ∪ S2| = 616.
• The union of L, LL, LLL, Ed, S2,S2S2, S2S2S2, E1L, LE1, and E1E1 amounts to 649, which is covered by LL ∪ E4 ∪ S2 ∪ S2S2.
• The 649 contains 3 problems that AProVE missed but they are merely due to a parse error and efficiency reasons.
• The 649 contains 8 problems that NaTT missed. Here 3 problems can be shown by S2 and L, but the remaining 5 problems are handled by E3, E4, or S2S2:
  AG01_3.40, Transformed_CSR_04_Ex4_DLMMU04_iGM, Transformed_CSR_04_LengthOfFiniteLists_nokinds_noand_C, and Transformed_CSR_04_PEANO_nokinds_noand_C.