Walnut Tutorial - Solutions 

  1. eval part1 "A x E y y=x+1";
eval part2 "A x E y x=y+1";
    The second evaluates to FALSE because 0 has no predecessor in N. 
  2. def odd "E k n=2*k+1";
def even "E k n=2*k";
eval thm1 "A m,n ($odd(m) & $odd(n)) => $even(m+n)";
eval thm2 "A m,n ($odd(m) & $even(n)) => $odd(m+n)";

  3. def hasover "A t (t<=n) => T[i+t]=T[i+n+t]";
    Other ways to express this are certainly possible, but this is one of the simplest! 
  4. eval no_overlap "~E i,n (n>=1) & $hasover(i,n)";
    Here the pitfall to avoid is that we have to ensure n ≥ 1. 

  5. eval mirror "A i,n E j A t (t<n) => T[i+t]=T[(j+n)-(t+1)]";

  6. def equal_fac "A t (t<n) => T[i+t]=T[j+t]";
    The key insight to solve the recurrence property is to realize that recurrence is the same as saying that for every occurrence of a string at position i there is another occurrence of the same string at position j > i. So we say that: 

    eval recurrent "A i,n E j j>i & $equal_fac(i,j,n)";

  7. We can try various increasing values of c using "doubling search": 
    eval c1 "A i,n E j (j<=n) & $equal_fac(i,j,n)";
eval c2 "A i,n E j (j<=2*n) & $equal_fac(i,j,n)";
eval c4 "A i,n E j (j<=4*n) & $equal_fac(i,j,n)";
eval c8 "A i,n E j (j<=8*n) & $equal_fac(i,j,n)";
    The first three all give FALSE while the last one gives TRUE. Now we can do binary search in the interval [4,8] to find the smallest value. 
    eval c6 "A i,n E j (j<=6*n) & $equal_fac(i,j,n)";
eval c5 "A i,n E j (j<=5*n) & $equal_fac(i,j,n)";
    So 6 is the optimal integer value. Actually one can prove with Walnut that 6n – 13 is the optimal bound for n ≥ 3, in the sense that (a) anything smaller won't work for all n ≥ 3, and (b) the bound 6n – 13 is achieved infinitely often. Try that! 
  8. def squarelen "n >= 1 & E i A t (t< n) => T[i+t]=T[i+n+t]";
    The resulting automaton looks like the following:

    From this the theorem is easy to see: there is a square xx in the Thue-Morse sequence with |x| = n if and only if n is either a power of 2, or 3 times a power of 2. 

  9. eval hasfibsquare "?msd_fib E i,n n>=1 & A t (t < n) => F[i+t]=F[i+t+n]";
eval hasfibcube "?msd_fib E i,n n>=1 & A t (t < 2*n) => F[i+t]=F[i+t+n]";
eval hasfib4th "?msd_fib E i,n n>=1 & A t (t < 3*n) => F[i+t]=F[i+t+n]";
    The first two return TRUE, while the last returns FALSE. Actually the "real" bound is (5+√5)/2, but this takes more work to prove with Walnut! 
  10. eval prob1 "?msd_fib E M A N (N > M) => E m,n,x,y m>=1 & n>=1 & $phin(m,x) & $phin(n,y) & N=x+y";
eval prob2 "?msd_fib E M A N (N>M) => E m,n,x,y m>=1 & n>=1 & $phi2n(m,x) & $phi2n(n,y) & N=x+y";
eval prob3 "?msd_fib E M A N (N>M) => E m,n,p,x,y,z m>=1 & n>=1 & p>=1 & $phi2n(m,x) & $phi2n(n,y) & 
   $phi2n(p,z) & N=x+y+z";