Mechanical Proving with Walnut for Squares and Cubes in Partial Words

Author John Machacek

Thumbnail PDF


  • Filesize: 0.66 MB
  • 11 pages

Document Identifiers

Author Details

John Machacek
  • Department of Mathematics, University of Oregon, Eugene, OR, USA

Cite AsGet BibTex

John Machacek. Mechanical Proving with Walnut for Squares and Cubes in Partial Words. In 33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 223, pp. 5:1-5:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Walnut is a software that can prove theorems in combinatorics on words about automatic sequences. We are able to apply this software to both prove new results as well as reprove some old results on avoiding squares and cubes in partial words. We also define the notion of an antisquare in a partial word and begin the study of binary partial words which contain only a fixed number of distinct squares and antisquares.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorics on words
  • Partial words
  • squares
  • antisquares
  • cubes
  • Walnut


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


  1. Jean-Paul Allouche and Jeffrey Shallit. Automatic sequences. Cambridge University Press, Cambridge, 2003. Theory, applications, generalizations. URL:
  2. Jean Berstel. Axel thue’s papers on repetitions in words: a translation. Publications de Laboratoire de Combinatoire et d’Informatique Mathématique 20, Université du Québec á Montréal, 1995. Google Scholar
  3. Kevin Black, Francine Blanchet-Sadri, Ian Coley, Brent Woodhouse, and Andrew Zemke. Pattern avoidance in partial words dense with holes. J. Autom. Lang. Comb., 22(4):209-241, 2017. URL:
  4. F. Blanchet-Sadri, Ilkyoo Choi, and Robert Mercaş. Avoiding large squares in partial words. Theoret. Comput. Sci., 412(29):3752-3758, 2011. URL:
  5. F. Blanchet-Sadri, James D. Currie, Narad Rampersad, and Nathan Fox. Abelian complexity of fixed point of morphism 0→012, 1→02, 2→1. Integers, 14:Paper No. A11, 17, 2014. Google Scholar
  6. F. Blanchet-Sadri, Yang Jiao, John M. Machacek, J. D. Quigley, and Xufan Zhang. Squares in partial words. Theoret. Comput. Sci., 530:42-57, 2014. URL:
  7. F. Blanchet-Sadri, Robert Mercaş, and Geoffrey Scott. Counting distinct squares in partial words. Acta Cybernet., 19(2):465-477, 2009. Google Scholar
  8. Francine Blanchet-Sadri, Kevin Black, and Andrew Zemke. Unary pattern avoidance in partial words dense with holes. In Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications - 5th International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011. Proceedings, volume 6638 of Lecture Notes in Computer Science, pages 155-166. Springer, 2011. URL:
  9. R. C. Entringer, D. E. Jackson, and J. A. Schatz. On nonrepetitive sequences. J. Combinatorial Theory Ser. A, 16:159-164, 1974. URL:
  10. Gabriele Fici, Antonio Restivo, Manuel Silva, and Luca Q. Zamboni. Anti-powers in infinite words. J. Combin. Theory Ser. A, 157:109-119, 2018. URL:
  11. Daniel Gabric and Jeffrey Shallit. The simplest binary word with only three squares. RAIRO Theor. Inform. Appl., 55:Paper No. 3, 7, 2021. URL:
  12. Vesa Halava, Tero Harju, and Tomi Kärki. On the number of squares in partial words. RAIRO Theor. Inform. Appl., 44(1):125-138, 2010. URL:
  13. M. Lothaire. Combinatorics on words. Cambridge Mathematical Library. Cambridge University Press, Cambridge, 1997. URL:
  14. John Machacek. Partial words with a unique position starting a square. Inform. Process. Lett., 145:44-47, 2019. URL:
  15. Hamoon Mousavi. Automatic theorem proving in Walnut. URL:
  16. Hamoon Mousavi, Luke Schaeffer, and Jeffrey Shallit. Decision algorithms for Fibonacci-automatic words, I: Basic results. RAIRO Theor. Inform. Appl., 50(1):39-66, 2016. URL:
  17. Tim Ng, Pascal Ochem, Narad Rampersad, and Jeffrey Shallit. New results on pseudosquare avoidance. In Combinatorics on words, volume 11682 of Lecture Notes in Comput. Sci., pages 264-274. Springer, Cham, 2019. URL:
  18. Narad Rampersad, Jeffrey Shallit, and Ming-wei Wang. Avoiding large squares in infinite binary words. Theoret. Comput. Sci., 339(1):19-34, 2005. URL:
  19. Michaël Rao, Michel Rigo, and Pavel Salimov. Avoiding 2-binomial squares and cubes. Theoret. Comput. Sci., 572:83-91, 2015. URL:
  20. Axel Thue. Selected mathematical papers. Universitetsforlaget, Oslo, 1977. With an introduction by Carl Ludwig Siegel and a biography by Viggo Brun, Edited by Trygve Nagell, Atle Selberg, Sigmund Selberg, and Knut Thalberg. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail