Walnut Tutorial

Here is a tutorial to introduce you to Walnut and some of the things it can do. We use the terms "string", "word", "block" as synonyms.

If you are computer-savvy, you can install Walnut on your computer by going to this page, or if you just want to try it in a web browser, go to this URL. It takes about 15-30 seconds to load. Once it loads, click the button that says "New ▼" and select "Walnut". You will now see a blue rectangle. You can now type in Walnut commands and click the small black right-pointing triangle ▸ to run them.

  1. The single most basic thing you can do with Walnut is Presburger arithmetic: quantified arithmetic expressions in multiple variables using only addition, subtraction, and multiplication by constants. Remember that Walnut's default domain is N, the natural numbers, so no subexpression should be negative.

    Use the syntax eval test followed the predicate in quotes, then a semicolon, to enter Walnut queries for

    Remember that A denotes "for all" and E denotes "there exists".

    Solution. Do you see why the first returns TRUE and the second FALSE?

  2. Now let's try proving a very simple theorem with Walnut: the sum of two odd numbers is even. To define an automaton accepting only the odd numbers, we write

    def odd "E k n=2*k+1";

    Try entering that now.

    By the way, if you want to see more of what is happening "behind the scenes", you can always end a command with a colon : instead of a semicolon ; . Or if you want to see even more, use two colons at the end.

    Next, define an automaton "even" in the same way, and then try evaluating the following command, which proves the theorem.

    eval thm1 "A m,n ($odd(m) & $odd(n)) => $even(m+n)";

    Notice that when you use a defined automaton, you precede its name with a dollar-sign. Next, prove that the sum of an odd number and an even number is odd.

    Solution.

  3. OK, now it's time to show off more of the power of Walnut: by proving theorems about some famous sequences! One of the most famous of all sequences in combinatorics on words is the Thue-Morse sequence 0110100110010110 ···, an infinite binary sequence, indexed starting at position 0. The i'th term of the sequence is defined to be the sum of the bits, taken modulo 2, of the base-2 representation of i. In Walnut this sequence is represented by T and you index its values with square brackets. So T[i] refers to the i'th term.

    Now let's prove one of the very first theorems in combinatorics on words, proved by the Norwegian mathematician Axel Thue in 1912: the Thue-Morse sequence has no overlaps. An overlap is a string of the form axaxa, where a is a single letter and x is an arbitrary string, possibly empty. An example of an overlap in English is the word alfalfa.

    Try writing a Walnut predicate hasover that asserts that T has an overlap axaxa of total length 2n + 1 beginning at position i of T. So here the variables i and n are unbound; they have no quantifier associated with them. It should look something like

    def hasover "definition goes here";

    Solution.

  4. Now that we have the automaton for the predicate hasover, we can use it. But it has two arguments, i and n. When we call it, how do we know which argument goes first? Here Walnut uses its own idiosyncratic rule: namely, you use a defined automaton like hasover by writing its arguments in dictionary order when it was defined. Since i comes before n in the dictionary and so when you use hasover the first argument corresponds to the i and the second n.

    Try writing a Walnut command starting with "eval" that asserts that T has no overlaps anywhere in it. Here you can use the symbol ~ for logical negation. There is a small pitfall here to avoid...

    Solution.

  5. The Thue-Morse sequence T has many interesting properties. Here is one: it is mirror-invariant: if a string x occurs in it somewhere, then so does the reversal of x. In this exercise, which is slightly more challenging, you will write Walnut code proving this property.

    In Walnut there is no way to directly quantify over all strings. You can only quantify over the natural numbers. So we can't express "if a string x occurs then ..." directly. Instead of working with strings, we work with occurrences of strings. These can be specified, for example, by giving the starting position i and the length n of the string, inside some sequence.

    Try writing a Walnut command proving the mirror invariant property for T.

    Solution.

  6. OK, now that you did that challenging exercise, the next one should be easy. In Walnut, one of the most useful things to define is the "equality of factors" predicate, which asserts that the block of length n occurring starting at position i is the same as that starting at position j.

    Try defining that one using def and then using it to prove that T has the property of recurrence: namely, every string occurring in T, actually occurs infinitely often.

    Solution.

  7. Another nice property of T is that every nonempty block of length n that appears anywhere in it is guaranteed to occur fairly early in T, starting at some position ≤ cn for some constant c. This exercise asks you to find a suitable value of c through experimentation. The predicate for "equality of factors" that you defined may be very useful here!

    Solution.

  8. So far we have been working with automata with every Walnut command, but we haven't seen any automata so far! Let's change that.

    Here's how Walnut can not only prove theorems, but actually figure out the right statement to prove! Consider the Thue-Morse sequence one more time. It has squares in it, that is, blocks of the form xx where x is nonempty, such as 00 and 010010. It is natural to ask what the length of these blocks can be. Write a Walnut predicate squarelen with n as a free variable (unbound by any quantifier) that says there exists a square of length 2n in the Thue-Morse sequence.

    Once you have created the automaton, you can deduce the theorem about what the lengths are by simply examining the strings it accepts, which are those n that are possible, expressed in base 2. What are they?

    (You can see the automaton in two different ways, depending on whether you have Walnut installed on your computer, or you're using the web browser version. For the latter, just type

    %showme squarelen

    and it should appear on your screen. For the former, a bit more work is needed. Use another terminal window, go to the Result directory, and look for the file squarelen.gv, which is a GraphViz encoding of the automaton. Then you can use a command like

    dot -Tpdf squarelen.gv > squarelen.pdf

    in Linux to create a pdf file you can view.

    Solution.

  9. So far we have just been working with the Thue-Morse word and base 2. It's time to work with another word and an exotic numeration system. In the Fibonacci numeration system, natural numbers are expressed as a sum of Fibonacci numbers 1,2,3,5,8,13,... instead of as a sum of powers of 2. We express numbers using the "digits" 0 and 1, just like in base 2, so 1010 means 5+2 or 7. To get unique representation, we are not allowed to use two consecutive Fibonacci numbers in a representation. With this numeration system we can talk about properties of the so-called Fibonacci word 0100101001001 ... which is 1 in position i ≥ 0 iff the Fibonacci representation of i ends in a 1. The Fibonacci word is built-into Walnut under the name F.

    Whenever we work with an exotic numeration system like Fibonacci, we need to tell Walnut that's what we are doing. To do this we write the query as

    "?msd_fib rest of query";

    Determine the degree of repetition in this sequence. Does it have squares, of the form xx, or cubes of the form xxx, or fourth powers of the form xxxx, where x is a nonempty block?

    Solution.

  10. For our last exercise, we introduce the notation of synchronized function. This is a very useful way to talk about functions from N to N in Walnut. We represent a function f(n) as a relation computed by an automaton: it takes two inputs in parallel, say n and x, and accepts if and only if x = f(n).

    Let ϕ = (1+√5)/2 be the golden ratio. It turns out that the functions n → floor (ϕ n) and n → floor (ϕ2 n) are both computable in this way, and the following Walnut code defines them, respectively, as phin and phi2n: 

    reg shift {0,1} {0,1} "([0,0]|[0,1][1,1]*[1,0])*";
def phin "?msd_fib (s=0 & n=0) | E x $shift(n-1,x) & s=x+1";
def phi2n "?msd_fib (s=0 & n=0) | E x,y $shift(n-1,x) & $shift(x,y) & s=y+2";
    It would take us too far afield to explain how this works, so please just take it on faith.

    Now we can do some additive number theory. Show that every sufficiently large natural number is representable as floor (ϕ m) + floor (ϕ n) for m, n ≥ 1. However this is not possible for floor (ϕ2 m) + floor (ϕ2 n). Also show that every sufficiently large natural number is representable as floor (ϕ2 m) + floor (ϕ2 n) + floor (ϕ2 p) for m, n, p ≥ 1.

    Solution.