A `Walnut` Diary

This is a place for Jeff's short informal notes about various things that can be done with Walnut.

August 11 2026

Continuing the last three diary entries... Geoffrey Caveney asked for an overlap-free quaternary word with an overlap-free curling sequence. Dong Haoxuan used an LLM to find a rather complicated solution involving a 4096-uniform morphism (!). But there is a much simpler construction. Once again ChatGPT 5.6 found a candidate that one can prove with Walnut. As in the previous construction, take
t = 01101001... the Thue-Morse sequence.

As before, slide a window of size 2 over t, one step at a time, and evaluate the adjacent pairs of symbols as a 2-bit base 2 number:
01 = 1
11 = 3
10 = 2
01 = 1
10 = 2
00 = 0
... and so forth. This gives the sequence p = 132120...

Now apply the morphism
0 -> 1001200122322300
1 -> 1001200122003220
2 -> 0313110021100200
3 -> 0313112202203003
to p, getting q = 10012001220032200313112202203003... Now consider the sequence q' = 00q. It is overlapfree and has curling sequence 12112... which is 1 + t(n+3), where t is Thue-Morse.

Walnut verification:

def p00 "T[n]=@0 & T[n+1]=@0": def p01 "T[n]=@0 & T[n+1]=@1": def p10 "T[n]=@1 & T[n+1]=@0": def p11 "T[n]=@1 & T[n+1]=@1": combine P p00=0 p01=1 p10=2 p11=3: morphism h "0->1001200122322300 1->1001200122003220 2->0313110021100200 3->0313112202203003": image Q h P: def qp0 "(n<=1) | (n>1 & Q[n-2]=@0)": def qp1 "Q[n-2]=@1": def qp2 "Q[n-2]=@2": def qp3 "Q[n-2]=@3": combine QP qp0=0 qp1=1 qp2=2 qp3=3: eval overlapfree "~Ei,n n>=1 & At (t<=n) => QP[i+t]=QP[i+n+t]": def curl "Ei,c c>=1 & i+2*c=n+1 & At (t<c) => QP[i+t]=QP[i+t+c]": def nocurl "~$curl(n)": combine D curl=2 nocurl=1: eval check "An D[n]=1 <=> T[n+3]=@0":

August 10 2026

Continuing the last two diary entries... Geoffrey Caveney asked for an overlap-free ternary word with a cubefree curling sequence. Once again ChatGPT 5.6 found a simple construction.

As in the previous construction, take
t = 01101001... the Thue-Morse sequence.

Now apply the morphism
0 -> 001
1 -> 002
2 -> 202
3 -> 212
to p, getting q = 002212202... Then q is overlap-free and its curling sequence d = 1212... is cubefree. Walnut proof:

def p00 "T[n]=@0 & T[n+1]=@0": def p01 "T[n]=@0 & T[n+1]=@1": def p10 "T[n]=@1 & T[n+1]=@0": def p11 "T[n]=@1 & T[n+1]=@1": combine P p00=0 p01=1 p10=2 p11=3: morphism h "0->001 1->002 2->202 3->212": image Q h P: eval overlapfree "~Ei,n n>=1 & At (t<=n) => Q[i+t]=Q[i+n+t]": def curl "Ei,c c>=1 & i+2*c=n+1 & At (t<c) => Q[i+t]=Q[i+t+c]": def nocurl "~$curl(n)": combine D curl=2 nocurl=1: eval check "~Ei,n n>=1 & At (t<2*n) => D[i+t]=D[i+n+t]":

By the way, there is no infinite ternary overlap-free word with an overlap-free curling number sequence. The longest such is of length 84 and here is one of them: 011010010200202121100200210021101001020020211011020020212110020021002112201122021100.

August 8 2026

Here's something else, continued from yesterday's diary entry. The construction is from ChatGPT, the proof is from Walnut.

ChatGPT produced the following example of a cubefree ternary sequence whose curling sequence is overlap-free.

Start with TM t = 01101001...

Slide a window of size 2 over t, one step at a time, and evaluate the adjacent pairs of symbols as a 2-bit base 2 number:
01 = 1
11 = 3
10 = 2
01 = 1
10 = 2
00 = 0
... and so forth. This gives the sequence 132120...

Now apply the morphism

0->0020201001002022
1->0010012001202010
2->0100202202122121
3->0100202200202010

