Macro Tree Transducers, Attribute Grammars, and MSO Definable Tree Translations
Macro Tree Transducers, Attribute Grammars, and MSO Definable Tree Translations
复制标题
宏树转换器、属性语法和 MSO 可定义树转换
DOI：
--
复制
发表时间：
1999
影响因子：
1
通讯作者：
S. Maneth
中科院分区：
文献类型：
--
作者：
J. Engelfriet;S. Maneth
给出了一元二阶逻辑中可定义的树平移类在宏树换能器上的表征。第一个主要结果是，MSO可定义的树翻译正是那些由具有常规前瞻性的宏树转换器（mtt）实现的树翻译，这些树翻译受单一使用的限制。因此，从属性语法中已知的单一使用限制被推广到mtt。由于MTT在常规预检下是封闭的，这意味着每个MSO可定义的树翻译都可以由MTT实现。第二个主要结果是，MSO可定义树翻译类也可以通过将常规预查的mtt限制为有限复制来获得，即要求每个输入子树只处理有限次。单次使用限制是对MTT规则的一种相当强的静态限制，而有限复制限制是对MTT派生的一种更自由的动态限制。
A characterization is given of the class of tree translations definable in monadic second-order logic (MSO), in terms of macro tree transducers. The first main result is that the MSO definable tree translations are exactly those tree translations realized by macro tree transducers (MTTs) with regular look-ahead that are single use restricted. For this the single use restriction known from attribute grammars is generalized to MTTs. Since MTTs are closed under regular look-ahead, this implies that every MSO definable tree translation can be realized by an MTT. The second main result is that the class of MSO definable tree translations can also be obtained by restricting MTTs with regular look-ahead to be finite copying, i.e., to require that each input subtree is processed only a bounded number of times. The single use restriction is a rather strong, static restriction on the rules of an MTT, whereas the finite copying restriction is a more liberal, dynamic restriction on the derivations of an MTT.