The First-Order Theory of Ground Tree Rewrite Graphs

TL;DR

This paper investigates the computational complexity of the first-order theory of ground tree rewrite graphs, establishing upper and lower bounds and demonstrating the existence of structures with non-elementary theories.

Contribution

It provides tight complexity bounds for the first-order theory of ground tree rewrite graphs and shows the existence of fixed graphs with non-elementary theories.

Findings

Complexity of the first-order theory is in ATIME(2^{2^{poly(n)}},O(n))

Matching lower bounds show the theory is hard for ATIME(2^{2^{poly(n)}},poly(n))

Existence of fixed graphs with non-elementary first-order theories

Abstract

We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(2^{2^{poly(n)}},O(n)). Providing a matching lower bound, we show that there is some fixed ground tree rewrite graph whose first-order theory is hard for ATIME(2^{2^{poly(n)}},poly(n)) with respect to logspace reductions. Finally, we prove that there exists a fixed ground tree rewrite graph together with a single unary predicate in form of a regular tree language such that the resulting structure has a non-elementary first-order theory.