索引语言的切片闭合与带计数约束的单词方程

索引语言是形式语言理论中的一个经典概念。作为二阶下推自动机的等价语言，它在更高阶模型检查中受到广泛关注。不幸的是，计数性质对索引语言而言极难判定：迄今为止关于非正则计数性质的所有结果都显示出不可判定性。本文着手研究索引语言(其 Parikh 像的)切片闭合的研究。切片是向量自然数集合，满足若包含 $u,u+v,u+w$ 则必包含 $u+v+w$。我们的主要结果是，给定索引语言 $L$，可计算其 Parikh 像包含最小切片的半线性表示。我们提出了两个应用。首先，可以计算索引语言 Parikh 像满足的所有仿射关系。这在特定方面上正好回答了 Kobayashi 的问题：在给定索引语言中，每个单词是否具有相同数量的 $a$ 和 $b$ 是否可判定。作为第二个应用，我们展示了带有有理约束和计数约束类单词方程(系统)的可判定性：这些约束允许我们寻找计数函数(由自动机定义)不为零的解。例如，可以判定带有有理约束的单词方程是否存在解，其中变量 $X$ 和 $Y$ 中出现的次数不同。