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 X1 = 1, X2 = 0, and Xn = Xn-1 + Xn-2 for n ≥ 3. In Walnut we can deal with the Fibonacci word Xn for n ≥ 2 as the prefix of length Fn 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 2Fn-2 - 3 runs in Xn for n ≥ 5. We can prove this in Walnut as follows.
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, M0, M1, w) for the number of runs in a prefix of f of length n, stored in the file frun.mpl. Now the Fibonacci word Xn has length Fn, which in Zeckendorf representation is 10n-2. So the number of runs is v M1 M0n-2 w, and hence is a linear combination of the entries of M0n-2. These entries satisfy a linear recurrence corresponding to the minimal polynomial of M0, which we can compute using Maple as follows:
read("frun.mpl"):
with(linalg):
factor(minpoly(M_n_0,x));
and the result is x4 (x2 - x - 1) (x - 1)2 (x + 1)2. It now follows from the fundamental theorem of linear recurrences that the number of runs in Xn is a linear combination of αn, βn, n, 1, (-1)n n, (-1)n. 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 Fn-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:
Exactly as before, we can now compute the minimal polynomial of the resulting matrix M0. It is x5 (x - 1)2 (x+1)2. It follows that for n-2 ≥ 5 the number of distinct runs is a linear combination of n, 1, (-1)n n, (-1)n. Solving the linear system using the values n = 7,8,9,10, we get (5/2)n - 51/4 - (-1)n/4. Rephrasing, we have that the number of distinct runs in Xn is floor((5n-25)/2) for n ≥ 7.
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)))":