Linear Recurrence Sequence Automata and the Addition of Abstract Numeration Systems
Olivier Carton, Jean-Michel Couvreur, Martin Delacourt, Nicolas Ollinger
TL;DR
The paper develops a framework to reason about arithmetic relations in abstract numeration systems using sequence automata whose edge weights are linear recurrence sequences, anchored in Dumont-Thomas numeration and substitutions. It proves that for Pisot recurrence polynomials the corresponding LRSA yield regular addition and enable conversions between ANSZ, with constructive methods to build the requisite automata. It provides a robust toolkit for producing automata that implement addition and cross-system conversions, and to compute Parikh vectors of fixpoint prefixes, under a Pisot regime. A practical pipeline, including the licofage prototype and Walnut integration, demonstrates mechanized verification and automated generation of these relations for complex numeration systems.
Abstract
Abstract numeration systems encode natural numbers using radix ordered words of an infinite regular language and linear recurrence sequences play a key role in their valuation. Sequence automata, which are deterministic finite automata with an additional linear recurrence sequence on each transition, are introduced to compute various $\mathbb{Z}$-rational non commutative formal series in abstract numeration systems. Under certain Pisot conditions on the recurrence sequences, the support of these series is regular. This property can be leveraged to derive various synchronized relations including a deterministic finite automaton that computes the addition relation of various Dumont-Thomas numeration systems and deterministic finite automata converting between various numeration systems. A practical implementation for Walnut is provided.