Polyregular functions on unordered trees of bounded height

TL;DR

This paper studies injective first-order interpretations on bounded height unordered trees, proving the decidability of their equivalence problem and developing a calculus for such functions, with applications to graph classes of bounded tree-depth.

Contribution

It introduces a decidable framework for equivalence of injective first-order tree interpretations and a typed calculus for deriving such functions.

Findings

Equivalence problem for these functions is decidable.

A calculus of typed functions and combinators is developed.

Results extend to MSO interpretations on bounded tree-depth graphs.

Abstract

We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. given two such interpretations, one can decide whether, for every input tree, the two output trees are isomorphic. We also give a calculus of typed functions and combinators which derives exactly injective first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus. As an application, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree-depth. In all cases studied in this paper, first-order logic and MSO have the same expressive power, and hence all results apply also to MSO interpretations.