Non-Termination of Logic Programs Using Patterns

Technical Summary: Non-Termination of Logic Programs Using Patterns

Problem Statement
This paper addresses the automatic detection of non-termination in logic programs (LPs). While much existing research focuses on detecting loops (finite rewrite sequences that can be repeated indefinitely), this work targets non-looping non-termination. These are infinite rewrite sequences that do not embed any loop, making them inherently non-periodic and difficult to detect. The author notes that such sequences can arise from simple logic programs, yet standard loop-detection methods often fail to identify them. The motivation is twofold: theoretical (studying remarkable forms of infinite sequences) and practical (helping programmers identify queries that run forever).

Methodology
The author adapts an approach originally introduced for term rewriting by Emmes et al. (2012) to the domain of logic programming. The core methodology involves defining a new unfolding technique that generates "patterns" describing potentially infinite sets of finite rewrite sequences.

1. Pattern Definitions:

   • Pattern Substitutions: Defined as pairs $\theta = (\sigma, \mu)$, denoted $\sigma \star \mu$, describing a set of substitutions $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$.
   • Pattern Terms: Pairs $(s, \theta)$ describing the set $\{s\theta(n) \mid n \in \mathbb{N}\}$.
   • Pattern Rules: Pairs of pattern terms $(p, q)$ describing a set of binary rules $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$.

2. Correctness and Unfolding:

   • A pattern rule is deemed correct with respect to a program $P$ if the set of rules it describes is a subset of the binary unfolding of $P$ ($binunf(P)$).
   • The author introduces a new unfolding operator $T^\pi_{P,B}$ that computes pattern rules from a program $P$ and a base set of correct pattern rules $B$. This operator uses a unification algorithm for pattern terms to combine rules, effectively "unfolding" the program faster than traditional binary unfolding by capturing infinite subsets of $binunf(P)$ in finite representations.

3. Simple Patterns and Unification:

   • To make the approach automatable, the author restricts the domain to simple pattern terms, where substitutions follow a specific structure involving unary contexts.
   • A unification algorithm is provided for these simple terms. It maps simple pattern terms to terms over a specialized signature $\Upsilon$ (using unary symbols $c_{a,b}$ to represent repeated embeddings) and applies classical unification algorithms (e.g., Robinson, Martelli-Montanari).
   • The algorithm is proven partially correct: if it terminates successfully, it produces a most general unifier (mgu) for the input pattern sequences.

4. Non-Termination Criteria:

   • General Criterion (Theorem 3): Adapted from Emmes et al., this states that if the pattern unfolding contains a rule of the form $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ where $\sigma'$ commutes with $\sigma$ and $\mu$, then an infinite chain exists.
   • Special Criterion (Theorem 5): A more easily checkable condition for special pattern rules (a subset of simple rules). If such a rule exists in the unfolding, the paper proves the existence of an infinite chain starting from specific instances of the rule's left-hand side.

Key Contributions
The paper presents four primary contributions:

1. New Unfolding Technique: A method to produce correct pattern rules for logic programming, offering a more compact presentation than the nine inference rules used in term rewriting and eliminating the need for complex application strategies.
2. Simple Pattern Terms and Unification: The definition of a restricted form of pattern terms ("simple") and a corresponding unification algorithm proven to be correct.
3. Automatable Sufficient Condition: An easily checkable condition (Theorem 5) to detect non-looping non-termination from simple pattern rules.
4. Implementation (NTI): The implementation of this approach in a tool named NTI.

Experimental Results
The author evaluated NTI on 41 logic programs derived from non-looping non-terminating Term Rewrite Systems (TRSs) in the Termination Problem Data Base (TPDB).

• Success: The tool successfully proved non-termination for 36 of the 41 programs. Notably, it succeeded on 4 programs (marked with † in the tables) that had not been proven non-terminating by any other TRS analyzer in the International Termination Competition up to 2024.
• Failure: The approach failed on 5 programs, primarily due to the incompleteness of the unification algorithm when using the "natural choice" for term representatives (as discussed in Example 12) or the restriction to simple patterns (Example 9).
• Performance: Execution times were generally low (under 300ms for successful cases), though some complex cases resulted in timeouts.

Significance and Claims
The author claims that their approach is the only tool participating in the International Termination Competition capable of disproving termination of logic programs. They note that while another approach by Payet (2024) exists for proving non-looping non-termination, it addresses a different class of non-loopingness and is unable to disprove termination of the specific programs tested in this paper (Tables 1 and 2). Conversely, the Payet (2024) approach can disprove termination of programs where this method fails. Thus, the two approaches are presented as complementary.

The paper concludes modestly, acknowledging that the unification algorithm is currently incomplete and that the restriction to simple patterns limits the scope (e.g., failing on programs requiring 1-contexts with variables). Future work is planned to address completeness, extend the initial pattern generation (Prop. 2), and adapt the approach to TRSs for direct comparison with Emmes et al. (2012).