Trotter-Weil 层级的并层级是可判定的

有限幺半群的簇 DA 拥有大量不同的刻画，范围从双变量一阶逻辑 $\text{FO}^2$ 到无歧义多项式。为了研究 DA 子簇的结构，Trotter 和 Weil 考虑了有限幺半群簇与带（即幂等幺半群）的交集。幂等幺半群的簇已被充分理解并完全分类。Trotter 和 Weil 证明，对于每个带簇 $V$，在 DA 内部存在唯一的最大簇 $W$，使得其与带的交集产生给定的带簇 $V$。这些最大簇 $W$ 定义了 Trotter-Weil 层级。该层级是无限的且穷尽了 DA；由带簇诱导，它自然具有锯齿形状。在他们的论文中，Trotter 和 Weil 证明了该层级的角点和交层级是可判定的。在本文中，我们为 Trotter-Weil 层级的每个并层级给出了一个 $\omega$-项的单一恒等式；这导出了可判定性。此外，我们证明了并层级与随后的交层级并不重合。Almeida 和 Azevedo 已证明 $\mathcal{R}$-平凡和 $\mathcal{L}$-平凡有限幺半群的并是可判定的；这是 Trotter-Weil 层级的第一个非平凡并层级。我们将此结果扩展到 Trotter-Weil 层级的其他并层级。在论文末尾，我们给出了两个应用。首先，我们证明了确定性和共确定性乘积的层级是可判定的。其次，我们证明了无歧义区间逻辑的方向交替深度是可判定的。