Automatic Sequences and Zip-Specifications
We consider infinite sequences of symbols, also known as streams, and the decidability question for equality of streams defined in a restricted format. (Some formats lead to undecidable equivalence problems.) This restricted format consists of prefixing a symbol at the head of a stream, of the stream function `zip', and recursion variables. Here `zip' interleaves the elements of two streams alternatingly. As a term rewriting rule, `zip' can be defined as follows:
zip(x:s,y:t) = x:y:zip(s,t)
The celebrated Thue--Morse sequence is obtained by the succinct `zip-specification'
M = 0 : X
X = 1 : zip(X,Y)
Y = 0 : zip(Y,X)
It turns out that the class of streams definable by zip-specifications is precisely the class of 2-automatic sequences. The generalization to k-automatic sequences is immediate using zipk interleaving k arguments:
zipk(x1:s1,...,xk:sk) = x1:...:xk::zipk(s1,...,sk)
Thus zip-specifications can be perceived as a term rewriting syntax for automatic sequences.
Our analysis, based on term rewriting and coalgebraic techniques, moreover leads to a coalgebraic characterization of automatic sequences. This characterization allows for playfully discovering whether a given stream is automatic.
Let s be a stream, and assume we want to check whether s is 2-automatic.
We construct a graph whose nodes are streams and whose edges are labelled with `even' and `odd'.
Initially the graph consists only of the root node s.
For every node t, we add outgoing edges `even' and `odd' to streams even(t) and odd(t), respectively,
where even(t) is the subsequence of t consisting of the elements at even positions,
and odd(t) is the subsequence of t consisting of elements at odd positions.
If even(t) or odd(t) are not yet nodes of the graph, then we add these.
Then the stream s is 2-automatic if and only if the construction stops
and thus the graph is finite.
Using term rewriting, `even' and `odd' can be defined in terms of each other as follows:
even(a : s) = a : odd(s)
odd(a : s) = even(s).
Of course this game can also be played using representatives of streams as the nodes
instead of streams themselves. If streams are defined by term rewriting, then terms
are a natural choice for these representatives. For example, for the zip-specification
defining Thue-Morse above, we obtain the following observation graph:
If we replace in this graph `even` by 0 and `odd' by 1, we obtain a 2-DFAO that
generates the Thue-Morse sequence M as automatic sequence.
As a natural extension of the class of automatic sequences,we also consider `zip-mix' specifications that use zips of different arities in one specification. For example:
Z = zip2(0:Z,Y)
Y = 1:zip3(Z,Y,0:Z)
The corresponding notion of automaton employs a state-dependent input-alphabet, with a number representation (n)_A = dm...d0 where the base of digit di is determined by the automaton A on input di-1...d0.
★ Research Questions / Open Problems
- Are there streams definable by zip-mix specifications that are not morphic?
- Is equivalence of zip-mix specifications still decidable?
For further reading, we refer to: