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.