A finer reparameterisation theorem for MSO and FO queries on strings

TL;DR

This paper presents a new theorem for monadic second-order and first-order queries on strings, showing how results can be characterized and minimized using MSO-definable parameters, with implications for logic and automata theory.

Contribution

It introduces a finer reparameterisation theorem for MSO and FO queries on strings, extending existing results and providing new insights into query characterization and dimension minimization.

Findings

Results can be MSO-definably identified from specific positions and finite data.

The theorem applies to both MSO and FO queries, including aperiodic monoids.

Dimension minimization holds for first-order string-to-string interpretations.

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.