An Automated Approach to the Collatz Conjecture

Emre Yolcu; Scott Aaronson; Marijn J. H. Heule

doi:10.1007/s10817-022-09658-8

An Automated Approach to the Collatz Conjecture

Yolcu, Emre; Aaronson, Scott; Heule, Marijn J. H. 2023-06-01 00:00:00 We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary–ternary representations of positive integers. We prove that the termination of this rewriting system is equivalent to the Collatz conjecture. We also prove that a previously studied rewriting system that simulates the Collatz function using unary representations does not admit termination proofs via natural matrix interpretations, even when used in conjunction with dependency pairs. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses natural/arctic matrix interpretations and we ﬁnd automated proofs of nontrivial weakenings of the Collatz conjecture. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach. Keywords String rewriting · Termination · Matrix interpretations · SAT solving · Collatz conjecture · Computer-assisted mathematics Emre Yolcu eyolcu@cs.cmu.edu Scott Aaronson scott@scottaaronson.com Marijn J. H. Heule marijn@cmu.edu Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA Department of Computer Science, University of Texas at Austin, Austin, TX, USA 0123456789().: V,-vol 123 15 Page 2 of 44 E. Yolcu et al. × × × 2 1 1 × + × × + × 2 1 1 3 2 1 × × × × 2 3 3 2 × × + × × + 2 3 1 3 2 1 ×2 ×3 +2 ×3 +1 ×2 × + × × + × + 2 1 3 3 1 2 1 × + × + × + × 2 1 3 1 3 2 2 × + × + × + × + 2 1 3 2 3 2 2 1 × × + 1 3 1 2 1 × + × × 1 3 1 1 2 2 × + × × + 1 3 2 1 2 2 1 × + × × + × × + × 1 3 2 3 3 2 3 3 2 1 × × + × × + × × + × 1 2 2 1 3 3 2 3 3 2 1 × × + × + × + × × + × 1 2 3 1 2 1 3 2 3 3 2 1 1 ×2 ×3 +1 ×3 +2 ×2 +1 ×3 ×3 +2 ×1 × × + × + × + × + × + × 1 2 3 1 3 2 3 1 2 1 3 2 1 × × + × + × + × + × + × 1 2 3 1 3 2 3 1 3 2 2 1 1 × × + × + × + × + × + × 1 2 3 1 3 2 3 1 3 2 3 2 1 × × + × + × + × + × + × 1 3 2 1 3 2 3 1 3 2 3 2 1 × × + × + × + × + × + × 1 3 3 2 2 1 3 1 3 2 3 2 1 × × + × + × × + × + × 1 3 3 2 3 2 2 3 2 3 2 1 × × + × + × + × × + × 1 3 3 2 3 2 3 1 2 3 2 1 1 ×3 ×3 +2 ×3 +2 ×3 +1 ×3 +1 ×2 ×1 × × + × + × + × + × 1 3 3 2 3 2 3 1 3 1 1 Diagrammatic view of the Collatz trajectory of 27. Each row in the cascade is a mixed binary–ternary repre- sentation of an iterate, with each box corresponding to a digit. Rewrite rules are shown at the top right corner. The zoomed-in slice at the bottom left corner highlights the intermediate rewrite steps performed to change the least signiﬁcant digit into binary while preserving the numeric value of the representation. 123 Automated Approach to Collatz Conjecture Page 3 of 44 15 1 Introduction Let N ={0, 1, 2,... } denote the natural numbers and N ={1, 2, 3,... } denote the positive + + integers. We deﬁne the Collatz function C : N → N as n/2if n ≡ 0 (mod 2) C (n) = 3n +1if n ≡ 1 (mod 2). Given a function f and a number k ∈ N, the function f denotes the kth iterate of f ,deﬁned as f := f ◦ f ◦ ··· ◦ f . The well-known Collatz conjecture is the following: k times + k Conjecture 1.1 For all n ∈ N , there exists some k ∈ N such that C (n) = 1. This is a longstanding open problem and there is a vast literature dedicated to its study. For its history and comprehensive surveys on the problem, we refer the reader to Lagarias [1–3]. See also the work by Tao [4] for dramatic recent progress on the problem. Deﬁnition 1.2 (Convergent function) Consider a function f : X → X and a designated N 2 element z ∈ X.Given x ∈ X, the sequence of iterates f (x ) := (x , f (x ), f (x), ...) is called the f -trajectory of x. If the trajectory f (x ) reaches a cycle containing z, the trajectory is convergent to z for x.Iffor all x ∈ X the trajectory f (x ) is convergent to z, the function f is convergent to z. As of 2020, it has been checked by computation that for all n ≤ 2 the Collatz trajectory of n is convergent [5]. This fact, along with the heuristic argument that on average the iterates in a trajectory tend to decrease [6], is often used as evidence to support the belief that the conjecture is true. On a different note, Conway proved that a generalization of the problem is undecidable [7], which Kurtz and Simon later extended to a variant even closer to the Collatz conjecture [8]. While the prevailing opinion is that the Collatz conjecture holds, and the heuristic arguments suggest that an average trajectory is convergent, the undecidability results help explainwhy this seemstobesohardtoshow. In this paper, we describe an approach based on termination of string rewriting to auto- matically search for a proof of the Collatz conjecture. Although trying to prove the Collatz conjecture via automated deduction is clearly a moonshot goal, there are two recent techno- logical advances that provide reasons for optimism that at least some interesting variants of the problem might be solvable. First, the invention of the method of matrix interpretations [9, 10] and its variants such as arctic interpretations [11, 12] turns the quest of ﬁnding a ranking function to witness termination into a problem that is suitable for systematic search. Second, the progress in satisﬁability (SAT) solving makes it possible to solve many seemingly difﬁcult combinatorial problems efﬁciently in practice. Their combination, i.e., using SAT solvers to ﬁnd interpretations, has so far been an effective strategy in solving challenging termination problems. We make the following contributions: • We show how a generalized Collatz function can be expressed as a rewriting system that is terminating if and only if the function is convergent. For the functions we deﬁne throughout this paper, the designated element z is clear from the context, so we refer to convergence without explicitly mentioning z. It is also apparent in all cases that z is in a cycle, and we simply call a trajectory convergent if it contains z. See https://pcbarina.ﬁt.vutbr.cz for David Barina’s ongoing veriﬁcation effort. 123 15 Page 4 of 44 E. Yolcu et al. • We prove that no termination proof via natural matrix interpretations exists for a certain system by Zantema [13] that simulates the Collatz function using unary representations of numbers. This result holds even when natural matrix interpretations are used in con- junction with the dependency pair transformation [14]. • We show that translations into rewriting systems that use non-unary representations of numbers are more amenable to automated methods, compared with the previously and commonly studied unary representations. • We automatically prove various weakenings of the Collatz conjecture. We observe that, for some of these weakenings, the only matrix interpretations that our termination tool was able to ﬁnd involved relatively large matrices (of dimension 5). Existing termination tools often limit their default strategies to search for small interpretations as they are tailored for the setting where the task is to quickly solve a large quantity of relatively easy problems. We make the point that, given more resources, the method of matrix interpretations has the potential to scale. • We observe that the phase-saving heuristic used by default in modern SAT solvers can degrade the performance of CDCL (conﬂict-driven clause learning) solvers [15]onfor- mulas encoding the existence of matrix interpretations, whereas using negative branching can improve solver performance. In Appendix C, we present adaptations of our rewriting system that allow reformulating several more open problems in mathematics as termination problems of small size. This article is an extended version of our CADE 2021 paper [16]. In addition to several small improvements throughout the article, we expanded Section 2 with extra background material to make the article more self-contained and accessible for nonexperts in rewriting. We included additional examples throughout, provided more detailed proofs especially for the main contributions in Section 3.2, and discussed several remarks in more detail. We included the additional Section 3.1.1 where we prove the nonexistence of proofs via natu- ral matrix interpretations for the rewriting system that uses unary representations. We also included Section 4.6 where we discuss the SAT solving aspect of termination proving in detail and provide experimental comparisons of the effectiveness of various heuristics in ﬁnding interpretations. 2 Preliminaries 2.1 String Rewriting Systems We brieﬂy review the notions related to string rewriting that are used in the rest of the paper. We adopt the notation of Zantema [13] and Endrullis et al. [10]. For a comprehensive introduction to string or term rewriting, see Book and Otto [17] or Baader and Nipkow [18], respectively. Deﬁnition 2.1 (String rewriting system) Let be an alphabet, i.e., a set of symbols. A string ∗ ∗ rewriting system (SRS) over is a relation R ⊆ × .Elements (, r ) ∈ R are called rewrite rules and are usually written as → r. The system R induces a rewrite relation ∗ ∗ → := {(st , srt ) | s, t ∈ , → r ∈ R} on the set of strings. Deﬁnition 2.2 (Termination) A relation → on A is terminating if there is no inﬁnite sequence s , s ,... ∈ A such that s → s for all i ≥ 0. A terminating relation is also commonly 0 1 i i +1 called Noetherian, well-founded, or strongly normalizing. We write SN(→) to denote that → is terminating. 123 Automated Approach to Collatz Conjecture Page 5 of 44 15 We often conﬂate an SRS R with the rewrite relation it induces when discussing termi- nation. In particular, we write “R is terminating” instead of “→ is terminating”. We also often do not specify the alphabet and take it to be the set of all the symbols that appear in a given rewriting system. Example 2.3 1. R ={aa → a} is terminating, which is proved easily by observing that each rewrite decreases the length of a string by 1. 2. R ={a → aa} is not terminating, since even a single occurrence of a allows indeﬁnitely producing more of the symbol a. 3. R ={ab → ba} is terminating, since all rewrite sequences eventually convert a given ∗ ∗ string into the form b a and stop. An example sequence is shown below, with the under- lines indicating the substrings that the rules are applied to. abbab → babab → bbaab → bbaba → bbbaa R R R R 3 3 3 3 A useful generalization of termination is relative termination: Deﬁnition 2.4 (Relative termination) Let → , → be relations on A.Then → is said to be 1 2 1 terminating relative to → if there is no inﬁnite sequence s , s ,... ∈ A such that 2 0 1 • s → s for inﬁnitely many values of i, i 1 i +1 • s → s for all other values of i. i 2 i +1 We write SN(→ / → ) to denote that → is terminating relative to → . 1 2 1 2 Equivalently, R is said to be terminating relative to S if every sequence of rewrites for the system R ∪ S applies the rules from R at most ﬁnitely many times. Note that we have SN(R / ∅) = SN(R) by the deﬁnition, so relative termination is indeed a generalization. Example 2.5 Let R ={aa → aba} and S ={b → bb}. The system R ∪ S is not terminating since S gives way to inﬁnite rewrite sequences; however, R is terminating relative to S because R by itself is terminating and applying the rule b → bb does not facilitate further applications of the rule aa → aba. Relative termination allows proofs of termination to be broken into steps as codiﬁed by the following theorem. Theorem 2.6 (Rule removal [13, Theorem 1]) Let R be an SRS. If there exists a subset T ⊆ R such that SN(T / R) and SN(R \ T ),then SN(R). This theorem allows us to “remove rules” in the following way. When proving SN(R), if we succeed at ﬁnding a subset T satisfying SN(T / R), the proof obligation becomes weakened to SN(R \ T ), where the rules of T are no longer present. This removal of rules can be repeated until no rules remain, thus producing a stepwise proof of termination. Another useful technique is reversal: Deﬁnition 2.7 (Reversal) Let s = s ... s ∈ be a string and R be an SRS. Letting 1 n rev rev rev rev s := s ... s ,the reversal of R is deﬁned as R := { → r | → r ∈ R}. n 1 Lemma 2.8 (Rule reversal [13, Lemma 2]) Let R, Sbe SRSs. Then, SN(R / S) if and only if rev rev SN(R / S ). 123 15 Page 6 of 44 E. Yolcu et al. Reversal is of interest because methods for proving termination are not necessarily invari- ant under reversal, that is, a given technique may fail to show the termination of a system R rev while succeeding for its reversal R . Yet another important notion is top termination: Deﬁnition 2.9 (Top termination) Let R be an SRS over .The top rewrite relation induced by R is deﬁned as → := {(s, rs) | s ∈ , → r ∈ R}.If → is terminating, R is R R top top said to be top terminating. In plain language, top termination allows rewrites to be performed only at the leftmost end of a string, so it requires a condition less strict than that of termination. As we will see in the next section (Theorem 2.15), top termination problems can admit proofs of a more relaxed form compared with termination. Relative top termination, i.e., proving SN(R / S) for SRSs R and S, is a crucial compo- top nent in the dependency pair approach [14], which reduces a termination problem to a relative top termination problem that often ends up being easier to solve via automated methods com- pared with the original problem. In order to avoid requiring familiarity with the dependency pair approach, we omit its discussion and instead prove a self-contained result (Lemma 3.18) that encapsulates dependency pairs in a more elementary manner for the speciﬁc rewriting systems that we consider in this paper. 2.2 Interpretation Method Let R be an SRS over the alphabet . The main idea when proving termination is to show ∗ ∗ that there exists a well-founded (strict) order > on such that, for all strings s, t ∈ , if s → t then s > t. When this is the case, R is terminating since any rewrite causes a “strict decrease” with respect to > and by its well-foundedness there cannot exist an inﬁnitely decreasing sequence. The condition over inﬁnitely many strings can be replaced by another one that involves only the rules of R by employing a reduction order [18, Section 5.2]; [17, Section 2.2]. Deﬁnition 2.10 (Reduction order) Let > be a well-founded order on .Iffor all s, t , p, q ∈ , s > t implies psq > ptq,then > is called a reduction order. Theorem 2.11 ([18, Theorem 5.2.3]; [17, Theorem 2.2.4]) Let R be an SRS over the alphabet . The system R is terminating if and only if there exists a reduction order > on such that > r holds for all → r ∈ R. The interpretation method is a particular way of deﬁning a reduction order. Instead of considering the strings directly, we interpret each symbol σ ∈ as a function [σ ]: A → A, where A is some carrier set, for example of natural numbers or vectors, and we extend this interpretation from symbols to strings s = s ... s ∈ as [s]:=[s ] ◦ ··· ◦ [s ]. When the 1 n 1 n domain A is already equipped with a well-founded order >, we can deﬁne a well-founded order > on by s > t if and only if [s](x)> [t ](x ) for all x ∈ A, (1) where A = (A, [·] ,>) is a structure with [·] := {[σ]| σ ∈ } denoting the collection of interpretations. For appropriately chosen interpretations, > ends up being a reduction order: 123 Automated Approach to Collatz Conjecture Page 7 of 44 15 Theorem 2.12 ([18, Theorem 5.3.3]) Let be an alphabet and let > be a well-founded order on A. If for all symbols σ ∈ the interpretation [σ ]: A → A is monotone with respect to >,then > as deﬁned in (1) is a reduction order on . Thus, after ﬁxing (A,>), proving termination reduces to ﬁnding suitable (monotone) interpretations of the symbols as functions [for details see 18, Section 5.3]. As a concrete example, here is a simple proof of termination via the interpretation method. Example 2.13 Recall R ={ab → ba} from Example 2.3 with ={a, b}.Fix (N ,>) with the usual order on positive integers, which is well-founded by the well-ordering principle. 2 + Let [a](x ) = x and [b](x ) = x + 1. Denote N = (N , {[a], [b]},>). Both functions are ∗ ∗ monotone with respect to >, so by Theorem 2.12 the relation > ={(s, t ) ∈ × | [s](x)> [t ](x ) for all x ∈ N } is a reduction order. For the rule ab → ba,since 2 2 ([a]◦[b])(x ) = (x + 1) > x + 1 = ([b]◦[a])(x ) holds for all x ∈ N ,wehave ab > ba. Thus, by Theorem 2.11 the SRS R is terminating. N 3 In order to use the interpretation method for relative termination (resp. top termination), the above ideas can be generalized in the form of extended (resp. weakly) monotone algebras [10]. Deﬁnition 2.14 (Extended/weakly monotone algebra) Let • be an alphabet, • A aset, •[σ ]: A → A an interpretation for every σ ∈ , • > and order relations over A such that > is well-founded and satisﬁes > · ⊆ >. Letting [·] ={[σ]| σ ∈ }, the structure (A, [·] ,>, ) is a weakly monotone -algebra if for every σ ∈ the interpretation [σ ] is monotone with respect to .Itisan extended monotone -algebra if, additionally, for every σ ∈ the interpretation [σ ] is monotone with respect to >. Relative termination (resp. top termination) is characterized as the existence of extended (resp. weakly) monotone algebras. Theorem 2.15 ([10, Theorem 2]) Let R and S be SRSs over the alphabet .Wehave SN(R/S) (resp. SN(R / S)) if and only if there exists an extended (resp. weakly) monotone -algebra top (A, [·] ,>, ) such that • for each rule → r ∈ R we have [](x)> [r ](x ) for all x ∈ A, • for each rule → r ∈ S we have [](x ) [r ](x ) for all x ∈ A. An effective way to automatically prove relative termination (or top termination) is to try to satisfy the conditions of the above theorem by ﬁxing (A,>, ) and algorithmically searching for appropriate interpretations of the symbols. Matrix interpretations is a speciﬁc instance of this generic method. In the following section we describe (at a high level) the method of matrix interpretations. For more details and background, we refer the reader to existing work [9–12]. It may seem an odd choice to focus on matrix interpretations and implement our own prover given that there is a wealth of other techniques for proving termination that are Termination is in fact equivalent to the existence of such interpretations [19, Proposition 1]. 123 15 Page 8 of 44 E. Yolcu et al. already implemented in the existing tools (e.g., AProVE [20], Matchbox [21], T T [22]). We T 2 did experiment with other methods; however, at least for the rewriting systems of the speciﬁc form in this paper it appears that the method of matrix interpretations is the most effective. For instance, one of the most difﬁcult instances in this paper (in the sense of the smallest proof of termination that we could ﬁnd) appears to require arctic matrix interpretations in all the proofs that we (and the authors of AProVE and Matchbox) could ﬁnd. (There remain some versions of matrix interpretations that we have not yet experimented with [23, 24].) Additionally, we chose to implement our own minimal prover to have ﬁner control over the SAT solving aspect of the search for an interpretation. We give a summary of our ﬁndings regarding this topic in Section 4.6. 2.3 Natural/Arctic Matrix Interpretations 2.3.1 Natural Numbers Let R be an SRS over the alphabet .Fix adimension d ∈ N . In the method of natural d d matrix interpretations [10]weset A = N and deﬁne, for vectors x, y ∈ N , x > y ⇐⇒ x > y ∧ x ≥ y for all i ∈{2,..., d}, 1 1 i i x y ⇐⇒ x ≥ y for all i ∈{1,..., d}. i i d d For interpreting each symbol σ ∈ , we consider an afﬁne function [σ ]: N → N : [σ ](x) = M x + v σ σ In this way, the structure (N , [·] ,>, ) satisﬁes the requirements of Deﬁnition 2.14 for a weakly monotone algebra. Additionally setting (M ) = 1 satisﬁes the requirements for σ 1,1 an extended monotone algebra. Furthermore, since the composition of afﬁne functions is afﬁne, for all s ∈ there d×d d exist M ∈ N , v ∈ N such that [s](x) = M x + v . As a result, given a collection s s s s [·] of natural matrix interpretations, the conditions of Theorem 2.15 can be checked by computing for each rule → r ∈ R the corresponding matrices M , M and vectors v , v r r d×d and comparing them elementwise [10,Lemma 4].Extend to matrices M, N ∈ N as M N ⇐⇒ M ≥ N for all i , j ∈{1,..., d}. i , j i , j Then, we have M M ∧ v > v ⇐⇒ [](x)> [r ](x) for all x ∈ N , r r M M ∧ v v ⇐⇒ [](x) [r ](x) for all x ∈ N . (2) r r This shows that it is decidable to check whether a given collection of interpretations of the form considered here constitutes a proof of termination. Example 2.16 Recall R ={aa → aba} and S ={b → bb} from Example 2.5 with ={a, b}. The following functions constitute a matrix interpretations proof that shows SN(R / S). 11 0 10 0 [a](x) = x + [b](x) = x + 00 1 00 0 123 Automated Approach to Collatz Conjecture Page 9 of 44 15 It is easy to check that the above interpretations give an extended monotone algebra and that they satisfy the below relations for all x ∈ N , which implies SN(R / S) via Theorem 2.15. 11 1 11 0 [aa](x) = x + > x + =[aba](x) 00 1 00 1 10 0 10 0 [b](x) = x + x + =[bb](x) 00 0 00 0 In order to automate the search for matrix interpretations given a rewriting system R, an approach that turns out to be effective is to encode all of the aforementioned constraints as a propositional formula in conjunctive normal form and use a SAT solver to look for a satisfying assignment. This additionally involves ﬁxing a ﬁnite domain for the coefﬁcients that can occur in the interpretations and encoding arithmetic over the chosen ﬁnite domain using propositional variables. (We discuss our choice of encoding in Section 4.6.) 2.3.2 Arctic Integers Natural matrix interpretations can also be adapted to the max–plus algebra of arctic natural numbers A = N∪{−∞} or arctic integers A = Z∪{−∞} as coefﬁcients. This adaptation N Z enables termination proofs in some cases where either there is no other automated method that leads to a proof or only relatively complicated proofs are known [11]. Let R be an SRS over the alphabet ,and let A be either one of A or A . In the method of N Z arctic matrix interpretations [11, 12] we use the arctic semiring (A, ⊕, ⊗), with the following operations: x ⊕ y = max{x , y} x ⊗ y = x + y Let > and ≥ denote the usual order relations over integers. Adopting the conventions that Z Z x > −∞ for all x ∈ Z and that −∞ ≥ −∞,wedeﬁne,for x , y ∈ A, Z Z x y ⇐⇒ x > y ∨ x = y =−∞, x ≥ y ⇐⇒ x ≥ y. We ﬁx a dimension d ∈ N and we extend both and ≥ to arctic vectors and arctic matrices elementwise. As these deﬁnitions allow −∞ −∞, the order is not well-founded. To d−1 ensure well-foundedness of we restrict the domain to N × A . Then, for interpreting d d each symbol σ ∈ , we consider an afﬁne function [σ ]: A → A , written as [σ ](x) = M ⊗ x ⊕ v , σ σ d−1 where we require (M ) ≥ 0or (v ) ≥ 0 to ensure that [σ ](z) ∈ N × A for z ∈ σ 1,1 σ 1 d−1 d−1 N × A . In this way, the structure (N × A , [·] , , ≥) satisﬁes the requirements of Deﬁnition 2.14 for a weakly monotone algebra. Additionally choosing A = A and setting each v to be the −∞ vector (consequently enforcing (M ) ≥ 0) satisﬁes the σ σ 1,1 requirements for an extended monotone algebra. This means that arctic integers (as opposed to arctic natural numbers) and vectors that contain ﬁnite elements (i.e., not all −∞)are used only when proving top termination. The name “arctic” was chosen to contrast with the min–plus algebra of the “tropical” semiring. 123 15 Page 10 of 44 E. Yolcu et al. As the composition of afﬁne functions over arctic vectors is afﬁne, given a collection [·] of arctic matrix interpretations we can compute for each rule → r ∈ R the corresponding arctic matrices M , M and arctic vectors v , v . Elementwise comparisons of these matrices r r and vectors give sufﬁcient conditions for the inequalities in Theorem 2.15. In particular, due to Koprowski and Waldmann [11,Lemma 6.5],wehave M M ∧ v v ⇒ [](x) [r ](x) for all x ∈ A , r r M ≥ M ∧ v ≥ v ⇒ [](x) ≥[r ](x) for all x ∈ A . r r Thus, the search for arctic matrix interpretations can be automated in a manner similar to natural matrix interpretations by encoding the aforementioned constraints as a SAT instance. Example 2.17 Let P denote the following SRS . b → ax aax → bxa ab → ba xb → ax a → ax As an example of the different capabilities of arctic versus natural matrix interpretations, consider trying to prove the relative termination statement SN({b → ax} / P). To our knowledge, there is no direct proof of this statement via natural matrix interpretations although there is one via the 4-dimensional arctic matrix interpretations below. In the inter- pretations, − indicates −∞, and the multiplication operator ⊗ as well as the vectors of all −∞s are omitted. ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 11 − 0 11 − 0 −− 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [a](x) = x [b](x) = x [x](x) = x ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ − 0 −− 10 1 − −−− 0 −− 0 − −− 0 − − 0 −− ⎡ ⎤ ⎡ ⎤ 0 − 0 − 0 −−− ⎢ ⎥ ⎢ ⎥ −−−− −−−− ⎢ ⎥ ⎢ ⎥ [](x) = x [](x) = x ⎣ ⎦ ⎣ ⎦ −−−− −−−− −−−− −−−− With the above interpretations, the rules of P satisfy the following relations, which, by Theorem 2.15, proves that {b → ax} is terminating relative to P. ⎡ ⎤ ⎡ ⎤ 10 1 − 0 − 0 − ⎢ ⎥ ⎢ ⎥ −−−− −−−− ⎢ ⎥ ⎢ ⎥ [b](x) = x x =[ax](x) ⎣ ⎦ ⎣ ⎦ −−−− −−−− −−−− −−−− ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 21 20 11 − 0 ⎢ ⎥ ⎢ ⎥ [aax](x) = x ≥ x =[bxa](x) ⎣ ⎦ ⎣ ⎦ 10 1 − 10 1 − −− 0 − −− 0 − This SRS simulates the Abelian sandpile model [25] over an inﬁnite path. The symbols , x, represent the vertices on the path. At each instant, the weight of a vertex is identiﬁed by the number of asand bs to its left until the next occurrence of a vertex symbol. 123 Automated Approach to Collatz Conjecture Page 11 of 44 15 ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 2201 2201 ⎢ ⎥ ⎢ ⎥ [ab](x) = x ≥ x =[ba](x) ⎣ ⎦ ⎣ ⎦ 11 − 0 11 − 0 10 1 − − 0 −− ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 10 1 − 10 1 − ⎢ ⎥ ⎢ ⎥ [xb](x) = x ≥ x =[ax](x) ⎣ ⎦ ⎣ ⎦ −− 0 − −− 0 − 11 − 0 −−− 0 ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 1 −−− 1 −−− ⎢ ⎥ ⎢ ⎥ [a](x) = x ≥ x =[ax](x) ⎣ ⎦ ⎣ ⎦ −−−− −−−− −−−− −−−− 2.4 Generalized Collatz Functions We consider instances of the following generalization of the Collatz function. Its variants have commonly appeared in the literature [6, 26–31]. Deﬁnition 2.18 (Generalized Collatz function) Let X be one of N, N ,or Z and deﬁne X := X ∪{⊥}. A function f : X → X is a generalized Collatz function if f (⊥) =⊥ ⊥ ⊥ ⊥ andthere existaninteger d ≥ 2 and rational numbers q ,..., q , r ,..., r such that 0 d−1 0 d−1 for all 0 ≤ i ≤ d − 1and all n ∈ X, we have a deﬁnition either of the form f (n) = q n + r if n ≡ i (mod d), i i or of the form f (n) =⊥ if n ≡ i (mod d). In the above deﬁnition, we allow the representation of a partially deﬁned function by mapping to ⊥ in the undeﬁned cases. We call a partial f convergent if all f -trajectories contain ⊥. Note that the Collatz function corresponds to the case d = 2, q = 1/2, r = 0, q = 3, 0 0 1 r = 1. Although the Collatz function is by far the most widely studied case, there are several other concrete examples of generalized Collatz functions the convergence of which is worth studying due to their connections to open problems in number theory and computability theory. We discuss these cases in Appendix C. 3 Rewriting the Collatz Function We start our discussion with systems that use unary representations and then demonstrate via examples that mixed-base representations can be more suitable for use with automated methods. 3.1 Rewriting in Unary The following system of Zantema [13] simulates the iterated application of the Collatz func- tion to a number represented in unary, and it terminates upon reaching 1. 123 15 Page 12 of 44 E. Yolcu et al. Example 3.1 Z denotes the following SRS, consisting of 5 symbols and 7 rules. h11 → 1h 11h → 11s h1 → t11 1s → s1 1t → t111 s → h t → h This system can be seen as encoding the execution of a Turing machine with cells that can be contracted/expanded. The symbols 1 and (blank) form the tape alphabet, while the symbols h (half), s (shift), t (triple) indicate the head along with the state of the machine. Through the following result, the Collatz conjecture can be reformulated as termination of string rewriting. Theorem 3.2 ([13, Theorem 16]) Z is terminating if and only if the Collatz conjecture holds. 2n ∗ n While the forward direction of the above theorem is easy to see (since h1 → h1 2n+1 ∗ 3n+2 for n > 1and h1 → h1 for n ≥ 0), the backward direction is far from obvious because not every string corresponds to a valid conﬁguration of the underlying machine. As another example, consider the system below, which follows a theme similar to Example 3.1. Example 3.3 W denotes the following SRS, consisting of 4 symbols and 4 rules. h11 → 1h 1h → 1t 1t → t111 t → h Johannes Waldmann shared the above system (originally due to Zantema ) with us, men- tioning that its termination has yet to be proved via automated methods. Nevertheless, there is a simple reason for its termination: It simulates the iterated application of a partial generalized + + Collatz function W : N → N deﬁned as follows, which is easily seen to be convergent. ⊥ ⊥ 3n/2if n ≡ 0 (mod 2) W (n) = ⊥ if n ≡ 1 (mod 2) 3.1.1 Nonexistence of Proofs via Natural Matrix Interpretations Natural matrix interpretations cannot be used to directly remove any of the rules from the above kind of unary rewriting systems that simulate certain maps, in particular the Collatz function. Deﬁnition 3.4 (N-rational sequence) A sequence x , x ,... ∈ N is called N-rational if there 1 2 d×d d exists a matrix M ∈ N and vectors v, w ∈ N of some dimension d such that, for all n, T n we have x = v M w. The following is a consequence of Berstel’s theorem [32, Theorem 8.1.1]. (See also the remark by Soittola [33, page 318].) Theorem 3.5 Let x , x ,... be an N-rational sequence. Then there exist m, p ∈ N such 1 2 that, for all j ∈{0, 1,..., p − 1}, each of the subsequences {x } has its nth m+kp+ j k=0 https://www.lri.fr/~marche/tpdb/tpdb-2.0/SRS/Zantema/z079.srs 123 Automated Approach to Collatz Conjecture Page 13 of 44 15 element equal to (1 + o(1))P(n)α for some nonzero polynomial P and a constant α> 0. In particular, each of these subsequences is monotonically nondecreasing after some ﬁnite point. Corollary 3.6 There exists no N-rational sequence x , x ,... satisfying x > x for 1 2 8n+1 9n+2 all n. Proof Let p be as in Theorem 3.5, and consider n of the form qp − 1 for some large enough q.Then (9n +2)−8n +1 = n +1 = qp,so x and x belong to the same subsequence. 8n+1 9n+2 This means that for all sufﬁciently large n of this form, we must have x ≤ x . 8n+1 9n+2 To make use of the above facts in ruling out the existence of natural matrix interpretations of the form described in Section 2.3.1, we also need the following result proving that we can work with interpretations that are purely linear (instead of afﬁne) by moving up to a higher dimension. Theorem 3.7 ([10, Theorem 6]) Let R be an SRS over the alphabet , and let [σ ](x) = M x + v denote a d-dimensional afﬁne interpretation for each σ ∈ . Deﬁne a (d + 1)- σ σ dimensional linear interpretation for each σ ∈ as M v + σ σ [σ ] (x) := D x = x, σ T 0 1 where 0 denotes the d-dimensional zero vector. For each rule → r ∈ R, let M , M , v , v , r r D , D denote the matrices and the vectors occurring in the corresponding interpretations (as obtained by composing the interpretations of the symbols). If we have M M and v v ,then D D . Additionally, if v > v ,then (D ) >(D ) . r r r 1,d+1 r 1,d+1 In informal terms, the above theorem states that if we have a collection of afﬁne interpre- tations to remove a rule from a system (due to the strict decrease across the ﬁrst elements of the corresponding two vectors), then there is also a collection of purely linear interpretations such that the top-right elements decrease strictly across the two matrices corresponding to this rule. With this fact at hand, we can prove the following. Theorem 3.8 Let ={1, , h, s, t}. There exists no collection [·] of natural matrix interpretations of any dimension d satisfying the requirements for an extended monotone -algebra such that • for at least one rule → r ∈ Z we have [](x)> [r ](x) for all x ∈ N , and • for the remaining → r ∈ Z we have [ ](x) [r ](x) for all x ∈ N . Proof Assume for a contradiction that such a collection of natural matrix interpretations exists for some dimension d − 1, with each symbol σ ∈ interpreted as [σ ](x) = M x + v and σ σ each matrix D deﬁned as in Theorem 3.7.Let → r ∈ Z be a rule for which [](x)> [r ](x) d−1 for all x ∈ N , and denote ρ ={ → r }. As the interpretations satisfy the requirements for ∗ d−1 extended monotonicity, for all s, t ∈ ,if s → t,then [s](x)> [t ](x) for all x ∈ N . This conclusion implies by (2)that M M and v > v , which, by Theorem 3.7,further s t s t imply D D and (D ) >(D ) . Thus, for all s, t ∈ , s t s 1,d t 1,d s → t ⇒ D D and (D ) >(D ) . (3) ρ s t s 1,d t 1,d We thank Gjergji Zaimi for this argument (see https://mathoverﬂow.net/a/270372). 123 15 Page 14 of 44 E. Yolcu et al. In Zantema’s system Z, we can represent an arbitrary integer k by the string h1 , interpreted as k k h1 (x) = D D D x. Let e ∈ N denote the ith standard basis vector, i.e., with 1 at the ith position and 0s elsewhere. Deﬁne T k f (k) := e h1 (e ) T k = e (D D D )e h d 1 1 (4) T k = (e D )D (D e ) h d 1 1 T k = v D w, where v = D e and w = D e are ﬁxed, so f (1), f (2), ... is an N-rational sequence. 1 d Now, since the system Z simulates the Collatz function (with the odd case incorporating an additional division by 2), for all numbers of the form 8n + 1 it can simulate the sequence of mappings 8n + 1 → 12n + 2 → 6n + 1 → 9n + 2 that results from applying the Collatz map three times. Thus, for all n,wehave 8n+1 ∗ 9n+2 h1 → h1 , which crucially requires the use of every single rule in Z (as it involves applying both m → m/2and m → (3m + 1)/2). This implies in particular that the rule → r is used in the above derivation. Recall also that the interpretations of all rules in Z are at least 8n+1 nonstrictly decreasing by assumption. This means along with (3) that, letting s = h1 9n+2 and t = h1 ,wehave (D ) >(D ) . From the deﬁnition of f ,for all n, s 1,d t 1,d T T f (8n + 1) = e D e = (D ) >(D ) = e D e = f (9n + 2), s d s 1,d t 1,d t d 1 1 butwealreadyarguedinCorollary 3.6 that no N-rational sequence can satisfy this inequality for all n, contradiction. Natural matrix interpretations fail to be useful for the unary rewriting systems even when used in conjunction with dependency pairs. For the reader familiar with dependency pairs, we show how to adapt the above proof to go through in the setting where the dependency pair transformation is applied before searching for natural matrix interpretations. Recall that, for an SRS R over , letting DP(R) denote the SRS consisting of all dependency pairs of R as deﬁned by Arts and Giesl [14, Deﬁnition 3], we have SN(R) if and only if SN(DP(R) / R) [14, Theorem 6]. For a deﬁned symbol s ∈ ,wewrite s to denote the top # corresponding tuple symbol. Let I ={ s → h, t → h}, and note that I ⊆ DP(Z). With an automated # # # # termination prover, the following is straightforward to establish for Zantema’s system Z after applying the dependency pair transformation and performing several steps of rule removal (e.g., using natural matrix interpretations). Lemma 3.9 SN(DP(Z) / Z) if and only if SN(I / Z). top top We prove below that neither rule in I can be removed using natural matrix interpretations. The proof is similar to that of Theorem 3.8, so we keep it relatively brief. Theorem 3.10 Let ={1, , , h, s, t}. There exists no collection [·] of natural matrix interpretations of any dimension d satisfying the requirements for a weakly monotone - algebra such that 123 Automated Approach to Collatz Conjecture Page 15 of 44 15 • for at least one rule → r ∈ I we have [](x)> [r ](x) for all x ∈ N , and • for every rule → r ∈ Z we have [ ](x) [r ](x) for all x ∈ N . Proof Assume for a contradiction that such a collection of natural matrix interpretations exists for some dimension d − 1, with each symbol σ ∈ interpreted as [σ ](x) = M x + v and σ σ each matrix D deﬁned as in Theorem 3.7.Let → r ∈ I bearulefor which [](x)> [r ](x) d−1 for all x ∈ N , and denote ρ ={ → r }. As the interpretations satisfy the requirements for ∗ d−1 only weak monotonicity, for all s, t ∈ ,if s → t,then [s](x)> [t ](x) for all x ∈ N . top Thus, for all s, t ∈ , s → t ⇒ D D and (D ) >(D ) . (5) ρ s t s 1,d t 1,d top We represent an arbitrary integer k by the string h1 , interpreted as k k h1 (x) = D D D x. # h # 1 Similar to (4), we let e ∈ N denote the ith standard basis vector and deﬁne g(k) := T k T u D w,where u = D e and w = D e are ﬁxed, so g(1), g(2), ... is an N-rational 1 d 1 h sequence. For all n,wehave 8n+1 ∗ 9n+2 h1 → h1 , # # I∪Z which crucially requires the use of both rules in I, and, moreover, these rules are applied only at the leftmost end of a string. In particular, the rule → r is used in the above derivation to perform a top rewrite. Thus, by (5), for all n,wehave g(8n + 1)> g(9n + 2),which contradicts Corollary 3.6. rev 8 Analogues of Theorems 3.8 and 3.10 also hold for the system Z , with its rules reversed. Moreover, by arguments similar to above, we can show that natural matrix interpretations fail to prove the termination of W. It is natural to expect that if a proof of the Collatz conjecture is to be produced by some automated method that relies on rewriting, then that method better be able to prove a statement as simple as the convergence of W . With this in mind, we describe an alternative rewriting system that simulates the Collatz function and terminates upon reaching 1. We then provide examples where the alternative system is more suitable for use with termination tools (for instance allowing a matrix interpretations proof of the convergence of W ). The arguments in this section that prove Theorems 3.8 and 3.10 also appear not to apply to the alternative system, because the connection between rewrite sequences and N-rational sequences gets lost when not using unary representations. More speciﬁcally, the proofs crucially use the fact that, since the system Z represents numbers in unary, it is possible to form a sequence such that the nth element is represented by some T n product v M w,where v and w are vectors and M is a matrix. There is no single such matrix that one can extract when using mixed binary–ternary, or even just binary, representations. Thus, the same kind of analysis, which uses the results known about N-rational sequences, does not go through for the alternative system. 3.2 Rewriting in Mixed Base In the mixed-base scheme, the overall idea is as follows. Given a number n ∈ N ,wewrite a mixed binary–ternary representation for it (noting that this representation is not unique). With 8 rev Speciﬁcally, Theorem 3.10 holds for Z with J ={ h11 → s11, 1h → 11t} in place of I. # # # # The corresponding version of Lemma 3.9 is again straightforward to establish using an automated termination prover. 123 15 Page 16 of 44 E. Yolcu et al. this representation, as long as the least signiﬁcant digit is binary, the parity of the number can be recognized by checking only this digit, as opposed to scanning the entire string when working in unary. This allows us to easily determine the correct case when applying the Collatz function. If the least signiﬁcant digit is ternary, then the representation is rewritten (while preserving its value) to make this digit binary. Afterwards, since computing n/2 corresponds to erasing a trailing binary 0 and computing 3n + 1 corresponds to inserting a trailing ternary 1, applying the Collatz function takes a single rewrite step. Intuitively, the rewriting system we present can be seen as applying the Collatz map to natural numbers written in binary, with some secondary computation performed using auxiliary symbols to facilitate the application of the map n → 3n + 1. However, since termination of rewriting is concerned with sequences that arise from any initial string and any possible application of the rules, we need to consider the behavior of the system over any string that may be encountered, which includes even the strings that could not result from computing in binary with a prescribed strategy for rule application. The mixed-base scheme is simply a way to give an arithmetical meaning to all strings and all possible rewrite steps. More formally, a mixed-base numeral system [34] is a numeral system where the base changes across positions, which we deﬁne as follows. Deﬁnition 3.11 (Mixed-base representation) Fix B ⊆ N to be a set of bases. Let n ,..., n ∈ 1 k N and let b ,..., b ∈ B. If we have for each 2 ≤ i ≤ k that n < b , then the matrix 1 k i i n n ... n 1 2 k N = b b ... b 1 2 k is called a mixed B-ary representation. To reduce clutter, we identify the matrix N with a string (n ) (n ) ...(n ) , where each (n ) is viewed as a single symbol denoting 1 (b ) 2 (b ) k (b ) i (b ) 1 2 k i the b -ary digit n . i i The string N in the above deﬁnition represents the number k k Val(N ) := n b . (6) i j i =1 j =i +1 Observing that the addition of leading zeros (symbols 0 for any b) to a string does not change its value, we may assume without loss of generality that n > 0. Furthermore, b does not 1 1 affect the value of the string, so we replace it by zero (noting that by Deﬁnition 3.11 no other base is zero). Example 3.12 1. With B ={2}, we have the binary numeral system. In the notation of Deﬁnition 3.11 we write 1 0 1 1 to represent the number 11. 2 2 2 2 2. With B ={2, 3}, we obtain the mixed binary–ternary system that we will use in the rest of this paper. In this system we may write, for instance, 1 2 1 or 2 1 1 or 1 1 2 to 0 3 2 0 2 2 0 2 3 represent the number 11. Now, deﬁne β (x ) := bx + n. After rearranging (6), we see that for a mixed B-ary string N = (n ) (n ) ...(n ) , its value Val(N ) is also given by evaluating the composite 1 (b ) 2 (b ) k (b ) 1 2 k function n n n k k−1 (x ) := (β ◦ β ◦ ··· ◦ β )(x ) (7) b b b k k−1 1 at any value (because b = 0 implies that the innermost function β (x ) = n is constant). 1 1 This gives us a string and a function view of the same representation, and we will switch 123 Automated Approach to Collatz Conjecture Page 17 of 44 15 between them as appropriate. In doing so, we also conﬂate the symbols and the corresponding functions, referring to β as n . As the last ingredient before describing the rewriting system, we observe that we can n n m m write (β ◦ β )(x ) = bcx + bm + n equivalently as another composition (β ◦ β )(x ) = b c c b cbx + cn + m for some suitable 0 ≤ n < b and 0 ≤ m < c. This allows us to swap the bases of adjacent positions while preserving the value of the string. From this point on, we constrain ourselves to the mixed {2, 3}-ary (binary–ternary) repre- sentations as we shift our focus to simulating the Collatz function (noting that it is possible to adapt the resulting rewriting system for other instances of the general case). More pre- cisely, we simulate the following redeﬁnition of the Collatz function, where the odd case incorporates an additional division by 2. if n ≡ 0 (mod 2) T (n) = 3n+1 if n ≡ 1 (mod 2) We will describe an SRS T over the symbols {f, t, 0, 1, 2, , } that simulates the iterated application of the Collatz function and terminates upon reaching 1. The symbols f, t cor- respond to binary digits 0 , 1 ;and 0, 1, 2 to ternary digits 0 , 1 , 2 . The symbol marks 2 2 3 3 3 the beginning of a string while also standing for the most signiﬁcant digit (without loss of generality assumed to be 1 )and marks the end of a string while also standing for the redundant trailing digit 0 . Consider the functional view of these symbols: 0(x ) = 3x f(x ) = 2x (x ) = 1 1(x ) = 3x + 1 (8) t(x ) = 2x + 1 (x ) = x 2(x ) = 3x + 2 Each positive integer can be expressed as some composition of these functions, which cor- responds to a string as per our previous discussion. Example 3.13 Viewing the expression (x ) as the constant 1, we can write 19 = Val(0f1) = (1(f(0((x ))))). The string representation ends with a ternary symbol, so we will rewrite it. With the function view, we have 1(f(x )) = 3(2x ) + 1 = 6x + 1 = 2(3x ) + 1 = t(0(x )). This shows that we could also write 19 = Val(00t), which now ends with the binary digit 1 . This gives us the rewrite rule f1 → 0t. We can now apply the Collatz function to this representation by rewriting only the rightmost two symbols of the string since 3(2x + 1) + 1 6x + 4 T ((t(x ))) = = = 3x + 2 = ((2(x ))). 2 2 This gives us the rewrite rule t → 2. After applying this rule to the string 00t,we indeed obtain T (19) = 29 = Val(002). In the manner of the above example, we compute all the necessary transformations and obtain the following 11-rule SRS T . ⎧ ⎫ ⎧ ⎫ f0 → 0f t0 → 1t 0 → t ⎨ ⎬ ⎨ ⎬ f → D = A = f1 → 0t t1 → 2f B = 1 → ff t → 2 ⎩ ⎭ ⎩ ⎭ f2 → 1f t2 → 2t 2 → ft 123 15 Page 18 of 44 E. Yolcu et al. This SRS is split into subsystems D (dynamic rules for T)and X = A ∪ B (auxiliary rules). The two rules in D encode the application of the Collatz function T , while the rules in X serve to push binary symbols towards the rightmost end of the string by swapping the bases of adjacent positions without changing the represented value. Example 3.14 (Rewrite sequence of T ) Consider the string s = ff0, which represents the number 12. Below is a possible rewrite sequence of T that starts from s, with the corre- sponding values (under the interpretations from (8)) displayed above the strings. Underlines indicate the parts of the strings where the rules are applied. 12 12 6 6 3 3 5 5 ff0 → f0f → f0 → 0f → 0 → t → 2 → ft A D A D B D B T T T 88 8 4 2 1 → f2 → 1f → fff → ff → f → D A B D D D T T T T The trajectory of T would continue upon reaching 1; however, in order to be able to formulate the Collatz conjecture as a termination problem, T is made in such a way that its rewrite sequences stop upon reaching the string representation of 1 since no rule is applicable. Termination of the subsystems of T with B or D removed is easily seen. However, since we have matrix interpretations at our disposal, let us give a compact and formal proof. Lemma 3.15 SN(T \ B) and SN(T \ D ). rev Proof It is easily checked that the interpretations below show SN((T \ B) ), which implies SN(T \ B) by Lemma 2.8. [f](x ) =[t](x ) = 2x + 1 []= x [0](x ) =[1](x ) =[2](x ) = 2x rev Similarly, the below interpretations show SN((T \ D ) ), which implies SN(T \ D ) T T by Lemma 2.8. [f](x ) =[t](x ) =[](x ) = x + 1 [0](x ) =[1](x ) =[2](x ) = 4x When considering the termination of T (on all initial strings), it sufﬁces to limit the discussion to initial strings of a speciﬁc form that we have been working with so far, e.g., in Examples 3.13 and 3.14. Lemma 3.16 If T is terminating on all initial strings of the canonical form (f|t|0|1|2) , then T is terminating (on all initial strings). For the proof of Lemma 3.16, we will use type introduction, which is a technique for proving termination by switching to typed rewriting. We refer the reader to Sabel and Zan- tema [35, Section 3.1] for background. We also offer a more elementary proof in Appendix A. Proof of Lemma 3.16 Let T ={ρ, σ, τ } be a set of types. It is straightforward to see that, with respect to the typing : σ → τ, f, t, 0, 1, 2 : σ → σ, : ρ → σ, 123 Automated Approach to Collatz Conjecture Page 19 of 44 15 the SRS T is well-typed, so it is terminating (in the untyped setting) if and only if it is terminating in the typed setting [35, Corollary 3.4]. Due to Lemma 3.15, a well-typed string with σ as its source or target type cannot admit an inﬁnite rewrite sequence for T . Thus, a well-typed string admits an inﬁnite rewrite sequence only if it is of type ρ → τ,which implies that it is of the canonical form. Note that the converse of the above lemma is obvious, since if T is terminating then it is terminating on all initial strings of any form, in particular (f|t|0|1|2) . As a whole, the rewriting system T simulates the iterated application of T (except at 1). Theorem 3.17 T is terminating if and only if T is convergent (i.e., the Collatz conjecture holds). Proof Without loss of generality (due to Lemma 3.16), consider only the strings of the canonical form (f|t|0|1|2) throughout this proof. We will show that, given such a string N, all rewrite sequences for T that start from N simulate the T -trajectory of Val(N ), except when Val(N ) = 1. More speciﬁcally, we prove the following and use them to deduce the theorem statement. Claim 1 For any pair N , N of strings, if N → N then Val(N ) = Val(N ), and if N → X D N then Val(N ) = T (Val(N )). Claim 2 For any string N with Val(N ) = 1, there exists no string N satisfying N → N . Claim 3 For any integer ν> 1 and any string N with Val(N ) = ν, there exists a string N such that N → N and Val(N ) = T (ν). Proof of Claim 1 Assume N → N . Then there exist strings X , Y and some rule → r ∈ X such that N = X Y and N = XrY . Recalling the deﬁnition of from (7), we have Val(N ) = Val(N ) if and only if ◦ ◦ = ◦ ◦ for all → r ∈ X.This Y r X Y X holds if and only if = for all → r ∈ X . With the functional views of the symbols as in (8), we indeed have: (x ) = f(0(x )) = 6x = 0(f(x )) = (x ) 0f f0 (x ) = t(0(x )) = 6x + 1 = 1(f(x )) = (x ) 0t f1 (x ) = f(1(x )) = 6x + 2 = 2(f(x )) = (x ) 1f f2 (x ) = t(1(x )) = 6x + 3 = 0(t(x )) = (x ) 1t t0 (x ) = f(2(x )) = 6x + 4 = 1(t(x )) = (x ) 2f t1 (x ) = t(2(x )) = 6x + 5 = 2(t(x )) = (x ) 2t t2 (x ) = t((x )) = 3 = 0((x )) = (x ) t 0 (x ) = f(f((x ))) = 4 = 1((x )) = (x ) ff 1 (x ) = t(f((x ))) = 5 = 2((x )) = (x ) ft 2 This proves the ﬁrst part of the claim. Now assume N → N . Again, there exist a string X and some rule → r ∈ D such D T that N = X and N = Xr (since the rules in D can be applied only at the rightmost end of thestring).WehaveVal(N ) = T (Val(N )) if and only if ◦ = T ◦ ◦ for all r X X → r ∈ D . This holds if and only if = T ◦ for all → r ∈ D . There are only two T r T rules to check, and indeed we have: (x ) = (x ) = x = T (2x ) = T ((f(x ))) = T ( (x )) (x ) = (2(x )) = 3x + 2 = T (2x + 1) = T ((t(x ))) = T ( (x )) 2 t This proves the second part of the claim. 123 15 Page 20 of 44 E. Yolcu et al. Proof of Claim 2 The string has Val() = 1, and inserting any symbol from {f, t, 0, 1, 2} in between the delimiters increases the value of the string, so is the unique string repre- senting 1. None of the rules in T apply to , which proves the claim. Proof of Claim 3 Let ν> 1beaninteger,and let N be a string with Val(N ) = ν.We will describe a rewrite sequence N → N → N , which implies by Claim 1 that X T Val(N ) = T (ν). For the rest of the proof let b and t stand for binary and ternary symbols, i i respectively. Assume that N contains some binary symbol (f or t), since otherwise it is of the form (0|1|2) and we can apply some rule from B to produce a binary symbol. Then the string contains some substring b t t ... t . We rewrite this substring into t b t ... t by 1 2 3 k 2 3 k applying some rule from X . For each 1 < i < k, assuming the current string contains some substring b t ... t , we rewrite it into t b t ... t . In the end we obtain a string N i i +1 k i +1 i +2 k with Val(N ) = ν that contains some b , so we apply some rule from D to obtain N such k T that Val(N ) = T (ν). Assume that the SRS T is not terminating. Let (N ) be an inﬁnite rewrite sequence i =0 for T , and consider the sequence (ν ) ,where ν = Val(N ). By Claim 1,for all i ∈ N, i i i i =0 we have either ν = ν or ν = T (ν ) depending on the rewrite rule used. Let I ={i ∈ i +1 i i +1 i N | ν = T (ν )}, which is the same as the set of indices at which some rule from D is i +1 i T applied in the rewrite sequence. By Lemma 3.15, the subsystem X = T \ D is terminating, so the rewrite → is performed inﬁnitely many times in the sequence. This implies that I is inﬁnite, proving that the sequence (ν ) is a Collatz trajectory. Moreover, this trajectory is i i ∈I nonconvergent, i.e., it does not contain 1, since otherwise the rewrite sequence could not be inﬁnite (because of Claim 2). This proves the backward implication in the theorem statement. Assume that the function T is not convergent. Let (ν ) be a nonconvergent trajectory, i =0 and note that ν > 1for all i ∈ N. We will inductively deﬁne a sequence (N ) such that i i i =0 Val(N ) = ν for all i ∈ N.Let N be any string with Val(N ) = ν . For each i ∈ N , i i 0 0 0 assuming Val(N ) = ν ,let N be a string such that N → N and Val(N ) = i −1 i −1 i i −1 i i T (ν ) = ν , which exists by Claim 3. Deﬁned in this manner, the sequence (N ) i −1 i i i =0 satisﬁes N → N for all i ∈ N,meaningthat T is not terminating. This proves the i i +1 forward implication in the theorem statement, which concludes the proof. When trying to remove a rule in D or B it sufﬁces to show relative top termination, allow- ing us to use weakly (instead of extended) monotone algebras when applying Theorem 2.15 and take advantage of the more relaxed constraints when searching for matrix interpretations. As we mentioned back in Section 2.1, the lemma below encapsulates dependency pairs, and it can in fact be automatically proved by the existing termination tools via the dependency pair transformation followed by an application of the dependency pair framework [36]. Lemma 3.18 1. For each subset R ⊆ B,if SN(R / T ) then SN(R / T ). top rev rev rev rev 2. For each subset Q ⊆ D ,if SN(Q / T ) then SN(Q / T ). top Proof Without loss of generality (due to Lemma 3.16), consider only the rewrite sequences that start with some string of the canonical form (f|t|0|1|2) (resp. its reversal). rev Let R ⊆ B (resp. Q ⊆ D ). The rules in R (resp. Q ) can be applied only at the leftmost end as they are all of the form s → t for some s, t not containing (resp. s → t for some s , t not containing ). rev rev Assume ¬ SN(R / T ) (resp. ¬ SN(Q / T )). Then there exists an inﬁnite rewrite rev rev sequence for T (resp. T ) where the rules from R (resp. Q ) are applied inﬁnitely many We thank an anonymous reviewer of CADE for pointing out this fact. 123 Automated Approach to Collatz Conjecture Page 21 of 44 15 times. As these rules can be applied only at the leftmost end, this implies relative top non- rev rev termination, i.e., ¬ SN(R / T ) (resp. ¬ SN(Q / T )). top top 3.3 Rewriting with a Hybrid System As another alternative to the rewriting system Z, instead of fully discarding unary in favor of a positional numeral system we may adopt a hybrid between the two approaches and design a system to increment/decrement by 1 or multiply/divide by 2 or 3 in a single rewrite. We will describe an SRS over the symbols {i, f, 0, , } viewed as follows. i(x ) = x + 1 f(x ) = 2x 0(x ) = 3x (x ) = 1 (x ) = x In essentially the same manner as we did for the system T , we have a set of dynamic rules that simulate the application of the Collatz function and a set of auxiliary rules that update the string representation so that the parity of the corresponding number can be recognized in a single step. We have the following 7-rule SRS L (designed by Luke Schaeffer). ⎧ ⎫ fii → if ⎨ ⎬ f → i → f i0 → 0iii D = A = B = fi → 0ii 0 → fi ⎩ ⎭ f0 → 0f As long as the string ends with f or fi, the parity of the represented number is apparent without needing to scan the whole string, which allows the Collatz function to be applied in a single rewrite. After the application of a dynamic rule, the string may no longer end with f or fi, so the auxiliary rules in X = A ∪ B push the symbol f towards the rightmost end of the string while preserving its value. Thus, L is yet another rewriting system that simulates the iterated application of the Collatz function. Theorem 3.19 L is terminating if and only if T is convergent. The proof of the above theorem is essentially the same as that of Theorem 3.17 once it is checked that the dynamic rules do indeed apply T and that the auxiliary rules do indeed preserve the value of a string under the functional view of the symbols. 4 Automated Proofs We adapt the rewriting system T for different generalized Collatz functions to explore the effectiveness of the mixed-base scheme on weakened variants of the Collatz conjecture. All of the rewriting systems, scripts to reproduce the proofs, and our minimal implementa- tion of a termination prover are available at https://github.com/emreyolcu/rewriting-collatz. In particular, any omitted relative termination proof that we refer to in this section is available at https://github.com/emreyolcu/rewriting-collatz/tree/main/proofs. 123 15 Page 22 of 44 E. Yolcu et al. 4.1 A Simple Example Earlier we mentioned a generalized Collatz function W as a simple example that could serve as a sanity check for an automated method aiming to solve Collatz-like problems. With the mixed binary–ternary scheme, this function can be seen to be simulated by the system W ={f → 0}∪ X . A small matrix interpretations proof is found for this system in less than a second, in contrast to its variant W that uses unary representations for which no automated proof is known. Additionally, the function W can be simulated by the rewriting system W ={f → 0}∪ X adapted from the hybrid system L, although we were unable to ﬁnd an automated proof of termination for W . Theorem 4.1 SN(W ). rev Proof The interpretations below prove SN({f → 0} / X ): 10 1 10 1 [f](x) = x + [t](x) = x + 01 1 00 0 10 12 [](x) = x [](x) = x 00 00 10 2 10 2 10 2 [0](x) = x + [1](x) = x + [2](x) = x + 01 0 10 2 10 2 rev With the above interpretations of the symbols, the rules of W satisfy the following rev relations, which, by Theorem 2.15, proves that {f → 0} is terminating relative to X . 12 3 12 2 [f](x) = x + > x + =[0](x) 00 0 00 0 10 3 10 3 [0f](x) = x + x + =[f0](x) 01 1 01 1 10 3 10 3 [1f](x) = x + x + =[t0](x) 10 3 00 0 10 3 10 3 [2f](x) = x + x + =[f1](x) 10 3 10 3 10 3 10 3 [0t](x) = x + x + =[t1](x) 00 0 00 0 10 3 10 3 [1t](x) = x + x + =[f2](x) 10 3 10 3 10 3 10 3 [2t](x) = x + x + =[t2](x) 10 3 00 0 10 2 10 1 [0](x) = x + > x + =[t](x) 00 0 00 0 10 2 10 2 [1](x) = x + x + =[ff](x) 10 2 00 2 123 Automated Approach to Collatz Conjecture Page 23 of 44 15 10 2 10 2 [2](x) = x + x + =[tf](x) 10 2 00 0 rev rev By Lemmas 2.8 and 3.15, X is terminating. As a result, W is terminating, which by Lemma 2.8 implies that W is terminating. 4.2 Farkas’Variant Let 2N + 1 ={1, 3, 5,... } denote the odd natural numbers. Farkas [37] studied a slight modiﬁcation F : 2N + 1 → 2N + 1 of the Collatz function for which it becomes possible to prove convergence via induction. We consider automatically proving the convergence of this function as another test case for the mixed-base scheme that is easier than the Collatz conjecture without being entirely trivial. Farkas deﬁned this function as ⎪ if n ≡ 0 (mod 3) n+1 F (n) = if n ≡ 0 (mod 3) and n ≡ 1 (mod 4) 3n+1 if n ≡ 0 (mod 3) and n ≡ 3 (mod 4). In this paper, we deﬁne another function F : N → N that resembles the Collatz function more closely than Farkas’ F (with respect to the deﬁnitions of the cases) while being equiv- alent to F in terms of convergence. It is obtained by introducing an additional case in the Collatz function for n ≡ 1 (mod 3) and applying T otherwise: n−1 ⎪ if n ≡ 1 (mod 3) F (n) = if n ≡ 0or n ≡ 2 (mod 6) 3n+1 if n ≡ 3or n ≡ 5 (mod 6) Given an F -trajectory, the bijection n → (n − 1)/2 applied to each of its iterates maps the trajectory to the corresponding F-trajectory. Thus, an F -trajectory reaches 1 if and only if the corresponding F-trajectory reaches 0. Furthermore, an F-trajectory reaches 0 if and only if it reaches 1, which is a convenient fact since in our string representations we do not represent 0, so in order to prove that F is convergent it sufﬁces to show that for all n ∈ N the trajectory F (n) contains 1. Note that F can also be viewed as a generalized Collatz function with 5 cases, which makes it straightforward to translate the cases of F into a set D of dynamic rules (shown below) to obtain a rewriting system that simulates the iterated application of F on positive integers. 1 → 0f → 0 1f → 1 1t → 12 2t → 22 Termination of the rewriting system F = D ∪ X is equivalent to the convergence of F. The proof of the equivalence is essentially the same as that of Theorem 3.17 except for the step where we construct a nonterminating rewrite sequence from a nonconvergent trajectory. To construct such a rewrite sequence for F, we take any nonconvergent F-trajectory and write the ﬁrst number in the trajectory in ternary (instead of binary). If the leading digit turns out to be 2 we replace it by 1 0 since the leading digit is always assumed to be 1 in 3 0 2 0 123 15 Page 24 of 44 E. Yolcu et al. our mixed-base representations. Then repeatedly performing the rightmost possible rewrite results in a rewrite sequence that simulates the F-trajectory. Farkas gave an inductive proof of convergence for F via case analysis. We found an auto- mated proof that F is terminating via arctic matrix interpretations. Below, we present both a manual proof of convergence for F and the automated proof of SN(F ). It is worth mention- ing that the default conﬁgurations of the existing termination tools (e.g., AProVE, Matchbox) are too conservative to prove the termination of this system, but after their authors tweaked the strategies they were also able to ﬁnd automated proofs via arctic matrix interpretations. It also remains an interesting question whether the automated proof somehow captures the argument in the inductive proof. + N Theorem 4.2 For all n ∈ N , the trajectory F (n) contains 1. Proof (in the manner of Farkas [37, Theorem 1]) We proceed by induction. For n = 1the result holds since F (1) = (1, 0, 0,...). Assuming it holds for all positive integers less than n, we will show that it holds for n. In particular, we will show that the trajectory of n reaches a number strictly smaller than n, which implies by the induction hypothesis that the trajectory contains 1. We split into three cases. (i) Assume n ≡ 1 (mod 3).Then F (n) = (n − 1)/3 is smaller than n. (ii) Assume n ≡ 0or n ≡ 2 (mod 6).Then F (n) = n/2 is smaller than n. (iii) Assume n ≡ 3or n ≡ 5 (mod 6). Denote n by N , and consider the trajectory F (N ) = (N , N , N ,...).Let 1 1 2 3 3N + 1 j −1 k = sup i ∈ N N = for all 1 < j ≤ i . We cannot have k =∞, i.e., F cannot apply N → (3N + 1)/2 indeﬁnitely, since for such a sequence we have j −1 3 3 N + 1 = (N + 1) = (N + 1). j j −1 1 2 2 As all the elements in the trajectory have to be integers, k −1 cannot exceed the number of times that N + 1 can be divided by 2, so k is ﬁnite. Consider N = (N + 1) − 1. k+1 1 It is of the form 3 · L − 1 for some positive integer L, so we know that either N ≡ 2 k+1 (mod 6) or N ≡ 5 (mod 6). Due to the way k is deﬁned, N cannot be congruent k+1 k+1 to 5 (mod 6),sowehave N ≡ 2 (mod 6). In particular, N is even, so (N + k+1 k+1 1 N +1 k 1) is odd, which in turn implies that is odd, i.e., we have N = 2 · (2M + 1) − 1 for some natural number M. Then, N satisﬁes k+1 k k k N = 3 · (2M + 1) − 1 = 3 · 2M + 3 − 1. k+1 Since N ≡ 2 (mod 6), we can deduce that k+1 k k N 3 · 2M + 3 − 1 k+1 F (N ) = = ≡ 1 (mod 3), k+1 2 2 and furthermore, k k 3 ·2M +3 −1 − 1 2 2 k−1 k−1 F (N ) = = 3 · 2M + 3 − 1 ≡ 2 (mod 6). k+1 123 Automated Approach to Collatz Conjecture Page 25 of 44 15 2k Repeatedly applying F in the above manner gives F (N ) = 2M.Since k ≥ 1, k+1 k N we have 2M < 2 · (2M + 1) − 1 = N = n,and so thetrajectory F (n) reaches a number strictly smaller than n. Proof (via arctic matrix interpretations) We will show SN(F ). By Lemmas 2.8 and 3.15, rev we have SN(X ). Consider the arctic matrix interpretations below. Recall that − indicates −∞ in the matrices. Also recall that arctic addition is max and arctic multiplication is +. ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−− 2 − 0 −−−− 2 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 20 −− − 020 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [f](x) = 2 −−−− x ⊕ − [t](x) = 2 − 2 −− x ⊕ − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ 0 0 −−−− ⎢ ⎥ ⎢ ⎥ 2 −−−−− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [](x) = − [](x) = −−−−− x ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ − −−−−− 4 −−−−− ⎡ ⎤ ⎡ ⎤ ⎡ 040 −− 1 −−−− 0 − 0 −− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 4 −−− − 40 −− − 4 −−− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0](x) = − 40 −− x [1](x) = − 40 −− x [2](x) = 0 − 1 − 0 x ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ 03 0 −− 0 −−−− −−−−− −−−−− 03 0 −− 0 − 0 − 0 (9) rev rev Above interpretations prove SN(D / X ) by Theorem 2.15. (See Appendix B for the top rev rev rev corresponding interpretations of the rules of F .) We then get SN(D / X ) by Lemma rev rev rev 3.18. As we know that X is terminating, by Theorem 2.6 we can conclude SN(D ∪X ), which implies SN(F ) via Lemma 2.8. 4.3 Subsets of the Collatz System It is also interesting to consider whether we can automatically prove termination of proper subsets of T . Speciﬁcally, we considered the 11 subsystems obtained by leaving out a single rewriting rule from T , and we found termination proofs via matrix interpretations for all of the 11 subproblems. The reason for our interest in these problems is threefold: 1. Termination of T implies termination of all of its subsystems, so proving its termination is at least as difﬁcult a task as proving termination of the 11 subsystems. Therefore, the subproblems serve as additional sanity checks that an automated approach aspiring to succeed for the Collatz conjecture ought to be able to pass. Furthermore, they form an additional source of weakened variants that give us a heuristic idea of the suitable choice of parameters to use when searching for interpretations for the full problem. 2. When proving termination in a stepwise manner, we solve a sequence of relative termina- tion problems. Having proved termination of all 11 subsystems is a partial solution to the full problem, since it implies that for any single rule → r ∈ T , proving SN({ → r }/T ) settles the Collatz conjecture. 123 15 Page 26 of 44 E. Yolcu et al. 3. After the removal of a rule, the termination of the remaining system still encodes a valid mathematical question about the Collatz trajectories. The question of the termination of a proper subset is equivalent to asking if every corresponding Collatz trajectory that does not require the use of the left-out rule is convergent. For instance, removing {t → 2} deletes the odd case of the Collatz function, which gives a clearly convergent function. Removing the auxiliary rules in X lead to potentially more interesting questions: For instance, the termination of T \{t1 → 2f} implies that the trajectories where the pattern t1 is never encountered during the simulation are all convergent. Note that this type of inquiry is less meaningful for the unary system Z as its simulation of the Collatz function depends crucially on each rule being present. Leaving out some subset of the rules from Z causes the system to become terminating for a trivial reason, i.e., the computation it expresses no longer corresponds to the iterated application of some function. Example 4.3 As an instance of leaving out a rule, consider the subsystem T \{f1 → 0t}. There is a single-step natural matrix interpretations proof that this system is terminating: 11 13 1 [f](x) = x [t](x) = x + 10 34 1 15 10 1 [](x) = x [](x) = x + 00 10 1 72 2 21 1 22 0 [0](x) = x + [1](x) = x + [2](x) = x + 25 1 11 0 24 2 It can be checked that under these interpretations the rules of T \{f1 → 0t} satisfy the following relations: 20 2 10 1 [f](x) = x + > x + =[](x) 10 1 10 1 40 5 40 4 [t](x) = x + > x + =[2](x) 70 8 60 8 97 3 97 2 [f0](x) = x + > x + =[0f](x) 72 2 72 1 46 2 32 1 [f2](x) = x + > x + =[1f](x) 22 0 21 0 13 17 6 510 4 [t0](x) = x + > x + =[1t](x) 29 26 11 47 2 54 2 42 0 [t1](x) = x + > x + =[2f](x) 10 7 4 62 2 814 7 814 4 [t2](x) = x + > x + =[2t](x) 14 22 9 14 22 8 17 27 7 16 23 6 [0](x) = x + > x + =[t](x) 00 0 00 0 123 Automated Approach to Collatz Conjecture Page 27 of 44 15 76 1 76 0 [1](x) = x + > x + =[ff](x) 00 0 00 0 12 22 10 922 7 [2](x) = x + > x + =[ft](x) 00 0 00 0 Note that the left-out rule f1 → 0t ends up receiving a nondecreasing interpretation as there is no constraint to enforce otherwise: 32 1 13 29 11 [f1](x) = x + > x + =[0t](x) 21 1 17 26 8 The above interpretations witness for instance that the Collatz trajectory starting at 3 (represented as t) is convergent, because the missing rule is not used in any derivation of 1() from 3. Below is an example derivation along with the values each string represents and a vector value of each string under the interpretations above (setting x = (0, 0) for the purpose of demonstration). We omit the subscripts from the rewrite relations and simply write →. 3 5 5 8 884 2 1 t → 2 → ft → f2 → 1f → fff → ff → f → 79 78 68 62 41 40 26 14 12 > > > > > > > > 0 0 0 0 0 0 0 0 0 Table 1 shows the parameters of the matrix interpretations proofs that we found for the termination of each subsystem. For each rule → r that is left out, we searched for a stepwise proof to show that B \{ → r } is terminating relative to T \{ → r } (freely utilizing weakly monotone algebras due to Lemma 3.18). Such a proof requires at most three steps since there areatmostthree rulesin B \{ → r }. In the table, we report the smallest parameters (in terms of matrix dimension) that work for all of these steps. As we already know that SN(T \ B) holds (by Lemma 3.15), the interpretations found allow us to conclude the termination of each subsystem. This is not the only way to prove termination of the subsystems; however, we chose this uniform strategy for the sake of comparison. In the experiments we searched for matrices of up to 7 dimensions, with the coefﬁcients taking at most 8 different values. 4.4 Odd Trajectories In the originally deﬁned Collatz function C, applying 2n + 1 → 6n + 4 produces an even number, so we incorporate a single division by 2 into the deﬁnition of the odd case and obtain the function T with the same overall dynamics as C. Taking this idea further by performing as many divisions by 2 as possible leads to the so-called Syracuse function Syr : 2N + 1 → 2N + 1, deﬁned as 3n + 1 + k Syr(n) = ,where k = max{k ∈ N | 2 divides 3n + 1}. The Syracuse function maps each odd number to the next odd number in its Collatz trajec- tory. In this sense, it has the same overall dynamics as the Collatz functions C or T we have previously deﬁned, i.e., Syr is convergent if and only if C or T is convergent. The function T takes fewer steps than C to reach 1 and can be thought of as an accelerated Collatz function, 123 15 Page 28 of 44 E. Yolcu et al. Table 1 Smallest proofs found for termination of subsystems of T in under 30 seconds. The columns show the matrix dimension D and the maximum number V of distinct coefﬁcients that appear in the matrices, along with the median time to ﬁnd an entire termination proof across 25 repetitions for the ﬁxed D and V . Natural Arctic Rule removed DV Time DV Time 1.42s 15.95s f → 34 35 t → 2 12 0.27s 13 0.28s f0 → 0f 42 0.92s 34 2.46s 0.50s 0.51s f1 → 0t 13 14 f2 → 1f 12 0.38s 13 0.39s t0 → 1t 43 1.20s 34 0.87s t1 → 2f 52 0.89s 43 0.84s t2 → 2t 44 10.00s 25 0.62s 0 → t 22 0.40s 23 0.42s 1 → ff 33 0.53s 34 0.57s 2 → ft 44 7.51s 43 4.04s making the Syracuse function a further accelerated version. Reducing the number of steps towards convergence is of interest mainly because the existence of various kinds of termi- nation proofs is dependent on the derivational complexity of the rewriting system staying below certain thresholds [38]. For instance, given a rewriting system, if its termination can be proved in a single-step via natural matrix interpretations then its derivational complexity is at most exponential [10]. Similarly, a single-step termination proof via arctic matrix inter- pretations implies a linear derivational complexity [11]. Thus, it can be preferable to work with an alternative rewriting system with smaller derivational complexity that still simulates the dynamics of the Collatz function. Expressing the Syracuse function as a generalized Collatz function would require inﬁnitely many cases to account for all of the possible appearances of 2 as the denominator with different values of k. As a result, we are unable to simulate it with a ﬁnite rewriting system. Nevertheless, we may compromise and accelerate the Collatz function by a smaller amount. 3n+1 We ﬁrst observe that if n ≡ 1 (mod 8) then Syr(n) = and if n ≡ 3 (mod 4) then 3n+1 Syr(n) = . Furthermore, for any n ∈ N we have Syr(8n + 5) = Syr(2n + 1) since 3(8n + 5) + 1 = 24n + 16 = 4(6n + 4) = 4(3(2n + 1) + 1). Putting these observations together, we can deﬁne a generalized Collatz function S : 2N + 1 → 2N + 1 as follows. 3n+1 if n ≡ 1 (mod 8) n−1 S(n) = if n ≡ 5 (mod 8) 3n+1 if n ≡ 3 (mod 4) Example 4.4 The three trajectories below illustrate how the dynamics of C, Syr, and S com- pare to one another. • C (19) = (19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1, 4, 2, 1,...) Derivational complexity is deﬁned as the maximal length of rewrite sequences in the system as a function of the length of the initial string in the sequence. 123 Automated Approach to Collatz Conjecture Page 29 of 44 15 • Syr (19) = (19, 29, 11, 17, 13, 5, 1, 1,...) • S (19) = (19, 29, 7, 11, 17, 13, 3, 5, 1, 1,...) Note that a Syr-trajectory simply consists of the odd numbers in the corresponding C- trajectory; however, an S-trajectory is not necessarily contained in the corresponding C-trajectory. This is due to the n ≡ 5 (mod 8) case of S that maps n to a number not necessarily contained in the C-trajectory (marked in bold above). Once one of the other two cases is encountered, the S-trajectory arrives back at the number Syr(n). S is convergent if and only if C (or T ) is convergent, and the number of steps that S takes to converge is between that of T and Syr. In a manner similar to before, we can translate the cases of S into a set D of dynamic rules (shown below). Since we are working with odd numbers we use a new symbol • to mark the end of a string, viewed functionally as •(x ) = 2x + 1. ff•→ 0• tf•→• t•→ 2• Termination of the rewriting system S = D ∪ X is equivalent to the convergence of S. Similar to T , proving the termination of S is currently beyond our reach, although it may potentially be an easier path to the Collatz conjecture (compared to proving SN(T )). Failing to prove the termination of S itself, we considered the subsystems of S as we did for T in Section 4.3. With matrix interpretations, termination of all but two of the 11-rule subsystems of S was automatically proved. Despite devoting thousands of CPU hours, we were not able to ﬁnd interpretations to prove that S = S \{ff•→ 0•} or S = S \{tf•→•} is 1 2 terminating. By the discussion in Section 4.3, termination of subsystems of S corresponds to questions about the trajectories of S. In particular, for S and S we have the following. 1 2 Proposition 4.5 1. SN(S ) if and only if all nonconvergent S-trajectories contain some n ≡ 1 (mod 8). 2. SN(S ) if and only if all nonconvergent S-trajectories contain some n ≡ 5 (mod 8). We can prove automatically via matrix interpretations that S = S \{t•→ 2•} is terminating, which implies the following through an equivalence of the above form for S . Proposition 4.6 All nonconvergent S-trajectories contain some n ≡ 3 (mod 4). Leaving out some dynamic rules from a mixed-base rewriting system that simulates a generalized Collatz function allows us to phrase the above kinds of questions as termination problems. Recall that, although S is equivalent to C in terms of convergence, its trajectories are not necessarily contained in the Collatz trajectories, so we cannot substitute C for S in the above statements (except for the second item of Proposition 4.5, since the left-out rule is the one that maps to a number not contained in the Collatz trajectory). In the next section, we perform the same kind of inquiry into the original Collatz trajectories. 4.5 Collatz Trajectories Modulo 8 Our initial motivation for the previous section was to ﬁnd rewriting systems with reduced derivational complexity. This inquiry led us to surprisingly difﬁcult Collatz-like problems, which we believe may be on the border of the reach of automated methods. In this section we explore more problems of a similar form and present the unsolved ones as potentially reachable targets for automated termination proving. 123 15 Page 30 of 44 E. Yolcu et al. Fig. 1 Transition graphs of the iterates in the Collatz trajectories across residue classes modulo 8 for the functions C (left), T (middle), S (right). For each function f , the edge u → v is part of its transition graph if and only if there exists some n ≡ u (mod 8) such that f (n) ≡ v(mod 8). Bold edges indicate transitions where f (n)> n. Let m beapower of 2. Given k ∈{0, 1,..., m − 1}, is it the case that all nonconvergent Collatz trajectories contain some n ≡ k (mod m)? For several values of k this can be proved by inspecting the transitions of the iterates in the Collatz trajectories across residue classes modulo m (shown on Figure 1 for m = 8). As an example, consider the case k = 6. Proposition 4.7 All nonconvergent C-trajectories contain some n ≡ 6 (mod 8). Proof Let t be a C-trajectory. The path that t takes over the transition graph of C in Figure 1 is a concatenation of the simple cycles of the graph. If t does not contain any n ≡ 6 (mod 8), then the cycles containing 6 cannot occur in the path, which leaves eight cycles (listed below). By composing the functions applied at each transition in the graph, we can compute the mapping (call it c) applied to an iterate after traversing a cycle: Cycle c(n) (0, 4, 2, 5, 0)(3n + 8)/8 (0, 0) n/2 (1, 4, 2, 1)(3n + 1)/4 (2, 5, 0, 4, 2)(3n + 2)/8 (2, 1, 4, 2)(3n + 2)/4 (4, 2, 5, 0, 4)(3n + 4)/8 (4, 2, 1, 4)(3n + 4)/4 (5, 0, 4, 2, 5)(3n + 1)/8 For t to be nonconvergent, it needs to contain inﬁnitely many occurrences of cycles that increase the values of the iterates. All of the above cycles decrease the values of the iterates, so each iterate of t eventually reaches a smaller number, implying t is convergent. Propositions of the above kind can also be formulated as termination of some rewriting systems. With this approach we found automated proofs for several cases. We start by studying the smallest interesting case m = 4. Consider the following two sets of dynamic rules to simulate the Collatz function. ⎧ ⎫ ⎧ ⎫ ff → f f → ⎨ ⎬ ⎨ ⎬ Even/4 Odd/4 D = tf → t D = ft → 1f C T ⎩ ⎭ ⎩ ⎭ t → 2f tt → 2t 123 Automated Approach to Collatz Conjecture Page 31 of 44 15 Even/4 Even/4 It is straightforward to see that the SRS C = D ∪ X simulates the function C Odd/4 Even/4 Odd/4 and the SRS T = D ∪ X simulates the function T . The ﬁrst two rules of D T C express the application of C to numbers of the form 4n and 4n +2. Similarly, the last two rules Odd/4 of D express the application of T to numbers of the form 4n +1and 4n + 3. Observing that a T -trajectory contains the same odd numbers as the corresponding C-trajectory, we have the following equivalences. Proposition 4.8 Even/4 1. SN(C \{ff → f}) if and only if all nonconvergent C-trajectories contain some n ≡ 0 (mod 4). Even/4 2. SN(C \{tf → t}) if and only if all nonconvergent C-trajectories contain some n ≡ 2 (mod 4). Odd/4 3. SN(T \{ft → 1f}) if and only if all nonconvergent C-trajectories contain some n ≡ 1 (mod 4). Odd/4 4. SN(T \{tt → 2t}) if and only if all nonconvergent C-trajectories contain some n ≡ 3 (mod 4). We were able to prove termination of the above four systems via matrix interpretations, thus establishing the following. Theorem 4.9 If there exists a nonconvergent Collatz trajectory, it cannot avoid any of the residue classes modulo 4. Next, we look at the case m = 8. It can be studied via the analogously deﬁned rewriting systems: ⎧ ⎫ ⎧ ⎫ fff → ff f → ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ftf → ft fft → 0tf ⎨ ⎬ ⎨ ⎬ Even/8 Odd/8 D = tff → tf D = ftt → 1ft C T ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ttf → tt tft → 2ff ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⎭ ⎩ ⎭ t → 2f ttt → 2tt Even/8 Odd/8 Even/8 Odd/8 The SRS C = D ∪ X simulates the function C and the SRS T = D ∪ X C T simulates the function T . We do not formally state the analogue of Proposition 4.8 —ter- Even/8 Odd/8 minations of the eight subsystems obtained from C or T are each equivalent to the question of whether all nonconvergent Collatz trajectories have to encounter the corre- sponding residue class modulo 8. Through automated proofs, we were able to establish the following. Theorem 4.10 If there exists a nonconvergent Collatz trajectory, it cannot avoid the residue classes of 2, 3, 4, 6 modulo 8. Theorems 4.9 and 4.10 are also not difﬁcult to prove by hand; however, it remains open whether an analogue of Theorem 4.10 holds for the residue classes of 0, 1, 5, 7 modulo 8, that is, we have neither manual nor automated proofs for these cases. They may serve well as easier Collatz-like open problems to test our abilities against, so we offer a $500 reward for a resolution of any of the following conjectures. See Denend [39, Section 4] for a heuristic prediction of the relative easiness of those cases. Denend uses an empirical measure based on the number of odd elements occurring in a trajectory until either a certain residue class or 1 is encountered, which resembles the ones-ratio and the stopping time ratio deﬁned by Applegate and Lagarias [40]. The case 0 is omitted as its answer follows from the case 5 by Figure 1. 123 15 Page 32 of 44 E. Yolcu et al. Conjecture 4.11 All nonconvergent C-trajectories contain some n ≡ 1 (mod 8). Conjecture 4.12 All nonconvergent C-trajectories contain some n ≡ 5 (mod 8). Conjecture 4.13 All nonconvergent C-trajectories contain some n ≡ 7 (mod 8). Even the following easier statement remains unproved, although we were able to prove (both manually and automatically) its versions with {1, 5} and {1, 7} as the residue classes. Conjecture 4.14 All nonconvergent C-trajectories contain either some n ≡ 5 (mod 8) or some n ≡ 7 (mod 8). We can alternatively formulate each of the above conjectures as the convergence problem of some partial generalized Collatz function. For instance, Conjecture 4.14 is equivalent to + + the convergence of the function H : N → N deﬁned as follows. ⊥ ⊥ 3n ⎪ if n ≡ 0 (mod 4) 9n+1 H (n) = if n ≡ 7 (mod 8) (10) ⊥ otherwise Proposition 4.15 H is convergent if and only if all nonconvergent C-trajectories contain either some n ≡ 5 (mod 8) or some n ≡ 7 (mod 8). Proof Recall from Figure 1 the transition graph of the iterates in C-trajectories across residue classes modulo 8. Observe that if a nonconvergent trajectory avoids the residue classes of 5 and 7 (mod 8), then it has to visit the residue class of 1 (mod 8), so we may assume without loss of generality that each nonconvergent trajectory starts with some n ≡ 1 (mod 8). Then a nonconvergent trajectory that avoids the residue classes of 5 and 7 (mod 8) can traverse only the cycle of classes (1, 4, 2, 1) or (1, 4, 6, 3, 2, 1). The former, which is traversed only if n ≡ 1 (mod 32), effects the map n → (3n + 1)/4. The latter, which is traversed only if n ≡ 57 (mod 64), effects the map n → (9n + 7)/8. If n belongs to any other residue class, either the trajectory is convergent, or it contains some k ≡ 5 (mod 8) or some k ≡ 7 + + (mod 8). As a result, the function G : N \{1}→ N \{1} deﬁned as ⊥ ⊥ 3n+1 ⎪ if n ≡ 1 (mod 32) 9n+7 G(n) = if n ≡ 57 (mod 64) ⊥ otherwise is nonconvergent if and only if there exists a nonconvergent C-trajectory that avoids the residue classes of 5 and 7 (mod 8). Moreover, H as deﬁned in (10)isconvergentifand only if G is convergent, because the bijection n → (n − 1)/8mapsa G-trajectory to an H-trajectory. 4.6 SAT Solving Considerations Phase-Saving Heuristic Most top-tier termination tools, such as AProVE, Matchbox,and T T ,use theSAT solver MiniSat [41] to search for matrix interpretations. This choice is T 2 somewhat surprising as MiniSat has not been updated since 2008 and the performance of SAT solvers has improved signiﬁcantly in the last decade. The use of MiniSat in these provers is motivated by its observed effectiveness in ﬁnding interpretations. We investigated the reason for this, which turned out to be a heuristic that MiniSat disables in its default conﬁguration. 123 Automated Approach to Collatz Conjecture Page 33 of 44 15 Most SAT solvers sort variables by the frequency of their occurrences in recent conﬂict clauses, selecting the highest ranked one as the variable to branch on [42]. This procedure is similar in MiniSat and modern SAT solvers. However, once a variable is picked, the solvers differ in the truth value assignment that they explore ﬁrst. MiniSat uses negative branching [41], which explores the “false” branch ﬁrst for all decision variables. The empirical effectiveness of this heuristic likely stems from its interaction with the common choices of propositional encodings used when translating problems into SAT instances. Modern SAT solvers use phase-saving [43], which ﬁrst explores the branch corresponding to the truth value to which the variable was forced most recently during unit propagation. We offer the following explanation for the effectiveness of negative branching. We use the order encoding [44, 45] when translating the integer constraints from Section 2.3 into CNF formulas. In this encoding, each variable X that takes values in a ﬁnite domain A ={0, 1,..., n + 1} is represented by a corresponding list of n + 1 Boolean variables (x , x ,..., x ). Each Boolean variable x indicates X > i.Asanexample, X = 2has 0 1 n i the corresponding assignment (1, 1, 0, 0,..., 0). This encoding gives a natural way of rep- resenting inequality constraints. For instance, the constraint a < X ≤ b can be enforced simply by setting x = 1and x = 0. As another example, for variables X, Y the inequality a b X ≤ Y can be expressed by the conjunction (¬x ∨ y ). Consequently, when using the i i i =0 order encoding, representations that correspond to smaller numbers require setting a larger fraction of the Boolean variables to false. For instance, the representation of zero or minus inﬁnity assigns all variables to false. Moreover, the matrices and the vectors that occur in the interpretations are often sparse and contain relatively few large numbers. As a result, negative branching possibly directs the search towards a satisfying assignment more often. Additionally, in contrast to phase-saving, negative branching tends to guide the solver to a potentially different part of the search space after a restart (which is performed frequently in SAT solvers). The increased diversity of the search space (across restarts) that is explored due to negative branching is also possibly helpful for the kinds of the problems discussed in this paper. One can enable negative branching in most SAT solvers, which in our case improves solver performance for some of the formulas that encode the existence of interpretations. Heavy-Tailed Behavior of SAT Solvers Combinatorial search algorithms can have a tendency to show a large variance in runtime across different, randomly selected initial conditions of the search. For instance, Gomes et al. [46] observed that DPLL solvers [47, 48] had a substantial fraction of very short runs when dealing with relatively hard instances. This suggests that trying to solve such instances using several parallel runs is a reasonable strategy, since some of the runs will have a nonnegligible chance of ﬁnishing early. Modern SAT solvers incorporate heuristics that alleviate the heavy-tailed behavior to some extent; however, the variability in runtime (especially on satisﬁable instances) is not completely eliminated. In our termination prover, we run multiple instances of the SAT solver (speciﬁcally, CaDiCaL [49]) in parallel on the formula that encodes the existence of an interpretation. We introduce additional randomness to the procedure by running each parallel instance with a different shufﬂing of the clauses in the formula. Ideally, solver performance would be invariant to the ordering of the clauses; however, the clause order indirectly affects the variable selection heuristic, which ends up inﬂuencing runtime. Experiments with Solver Conﬁgurations Table 2 shows the difference in runtime for both MiniSat and CaDiCaL due to negative branching and parallelism with a few small-scale 123 15 Page 34 of 44 E. Yolcu et al. Table 2 Difference in runtime due to negative branching and parallelism. Each row cor- responds to a single step of a relative termination proof occurring in the previous sections of this paper. The leftmost columns show the original system being proved as terminating, along with the parameters of the interpretations being searched for (D for dimension, V for the number of different values each coefﬁcient may take) that remove at least a single rule from the system. For each solver, each of the remaining columns shows the median time the experiment takes over 25 repetitions. Each run times out after 120 seconds, and runs that time out are counted as having taken double the allowed time. Phase-saving Negative branching Problem Interp. DV Solver Single Parallel Single Parallel F Arctic 5 8 240.00s 240.00s 85.60s 5.47s T \{f → } Arctic 3 5 0.62s 0.09s 67.69s 15.74s T \{f0 → 0f} Arctic 3 4 3.18s 0.91s 2.19s 0.91s T \{t2 → 2t} Natural 4 4 240.00s 63.71s 240.00s 87.85s T \{2 → ft} Natural 4 4 240.00s 240.00s 69.73s 5.25s T \{2 → ft} Arctic 4 3 1.39s 0.18s 7.65s 1.71s Even/8 C \{ttf → tt} Natural 3 11 240.00s 240.00s 240.00s 240.00s Odd/8 T \{ftt → 1ft} Arctic 3 12 2.35s 0.36s 117.37s 0.88s F Arctic 5 8 240.00s 240.00s 44.45s 9.22s T \{f → } Arctic 3 5 1.52s 0.13s 29.95s 13.12s T \{f0 → 0f} Arctic 3 4 3.75s 0.83s 3.27s 1.71s T \{t2 → 2t} Natural 4 4 75.78s 19.12s 29.62s 8.13s T \{2 → ft} Natural 4 4 75.05s 5.22s 24.31s 6.43s T \{2 → ft} Arctic 4 3 3.33s 0.52s 11.55s 3.84s Even/8 C \{ttf → tt} Natural 3 11 240.00s 240.00s 240.00s 79.05s Odd/8 T \{ftt → 1ft} Arctic 3 12 1.94s 0.33s 3.28s 0.38s experiments. From all the automated proofs in this paper, we selected the steps where the SAT solving phase took longer than 2 seconds, and reran the prover for these speciﬁc steps with different conﬁgurations of those SAT solvers. When running only a single instance of a solver, we used the nonshufﬂed formula. In the parallel case, we ran 8 solver instances with one of the instances receiving the nonshufﬂed formula and the other 7 receiving random shufﬂes. Running multiple instances of a solver in parallel is a considerable improvement in all cases where the allotted time is enough to ﬁnd an interpretation. Negative branching has an adverse effect in some cases, although in two of the most difﬁcult instances (F and Even/8 C \{ttf → tt}) it makes the difference between ﬁnding an interpretation relatively quickly and timing out. It also appears that, at least for the more difﬁcult cases, replacing MiniSat by CaDiCaL can be beneﬁcial. These experiments are not extensive enough to derive broad conclusions; however, they suggest that running multiple instances of a modern SAT solver with negative branching enabled in some and disabled in others can be a reasonably diverse strategy when searching for matrix interpretations. CaDiCaL MiniSat Automated Approach to Collatz Conjecture Page 35 of 44 15 5 Related Work There are several previous studies of the Collatz conjecture through alternative models of computation. String Rewriting Systems To our knowledge, Zantema [13], with his system Z,which we saw in Section 3.1, was the ﬁrst to attempt using an automated method and string rewriting to search for a proof of the Collatz conjecture. In addition, although we independently discovered the mixed binary–ternary system described in Section 3.2, Scollo [50] had essentially the same idea, the distinction being that he adopted a functional view of the digits that is different than in (8). Scollo was not concerned with proving termination, though, and proposed rewriting primarily as a formalism that forgoes the arithmetic interpretation of the iterates and instead emphasizes the dynamic/computational behavior. Tag Systems An m-tag system [51] is a computational model described by a set of produc- tion rules that map symbols to strings (or “tags”). Given an initial string X = x x ... x ,the 0 1 n tag system ﬁnds the rule x Z whose LHS matches the leftmost symbol of X, appends the tag Z to X, and deletes the ﬁrst m symbols of XZ; resulting in a new string X = x x ... x Z. m m+1 n The tag system repeats this transformation until reaching a string of length less than m,at which point it halts. De Mol [52] showed the existence of a small 2-tag system with the following rules that simulates the iterated application of the Collatz function given a unary representation: This tag system halts if and only if the Collatz conjecture holds, giving yet another formulation of the problem. De Mol further extended this scheme to allow the simulation of an arbitrary generalized Collatz function with modulus d by a d-tag system. Cellular Automata Kari [53] designed 1D cellular automata that perform multiplication by 3and 3/2 in base 6, and reformulated both the Collatz conjecture and Mahler’s 3/2 problem as sets of constraints to be satisﬁed by the space-time diagrams of these cellular automata. String Arithmetic Kauffman [54] developed a formalism to perform arithmetic, which he called string arithmetic, and expressed the Collatz conjecture within it. This formalism works with unary representations of numbers, and uses the three symbols 1, , . Letting denote the empty string and N be any string representing a number, string arithmetic consists of the following bidirectional rewrite rules (or “identities”) to convert between different strings representing the same number: ← → 11 ← → 1 1N ← → N1 Along with the above identities, Kauffman’s encoding of the Collatz function uses the fol- lowing two rules: N → N N1 → N1N 123 15 Page 36 of 44 E. Yolcu et al. The Collatz conjecture becomes the question of whether for strings of 1s of all lengths there exists a rewrite sequence using the ﬁve rules above to reach the string 1. 6 Conclusions We presented an approach to prove convergence of instances of generalized Collatz functions by translating them into string rewriting systems and applying SAT solving to ﬁnd matrix interpretations that show termination. Important components of our approach include the quality of the translation into rewriting, the use of weakly monotone -algebras, and dedi- cated heuristics in the SAT solving phase. We considered some interesting, simpler variants of the Collatz conjecture to gauge the feasibility of this approach in proving mathemati- cally interesting statements. We observed that some variants could be solved only via natural matrix interpretations, while others required arctic matrix interpretations. Several extensions to this work can further our understanding of the potential of rewriting techniques for answering mathematical questions. For instance, it is of interest to study the efﬁcacy of different termination proving techniques on the problems that we considered. In particular, we found matrix interpretations to be the most successful for our purposes despite the existence of newer techniques developed for automatically proving termination of a few select challenging instances. Although matrix interpretations lead to automated proofs of several weakened variants discussed in this paper, it might still be the case that there exist no such interpretations to establish the termination of the Collatz system T (as we have shown in the case of natural matrix interpretations for Zantema’s system Z). This would be an interesting result in itself. Another issue is the matter of representation; speciﬁcally, it is worth exploring whether there exists a suitable translation of the Collatz conjecture into the termination of a term, instead of string, rewriting system since many automated termination proving techniques are generalized to term rewriting. Finally, injecting problem-speciﬁc knowledge into the rewriting systems or the termination techniques would be helpful as there exists a wealth of information about the Collatz conjecture that could simplify the search for a termination proof. Acknowledgements We thank Johannes Waldmann for insightful discussions regarding arctic matrix inter- pretations, for pointing us to [53] and the rewriting system in Example 3.3, for responding to our challenge to solve Farkas’ variant with Matchbox, and for feedback on an early draft. We thank Carsten Fuhs and Jürgen Giesl for responding to our challenge to solve Farkas’ variant with AProVE. We additionally thank Carsten Fuhs for his thorough explanations of the dependency pair framework and AProVE’s strategies. We thank Florian Frohn for responding to the challenge to solve the subsystems from Section 4.3 with AProVE.We thank Jeffrey Lagarias for discussions regarding the problems in Section 4.5. We thank Luke Schaeffer and Chris Lynch for discussions on alternative rewriting systems that simulate the Collatz map. We thank Jeremy Avigad and Jasmin Blanchette for their detailed comments on an early draft. Finally, we thank the reviewers of CADE for their comments on the preliminary version of this paper and the reviewers of the Journal of Automated Reasoning for their comments on the journal version. This material is based upon work supported by the National Science Foundation under grant CCF-2006363. Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. 123 Automated Approach to Collatz Conjecture Page 37 of 44 15 A Alternative Proof of Lemma 3.16 Let us recall the statement of the result before proceeding with the proof. Lemma 3.16 If T is terminating on all initial strings of the canonical form (f|t|0|1|2) , then T is terminating (on all initial strings). Proof Assume there exists some string X ∈{f, t, 0, 1, 2, , } that admits an inﬁnite rewrite sequence for T .View X as split into blocks delimited by or , i.e., for some k ∈ N , write X = N d N d ... d N , 1 1 2 2 k−1 k where d ∈{, } for each 1 ≤ i < k,and N ∈{f, t, 0, 1, 2} for each 1 ≤ i ≤ k.Any i i string containing X also admits an inﬁnite rewrite sequence, so instead consider Z = d Xd , 0 k written as Z = d N d N d ... d N d , 0 1 1 2 2 k−1 k k where d , d ∈{, }. 0 k As T is not terminating on Z, there exists some rewrite rule applicable to it. Consider an arbitrary block of Z along with its neighbors (to which some rewrite rule of T applies), written as V = PcQd R, where c, d ∈{, } and P, Q, R ∈{f, t, 0, 1, 2} . Due to the shapes of the rules of T ,the string V can be rewritten only into one of the following: " " V = PcQd R such that Pc → Pc 1 T " " V = PcQd R such that cQd → cQd 2 T " " V = PcQd R such that dR → d R 3 T In any case, the delimiters are unchanged, and only a single block is affected by the rewrite. This means that any rewrite sequence that starts from Z consists of several sequences that each operate entirely on some block of Z. Thus, since Z has ﬁnitely many blocks, there exists some block that admits an inﬁnite rewrite sequence. In particular, there exists a string cNd, where c, d ∈{, } and N ∈{f, t, 0, 1, 2} , that can be rewritten indeﬁnitely. We claim that this requires c = and d = , so the string cNd is of the canonical form (f|t|0|1|2) .As shown below, the other cases are all terminating. (i) N : This string does not contain , so it can be rewritten using only the rules in T \ B, but we know from Lemma 3.15 that SN(T \ B), so there can be no inﬁnite rewrite sequence. (ii) N : This string does not contain , so it can be rewritten using only the rules in T \D , but we know from Lemma 3.15 that SN(T \ D ), so there can be no inﬁnite rewrite sequence. (iii) N :The SRS T contains no rules of the form s → t or s → t for any s, t,so this string can be rewritten using only the rules in T \ (B ∪ D ). Since each subset of a terminating SRS is terminating, by Lemma 3.15 we conclude SN(T \ (B ∪ D )),so there can be no inﬁnite rewrite sequence. This proves the contrapositive of the lemma statement. 123 15 Page 38 of 44 E. Yolcu et al. B Remaining Part of the Automated Proof for Farkas’ Variant rev With the interpretations from (9), the rules of F satisfy the following relations: ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 1 −−−− − 0 −−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 252 −− 0 040 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [f0](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[0](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 −−−− 0 1 −−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [f1](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[1](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 252 −− 0 140 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [t1](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[21](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 − 2 − 2 0 0 − 1 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [t2](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[22](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2642 − 0 25 2 −− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 64 −− − − 60 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0f](x) = 264 −− x ⊕ − ≥ 26 2 −− x ⊕ − =[f0](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ 2532 − 0 −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−− 3 − 1 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 264 −− − 06 0 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1f](x) = 264 −− x ⊕ − ≥ 26 2 −− x ⊕ − =[t0](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−− 2 − 0 −−−−− − 2532 − 0 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 −− 2 − 0 2 −−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 64 −− − − 62 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [2f](x) = 3 −− 2 − x ⊕ 0 ≥ 3 −−−− x ⊕ − =[f1](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − 2 −− 2 − 0 −−−−− − 123 Automated Approach to Collatz Conjecture Page 39 of 44 15 ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 464 − 4 0 25 2 −− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 464 − 4 − 162 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0t](x) = 464 − 4 x ⊕ − ≥ 362 −− x ⊕ − =[t1](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ 353 − 3 0 −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−− 3 1 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 464 − 4 − 061 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1t](x) = 464 − 4 x ⊕ − ≥ 2 − 2 −− x ⊕ − =[f2](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−− 2 0 −−−−− − 353 − 3 0 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 − 2 − 2 0 2 − 2 − 2 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 464 − 4 − 061 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [2t](x) = 3 − 3 − 2 x ⊕ 0 ≥ 2 − 3 − 2 x ⊕ − =[t2](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − 2 − 2 − 2 0 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−−− 6 −−−−− 6 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− 6 −−−−− 4 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0](x) = −−−−− x ⊕ 6 ≥ −−−−− x ⊕ 2 =[t](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− 5 −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−−− 1 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− 6 −−−−− 6 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1](x) = −−−−− x ⊕ 6 ≥ −−−−− x ⊕ 2 =[ff](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− 0 −−−−− − −−−−− 5 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−−− 0 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− 6 −−−−− 6 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [2](x) = −−−−− x ⊕ 4 ≥ −−−−− x ⊕ 4 =[tf](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− 4 −−−−− − C More Problems to Approach via Rewriting We adapt the mixed base scheme for several other open problems and reformulate them as termination of relatively small rewriting systems. C.1 Mahler’s 3/2 Problem Deﬁnition C.1 Let ξ ∈ R be a positive real number. It is called a Z-number if for all k ∈ N >0 # $ 3 1 we have frac ξ < , where frac(·) denotes the fractional part of the number. 2 2 123 15 Page 40 of 44 E. Yolcu et al. Mahler [55] conjectured that there are no Z-numbers. Moreover, he considered a gener- + + alized Collatz function M : N → N , deﬁned as follows. 3n if n ≡ 0 (mod 2) M (n) = 3n+1 if n ≡ 1 (mod 2) He related the behaviors of M-trajectories to the existence of Z-numbers: Theorem C.2 For n ∈ N , if a Z-number exists in the interval [n, n + 1), then there is no k ∈ N for which M (n) ≡ 3 (mod 4). In order to formulate this as a termination problem, we split the odd case of M into two and leave one undeﬁned: 3n ⎪ if n ≡ 0 (mod 2) 3n+1 M (n) = if n ≡ 1 (mod 4) ⊥ if n ≡ 3 (mod 4) Given n ∈ N , if the trajectory M (n) contains ⊥ then by the contrapositive of Theorem C.2 there is no Z-number in the interval [n, n + 1). When proving nonexistence, we may assume without loss of generality that a Z-number is at least 1, since if ξ ∈ (0, 1) is a Z-number then ξ ∈[1, ∞) is another one for sufﬁciently large m ∈ N. Thus, the nonexistence of Z-numbers can be established by proving that M is convergent, which is equivalent to the termination of the following rewriting system M. In order to ensure termination at the case n ≡ 3 (mod 4), there is no rule with the LHS tt. f → 0 f0 → 0f t0 → 1t 0 → t ft → 10 f1 → 0t t1 → 2f 1 → ff f2 → 1f t2 → 2t 2 → ft C.2 Halting Problem for Busy Beavers The busy beaver problem [56] concerns ﬁnding binary-alphabet Turing machines with n states that, when given an input tape of all 0s, write the largest number of 1s on the tape upon halting. For each n, a machine that achieves this is called an n-state Busy Beaver (or BB-n for short). Note that this deﬁnition only requires the machines to halt on all-0 inputs, leaving the behavior on other inputs unspeciﬁed and allowing them not to halt in general. Michel [31] observed that for n ∈{2, 3, 4}, the busy beaver machines are all total Turing machines, i.e., they halt on all inputs, and moreover proved that they all simulate some generalized Collatz function. It is an open problem whether all busy beavers are total Turing machines. In particular, it is unknown whether the current BB-5 candidate is total. Michel showed that the BB-5 candidate simulates the following generalized Collatz function. 5n+18 ⎪ if n ≡ 0 (mod 3) 5n+22 B(n) = if n ≡ 1 (mod 3) ⊥ if n ≡ 2 (mod 3) Convergence of the above function can be studied via the termination of a corresponding rewriting system, although the translation is not as straightforward as the other generalized Collatz functions we have in this paper. Speciﬁcally, the mixed base scheme results in a compact rewriting system only when all the mappings an + b → cn + d appliedbythe 123 Automated Approach to Collatz Conjecture Page 41 of 44 15 generalized Collatz function at hand satisfy d < c. This is not the case for the function B above since it requires us to express 3n → 5n + 6and 3n + 1 → 5n + 9. These mappings are expressed more easily by the help of unary representations, so we can have the following hybrid rewriting system BB over the alphabet {i, v, 0, , } to simulate the function B, where the new symbol v has the functional view v(x ) = 5x. 0 → ivi 0iii → i0 ii → 0 0i → iviiii iv → viiiii v → 0ii 0v → v0 We did not succeed in proving the termination of this rewriting system, which is not too surprising since the hybrid scheme does not even pass the test of proving the convergence of W . Alternatively, we can split the cases of B further for the congruence classes modulo 3 with k > 1 until the iterated application of B can either be expressed as an + b → cn + d with d < c, or it reaches ⊥. After we perform this procedure while ensuring that the number of newly introduced cases are kept to a minimum, we end up with the following mappings to simulate B in an accelerated manner (similar to the idea in Section 4.4). 9n → 25n + 16 9n + 1 → 25n + 21 27n + 6 → 125n + 64 27n + 7 → 125n + 71 (11) 27n + 16 → 125n + 114 81n + 51 → 625n + 459 243n + 78 → 3125n + 1116 243n + 159 → 3125n + 2159 Consider the symbols {0, 1, 2, v, w, x, y, z, , } with the following functional views. v(x ) = 5x 0(x ) = 3x w(x ) = 5x + 1 (x ) = 0 1(x ) = 3x + 1 x(x ) = 5x + 2 (x ) = x 2(x ) = 3x + 2 y(x ) = 5x + 3 z(x ) = 5x + 4 With these symbols, we have the following mixed {3, 5}-ary (ternary–quinary) system BB the termination of which is equivalent to the convergence of B. The dynamic rules on the left implement the mappings from (11) and the rest are auxiliary rules that push ternary symbols towards the rightmost end of the string while preserving its value. We were unable to prove the termination of this system, so we include it as yet another challenge for automated termination proving. 00 → yw 0v → v0 1v → w2 2v → y1 v → 0 01 → zw 0w → v1 1w → x0 2w → y2 w → 1 020 → xxz 0x → v2 1x → x1 2x → z0 x → 2 021 → xzw 0y → w0 1y → x2 2y → z1 y → 10 121 → zxz 0z → w1 1z → y0 2z → z2 z → 11 1220 → yywz 02220 → wyzyw 12220 → yxwwz 123 15 Page 42 of 44 E. Yolcu et al. C.3 Ternary Expansions of 2 Erdos ˝ [57] asked: When does the ternary expansion of 2 omit the digit 2? This is the case 0 2 8 for 2 = (1) ,2 = (11) ,and 2 = (100111) . He conjectured that it does not happen 3 3 3 for n > 8. This conjecture can be reformulated as the statement that the following rewriting ← − system E,where X ={r → | → r ∈ X }, is terminating on all initial strings of the form 8 + f f . ⎧ ⎫ 0 → 0f → f0 1t → t0 t → 0 ⎨ ⎬ ← − 1 → 0t → f1 2f → t1 ff → 1 X = ⎩ ⎭ → 1f → f2 2t → t2 ft → 2 Given a string that corresponds to the binary representation of a power of 2, the inverted ← − system X essentially rewrites the string into ternary by pushing ternary symbols to the right without altering the value that the string represents. The two rules {0 → , 1 → } remove the occurrences of the ternary digits 0 and 1 (but not 2). If the ternary expansion does not contain the digit 2 then all digits will be removed, resulting in the string that can then be rewritten to itself indeﬁnitely. This problem, as described, is an instance of “local termination” [58] since it is concerned with termination on not all possible strings but a subset of them. We have not performed experiments with this system or local termination yet and we leave this for future work. References 1. Lagarias, J.C.: The Ultimate Challenge: The 3x +1 Problem. American Mathematical Society, Providence (2010) 2. Lagarias, J.C.: The 3x + 1 Problem: An Annotated Bibliography (1963–1999). arXiv:math/0309224 (2011) 3. Lagarias, J.C.: The 3x + 1 Problem: An Annotated Bibliography, II (2000–2009). arXiv:math/0608208 (2012) 4. Tao, T.: Almost All Orbits of the Collatz Map Attain Almost Bounded Values. arXiv:1909.03562 (2020) 5. Barina, D.: Convergence veriﬁcation of the Collatz problem. The Journal of Supercomputing 77(3), 2681–2688 (2021). https://doi.org/10.1007/s11227-020-03368-x 6. Lagarias, J.C.: The 3x + 1 problem and its generalizations. The American Mathematical Monthly 92(1), 3–23 (1985). https://doi.org/10.2307/2322189 7. Conway, J.H.: Unpredictable iterations. In: Proceedings of the Number Theory Conference (University of Colorado, Boulder, Colorado), pp. 49–52 (1972) 8. Kurtz, S.A., Simon, J.: The undecidability of the generalized Collatz problem. In: Proceedings of the 4th International Conference on Theory and Applications of Models of Computation (TAMC). Lecture Notes in Computer Science, pp. 542–553. Springer, New York (2007). https://doi.org/10.1007/978-3- 540-72504-6_49 9. Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 328–342. Springer, New York (2006). https://doi.org/10.1007/11805618_25 10. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning 40(2), 195–220 (2008). https://doi.org/10.1007/s10817-007-9087-9 11. Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybernetica 19(2), 357–392 (2009) 12. Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certiﬁcation of termination and complex- ity proofs. In: Proceedings of the 25th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 441–455. Springer, New York (2014). https://doi.org/10. 1007/978-3-319-08918-8_30 13. Zantema, H.: Termination of string rewriting proved automatically. Journal of Automated Reasoning 34(2), 105–139 (2005). https://doi.org/10.1007/s10817-005-6545-0 123 Automated Approach to Collatz Conjecture Page 43 of 44 15 14. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8 15. Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisﬁability. IEEE Transactions on Computers 48(5), 506–521 (1999). https://doi.org/10.1109/12.769433 16. Yolcu, E., Aaronson, S., Heule, M.J.H.: An automated approach to the Collatz conjecture. In: Proceedings of the 28th Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, pp. 468– 484. Springer, New York (2021). https://doi.org/10.1007/978-3-030-79876-5_27 17. Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993). https://doi.org/10.1007/978- 1-4613-9771-7 18. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https://doi.org/10.1017/CBO9781139172752 19. Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17(1), 23–50 (1994). https://doi.org/10.1006/jsco.1994.1003 20. Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. Journal of Automated Reasoning 58(1), 3–31 (2017). https:// doi.org/10.1007/s10817-016-9388-y 21. Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: Proceedings of the 15th Interna- tional Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 85–94. Springer, New York (2004). https://doi.org/10.1007/978-3-540-25979-4_6 22. Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 295–304. Springer, New York (2009). https://doi.org/10.1007/978-3-642-02348- 4_21 23. Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretation. In: Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM). Lecture Notes in Computer Science, pp. 283–295. Springer, New York (2010). https://doi.org/10.1007/978-3-642-11266- 9_24 24. rn Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewrit- ing. In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA). Leibniz International Proceedings in Informatics, pp. 251–266. Schloss Dagstuhl, Wadern (2011). https://doi.org/10.4230/LIPIcs.RTA.2011.251 25. Bak, P., Tang, C., Wiesenfeld, K.: Self-organized criticality: An explanation of the 1/ f noise. Physical Review Letters 59(4), 381–384 (1987). https://doi.org/10.1103/PhysRevLett.59.381 26. Rawsthorne, D.A.: Imitation of an iteration. Mathematics Magazine 58(3), 172–176 (1985). https://doi. org/10.2307/2689917 27. Wagon, S.: The Collatz problem. The Mathematical Intelligencer 7(1), 72–76 (1985). https://doi.org/10. 1007/BF03023011 28. Buttsworth, R.N., Matthews, K.R.: On some Markov matrices arising from the generalized Collatz map- ping. Acta Arithmetica 55(1), 43–57 (1990). https://doi.org/10.4064/aa-55-1-43-57 29. Kašcák, ˇ F.: Small universal one-state linear operator algorithm. In: Proceedings of the 17th International Symposium on Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science, pp. 327–335. Springer, New York (1992). https://doi.org/10.1007/3-540-55808-X_31 30. Kohl, S.: Wildness of iteration of certain residue-class-wise afﬁne mappings. Advances in Applied Math- ematics 39(3), 322–328 (2007). https://doi.org/10.1016/j.aam.2006.08.003 31. Michel, P.: Problems in number theory from busy beaver competition. Logical Methods in Computer Science 11(4:10), (2015). https://doi.org/10.2168/LMCS-11(4:10)2015 32. Reutenauer, C., Berstel, J.: Noncommutative Rational Series with Applications. Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9780511760860 33. Soittola, M.: Positive rational sequences. Theoretical Computer Science 2(3), 317–322 (1976). https:// doi.org/10.1016/0304-3975(76)90084-0 34. Cantor, G.: Über einfache zahlensysteme. Zeitschrift für Mathematik und Physik 14, 121–128 (1869) 35. Sabel, D., Zantema, H.: Termination of cycle rewriting by transformation and matrix interpretation. Logical Methods in Computer Science 13(1:11), (2017). https://doi.org/10.23638/LMCS-13(1:11)2017 36. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006). https://doi.org/10.1007/s10817-006-9057-7 37. Farkas, H.M.: Variants of the 3N + 1 conjecture and multiplicative semigroups. In: Geometry, Spec- tral Theory, Groups, and Dynamics. Contemporary Mathematics, pp. 121–127. American Mathematical Society, Providence (2005). https://doi.org/10.1090/conm/387/07238 123 15 Page 44 of 44 E. Yolcu et al. 38. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: In: Proceedings of the 3rd International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 167–177. Springer, New York (1989). https://doi.org/10.1007/3-540-51081- 8_107 39. Denend, M.: Challenging variants of the Collatz conjecture. Master’s thesis, University of Texas at Austin (2018). https://doi.org/10.26153/tsw/1559 40. Applegate, D., Lagarias, J.C.: Lower bounds for the total stopping time of 3x + 1 iterates. Mathematics of Computation 72(242), 1035–1049 (2003). https://doi.org/10.1090/S0025-5718-02-01425-4 41. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proceedings of the 6th International Conference on Theory and Applications of Satisﬁability Testing (SAT). Lecture Notes in Computer Science, pp. 502–518. Springer, New York (2004). https://doi.org/10.1007/978-3-540-24605-3_37 42. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efﬁcient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC), pp. 530–535. Association for Computing Machinery, New York (2001). https://doi.org/10.1145/378239.379017 43. Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisﬁability solvers. In: Proceedings of the 10th International Conference on Theory and Applications of Satisﬁability Testing (SAT). Lecture Notes in Computer Science, pp. 294–299. Springer, New York (2007). https://doi.org/10. 1007/978-3-540-72788-0_28 44. Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling ﬁnite linear CSP into SAT. Constraints 14(2), 254–272 (2009). https://doi.org/10.1007/s10601-008-9061-0 45. Petke, J., Jeavons, P.: The order encoding: From tractable CSP to tractable SAT. In: Proceedings of the 14th International Conference on Theory and Applications of Satisﬁability Testing (SAT). Lecture Notes in Computer Science, pp. 371–372. Springer, New York (2011). https://doi.org/10.1007/978-3-642-21581- 0_34 46. Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisﬁability and constraint satisfaction problems. Journal of Automated Reasoning 24(1), 67–100 (2000). https://doi.org/10.1023/ A:1006314320276 47. Davis, M., Putnam, H.: A computing procedure for quantiﬁcation theory. Journal of the ACM 7(3), 201–215 (1960). https://doi.org/10.1145/321033.321034 48. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962). https://doi.org/10.1145/368273.368557 49. Biere, A.: CaDiCaL at the SAT Race 2019. In: Proceedings of the SAT Race 2019: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, pp. 8–9. University of Helsinki, Helsinki (2019) 50. Scollo, G.: ω-rewriting the Collatz problem. Fundamenta Informaticae 64(1–4), 405–416 (2005) 51. Post, E.L.: Formal reductions of the general combinatorial decision problem. American Journal of Math- ematics 65(2), 197–215 (1943). https://doi.org/10.2307/2371809 52. De Mol, L.: Tag systems and Collatz-like functions. Theoretical Computer Science 390(1), 92–101 (2008). https://doi.org/10.1016/j.tcs.2007.10.020 53. Kari, J.: Cellular automata, the Collatz conjecture and powers of 3/2. In: Proceedings of the 16th Inter- national Conference on Developments in Language Theory (DLT). Lecture Notes in Computer Science, pp. 40–49. Springer, New York (2012). https://doi.org/10.1007/978-3-642-31653-1_5 54. Kauffman, L.H.: Arithmetic in the form. Cybernetics and Systems 26(1), 1–57 (1995). https://doi.org/10. 1080/01969729508927486 55. Mahler, K.: An unsolved problem on the powers of 3/2. Journal of the Australian Mathematical Society 8(2), 313–321 (1968). https://doi.org/10.1017/S1446788700005371 56. Radó, T.: On non-computable functions. The Bell System Technical Journal 41(3), 877–884 (1962). https://doi.org/10.1002/j.1538-7305.1962.tb00480.x 57. Erdos, ˝ P.: Some unconventional problems in number theory. Mathematics Magazine 52(2), 67–70 (1979). https://doi.org/10.2307/2689842 58. Waldmann, J., de Vrijer, R., Endrullis, J.: Local termination: Theory and practice. Logical Methods in Computer Science 6(3:20), (2010). https://doi.org/10.2168/LMCS-6(3:20)2010 Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional afﬁliations. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals http://www.deepdyve.com/lp/springer-journals/an-automated-approach-to-the-collatz-conjecture-SCed0ywpgw

