Polyregular functions form a robust class of string-to-string functions with polynomial growth, as evidenced by Bojanczyk (2018). This class admits numerous descriptions and enjoys several closure properties. Most notably, polyregular functions are regularity reflecting (\ie the inverse image of a regular language is regular). In this work, we propose a robust class of string-to-string functions with exponential growth which we call expregular functions. We consider the following three models for describing them: - MSO set interpretations, which extend MSO interpretations (one of the models capturing polyregular functions), by operating on monadic variables instead of tuples of first-order variables; - yield-Hennie machines, which are branching one-tape Turing machines with bounded visit; and - Ariadne transducers, a new model of 2-way pushdown machines with a bounded visit restriction. Our main contribution is a translation from MSO set interpretations to yield-Hennie machines, which are known to be regularity reflecting (Dartois, Nguy\~{ê}n, Peyrat 2026). In particular this establishes that MSO set interpretations are regularity reflecting, which in turn settles a major conjecture about automatic structures: every automatic $ω$-word has a decidable MSO theory. Yield-Hennie machine directly translate to Ariadne transducers, and our second contribution is to prove that Ariadne transducers also translate to MSO set interpretations, thus establishing the equivalence of the three models. This is obtained by showing that Ariadne automata -- the automaton model corresponding to Ariadne transducers -- recognise regular languages.
翻译:多正则函数构成了一类具有多项式增长的字符串到字符串映射的健壮类,如Bojanczyk(2018)所述。该类拥有多种描述方式,并具备若干封闭性质,其中最显著的是多正则函数具有正则性反射性(即正则语言的原像仍为正则语言)。在本文中,我们提出了一类具有指数增长的字符串到字符串映射的健壮类,称为指数正则函数。我们考虑以下三种模型来描述它们:- MSO集合解释(扩展了MSO解释——捕捉多正则函数的模型之一),通过操作一元变量而非一阶变量元组实现;- yield-Hennie机器,一种具有有界访问的分支单带图灵机;- Ariadne换能器,一种具有有界访问限制的双向下推机新模型。我们的主要贡献是将MSO集合解释转化为yield-Hennie机器,已知后者具有正则性反射性(Dartois, Nguyễn, Peyrat 2026)。这特别确立了MSO集合解释的正则性反射性,进而解决了一个关于自动结构的主要猜想:每个自动ω-词都有可判定的MSO理论。yield-Hennie机器可直接转化为Ariadne换能器,我们的第二个贡献是证明Ariadne换能器也能转化为MSO集合解释,从而建立三种模型的等价性。这是通过证明Ariadne自动机——对应于Ariadne换能器的自动机模型——能够识别正则语言来实现的。