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 w the following are equivalent:(a) w can be specified using zip;(b) w is 2-automatic; and (c) w has a finite observation graph using the cobasis (head, 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 = d_m ... 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.
展开▼