to this sequence, getting
001001200120201001002022002020100100202202122121...
with curling sequence
121122... which is (t(3) t(4) t(5)....) + 1 and hence overlap-free.

Here is the proof in Walnut:

def p00 "T[n]=@0 & T[n+1]=@0": def p01 "T[n]=@0 & T[n+1]=@1": def p10 "T[n]=@1 & T[n+1]=@0": def p11 "T[n]=@1 & T[n+1]=@1": combine P p00=0 p01=1 p10=2 p11=3: morphism h "0->0020201001002022 1->0010012001202010 2->0100202202122121 3->0100202200202010": image B h P: eval cubef "~Ei,n n>=1 & At (t<2*n) => B[i+t]=B[i+n+t]": def curl "Ei,c c>=1 & i+2*c=n+1 & At (t<c) => B[i+t]=B[i+t+c]": def nocurl "~$curl(n)": combine D curl=2 nocurl=1: eval check "An (T[n+3]=@0 <=> D[n]=@1)":

August 7 2026

On the SeqFan mailing list, Geoffrey Caveney asked if there is an infinite cubefree sequence over {0,1,2} such that its curling number sequence is also cubefree.

Here is how to construct such a sequence: Take the Thue-Morse sequence 01101001.... and apply the morphism that maps 0 to 011010 and 1 to 121122. The resulting word U = 01101012112212112201101012112201101001101012112212 ... has the property you want; its curling number sequence is C = 11211221121211221211211221121211211221211221121211 ... and is cubefree.

The construction itself was found by ChatGPT 5.6 Pro. Once you know it, you can easily check its correctness with Walnut as follows:

morphism m "0->011010 1->121122": # define the morphism image U m T: # apply it to the Thue-Morse word, defining U eval cubef "~Ei,n n>=1 & At (t<2*n) => U[i+t]=U[i+n+t]": # check that U is cubefree; it answers TRUE def curl "Ei,c c>=1 & i+2*c=n+1 & At (t<c) => U[i+t]=U[i+t+c]": # determine if the prefix of U of length n+1 (for n ≥ 0) ends with a square def nocurl "~Ei,c c>=1 & i+2*c=n+1 & At (t<c) => U[i+t]=U[i+t+c]": # determine if the prefix of U of length n+1 does NOT end with a square combine C curl=2 nocurl=1: # make a DFAO to compute the sequence C eval tmp "~Ei,n n>=1 & At (t<2*n) => C[i+t]=C[i+t+n]": # check that there are no cubes in C, it answers TRUE

Exercise: show that the largest fractional power appearing in U is 5/2, and the largest fractional power in C is 8/3.

August 6 2026

Sequence A273050 in the OEIS asks for those natural numbers k with the property that if you rotate the bits of the base-2 representation of k one place to the left (with wraparound), and to the right, and take the XOR of the resulting two numbers, you get k back again. There contributors gave various complicated characterizations of the resulting numbers.

Here is a general technique for approaching this problem in Walnut.

First, we need an automaton that will accept, in parallel, the base-2 representation of a number k together with its left rotation by one bit. You have to write this code by hand, but it's not hard. Here it is in Walnut's internal format, called 'rotl.txt':

{0,1} {0,1}

0 1
0 0 -> 1
0 1 -> 2
1 0 -> 3
1 1 -> 4

1 1
0 0 -> 1
0 1 -> 2

2 0
1 0 -> 1
1 1 -> 2

3 0
0 0 -> 3
0 1 -> 4

4 1
1 0 -> 3
1 1 -> 4

