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.

翻译：本文研究输入和输出均为有界高度树的内射一阶解释。由于一阶解释可利用k元组输入节点表示单个输出节点，相应函数具有多项式输出规模。我们证明此类函数的等价问题可判定：即给定两个这样的解释，可判定对于每个输入树，两个输出树是否同构。我们还给出一个带类型函数与组合子的演算，该演算恰好导出有界高度无序树的内射一阶解释。此演算基于类型系统，其类型构造子包括积、余积及多重集单子。借助树到树解释的相关结果，该演算的等价问题可判定。作为应用，我们证明对于具有有界树深度的图类，其上的内射一阶解释等价问题可判定。本文研究的所有情形中，一阶逻辑与MSO具有相同的表达能力，因此所有结论也适用于MSO解释。