pith. sign in

arxiv: 2512.06466 · v2 · pith:PJ42CHL4new · submitted 2025-12-06 · 💻 cs.LO · cs.FL

A finer reparameterisation theorem for MSO and FO queries on strings

L\^e Th\`anh D\~ung Nguy\^en , Pawe{\l} Parys This is my paper

Pith reviewed 2026-05-25 07:45 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords monadic second-order logicfirst-order logicqueries on stringsreparameterisationdefinabilityfinite wordsoutput cardinalitystring interpretations
0
0 comments X

The pith

If an MSO query on binary strings has O(#0s × #1s) results, each result is MSO-definably recoverable from one 0-position, one 1-position and finite data.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves a reparameterisation theorem for monadic second-order k-ary queries on finite words. It shows that when the number of results on binary strings is bounded by a constant times the product of the counts of 0s and 1s, each result tuple can be selected by an MSO formula that uses one position of each symbol together with a fixed finite amount of auxiliary data. The same statement holds when the query is restricted to first-order logic and aperiodic monoids. As a direct consequence the paper establishes that dimension minimisation is possible for first-order string-to-string interpretations.

Core claim

For an MSO k-ary query on finite words, an output cardinality bound of the form O(|A| · |B|) for two symbol classes A and B implies that every output tuple is the value of an MSO-definable function applied to one position from A, one position from B, and a fixed finite datum. The identical statement holds for first-order queries over aperiodic monoids, which in turn yields the folklore claim that every first-order string-to-string interpretation admits a dimension-minimal form.

What carries the argument

The reparameterisation theorem that converts an output-size bound into MSO-definable selection from two symbol positions plus finite auxiliary data.

Load-bearing premise

The precise asymptotic bound O(#0s × #1s) on the number of results is the condition that permits each result to be recovered by an MSO formula from one 0-position, one 1-position and finite data.

What would settle it

An MSO query on binary strings whose result set has size at most C·#0s·#1s for some constant C, yet for which no MSO formula exists that maps each result to a 0-position, a 1-position and a finite datum.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper establishes a reparameterisation theorem for monadic second-order (MSO) k-ary queries on finite words. It shows that if the number of results of such a query on binary strings is O(#0s × #1s), then each result can be MSO-definably identified from a 0-position, a 1-position and some finite data. The proofs also cover the first-order (FO) case via aperiodic monoids and include a proof of the folklore theorem that dimension minimisation holds for first-order string-to-string interpretations.

Significance. If the central implication holds, the result refines the relationship between output cardinality bounds and logical definability for queries on strings, providing a tool for parameter reduction in MSO and FO interpretations. This strengthens the theory of logical transducers and automata on words by linking asymptotic bounds directly to definable reparameterisations, with the FO/aperiodic case adding breadth.

minor comments (2)
  1. [Abstract] The abstract states the main claim clearly but the manuscript should include an explicit statement of the finite data (e.g., a fixed tuple of constants or a parameter from a finite set) in the theorem formulation to avoid ambiguity in the reparameterisation.
  2. The transition between the MSO case and the FO/aperiodic-monoid case would benefit from a dedicated subsection or lemma that isolates the additional assumptions needed for the FO result.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our paper, the assessment of its significance, and the recommendation for minor revision. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper states a theorem establishing that an MSO (or FO) k-ary query on words satisfying the O(#0s × #1s) cardinality bound admits an MSO-definable reparameterisation from one 0-position, one 1-position and finite data. This is presented as a direct implication resting on the standard semantics of MSO/FO logic and monoid interpretations; the abstract and description contain no equations, fitted parameters, or self-citations that reduce the central claim to its own inputs by construction. The derivation is therefore self-contained against external logical definitions.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available, so no free parameters, axioms, or invented entities can be extracted from the text.

pith-pipeline@v0.9.0 · 5637 in / 1037 out tokens · 39181 ms · 2026-05-25T07:45:51.862412+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

6 extracted references · 6 canonical work pages · 2 internal anchors

  1. [1]

    String-to-String Interpretations with Polynomial-Size Output

    Mikołaj Bojańczyk, Sandra Kiefer, and Nathan Lhote. String-to-string interpretations with polynomial-size output. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece , pages 106:1--106:14, 2019. Technical report with appendix: https://arxiv.org/abs/1905.13190. https://doi.org/10.4230/LIPIcs...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.4230/lipics.icalp.2019.106 2019

  2. [2]

    Polyregular Functions

    Mikołaj Bojańczyk. Polyregular functions, 2018. https://arxiv.org/abs/1810.08760 arXiv:1810.08760

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  3. [3]

    Transducers of polynomial growth (invited talk)

    Mikołaj Bojańczyk. Transducers of polynomial growth (invited talk). In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , pages 1:1--1:27. ACM , 2022. https://doi.org/10.1145/3531130.3533326 doi:10.1145/3531130.3533326

    work page doi:10.1145/3531130.3533326 2022

  4. [4]

    On the growth rates of polyregular functions

    Mikołaj Bojańczyk. On the growth rates of polyregular functions. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , 2023. https://doi.org/10.1109/LICS56636.2023.10175808 doi:10.1109/LICS56636.2023.10175808

    work page doi:10.1109/lics56636.2023.10175808 2023

  5. [5]

    Optimization of string transducers

    Gaëtan Douéneau-Tabot. Optimization of string transducers . PhD thesis, Université Paris Cité, November 2023. URL: https://theses.hal.science/tel-04690881

    work page 2023

  6. [6]

    The structure of polynomial growth for tree automata/transducers and mso set queries, 2025

    Paul Gallot, Nathan Lhote, and Lê Thành Dũng N T5 guyễn . The structure of polynomial growth for tree automata/transducers and mso set queries, 2025. https://arxiv.org/abs/2501.10270 arXiv:2501.10270

    work page arXiv 2025