Notice that we declare the alphabet to be {0,1} instead of msd_2, because we are dealing with strings of bits where we want to handle leading zeroes correctly. (Walnut usually works with integers, not bit strings, and the result is that in msd_2 leading zeroes don't have any effect.) The idea is that we keep track of the first bit f of k seen, and the bit we are expecting to see, e, based on its left shift. State 1 corresponds to (f,e) = (0,0); state 2 is (f,e) = (0,1); state 3 is (f,e) = (1,0); state 4 is (f,e) = (1,1). We accept iff f = e. This is an more or less an undergraduate exercise in beginning automata theory.

Now we don't need to write a separate automaton for right rotation, because we can just use rotl and switch the arguments.

Next we want to enforce that the k that we deal with start with 1 in their base-2 representation. Again, this is to ensure we're not dealing with expansions that are not canonical. We can do this as follows:

reg start1 {0,1} "1(0|1)*":

which uses a regular expression to define the automaton.

We need an automaton for xor.

reg xor {0,1} {0,1} {0,1} "([0,0,0]|[1,1,0]|[0,1,1]|[1,0,1])*":

Finally we can define the sequence:

def a273050 "Ex,y $rotl(k,x) & $rotl(y,k) & $xor(x,y,k) & $start1(k)":

which in English means: there exists x and y such that x is the left rotation of k and y is the right rotation of k and the xor of x and y is k and furthermore I only want to consider the canonical base-2 representation of k, not one with leading zeroes. This gives an automaton of 8 states displayed below.

And inspection gives that the base-2 representations of the sequence elements are of the form (101)+ and (110)+. From this the more complicated descriptions of the sequence elements are very easily obtained.

May 6 2026

Schaefer, Sedgwick, and Stefankovic wrote an interesting paper in 2011 called Spiraling and folding: The word view. Back in June 2023, I realized that some of what they did in that paper could be done with Walnut.

Here is the Walnut code that verifies the various claims in their paper, especially pages 621-623, and also proves the conjecture implicitly given in Remark 4.7.

reg shift {0,1} {0,1} "([0,0]|[0,1][1,1]*[1,0])*": def phin "?msd_fib (s=0 & n=0) | Ex $shift(n-1,x) & s=x+1": # automaton accepting (n,s) where s = floor(n*phi), from my Walnut book, p. 278 def even "?msd_fib Ex n=2*x": # true if n is even def san "?msd_fib Ex $phin(n,x) & ~$even(x)": # accepts n if floor(n*phi) mod 2 is 1 combine SAN san: # makes a 13-state DFAO called 'SAN' computing a(n) def squares_in_an "?msd_fib (n>=1) & Ei Aj (j<n) => SAN[i+j]=SAN[i+j+n]": # accept orders of nonempty squares in sequence a(n) # the automaton it computes proves remark 4.7, as it only # accepts words of the form 1(000)*, corresponding to Fibonacci numbers # of the form F_{3n+2} eval exists_even_square "?msd_fib En $even(n) & $squares_in_an(n)": # returns FALSE, so no even squares, thus verifying lema 4.6 Now the proof of Lemma 4.3: we need floor(n*phi + 1/2) = floor((2*n*phi + 1)/2) = floor( floor(2*n*phi+1)/2 ) = floor( (floor(2*n*phi) + 1)/2 ) def phin2 "?msd_fib Ex $phin(2*n,x) & y=(x+1)/2": def san2 "?msd_fib Ey $phin2(n,y) & ~$even(y)": combine SAN2 san2: # makes a 24-state DFAO called "SAN2" computing (closest integer to n*phi) mod 2 reg isfib msd_fib "0*10*": # a Fibonacci number reg isfib32 msd_fib "0*1(000)*": # these define Fibonacci numbers of the form F_{3k+2} eval lemma43 "?msd_fib Ax $isfib(x) => (SAN2[x]=@0 <=> $isfib32(x))": # returns TRUE eval lemma44pt1 "?msd_fib Ak,l,x (k>=1 & l>=1 & k+l=x & $isfib32(x)) => SAN[k]!=SAN[l]": eval lemma44pt2 "?msd_fib Ak,l,x (k>=1 & l>=1 & k+l=x & $isfib(x) & ~$isfib32(x)) => SAN[k]=SAN[l]": # both return TRUE Now the verification of corollary 4.8. It suffices to show SAN[1..F_n - 1] = SAN[1..F_{n-1} - 1] (SAN[1..F_{n-2}])^R if n == 0, 1 (mod 3) = SAN[1..F_{n-1} - 1] negation of (SAN[1..F_{n-2}])^R if n == 2 (md 3) def two_consec_fib "?msd_fib $isfib(x) & $isfib(y) & x>y & x<=2*y": # x and y are two consecutive Fibonacci numbers with x > y eval cor48case01 "?msd_fib Ax,y ($isfib(x) & $two_consec_fib(x,y) & ~$isfib32(x)) => (Ai (i>=1 & i<=x-y) => SAN[i]=SAN[x-i])": # returns TRUE eval cor48case2 "?msd_fib Ax,y ($isfib(x) & $two_consec_fib(x,y) & $isfib32(x)) => (Ai (i>=1 & i<=x-y) => SAN[i]!=SAN[x-i])": # returns TRUE

Yesterday I heard from Narad Rampersad that he recently came across this paper and found the same things.

May 5 2026

Today Gandhar Joshi gave a nice talk on recurrences, morphisms, Dumont-Thomas numeration systems, and Walnut in the One World Numeration seminar. It is based on his paper with Fokkink that recently appeared in the Ramanujan Journal.

In the paper he discussed the sequence s = 10001010101000101000... which is the fixed point of the morphism that sends 1 to 1000 and 0 to 10. In his paper with Fokkink, he analyzed this sequence using the Dumont-Thomas numeration system using the sequence 1, 2, 6, 16, 44, 120, ... that satisfies B_n+1 = 2B_n + 2B_n-1, and connected the sequence with √3. In particular his numeration system was not greedy.

However, if instead of the sequence above, we shift it by 1 and divide by 2, we get the sequence 1,3,8,22,60,... which I studied in this paper in 2024, and called the Kimberling numeration system. The advantage to this system is that it has simple greedy representations and an addable numeration system.

In this numeration system s has a rather simple description in terms of a 13-state automaton, which I call J.txt in honor of Joshi. Here it is:

msd_kim

0 1
0 -> 0
1 -> 1
2 -> 2

1 0
0 -> 3
1 -> 4
2 -> 2

2 0
0 -> 0
1 -> 1

3 0
0 -> 0
1 -> 1
2 -> 5

4 1
0 -> 6
1 -> 1
2 -> 2

5 1
0 -> 0
1 -> 1

6 0
0 -> 3
1 -> 7
2 -> 8

7 0
0 -> 6
1 -> 9
2 -> 10

8 1
0 -> 11
1 -> 1

9 1
0 -> 3
1 -> 4
2 -> 2

10 0
0 -> 3
1 -> 7

11 0
0 -> 12
1 -> 7
2 -> 8

12 1
0 -> 11
1 -> 1
2 -> 5

With this and the techniques in my paper mentioned above I imagine one can obtain the same results as Joshi, in perhaps a simpler and more straightforward way.

April 10 2026

Some people who work in combinatorics on words have defined "run" in a word x to be a pair of integers (i,j) such that i ≤ j and x[i..j] has period p and p ≤ (j-i+1)/2, and furthermore the run is "maximal" in the sense that it cannot be extended to the left or right in x and still have period p. "Run" is bad terminology; it really should be something like "occurrence of a maximal repetition" or something like that. It is important to understand that a run is not a word, but rather a particular occurrence of a word within x.

For example, consider x = x[1..8] = 01001010. Here the runs are (1,6), (3,4), and (4,8).

Counting the number of runs in a word has become a kind of industry in the field, culminating in the 2017 paper by Bannai et al. that proved that a word of length n has < n runs.

The Fibonacci words give a class of words with a lot of runs. They are defined by X₁ = 1, X₂ = 0, and X_n = X_n-1 + X_n-2 for n ≥ 3. In Walnut we can deal with the Fibonacci word X_n for n ≥ 2 as the prefix of length F_n of the infinite Fibonacci word f, which is built-in to Walnut under the name F. Recall that infinite words in Walnut are indexed starting at position 0.

As mentioned in Theorem 7 of Crochemore et al., it is known that there are exactly 2F_n-2 - 3 runs in X_n for n ≥ 5. We can prove this in Walnut as follows.

def fper "?msd_fib p>0 & At (t>=i & t+p<=j) => F[t]=F[t+p]": # asserts F[i..j] has period p>0 def fminper "?msd_fib $fper(i,j,p) & Aq $fper(i,j,q) => q>=p": # asserts F[i..j] has minimal period p def frun n "?msd_fib i<=j & j<n & Ep $fminper(i,j,p) & j+1>=2*p+i & (~$fper(i-1,j,p)) & ((j+1<n & ~$fper(i,j+1,p)) | (j+1=n))": # asserts that (i,j) is a run in f[0..n-1] # and also creates linear representation frun.mpl counting the number # of runs in prefix of length n of Fibonacci word

Only frun needs explanation. Here we assert that
(a) i ≤ j
(b) j < n (we are considering f[0..n-1])
(c) there is some period p satisfying p ≤ (j-i+1)/2 (notice we rewote the inequality to avoid subtraction and division)
(d) when we extend to the left the result doesn't have period p (notice that if i=0 then $fper will never return TRUE)
(e) when we extend to the right the result doesn't have period p (notice we have to special-case the possibility that j=n-1, in which case it's not possible to extend it to the right).

