The logical approach to automatic sequences. Exploring combinatorics on words with Walnut. (English) Zbl 1544.68005

Shallit, Jeffrey

London Mathematical Society Lecture Note Series 482. Cambridge: Cambridge University Press (ISBN 978-1-108-74524-6/pbk; 978-1-108-77526-7/ebook). xv, 358 p. (2023).

An infinite sequence is automatic if its \(n\)th element can be computed by a finite automaton from the representation of \(n\) in a convenient numeration system. A classical example is the Thue-Morse sequence \(\mathbf t\) over two letters, which is defined by setting \(\mathbf t_n\) to be the parity of the number of ones in the binary expansion of \(n\).
The title of the reviewed book is admitted to be a bit of a pun. Indeed, it is logical to study automatic sequences using automata, but it is also logical to exploit formal logic in studying them “automatically”, an approach largely missing in the classical monograph [J.-P. Allouche and J. Shallit, Automatic sequences. Theory, applications, generalizations. Cambridge: Cambridge University Press (2003; Zbl 1086.11015)]. The basic fact underlying the logical approach is that Presburger arithmetic \(\mathrm{Th}(\mathbb N,+)\) is decidable. What’s more, for every first-order formula of Presburger arithmetic (with free variables) one can construct a finite automaton which accepts (\(b\)-base representations of) exactly those tuples of numbers that satisfy the formula. The same holds for some reasonable generalizations concerning in particular the choice of representation of numbers. The key requirement is that the operation of addition can be recognized by a finite automaton reading numbers in the given representation (that is, the automaton accepts the triple \((x,y,z)\) if and only if \(x + y = z\)).
As a theoretical fact, this has been known since 1929 (cf. [M. Presburger and D. Jacquette, Hist. Philos. Log. 12, No. 2, 225–233 (1991; Zbl 0741.03027)]). However, only recently an open-source automatic prover, written originally by Hamoon Mousavi and called Walnut [H. Mousavi, “Automatic theorem proving in Walnut”, Preprint, arXiv:1603.06017], has been published, which makes clear that the prohibitive worst-case complexity of the decision is not relevant for a rich variety of practical problems. This has led to a series of papers reproving in a straightforward “automatic” way a large number of results that were obtained in the literature often by complex and tedious arguments.
The current book is a concise introduction to various ingredients of this remarkable field, ranging from logical foundations, through automata and number-theoretic background to a practical introduction to Walnut itself. After a brief opening chapter, there are five chapters dealing with words and sequences, number representations, automata, automatic sequences, and first-order logic, respectively. Number representations presented in Chapter 2 include, in addition to the most obvious \(b\)-base representation, also the Fibonacci, the tribonacci and the Pell representations, as well as the general Ostrowski representation, which is based on the continued fraction expansion of some irrational number and is closely related to Sturmian words. The first part of the book culminates in Chapter 7, which is a kind of a guide to using Walnut. Chapter 8 is an extensive catalog of examples of properties of automatic sequences that can be expressed in first-order logic, and hence processed by Walnut. Four concluding chapters provide more advanced material. Chapter 9 discusses regular sequences, which are more general than automatic sequences since they can contain infinitely many values. Nevertheless, regular sequences admit linear representation in terms of matrices which, for instance, allows one to count the number of factors of length \(n\) satisfying a particular first-order property. Calculating such a linear representation is another feature of Walnut. Chapter 10 deals with synchronized sequences, which correspond to relational representation of certain functions. Chapter 11 discusses additive number theory: the problem of obtaining numbers as sums of a certain form, in the spirit of Lagrange’s four-square theorem. Finally, Chapter 12 is about paperfolding sequences, giving an example of a parameterized family of (uncountable many) automatic sequences some properties of which can be examined for the whole family at once.
In the whole book, the reader will find many examples and exercises (there are 164 of the latter, unfortunately numbered continuously within the whole book, not per chapters), as well as open research problems (at least one of them already solved), and a rich bibliography. Moreover, the author maintains a page with errata, and with the Walnut code used in the book. Mostly, the book is well readable and entertaining. Although it is to some extent a compilation of previously published sources, only rarely one can feel seams between chapters (for example, a more explicit link between Fibonacci and Pell representations and the general Ostrowski representation would be beneficial).
Altogether, the book is an excellent and self-contained source for current and prospective Walnut users. It represents compelling evidence that first-order properties of automatic sequences should be proved by pen and paper never more. Moreover, it is a convenient reference for a large audience interested in various aspects of the related theory.

Reviewer: Štěpán Holub (Praha)

MSC:

68-02	Research exposition (monographs, survey articles) pertaining to computer science
03D05	Automata and formal grammars in connection with logical questions
11B85	Automata sequences
11U05	Decidability (number-theoretic aspects)
68R15	Combinatorics on words
68V15	Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Keywords:

automatic sequences; first-order logic; automatic provers; Walnut

Citations:

Zbl 1086.11015; Zbl 0741.03027

Software:

OEIS; Walnut; Pecan