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 解释(捕获多项式正则函数的模型之一);- 产出-亨尼机,这是一种具有有界访问次数的分支单带图灵机;以及 - Ariadne 转换器,这是一种具有有界访问限制的新型双向下推机模型。我们的主要贡献是将 MSO 集合解释翻译为产出-亨尼机,而后者已知是正则性保持的(Dartois, Nguy\~{ê}n, Peyrat 2026)。这尤其确立了 MSO 集合解释是正则性保持的,从而解决了一个关于自动结构的主要猜想:每个自动 $ω$-字都具有可判定的 MSO 理论。产出-亨尼机可以直接翻译为 Ariadne 转换器,而我们的第二个贡献是证明 Ariadne 转换器也可以翻译为 MSO 集合解释,从而确立了这三种模型的等价性。这是通过证明 Ariadne 自动机——对应于 Ariadne 转换器的自动机模型——识别正则语言来实现的。