WALNUT VERIFICATION -- "Meta-Automatic Sequences"
==================================================

This directory contains the Walnut input files needed to verify computationally
the algorithmic claims of the paper "Meta-Automatic Sequences".

Tested with Walnut 7.1.

Contents
--------

  Word_Automata_Library/
    QMA.txt      base-4 MSB-first DFAO for the sequence Q  (3 states)
    M1A.txt      base-4 MSB-first DFAO for the sequence M1 (4 states)
    M2A.txt      base-4 MSB-first DFAO for the sequence M2 (4 states)

  Command_Files/
    verify_basic_recurrences.txt
        Verifies that the three DFAOs satisfy the defining recurrences of
        Q, M1, M2, together with the balancedness property a(2n)+a(2n+1)=1.
    verify_factor_complexity_QMA.txt
        Verifies the right-special factor structure of Q for all n >= 16.
    verify_factor_complexity_M2A.txt
        Verifies the right-special factor structure of M2 for all n >= 8.


Installation
------------

  1. Copy the three files in Word_Automata_Library/ to Walnut's
     Word Automata Library directory.

  2. Copy the three files in Command_Files/ to Walnut's Command Files
     directory.

  3. In a Walnut session, run:

         load verify_basic_recurrences.txt;
         load verify_factor_complexity_QMA.txt;
         load verify_factor_complexity_M2A.txt;

Each "eval" command should return TRUE.

If Walnut 7.1 reports a file-encoding error, save the .txt files as
UTF-16 (see the Walnut manual).


What each file checks
---------------------

verify_basic_recurrences.txt
  Eight "eval" commands. Each asks Walnut to decide a universal first-order
  statement over the natural numbers; the expected answer is TRUE in every
  case.

    qma_rec       Q(4n)=Q(n), Q(4n+1)!=Q(n), Q(4n+2)=Q(2n), Q(4n+3)!=Q(2n)
    qma_balance   Q(2n)+Q(2n+1) = 1 for all n
    m1a_rec01     M1(4n)=M1(n) and M1(4n+1)!=M1(n)
    m1a_rec23     The case-split form of M1(4n+2) = M1(2n+1-M1(n))
                  and M1(4n+3) = 1 - M1(4n+2)
    m1a_balance   M1(2n)+M1(2n+1) = 1 for all n
    m2a_rec01     The case-split form of M2(4n) = M2(2n+M2(n))
                  and M2(4n+1) = 1 - M2(4n)
    m2a_rec23     The case-split form of M2(4n+2) = M2(2n+1-M2(n))
                  and M2(4n+3) = 1 - M2(4n+2)
    m2a_balance   M2(2n)+M2(2n+1) = 1 for all n

verify_factor_complexity_QMA.txt
  Defines length-n factor equality, canonical first occurrence, and the
  set of length-n right-special factors of Q. The three final "eval"
  commands check, for all n >= 16:

    rs2_qma(n) <=> qma_rs2_range(n)
    rs3_qma(n) <=> qma_rs3_range(n)
    rs4_qma(n) <=> qma_rs4_range(n)

  where the right-hand sides encode the three ranges in
  Proposition (Q-complete) of the paper. Expected output: TRUE for all
  three.

verify_factor_complexity_M2A.txt
  Analogous to the file above but for M2. The right-special-factor count
  for M2 takes only the values 2 and 4, so only two checks are needed.
  The two final "eval" commands check, for all n >= 8:

    rs2_m2a(n) <=> m2a_rs2_range(n)
    rs4_m2a(n) <=> m2a_rs4_range(n)

  Expected output: TRUE in both cases.

  The helpers pow2_k0_4, pow2_k1_4, pow2_k2_4 detect powers of 2 by their
  exponent residue modulo 3, since the piecewise behaviour of
  Proposition (M2-complete) depends on this residue.


Expected runtime
----------------

  verify_basic_recurrences.txt        seconds
  verify_factor_complexity_QMA.txt    a few minutes
  verify_factor_complexity_M2A.txt    a few minutes

Memory usage is moderate. If Walnut runs out of heap, increase the JVM
heap size (e.g. java -Xmx8g -jar Walnut.jar).
