  We contribute to the study of formal languages that can be recognized by
transformer encoders. We focus on two self-attention mechanisms: (1) UHAT
(Unique Hard Attention Transformers) and (2) AHAT (Average Hard Attention
Transformers). UHAT encoders are known to recognize only languages inside the
circuit complexity class ${\sf AC}^0$, i.e., accepted by a family of poly-sized
and depth-bounded boolean circuits with unbounded fan-ins. On the other hand,
AHAT encoders can recognize languages outside ${\sf AC}^0$), but their
expressive power still lies within the bigger circuit complexity class ${\sf
TC}^0$, i.e., ${\sf AC}^0$-circuits extended by majority gates. We first show a
negative result that there is an ${\sf AC}^0$-language that cannot be
recognized by an UHAT encoder. On the positive side, we show that UHAT encoders
can recognize a rich fragment of ${\sf AC}^0$-languages, namely, all languages
definable in first-order logic with arbitrary unary numerical predicates. This
logic, includes, for example, all regular languages from ${\sf AC}^0$. We then
show that AHAT encoders can recognize all languages of our logic even when we
enrich it with counting terms. We apply these results to derive new results on
the expressive power of UHAT and AHAT up to permutation of letters (a.k.a.
Parikh images).
