《Journal of Computer and System Sciences》：Languages structured by the subword order and length relations
编辑推荐：
研究人员考虑一个语言连同子词关系、关联两个词长度的二元关系以及正则谓词。对于此类结构，研究人员考虑由阈值计数量词与模计数量词对一阶逻辑的扩展。依赖于该语言、所使用的谓词以及逻辑片段，研究人员确定了四个可产生可判定理论的新组合。这些结果扩展了先前的结论，即仅考虑
研究人员考虑一个语言连同子词关系、关联两个词长度的二元关系以及正则谓词。对于此类结构，研究人员考虑由阈值计数量词与模计数量词对一阶逻辑的扩展。依赖于该语言、所使用的谓词以及逻辑片段，研究人员确定了四个可产生可判定理论的新组合。这些结果扩展了先前的结论，即仅考虑所有词构成的语言（不含长度关系）以及一阶逻辑片段的情形。
研究人员研究由子词关系（subword relation，亦称散乱子词关系）排序的词集合的逻辑性质，主要关注可获得可判定逻辑理论的一般情形。在引言部分，研究人员指出：仅就子词序而言，??-理论或Σ1-理论是可判定的，而????-理论或Σ2-理论是不可判定的；对于子词序连同正则谓词，二元变量理论可判定，而三元变量理论以及??-理论不可判定。因此，要获得可判定理论，必须显著限制一阶逻辑的表达力。为此，研究人员从四个方面细化分析：将论域从全部词限制到给定语言L；在结构中可能加入或不加入正则谓词或常量；除子词序外，还考虑表达两词长度差至少为给定常数?的谓词ld≥?；在逻辑中加入阈值计数量词与模计数量词，即考虑结构(L,?,(ld≥?)?≥0,(K∩L)K regular,(w)w∈L)的归约以及由阈值与模计数量词扩展一阶逻辑所得逻辑C+MOD的片段。
研究人员识别出四类新的可判定理论：（1）若L有界且为上下文无关语言，则整个结构的C+MOD-理论可判定（定理3.5）；（2）若L为正则语言，则整个结构的C+MOD2-理论可判定（推论4.17）；（3）若L为正则语言，则结构(L,?)的Σ1-理论可判定（定理5.1）；（4）若L为正则（可能无界）且几乎所有词对每个字母都含有不可忽略数量的出现，则结构(L,?,(w)w∈L)的Σ1-理论可判定（定理6.2）。这些结果的重要意义在于：它们扩展了此前仅考虑全部词构成的语言（不含长度关系）与一阶逻辑片段的可判定性结论，并刻画了子词序逻辑理论可判定与不可判定之间的部分边界。
在技术方法上，研究人员主要采用以下关键技术：利用Parikh定理、子词关系的有理性与Nivat定理，将有界上下文无关语言情形归约为(N,+)的FO+MOD(tuple)-理论；针对正则语言情形，建立无歧义有理关系（unambiguous rational relation）下正则语言对计数像的封闭性理论，并借助加权自动机（weighted automata）进行证明，进而给出C+MOD2的量词消去程序；对于Σ1-理论，证明每个有限偏序均可嵌入无界正则语言的子词序结构，其中用到本原词（primitive word）与前缀极大子词（prefix-maximal subword）的组合性质；对于带常量的Σ1-理论，进一步利用上述嵌入性质与良序（well-quasi-order）理论的组合论证。样本队列来源方面，本文为理论研究，未涉及样本队列。
研究结果部分：（1）含正则谓词的C+MOD-理论：研究人员证明了若L有界且上下文无关，则结构(L,?,(ld≥?)?∈N,(K∩L)K regular,(w)w∈L)的FO+MOD-理论可判定，方法是通过四个预备引理将长度差谓词、正则谓词交、子词关系与语言L分别归约为半线性集，从而将该结构解释到(N,+)中，再借助(N,+)的FO+MOD(tuple)-理论的可判定性得出结论。（2）含正则谓词的C+MOD2-理论：研究人员证明了若L为正则语言，则结构(L,?,(ld≥?)?∈N,(K∩L)K regular,(w)w∈L)的C+MOD2-理论可判定；为此先证明关系?∩ld≥?、?∩ld=?、∥∩ld≥?、∥∩ld=?为有效无歧义有理关系，再证明无歧义有理关系下正则语言对计数像封闭，进而建立C+MOD2的量词消去程序（引理4.15、定理4.16、推论4.17）。（3）Σ1-理论：研究人员证明了若L为正则语言，则(L,?)的Σ1-理论可判定；关键是通过自动机论证找到词x,u,v,z使得|u|=|v|、uv为本原词且x{u,v}?z?L，并证明每个有限偏序可嵌入({u,v}?,?)，从而将Σ1-语句的可满足性归约到有限偏序上的检验（定理5.1）。（4）带常量的Σ1-理论：研究人员证明了若L为无界正则语言且几乎所有词对每个字母都有不可忽略数量的出现，则(L,?,(w)w∈L)的Σ1-理论可判定；证明中利用L?w↑有限、L∩w↑无界且正则这一性质，将量词自由公式化为若干类文字的正布尔组合并检验其在有限偏序中的可满足性（定理6.2）。
讨论部分与结论：研究人员在开放问题中指出，本文未考虑复杂度问题；已知在piecewise-testable语言情形下C2-理论可在二重指数交替时间（线性多次交替）内判定，但现有技术无法处理模计数量词或任意正则语言；对于有界上下文无关语言情形，研究人员将FO+MOD-理论归约到(N,+)的FO+MOD(tuple)-理论（已知可在二重指数空间内判定），但未分析所得公式相对原公式的大小；此外，本文未给出新的不可判定性结果，并指出应寻找更多不可判定情形以缩小可判定与不可判定情形之间的差距。研究结论部分可译为：研究人员识别出与子词序相关的四类可判定理论；本文集中于这些正面结果，即未试图寻找新的不可判定理论；特别地，若能理解正则语言L的哪些性质决定结构(L,?,(w)w∈L)的Σ1-理论的可判定性，将是很有意义的（该理论对L=Σ?不可判定，而对例如L={ab,baa}?∪bb{abb}?可判定）；另一个开放问题涉及本文可判定性结果的复杂度。