This gives us a linear representation (v, M₀, M₁, w) for the number of runs in a prefix of f of length n, stored in the file frun.mpl. Now the Fibonacci word X_n has length F_n, which in Zeckendorf representation is 10^n-2. So the number of runs is v M₁ M₀^n-2 w, and hence is a linear combination of the entries of M₀^n-2. These entries satisfy a linear recurrence corresponding to the minimal polynomial of M₀, which we can compute using Maple as follows:


read("frun.mpl"):
with(linalg):
factor(minpoly(M_n_0,x));

and the result is x⁴ (x² - x - 1) (x - 1)² (x + 1)². It now follows from the fundamental theorem of linear recurrences that the number of runs in X_n is a linear combination of αⁿ, βⁿ, n, 1, (-1)ⁿ n, (-1)ⁿ. When we solve for the linear combination using the first few values of the number of runs (which we can compute directly from the linear representation), we find that this number is 2 F_n-2 - 3 for n-2 ≥ 4. We can check it also holds for n = 5, and the result is now proved.

Oddly enough, it seems no one up to now computed the number of distinct runs in the n'th Fibonacci word. Here we are thinking of a run as a word, rather than the occurrence of a word. We can also do this with Walnut as follows:

def fibeqfac "?msd_fib At (t<n) => F[i+t]=F[j+t]": # asserts F[i..i+n-1]=F[j..j+n-1] def fdrun n "?msd_fib $frun(i,j,n) & ~Ek k<i & $frun(k,(k+j)-i,n) & $fibeqfac(i,k,(j+1)-i)": # creates linear representation fdrun.mpl counting the number # of distinct runs in prefix of length n of Fibonacci word

