Over finite words, there is a tight connection between the quantifier alternation hierarchy inside two-variable first-order logic FO~2 and a hierarchy of finite monoids: the Trotter-Weil Hierarchy. The various ways of climbing up this hierarchy include Mal'cev products, deterministic and co-deterministic concatenation as well as identities of ω-terms. We show that the word problem for ω-terms over each level of the Trotter-Weil Hierarchy is decidable; this means, for every variety V of the hierarchy and every identity u = v of ω-terms, one can decide whether all monoids in V satisfy u = v. More precisely, for every fixed variety V, our approach yields non-deterministic logarithmic space (NL) and deterministic polynomial time algorithms, which are more efficient than straightforward translations of the NL-algorithms. From a language perspective, the word problem for ω-terms is the following: for every language variety V in the Trotter-Weil Hierarchy and every language variety W given by an identity of ω-terms, one can decide whether V {is contained in} W. This includes the case where V is some level of the FO~2 quantifier alternation hierarchy. As an application of our results, we show that the separation problems for the so-called corners of the Trotter-Weil Hierarchy are decidable.
展开▼
