Macro Tree Translations of Linear Size Increase are MSO Definable
Macro Tree Translations of Linear Size Increase are MSO Definable
复制标题
线性大小增加的宏树翻译可由 MSO 定义
DOI：
10.1137/s0097539701394511
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
S. Maneth
中科院分区：
文献类型：
--
作者：
J. Engelfriet;S. Maneth
第一个主要结果是，如果宏树的翻译是线性增长的，即，如果每个输出树的大小线性地受到相应输入树的大小的限制，那么翻译是MSO可定义的（即，在一元二阶逻辑中是可定义的）。从宏树换能器的角度，给出了MSO可定义树平移的新特征：它们正是线性增长的宏树平移。第二个主要结果是，给定一个宏树换能器，可以确定其翻译是否是MSO可定义的，如果是，则可以构造一个等效的MSO换能器。属性语法也有类似的结果，它们定义了宏树翻译的一个子类。
The first main result is that if a macro tree translation is of linear size increase, i.e., if the size of every output tree is linearly bounded by the size of the corresponding input tree, then the translation is MSO definable (i.e., definable in monadic second-order logic). This gives a new characterization of the MSO definable tree translations in terms of macro tree transducers: they are exactly the macro tree translations of linear size increase. The second main result is that given a macro tree transducer, it can be decided whether or not its translation is MSO definable, and if it is, then an equivalent MSO transducer can be constructed. Similar results hold for attribute grammars, which define a subclass of the macro tree translations.