Compressed Tree Canonization

TL;DR

This paper demonstrates that isomorphism and bisimulation equivalence of unordered trees represented by SLT grammars are decidable in polynomial time, extending known results to unordered and unrooted trees, with complexity bounds for non-linear grammars.

Contribution

It extends polynomial-time decidability of tree isomorphism to unordered and unrooted trees represented by SLT grammars, including non-linear cases with higher complexity bounds.

Findings

Polynomial-time decidability of unordered tree isomorphism from SLT grammars.

Polynomial-time decidability of bisimulation equivalence for unrooted unordered trees.

Complexity bounds for non-linear SLT grammars showing PSPACE-hardness and EXPTIME membership.

Abstract

Straight-line (linear) context-free tree (SLT) grammars have been used to compactly represent ordered trees. It is well known that equivalence of SLT grammars is decidable in polynomial time. Here we extend this result and show that isomorphism of unordered trees given as SLT grammars is decidable in polynomial time. The proof constructs a compressed version of the canonical form of the tree represented by the input SLT grammar. The result is generalized to unrooted trees by "re-rooting" the compressed trees in polynomial time. We further show that bisimulation equivalence of unrooted unordered trees represented by SLT grammars is decidable in polynomial time. For non-linear SLT grammars which can have double-exponential compression ratios, we prove that unordered isomorphism is PSPACE-hard and in EXPTIME. The same complexity bounds are shown for bisimulation equivalence.