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.
翻译:我们通过终止字符串重写的透镜探索科拉茨猜想及其变体。 我们构建了一个重写系统, 模拟在字符串上反复应用科拉兹函数, 与正数的混合双向式整数相匹配; 我们证明这一重写系统的终止相当于科拉茨猜想。 我们还证明, 先前研究过的利用非隐含式表示模拟科拉茨函数的重写系统, 不通过自然矩阵解释来接受终止证明, 即使与依赖性对口同时使用。 为了展示我们在数学上证明有趣的说明方法的可行性, 我们实施了一个最小的终止证明, 使用自然/ 弧式矩阵解释, 并找到自动证明科拉茨猜想非三角体弱化的证明。 虽然我们没有成功证明科拉茨猜想, 但我们认为, 这里的想法是一个有趣的新方法。