Walnut is free software, written in Java, for
deciding first-order statements phrased in an extension of
Presburger arithmetic, called Buchi arithmetic. It
can be used to prove hundreds of results in combinatorics
on words, number theory, and other areas of discrete
mathematics. It can handle a wide variety of problems. There are some recent additions to Walnut, written by Aseem Baranwal,
Kai Hsiang Yang, and Anatoly Zavyalov.
News
March 27 2023
Walnut 5.4 is now available! It contains several new commands, including
the ability to do transductions of automatic sequences, and fixes one obscure
bug introduced in Walnut 3: namely, regular expressions with negative elements
could under some rare circumstances be interpreted incorrectly. This version
was modified by Anatoly Zavyalov. This version supersedes all previous versions.
The Walnut book is now available
from Cambridge University Press. Get your copy today!
August 15 2022
Walnut 4 is now available! It contains several
new and useful commands,
in particular for handling negative bases and quantification over Z
instead of N.
It is available for download here. This version incorporates new original work by Kai Hsiang Yang.
September 6 2021
Walnut 3 is now available! It contains several
new and useful commands.
It is available for download
here.
This version represents additional work done by Laindon C. Burnett
to the previous versions of Walnut written by Hamoon Mousavi and updated
by Aseem Raj Baranwal. For this version, you should type
java Main.Prover to get started, insted of the older
java Main.prover.
Installing Walnut
When you go to the github site above,
click on the green "Code" button, then choose "Download Zip".
When you get the zip file downloaded, you might (depending exactly one what system you use) just click on it
to extract it. Otherwise you might have to use a zip extractor.
Now you should have a directory called something like Walnut-main.
Go into that directory and there is a command called "build.sh".
Execute that command - on my Unix system you type
./build.sh
to do that.
That should take a few seconds to compile.
Then go to the "bin" directory and type
java Main.Prover
that gets you into Walnut. To leave, type quit;
Depending on your system, you may need a "Java Development Kit" to install
Walnut. If so, try the command
sudo apt install openjdk-11-jdk
from a terminal window. Once that is done, to compile Walnut,
go to the Walnut directory
and type
sh build-sh (Windows)
It might be that you can get by without the "sh" before the command,
depending on your system.
Or
./build-sh (Linux)
That should do it! Now you are ready to go to the "bin" directory
and type
java Main.Prover
Let me know if you have any difficulties.
Walnut Software
The old version of Walnut is available at github. For the new version, see above.
After you download it and install it, go to the directory
Walnut/bin and type java Main.prover to get started.
A manual of how to use it is available on the
arxiv.
There is also a text file with some
examples of
how to use Walnut.
Here is a video tutorial
on how to use Walnut:
Here is a talk, given on October 18 2022,
about how to use Walnut to prove properties of the
sequences in the OEIS:
If you are using Walnut under the Eclipse environment, here are a few tips.
Download the Walnut software. Start Eclipse up. Use the default
workspace. Open "Project" from the File choices, and choose "Walnut".
Next, go to src/Main in the menu choices, right-click on prover.java
or Prover.java
and choose "Run As Java Application". You should now get a window where
you can enter Walnut commands. To see results, go to
the Eclipse file menu, right-click on "Result" and choose "Refresh" and
the results should be there. Thanks to Stepan Holub for this info.
Recently Walnut has been modified by Aseem Baranwal to handle the Pell
number system, and more generally, the Ostrowski number system based
on any quadratic irrational. To use this version of Walnut, visit
https://github.com/aseemrb/walnut. After you download and install it, go to the directory
Ostrowski/bin and type java Main.Prover to get started.
(Note: for the old Walnut, you use lowercase "p" in prover; for the
new version you use uppercase "P" in prover.)
The command "ost name [0 1 2] [3 4]", for example, defines
an Ostrowski number system for the continued fraction [0,1,2,3,4,3,4,3,4,...].
It can then be used by prefacing a query with "?msd_name" or "?lsd_name".
Aseem Baranwal has prepared a brief summary of his additions to
Walnut here.
If you find Walnut useful in your research, please be sure to cite
Hamoon Mousavi as the author of the software, and let me know what you
achieved with it.
Walnut has been used in a variety of papers and books. A partial list is here
(will be updated):
Nicolas Ollinger, Jeffrey Shallit,
The repetition threshold for Rote sequences,
Arxiv preprint arXiv:2406.17867 [math.CO], June 25 2024.
Available at https://arxiv.org/abs/2406.17867. There is some supplementary material, including
An html file with more information
about the computations
Olivier Carton, Jean-Michel Couvreur, Martin Delacourt, Nicolas Ollinger,
Addition in Dumont-Thomas Numeration Systems in Theory and Practice,
Arxiv preprint arXiv:2406.09868 [cs.FL], June 14 2024. Available
at https://arxiv.org/abs/2406.09868.
Jean-Paul Allouche, John M. Campbell, Jeffrey Shallit, Manon Stipulanti,
The reflection complexity of sequences over finite alphabets,
Arxiv preprint arXiv:2406:09302 [math.CO], June 13 2024.
Available at https://arxiv.org/abs/2406.09302.
J.-P. Allouche, N. Rampersad, and J. Shallit,
Repetition threshold for binary automatic sequences,
Arxiv preprint arXiv:2406.06513 [math.CO], June 10 2024. Available
at https://arxiv.org/abs/2406.06513.
To check the claims of the paper, you can use
the following Walnut code.
Code for checking that the morphisms in Table 1 generate
squarefree words by iteration: ARS-table1.txt
Code for checking cases k = 3,6 in Table 2: ARS-table2.txt
Fibonacci DFAO in Figure 1 to compute the sequence y,
put this in the Word Automata
directory of Walnut: Y2.txt
Code for checking squarefreeness of y
and computing h(y) in Remark 12:
ARS-remark12.txt
Fibonacci DFAO for the word w in Remark 12, put this in the
Word Automata directory of Walnut:
W.txt
Rob Burns,
Synchronisation of running sums of automatic sequences,
Arxiv preprint arXiv:2405.17536 [math.NT],
May 27 2024. Available at
https://arxiv.org/abs/2405.17536.
Aaron Barnoff, Curtis Bright, and Jeffrey Shallit,
Using finite automata to compute the base-b representation of the golden ratio and other quadratic irrationals,
Arxiv preprint arXiv:2405.02727 [cs.FL], May 4 2024. Available
at
https://arxiv.org/abs/2405.02727.
Marieh Jahannia and Manon Stipulanti,
Exploring the Crochemore and Ziv-Lempel factorizations of
some automatic sequences with the software Walnut,
Arxiv preprint arXiv:2403.15215 [cs.DM],
March 22 2024. Available at
https://arxiv.org/abs/2403.15215.
Jason Bell, Chris Schulz, and Jeffrey Shallit,
Consecutive Power Occurrences in Sturmian Words,
Arxiv preprint arXiv:2402.09597 [math.CO],
February 14 2024. Available at
https://arxiv.org/abs/2402.09597.
Luke Schaeffer, Jeffrey Shallit, and Stefan Zorcic,
Beatty Sequences for a Quadratic Irrational: Decidability and Applications,
Arxiv preprint arXiv:2402.08331 [math.NT],
February 13 2024. Available at
https://arxiv.org/abs/2402.08331.
X.txt, put in the Word Automata directory of Walnut
Y.txt, put in the Word Automata directory of Walnut
tar file of automata produced, unpack and put in the Automata Library directory of Walnut. These will be produced by
the commands above if you have enough RAM
on your machine and time to devote (about two weeks of computation time on a machine with 400G of RAM). But if you do not have this time you can just
work with the automata produced.
files for the sequences, unpack and
put all these files in the "Automata Library" of Walnut.
J. Shallit, Proving Results About OEIS Sequences with Walnut,
in C. Dubois and M. Kerber, eds., CICM 2023, LNAI Vol. 14101,
Springer, 2023, pp. 270-282.
L. Schaeffer and J. Shallit,
The first-order theory of binary overlap-free words is decidable,
Canad. J. Math. (2023).
There is a small error in the statement of Theorem 5.5.
It refers to all overlap-free words, but the theorem is actually about
all overlap-free Restivo words.
The definition for `normalize' was omitted.
You can download it here: normalize.txt.
The definition for `CODE' was omitted.
You can download it here: CODE.txt.
M. Rigo, M. Stipulanti, and M. A. Whiteland,
Automaticity and Parikh-collinear morphisms,
in A. Frid and R. Mercas, eds., WORDS 2023, LNCS 13899, Springer, 2023,
pp. 247-260.
J. Shallit,
Proving Properties of ϕ-Representations with the Walnut
Theorem-Prover, arxiv preprint arXiv:2305.02672 [math.NT],
May 4 2023. Available at
https://arxiv.org/abs/2305.02672.
J. Shallit and A. Zavyalov,
Transduction of automatic sequences and applications,
arxiv preprint arXiv:2303.15203 [cs.FL], March 27 2023. Available at
https://arxiv.org/abs/2303.15203.
RS4.txt; put this in the Word Automata
Library of Walnut
rss.txt; put this in the Automata Library
of Walnut
rst.txt; put this in the Automata Library
of Walnut
An abbreviated version of this paper appeared
in A. Frid and R. Mercas, eds., WORDS 2023, LNCS 13899, Springer, 2023,
pp. 233-246.
Jeffrey Shallit, Proof of a conjecture of Krawchuk and Rampersad,
arxiv preprint arXiv:2301.11473 [math.CO], January 27 2023.
Available at https://arxiv.org/abs/2301.11473.
R. Fokkink, G. F. Ortega, and D. Rust,
Corner the empress, Arxiv preprint arXiv:2204.11805 [math.CO], December 8 2022. Available at https://arxiv.org/abs/2204.11805.
Dominik Leon Jilg,
Frobeniuszahl ausgewählter Zahlenfolgen:
Analyse der Frobeniuszahl von synchronisierten Folgen und Folgen mit automatisierter charakteristischer Folge, Bachelor's thesis,
Lehrstuhl für Mathematik IV,
Julius-Maximilians-Universität Würzburg, Germany, August 12 2022.
Jeffrey Shallit,
The Logical Approach To Automatic Sequences: Exploring Combinatorics on Words with Walnut, London Math. Soc. Lecture Note Series,
Vol. 482,
Cambridge University
Press, September 29 2022.
Jeffrey Shallit,
Some Tribonacci conjectures,
arxiv preprint arXiv:2210.03996 [math.CO],
October 8 2022.
Here are the files for the automata you will need
in this paper. Put them in the "Automaton Library" of Walnut.
Aseem Baranwal, James Currie, Lucas Mol, Pascal Ochem,
Narad Rampersad, and Jeffrey Shallit,
Antisquares and
critical exponents,
arxiv preprint arXiv:2209.09223 [math.CO],
September 19 2022.
Jeffrey Shallit, Sonja Linghui Shan, and Kai Hsiang Yang,
Automatic Sequences in Negative Bases and Proofs of Some Conjectures of
Shevelev, arxiv preprint arXiv:2208.06025 [cs.FL], August 11 2022,
available at https://arxiv.org/abs/2208.06025. Appeared in
J. Shallit, S. L. Shan and K. H. Yang,
"Automatic sequences in negative bases and proofs of some
conjectures of Shevelev", RAIRO-Theor. Inf. Appl.57 (2023), 4.
Shuo Li, A note on the Lie complexity and beyond,
Arxiv preprint arXiv:2207.05859 [math.CO], July 12 2022, available at
https://arxiv.org/abs/2207.05859.
Golnaz Badkobeh, Tero Harju, Pascal Ochem, and Matthieu Rosenfeld,
Avoiding square-free words on free groups, Theoretical Computer Science
922 (2022) 206-217.
James Currie, Pascal Ochem, Narad Rampersad, and Jeffrey Shallit, Properties of a ternary infinite
word. Arxiv preprint arXiv:2206.01776 [cs.DM], June 3 2022.
Available at https://arxiv.org/abs/2206.01776.
To reproduce the calculations, first download the latest
version of Walnut
here.
Second, put the two files
R. Burns, Factorials and Legendre's three-square theorem: II,
arxiv preprint arXiv:2203.16469 [math.NT],
March 30 2022. Available at https://arxiv.org/abs/2203.16469.
J. Shallit, Note on a Fibonacci parity sequence,
arxiv preprint arXiv:2203.10504 [cs.FL], March 20 2022.
Available at https://arxiv.org/abs/2203.10504.
Appeared in J. Shallit,
Cryptography and Communications15 (2023), 309-315.
N. Rampersad, The periodic complexity function of the Thue-Morse word, the Rudin-Shapiro word, and the period-doubling word,
arxiv preprint arXiv:2112.04416, December 8 2021.
Available at https://arxiv.org/abs/2112.04416. Appeared in Australasian J. Combinatorics85 (2023), 150-158.
N. Rampersad, Prefixes of the Fibonacci word that end with a cube,
arxiv preprint arXiv:2111.09253, November 17 2021.
Available at https://arxiv.org/abs/2111.09253. Appeared as
N. Rampersad, Prefixes of the Fibonacci word,
C. R. Math. Acad. Sci. Paris361 (2023) 323-330.
J. Shallit, Intertwining of Complementary Thue-Morse Factors,
arxiv preprint arXiv:2203.02917 [cs.FL], March 6 2022.
Available at https://arxiv.org/abs/2203.02917. Revised, published version in
Australasian J. Combinatorics84 (2022), 419-430.
Available here
.
J. Shallit,
Sumsets of Wythoff sequences, Fibonacci representation, and beyond,
Periodica Mathematica Hungarica84 (2022), 37--46.
Available here.
Phakhinkon Napp Phunphayap, Prapanpong Pongsriiam, and
Jeffrey Shallit,
Sumsets associated with Beatty sequences, to appear,
Discrete Mathematics.
TP.txt file, place this in the
Word Automata directory of Walnut
C. S. Kaplan and J. Shallit,
A frameless 2-coloring of the plane lattice,
Math. Magazine94 (5) (2021), 353-360.
A limited number of free-eprints are available
here.
shift.txt (put this in the "Automata Library" of Walnut)
fibinc.txt (put this in the "Automata Library" of Walnut)
Jason P. Bell and J. Shallit,
Lie complexity of words, Arxiv preprint, Feb 7 2021,
arXiv:2102.03821 [cs.FL]. Available
here.
Aseem Baranwal, Luke Schaeffer, and Jeffrey Shallit,
Ostrowski-automatic sequences: Theory and applications,
Theor. Comput. Sci.858 (2021) 122-142. Available
here
until March 11 2021.
Aseem Raj Baranwal, Jeffrey Shallit,
Repetitions in infinite palindrome-rich words, arxiv preprint, April 22 2019.
In Mercas R., Reidenbach D. (eds.) Combinatorics on Words. WORDS 2019.
Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 93-105.
Available
here.
Tim Ng, Pascal Ochem, Narad Rampersad, Jeffrey Shallit,
New
results on pseudosquare avoidance, arxiv preprint, April 19 2019.
In Mercas R., Reidenbach D. (eds.) Combinatorics on Words. WORDS 2019.
Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 264-274.
Available
here.
T. Clokie, D. Gabric, and J. Shallit,
Circularly squarefree words and unbordered conjugates: a new approach,
arxiv preprint, April 17 2019.
In Mercas R., Reidenbach D. (eds.) Combinatorics on Words. WORDS 2019.
Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 264-274.
Available
here.
Aseem R. Baranwal, Jeffrey Shallit,
Critical exponent
of infinite balanced words via the Pell number system,
arxiv Preprint, February 1 2019.
In Mercas R., Reidenbach D. (eds.) Combinatorics on Words. WORDS 2019.
Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 80-92.
Available
here.
James Currie, Narad Rampersad, Tero Harju, and Pascal Ochem,
Some further results on squarefree arithmetic
progressions in infinite words,
arxiv preprint,
January 18 2019. Appeared in
Theoretical Computer Science799 (2019) 140-148.
James Currie and Narad Rampersad,
On some problems of Harju concerning squarefree
arithmetic progressions in infinite words,
arxiv preprint,
December 5 2018.
Lukasz Merta,
Formal inverses of the generalized Thue-Morse sequences
and variations of the Rudin-Shapiro sequence,
arxiv preprint,
October 8 2018. Appeared in
Discrete Mathematics and Theoretical Computer Science
Vol. 22:1, 2020, #15.
Jeffrey Shallit and Ramin Zarifi,
Circular critical exponents for Thue–Morse factors,
RAIRO Info. Theor., published online 17 January 2019.
Available here.
Pierre Bonardo, Anna E. Frid, Jeffrey Shallit,
"The number of valid factorizations of Fibonacci prefixes",
Theor. Comput. Sci., 2019, to appear.
Available online at https://doi.org/10.1016/j.tcs.2018.12.016.
Jason Bell, Kathryn Hare and Jeffrey Shallit,
When is an automatic set an additive basis?
Proc. Amer. Math. Soc. Ser. B5 (2018), 50-63.
Available here.
Jason Bell, Thomas Finn Lidbetter, and Jeffrey Shallit,
Additive Number Theory via Approximation by Regular Languages,
arxiv preprint, April 23 2018. Appeared in M. Hoshi and S. Seki, eds.,
DLT 2018, LNCS Vol. 11088, Springer, 2018, pp. 121-132.
Here are text files describing how you can verify the results
yourself using Grail and Walnut.
James Currie, Lucas Mol, and Narad Rampersad,
A family of formulas with reversal of high avoidability index,
International Journal of Algebra and Computation27 (2017)
477-493.
A. Rajasekaran, N. Rampersad, J. Shallit,
Overpals, Underlaps, and Underpals,
in WORDS 2017: Combinatorics on Words, 2017, pp. 17-29.
Floriane Magera, Automatic demonstration of mathematical
conjectures, Master's thesis, University of Liège,
2015-6. Available at
https://matheo.uliege.be/handle/2268.2/1679.
Daniel Goc, Hamoon Mousavi, Luke Schaeffer, Jeffrey Shallit,
A New Approach to the Paperfolding Sequences,
in Arnold Beckmann, Victor Mitrana, Mariya Soskova, eds.,
Evolving Computability:
11th Conference on Computability in Europe, CiE 2015, Springer, LNICS,
Vol. 9136, 2015, pp. 34-43. Available
here.
H. Mousavi and J. Shallit,
Mechanical Proofs of Properties of the Tribonacci Word,
in
F. Manea and D. Nowotka, eds.,
WORDS 2015, LNCS 9304, Springer, 2015, pp. 1-21. Here are the
Walnut predicates you can use to reproduce most of the results in this
paper:
This was one of the first Walnut papers we wrote, and now (in 2024)
we know there are better ways to do some of the things we did in this one.
For example, to check whether TR[i..i+n-1] is a palindrome, where TR denotes
the Tribonacci word, one can simply write
def tribpal "?msd_trib Au,v (u>=i & u<i+n & u+v+1=2*i+n) => TR[u]=TR[v]":
and hence avoid the split into even and odd cases. It runs very quickly!
Similarly, to check that TR is mirror invariant, one can write
def trib_fac_reverse_equiv "?msd_trib Au,v (u>=i & u<i+n & u+v+1=i+j+n) => TR[u]=TR[v]":
def trib_mirror "?msd_trib Ai,n Ej $trib_fac_reverse_equiv(i,j,n)":
which also runs rather quickly.
Daniel Goc, Narad Rampersad, Michel Rigo, Pavel Salimov,
On the number of Abelian Bordered Words (with an Example of Automatic Theorem-Proving)
Int. J. Found. Comput. Sci.25 (2014), 1097-1110.