Loading next page...

References (74)

D. Applegate, J. Lagarias (2001)
Lower bounds for the total stopping time of 3x + 1 iterates
Math. Comput., 72
(1869)
Über einfache zahlensysteme
Daniel Rawsthorne (1985)
Imitation of an Iteration
Mathematics Magazine, 58
D. Hofbauer, Johannes Waldmann (2006)
Termination of String Rewriting with Matrix Interpretations
G Scollo (2005)
?\documentclass[12pt]{minimal}
Fundamenta Informaticae, 64
T. Arts, J. Giesl (2000)
Termination of term rewriting using dependency pairs
Theor. Comput. Sci., 236
L. Mol (2008)
Tag systems and Collatz-like functions
Theor. Comput. Sci., 390
P. Bak, Chao Tang, K. Wiesenfeld (1988)
Self-organized criticality.
Physical review. A, General physics, 38 1
P Bak, C Tang, K Wiesenfeld (1987)
Self-organized criticality: An explanation of the 1/f\documentclass[12pt]{minimal}
Physical Review Letters, 59
(2008)
Compiling finite linear CSP into SAT
J. Endrullis, Johannes Waldmann, H. Zantema (2006)
Matrix Interpretations for Proving Termination of Term Rewriting
Journal of Automated Reasoning, 40
Martin Korp, C. Sternagel, Harald Zankl, A. Middeldorp (2009)
Tyrolean Termination Tool 2
Chang Liu (2000)
Term rewriting and all that
ACM SIGSOFT Softw. Eng. Notes, 25
J. Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephan Swiderski, René Thiemann (2016)
Analyzing Program Termination and Complexity Automatically with AProVE
Journal of Automated Reasoning, 58
R. Book, F. Otto (1993)
String-Rewriting Systems
F. Kascak (1992)
Small Universal One-State Linear Operator Algorithm
D Applegate, JC Lagarias (2003)
Lower bounds for the total stopping time of 3x+1\documentclass[12pt]{minimal}
Mathematics of Computation, 72
A. Koprowski, Johannes Waldmann (2009)
Max/Plus Tree Automata for Termination of Term Rewriting
Acta Cybern., 19
M. Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, S. Malik (2001)
Chaff: engineering an efficient SAT solver
Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232)
H. Zantema (1994)
Termination of Term Rewriting: Interpretation and Type Elimination
J. Symb. Comput., 17
K. Mahler (1968)
An unsolved problem on the powers of 3/2
Journal of the Australian Mathematical Society, 8
Friedrich Neurauter, A. Middeldorp (2011)
Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
N. Eén, Niklas Sörensson (2003)
An Extensible SAT-solver
JC Lagarias (1985)
The 3x+1\documentclass[12pt]{minimal}
The American Mathematical Monthly, 92
Roupam Ghosh (2008)
On the Collatz Problem
arXiv: General Mathematics
P. Erdös (1979)
Some Unconventional Problems in Number Theory
Acta Mathematica Hungarica, 33
K Mahler (1968)
An unsolved problem on the powers of 3/2\documentclass[12pt]{minimal}
Journal of the Australian Mathematical Society, 8
David Sabel, H. Zantema (2016)
Termination of Cycle Rewriting by Transformation and Matrix Interpretation
Log. Methods Comput. Sci., 13
Pierre Courtieu, G. Gbedo, O. Pons (2009)
Improved Matrix Interpretation
G. Alexits (2004)
Some unconventional problems in number theory
J. Petke, P. Jeavons (2011)
The Order Encoding: From Tractable CSP to Tractable SAT
J. Lagarias (2003)
The 3x+1 problem: An annotated bibliography (1963--1999)
S. Kurtz, Janos Simon (2007)
The Undecidability of the Generalized Collatz Problem
J. Kari (2012)
Cellular Automata, the Collatz Conjecture and Powers of 3/2
J. Endrullis, R. Vrijer, Johannes Waldmann (2010)
Local Termination: theory and practice
Log. Methods Comput. Sci., 6
R 2 = { a → aa } is not terminating, since even a single occurrence of a allows indeﬁnitely producing more of the symbol a
C. Gomes, B. Selman, N. Crato, Henry Kautz (2000)
Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems
Journal of Automated Reasoning, 24
T. Tao (2019)
Almost all orbits of the Collatz map attain almost bounded values
Forum of Mathematics, Pi, 10
(1972)
Unpredictable iterations
Matti Soittola (1976)
Positive Rational Sequences
Theor. Comput. Sci., 2
Armin Biere (2019)
CADICAL at the SAT Race 2019
(iii) (cid:46)N (cid:47)
David Barina (2020)
Convergence verification of the Collatz problem
The Journal of Supercomputing
Martin Davis, G. Logemann, D. Loveland (2011)
A machine program for theorem-proving
Commun. ACM, 5
J. Lagarias (2006)
The 3x+1 Problem: An Annotated Bibliography, II (2000-2009)
arXiv: Number Theory
Joao Marques-Silva, K. Sakallah (1999)
GRASP: A Search Algorithm for Propositional Satisfiability
IEEE Trans. Computers, 48
SN( C Even / 4 \ { tf (cid:46) → t (cid:46) } ) if and only if all nonconvergent C -trajectories contain some n ≡ 2 (mod 4)
S. Kohl (2007)
Wildness of iteration of certain residue-class-wise affine mappings
Adv. Appl. Math., 39
G. Scollo (2004)
ω-rewriting the Collatz Problem
Fundamenta Informaticae, 64
Pascal Michel (2013)
Problems in number theory from busy beaver competition
Log. Methods Comput. Sci., 11
(2009)
Lecture Notes in Computer Science
BibliographyJ. LagariasAT, T. Park
3x + 1 Problem Annotated Bibliography
L. Kauffman (1995)
ARITHMETIC IN THE FORM
Cybernetics and Systems, 26
J. Berstel, C. Reutenauer (2010)
Noncommutative Rational Series with Applications
Knot Pipatsrisawat, Adnan Darwiche (2007)
A Lightweight Component Caching Scheme for Satisfiability Solvers
Johannes Waldmann (2004)
Matchbox: A Tool for Match-Bounded String Rewriting
M. Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, S. Malik (2001)
Cha : Engineering an e cient SAT solver
S. Wagon (1985)
The evidence
The Mathematical Intelligencer, 7
Matthew Denend (2018)
Challenging variants of the Collatz Conjecture
H. Zantema (2005)
Termination of String Rewriting Proved Automatically
Journal of Automated Reasoning, 34
S Wagon (1985)
The Collatz problem
The Mathematical Intelligencer, 7
(2010)
TheUltimate Challenge: The 3x+1 Problem.AmericanMathematical Society, Providence
J. Lagarias (2011)
The Ultimate Challenge: The 3x+1 Problem
Martin Davis, H. Putnam (1960)
A Computing Procedure for Quantification Theory
J. ACM, 7
J. Giesl, René Thiemann, Peter Schneider-Kamp, S. Falke (2006)
Mechanizing and Improving Dependency Pairs
Journal of Automated Reasoning, 37
T. Rado (1962)
On non-computable functions
Bell System Technical Journal, 41
R. Buttsworth, K. Matthews (1990)
On some Markov matrices arising from the generalized Collatz mapping
Acta Arithmetica, 55
MW Burdette (2016)
The Ultimate Challenge
(2005)
Variants of the 3N + 1 conjecture and multiplicative semigroups
J. Lagarias (1985)
The 3x + 1 Problem and its Generalizations
American Mathematical Monthly, 92
C. Sternagel, René Thiemann (2014)
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
Emil Post (1943)
Formal Reductions of the General Combinatorial Decision Problem
American Journal of Mathematics, 65
Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations
D. Hofbauer, C. Lautemann (1989)
Termination Proofs and the Length of Derivations (Preliminary Version)

