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 [] ... []
Here is the name of a DFAO (possibly with multiple inputs) that takes inputs in
a negative base, and produces a new DFAO with name 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 [] ... []
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 ...
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.