Preprints by Jan Willem Klop
- 294
-
«Automatic Sequences and Zip-Specifications»
igitur archive March 20 2012We consider infinite sequences of symbols, also known as streams, and the decidability question for equality of streams defined in a restricted format. 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 in alternating order, starting with the first stream; e.g., for the streams defined by {zeros = 0 : zeros, ones = 1 : ones, alt = 0 : 1 : alt} we have zip(zeros, ones) = alt. 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)}.
Our analysis of such systems employs both term rewriting and coalgebraic techniques. We establish decidability for these zip-specifications, employing bisimilarity of observation graphs based on a suitably chosen cobasis. The importance of zip-specifications resides in their intimate connection with automatic sequences. The analysis leading to the decidability proof of the `infinite word problem' for zip-specifications, yields a new and simple characterization of automatic sequences. Thus we obtain for the binary zip that a stream is 2-automatic iff its observation graph using the cobasis (hd,even,odd) is finite. Here odd and even have the usual recursive definition: even(a : s) = a : odd(s), and odd(a : s) = even(s). The generalization to zip-k specifications and their relation to k-automaticity is straightforward. In fact, zip-specifications can be perceived as a term rewriting syntax for automatic sequences. Our study of zip-specifications is placed in an even wider perspective by employing the observation graphs in a dynamic logic setting, leading to an alternative characterization of automatic sequences.
We further obtain a natural extension of the class of automatic sequences, obtained by `zip-mix' specifications that use zips of different arities in one specification (recursion system). 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.
We also show that equivalence is undecidable for a simple extension of the zip-mix format with projections like even and odd. However, it remains open whether zip-mix specifications have a decidable equivalence problem. - 268
-
«Productivity of stream definitions»
igitur archive November 2008We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called ‘productive’ if it can be evaluated continually in such a way that a uniquely determined stream in constructor normal form is obtained as the limit. Whereas productivity is undecidable for stream definitions in general, we show that it can be decided for ‘pure’ stream definitions. For every pure stream definition the process of its evaluation can be modelled by the dataflow of abstract stream elements, called ‘pebbles’, in a finite ‘pebbleflow net(work)’. And the production of a pebbleflow net associated with a pure stream definition, that is, the amount of pebbles the net is able to produce at its output port, can be calculated by reducing nets to trivial nets.
- 166
-
«Diagram Techniques for Confluence»
igitur archive July 1996We develop diagram techniques for proving confluence in abstract reductions systems. The underlying theory gives a systematic and uniform framework in which a number of known results, widely scattered throughout the literature, can be understood. These results include Newman's Lemma (1942), Lemma 3.1 of Winkler and Buchberger (1985), the Hindley-Rosen Lemma (1964), the Request Lemmas of Staples (1975), the Strong Confluence Lemma of Huet (1980) and the Lemma of De Bruijn (1978).