A finer reparameterisation theorem for MSO and FO queries on strings
Lê Thành Dũng Nguyên, Paweł Parys
TL;DR
The paper proves a finer reparameterisation theorem for MSO and FO queries on finite strings: if the number of φ-solutions on a word w is O of the product of the η_i-solution counts, then there exists an MSO/FO formula ψ that defines a total functional relation from φ-solutions to η-solutions, with each η-output having only O(1) φ-preimages. The authors achieve this by combining monoid recognisability, Simon's factorisation forests, and pumping arguments with Hall's theorem to bound preimages and construct ψ in MSO (and in FO in the aperiodic case). The results extend to FO with aperiodicity and lead to dimension minimisation for string-to-string interpretations, enabling an ℓ-dimensional FO interpretation to implement an ℓ-th root of a given interpretation. The approach unifies MSO and FO cases and builds on prior work (PolyregularGrowth, GaetanPhD) to provide a coherent framework for reparameterising MSO/FO queries on words.
Abstract
We show a theorem on monadic second-order k-ary queries on finite words. It may be illustrated by the following example: if the number of results of a query on binary strings is O(number of 0s $\times$ number of 1s), then each result can be MSO-definably identified from a 0-position, a 1-position and some finite data. Our proofs also handle the case of first-order logic / aperiodic monoids. Thus we can state and prove the folklore theorem that dimension minimisation holds for first-order string-to-string interpretations.