Document

Lagrange's Theorem for Binary Squares

File

LIPIcs.MFCS.2018.18.pdf
• Filesize: 448 kB
• 14 pages

Cite As

P. Madhusudan, Dirk Nowotka, Aayush Rajasekaran, and Jeffrey Shallit. Lagrange's Theorem for Binary Squares. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.MFCS.2018.18

Abstract

We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. Here the number 4 is optimal. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.

Subject Classification

ACM Subject Classification
• Theory of computation → Models of computation
• Theory of computation → Constructive mathematics
• Mathematics of computing → Discrete mathematics
Keywords
• binary square
• theorem-proving
• finite automaton
• decision procedure
• decidable theory

Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

References

1. W. D. Banks. Every natural number is the sum of forty-nine palindromes. INTEGERS - Electronic J. Combinat. Number Theory, 16, 2016. #A3.
2. J. Cilleruelo, F. Luca, and L. Baxter. Every positive integer is a sum of three palindromes. Math. Comp., 2017. Published electronically at URL: http://dx.doi.org/10.1090/mcom/3221.
3. R. C. Crocker. On the sum of two squares and two powers of k. Colloq. Math., 112:235-267, 2008.
4. W. J. Ellison. Waring’s problem. Amer. Math. Monthly, 78:10-36, 1971.
5. E. Grosswald. Representations of Integers as Sums of Squares. Springer-Verlag, 1985.
6. M. Heizmann, D. Dietsch, M. Greitschus, J. Leike, B. Musa, C. Schätzle, and A. Podelski. Ultimate automizer with two-track proofs. In M. Chechik and J.-F. Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pages 950-953. Springer-Verlag, 2016.
7. M. Heizmann, J. Hoenicke, and A. Podelski. Software model checking for people who love automata. In N. Sharygina and H. Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, volume 8044 of Lecture Notes in Computer Science, pages 36-52. Springer-Verlag, 2013.
8. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.
9. D. M. Kane, C. Sanna, and J. Shallit. Waring’s theorem for binary powers. Preprint, available at https://arxiv.org/abs/1801.04483, 2018.
10. J.-L. Lagrange. Démonstration d'un théoréme d'arithmétique. Nouv. Mém. Acad. Roy. Sc. de Berlin, pages 123-133, 1770. Also in Oeuvres de Lagrange, 3 (1869), pp. 189-201.
11. C. J. Moreno and S. S. Wagstaff, Jr. Sums of Squares of Integers. Chapman and Hall/CRC, 2005.
12. M. B. Nathanson. Additive Number Theory: The Classical Bases. Springer-Verlag, 1996.
13. M. B. Nathanson. Elementary Methods in Number Theory. Springer-Verlag, 2000.
14. D. Platt and T. Trudgian. On the sum of two squares and at most two powers of 2. Preprint, available at https://arxiv.org/abs/1610.01672, 2016.
15. A. Rajasekaran. Using automata theory to solve problems in additive number theory. Master’s thesis, School of Computer Science, University of Waterloo, 2018.
16. A. Rajasekaran, J. Shallit, and T. Smith. Sums of palindromes: an approach via nested-word automata. Preprint, available at https://arxiv.org/abs/1706.10206, 2017.
17. A. Rajasekaran, J. Shallit, and T. Smith. Sums of palindromes: an approach via automata. In R. Niedermeier and B. Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), Leibniz International Proceedings in Informatics, pages 54:1-54:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
18. N. J. A. Sloane. The on-line encyclopedia of integer sequences. Available at https://oeis.org, 2016.
19. C. Small. Waring’s problem. Math. Mag., 50:12-16, 1977.
20. R. C. Vaughan. The Hardy–Littlewood Method, volume 125 of Cambridge Tracts in Mathematics. Cambridge University Press, 2nd edition, 1997.
21. R. C. Vaughan and T. Wooley. Waring’s problem: a survey. In M. A. Bennett, B. C. Berndt, N. Boston, H. G. Diamond, A. J. Hildebrand, and W. Philipp, editors, Number Theory for the Millennium. III, pages 301-340. A. K. Peters, 2002.
X

Feedback for Dagstuhl Publishing

Feedback submitted

Could not send message

Please try again later or send an E-mail