一句话：证明有界高度无序树上单射一阶解释的等价问题可判定，并给出精确刻画它的类型化演算。
论文研究有界高度无序树之间的单射一阶解释，这类函数的输出规模为多项式，因为一个输出结点可由输入结点的 k 元组表示。作者证明其等价问题可判定：给定两个此类解释，可判定是否对每个输入树，两个输出树都同构。为刻画该函数类，他们提出一个类型化函数与组合子演算，类型构造子包括积、余积和多重集 monad，并证明该演算恰好导出此类单射一阶解释；借助树到树的等价性结果，演算的等价问题也可判定。作为应用，还得到有界树深图类之间一阶解释的等价问题可判定；由于所涉情形中一阶逻辑与 MSO 表达能力相同，结论也适用于 MSO 解释。
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.
@article{paperbot2656,
title = {Polyregular Functions on Unordered Trees of Bounded Height},
author = {Mikołaj Bojańczyk and Bartek Klin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632887}
}