Walnut Exercises

Here are some exercises you can try to test your understanding of Walnut.

  1. Use the technique of "automatic breadth-first search", as discussed in the Walnut book, to find a small automaton whose inputs are in base 3 and generates a word over the alphabet {0,1,2} having no (7/4+ε)-powers. Then, once you've found a candidate, use Walnut to prove it is correct.

  2. Use Walnut to prove the results in this 1991 paper: Timothy Chow, A new characterization of the Fibonacci-free partition, Fibonacci Quart. 29 (1991), 174-180. Hints: to find an automaton for the set A, use the technique of "guessing the automaton", as discussed in the Walnut book; then prove it is correct and unique using induction. Since Walnut cannot do induction directly, use Walnut to prove the induction step, which is "once the numbers from 1 to n have been assigned to the sets A and B, the choice for the number n+1 is forced".

    Now do the same thing to prove a similar result where the Fibonacci numbers are replaced by the Lucas numbers 2,1,3,4,7,11, ...

  3. Use automatic breadth-first search to find a candidate automatic sequence over the alphabet {0,1} avoiding all squares xx and antisquares xx̅ with |x| ≥ 3. Then prove your automaton is correct using Walnut. Here means the complementary string formed by exchanging 0's and 1's.

  4. Rederive the results for counting subsequences of the Fibonacci word in the following paper: A. Salomaa, Subword occurrences, weighted automata and iterated morphisms, especially the Fibonacci morphism, Theor. Comput. Sci. 432 (2012), 85-93. Note: with Walnut you can find a linear representation for the number of these subsequences in any prefix of arbitrary length n, not just for the i'th iteration of the Fibonacci morphism.

  5. Guess and prove a synchronized automaton for the starting positions of runs in the (ordinary) paperfolding sequence. Use this automaton to rederive the results in the recent paper of Bunder, Bates, and Arnold, The summed paperfolding sequence, Bull. Austral. Math. Soc. 110 (2024), 189-198.

  6. Consider the set of natural numbers whose Tribonacci expansion ends in a 1, and arrange them in ascending order: 1, 3, 5, 8, 10, 12, 14, 16, 18, 21, 23, 25, 27, 29, 32,... Guess a Tribonacci automaton with two inputs, n and x, and accepts if x is the n'th number on this list.

    Once you have your guess, prove it is correct with Walnut.

  7. Look at the function defined by Burton and Campbell, A curious recursive function, Intern. J. Computer Math. 19 (1986), 245-257. Guess a Fibonacci automaton for the function, verify that it is correct because it solves the recurrence, and then verify their closed form for it.

  8. A theorem of Chung and Graham (On irregularities of distribution, Colloq. Math. Soc. Janos Bolyai 37 (1984), 181-222) says that every non-negative integer has a unique representation as a sum of Fibonacci numbers, sum(ai * F(2i), 1 ≤ i ≤ t), where ai ∈ {0,1,2}, with the proviso that if ai = 2 and aj = 2 with i < j then some index k, i < k < j, has ak = 0. Prove this with Walnut. Hint: first define a regular expression for those strings with 0's in positions corresponding to odd-indexed Fibonacci numbers, and allowing {0,1,2} for the even positions; then create a "canonicalizer" to convert it to the corresponding Fibonacci representation.