Logic in Computer Science (LICS 1995)

Paper: Tree Canonization and Transtive Closure (at LICS 1995)

Authors: Kousha Etessami Neil Immerman

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 Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {331-341},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }