An automated approach to the Collatz conjecture. (English) Zbl 07702721
Summary: 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 find 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.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Keywords:
string rewriting; termination; matrix interpretations; SAT solving; Collatz conjecture; computer-assisted mathematicsOnline Encyclopedia of Integer Sequences:
a(n) = (n-1)/3 if n mod 3 = 1; a(n) = n/2 if n mod 6 = 0 or n mod 6 = 2; a(n) = (3n+1)/2 if n mod 6 = 3 or n mod 6 = 5.Irregular triangle T(n,k) read by rows in which row n lists the iterates of the A350515 map from n to 0.
References:
| [1] | Lagarias, J.C.: The Ultimate Challenge: The \(3x+1\) Problem. American Mathematical Society, Providence (2010) · Zbl 1253.11003 |
| [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 verification of the Collatz problem, The Journal of Supercomputing, 77, 3, 2681-2688 (2021) · doi:10.1007/s11227-020-03368-x |
| [6] | Lagarias, JC, The \(3x+1\) problem and its generalizations, The American Mathematical Monthly, 92, 1, 3-23 (1985) · Zbl 0566.10007 · doi: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) · Zbl 0337.10041 |
| [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). doi:10.1007/978-3-540-72504-6_49 · Zbl 1198.03043 |
| [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). doi:10.1007/11805618_25 · Zbl 1151.68447 |
| [10] | Endrullis, J.; Waldmann, J.; Zantema, H., Matrix interpretations for proving termination of term rewriting, Journal of Automated Reasoning, 40, 2, 195-220 (2008) · Zbl 1139.68049 · doi: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) · Zbl 1224.68041 |
| [12] | Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certification of termination and complexity 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). doi:10.1007/978-3-319-08918-8_30 · Zbl 1416.68180 |
| [13] | Zantema, H., Termination of string rewriting proved automatically, Journal of Automated Reasoning, 34, 2, 105-139 (2005) · Zbl 1102.68649 · doi:10.1007/s10817-005-6545-0 |
| [14] | Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theoretical Computer Science, 236, 1, 133-178 (2000) · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8 |
| [15] | Marques-Silva, JP; Sakallah, KA, GRASP: A search algorithm for propositional satisfiability, IEEE Transactions on Computers, 48, 5, 506-521 (1999) · Zbl 1392.68388 · doi: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). doi:10.1007/978-3-030-79876-5_27 · Zbl 1540.68116 |
| [17] | Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993). doi:10.1007/978-1-4613-9771-7 · Zbl 0832.68061 |
| [18] | Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). doi:10.1017/CBO9781139172752 · Zbl 0948.68098 |
| [19] | Zantema, H., Termination of term rewriting: Interpretation and type elimination, Journal of Symbolic Computation, 17, 1, 23-50 (1994) · Zbl 0810.68087 · doi: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) · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [21] | Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 85-94. Springer, New York (2004). doi: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). doi: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). doi:10.1007/978-3-642-11266-9_24 · Zbl 1274.68148 |
| [24] | rn Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. 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). doi:10.4230/LIPIcs.RTA.2011.251 · Zbl 1236.68141 |
| [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) · doi:10.1103/PhysRevLett.59.381 |
| [26] | Rawsthorne, DA, Imitation of an iteration, Mathematics Magazine, 58, 3, 172-176 (1985) · Zbl 0587.10030 · doi:10.2307/2689917 |
| [27] | Wagon, S., The Collatz problem, The Mathematical Intelligencer, 7, 1, 72-76 (1985) · Zbl 0566.10008 · doi:10.1007/BF03023011 |
| [28] | Buttsworth, RN; Matthews, KR, On some Markov matrices arising from the generalized Collatz mapping, Acta Arithmetica, 55, 1, 43-57 (1990) · Zbl 0653.10004 · doi:10.4064/aa-55-1-43-57 |
| [29] | Kaščá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). doi:10.1007/3-540-55808-X_31 · Zbl 1493.68392 |
| [30] | Kohl, S., Wildness of iteration of certain residue-class-wise affine mappings, Advances in Applied Mathematics, 39, 3, 322-328 (2007) · Zbl 1146.11015 · doi: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). doi:10.2168/LMCS-11(4:10)2015 · Zbl 1448.03028 |
| [32] | Reutenauer, C., Berstel, J.: Noncommutative Rational Series with Applications. Cambridge University Press, Cambridge (2010). doi:10.1017/CBO9780511760860 · Zbl 1250.68007 |
| [33] | Soittola, M., Positive rational sequences, Theoretical Computer Science, 2, 3, 317-322 (1976) · Zbl 0341.68056 · doi:10.1016/0304-3975(76)90084-0 |
| [34] | Cantor, G., Über einfache zahlensysteme, Zeitschrift für Mathematik und Physik, 14, 121-128 (1869) · JFM 02.0085.01 |
| [35] | Sabel, D., Zantema, H.: Termination of cycle rewriting by transformation and matrix interpretation. Logical Methods in Computer Science 13(1:11), (2017). doi:10.23638/LMCS-13(1:11)2017 · Zbl 1398.68281 |
| [36] | Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S., Mechanizing and improving dependency pairs, Journal of Automated Reasoning, 37, 3, 155-203 (2006) · Zbl 1113.68088 · doi:10.1007/s10817-006-9057-7 |
| [37] | Farkas, H.M.: Variants of the \(3N+1\) conjecture and multiplicative semigroups. In: Geometry, Spectral Theory, Groups, and Dynamics. Contemporary Mathematics, pp. 121-127. American Mathematical Society, Providence (2005). doi:10.1090/conm/387/07238 · Zbl 1120.11014 |
| [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). doi:10.1007/3-540-51081-8_107 · Zbl 1503.68116 |
| [39] | Denend, M.: Challenging variants of the Collatz conjecture. Master’s thesis, University of Texas at Austin (2018). doi:10.26153/tsw/1559 |
| [40] | Applegate, D.; Lagarias, JC, Lower bounds for the total stopping time of \(3x+1\) iterates, Mathematics of Computation, 72, 242, 1035-1049 (2003) · Zbl 1052.11017 · doi: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 Satisfiability Testing (SAT). Lecture Notes in Computer Science, pp. 502-518. Springer, New York (2004). doi:10.1007/978-3-540-24605-3_37 |
| [42] | Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC), pp. 530-535. Association for Computing Machinery, New York (2001). doi:10.1145/378239.379017 |
| [43] | Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, pp. 294-299. Springer, New York (2007). doi:10.1007/978-3-540-72788-0_28 |
| [44] | Tamura, N.; Taga, A.; Kitagawa, S.; Banbara, M., Compiling finite linear CSP into SAT, Constraints, 14, 2, 254-272 (2009) · Zbl 1186.68076 · doi: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 Satisfiability Testing (SAT). Lecture Notes in Computer Science, pp. 371-372. Springer, New York (2011). doi:10.1007/978-3-642-21581-0_34 |
| [46] | Gomes, CP; Selman, B.; Crato, N.; Kautz, H., Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, Journal of Automated Reasoning, 24, 1, 67-100 (2000) · Zbl 0967.68145 · doi:10.1023/A:1006314320276 |
| [47] | Davis, M.; Putnam, H., A computing procedure for quantification theory, Journal of the ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203 · doi: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) · Zbl 0217.54002 · doi: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., \( \omega \)-rewriting the Collatz problem, Fundamenta Informaticae, 64, 1-4, 405-416 (2005) · Zbl 1102.68051 |
| [51] | Post, EL, Formal reductions of the general combinatorial decision problem, American Journal of Mathematics, 65, 2, 197-215 (1943) · Zbl 0063.06327 · doi:10.2307/2371809 |
| [52] | De Mol, L., Tag systems and Collatz-like functions, Theoretical Computer Science, 390, 1, 92-101 (2008) · Zbl 1134.68024 · doi: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 International Conference on Developments in Language Theory (DLT). Lecture Notes in Computer Science, pp. 40-49. Springer, New York (2012). doi:10.1007/978-3-642-31653-1_5 · Zbl 1358.68208 |
| [54] | Kauffman, LH, Arithmetic in the form, Cybernetics and Systems, 26, 1, 1-57 (1995) · Zbl 0827.03033 · doi: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) · Zbl 0155.09501 · doi:10.1017/S1446788700005371 |
| [56] | Radó, T., On non-computable functions, The Bell System Technical Journal, 41, 3, 877-884 (1962) · Zbl 1497.68176 · doi:10.1002/j.1538-7305.1962.tb00480.x |
| [57] | Erdős, P., Some unconventional problems in number theory, Mathematics Magazine, 52, 2, 67-70 (1979) · Zbl 0407.10001 · doi: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). doi:10.2168/LMCS-6(3:20)2010 · Zbl 1211.68085 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