Exactly as before, we can now compute the minimal polynomial of the resulting matrix M₀. It is x⁵ (x - 1)² (x+1)². It follows that for n-2 ≥ 5 the number of distinct runs is a linear combination of n, 1, (-1)ⁿ n, (-1)ⁿ. Solving the linear system using the values n = 7,8,9,10, we get (5/2)n - 51/4 - (-1)ⁿ/4. Rephrasing, we have that the number of distinct runs in X_n is floor((5n-25)/2) for n ≥ 7.

April 1 2026

A recent paper on the arxiv, by 5 people at OpenAI, used LLM's to come up with short proofs of existing results (and even improve them).

I recognized two of the lemmas (Lemmas 3.2 and 3.3) as doable with Walnut. It was very easy. Notice the usual trick of handling powers of the base; instead of writing powers as a function of k as in the paper, we merely assert that x or y is a power of 5 without specifying exactly which one it is. This is often good enough.

reg ispower5 msd_5 "0*10*":
# is argument a power of 5 ?

def ck "?msd_5 n=4*x":
# accepts c_k, where 5^{k-1} = x

def bk "?msd_5 5*x<=n & n<6*x":
# accepts members of B_k, where 5^{k-1} = x

def fk "?msd_5 10*x-1<=n & n<=15*x":
# accepts members of F_k, where 5^{k-1} = x

def ak "?msd_5 Ex $ispower5(x) & x<=y & (n=2 | n=3 | $ck(n,x) | $bk(n,x) | $fk(n,x))":
# accepts members of A_k, where 5^{k-1} = y

def a "?msd_5 Ey $ispower5(y) & $ak(n,y)":
# accepts members of A

eval lemma32 "?msd_5 Ay,n (4<=n & n<=6*5*y & $ispower5(y)) => En1, n2 $ak(n1,y) & $ak(n2,y)  & n=n1+n2":

def jk "?msd_5 9*x<=n & n<10*x":
# accepts members of J_k, where x = 5^{k-1}

eval lemma33 "?msd_5 An,y,c,d ($ispower5(y) & $jk(n,y) & $a(c) & $a(d) & n=c+d)
   => (($ck(c,y) & $bk(d,y)) | ($ck(d,y)|$bk(c,y)))":

A Walnut Diary