Paper: Tree Canonization and Transtive Closure (at LICS 1995)
Abstract
We prove that tree isomorphism is not expressible in the language (FO + TC + COUNT). This is surprising since in the presence of ordering the language captures NL, whereas tree isomorphism and canonization are in L ([L90]). To prove this result we introduce a new Ehrenfeucht- Fraisse game for transitive closure logics. As a corresponding upper bound, we show that tree canonization is expressible in (FO + COUNT)[log n]. The best previous upper bound had been (FO + COUNT)[n^O(1)]. ([DM90]). The lower bound remains true for bounded-degree trees, and we show that for bounded-degree trees counting is not needed in the upper bound. These results are the first separations of the unordered versions of the logical languages for NL, AC^1, and ThC^1. Our results were motivated by a conjecture in [EI94a] that (FO + TC + COUNT + 1LO) = NL, i.e., that a one-way local ordering sufficed to capture NL. We disprove this conjecture, but we prove that a TWO-WAY local ordering does suffice, i.e., (FO + TC + COUNT + 2LO)=NL.
BibTeX
@InProceedings{EtessamiImmerman-TreeCanonizationand, author = {Kousha Etessami and Neil Immerman}, title = {Tree Canonization and Transtive Closure}, booktitle = {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)}, year = {1995}, month = {June}, pages = {331--341}, location = {San Diego, CA, USA}, publisher = {IEEE Computer Society Press} }