Addition-Invariant FO and Regularity
Addition-Invariant FO and Regularity
复制标题
加法不变 FO 和正则性
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
L. Segoufin
中科院分区：
文献类型：
--
作者：
Nicole Schweikardt;L. Segoufin
我们考虑这样的公式，除了词汇表中的符号外，还可以使用两个指定的符号\prec和+，这两个符号必须被解释为线性顺序及其相关的加法。如果对于初始词汇表的每个固定解释，其结果与\prec和+的特定解释无关，则称为加法不变量公式。本文研究了有限串类上加法不变一阶逻辑+-inv-FO的表达能力。我们的第一个主要结果给出了可在+-inv-FO中定义的正则语言的特征：我们证明了这些语言正是可在FO中定义的带有额外谓词的语言，简称为“lm”，用于测试字符串模取某个固定数字的长度。我们的第二个主要结果表明，在+-inv-FO中可定义的所有语言，即有界的、可交换的或确定性上下文无关的语言，都是正则的。作为这两个主要结果的直接结果，我们得到了+-inv-FO在有限有色集合类上等价于FO（lm）。我们的证明方法包括Ehrenfeucht-Fraïssé游戏，代数自动机理论的工具，以及半线性集的推理。
We consider formulas which, in addition to the symbols in the vocabulary, may use two designated symbols \prec and + that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the initial vocabulary, its result is independent of the particular interpretation of \prec and +. This paper studies the expressive power of addition invariant first-order logic, +-inv-FO, on the class of finite strings. Our first main result gives a characterization of the regular languages definable in +-inv-FO: we show that these are exactly the languages definable in FO with extra predicates, denoted by “lm” for short, for testing the length of the string modulo some fixed number. Our second main result shows that every language definable in +-inv-FO, that is bounded or commutative or deterministic context-free, is regular. As an immediate consequence of these two main results, we obtain that +-inv-FO is equivalent to FO(lm) on the class of finite colored sets. Our proof methods involve Ehrenfeucht-Fraïssé games, tools from algebraic automata theory, and reasoning about semi-linear sets.