Lics

IEEE Symposium on Logic in Computer Science

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}
 }