Macro tree transducers, attribute grammars, and MSO definable tree translations

A characterization is given of the class of tree translations definable in monadic second-order logic (MSO), in terms of macro tree transducers. The f irst main result is that the MSO definable tree translations are exactly th ose tree translations realized by macro tree transducers (MTTs) with regula r look-ahead that are single use restricted. For this the single use restri ction 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 restrictin g 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 M TT, whereas the finite copying restriction is a more liberal, dynamic restr iction on the derivations of an MTT. (C) 1999 Academic Press.