# Is equivalence of uniform AC0 decidable?

Is there a representation of the functions from $$\mathsf{DLogTime}$$-uniform $$\mathsf{AC}^0$$ for which equivalence is decidable?

Since the languages defined by nondeterministic pushdown automata belong to $$\mathsf{LogCFL}$$, and we know that their equivalence is not decidable, we know that there can be no representation of the functions from $$\mathsf{LogCFL}$$ for which equivalence would be decidable. Since $$\mathsf{AC}^0$$ is nearly the most powerful class which we still can separate from $$\mathsf{LogCFL}$$, learning that equivalence of $$\mathsf{AC}^0$$ is decidable should have no surprising consequences (at least I expect that if equivalence of $$\mathsf{TC}^0$$ were known to be decidable, then we could separate $$\mathsf{TC}^0$$ from $$\mathsf{LogCFL}$$).

Edit: Emil's comment hints that the answer is "no", but that this question did not define what it means by "representation" rigorously enough to allow any definite answer at all. Let me first try to guess why the answer is "no": Since length is $$\mathsf{DLogTime}$$ computable, it is probably possible to pad the input at will, by writting the padded length in binary at the beginning, and hence reducing the equivalence problem for $$\mathsf{CFL}$$ to the equivalence problem for $$\mathsf{DLogTime}$$.

Given the paragraph about $$\mathsf{LogCFL}$$ above, one should expect that this question interprets "representation" in a way that is compatible with that conclusion. But that is not the case. (But making my guess about padding the input rigorous would nevertheless answer this question.) It assumes that "representation" simply has its intuitive meaning. So we have strings over some alphabet, we can computationally decide whether a string is "valid", every language from $$\mathsf{DLogTime}$$-uniform $$\mathsf{AC}^0$$ is represented by some "valid" string, and given a "valid" string, it is possible to computationally enumerate the language represented by that string.

• What, exactly, do you mean by “a representation”? Equivalence is certainly undecidable for common natural representations of AC^0 (e.g., clocked O(log n)-time alternating turing machines with a constant number of alternations, or FO(+,.)-formulas). However, let $\{L_n:n\in\omega\}$ be any bijective enumeration of AC^0-languages, and represent $L_n$ by $n$. Then equivalence is decidable (as it amounts to identity). – Emil Jeřábek Jun 29 '19 at 19:31
• @EmilJeřábek I was mostly thinking about representations by $\mathsf{FO}$ formulas, because they at least have a form where it might be possible that there is some algorithm for deciding whether they are satisfied by the same finite structures. The representation should at least allow to computationally decide membership in the language represented by a specific member. Not sure whether this will be possible for $L_n$ if you are given $n$, for your bijective enumeration of AC^0. – Thomas Klimpel Jun 29 '19 at 20:25
• I'm with @EmilJeřábek: I'm not sure the question is well-defined. You mention that PDA equivalence is undecidable—sure thing, but, along the line's of Emil's argument, there are representations of CFLs for which equivalence is decidable. If your question is about FO, you should word it this way (in which case, equivalence is surely undecidable). – Michaël Cadilhac Jun 29 '19 at 22:40
• @MichaëlCadilhac If the answer should be "yes, equivalence is decidable for AC0, it is even decidable for CFLs", then that would also help me. Do those representations of CFLs allow to computationally decide membership in the language represented by a specific member, or at least computationally enumerate that language? (If not, then I don't understand why it should be considered to be a reasonable representation.) Since I often struggle with descriptive complexity theory, I don't want to limit this question to $\mathsf{FO}$. – Thomas Klimpel Jun 30 '19 at 4:33
• If not, then I don't understand why it should be considered to be a reasonable representation: exactly my point. So, you need to tell us what you consider a reasonable representation. – Emil Jeřábek Jun 30 '19 at 7:02