{'fraction_non_alphanumeric': 0.04937519049070405, 'fraction_numerical': 0.01264858274916184, 'mean_word_length': 4.147450980392157, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Non-termination using Regular Languages

We describe a method for proving non-looping non-termination, that is, of term rewriting systems that do not admit looping reductions. As certificates of non-termination, we employ regular (tree) automata.


Introduction
We describe a method for proving non-termination of term rewriting systems that do not admit looping reductions, that is, reductions from a term t to a term C[tσ] containing a substitution instance of t. For this purpose, we employ tree automata as certificates of non-termination. For proving non-termination of a term rewriting system R, we search a tree automaton A whose language L(A) is not empty, weakly closed under rewriting and every term of the language contains a redex occurrence. We have fully automated the search for these certificates employing SAT-solvers. All automata that we use as example in this paper have been found automatically; this concerns in particular fully automated proofs of non-termination for the following two rewrite systems. Example 1. We consider the following string rewriting system: This rewrite system admits no reductions of the form s → * sr.

Example 2.
We consider the S-rule from combinatory logic: For the S-rule it is known that there are no reductions t → * C[t] for ground terms t, see [15]. For open terms t the existence of reductions t → * C[tσ] is open.
It turns out that the method can be fruitfully applied to obtain non-termination proofs of several string rewriting systems that have remained unsolved in the last full run of the termination competition.

Related Work
The paper [11] investigates necessary conditions for the existence of loops. The work [17] employs SAT solvers to find loops, [18] uses forward closures to find loops efficiently, and the wook [16] introduces 'compressed loops' to find certain forms of (possibly very long) loops.
Non-termination beyond loops has been investigated in [14] and [2]; we note that Example 2 cannot be handled by these techniques.
Here we prove non-looping non-termination on regular languages. The converse, local termination on regular languages, has been investigated in [3]. Regular (tree) automata have been fruitfully applied to a wide rage of properties of term rewriting systems: for proving termination [10,8,12], for infinitary normalization [4], for proving liveness [13], and for analysing reachability and deciding the existance of common reducts [9,5].

2
Non-termination and Weakly Closed Languages Definition 3. Let L ⊆ T (Σ, ∅) a language and R a TRS over Σ. Then L is called: closed under rewriting if for every t ∈ L and s such that t → s, one has s ∈ L, and weakly closed under rewriting if for every t ∈ L that is not in normal form, there exists s ∈ L such that t → R s.
The following theorem describes the basic idea that we employ for proving non-termination.

Theorem 4. A term rewriting system R over Σ is non-terminating if and only if there exists a non-empty language
(i) every t ∈ L contains a redex (that is, t → s for some term s), and (ii) L is weakly closed under rewriting. A language fulfilling the properties of Theorem 4 is also called a recurrence set, see [1].
To automate this method, we need to restrict to a certain family of languages. In this paper, we consider regular tree languages. To guarantee that the language of a tree automaton is weakly closed under rewriting, we check that the language is not empty and that the automaton is a quasi-model (see Definition 13) for the rewrite system. The latter condition is actually too strict; it implies that the languages is not only weakly closed, but also closed under rewriting. In future, we plan to relieve this restriction.

3
Tree Automata In examples, we often write the transition relation δ f as → f . Example 6. The following is a tree automaton for the signature in Example 1. We consider string rewriting systems as term rewriting systems by interpreting all symbols as unary and adding a special constant ε to denote the end of the word. Let The transition relation for ε can be thought of as defining the initial states (here 0) of a word automaton.

Example 7.
The following is a tree automaton for Example 2.
In Example 12 we show that this automaton accepts the term SSS(SSS)(SSS(SSS)).

Actually, it suffices to check the property [ , α] A ⊆ [r, α]
A for assignments α : X → P(Q) that map variables to singleton sets.

Lemma 14. A tree automaton
Example 15. It is not difficult to check that the automaton A LR from Example 6 is a quasi-model for rewrite system in Example 1.

Example 16.
We consider the automaton A S from Example 7. We write (a, b, c) The interpretation [r, α] has all the above and additionally: As a consequence A S is a quasi-model for the S-rule.
The following theorem is immediate: Theorem 17. Let A = Q, Σ, F, δ be a tree automaton and R a term rewriting system over Σ. If A is a quasi-model for R then the language of A is closed under rewriting.

Ensuring Redex Occurrences
Next, we want to guarantee that every term in the language L(A) of an automaton A contains a redex with respect to the term rewriting system R. For left-linear systems R, this problem can be reduced to deciding the inclusion of regular languages. Let R be a left-linear term rewriting system. Then the set of ground terms containing a redex is a regular tree language. A deterministic automaton B for this language can be constructed using the overlap-closure of subterms of left-hand sides, see further [6,7].
As a consequence the problem of checking whether every term in L(A) contains a redex boils down to checking that L(A) ⊆ L(B). For non-deterministic A and deterministic B, this property can be decided by constructing the product automaton and considering the reachable states.
The following theorem gives a method for checking L(A) ⊆ L(B) without the need for determinising A (only B needs to be deterministic).
Theorem 21. Let A = Q, Σ, F, δ and B = Q , Σ, F , δ be tree automata such that B is deterministic. Let S be the set of reachable states of the product automaton A · B. Then L(A) ⊆ L(B) if and only if for all (q, p) ∈ S it holds that q ∈ F =⇒ p ∈ F . Example 22. The reachable states of product automaton A S · C of the automata A S from Example 7 and C from Example 18 are (0, 0), (1, 1), (2, 2), (2, 1), (3,3), (3,2), (2,3), (4,3). The only state (q, q ) such that q is accepting in A S is (4, 3) and 3 is an accepting state of C. Thus the conditions of Theorem 21 are fulfilled and hence L(A S ) ⊆ L(C). Thus every term accepted by A S contains a redex.