WALNUT 4 Additional Documentation


This new version of Walnut has many new capabilities added by Kai Hsiang Yang (kh2yang@uwaterloo.ca), with direction from Jeffrey Shallit (shallit@uwaterloo.ca).

The new capabilities are as follows:

#1:  Quantification over Z and negative bases
#2:  The "split" command
#3:  The "rsplit" command
#4:  The "join" command
#5:  Allowing arithmetic on sequence values
#6:  New quantifier I
#7:  Bug fixes

#1:   One can now quantify over Z (all integers) instead of just N (natural numbers) in some cases.  This is accomplished by means of negative bases, where one can represent members of Z in base (-k) or
negaFibonacci base.

To use negative bases, use 

?msd_neg_k   
?lsd_neg_k

To use the negaFibonacci system, use

?msd_neg_fib
?lsd_neg_fib

To represent unary minus, use the underscore so that (for example) _5 represents the
number -5.

Example:

eval tmp "?msd_neg_2 _a + _5 = c":

When one uses a negative base, then quantification like E or A refers to all of Z, not just N.

Currently there is no support for negative bases for the Tribonacci and Ostrowski numeration
systems.


#2:  The "split" command.   This allows the user to take a DFAO defined in a negative
base and "split" it into two or more DFAO's that work in a positive base, handling the positive and negative numbers separated.  The syntax is

split <new> <old> [<sign1>] ... [<signn>]

Here <old> is the name of a DFAO (possibly with multiple inputs) that takes inputs in
a negative base, and produces a new DFAO with name <new> in the corresponding positive
base, that handles the numbers with the given sign(s) of inputs.

For example if N is a DFAO taking inputs (x,y,z) where x is represented in msd_neg_2
y in msd_neg_3, and z in msd_2, then the command

split M N [+] [-] []

produces a new DFAO (Word Automaton) M such that M[x][y][z] = N[x'][y'][z], where
x is represented in msd_2, y is represented in msd_3, z is represented in msd_2,
and M[x][y][z] = N[x'][y'][z], and [x]_2 = [x']_{-2} and [y]_3 = [-y']_{-3}.


#3:  The "rsplit" command.    This is a sort of inverse to "split".   Given a DFAO with input in a positive base, this produces a DFAO in the corresponding negative
base.    The syntax is

rsplit <new> [<sign1>] ... [<signn>] <old>

For example, if M is a DFAO with inputs in msd_2, msd_3, and msd_2 then

rsplit N [+] [-] [] M

produces a new DFAO (Word Automaton) M such that N[x'][y'][z] = M[x][y][z] where x' is in msd_neg_2, x is in msd_2, y' is in msd_neg_3, y in msd_3, [x']_-2 = [x]_2, and [y']_-3 = [-y]_3. Moreover N[x'][y'][z] = 0 when x' < 0 or y' > 0.


#4:   The "join" command.   Given multiple DFAO's (Word Automata), this produces
a DFAO with output equal to the first non-zero output.  The syntax is

join <new> <DFAO1> ... <DFAOn>

For example, if N1, N2, N3 are DFAO's with two inputs, then

join M N1[a][b] N2[b][c] N3[a][c]

produces a new DFAO M which, on inputs (a,b,c) outputs 

N1[a][b] if it is nonzero

N2[b][c] if it is nonzero, but N1[a][b] is zero

N3[a][c] if it is nonzero, but both N1[a][b] and N2[b][c] are zero.


#5:   Arithmetic on automaton values.  Previously the outputs of automata were
treated as "second-class" objects that one could not (for example) add; one could
only compare them.   Now you can use the ouputs in arithmetic expression.

Here is the allowable syntax:

- T[a]+c, T[a]-c T[a]*c, _(T[a]), T[a]/c, c/T[a] where c is any constant or alphabet symbol (i.e., 1, 3, @1, @3). We require c to be non-zero if we write T[a]/c. We require T to have non-zero outputs if we write c/T[a]. We must be in a negative base to use negative constants (i.e., _2).

- T[a]+b, T[a]-b T[a]*b, b/T[a] where b is a variable. We require T to have non-zero outputs if we write b/T[a]. We can also replace b with any other expression (i.e., T[a]*(d-e)).

- T[a]+M[b], T[a]-M[b], T[a]*M[b], T[a]/M[b] where M is a DFAO with one input. We required M to have non-zero ouputs if we write T[a]/M[b].


#6:   The new quantifier "I", meaning
"there exist infinitely many".    This joins A and E as special quantifier symbols.

For example, you can now write

eval tmp "?msd_2 I x,y x+y>=z":

Using the I quantifier always returns the true or false automaton, even if you don't quantify over all free variables.


#7:  Bug fixes.  An obscure bug that sometimes prevented arithmetic expressions with two occurrences
of the same variable, such as "n=x+x", from being processed correctly, has been fixed.