Polynomial closure and unambiguous product

This article is a contribution to the algebraic theory of automata, but it also contains an application to Buchi’s sequential calculus. The polynomial closure of a class of languagesC is the set of languages that are finite unions of languages of the formL0a1L1 ···anLn, where theai’s are letters and theLi’s are elements ofC. Our main result is an algebraic characterization, via the syntactic monoid, of the polynomial closure of a variety of languages. We show that the algebraic operation corresponding to the polynomial closure is a certain Mal’cev product of varieties. This result has several consequences. We first study the concatenation hierarchies similar to the dot-depth hierarchy, obtained by counting the number of alternations between boolean operations and concatenation. For instance, we show that level 3/2 of the Straubing hierarchy is decidable and we give a simplified proof of the partial result of Cowan on level 2. We propose a general conjecture for these hierarchies. We also show that if a language and its complement are in the polynomial closure of a variety of languages, then this language can be written as a disjoint union of marked unambiguous products of languages of the variety. This allows us to extend the results of Thomas on quantifier hierarchies of first-order logic.