Publisher: Springer Journals
Copyright: Copyright © The Author(s) 2023
ISSN: 0168-7433
eISSN: 1573-0670
DOI: 10.1007/s10817-022-09658-8
Publisher site: See Article on Publisher Site

Abstract

We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary–ternary representations of positive integers. We prove that the termination of this rewriting system is equivalent to the Collatz conjecture. We also prove that a previously studied rewriting system that simulates the Collatz function using unary representations does not admit termination proofs via natural matrix interpretations, even when used in conjunction with dependency pairs. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses natural/arctic matrix interpretations and we ﬁnd automated proofs of nontrivial weakenings of the Collatz conjecture. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach. Keywords String rewriting · Termination · Matrix interpretations · SAT solving · Collatz conjecture · Computer-assisted mathematics Emre Yolcu eyolcu@cs.cmu.edu Scott Aaronson scott@scottaaronson.com Marijn J. H. Heule marijn@cmu.edu Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA Department of Computer Science, University of Texas at Austin, Austin, TX, USA 0123456789().: V,-vol 123 15 Page 2 of 44 E. Yolcu et al. × × × 2 1 1 × + × × + × 2 1 1 3 2 1 × × × × 2 3 3 2 × × + × × + 2 3 1 3 2 1 ×2 ×3 +2 ×3 +1 ×2 × + × × + × + 2 1 3 3 1 2 1 × + × + × + × 2 1 3 1 3 2 2 × + × + × + × + 2 1 3 2 3 2 2 1 × × + 1 3 1 2 1 × + × × 1 3 1 1 2 2 × + × × + 1 3 2 1 2 2 1 × + × × + × × + × 1 3 2 3 3 2 3 3 2 1 × × + × × + × × + × 1 2 2 1 3 3 2 3 3 2 1 × × + × + × + × × + × 1 2 3 1 2 1 3 2 3 3 2 1 1 ×2 ×3 +1 ×3 +2 ×2 +1 ×3 ×3 +2 ×1 × × + × + × + × + × + × 1 2 3 1 3 2 3 1 2 1 3 2 1 × × + × + × + × + × + × 1 2 3 1 3 2 3 1 3 2 2 1 1 × × + × + × + × + × + × 1 2 3 1 3 2 3 1 3 2 3 2 1 × × + × + × + × + × + × 1 3 2 1 3 2 3 1 3 2 3 2 1 × × + × + × + × + × + × 1 3 3 2 2 1 3 1 3 2 3 2 1 × × + × + × × + × + × 1 3 3 2 3 2 2 3 2 3 2 1 × × + × + × + × × + × 1 3 3 2 3 2 3 1 2 3 2 1 1 ×3 ×3 +2 ×3 +2 ×3 +1 ×3 +1 ×2 ×1 × × + × + × + × + × 1 3 3 2 3 2 3 1 3 1 1 Diagrammatic view of the Collatz trajectory of 27. Each row in the cascade is a mixed binary–ternary repre- sentation of an iterate, with each box corresponding to a digit. Rewrite rules are shown at the top right corner. The zoomed-in slice at the bottom left corner highlights the intermediate rewrite steps performed to change the least signiﬁcant digit into binary while preserving the numeric value of the representation. 123 Automated Approach to Collatz Conjecture Page 3 of 44 15 1 Introduction Let N ={0, 1, 2,... } denote the natural numbers and N ={1, 2, 3,... } denote the positive + + integers. We deﬁne the Collatz function C : N → N as n/2if n ≡ 0 (mod 2) C (n) = 3n +1if n ≡ 1 (mod 2). Given a function f and a number k ∈ N, the function f denotes the kth iterate of f ,deﬁned as f := f ◦ f ◦ ··· ◦ f . The well-known Collatz conjecture is the following: k times + k Conjecture 1.1 For all n ∈ N , there exists some k ∈ N such that C (n) = 1. This is a longstanding open problem and there is a vast literature dedicated to its study. For its history and comprehensive surveys on the problem, we refer the reader to Lagarias [1–3]. See also the work by Tao [4] for dramatic recent progress on the problem. Deﬁnition 1.2 (Convergent function) Consider a function f : X → X and a designated N 2 element z ∈ X.Given x ∈ X, the sequence of iterates f (x ) := (x , f (x ), f (x), ...) is called the f -trajectory of x. If the trajectory f (x ) reaches a cycle containing z, the trajectory is convergent to z for x.Iffor all x ∈ X the trajectory f (x ) is convergent to z, the function f is convergent to z. As of 2020, it has been checked by computation that for all n ≤ 2 the Collatz trajectory of n is convergent [5]. This fact, along with the heuristic argument that on average the iterates in a trajectory tend to decrease [6], is often used as evidence to support the belief that the conjecture is true. On a different note, Conway proved that a generalization of the problem is undecidable [7], which Kurtz and Simon later extended to a variant even closer to the Collatz conjecture [8]. While the prevailing opinion is that the Collatz conjecture holds, and the heuristic arguments suggest that an average trajectory is convergent, the undecidability results help explainwhy this seemstobesohardtoshow. In this paper, we describe an approach based on termination of string rewriting to auto- matically search for a proof of the Collatz conjecture. Although trying to prove the Collatz conjecture via automated deduction is clearly a moonshot goal, there are two recent techno- logical advances that provide reasons for optimism that at least some interesting variants of the problem might be solvable. First, the invention of the method of matrix interpretations [9, 10] and its variants such as arctic interpretations [11, 12] turns the quest of ﬁnding a ranking function to witness termination into a problem that is suitable for systematic search. Second, the progress in satisﬁability (SAT) solving makes it possible to solve many seemingly difﬁcult combinatorial problems efﬁciently in practice. Their combination, i.e., using SAT solvers to ﬁnd interpretations, has so far been an effective strategy in solving challenging termination problems. We make the following contributions: • We show how a generalized Collatz function can be expressed as a rewriting system that is terminating if and only if the function is convergent. For the functions we deﬁne throughout this paper, the designated element z is clear from the context, so we refer to convergence without explicitly mentioning z. It is also apparent in all cases that z is in a cycle, and we simply call a trajectory convergent if it contains z. See https://pcbarina.ﬁt.vutbr.cz for David Barina’s ongoing veriﬁcation effort. 123 15 Page 4 of 44 E. Yolcu et al. • We prove that no termination proof via natural matrix interpretations exists for a certain system by Zantema [13] that simulates the Collatz function using unary representations of numbers. This result holds even when natural matrix interpretations are used in con- junction with the dependency pair transformation [14]. • We show that translations into rewriting systems that use non-unary representations of numbers are more amenable to automated methods, compared with the previously and commonly studied unary representations. • We automatically prove various weakenings of the Collatz conjecture. We observe that, for some of these weakenings, the only matrix interpretations that our termination tool was able to ﬁnd involved relatively large matrices (of dimension 5). Existing termination tools often limit their default strategies to search for small interpretations as they are tailored for the setting where the task is to quickly solve a large quantity of relatively easy problems. We make the point that, given more resources, the method of matrix interpretations has the potential to scale. • We observe that the phase-saving heuristic used by default in modern SAT solvers can degrade the performance of CDCL (conﬂict-driven clause learning) solvers [15]onfor- mulas encoding the existence of matrix interpretations, whereas using negative branching can improve solver performance. In Appendix C, we present adaptations of our rewriting system that allow reformulating several more open problems in mathematics as termination problems of small size. This article is an extended version of our CADE 2021 paper [16]. In addition to several small improvements throughout the article, we expanded Section 2 with extra background material to make the article more self-contained and accessible for nonexperts in rewriting. We included additional examples throughout, provided more detailed proofs especially for the main contributions in Section 3.2, and discussed several remarks in more detail. We included the additional Section 3.1.1 where we prove the nonexistence of proofs via natu- ral matrix interpretations for the rewriting system that uses unary representations. We also included Section 4.6 where we discuss the SAT solving aspect of termination proving in detail and provide experimental comparisons of the effectiveness of various heuristics in ﬁnding interpretations. 2 Preliminaries 2.1 String Rewriting Systems We brieﬂy review the notions related to string rewriting that are used in the rest of the paper. We adopt the notation of Zantema [13] and Endrullis et al. [10]. For a comprehensive introduction to string or term rewriting, see Book and Otto [17] or Baader and Nipkow [18], respectively. Deﬁnition 2.1 (String rewriting system) Let be an alphabet, i.e., a set of symbols. A string ∗ ∗ rewriting system (SRS) over is a relation R ⊆ × .Elements (, r ) ∈ R are called rewrite rules and are usually written as → r. The system R induces a rewrite relation ∗ ∗ → := {(st , srt ) | s, t ∈ , → r ∈ R} on the set of strings. Deﬁnition 2.2 (Termination) A relation → on A is terminating if there is no inﬁnite sequence s , s ,... ∈ A such that s → s for all i ≥ 0. A terminating relation is also commonly 0 1 i i +1 called Noetherian, well-founded, or strongly normalizing. We write SN(→) to denote that → is terminating. 123 Automated Approach to Collatz Conjecture Page 5 of 44 15 We often conﬂate an SRS R with the rewrite relation it induces when discussing termi- nation. In particular, we write “R is terminating” instead of “→ is terminating”. We also often do not specify the alphabet and take it to be the set of all the symbols that appear in a given rewriting system. Example 2.3 1. R ={aa → a} is terminating, which is proved easily by observing that each rewrite decreases the length of a string by 1. 2. R ={a → aa} is not terminating, since even a single occurrence of a allows indeﬁnitely producing more of the symbol a. 3. R ={ab → ba} is terminating, since all rewrite sequences eventually convert a given ∗ ∗ string into the form b a and stop. An example sequence is shown below, with the under- lines indicating the substrings that the rules are applied to. abbab → babab → bbaab → bbaba → bbbaa R R R R 3 3 3 3 A useful generalization of termination is relative termination: Deﬁnition 2.4 (Relative termination) Let → , → be relations on A.Then → is said to be 1 2 1 terminating relative to → if there is no inﬁnite sequence s , s ,... ∈ A such that 2 0 1 • s → s for inﬁnitely many values of i, i 1 i +1 • s → s for all other values of i. i 2 i +1 We write SN(→ / → ) to denote that → is terminating relative to → . 1 2 1 2 Equivalently, R is said to be terminating relative to S if every sequence of rewrites for the system R ∪ S applies the rules from R at most ﬁnitely many times. Note that we have SN(R / ∅) = SN(R) by the deﬁnition, so relative termination is indeed a generalization. Example 2.5 Let R ={aa → aba} and S ={b → bb}. The system R ∪ S is not terminating since S gives way to inﬁnite rewrite sequences; however, R is terminating relative to S because R by itself is terminating and applying the rule b → bb does not facilitate further applications of the rule aa → aba. Relative termination allows proofs of termination to be broken into steps as codiﬁed by the following theorem. Theorem 2.6 (Rule removal [13, Theorem 1]) Let R be an SRS. If there exists a subset T ⊆ R such that SN(T / R) and SN(R \ T ),then SN(R). This theorem allows us to “remove rules” in the following way. When proving SN(R), if we succeed at ﬁnding a subset T satisfying SN(T / R), the proof obligation becomes weakened to SN(R \ T ), where the rules of T are no longer present. This removal of rules can be repeated until no rules remain, thus producing a stepwise proof of termination. Another useful technique is reversal: Deﬁnition 2.7 (Reversal) Let s = s ... s ∈ be a string and R be an SRS. Letting 1 n rev rev rev rev s := s ... s ,the reversal of R is deﬁned as R := { → r | → r ∈ R}. n 1 Lemma 2.8 (Rule reversal [13, Lemma 2]) Let R, Sbe SRSs. Then, SN(R / S) if and only if rev rev SN(R / S ). 123 15 Page 6 of 44 E. Yolcu et al. Reversal is of interest because methods for proving termination are not necessarily invari- ant under reversal, that is, a given technique may fail to show the termination of a system R rev while succeeding for its reversal R . Yet another important notion is top termination: Deﬁnition 2.9 (Top termination) Let R be an SRS over .The top rewrite relation induced by R is deﬁned as → := {(s, rs) | s ∈ , → r ∈ R}.If → is terminating, R is R R top top said to be top terminating. In plain language, top termination allows rewrites to be performed only at the leftmost end of a string, so it requires a condition less strict than that of termination. As we will see in the next section (Theorem 2.15), top termination problems can admit proofs of a more relaxed form compared with termination. Relative top termination, i.e., proving SN(R / S) for SRSs R and S, is a crucial compo- top nent in the dependency pair approach [14], which reduces a termination problem to a relative top termination problem that often ends up being easier to solve via automated methods com- pared with the original problem. In order to avoid requiring familiarity with the dependency pair approach, we omit its discussion and instead prove a self-contained result (Lemma 3.18) that encapsulates dependency pairs in a more elementary manner for the speciﬁc rewriting systems that we consider in this paper. 2.2 Interpretation Method Let R be an SRS over the alphabet . The main idea when proving termination is to show ∗ ∗ that there exists a well-founded (strict) order > on such that, for all strings s, t ∈ , if s → t then s > t. When this is the case, R is terminating since any rewrite causes a “strict decrease” with respect to > and by its well-foundedness there cannot exist an inﬁnitely decreasing sequence. The condition over inﬁnitely many strings can be replaced by another one that involves only the rules of R by employing a reduction order [18, Section 5.2]; [17, Section 2.2]. Deﬁnition 2.10 (Reduction order) Let > be a well-founded order on .Iffor all s, t , p, q ∈ , s > t implies psq > ptq,then > is called a reduction order. Theorem 2.11 ([18, Theorem 5.2.3]; [17, Theorem 2.2.4]) Let R be an SRS over the alphabet . The system R is terminating if and only if there exists a reduction order > on such that > r holds for all → r ∈ R. The interpretation method is a particular way of deﬁning a reduction order. Instead of considering the strings directly, we interpret each symbol σ ∈ as a function [σ ]: A → A, where A is some carrier set, for example of natural numbers or vectors, and we extend this interpretation from symbols to strings s = s ... s ∈ as [s]:=[s ] ◦ ··· ◦ [s ]. When the 1 n 1 n domain A is already equipped with a well-founded order >, we can deﬁne a well-founded order > on by s > t if and only if [s](x)> [t ](x ) for all x ∈ A, (1) where A = (A, [·] ,>) is a structure with [·] := {[σ]| σ ∈ } denoting the collection of interpretations. For appropriately chosen interpretations, > ends up being a reduction order: 123 Automated Approach to Collatz Conjecture Page 7 of 44 15 Theorem 2.12 ([18, Theorem 5.3.3]) Let be an alphabet and let > be a well-founded order on A. If for all symbols σ ∈ the interpretation [σ ]: A → A is monotone with respect to >,then > as deﬁned in (1) is a reduction order on . Thus, after ﬁxing (A,>), proving termination reduces to ﬁnding suitable (monotone) interpretations of the symbols as functions [for details see 18, Section 5.3]. As a concrete example, here is a simple proof of termination via the interpretation method. Example 2.13 Recall R ={ab → ba} from Example 2.3 with ={a, b}.Fix (N ,>) with the usual order on positive integers, which is well-founded by the well-ordering principle. 2 + Let [a](x ) = x and [b](x ) = x + 1. Denote N = (N , {[a], [b]},>). Both functions are ∗ ∗ monotone with respect to >, so by Theorem 2.12 the relation > ={(s, t ) ∈ × | [s](x)> [t ](x ) for all x ∈ N } is a reduction order. For the rule ab → ba,since 2 2 ([a]◦[b])(x ) = (x + 1) > x + 1 = ([b]◦[a])(x ) holds for all x ∈ N ,wehave ab > ba. Thus, by Theorem 2.11 the SRS R is terminating. N 3 In order to use the interpretation method for relative termination (resp. top termination), the above ideas can be generalized in the form of extended (resp. weakly) monotone algebras [10]. Deﬁnition 2.14 (Extended/weakly monotone algebra) Let • be an alphabet, • A aset, •[σ ]: A → A an interpretation for every σ ∈ , • > and order relations over A such that > is well-founded and satisﬁes > · ⊆ >. Letting [·] ={[σ]| σ ∈ }, the structure (A, [·] ,>, ) is a weakly monotone -algebra if for every σ ∈ the interpretation [σ ] is monotone with respect to .Itisan extended monotone -algebra if, additionally, for every σ ∈ the interpretation [σ ] is monotone with respect to >. Relative termination (resp. top termination) is characterized as the existence of extended (resp. weakly) monotone algebras. Theorem 2.15 ([10, Theorem 2]) Let R and S be SRSs over the alphabet .Wehave SN(R/S) (resp. SN(R / S)) if and only if there exists an extended (resp. weakly) monotone -algebra top (A, [·] ,>, ) such that • for each rule → r ∈ R we have [](x)> [r ](x ) for all x ∈ A, • for each rule → r ∈ S we have [](x ) [r ](x ) for all x ∈ A. An effective way to automatically prove relative termination (or top termination) is to try to satisfy the conditions of the above theorem by ﬁxing (A,>, ) and algorithmically searching for appropriate interpretations of the symbols. Matrix interpretations is a speciﬁc instance of this generic method. In the following section we describe (at a high level) the method of matrix interpretations. For more details and background, we refer the reader to existing work [9–12]. It may seem an odd choice to focus on matrix interpretations and implement our own prover given that there is a wealth of other techniques for proving termination that are Termination is in fact equivalent to the existence of such interpretations [19, Proposition 1]. 123 15 Page 8 of 44 E. Yolcu et al. already implemented in the existing tools (e.g., AProVE [20], Matchbox [21], T T [22]). We T 2 did experiment with other methods; however, at least for the rewriting systems of the speciﬁc form in this paper it appears that the method of matrix interpretations is the most effective. For instance, one of the most difﬁcult instances in this paper (in the sense of the smallest proof of termination that we could ﬁnd) appears to require arctic matrix interpretations in all the proofs that we (and the authors of AProVE and Matchbox) could ﬁnd. (There remain some versions of matrix interpretations that we have not yet experimented with [23, 24].) Additionally, we chose to implement our own minimal prover to have ﬁner control over the SAT solving aspect of the search for an interpretation. We give a summary of our ﬁndings regarding this topic in Section 4.6. 2.3 Natural/Arctic Matrix Interpretations 2.3.1 Natural Numbers Let R be an SRS over the alphabet .Fix adimension d ∈ N . In the method of natural d d matrix interpretations [10]weset A = N and deﬁne, for vectors x, y ∈ N , x > y ⇐⇒ x > y ∧ x ≥ y for all i ∈{2,..., d}, 1 1 i i x y ⇐⇒ x ≥ y for all i ∈{1,..., d}. i i d d For interpreting each symbol σ ∈ , we consider an afﬁne function [σ ]: N → N : [σ ](x) = M x + v σ σ In this way, the structure (N , [·] ,>, ) satisﬁes the requirements of Deﬁnition 2.14 for a weakly monotone algebra. Additionally setting (M ) = 1 satisﬁes the requirements for σ 1,1 an extended monotone algebra. Furthermore, since the composition of afﬁne functions is afﬁne, for all s ∈ there d×d d exist M ∈ N , v ∈ N such that [s](x) = M x + v . As a result, given a collection s s s s [·] of natural matrix interpretations, the conditions of Theorem 2.15 can be checked by computing for each rule → r ∈ R the corresponding matrices M , M and vectors v , v r r d×d and comparing them elementwise [10,Lemma 4].Extend to matrices M, N ∈ N as M N ⇐⇒ M ≥ N for all i , j ∈{1,..., d}. i , j i , j Then, we have M M ∧ v > v ⇐⇒ [](x)> [r ](x) for all x ∈ N , r r M M ∧ v v ⇐⇒ [](x) [r ](x) for all x ∈ N . (2) r r This shows that it is decidable to check whether a given collection of interpretations of the form considered here constitutes a proof of termination. Example 2.16 Recall R ={aa → aba} and S ={b → bb} from Example 2.5 with ={a, b}. The following functions constitute a matrix interpretations proof that shows SN(R / S). 11 0 10 0 [a](x) = x + [b](x) = x + 00 1 00 0 123 Automated Approach to Collatz Conjecture Page 9 of 44 15 It is easy to check that the above interpretations give an extended monotone algebra and that they satisfy the below relations for all x ∈ N , which implies SN(R / S) via Theorem 2.15. 11 1 11 0 [aa](x) = x + > x + =[aba](x) 00 1 00 1 10 0 10 0 [b](x) = x + x + =[bb](x) 00 0 00 0 In order to automate the search for matrix interpretations given a rewriting system R, an approach that turns out to be effective is to encode all of the aforementioned constraints as a propositional formula in conjunctive normal form and use a SAT solver to look for a satisfying assignment. This additionally involves ﬁxing a ﬁnite domain for the coefﬁcients that can occur in the interpretations and encoding arithmetic over the chosen ﬁnite domain using propositional variables. (We discuss our choice of encoding in Section 4.6.) 2.3.2 Arctic Integers Natural matrix interpretations can also be adapted to the max–plus algebra of arctic natural numbers A = N∪{−∞} or arctic integers A = Z∪{−∞} as coefﬁcients. This adaptation N Z enables termination proofs in some cases where either there is no other automated method that leads to a proof or only relatively complicated proofs are known [11]. Let R be an SRS over the alphabet ,and let A be either one of A or A . In the method of N Z arctic matrix interpretations [11, 12] we use the arctic semiring (A, ⊕, ⊗), with the following operations: x ⊕ y = max{x , y} x ⊗ y = x + y Let > and ≥ denote the usual order relations over integers. Adopting the conventions that Z Z x > −∞ for all x ∈ Z and that −∞ ≥ −∞,wedeﬁne,for x , y ∈ A, Z Z x y ⇐⇒ x > y ∨ x = y =−∞, x ≥ y ⇐⇒ x ≥ y. We ﬁx a dimension d ∈ N and we extend both and ≥ to arctic vectors and arctic matrices elementwise. As these deﬁnitions allow −∞ −∞, the order is not well-founded. To d−1 ensure well-foundedness of we restrict the domain to N × A . Then, for interpreting d d each symbol σ ∈ , we consider an afﬁne function [σ ]: A → A , written as [σ ](x) = M ⊗ x ⊕ v , σ σ d−1 where we require (M ) ≥ 0or (v ) ≥ 0 to ensure that [σ ](z) ∈ N × A for z ∈ σ 1,1 σ 1 d−1 d−1 N × A . In this way, the structure (N × A , [·] , , ≥) satisﬁes the requirements of Deﬁnition 2.14 for a weakly monotone algebra. Additionally choosing A = A and setting each v to be the −∞ vector (consequently enforcing (M ) ≥ 0) satisﬁes the σ σ 1,1 requirements for an extended monotone algebra. This means that arctic integers (as opposed to arctic natural numbers) and vectors that contain ﬁnite elements (i.e., not all −∞)are used only when proving top termination. The name “arctic” was chosen to contrast with the min–plus algebra of the “tropical” semiring. 123 15 Page 10 of 44 E. Yolcu et al. As the composition of afﬁne functions over arctic vectors is afﬁne, given a collection [·] of arctic matrix interpretations we can compute for each rule → r ∈ R the corresponding arctic matrices M , M and arctic vectors v , v . Elementwise comparisons of these matrices r r and vectors give sufﬁcient conditions for the inequalities in Theorem 2.15. In particular, due to Koprowski and Waldmann [11,Lemma 6.5],wehave M M ∧ v v ⇒ [](x) [r ](x) for all x ∈ A , r r M ≥ M ∧ v ≥ v ⇒ [](x) ≥[r ](x) for all x ∈ A . r r Thus, the search for arctic matrix interpretations can be automated in a manner similar to natural matrix interpretations by encoding the aforementioned constraints as a SAT instance. Example 2.17 Let P denote the following SRS . b → ax aax → bxa ab → ba xb → ax a → ax As an example of the different capabilities of arctic versus natural matrix interpretations, consider trying to prove the relative termination statement SN({b → ax} / P). To our knowledge, there is no direct proof of this statement via natural matrix interpretations although there is one via the 4-dimensional arctic matrix interpretations below. In the inter- pretations, − indicates −∞, and the multiplication operator ⊗ as well as the vectors of all −∞s are omitted. ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 11 − 0 11 − 0 −− 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [a](x) = x [b](x) = x [x](x) = x ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ − 0 −− 10 1 − −−− 0 −− 0 − −− 0 − − 0 −− ⎡ ⎤ ⎡ ⎤ 0 − 0 − 0 −−− ⎢ ⎥ ⎢ ⎥ −−−− −−−− ⎢ ⎥ ⎢ ⎥ [](x) = x [](x) = x ⎣ ⎦ ⎣ ⎦ −−−− −−−− −−−− −−−− With the above interpretations, the rules of P satisfy the following relations, which, by Theorem 2.15, proves that {b → ax} is terminating relative to P. ⎡ ⎤ ⎡ ⎤ 10 1 − 0 − 0 − ⎢ ⎥ ⎢ ⎥ −−−− −−−− ⎢ ⎥ ⎢ ⎥ [b](x) = x x =[ax](x) ⎣ ⎦ ⎣ ⎦ −−−− −−−− −−−− −−−− ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 21 20 11 − 0 ⎢ ⎥ ⎢ ⎥ [aax](x) = x ≥ x =[bxa](x) ⎣ ⎦ ⎣ ⎦ 10 1 − 10 1 − −− 0 − −− 0 − This SRS simulates the Abelian sandpile model [25] over an inﬁnite path. The symbols , x, represent the vertices on the path. At each instant, the weight of a vertex is identiﬁed by the number of asand bs to its left until the next occurrence of a vertex symbol. 123 Automated Approach to Collatz Conjecture Page 11 of 44 15 ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 2201 2201 ⎢ ⎥ ⎢ ⎥ [ab](x) = x ≥ x =[ba](x) ⎣ ⎦ ⎣ ⎦ 11 − 0 11 − 0 10 1 − − 0 −− ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 10 1 − 10 1 − ⎢ ⎥ ⎢ ⎥ [xb](x) = x ≥ x =[ax](x) ⎣ ⎦ ⎣ ⎦ −− 0 − −− 0 − 11 − 0 −−− 0 ⎡ ⎤ ⎡ ⎤ 0 −−− 0 −−− ⎢ ⎥ ⎢ ⎥ 1 −−− 1 −−− ⎢ ⎥ ⎢ ⎥ [a](x) = x ≥ x =[ax](x) ⎣ ⎦ ⎣ ⎦ −−−− −−−− −−−− −−−− 2.4 Generalized Collatz Functions We consider instances of the following generalization of the Collatz function. Its variants have commonly appeared in the literature [6, 26–31]. Deﬁnition 2.18 (Generalized Collatz function) Let X be one of N, N ,or Z and deﬁne X := X ∪{⊥}. A function f : X → X is a generalized Collatz function if f (⊥) =⊥ ⊥ ⊥ ⊥ andthere existaninteger d ≥ 2 and rational numbers q ,..., q , r ,..., r such that 0 d−1 0 d−1 for all 0 ≤ i ≤ d − 1and all n ∈ X, we have a deﬁnition either of the form f (n) = q n + r if n ≡ i (mod d), i i or of the form f (n) =⊥ if n ≡ i (mod d). In the above deﬁnition, we allow the representation of a partially deﬁned function by mapping to ⊥ in the undeﬁned cases. We call a partial f convergent if all f -trajectories contain ⊥. Note that the Collatz function corresponds to the case d = 2, q = 1/2, r = 0, q = 3, 0 0 1 r = 1. Although the Collatz function is by far the most widely studied case, there are several other concrete examples of generalized Collatz functions the convergence of which is worth studying due to their connections to open problems in number theory and computability theory. We discuss these cases in Appendix C. 3 Rewriting the Collatz Function We start our discussion with systems that use unary representations and then demonstrate via examples that mixed-base representations can be more suitable for use with automated methods. 3.1 Rewriting in Unary The following system of Zantema [13] simulates the iterated application of the Collatz func- tion to a number represented in unary, and it terminates upon reaching 1. 123 15 Page 12 of 44 E. Yolcu et al. Example 3.1 Z denotes the following SRS, consisting of 5 symbols and 7 rules. h11 → 1h 11h → 11s h1 → t11 1s → s1 1t → t111 s → h t → h This system can be seen as encoding the execution of a Turing machine with cells that can be contracted/expanded. The symbols 1 and (blank) form the tape alphabet, while the symbols h (half), s (shift), t (triple) indicate the head along with the state of the machine. Through the following result, the Collatz conjecture can be reformulated as termination of string rewriting. Theorem 3.2 ([13, Theorem 16]) Z is terminating if and only if the Collatz conjecture holds. 2n ∗ n While the forward direction of the above theorem is easy to see (since h1 → h1 2n+1 ∗ 3n+2 for n > 1and h1 → h1 for n ≥ 0), the backward direction is far from obvious because not every string corresponds to a valid conﬁguration of the underlying machine. As another example, consider the system below, which follows a theme similar to Example 3.1. Example 3.3 W denotes the following SRS, consisting of 4 symbols and 4 rules. h11 → 1h 1h → 1t 1t → t111 t → h Johannes Waldmann shared the above system (originally due to Zantema ) with us, men- tioning that its termination has yet to be proved via automated methods. Nevertheless, there is a simple reason for its termination: It simulates the iterated application of a partial generalized + + Collatz function W : N → N deﬁned as follows, which is easily seen to be convergent. ⊥ ⊥ 3n/2if n ≡ 0 (mod 2) W (n) = ⊥ if n ≡ 1 (mod 2) 3.1.1 Nonexistence of Proofs via Natural Matrix Interpretations Natural matrix interpretations cannot be used to directly remove any of the rules from the above kind of unary rewriting systems that simulate certain maps, in particular the Collatz function. Deﬁnition 3.4 (N-rational sequence) A sequence x , x ,... ∈ N is called N-rational if there 1 2 d×d d exists a matrix M ∈ N and vectors v, w ∈ N of some dimension d such that, for all n, T n we have x = v M w. The following is a consequence of Berstel’s theorem [32, Theorem 8.1.1]. (See also the remark by Soittola [33, page 318].) Theorem 3.5 Let x , x ,... be an N-rational sequence. Then there exist m, p ∈ N such 1 2 that, for all j ∈{0, 1,..., p − 1}, each of the subsequences {x } has its nth m+kp+ j k=0 https://www.lri.fr/~marche/tpdb/tpdb-2.0/SRS/Zantema/z079.srs 123 Automated Approach to Collatz Conjecture Page 13 of 44 15 element equal to (1 + o(1))P(n)α for some nonzero polynomial P and a constant α> 0. In particular, each of these subsequences is monotonically nondecreasing after some ﬁnite point. Corollary 3.6 There exists no N-rational sequence x , x ,... satisfying x > x for 1 2 8n+1 9n+2 all n. Proof Let p be as in Theorem 3.5, and consider n of the form qp − 1 for some large enough q.Then (9n +2)−8n +1 = n +1 = qp,so x and x belong to the same subsequence. 8n+1 9n+2 This means that for all sufﬁciently large n of this form, we must have x ≤ x . 8n+1 9n+2 To make use of the above facts in ruling out the existence of natural matrix interpretations of the form described in Section 2.3.1, we also need the following result proving that we can work with interpretations that are purely linear (instead of afﬁne) by moving up to a higher dimension. Theorem 3.7 ([10, Theorem 6]) Let R be an SRS over the alphabet , and let [σ ](x) = M x + v denote a d-dimensional afﬁne interpretation for each σ ∈ . Deﬁne a (d + 1)- σ σ dimensional linear interpretation for each σ ∈ as M v + σ σ [σ ] (x) := D x = x, σ T 0 1 where 0 denotes the d-dimensional zero vector. For each rule → r ∈ R, let M , M , v , v , r r D , D denote the matrices and the vectors occurring in the corresponding interpretations (as obtained by composing the interpretations of the symbols). If we have M M and v v ,then D D . Additionally, if v > v ,then (D ) >(D ) . r r r 1,d+1 r 1,d+1 In informal terms, the above theorem states that if we have a collection of afﬁne interpre- tations to remove a rule from a system (due to the strict decrease across the ﬁrst elements of the corresponding two vectors), then there is also a collection of purely linear interpretations such that the top-right elements decrease strictly across the two matrices corresponding to this rule. With this fact at hand, we can prove the following. Theorem 3.8 Let ={1, , h, s, t}. There exists no collection [·] of natural matrix interpretations of any dimension d satisfying the requirements for an extended monotone -algebra such that • for at least one rule → r ∈ Z we have [](x)> [r ](x) for all x ∈ N , and • for the remaining → r ∈ Z we have [ ](x) [r ](x) for all x ∈ N . Proof Assume for a contradiction that such a collection of natural matrix interpretations exists for some dimension d − 1, with each symbol σ ∈ interpreted as [σ ](x) = M x + v and σ σ each matrix D deﬁned as in Theorem 3.7.Let → r ∈ Z be a rule for which [](x)> [r ](x) d−1 for all x ∈ N , and denote ρ ={ → r }. As the interpretations satisfy the requirements for ∗ d−1 extended monotonicity, for all s, t ∈ ,if s → t,then [s](x)> [t ](x) for all x ∈ N . This conclusion implies by (2)that M M and v > v , which, by Theorem 3.7,further s t s t imply D D and (D ) >(D ) . Thus, for all s, t ∈ , s t s 1,d t 1,d s → t ⇒ D D and (D ) >(D ) . (3) ρ s t s 1,d t 1,d We thank Gjergji Zaimi for this argument (see https://mathoverﬂow.net/a/270372). 123 15 Page 14 of 44 E. Yolcu et al. In Zantema’s system Z, we can represent an arbitrary integer k by the string h1 , interpreted as k k h1 (x) = D D D x. Let e ∈ N denote the ith standard basis vector, i.e., with 1 at the ith position and 0s elsewhere. Deﬁne T k f (k) := e h1 (e ) T k = e (D D D )e h d 1 1 (4) T k = (e D )D (D e ) h d 1 1 T k = v D w, where v = D e and w = D e are ﬁxed, so f (1), f (2), ... is an N-rational sequence. 1 d Now, since the system Z simulates the Collatz function (with the odd case incorporating an additional division by 2), for all numbers of the form 8n + 1 it can simulate the sequence of mappings 8n + 1 → 12n + 2 → 6n + 1 → 9n + 2 that results from applying the Collatz map three times. Thus, for all n,wehave 8n+1 ∗ 9n+2 h1 → h1 , which crucially requires the use of every single rule in Z (as it involves applying both m → m/2and m → (3m + 1)/2). This implies in particular that the rule → r is used in the above derivation. Recall also that the interpretations of all rules in Z are at least 8n+1 nonstrictly decreasing by assumption. This means along with (3) that, letting s = h1 9n+2 and t = h1 ,wehave (D ) >(D ) . From the deﬁnition of f ,for all n, s 1,d t 1,d T T f (8n + 1) = e D e = (D ) >(D ) = e D e = f (9n + 2), s d s 1,d t 1,d t d 1 1 butwealreadyarguedinCorollary 3.6 that no N-rational sequence can satisfy this inequality for all n, contradiction. Natural matrix interpretations fail to be useful for the unary rewriting systems even when used in conjunction with dependency pairs. For the reader familiar with dependency pairs, we show how to adapt the above proof to go through in the setting where the dependency pair transformation is applied before searching for natural matrix interpretations. Recall that, for an SRS R over , letting DP(R) denote the SRS consisting of all dependency pairs of R as deﬁned by Arts and Giesl [14, Deﬁnition 3], we have SN(R) if and only if SN(DP(R) / R) [14, Theorem 6]. For a deﬁned symbol s ∈ ,wewrite s to denote the top # corresponding tuple symbol. Let I ={ s → h, t → h}, and note that I ⊆ DP(Z). With an automated # # # # termination prover, the following is straightforward to establish for Zantema’s system Z after applying the dependency pair transformation and performing several steps of rule removal (e.g., using natural matrix interpretations). Lemma 3.9 SN(DP(Z) / Z) if and only if SN(I / Z). top top We prove below that neither rule in I can be removed using natural matrix interpretations. The proof is similar to that of Theorem 3.8, so we keep it relatively brief. Theorem 3.10 Let ={1, , , h, s, t}. There exists no collection [·] of natural matrix interpretations of any dimension d satisfying the requirements for a weakly monotone - algebra such that 123 Automated Approach to Collatz Conjecture Page 15 of 44 15 • for at least one rule → r ∈ I we have [](x)> [r ](x) for all x ∈ N , and • for every rule → r ∈ Z we have [ ](x) [r ](x) for all x ∈ N . Proof Assume for a contradiction that such a collection of natural matrix interpretations exists for some dimension d − 1, with each symbol σ ∈ interpreted as [σ ](x) = M x + v and σ σ each matrix D deﬁned as in Theorem 3.7.Let → r ∈ I bearulefor which [](x)> [r ](x) d−1 for all x ∈ N , and denote ρ ={ → r }. As the interpretations satisfy the requirements for ∗ d−1 only weak monotonicity, for all s, t ∈ ,if s → t,then [s](x)> [t ](x) for all x ∈ N . top Thus, for all s, t ∈ , s → t ⇒ D D and (D ) >(D ) . (5) ρ s t s 1,d t 1,d top We represent an arbitrary integer k by the string h1 , interpreted as k k h1 (x) = D D D x. # h # 1 Similar to (4), we let e ∈ N denote the ith standard basis vector and deﬁne g(k) := T k T u D w,where u = D e and w = D e are ﬁxed, so g(1), g(2), ... is an N-rational 1 d 1 h sequence. For all n,wehave 8n+1 ∗ 9n+2 h1 → h1 , # # I∪Z which crucially requires the use of both rules in I, and, moreover, these rules are applied only at the leftmost end of a string. In particular, the rule → r is used in the above derivation to perform a top rewrite. Thus, by (5), for all n,wehave g(8n + 1)> g(9n + 2),which contradicts Corollary 3.6. rev 8 Analogues of Theorems 3.8 and 3.10 also hold for the system Z , with its rules reversed. Moreover, by arguments similar to above, we can show that natural matrix interpretations fail to prove the termination of W. It is natural to expect that if a proof of the Collatz conjecture is to be produced by some automated method that relies on rewriting, then that method better be able to prove a statement as simple as the convergence of W . With this in mind, we describe an alternative rewriting system that simulates the Collatz function and terminates upon reaching 1. We then provide examples where the alternative system is more suitable for use with termination tools (for instance allowing a matrix interpretations proof of the convergence of W ). The arguments in this section that prove Theorems 3.8 and 3.10 also appear not to apply to the alternative system, because the connection between rewrite sequences and N-rational sequences gets lost when not using unary representations. More speciﬁcally, the proofs crucially use the fact that, since the system Z represents numbers in unary, it is possible to form a sequence such that the nth element is represented by some T n product v M w,where v and w are vectors and M is a matrix. There is no single such matrix that one can extract when using mixed binary–ternary, or even just binary, representations. Thus, the same kind of analysis, which uses the results known about N-rational sequences, does not go through for the alternative system. 3.2 Rewriting in Mixed Base In the mixed-base scheme, the overall idea is as follows. Given a number n ∈ N ,wewrite a mixed binary–ternary representation for it (noting that this representation is not unique). With 8 rev Speciﬁcally, Theorem 3.10 holds for Z with J ={ h11 → s11, 1h → 11t} in place of I. # # # # The corresponding version of Lemma 3.9 is again straightforward to establish using an automated termination prover. 123 15 Page 16 of 44 E. Yolcu et al. this representation, as long as the least signiﬁcant digit is binary, the parity of the number can be recognized by checking only this digit, as opposed to scanning the entire string when working in unary. This allows us to easily determine the correct case when applying the Collatz function. If the least signiﬁcant digit is ternary, then the representation is rewritten (while preserving its value) to make this digit binary. Afterwards, since computing n/2 corresponds to erasing a trailing binary 0 and computing 3n + 1 corresponds to inserting a trailing ternary 1, applying the Collatz function takes a single rewrite step. Intuitively, the rewriting system we present can be seen as applying the Collatz map to natural numbers written in binary, with some secondary computation performed using auxiliary symbols to facilitate the application of the map n → 3n + 1. However, since termination of rewriting is concerned with sequences that arise from any initial string and any possible application of the rules, we need to consider the behavior of the system over any string that may be encountered, which includes even the strings that could not result from computing in binary with a prescribed strategy for rule application. The mixed-base scheme is simply a way to give an arithmetical meaning to all strings and all possible rewrite steps. More formally, a mixed-base numeral system [34] is a numeral system where the base changes across positions, which we deﬁne as follows. Deﬁnition 3.11 (Mixed-base representation) Fix B ⊆ N to be a set of bases. Let n ,..., n ∈ 1 k N and let b ,..., b ∈ B. If we have for each 2 ≤ i ≤ k that n < b , then the matrix 1 k i i n n ... n 1 2 k N = b b ... b 1 2 k is called a mixed B-ary representation. To reduce clutter, we identify the matrix N with a string (n ) (n ) ...(n ) , where each (n ) is viewed as a single symbol denoting 1 (b ) 2 (b ) k (b ) i (b ) 1 2 k i the b -ary digit n . i i The string N in the above deﬁnition represents the number k k Val(N ) := n b . (6) i j i =1 j =i +1 Observing that the addition of leading zeros (symbols 0 for any b) to a string does not change its value, we may assume without loss of generality that n > 0. Furthermore, b does not 1 1 affect the value of the string, so we replace it by zero (noting that by Deﬁnition 3.11 no other base is zero). Example 3.12 1. With B ={2}, we have the binary numeral system. In the notation of Deﬁnition 3.11 we write 1 0 1 1 to represent the number 11. 2 2 2 2 2. With B ={2, 3}, we obtain the mixed binary–ternary system that we will use in the rest of this paper. In this system we may write, for instance, 1 2 1 or 2 1 1 or 1 1 2 to 0 3 2 0 2 2 0 2 3 represent the number 11. Now, deﬁne β (x ) := bx + n. After rearranging (6), we see that for a mixed B-ary string N = (n ) (n ) ...(n ) , its value Val(N ) is also given by evaluating the composite 1 (b ) 2 (b ) k (b ) 1 2 k function n n n k k−1 (x ) := (β ◦ β ◦ ··· ◦ β )(x ) (7) b b b k k−1 1 at any value (because b = 0 implies that the innermost function β (x ) = n is constant). 1 1 This gives us a string and a function view of the same representation, and we will switch 123 Automated Approach to Collatz Conjecture Page 17 of 44 15 between them as appropriate. In doing so, we also conﬂate the symbols and the corresponding functions, referring to β as n . As the last ingredient before describing the rewriting system, we observe that we can n n m m write (β ◦ β )(x ) = bcx + bm + n equivalently as another composition (β ◦ β )(x ) = b c c b cbx + cn + m for some suitable 0 ≤ n < b and 0 ≤ m < c. This allows us to swap the bases of adjacent positions while preserving the value of the string. From this point on, we constrain ourselves to the mixed {2, 3}-ary (binary–ternary) repre- sentations as we shift our focus to simulating the Collatz function (noting that it is possible to adapt the resulting rewriting system for other instances of the general case). More pre- cisely, we simulate the following redeﬁnition of the Collatz function, where the odd case incorporates an additional division by 2. if n ≡ 0 (mod 2) T (n) = 3n+1 if n ≡ 1 (mod 2) We will describe an SRS T over the symbols {f, t, 0, 1, 2, , } that simulates the iterated application of the Collatz function and terminates upon reaching 1. The symbols f, t cor- respond to binary digits 0 , 1 ;and 0, 1, 2 to ternary digits 0 , 1 , 2 . The symbol marks 2 2 3 3 3 the beginning of a string while also standing for the most signiﬁcant digit (without loss of generality assumed to be 1 )and marks the end of a string while also standing for the redundant trailing digit 0 . Consider the functional view of these symbols: 0(x ) = 3x f(x ) = 2x (x ) = 1 1(x ) = 3x + 1 (8) t(x ) = 2x + 1 (x ) = x 2(x ) = 3x + 2 Each positive integer can be expressed as some composition of these functions, which cor- responds to a string as per our previous discussion. Example 3.13 Viewing the expression (x ) as the constant 1, we can write 19 = Val(0f1) = (1(f(0((x ))))). The string representation ends with a ternary symbol, so we will rewrite it. With the function view, we have 1(f(x )) = 3(2x ) + 1 = 6x + 1 = 2(3x ) + 1 = t(0(x )). This shows that we could also write 19 = Val(00t), which now ends with the binary digit 1 . This gives us the rewrite rule f1 → 0t. We can now apply the Collatz function to this representation by rewriting only the rightmost two symbols of the string since 3(2x + 1) + 1 6x + 4 T ((t(x ))) = = = 3x + 2 = ((2(x ))). 2 2 This gives us the rewrite rule t → 2. After applying this rule to the string 00t,we indeed obtain T (19) = 29 = Val(002). In the manner of the above example, we compute all the necessary transformations and obtain the following 11-rule SRS T . ⎧ ⎫ ⎧ ⎫ f0 → 0f t0 → 1t 0 → t ⎨ ⎬ ⎨ ⎬ f → D = A = f1 → 0t t1 → 2f B = 1 → ff t → 2 ⎩ ⎭ ⎩ ⎭ f2 → 1f t2 → 2t 2 → ft 123 15 Page 18 of 44 E. Yolcu et al. This SRS is split into subsystems D (dynamic rules for T)and X = A ∪ B (auxiliary rules). The two rules in D encode the application of the Collatz function T , while the rules in X serve to push binary symbols towards the rightmost end of the string by swapping the bases of adjacent positions without changing the represented value. Example 3.14 (Rewrite sequence of T ) Consider the string s = ff0, which represents the number 12. Below is a possible rewrite sequence of T that starts from s, with the corre- sponding values (under the interpretations from (8)) displayed above the strings. Underlines indicate the parts of the strings where the rules are applied. 12 12 6 6 3 3 5 5 ff0 → f0f → f0 → 0f → 0 → t → 2 → ft A D A D B D B T T T 88 8 4 2 1 → f2 → 1f → fff → ff → f → D A B D D D T T T T The trajectory of T would continue upon reaching 1; however, in order to be able to formulate the Collatz conjecture as a termination problem, T is made in such a way that its rewrite sequences stop upon reaching the string representation of 1 since no rule is applicable. Termination of the subsystems of T with B or D removed is easily seen. However, since we have matrix interpretations at our disposal, let us give a compact and formal proof. Lemma 3.15 SN(T \ B) and SN(T \ D ). rev Proof It is easily checked that the interpretations below show SN((T \ B) ), which implies SN(T \ B) by Lemma 2.8. [f](x ) =[t](x ) = 2x + 1 []= x [0](x ) =[1](x ) =[2](x ) = 2x rev Similarly, the below interpretations show SN((T \ D ) ), which implies SN(T \ D ) T T by Lemma 2.8. [f](x ) =[t](x ) =[](x ) = x + 1 [0](x ) =[1](x ) =[2](x ) = 4x When considering the termination of T (on all initial strings), it sufﬁces to limit the discussion to initial strings of a speciﬁc form that we have been working with so far, e.g., in Examples 3.13 and 3.14. Lemma 3.16 If T is terminating on all initial strings of the canonical form (f|t|0|1|2) , then T is terminating (on all initial strings). For the proof of Lemma 3.16, we will use type introduction, which is a technique for proving termination by switching to typed rewriting. We refer the reader to Sabel and Zan- tema [35, Section 3.1] for background. We also offer a more elementary proof in Appendix A. Proof of Lemma 3.16 Let T ={ρ, σ, τ } be a set of types. It is straightforward to see that, with respect to the typing : σ → τ, f, t, 0, 1, 2 : σ → σ, : ρ → σ, 123 Automated Approach to Collatz Conjecture Page 19 of 44 15 the SRS T is well-typed, so it is terminating (in the untyped setting) if and only if it is terminating in the typed setting [35, Corollary 3.4]. Due to Lemma 3.15, a well-typed string with σ as its source or target type cannot admit an inﬁnite rewrite sequence for T . Thus, a well-typed string admits an inﬁnite rewrite sequence only if it is of type ρ → τ,which implies that it is of the canonical form. Note that the converse of the above lemma is obvious, since if T is terminating then it is terminating on all initial strings of any form, in particular (f|t|0|1|2) . As a whole, the rewriting system T simulates the iterated application of T (except at 1). Theorem 3.17 T is terminating if and only if T is convergent (i.e., the Collatz conjecture holds). Proof Without loss of generality (due to Lemma 3.16), consider only the strings of the canonical form (f|t|0|1|2) throughout this proof. We will show that, given such a string N, all rewrite sequences for T that start from N simulate the T -trajectory of Val(N ), except when Val(N ) = 1. More speciﬁcally, we prove the following and use them to deduce the theorem statement. Claim 1 For any pair N , N of strings, if N → N then Val(N ) = Val(N ), and if N → X D N then Val(N ) = T (Val(N )). Claim 2 For any string N with Val(N ) = 1, there exists no string N satisfying N → N . Claim 3 For any integer ν> 1 and any string N with Val(N ) = ν, there exists a string N such that N → N and Val(N ) = T (ν). Proof of Claim 1 Assume N → N . Then there exist strings X , Y and some rule → r ∈ X such that N = X Y and N = XrY . Recalling the deﬁnition of from (7), we have Val(N ) = Val(N ) if and only if ◦ ◦ = ◦ ◦ for all → r ∈ X.This Y r X Y X holds if and only if = for all → r ∈ X . With the functional views of the symbols as in (8), we indeed have: (x ) = f(0(x )) = 6x = 0(f(x )) = (x ) 0f f0 (x ) = t(0(x )) = 6x + 1 = 1(f(x )) = (x ) 0t f1 (x ) = f(1(x )) = 6x + 2 = 2(f(x )) = (x ) 1f f2 (x ) = t(1(x )) = 6x + 3 = 0(t(x )) = (x ) 1t t0 (x ) = f(2(x )) = 6x + 4 = 1(t(x )) = (x ) 2f t1 (x ) = t(2(x )) = 6x + 5 = 2(t(x )) = (x ) 2t t2 (x ) = t((x )) = 3 = 0((x )) = (x ) t 0 (x ) = f(f((x ))) = 4 = 1((x )) = (x ) ff 1 (x ) = t(f((x ))) = 5 = 2((x )) = (x ) ft 2 This proves the ﬁrst part of the claim. Now assume N → N . Again, there exist a string X and some rule → r ∈ D such D T that N = X and N = Xr (since the rules in D can be applied only at the rightmost end of thestring).WehaveVal(N ) = T (Val(N )) if and only if ◦ = T ◦ ◦ for all r X X → r ∈ D . This holds if and only if = T ◦ for all → r ∈ D . There are only two T r T rules to check, and indeed we have: (x ) = (x ) = x = T (2x ) = T ((f(x ))) = T ( (x )) (x ) = (2(x )) = 3x + 2 = T (2x + 1) = T ((t(x ))) = T ( (x )) 2 t This proves the second part of the claim. 123 15 Page 20 of 44 E. Yolcu et al. Proof of Claim 2 The string has Val() = 1, and inserting any symbol from {f, t, 0, 1, 2} in between the delimiters increases the value of the string, so is the unique string repre- senting 1. None of the rules in T apply to , which proves the claim. Proof of Claim 3 Let ν> 1beaninteger,and let N be a string with Val(N ) = ν.We will describe a rewrite sequence N → N → N , which implies by Claim 1 that X T Val(N ) = T (ν). For the rest of the proof let b and t stand for binary and ternary symbols, i i respectively. Assume that N contains some binary symbol (f or t), since otherwise it is of the form (0|1|2) and we can apply some rule from B to produce a binary symbol. Then the string contains some substring b t t ... t . We rewrite this substring into t b t ... t by 1 2 3 k 2 3 k applying some rule from X . For each 1 < i < k, assuming the current string contains some substring b t ... t , we rewrite it into t b t ... t . In the end we obtain a string N i i +1 k i +1 i +2 k with Val(N ) = ν that contains some b , so we apply some rule from D to obtain N such k T that Val(N ) = T (ν). Assume that the SRS T is not terminating. Let (N ) be an inﬁnite rewrite sequence i =0 for T , and consider the sequence (ν ) ,where ν = Val(N ). By Claim 1,for all i ∈ N, i i i i =0 we have either ν = ν or ν = T (ν ) depending on the rewrite rule used. Let I ={i ∈ i +1 i i +1 i N | ν = T (ν )}, which is the same as the set of indices at which some rule from D is i +1 i T applied in the rewrite sequence. By Lemma 3.15, the subsystem X = T \ D is terminating, so the rewrite → is performed inﬁnitely many times in the sequence. This implies that I is inﬁnite, proving that the sequence (ν ) is a Collatz trajectory. Moreover, this trajectory is i i ∈I nonconvergent, i.e., it does not contain 1, since otherwise the rewrite sequence could not be inﬁnite (because of Claim 2). This proves the backward implication in the theorem statement. Assume that the function T is not convergent. Let (ν ) be a nonconvergent trajectory, i =0 and note that ν > 1for all i ∈ N. We will inductively deﬁne a sequence (N ) such that i i i =0 Val(N ) = ν for all i ∈ N.Let N be any string with Val(N ) = ν . For each i ∈ N , i i 0 0 0 assuming Val(N ) = ν ,let N be a string such that N → N and Val(N ) = i −1 i −1 i i −1 i i T (ν ) = ν , which exists by Claim 3. Deﬁned in this manner, the sequence (N ) i −1 i i i =0 satisﬁes N → N for all i ∈ N,meaningthat T is not terminating. This proves the i i +1 forward implication in the theorem statement, which concludes the proof. When trying to remove a rule in D or B it sufﬁces to show relative top termination, allow- ing us to use weakly (instead of extended) monotone algebras when applying Theorem 2.15 and take advantage of the more relaxed constraints when searching for matrix interpretations. As we mentioned back in Section 2.1, the lemma below encapsulates dependency pairs, and it can in fact be automatically proved by the existing termination tools via the dependency pair transformation followed by an application of the dependency pair framework [36]. Lemma 3.18 1. For each subset R ⊆ B,if SN(R / T ) then SN(R / T ). top rev rev rev rev 2. For each subset Q ⊆ D ,if SN(Q / T ) then SN(Q / T ). top Proof Without loss of generality (due to Lemma 3.16), consider only the rewrite sequences that start with some string of the canonical form (f|t|0|1|2) (resp. its reversal). rev Let R ⊆ B (resp. Q ⊆ D ). The rules in R (resp. Q ) can be applied only at the leftmost end as they are all of the form s → t for some s, t not containing (resp. s → t for some s , t not containing ). rev rev Assume ¬ SN(R / T ) (resp. ¬ SN(Q / T )). Then there exists an inﬁnite rewrite rev rev sequence for T (resp. T ) where the rules from R (resp. Q ) are applied inﬁnitely many We thank an anonymous reviewer of CADE for pointing out this fact. 123 Automated Approach to Collatz Conjecture Page 21 of 44 15 times. As these rules can be applied only at the leftmost end, this implies relative top non- rev rev termination, i.e., ¬ SN(R / T ) (resp. ¬ SN(Q / T )). top top 3.3 Rewriting with a Hybrid System As another alternative to the rewriting system Z, instead of fully discarding unary in favor of a positional numeral system we may adopt a hybrid between the two approaches and design a system to increment/decrement by 1 or multiply/divide by 2 or 3 in a single rewrite. We will describe an SRS over the symbols {i, f, 0, , } viewed as follows. i(x ) = x + 1 f(x ) = 2x 0(x ) = 3x (x ) = 1 (x ) = x In essentially the same manner as we did for the system T , we have a set of dynamic rules that simulate the application of the Collatz function and a set of auxiliary rules that update the string representation so that the parity of the corresponding number can be recognized in a single step. We have the following 7-rule SRS L (designed by Luke Schaeffer). ⎧ ⎫ fii → if ⎨ ⎬ f → i → f i0 → 0iii D = A = B = fi → 0ii 0 → fi ⎩ ⎭ f0 → 0f As long as the string ends with f or fi, the parity of the represented number is apparent without needing to scan the whole string, which allows the Collatz function to be applied in a single rewrite. After the application of a dynamic rule, the string may no longer end with f or fi, so the auxiliary rules in X = A ∪ B push the symbol f towards the rightmost end of the string while preserving its value. Thus, L is yet another rewriting system that simulates the iterated application of the Collatz function. Theorem 3.19 L is terminating if and only if T is convergent. The proof of the above theorem is essentially the same as that of Theorem 3.17 once it is checked that the dynamic rules do indeed apply T and that the auxiliary rules do indeed preserve the value of a string under the functional view of the symbols. 4 Automated Proofs We adapt the rewriting system T for different generalized Collatz functions to explore the effectiveness of the mixed-base scheme on weakened variants of the Collatz conjecture. All of the rewriting systems, scripts to reproduce the proofs, and our minimal implementa- tion of a termination prover are available at https://github.com/emreyolcu/rewriting-collatz. In particular, any omitted relative termination proof that we refer to in this section is available at https://github.com/emreyolcu/rewriting-collatz/tree/main/proofs. 123 15 Page 22 of 44 E. Yolcu et al. 4.1 A Simple Example Earlier we mentioned a generalized Collatz function W as a simple example that could serve as a sanity check for an automated method aiming to solve Collatz-like problems. With the mixed binary–ternary scheme, this function can be seen to be simulated by the system W ={f → 0}∪ X . A small matrix interpretations proof is found for this system in less than a second, in contrast to its variant W that uses unary representations for which no automated proof is known. Additionally, the function W can be simulated by the rewriting system W ={f → 0}∪ X adapted from the hybrid system L, although we were unable to ﬁnd an automated proof of termination for W . Theorem 4.1 SN(W ). rev Proof The interpretations below prove SN({f → 0} / X ): 10 1 10 1 [f](x) = x + [t](x) = x + 01 1 00 0 10 12 [](x) = x [](x) = x 00 00 10 2 10 2 10 2 [0](x) = x + [1](x) = x + [2](x) = x + 01 0 10 2 10 2 rev With the above interpretations of the symbols, the rules of W satisfy the following rev relations, which, by Theorem 2.15, proves that {f → 0} is terminating relative to X . 12 3 12 2 [f](x) = x + > x + =[0](x) 00 0 00 0 10 3 10 3 [0f](x) = x + x + =[f0](x) 01 1 01 1 10 3 10 3 [1f](x) = x + x + =[t0](x) 10 3 00 0 10 3 10 3 [2f](x) = x + x + =[f1](x) 10 3 10 3 10 3 10 3 [0t](x) = x + x + =[t1](x) 00 0 00 0 10 3 10 3 [1t](x) = x + x + =[f2](x) 10 3 10 3 10 3 10 3 [2t](x) = x + x + =[t2](x) 10 3 00 0 10 2 10 1 [0](x) = x + > x + =[t](x) 00 0 00 0 10 2 10 2 [1](x) = x + x + =[ff](x) 10 2 00 2 123 Automated Approach to Collatz Conjecture Page 23 of 44 15 10 2 10 2 [2](x) = x + x + =[tf](x) 10 2 00 0 rev rev By Lemmas 2.8 and 3.15, X is terminating. As a result, W is terminating, which by Lemma 2.8 implies that W is terminating. 4.2 Farkas’Variant Let 2N + 1 ={1, 3, 5,... } denote the odd natural numbers. Farkas [37] studied a slight modiﬁcation F : 2N + 1 → 2N + 1 of the Collatz function for which it becomes possible to prove convergence via induction. We consider automatically proving the convergence of this function as another test case for the mixed-base scheme that is easier than the Collatz conjecture without being entirely trivial. Farkas deﬁned this function as ⎪ if n ≡ 0 (mod 3) n+1 F (n) = if n ≡ 0 (mod 3) and n ≡ 1 (mod 4) 3n+1 if n ≡ 0 (mod 3) and n ≡ 3 (mod 4). In this paper, we deﬁne another function F : N → N that resembles the Collatz function more closely than Farkas’ F (with respect to the deﬁnitions of the cases) while being equiv- alent to F in terms of convergence. It is obtained by introducing an additional case in the Collatz function for n ≡ 1 (mod 3) and applying T otherwise: n−1 ⎪ if n ≡ 1 (mod 3) F (n) = if n ≡ 0or n ≡ 2 (mod 6) 3n+1 if n ≡ 3or n ≡ 5 (mod 6) Given an F -trajectory, the bijection n → (n − 1)/2 applied to each of its iterates maps the trajectory to the corresponding F-trajectory. Thus, an F -trajectory reaches 1 if and only if the corresponding F-trajectory reaches 0. Furthermore, an F-trajectory reaches 0 if and only if it reaches 1, which is a convenient fact since in our string representations we do not represent 0, so in order to prove that F is convergent it sufﬁces to show that for all n ∈ N the trajectory F (n) contains 1. Note that F can also be viewed as a generalized Collatz function with 5 cases, which makes it straightforward to translate the cases of F into a set D of dynamic rules (shown below) to obtain a rewriting system that simulates the iterated application of F on positive integers. 1 → 0f → 0 1f → 1 1t → 12 2t → 22 Termination of the rewriting system F = D ∪ X is equivalent to the convergence of F. The proof of the equivalence is essentially the same as that of Theorem 3.17 except for the step where we construct a nonterminating rewrite sequence from a nonconvergent trajectory. To construct such a rewrite sequence for F, we take any nonconvergent F-trajectory and write the ﬁrst number in the trajectory in ternary (instead of binary). If the leading digit turns out to be 2 we replace it by 1 0 since the leading digit is always assumed to be 1 in 3 0 2 0 123 15 Page 24 of 44 E. Yolcu et al. our mixed-base representations. Then repeatedly performing the rightmost possible rewrite results in a rewrite sequence that simulates the F-trajectory. Farkas gave an inductive proof of convergence for F via case analysis. We found an auto- mated proof that F is terminating via arctic matrix interpretations. Below, we present both a manual proof of convergence for F and the automated proof of SN(F ). It is worth mention- ing that the default conﬁgurations of the existing termination tools (e.g., AProVE, Matchbox) are too conservative to prove the termination of this system, but after their authors tweaked the strategies they were also able to ﬁnd automated proofs via arctic matrix interpretations. It also remains an interesting question whether the automated proof somehow captures the argument in the inductive proof. + N Theorem 4.2 For all n ∈ N , the trajectory F (n) contains 1. Proof (in the manner of Farkas [37, Theorem 1]) We proceed by induction. For n = 1the result holds since F (1) = (1, 0, 0,...). Assuming it holds for all positive integers less than n, we will show that it holds for n. In particular, we will show that the trajectory of n reaches a number strictly smaller than n, which implies by the induction hypothesis that the trajectory contains 1. We split into three cases. (i) Assume n ≡ 1 (mod 3).Then F (n) = (n − 1)/3 is smaller than n. (ii) Assume n ≡ 0or n ≡ 2 (mod 6).Then F (n) = n/2 is smaller than n. (iii) Assume n ≡ 3or n ≡ 5 (mod 6). Denote n by N , and consider the trajectory F (N ) = (N , N , N ,...).Let 1 1 2 3 3N + 1 j −1 k = sup i ∈ N N = for all 1 < j ≤ i . We cannot have k =∞, i.e., F cannot apply N → (3N + 1)/2 indeﬁnitely, since for such a sequence we have j −1 3 3 N + 1 = (N + 1) = (N + 1). j j −1 1 2 2 As all the elements in the trajectory have to be integers, k −1 cannot exceed the number of times that N + 1 can be divided by 2, so k is ﬁnite. Consider N = (N + 1) − 1. k+1 1 It is of the form 3 · L − 1 for some positive integer L, so we know that either N ≡ 2 k+1 (mod 6) or N ≡ 5 (mod 6). Due to the way k is deﬁned, N cannot be congruent k+1 k+1 to 5 (mod 6),sowehave N ≡ 2 (mod 6). In particular, N is even, so (N + k+1 k+1 1 N +1 k 1) is odd, which in turn implies that is odd, i.e., we have N = 2 · (2M + 1) − 1 for some natural number M. Then, N satisﬁes k+1 k k k N = 3 · (2M + 1) − 1 = 3 · 2M + 3 − 1. k+1 Since N ≡ 2 (mod 6), we can deduce that k+1 k k N 3 · 2M + 3 − 1 k+1 F (N ) = = ≡ 1 (mod 3), k+1 2 2 and furthermore, k k 3 ·2M +3 −1 − 1 2 2 k−1 k−1 F (N ) = = 3 · 2M + 3 − 1 ≡ 2 (mod 6). k+1 123 Automated Approach to Collatz Conjecture Page 25 of 44 15 2k Repeatedly applying F in the above manner gives F (N ) = 2M.Since k ≥ 1, k+1 k N we have 2M < 2 · (2M + 1) − 1 = N = n,and so thetrajectory F (n) reaches a number strictly smaller than n. Proof (via arctic matrix interpretations) We will show SN(F ). By Lemmas 2.8 and 3.15, rev we have SN(X ). Consider the arctic matrix interpretations below. Recall that − indicates −∞ in the matrices. Also recall that arctic addition is max and arctic multiplication is +. ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−− 2 − 0 −−−− 2 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 20 −− − 020 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [f](x) = 2 −−−− x ⊕ − [t](x) = 2 − 2 −− x ⊕ − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ 0 0 −−−− ⎢ ⎥ ⎢ ⎥ 2 −−−−− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [](x) = − [](x) = −−−−− x ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ − −−−−− 4 −−−−− ⎡ ⎤ ⎡ ⎤ ⎡ 040 −− 1 −−−− 0 − 0 −− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 4 −−− − 40 −− − 4 −−− ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0](x) = − 40 −− x [1](x) = − 40 −− x [2](x) = 0 − 1 − 0 x ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ 03 0 −− 0 −−−− −−−−− −−−−− 03 0 −− 0 − 0 − 0 (9) rev rev Above interpretations prove SN(D / X ) by Theorem 2.15. (See Appendix B for the top rev rev rev corresponding interpretations of the rules of F .) We then get SN(D / X ) by Lemma rev rev rev 3.18. As we know that X is terminating, by Theorem 2.6 we can conclude SN(D ∪X ), which implies SN(F ) via Lemma 2.8. 4.3 Subsets of the Collatz System It is also interesting to consider whether we can automatically prove termination of proper subsets of T . Speciﬁcally, we considered the 11 subsystems obtained by leaving out a single rewriting rule from T , and we found termination proofs via matrix interpretations for all of the 11 subproblems. The reason for our interest in these problems is threefold: 1. Termination of T implies termination of all of its subsystems, so proving its termination is at least as difﬁcult a task as proving termination of the 11 subsystems. Therefore, the subproblems serve as additional sanity checks that an automated approach aspiring to succeed for the Collatz conjecture ought to be able to pass. Furthermore, they form an additional source of weakened variants that give us a heuristic idea of the suitable choice of parameters to use when searching for interpretations for the full problem. 2. When proving termination in a stepwise manner, we solve a sequence of relative termina- tion problems. Having proved termination of all 11 subsystems is a partial solution to the full problem, since it implies that for any single rule → r ∈ T , proving SN({ → r }/T ) settles the Collatz conjecture. 123 15 Page 26 of 44 E. Yolcu et al. 3. After the removal of a rule, the termination of the remaining system still encodes a valid mathematical question about the Collatz trajectories. The question of the termination of a proper subset is equivalent to asking if every corresponding Collatz trajectory that does not require the use of the left-out rule is convergent. For instance, removing {t → 2} deletes the odd case of the Collatz function, which gives a clearly convergent function. Removing the auxiliary rules in X lead to potentially more interesting questions: For instance, the termination of T \{t1 → 2f} implies that the trajectories where the pattern t1 is never encountered during the simulation are all convergent. Note that this type of inquiry is less meaningful for the unary system Z as its simulation of the Collatz function depends crucially on each rule being present. Leaving out some subset of the rules from Z causes the system to become terminating for a trivial reason, i.e., the computation it expresses no longer corresponds to the iterated application of some function. Example 4.3 As an instance of leaving out a rule, consider the subsystem T \{f1 → 0t}. There is a single-step natural matrix interpretations proof that this system is terminating: 11 13 1 [f](x) = x [t](x) = x + 10 34 1 15 10 1 [](x) = x [](x) = x + 00 10 1 72 2 21 1 22 0 [0](x) = x + [1](x) = x + [2](x) = x + 25 1 11 0 24 2 It can be checked that under these interpretations the rules of T \{f1 → 0t} satisfy the following relations: 20 2 10 1 [f](x) = x + > x + =[](x) 10 1 10 1 40 5 40 4 [t](x) = x + > x + =[2](x) 70 8 60 8 97 3 97 2 [f0](x) = x + > x + =[0f](x) 72 2 72 1 46 2 32 1 [f2](x) = x + > x + =[1f](x) 22 0 21 0 13 17 6 510 4 [t0](x) = x + > x + =[1t](x) 29 26 11 47 2 54 2 42 0 [t1](x) = x + > x + =[2f](x) 10 7 4 62 2 814 7 814 4 [t2](x) = x + > x + =[2t](x) 14 22 9 14 22 8 17 27 7 16 23 6 [0](x) = x + > x + =[t](x) 00 0 00 0 123 Automated Approach to Collatz Conjecture Page 27 of 44 15 76 1 76 0 [1](x) = x + > x + =[ff](x) 00 0 00 0 12 22 10 922 7 [2](x) = x + > x + =[ft](x) 00 0 00 0 Note that the left-out rule f1 → 0t ends up receiving a nondecreasing interpretation as there is no constraint to enforce otherwise: 32 1 13 29 11 [f1](x) = x + > x + =[0t](x) 21 1 17 26 8 The above interpretations witness for instance that the Collatz trajectory starting at 3 (represented as t) is convergent, because the missing rule is not used in any derivation of 1() from 3. Below is an example derivation along with the values each string represents and a vector value of each string under the interpretations above (setting x = (0, 0) for the purpose of demonstration). We omit the subscripts from the rewrite relations and simply write →. 3 5 5 8 884 2 1 t → 2 → ft → f2 → 1f → fff → ff → f → 79 78 68 62 41 40 26 14 12 > > > > > > > > 0 0 0 0 0 0 0 0 0 Table 1 shows the parameters of the matrix interpretations proofs that we found for the termination of each subsystem. For each rule → r that is left out, we searched for a stepwise proof to show that B \{ → r } is terminating relative to T \{ → r } (freely utilizing weakly monotone algebras due to Lemma 3.18). Such a proof requires at most three steps since there areatmostthree rulesin B \{ → r }. In the table, we report the smallest parameters (in terms of matrix dimension) that work for all of these steps. As we already know that SN(T \ B) holds (by Lemma 3.15), the interpretations found allow us to conclude the termination of each subsystem. This is not the only way to prove termination of the subsystems; however, we chose this uniform strategy for the sake of comparison. In the experiments we searched for matrices of up to 7 dimensions, with the coefﬁcients taking at most 8 different values. 4.4 Odd Trajectories In the originally deﬁned Collatz function C, applying 2n + 1 → 6n + 4 produces an even number, so we incorporate a single division by 2 into the deﬁnition of the odd case and obtain the function T with the same overall dynamics as C. Taking this idea further by performing as many divisions by 2 as possible leads to the so-called Syracuse function Syr : 2N + 1 → 2N + 1, deﬁned as 3n + 1 + k Syr(n) = ,where k = max{k ∈ N | 2 divides 3n + 1}. The Syracuse function maps each odd number to the next odd number in its Collatz trajec- tory. In this sense, it has the same overall dynamics as the Collatz functions C or T we have previously deﬁned, i.e., Syr is convergent if and only if C or T is convergent. The function T takes fewer steps than C to reach 1 and can be thought of as an accelerated Collatz function, 123 15 Page 28 of 44 E. Yolcu et al. Table 1 Smallest proofs found for termination of subsystems of T in under 30 seconds. The columns show the matrix dimension D and the maximum number V of distinct coefﬁcients that appear in the matrices, along with the median time to ﬁnd an entire termination proof across 25 repetitions for the ﬁxed D and V . Natural Arctic Rule removed DV Time DV Time 1.42s 15.95s f → 34 35 t → 2 12 0.27s 13 0.28s f0 → 0f 42 0.92s 34 2.46s 0.50s 0.51s f1 → 0t 13 14 f2 → 1f 12 0.38s 13 0.39s t0 → 1t 43 1.20s 34 0.87s t1 → 2f 52 0.89s 43 0.84s t2 → 2t 44 10.00s 25 0.62s 0 → t 22 0.40s 23 0.42s 1 → ff 33 0.53s 34 0.57s 2 → ft 44 7.51s 43 4.04s making the Syracuse function a further accelerated version. Reducing the number of steps towards convergence is of interest mainly because the existence of various kinds of termi- nation proofs is dependent on the derivational complexity of the rewriting system staying below certain thresholds [38]. For instance, given a rewriting system, if its termination can be proved in a single-step via natural matrix interpretations then its derivational complexity is at most exponential [10]. Similarly, a single-step termination proof via arctic matrix inter- pretations implies a linear derivational complexity [11]. Thus, it can be preferable to work with an alternative rewriting system with smaller derivational complexity that still simulates the dynamics of the Collatz function. Expressing the Syracuse function as a generalized Collatz function would require inﬁnitely many cases to account for all of the possible appearances of 2 as the denominator with different values of k. As a result, we are unable to simulate it with a ﬁnite rewriting system. Nevertheless, we may compromise and accelerate the Collatz function by a smaller amount. 3n+1 We ﬁrst observe that if n ≡ 1 (mod 8) then Syr(n) = and if n ≡ 3 (mod 4) then 3n+1 Syr(n) = . Furthermore, for any n ∈ N we have Syr(8n + 5) = Syr(2n + 1) since 3(8n + 5) + 1 = 24n + 16 = 4(6n + 4) = 4(3(2n + 1) + 1). Putting these observations together, we can deﬁne a generalized Collatz function S : 2N + 1 → 2N + 1 as follows. 3n+1 if n ≡ 1 (mod 8) n−1 S(n) = if n ≡ 5 (mod 8) 3n+1 if n ≡ 3 (mod 4) Example 4.4 The three trajectories below illustrate how the dynamics of C, Syr, and S com- pare to one another. • C (19) = (19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1, 4, 2, 1,...) Derivational complexity is deﬁned as the maximal length of rewrite sequences in the system as a function of the length of the initial string in the sequence. 123 Automated Approach to Collatz Conjecture Page 29 of 44 15 • Syr (19) = (19, 29, 11, 17, 13, 5, 1, 1,...) • S (19) = (19, 29, 7, 11, 17, 13, 3, 5, 1, 1,...) Note that a Syr-trajectory simply consists of the odd numbers in the corresponding C- trajectory; however, an S-trajectory is not necessarily contained in the corresponding C-trajectory. This is due to the n ≡ 5 (mod 8) case of S that maps n to a number not necessarily contained in the C-trajectory (marked in bold above). Once one of the other two cases is encountered, the S-trajectory arrives back at the number Syr(n). S is convergent if and only if C (or T ) is convergent, and the number of steps that S takes to converge is between that of T and Syr. In a manner similar to before, we can translate the cases of S into a set D of dynamic rules (shown below). Since we are working with odd numbers we use a new symbol • to mark the end of a string, viewed functionally as •(x ) = 2x + 1. ff•→ 0• tf•→• t•→ 2• Termination of the rewriting system S = D ∪ X is equivalent to the convergence of S. Similar to T , proving the termination of S is currently beyond our reach, although it may potentially be an easier path to the Collatz conjecture (compared to proving SN(T )). Failing to prove the termination of S itself, we considered the subsystems of S as we did for T in Section 4.3. With matrix interpretations, termination of all but two of the 11-rule subsystems of S was automatically proved. Despite devoting thousands of CPU hours, we were not able to ﬁnd interpretations to prove that S = S \{ff•→ 0•} or S = S \{tf•→•} is 1 2 terminating. By the discussion in Section 4.3, termination of subsystems of S corresponds to questions about the trajectories of S. In particular, for S and S we have the following. 1 2 Proposition 4.5 1. SN(S ) if and only if all nonconvergent S-trajectories contain some n ≡ 1 (mod 8). 2. SN(S ) if and only if all nonconvergent S-trajectories contain some n ≡ 5 (mod 8). We can prove automatically via matrix interpretations that S = S \{t•→ 2•} is terminating, which implies the following through an equivalence of the above form for S . Proposition 4.6 All nonconvergent S-trajectories contain some n ≡ 3 (mod 4). Leaving out some dynamic rules from a mixed-base rewriting system that simulates a generalized Collatz function allows us to phrase the above kinds of questions as termination problems. Recall that, although S is equivalent to C in terms of convergence, its trajectories are not necessarily contained in the Collatz trajectories, so we cannot substitute C for S in the above statements (except for the second item of Proposition 4.5, since the left-out rule is the one that maps to a number not contained in the Collatz trajectory). In the next section, we perform the same kind of inquiry into the original Collatz trajectories. 4.5 Collatz Trajectories Modulo 8 Our initial motivation for the previous section was to ﬁnd rewriting systems with reduced derivational complexity. This inquiry led us to surprisingly difﬁcult Collatz-like problems, which we believe may be on the border of the reach of automated methods. In this section we explore more problems of a similar form and present the unsolved ones as potentially reachable targets for automated termination proving. 123 15 Page 30 of 44 E. Yolcu et al. Fig. 1 Transition graphs of the iterates in the Collatz trajectories across residue classes modulo 8 for the functions C (left), T (middle), S (right). For each function f , the edge u → v is part of its transition graph if and only if there exists some n ≡ u (mod 8) such that f (n) ≡ v(mod 8). Bold edges indicate transitions where f (n)> n. Let m beapower of 2. Given k ∈{0, 1,..., m − 1}, is it the case that all nonconvergent Collatz trajectories contain some n ≡ k (mod m)? For several values of k this can be proved by inspecting the transitions of the iterates in the Collatz trajectories across residue classes modulo m (shown on Figure 1 for m = 8). As an example, consider the case k = 6. Proposition 4.7 All nonconvergent C-trajectories contain some n ≡ 6 (mod 8). Proof Let t be a C-trajectory. The path that t takes over the transition graph of C in Figure 1 is a concatenation of the simple cycles of the graph. If t does not contain any n ≡ 6 (mod 8), then the cycles containing 6 cannot occur in the path, which leaves eight cycles (listed below). By composing the functions applied at each transition in the graph, we can compute the mapping (call it c) applied to an iterate after traversing a cycle: Cycle c(n) (0, 4, 2, 5, 0)(3n + 8)/8 (0, 0) n/2 (1, 4, 2, 1)(3n + 1)/4 (2, 5, 0, 4, 2)(3n + 2)/8 (2, 1, 4, 2)(3n + 2)/4 (4, 2, 5, 0, 4)(3n + 4)/8 (4, 2, 1, 4)(3n + 4)/4 (5, 0, 4, 2, 5)(3n + 1)/8 For t to be nonconvergent, it needs to contain inﬁnitely many occurrences of cycles that increase the values of the iterates. All of the above cycles decrease the values of the iterates, so each iterate of t eventually reaches a smaller number, implying t is convergent. Propositions of the above kind can also be formulated as termination of some rewriting systems. With this approach we found automated proofs for several cases. We start by studying the smallest interesting case m = 4. Consider the following two sets of dynamic rules to simulate the Collatz function. ⎧ ⎫ ⎧ ⎫ ff → f f → ⎨ ⎬ ⎨ ⎬ Even/4 Odd/4 D = tf → t D = ft → 1f C T ⎩ ⎭ ⎩ ⎭ t → 2f tt → 2t 123 Automated Approach to Collatz Conjecture Page 31 of 44 15 Even/4 Even/4 It is straightforward to see that the SRS C = D ∪ X simulates the function C Odd/4 Even/4 Odd/4 and the SRS T = D ∪ X simulates the function T . The ﬁrst two rules of D T C express the application of C to numbers of the form 4n and 4n +2. Similarly, the last two rules Odd/4 of D express the application of T to numbers of the form 4n +1and 4n + 3. Observing that a T -trajectory contains the same odd numbers as the corresponding C-trajectory, we have the following equivalences. Proposition 4.8 Even/4 1. SN(C \{ff → f}) if and only if all nonconvergent C-trajectories contain some n ≡ 0 (mod 4). Even/4 2. SN(C \{tf → t}) if and only if all nonconvergent C-trajectories contain some n ≡ 2 (mod 4). Odd/4 3. SN(T \{ft → 1f}) if and only if all nonconvergent C-trajectories contain some n ≡ 1 (mod 4). Odd/4 4. SN(T \{tt → 2t}) if and only if all nonconvergent C-trajectories contain some n ≡ 3 (mod 4). We were able to prove termination of the above four systems via matrix interpretations, thus establishing the following. Theorem 4.9 If there exists a nonconvergent Collatz trajectory, it cannot avoid any of the residue classes modulo 4. Next, we look at the case m = 8. It can be studied via the analogously deﬁned rewriting systems: ⎧ ⎫ ⎧ ⎫ fff → ff f → ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ftf → ft fft → 0tf ⎨ ⎬ ⎨ ⎬ Even/8 Odd/8 D = tff → tf D = ftt → 1ft C T ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ttf → tt tft → 2ff ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⎭ ⎩ ⎭ t → 2f ttt → 2tt Even/8 Odd/8 Even/8 Odd/8 The SRS C = D ∪ X simulates the function C and the SRS T = D ∪ X C T simulates the function T . We do not formally state the analogue of Proposition 4.8 —ter- Even/8 Odd/8 minations of the eight subsystems obtained from C or T are each equivalent to the question of whether all nonconvergent Collatz trajectories have to encounter the corre- sponding residue class modulo 8. Through automated proofs, we were able to establish the following. Theorem 4.10 If there exists a nonconvergent Collatz trajectory, it cannot avoid the residue classes of 2, 3, 4, 6 modulo 8. Theorems 4.9 and 4.10 are also not difﬁcult to prove by hand; however, it remains open whether an analogue of Theorem 4.10 holds for the residue classes of 0, 1, 5, 7 modulo 8, that is, we have neither manual nor automated proofs for these cases. They may serve well as easier Collatz-like open problems to test our abilities against, so we offer a $500 reward for a resolution of any of the following conjectures. See Denend [39, Section 4] for a heuristic prediction of the relative easiness of those cases. Denend uses an empirical measure based on the number of odd elements occurring in a trajectory until either a certain residue class or 1 is encountered, which resembles the ones-ratio and the stopping time ratio deﬁned by Applegate and Lagarias [40]. The case 0 is omitted as its answer follows from the case 5 by Figure 1. 123 15 Page 32 of 44 E. Yolcu et al. Conjecture 4.11 All nonconvergent C-trajectories contain some n ≡ 1 (mod 8). Conjecture 4.12 All nonconvergent C-trajectories contain some n ≡ 5 (mod 8). Conjecture 4.13 All nonconvergent C-trajectories contain some n ≡ 7 (mod 8). Even the following easier statement remains unproved, although we were able to prove (both manually and automatically) its versions with {1, 5} and {1, 7} as the residue classes. Conjecture 4.14 All nonconvergent C-trajectories contain either some n ≡ 5 (mod 8) or some n ≡ 7 (mod 8). We can alternatively formulate each of the above conjectures as the convergence problem of some partial generalized Collatz function. For instance, Conjecture 4.14 is equivalent to + + the convergence of the function H : N → N deﬁned as follows. ⊥ ⊥ 3n ⎪ if n ≡ 0 (mod 4) 9n+1 H (n) = if n ≡ 7 (mod 8) (10) ⊥ otherwise Proposition 4.15 H is convergent if and only if all nonconvergent C-trajectories contain either some n ≡ 5 (mod 8) or some n ≡ 7 (mod 8). Proof Recall from Figure 1 the transition graph of the iterates in C-trajectories across residue classes modulo 8. Observe that if a nonconvergent trajectory avoids the residue classes of 5 and 7 (mod 8), then it has to visit the residue class of 1 (mod 8), so we may assume without loss of generality that each nonconvergent trajectory starts with some n ≡ 1 (mod 8). Then a nonconvergent trajectory that avoids the residue classes of 5 and 7 (mod 8) can traverse only the cycle of classes (1, 4, 2, 1) or (1, 4, 6, 3, 2, 1). The former, which is traversed only if n ≡ 1 (mod 32), effects the map n → (3n + 1)/4. The latter, which is traversed only if n ≡ 57 (mod 64), effects the map n → (9n + 7)/8. If n belongs to any other residue class, either the trajectory is convergent, or it contains some k ≡ 5 (mod 8) or some k ≡ 7 + + (mod 8). As a result, the function G : N \{1}→ N \{1} deﬁned as ⊥ ⊥ 3n+1 ⎪ if n ≡ 1 (mod 32) 9n+7 G(n) = if n ≡ 57 (mod 64) ⊥ otherwise is nonconvergent if and only if there exists a nonconvergent C-trajectory that avoids the residue classes of 5 and 7 (mod 8). Moreover, H as deﬁned in (10)isconvergentifand only if G is convergent, because the bijection n → (n − 1)/8mapsa G-trajectory to an H-trajectory. 4.6 SAT Solving Considerations Phase-Saving Heuristic Most top-tier termination tools, such as AProVE, Matchbox,and T T ,use theSAT solver MiniSat [41] to search for matrix interpretations. This choice is T 2 somewhat surprising as MiniSat has not been updated since 2008 and the performance of SAT solvers has improved signiﬁcantly in the last decade. The use of MiniSat in these provers is motivated by its observed effectiveness in ﬁnding interpretations. We investigated the reason for this, which turned out to be a heuristic that MiniSat disables in its default conﬁguration. 123 Automated Approach to Collatz Conjecture Page 33 of 44 15 Most SAT solvers sort variables by the frequency of their occurrences in recent conﬂict clauses, selecting the highest ranked one as the variable to branch on [42]. This procedure is similar in MiniSat and modern SAT solvers. However, once a variable is picked, the solvers differ in the truth value assignment that they explore ﬁrst. MiniSat uses negative branching [41], which explores the “false” branch ﬁrst for all decision variables. The empirical effectiveness of this heuristic likely stems from its interaction with the common choices of propositional encodings used when translating problems into SAT instances. Modern SAT solvers use phase-saving [43], which ﬁrst explores the branch corresponding to the truth value to which the variable was forced most recently during unit propagation. We offer the following explanation for the effectiveness of negative branching. We use the order encoding [44, 45] when translating the integer constraints from Section 2.3 into CNF formulas. In this encoding, each variable X that takes values in a ﬁnite domain A ={0, 1,..., n + 1} is represented by a corresponding list of n + 1 Boolean variables (x , x ,..., x ). Each Boolean variable x indicates X > i.Asanexample, X = 2has 0 1 n i the corresponding assignment (1, 1, 0, 0,..., 0). This encoding gives a natural way of rep- resenting inequality constraints. For instance, the constraint a < X ≤ b can be enforced simply by setting x = 1and x = 0. As another example, for variables X, Y the inequality a b X ≤ Y can be expressed by the conjunction (¬x ∨ y ). Consequently, when using the i i i =0 order encoding, representations that correspond to smaller numbers require setting a larger fraction of the Boolean variables to false. For instance, the representation of zero or minus inﬁnity assigns all variables to false. Moreover, the matrices and the vectors that occur in the interpretations are often sparse and contain relatively few large numbers. As a result, negative branching possibly directs the search towards a satisfying assignment more often. Additionally, in contrast to phase-saving, negative branching tends to guide the solver to a potentially different part of the search space after a restart (which is performed frequently in SAT solvers). The increased diversity of the search space (across restarts) that is explored due to negative branching is also possibly helpful for the kinds of the problems discussed in this paper. One can enable negative branching in most SAT solvers, which in our case improves solver performance for some of the formulas that encode the existence of interpretations. Heavy-Tailed Behavior of SAT Solvers Combinatorial search algorithms can have a tendency to show a large variance in runtime across different, randomly selected initial conditions of the search. For instance, Gomes et al. [46] observed that DPLL solvers [47, 48] had a substantial fraction of very short runs when dealing with relatively hard instances. This suggests that trying to solve such instances using several parallel runs is a reasonable strategy, since some of the runs will have a nonnegligible chance of ﬁnishing early. Modern SAT solvers incorporate heuristics that alleviate the heavy-tailed behavior to some extent; however, the variability in runtime (especially on satisﬁable instances) is not completely eliminated. In our termination prover, we run multiple instances of the SAT solver (speciﬁcally, CaDiCaL [49]) in parallel on the formula that encodes the existence of an interpretation. We introduce additional randomness to the procedure by running each parallel instance with a different shufﬂing of the clauses in the formula. Ideally, solver performance would be invariant to the ordering of the clauses; however, the clause order indirectly affects the variable selection heuristic, which ends up inﬂuencing runtime. Experiments with Solver Conﬁgurations Table 2 shows the difference in runtime for both MiniSat and CaDiCaL due to negative branching and parallelism with a few small-scale 123 15 Page 34 of 44 E. Yolcu et al. Table 2 Difference in runtime due to negative branching and parallelism. Each row cor- responds to a single step of a relative termination proof occurring in the previous sections of this paper. The leftmost columns show the original system being proved as terminating, along with the parameters of the interpretations being searched for (D for dimension, V for the number of different values each coefﬁcient may take) that remove at least a single rule from the system. For each solver, each of the remaining columns shows the median time the experiment takes over 25 repetitions. Each run times out after 120 seconds, and runs that time out are counted as having taken double the allowed time. Phase-saving Negative branching Problem Interp. DV Solver Single Parallel Single Parallel F Arctic 5 8 240.00s 240.00s 85.60s 5.47s T \{f → } Arctic 3 5 0.62s 0.09s 67.69s 15.74s T \{f0 → 0f} Arctic 3 4 3.18s 0.91s 2.19s 0.91s T \{t2 → 2t} Natural 4 4 240.00s 63.71s 240.00s 87.85s T \{2 → ft} Natural 4 4 240.00s 240.00s 69.73s 5.25s T \{2 → ft} Arctic 4 3 1.39s 0.18s 7.65s 1.71s Even/8 C \{ttf → tt} Natural 3 11 240.00s 240.00s 240.00s 240.00s Odd/8 T \{ftt → 1ft} Arctic 3 12 2.35s 0.36s 117.37s 0.88s F Arctic 5 8 240.00s 240.00s 44.45s 9.22s T \{f → } Arctic 3 5 1.52s 0.13s 29.95s 13.12s T \{f0 → 0f} Arctic 3 4 3.75s 0.83s 3.27s 1.71s T \{t2 → 2t} Natural 4 4 75.78s 19.12s 29.62s 8.13s T \{2 → ft} Natural 4 4 75.05s 5.22s 24.31s 6.43s T \{2 → ft} Arctic 4 3 3.33s 0.52s 11.55s 3.84s Even/8 C \{ttf → tt} Natural 3 11 240.00s 240.00s 240.00s 79.05s Odd/8 T \{ftt → 1ft} Arctic 3 12 1.94s 0.33s 3.28s 0.38s experiments. From all the automated proofs in this paper, we selected the steps where the SAT solving phase took longer than 2 seconds, and reran the prover for these speciﬁc steps with different conﬁgurations of those SAT solvers. When running only a single instance of a solver, we used the nonshufﬂed formula. In the parallel case, we ran 8 solver instances with one of the instances receiving the nonshufﬂed formula and the other 7 receiving random shufﬂes. Running multiple instances of a solver in parallel is a considerable improvement in all cases where the allotted time is enough to ﬁnd an interpretation. Negative branching has an adverse effect in some cases, although in two of the most difﬁcult instances (F and Even/8 C \{ttf → tt}) it makes the difference between ﬁnding an interpretation relatively quickly and timing out. It also appears that, at least for the more difﬁcult cases, replacing MiniSat by CaDiCaL can be beneﬁcial. These experiments are not extensive enough to derive broad conclusions; however, they suggest that running multiple instances of a modern SAT solver with negative branching enabled in some and disabled in others can be a reasonably diverse strategy when searching for matrix interpretations. CaDiCaL MiniSat Automated Approach to Collatz Conjecture Page 35 of 44 15 5 Related Work There are several previous studies of the Collatz conjecture through alternative models of computation. String Rewriting Systems To our knowledge, Zantema [13], with his system Z,which we saw in Section 3.1, was the ﬁrst to attempt using an automated method and string rewriting to search for a proof of the Collatz conjecture. In addition, although we independently discovered the mixed binary–ternary system described in Section 3.2, Scollo [50] had essentially the same idea, the distinction being that he adopted a functional view of the digits that is different than in (8). Scollo was not concerned with proving termination, though, and proposed rewriting primarily as a formalism that forgoes the arithmetic interpretation of the iterates and instead emphasizes the dynamic/computational behavior. Tag Systems An m-tag system [51] is a computational model described by a set of produc- tion rules that map symbols to strings (or “tags”). Given an initial string X = x x ... x ,the 0 1 n tag system ﬁnds the rule x Z whose LHS matches the leftmost symbol of X, appends the tag Z to X, and deletes the ﬁrst m symbols of XZ; resulting in a new string X = x x ... x Z. m m+1 n The tag system repeats this transformation until reaching a string of length less than m,at which point it halts. De Mol [52] showed the existence of a small 2-tag system with the following rules that simulates the iterated application of the Collatz function given a unary representation: This tag system halts if and only if the Collatz conjecture holds, giving yet another formulation of the problem. De Mol further extended this scheme to allow the simulation of an arbitrary generalized Collatz function with modulus d by a d-tag system. Cellular Automata Kari [53] designed 1D cellular automata that perform multiplication by 3and 3/2 in base 6, and reformulated both the Collatz conjecture and Mahler’s 3/2 problem as sets of constraints to be satisﬁed by the space-time diagrams of these cellular automata. String Arithmetic Kauffman [54] developed a formalism to perform arithmetic, which he called string arithmetic, and expressed the Collatz conjecture within it. This formalism works with unary representations of numbers, and uses the three symbols 1, , . Letting denote the empty string and N be any string representing a number, string arithmetic consists of the following bidirectional rewrite rules (or “identities”) to convert between different strings representing the same number: ← → 11 ← → 1 1N ← → N1 Along with the above identities, Kauffman’s encoding of the Collatz function uses the fol- lowing two rules: N → N N1 → N1N 123 15 Page 36 of 44 E. Yolcu et al. The Collatz conjecture becomes the question of whether for strings of 1s of all lengths there exists a rewrite sequence using the ﬁve rules above to reach the string 1. 6 Conclusions We presented an approach to prove convergence of instances of generalized Collatz functions by translating them into string rewriting systems and applying SAT solving to ﬁnd matrix interpretations that show termination. Important components of our approach include the quality of the translation into rewriting, the use of weakly monotone -algebras, and dedi- cated heuristics in the SAT solving phase. We considered some interesting, simpler variants of the Collatz conjecture to gauge the feasibility of this approach in proving mathemati- cally interesting statements. We observed that some variants could be solved only via natural matrix interpretations, while others required arctic matrix interpretations. Several extensions to this work can further our understanding of the potential of rewriting techniques for answering mathematical questions. For instance, it is of interest to study the efﬁcacy of different termination proving techniques on the problems that we considered. In particular, we found matrix interpretations to be the most successful for our purposes despite the existence of newer techniques developed for automatically proving termination of a few select challenging instances. Although matrix interpretations lead to automated proofs of several weakened variants discussed in this paper, it might still be the case that there exist no such interpretations to establish the termination of the Collatz system T (as we have shown in the case of natural matrix interpretations for Zantema’s system Z). This would be an interesting result in itself. Another issue is the matter of representation; speciﬁcally, it is worth exploring whether there exists a suitable translation of the Collatz conjecture into the termination of a term, instead of string, rewriting system since many automated termination proving techniques are generalized to term rewriting. Finally, injecting problem-speciﬁc knowledge into the rewriting systems or the termination techniques would be helpful as there exists a wealth of information about the Collatz conjecture that could simplify the search for a termination proof. Acknowledgements We thank Johannes Waldmann for insightful discussions regarding arctic matrix inter- pretations, for pointing us to [53] and the rewriting system in Example 3.3, for responding to our challenge to solve Farkas’ variant with Matchbox, and for feedback on an early draft. We thank Carsten Fuhs and Jürgen Giesl for responding to our challenge to solve Farkas’ variant with AProVE. We additionally thank Carsten Fuhs for his thorough explanations of the dependency pair framework and AProVE’s strategies. We thank Florian Frohn for responding to the challenge to solve the subsystems from Section 4.3 with AProVE.We thank Jeffrey Lagarias for discussions regarding the problems in Section 4.5. We thank Luke Schaeffer and Chris Lynch for discussions on alternative rewriting systems that simulate the Collatz map. We thank Jeremy Avigad and Jasmin Blanchette for their detailed comments on an early draft. Finally, we thank the reviewers of CADE for their comments on the preliminary version of this paper and the reviewers of the Journal of Automated Reasoning for their comments on the journal version. This material is based upon work supported by the National Science Foundation under grant CCF-2006363. Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. 123 Automated Approach to Collatz Conjecture Page 37 of 44 15 A Alternative Proof of Lemma 3.16 Let us recall the statement of the result before proceeding with the proof. Lemma 3.16 If T is terminating on all initial strings of the canonical form (f|t|0|1|2) , then T is terminating (on all initial strings). Proof Assume there exists some string X ∈{f, t, 0, 1, 2, , } that admits an inﬁnite rewrite sequence for T .View X as split into blocks delimited by or , i.e., for some k ∈ N , write X = N d N d ... d N , 1 1 2 2 k−1 k where d ∈{, } for each 1 ≤ i < k,and N ∈{f, t, 0, 1, 2} for each 1 ≤ i ≤ k.Any i i string containing X also admits an inﬁnite rewrite sequence, so instead consider Z = d Xd , 0 k written as Z = d N d N d ... d N d , 0 1 1 2 2 k−1 k k where d , d ∈{, }. 0 k As T is not terminating on Z, there exists some rewrite rule applicable to it. Consider an arbitrary block of Z along with its neighbors (to which some rewrite rule of T applies), written as V = PcQd R, where c, d ∈{, } and P, Q, R ∈{f, t, 0, 1, 2} . Due to the shapes of the rules of T ,the string V can be rewritten only into one of the following: " " V = PcQd R such that Pc → Pc 1 T " " V = PcQd R such that cQd → cQd 2 T " " V = PcQd R such that dR → d R 3 T In any case, the delimiters are unchanged, and only a single block is affected by the rewrite. This means that any rewrite sequence that starts from Z consists of several sequences that each operate entirely on some block of Z. Thus, since Z has ﬁnitely many blocks, there exists some block that admits an inﬁnite rewrite sequence. In particular, there exists a string cNd, where c, d ∈{, } and N ∈{f, t, 0, 1, 2} , that can be rewritten indeﬁnitely. We claim that this requires c = and d = , so the string cNd is of the canonical form (f|t|0|1|2) .As shown below, the other cases are all terminating. (i) N : This string does not contain , so it can be rewritten using only the rules in T \ B, but we know from Lemma 3.15 that SN(T \ B), so there can be no inﬁnite rewrite sequence. (ii) N : This string does not contain , so it can be rewritten using only the rules in T \D , but we know from Lemma 3.15 that SN(T \ D ), so there can be no inﬁnite rewrite sequence. (iii) N :The SRS T contains no rules of the form s → t or s → t for any s, t,so this string can be rewritten using only the rules in T \ (B ∪ D ). Since each subset of a terminating SRS is terminating, by Lemma 3.15 we conclude SN(T \ (B ∪ D )),so there can be no inﬁnite rewrite sequence. This proves the contrapositive of the lemma statement. 123 15 Page 38 of 44 E. Yolcu et al. B Remaining Part of the Automated Proof for Farkas’ Variant rev With the interpretations from (9), the rules of F satisfy the following relations: ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 1 −−−− − 0 −−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 252 −− 0 040 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [f0](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[0](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 −−−− 0 1 −−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [f1](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[1](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 252 −− 0 140 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [t1](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[21](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 − 2 − 2 0 0 − 1 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− − −−−−− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [t2](x) = −−−−− x ⊕ − −−−−− x ⊕ − =[22](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2642 − 0 25 2 −− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 64 −− − − 60 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0f](x) = 264 −− x ⊕ − ≥ 26 2 −− x ⊕ − =[f0](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ 2532 − 0 −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−− 3 − 1 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 264 −− − 06 0 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1f](x) = 264 −− x ⊕ − ≥ 26 2 −− x ⊕ − =[t0](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−− 2 − 0 −−−−− − 2532 − 0 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 −− 2 − 0 2 −−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ − 64 −− − − 62 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [2f](x) = 3 −− 2 − x ⊕ 0 ≥ 3 −−−− x ⊕ − =[f1](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − 2 −− 2 − 0 −−−−− − 123 Automated Approach to Collatz Conjecture Page 39 of 44 15 ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 464 − 4 0 25 2 −− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 464 − 4 − 162 −− − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0t](x) = 464 − 4 x ⊕ − ≥ 362 −− x ⊕ − =[t1](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ 353 − 3 0 −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−− 3 1 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 464 − 4 − 061 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1t](x) = 464 − 4 x ⊕ − ≥ 2 − 2 −− x ⊕ − =[f2](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−− 2 0 −−−−− − 353 − 3 0 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ 2 − 2 − 2 0 2 − 2 − 2 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ 464 − 4 − 061 − 0 − ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [2t](x) = 3 − 3 − 2 x ⊕ 0 ≥ 2 − 3 − 2 x ⊕ − =[t2](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − 2 − 2 − 2 0 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−−− 6 −−−−− 6 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− 6 −−−−− 4 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [0](x) = −−−−− x ⊕ 6 ≥ −−−−− x ⊕ 2 =[t](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− 5 −−−−− − −−−−− − −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−−− 1 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− 6 −−−−− 6 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [1](x) = −−−−− x ⊕ 6 ≥ −−−−− x ⊕ 2 =[ff](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− 0 −−−−− − −−−−− 5 −−−−− − ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ ⎡ ⎤ −−−−− 0 −−−−− 0 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ −−−−− 6 −−−−− 6 ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ [2](x) = −−−−− x ⊕ 4 ≥ −−−−− x ⊕ 4 =[tf](x) ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ ⎣ ⎦ −−−−− − −−−−− − −−−−− 4 −−−−− − C More Problems to Approach via Rewriting We adapt the mixed base scheme for several other open problems and reformulate them as termination of relatively small rewriting systems. C.1 Mahler’s 3/2 Problem Deﬁnition C.1 Let ξ ∈ R be a positive real number. It is called a Z-number if for all k ∈ N >0 # $ 3 1 we have frac ξ < , where frac(·) denotes the fractional part of the number. 2 2 123 15 Page 40 of 44 E. Yolcu et al. Mahler [55] conjectured that there are no Z-numbers. Moreover, he considered a gener- + + alized Collatz function M : N → N , deﬁned as follows. 3n if n ≡ 0 (mod 2) M (n) = 3n+1 if n ≡ 1 (mod 2) He related the behaviors of M-trajectories to the existence of Z-numbers: Theorem C.2 For n ∈ N , if a Z-number exists in the interval [n, n + 1), then there is no k ∈ N for which M (n) ≡ 3 (mod 4). In order to formulate this as a termination problem, we split the odd case of M into two and leave one undeﬁned: 3n ⎪ if n ≡ 0 (mod 2) 3n+1 M (n) = if n ≡ 1 (mod 4) ⊥ if n ≡ 3 (mod 4) Given n ∈ N , if the trajectory M (n) contains ⊥ then by the contrapositive of Theorem C.2 there is no Z-number in the interval [n, n + 1). When proving nonexistence, we may assume without loss of generality that a Z-number is at least 1, since if ξ ∈ (0, 1) is a Z-number then ξ ∈[1, ∞) is another one for sufﬁciently large m ∈ N. Thus, the nonexistence of Z-numbers can be established by proving that M is convergent, which is equivalent to the termination of the following rewriting system M. In order to ensure termination at the case n ≡ 3 (mod 4), there is no rule with the LHS tt. f → 0 f0 → 0f t0 → 1t 0 → t ft → 10 f1 → 0t t1 → 2f 1 → ff f2 → 1f t2 → 2t 2 → ft C.2 Halting Problem for Busy Beavers The busy beaver problem [56] concerns ﬁnding binary-alphabet Turing machines with n states that, when given an input tape of all 0s, write the largest number of 1s on the tape upon halting. For each n, a machine that achieves this is called an n-state Busy Beaver (or BB-n for short). Note that this deﬁnition only requires the machines to halt on all-0 inputs, leaving the behavior on other inputs unspeciﬁed and allowing them not to halt in general. Michel [31] observed that for n ∈{2, 3, 4}, the busy beaver machines are all total Turing machines, i.e., they halt on all inputs, and moreover proved that they all simulate some generalized Collatz function. It is an open problem whether all busy beavers are total Turing machines. In particular, it is unknown whether the current BB-5 candidate is total. Michel showed that the BB-5 candidate simulates the following generalized Collatz function. 5n+18 ⎪ if n ≡ 0 (mod 3) 5n+22 B(n) = if n ≡ 1 (mod 3) ⊥ if n ≡ 2 (mod 3) Convergence of the above function can be studied via the termination of a corresponding rewriting system, although the translation is not as straightforward as the other generalized Collatz functions we have in this paper. Speciﬁcally, the mixed base scheme results in a compact rewriting system only when all the mappings an + b → cn + d appliedbythe 123 Automated Approach to Collatz Conjecture Page 41 of 44 15 generalized Collatz function at hand satisfy d < c. This is not the case for the function B above since it requires us to express 3n → 5n + 6and 3n + 1 → 5n + 9. These mappings are expressed more easily by the help of unary representations, so we can have the following hybrid rewriting system BB over the alphabet {i, v, 0, , } to simulate the function B, where the new symbol v has the functional view v(x ) = 5x. 0 → ivi 0iii → i0 ii → 0 0i → iviiii iv → viiiii v → 0ii 0v → v0 We did not succeed in proving the termination of this rewriting system, which is not too surprising since the hybrid scheme does not even pass the test of proving the convergence of W . Alternatively, we can split the cases of B further for the congruence classes modulo 3 with k > 1 until the iterated application of B can either be expressed as an + b → cn + d with d < c, or it reaches ⊥. After we perform this procedure while ensuring that the number of newly introduced cases are kept to a minimum, we end up with the following mappings to simulate B in an accelerated manner (similar to the idea in Section 4.4). 9n → 25n + 16 9n + 1 → 25n + 21 27n + 6 → 125n + 64 27n + 7 → 125n + 71 (11) 27n + 16 → 125n + 114 81n + 51 → 625n + 459 243n + 78 → 3125n + 1116 243n + 159 → 3125n + 2159 Consider the symbols {0, 1, 2, v, w, x, y, z, , } with the following functional views. v(x ) = 5x 0(x ) = 3x w(x ) = 5x + 1 (x ) = 0 1(x ) = 3x + 1 x(x ) = 5x + 2 (x ) = x 2(x ) = 3x + 2 y(x ) = 5x + 3 z(x ) = 5x + 4 With these symbols, we have the following mixed {3, 5}-ary (ternary–quinary) system BB the termination of which is equivalent to the convergence of B. The dynamic rules on the left implement the mappings from (11) and the rest are auxiliary rules that push ternary symbols towards the rightmost end of the string while preserving its value. We were unable to prove the termination of this system, so we include it as yet another challenge for automated termination proving. 00 → yw 0v → v0 1v → w2 2v → y1 v → 0 01 → zw 0w → v1 1w → x0 2w → y2 w → 1 020 → xxz 0x → v2 1x → x1 2x → z0 x → 2 021 → xzw 0y → w0 1y → x2 2y → z1 y → 10 121 → zxz 0z → w1 1z → y0 2z → z2 z → 11 1220 → yywz 02220 → wyzyw 12220 → yxwwz 123 15 Page 42 of 44 E. Yolcu et al. C.3 Ternary Expansions of 2 Erdos ˝ [57] asked: When does the ternary expansion of 2 omit the digit 2? This is the case 0 2 8 for 2 = (1) ,2 = (11) ,and 2 = (100111) . He conjectured that it does not happen 3 3 3 for n > 8. This conjecture can be reformulated as the statement that the following rewriting ← − system E,where X ={r → | → r ∈ X }, is terminating on all initial strings of the form 8 + f f . ⎧ ⎫ 0 → 0f → f0 1t → t0 t → 0 ⎨ ⎬ ← − 1 → 0t → f1 2f → t1 ff → 1 X = ⎩ ⎭ → 1f → f2 2t → t2 ft → 2 Given a string that corresponds to the binary representation of a power of 2, the inverted ← − system X essentially rewrites the string into ternary by pushing ternary symbols to the right without altering the value that the string represents. The two rules {0 → , 1 → } remove the occurrences of the ternary digits 0 and 1 (but not 2). If the ternary expansion does not contain the digit 2 then all digits will be removed, resulting in the string that can then be rewritten to itself indeﬁnitely. This problem, as described, is an instance of “local termination” [58] since it is concerned with termination on not all possible strings but a subset of them. We have not performed experiments with this system or local termination yet and we leave this for future work. References 1. Lagarias, J.C.: The Ultimate Challenge: The 3x +1 Problem. American Mathematical Society, Providence (2010) 2. Lagarias, J.C.: The 3x + 1 Problem: An Annotated Bibliography (1963–1999). arXiv:math/0309224 (2011) 3. Lagarias, J.C.: The 3x + 1 Problem: An Annotated Bibliography, II (2000–2009). arXiv:math/0608208 (2012) 4. Tao, T.: Almost All Orbits of the Collatz Map Attain Almost Bounded Values. arXiv:1909.03562 (2020) 5. Barina, D.: Convergence veriﬁcation of the Collatz problem. The Journal of Supercomputing 77(3), 2681–2688 (2021). https://doi.org/10.1007/s11227-020-03368-x 6. Lagarias, J.C.: The 3x + 1 problem and its generalizations. The American Mathematical Monthly 92(1), 3–23 (1985). https://doi.org/10.2307/2322189 7. Conway, J.H.: Unpredictable iterations. In: Proceedings of the Number Theory Conference (University of Colorado, Boulder, Colorado), pp. 49–52 (1972) 8. Kurtz, S.A., Simon, J.: The undecidability of the generalized Collatz problem. In: Proceedings of the 4th International Conference on Theory and Applications of Models of Computation (TAMC). Lecture Notes in Computer Science, pp. 542–553. Springer, New York (2007). https://doi.org/10.1007/978-3- 540-72504-6_49 9. Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 328–342. Springer, New York (2006). https://doi.org/10.1007/11805618_25 10. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning 40(2), 195–220 (2008). https://doi.org/10.1007/s10817-007-9087-9 11. Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybernetica 19(2), 357–392 (2009) 12. Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certiﬁcation of termination and complex- ity proofs. In: Proceedings of the 25th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 441–455. Springer, New York (2014). https://doi.org/10. 1007/978-3-319-08918-8_30 13. Zantema, H.: Termination of string rewriting proved automatically. Journal of Automated Reasoning 34(2), 105–139 (2005). https://doi.org/10.1007/s10817-005-6545-0 123 Automated Approach to Collatz Conjecture Page 43 of 44 15 14. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8 15. Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisﬁability. IEEE Transactions on Computers 48(5), 506–521 (1999). https://doi.org/10.1109/12.769433 16. Yolcu, E., Aaronson, S., Heule, M.J.H.: An automated approach to the Collatz conjecture. In: Proceedings of the 28th Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, pp. 468– 484. Springer, New York (2021). https://doi.org/10.1007/978-3-030-79876-5_27 17. Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993). https://doi.org/10.1007/978- 1-4613-9771-7 18. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https://doi.org/10.1017/CBO9781139172752 19. Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17(1), 23–50 (1994). https://doi.org/10.1006/jsco.1994.1003 20. Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. Journal of Automated Reasoning 58(1), 3–31 (2017). https:// doi.org/10.1007/s10817-016-9388-y 21. Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: Proceedings of the 15th Interna- tional Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 85–94. Springer, New York (2004). https://doi.org/10.1007/978-3-540-25979-4_6 22. Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 295–304. Springer, New York (2009). https://doi.org/10.1007/978-3-642-02348- 4_21 23. Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretation. In: Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM). Lecture Notes in Computer Science, pp. 283–295. Springer, New York (2010). https://doi.org/10.1007/978-3-642-11266- 9_24 24. rn Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewrit- ing. In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA). Leibniz International Proceedings in Informatics, pp. 251–266. Schloss Dagstuhl, Wadern (2011). https://doi.org/10.4230/LIPIcs.RTA.2011.251 25. Bak, P., Tang, C., Wiesenfeld, K.: Self-organized criticality: An explanation of the 1/ f noise. Physical Review Letters 59(4), 381–384 (1987). https://doi.org/10.1103/PhysRevLett.59.381 26. Rawsthorne, D.A.: Imitation of an iteration. Mathematics Magazine 58(3), 172–176 (1985). https://doi. org/10.2307/2689917 27. Wagon, S.: The Collatz problem. The Mathematical Intelligencer 7(1), 72–76 (1985). https://doi.org/10. 1007/BF03023011 28. Buttsworth, R.N., Matthews, K.R.: On some Markov matrices arising from the generalized Collatz map- ping. Acta Arithmetica 55(1), 43–57 (1990). https://doi.org/10.4064/aa-55-1-43-57 29. Kašcák, ˇ F.: Small universal one-state linear operator algorithm. In: Proceedings of the 17th International Symposium on Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science, pp. 327–335. Springer, New York (1992). https://doi.org/10.1007/3-540-55808-X_31 30. Kohl, S.: Wildness of iteration of certain residue-class-wise afﬁne mappings. Advances in Applied Math- ematics 39(3), 322–328 (2007). https://doi.org/10.1016/j.aam.2006.08.003 31. Michel, P.: Problems in number theory from busy beaver competition. Logical Methods in Computer Science 11(4:10), (2015). https://doi.org/10.2168/LMCS-11(4:10)2015 32. Reutenauer, C., Berstel, J.: Noncommutative Rational Series with Applications. Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9780511760860 33. Soittola, M.: Positive rational sequences. Theoretical Computer Science 2(3), 317–322 (1976). https:// doi.org/10.1016/0304-3975(76)90084-0 34. Cantor, G.: Über einfache zahlensysteme. Zeitschrift für Mathematik und Physik 14, 121–128 (1869) 35. Sabel, D., Zantema, H.: Termination of cycle rewriting by transformation and matrix interpretation. Logical Methods in Computer Science 13(1:11), (2017). https://doi.org/10.23638/LMCS-13(1:11)2017 36. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006). https://doi.org/10.1007/s10817-006-9057-7 37. Farkas, H.M.: Variants of the 3N + 1 conjecture and multiplicative semigroups. In: Geometry, Spec- tral Theory, Groups, and Dynamics. Contemporary Mathematics, pp. 121–127. American Mathematical Society, Providence (2005). https://doi.org/10.1090/conm/387/07238 123 15 Page 44 of 44 E. Yolcu et al. 38. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: In: Proceedings of the 3rd International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 167–177. Springer, New York (1989). https://doi.org/10.1007/3-540-51081- 8_107 39. Denend, M.: Challenging variants of the Collatz conjecture. Master’s thesis, University of Texas at Austin (2018). https://doi.org/10.26153/tsw/1559 40. Applegate, D., Lagarias, J.C.: Lower bounds for the total stopping time of 3x + 1 iterates. Mathematics of Computation 72(242), 1035–1049 (2003). https://doi.org/10.1090/S0025-5718-02-01425-4 41. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proceedings of the 6th International Conference on Theory and Applications of Satisﬁability Testing (SAT). Lecture Notes in Computer Science, pp. 502–518. Springer, New York (2004). https://doi.org/10.1007/978-3-540-24605-3_37 42. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efﬁcient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC), pp. 530–535. Association for Computing Machinery, New York (2001). https://doi.org/10.1145/378239.379017 43. Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisﬁability solvers. In: Proceedings of the 10th International Conference on Theory and Applications of Satisﬁability Testing (SAT). Lecture Notes in Computer Science, pp. 294–299. Springer, New York (2007). https://doi.org/10. 1007/978-3-540-72788-0_28 44. Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling ﬁnite linear CSP into SAT. Constraints 14(2), 254–272 (2009). https://doi.org/10.1007/s10601-008-9061-0 45. Petke, J., Jeavons, P.: The order encoding: From tractable CSP to tractable SAT. In: Proceedings of the 14th International Conference on Theory and Applications of Satisﬁability Testing (SAT). Lecture Notes in Computer Science, pp. 371–372. Springer, New York (2011). https://doi.org/10.1007/978-3-642-21581- 0_34 46. Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisﬁability and constraint satisfaction problems. Journal of Automated Reasoning 24(1), 67–100 (2000). https://doi.org/10.1023/ A:1006314320276 47. Davis, M., Putnam, H.: A computing procedure for quantiﬁcation theory. Journal of the ACM 7(3), 201–215 (1960). https://doi.org/10.1145/321033.321034 48. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962). https://doi.org/10.1145/368273.368557 49. Biere, A.: CaDiCaL at the SAT Race 2019. In: Proceedings of the SAT Race 2019: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, pp. 8–9. University of Helsinki, Helsinki (2019) 50. Scollo, G.: ω-rewriting the Collatz problem. Fundamenta Informaticae 64(1–4), 405–416 (2005) 51. Post, E.L.: Formal reductions of the general combinatorial decision problem. American Journal of Math- ematics 65(2), 197–215 (1943). https://doi.org/10.2307/2371809 52. De Mol, L.: Tag systems and Collatz-like functions. Theoretical Computer Science 390(1), 92–101 (2008). https://doi.org/10.1016/j.tcs.2007.10.020 53. Kari, J.: Cellular automata, the Collatz conjecture and powers of 3/2. In: Proceedings of the 16th Inter- national Conference on Developments in Language Theory (DLT). Lecture Notes in Computer Science, pp. 40–49. Springer, New York (2012). https://doi.org/10.1007/978-3-642-31653-1_5 54. Kauffman, L.H.: Arithmetic in the form. Cybernetics and Systems 26(1), 1–57 (1995). https://doi.org/10. 1080/01969729508927486 55. Mahler, K.: An unsolved problem on the powers of 3/2. Journal of the Australian Mathematical Society 8(2), 313–321 (1968). https://doi.org/10.1017/S1446788700005371 56. Radó, T.: On non-computable functions. The Bell System Technical Journal 41(3), 877–884 (1962). https://doi.org/10.1002/j.1538-7305.1962.tb00480.x 57. Erdos, ˝ P.: Some unconventional problems in number theory. Mathematics Magazine 52(2), 67–70 (1979). https://doi.org/10.2307/2689842 58. Waldmann, J., de Vrijer, R., Endrullis, J.: Local termination: Theory and practice. Logical Methods in Computer Science 6(3:20), (2010). https://doi.org/10.2168/LMCS-6(3:20)2010 Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional afﬁliations.

Journal

Journal of Automated Reasoning – Springer Journals

Published: Jun 1, 2023

Keywords: String rewriting; Termination; Matrix interpretations; SAT solving; Collatz conjecture; Computer-assisted mathematics

Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

An Automated Approach to the Collatz Conjecture

An Automated Approach to the Collatz Conjecture

Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

An Automated Approach to the Collatz Conjecture

An Automated Approach to the Collatz Conjecture

References (74)

Abstract

Journal

Recommended Articles

There are no references for this article.

Our policy towards the use of cookies