An Automated Approach to the Collatz Conjecture
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...
Main Authors: | , , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | unknown |
Published: |
arXiv
2021
|
Subjects: | |
Online Access: | https://dx.doi.org/10.48550/arxiv.2105.14697 https://arxiv.org/abs/2105.14697 |
id |
ftdatacite:10.48550/arxiv.2105.14697 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.48550/arxiv.2105.14697 2023-05-15T15:04:10+02:00 An Automated Approach to the Collatz Conjecture Yolcu, Emre Aaronson, Scott Heule, Marijn J. H. 2021 https://dx.doi.org/10.48550/arxiv.2105.14697 https://arxiv.org/abs/2105.14697 unknown arXiv Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 CC-BY Logic in Computer Science cs.LO FOS Computer and information sciences Article CreativeWork article Preprint 2021 ftdatacite https://doi.org/10.48550/arxiv.2105.14697 2022-03-10T14:30:07Z 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 matrix interpretations. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses matrix/arctic interpretations and we find automated proofs of nontrivial weakenings of the Collatz conjecture. Finally, we adapt our rewriting system to show that other open problems in mathematics can also be approached as termination problems for relatively small rewriting systems. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach. Article in Journal/Newspaper Arctic DataCite Metadata Store (German National Library of Science and Technology) Arctic |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
unknown |
topic |
Logic in Computer Science cs.LO FOS Computer and information sciences |
spellingShingle |
Logic in Computer Science cs.LO FOS Computer and information sciences Yolcu, Emre Aaronson, Scott Heule, Marijn J. H. An Automated Approach to the Collatz Conjecture |
topic_facet |
Logic in Computer Science cs.LO FOS Computer and information sciences |
description |
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 matrix interpretations. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses matrix/arctic interpretations and we find automated proofs of nontrivial weakenings of the Collatz conjecture. Finally, we adapt our rewriting system to show that other open problems in mathematics can also be approached as termination problems for relatively small rewriting systems. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach. |
format |
Article in Journal/Newspaper |
author |
Yolcu, Emre Aaronson, Scott Heule, Marijn J. H. |
author_facet |
Yolcu, Emre Aaronson, Scott Heule, Marijn J. H. |
author_sort |
Yolcu, Emre |
title |
An Automated Approach to the Collatz Conjecture |
title_short |
An Automated Approach to the Collatz Conjecture |
title_full |
An Automated Approach to the Collatz Conjecture |
title_fullStr |
An Automated Approach to the Collatz Conjecture |
title_full_unstemmed |
An Automated Approach to the Collatz Conjecture |
title_sort |
automated approach to the collatz conjecture |
publisher |
arXiv |
publishDate |
2021 |
url |
https://dx.doi.org/10.48550/arxiv.2105.14697 https://arxiv.org/abs/2105.14697 |
geographic |
Arctic |
geographic_facet |
Arctic |
genre |
Arctic |
genre_facet |
Arctic |
op_rights |
Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 |
op_rightsnorm |
CC-BY |
op_doi |
https://doi.org/10.48550/arxiv.2105.14697 |
_version_ |
1766335983009136640 |