On Normalization and Type Checking for Tree Transducers [Elektronische Ressource] / Sylvia Friese. Gutachter: Klaus U. Schulz ; Helmut Seidl. Betreuer: Helmut Seidl

Sujets

• Wissenschaft

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2011
• Nombre de lectures: 15
• Langue: English
• Poids de l'ouvrage: 3 Mo

Extrait

Technische Universitat Munchen
Institut fur Informatik
On Normalization and
Type Checking for
Tree Transducers
Dipl.-Inform. Sylvia Friese
Vollst andiger Abdruck der von der Fakult at fur Informatik der
Technischen Universit at Munc hen zur Erlangung des akademischen
Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Alfons Kemper, Ph.D.
Prufer der Dissertation: 1. Dr. Helmut Seidl
2. Dr. Klaus U. Schulz,
Ludwig-Maximilians-Universit at Munc hen
Die Dissertation wurde am 24.03.2011 bei der Technischen
Universit at Munc hen eingereicht und durch die Fakult at fur
Informatik am 07.07.2011 angenommen.Abstract
Tree transducers are an expressive formalism for reasoning about tree structured
data. Practical applications range from XSLT-like document transformations
to translations of natural languages. Important problems for transducers are to
decide whether two transducers are equivalent, to construct normal forms, give
semantic characterizations, and type checking, i.e., to check whether the pro-
duced outputs satisfy given structural constraints. This thesis addresses these
problems for important classes of tree transducers. Constructive solutions are
provided and classes of transducers for which these algorithms run in polynomial
time, are identi ed.
Equivalence testing, normalization, and semantic characterization are often
solved together by the use of a Myhill-Nerode theorem. This identi es neces-
sary and su cient semantic properties for transformations de nable by a speci c
class of transducers. The theorem also implies that a unique normal form of
those transducers exists. Moreover, it implies that, given a transducer, the nor-
mal transducer can be constructed. This immediately leads to the question:
Are there classes of tree transducers for which a Myhill-Nerode theorem ex-
ists? We give an a rmative answer for the class of deterministic bottom-up
tree transducers. A semantic characterization of transformations de nable by
these transducers is presented, and, moreover, it is evidenced that for every
deterministic bottom-up tree transducer, a unique equivalent transducer can
be constructed, which is minimal. The construction is based on a sequence of
normalizing transformations, which, among others, guarantee that non-trivial
output is produced as early as possible. For a deterministic bottom-up trans-
ducer where every state produces either none or in nitely many outputs, the
minimal transducer can be constructed in polynomial time.
One of the useful properties of tree walking transducers is decidability of
type checking: Given a transducer and input and output types, it can be checked
statically whether each document adhering to the input type is necessarily trans-
formed by the transducer into documents adhering to the output type. Here,
a \type" means a regular set of trees speci ed by a nite-state tree automa-
ton. Usually, type checking of tree transducers is extremely expensive; already
for simple top-down tree transducers it is known to be EXPTIME-complete.
Are there expressive classes of tree for which type checking can be
performed in polynomial time? Most of the previous approaches are based on
inverse type inference. In contrast, the approach presented here uses forward
iiiiv
type inference. This means to infer, given a transducer and an input type, the
corresponding set of output trees. In general, this set is not a type, i.e., it is
not regular. However, it can be decided if its intersection with a given type
is empty. Using this approach, we show that type checking can be performed
in polynomial time if (1) the output type is speci ed by a deterministic tree
automaton, and (2) the tree walking transducer visits every input node only a
bounded number of times. If the is additionally equipped with ac-
cumulating call-by-value parameters, then the complexity of type checking also
depends (exponentially) on the number of such parameters. For this case, a
fast approximative type checking algorithm is presented, based on context-free
tree grammars. Finally, the approach is generalized from trees to forest walk-
ing transducers, which additionally support concatenation as a built-in output
operation.Zusammenfassung
Baumub ersetzer sind ein ausdrucksstarker Formalismus, um baumstrukturier-
te Daten zu analysieren. Praktische Anwendungen reichen von XSLT-artigen
Dokumentumstrukturierungen zu Ubersetzungen naturlic her Sprache. Bedeu-
tende Problemstellungen fur Ubersetzer sind, zu entscheiden, ob zwei Ubersetzer
aquivalent sind, eine Normalform konstruiert werden kann, es eine semantische
Charakterisierung gibt und Typub erprufung, d.h., zu ub erprufen, ob die erzeug-
ten Ausgaben gegebene strukturelle Bedingungen erfullen. Diese Dissertation
befasst sich mit diesen Fragen fur wesentliche Baumub ersetzerklassen. Wir stel-
len konstruktive L osungen bereit und identi zieren Ubersetzerklassen, fur die
diese Algorithmen nur polynomielle Zeit ben otigen.
Aquivalenztest, Normalisierung und semantische Charakterisierung sind oft
mittels eines Myhill-Nerode Theorems gemeinsam osbar.l Es zeigt notwendige
und hinreichende semantische Eigenschaften fur Ubersetzungen einer bestimm-
ten Klasse von Ubersetzern auf und impliziert eine eindeutige Normalform fur
diese Ubersetzer. Zus atzlich beinhaltet das Theorem, dass der entsprechen-
de Ubersetzer in Normalform aus einem beliebigen Ubersetzer konstruiert wer-
den kann. Es stellt sich also die Frage, ob es Klassen von Baumub ersetzern
gibt, fur die ein Myhill-Nerode Theorem existiert. Fur deterministische Auf-
w arts-Baumub ersetzer (deterministic bottom-up tree transducers) geben wir
eine positive Antwort. Wir pr asentieren eine semantische Charakterisierung fur
Ubersetzungen, die durch solche Ubersetzer beschrieben werden k onnen. Des-
weiteren zeigen wir, dass fur jeden deterministischen Aufw arts-Baumub ersetzer
ein eindeutiger aquivalenter Ubersetzer konstruiert werden kann, der minimal
ist. Diese Konstruktion basiert auf einer Folge von Normalisierungen, welche
unter anderem garantieren, dass nicht-triviale Ausgaben so fruh wie m oglich
erzeugt werden. Wenn jeder Zustand eines deterministischen Aufw arts-Baum-
ub ersetzers entweder keine oder unendlich viele Ausgaben produziert, kann der
minimale Ubersetzer in polynomieller Zeit konstruiert werden.
Eine der nutzlic hen Eigenschaften von Zwei-Wege-Baumub ersetzern (tree
walking transducers) ist, dass das Problem der Typub erprufung entscheidbar
ist: Wenn ein Ubersetzer und ein Eingabe- sowie ein Ausgabetyp vorgegeben
sind, kann statisch gepruft werden, ob der Ubersetzer Dokumente, die dem Ein-
gabetyp entsprechen, grunds atzlich in Dokumente des Ausgabetyps ub ersetzt.
Dabei verstehen wir unter \Typ" eine regul are Baummenge, die durch einen
endlichen Automaten spezi ziert ist. Normalerweise ist Typub erprufung von
vvi
Baumub ersetzern extrem aufw andig. Es ist bekannt, dass dieses Problem bereits
fur einfache Abw arts-Baumub ersetzer (top-down tree transducers) EXPTIME-
vollst andig ist. Es stellt sich die Frage, ob es ausdrucksstarke Baumub ersetzer-
klassen gibt, fur die Typub erprufung in polynomieller Zeit durchgefuh rt werden
kann. Die meisten bisherigen Ans atze basierten auf inverser Typinferenz. Wir
benutzen hier den entgegengesetzen Ansatz mittels vorw artsgerichteter Typin-
ferenz. Das hei t, fur einen gegebenen Ubersetzer und einen Eingabetyp leiten
wir die Menge aller zugehorigen Ausgabeb aume her. Im Allgemeinen ist diese
Menge kein Typ, d.h., es ist keine regul are Menge. Trotzdem ist es entscheid-
bar, ob die Schnittmenge mit einem gegebenen Ausgabetyp leer ist. Mit diesem
Ansatz zeigen wir, dass man Typub erprufung in polynomieller Zeit durchfuh-
ren kann, wenn (1) der Ausgabetyp mittels eines deterministischen Automaten
gegeben ist und (2) der Zwei-Wege-Baumub ersetzer jeden Knoten eines Einga-
bebaums h ochstens begrenzt oft besucht. Wenn der Baumub ersetzer zus atzlich
mit Wertparametern (call-by-value) ausgestattet ist, h angt die Komplexit at aus-
serdem (exponentiell) von der Anzahl der Parameter ab. In diesem Fall wird
ein schneller approximativer Typub erprufungsalgorithm us pr asentiert, der auf
kontextfreien Baumgrammatiken basiert. Zum Schlu wird dieser Ansatz von
B aumen auf Zwei-Wege- Waldub ersetzer verallgemeinert. Diese Ubersetzer er-
lauben zus atzlich Konkatenation als Operation auf Ausgabeb aumen.Contents
1 Introduction 1
1.1 Tree Transducers . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2 Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.5 Own Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2 Preliminaries 13
2.1 Trees and Forests . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Nodes and Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Tree Monoid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.4 Trees with State Calls . . . . . . . . . . . . . . . . . . . . . . . . 22
I Myhill-Nerode Theorem for DBTTs 23
3 Introduction 25
4 Bottom-Up Tree Transducers 29
4.1 Trim