ToPSのご案内

告知です． MSO Logic definable tree transducers (MSOTT) というのは，合成で閉じている Tree Transducer の中でも大きなクラスの一つで， 大雑把に言えば一回参照の属性文法と同じ表現力を持っています． この手の結果は，属性文法合成に基づく融合（descriptional composition）の発展に役立つかもしれません． 時間のある方は是非お越し下さい．

Event

The 33rd Tokyo Programming Seminar (ToPS)

Time

February 22nd, 15:00-16:30

Place

Room 534, Engineering Building 14 of Faculty of Engineering, University of Tokyo

Speaker

Sebastian Maneth (NICTA Ltd and UNSW Sydney, Australia)

Title

MSO Logic and Tree Transducers with Decidable Equivalence (joint work with Joost Engelfriet and Helmut Seidl)

Abstract

This talks shows how old results from automata and formal language theory can be used to solve problems on XML transformations which are of current interest.

Tree transducers are formal models to describe translations on labeled, ordered trees. They originate from the early days in compilers, but have gained applicability through recent interest in semi-structured data on the web, and XML in particular. Even though tree transducers are fairly old and mature models, not much is known about the decidability of their equivalence problem, i.e., the question whether two given transducers realize the same (tree) translation. The problem is undecidable for non-deterministic transducers, even already in case of word transducers. In this talk I want to discuss two recent advances on the equivalence problem for tree transducers.

(1) Equivalence is decidable for deterministic MSO Logic definable tree transducers. Using MSO logic to describe tree translations gives rise to a particular natural and robust class of translations with many good properties (such as, for instance, closure under sequential composition). The proof of the decidability is based on the fact that images of context-free graph languages under MSO translations are Parikh (i.e., their Parikh vectors form a semi-linear set) and hence constitutes a nice application of old formal language theory results to problems that are of current interest in semistructured/XML databases.

(2) Equivalence of deterministic top-down tree transducers can be decided in polynomial time, if the transducers are in "earliest normalform". Many useful XML transformations can be formulated through deterministic top-down tree (DT) transducers. It has been known for a long time (Zoltan Esik 1981) that equivalence of DT transducers is decidable. Nothing however has been known about the complexity of this problem. The "earliest" property constitutes a canonical form for DT transducers in which each transducer emits any output symbol as early in a translation as possible. If a DT transducer is total then an equivalent earliest transducer can be obtained in polynomial time too. We expect that the concept of earliest transducers has more applications, for instance, to the problem of streaming XML transformations.