What about the other direction? What languages are expressible w/ RNNs & LTLs that require exponential blowup for transformers?
i.e. the blowup is only exponential in one direction.
Edit: Actually nevermind. If UHAT could be compiled into LTL w/ polynomial overhead then that would also work for the languages that have exponential overhead in LTL but since they don't there is a strict separation.