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. 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) The main results are as follows. We establish decidability of equivalence of zip-specifications, by employing bisimilarity of observation graphs based on a suitably chosen cobasis. Furthermore, our analysis, based on term rewriting and coalgebraic techniques, reveals an intimate connection between zip-specifications and automatic sequences. This leads to a new and simple characterization of automatic sequences. The study of zip-specifications is placed in a wider perspective by employing observation graphs in a dynamic logic setting, yielding yet another alternative characterization of automatic sequences. By the first characterization result, zip-specifications can be perceived as a term rewriting syntax for automatic sequences. For streams sigma the following are equivalent: (a) sigma can be specified using zip; (b) sigma is 2-automatic; and (c) sigma has a finite observation graph using the cobasis < hd, even, odd >. Here even and odd are defined by even(a : s) = a : odd(s), and odd(a : s) = even(s). The generalization to zip-k specifications (with zip-k interleaving k streams) and to k-automaticity is straightforward. 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. The corresponding notion of automaton employs a state-dependent input-alphabet, with a number representation (n)(A) = dm ... d(0) where the base of digit d(i) is determined by the automaton A on input d(i-1) ... d(0). Finally we show that equivalence is undecidable for a simple extension of the zip-mix format with projections analogous to even and odd.