Automatic Sequences and Zip-Specifications

DOI10.1109/LICS.2012.44zbMATH Open1361.68155arXiv1201.3251OpenAlexW2040381387WikidataQ130985165 ScholiaQ130985165MaRDI QIDQ2986809FDOQ2986809

Clemens Grabmayer, Lawrence S. Moss, Jan Willem Klop, Dimitri Hendriks, Jörg Endrullis

Publication date: 16 May 2017

Published in: 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: We 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. For example, the Thue-Morse sequence is obtained by the `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. We establish 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. 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. 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.

Full work available at URL: https://arxiv.org/abs/1201.3251

zbMATH Keywords

coalgebraautomatic sequencesterm rewritingdynamic logicstreamsequational specifications

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Automata sequences (11B85) Abstract data types; algebraic specification (68Q65)

Cited In (7)

• A Final Coalgebra for k-regular Sequences
• Linearization of automatic arrays and weave specifications
• Adapting behaviors via reactive synthesis
• Checking equivalence of corecursive streams: an inductive procedure
• A Complete Logic for Behavioural Equivalence in Coalgebras of Finitary Set Functors
• Title not available (Why is that?)
• A complete logic for behavioural equivalence in coalgebras of finitary set functors

This page was built for publication: Automatic Sequences and Zip-Specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2986809)