Given an $\mathbb{N}$-weighted tree automaton, we give a decision procedure for exponential vs polynomial growth (with respect to the input size) in quadratic time, and an algorithm that computes the exact polynomial degree of growth in cubic time. As a special case, they apply to the growth of the ambiguity of a nondeterministic tree automaton, i.e. the number of distinct accepting runs over a given input. Our time complexities match the recent fine-grained lower bounds for these problems restricted to ambiguity of word automata. We deduce analogous decidability results (ignoring complexity) for the growth of the number of results of set queries in Monadic Second-Order logic (MSO) over ranked trees. In the case of polynomial growth of degree $k$, we also prove a reparameterization theorem for such queries: their results can be mapped to $k$-tuples of input nodes in a finite-to-one and MSO-definable fashion. This property of MSO set queries leads directly to a generalization of the dimension minimization theorem for string-to-string polyregular functions. Our generalization applies to MSO set interpretations from trees, which subsume (as we show) tree-walking tree transducers and invisible pebble tree-to-string transducers. Finally, with a bit more work we obtain the following: * a new, short and conceptual proof that macro tree transducers (MTTs) of linear growth compute only tree-to-tree MSO transductions; * a procedure to decide polynomial size-to-height increase for MTTs and compute the degree. The paper concludes with a survey of a wide range of related work, with over a hundred references.
翻译:给定一个$\mathbb{N}$加权树自动机,我们提出了一种在二次时间内判定指数增长与多项式增长(相对于输入规模)的决策过程,以及一种在三次时间内计算精确多项式增长次数的算法。作为特例,这些方法适用于非确定性树自动机的歧义性增长,即给定输入上不同接受运行的数量。我们的时间复杂度与近期针对词自动机歧义性问题的细粒度下界相匹配。我们推导出关于带秩树上单子二阶逻辑(MSO)集合查询结果数量增长的类似可判定性结果(忽略复杂度)。对于次数为$k$的多项式增长情况,我们还证明了此类查询的重参数化定理:其查询结果可以通过有限对一且MSO可定义的方式映射到输入节点的$k$元组。MSO集合查询的这一性质直接导出了字符串到字符串多正则函数维度最小化定理的推广。我们的推广适用于从树出发的MSO集合解释,其包含(如我们所证明的)树行走树转换器和隐形卵石树到字符串转换器。最后,通过进一步工作我们获得:* 关于线性增长的宏树转换器(MTT)仅计算树到树MSO转换的新颖、简洁且概念性证明;* 判定MTT多项式规模到高度增长并计算其次数的过程。本文最后对广泛的相关工作进行了综述,包含逾百篇参考文献。