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.
翻译:我们证明了有限单词上的一元二阶k元查询的一个定理。该定理可通过以下例子说明:如果二元字符串上的查询结果数量为O(0的个数×1的个数),则每个结果可以从一个0位置、一个1位置以及某些有限数据中通过MSO定义的方式识别。我们的证明还涵盖了一阶逻辑/非周期幺半群的情形。因此,我们可以陈述并证明如下众所周知的定理:字符串到字符串的一阶解释中维度最小化成立。