219 Pages
English
Gain access to the library to view online
Learn more

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

Gain access to the library to view online
Learn more
219 Pages
English

Description

Technische Universitat MunchenInstitut fur InformatikOn Normalization andType Checking forTree TransducersDipl.-Inform. Sylvia FrieseVollst andiger Abdruck der von der Fakult at fur Informatik derTechnischen Universit at Munc hen zur Erlangung des akademischenGrades einesDoktors der Naturwissenschaften (Dr. rer. nat.)genehmigten Dissertation.Vorsitzender: Univ.-Prof. Alfons Kemper, Ph.D.Prufer der Dissertation: 1. Dr. Helmut Seidl2. Dr. Klaus U. Schulz,Ludwig-Maximilians-Universit at Munc henDie Dissertation wurde am 24.03.2011 bei der TechnischenUniversit at Munc hen eingereicht und durch die Fakult at furInformatik am 07.07.2011 angenommen.AbstractTree transducers are an expressive formalism for reasoning about tree structureddata. Practical applications range from XSLT-like document transformationsto translations of natural languages. Important problems for transducers are todecide whether two transducers are equivalent, to construct normal forms, givesemantic characterizations, and type checking, i.e., to check whether the pro-duced outputs satisfy given structural constraints. This thesis addresses theseproblems for important classes of tree transducers. Constructive solutions areprovided and classes of transducers for which these algorithms run in polynomialtime, are identi ed.Equivalence testing, normalization, and semantic characterization are oftensolved together by the use of a Myhill-Nerode theorem.

Subjects

Informations

Published by
Published 01 January 2011
Reads 15
Language English
Document size 3 MB

Exrait

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 Transducers . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5 Partition 37
5.1 Partitions of DBTTs . . . . . . . . . . . . . . . . . . . . . . . . . 40
5.1.1 Finite Index . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.1.2 Path-Finite Partition . . . . . . . . . . . . . . . . . . . . . 43
5.2 Bottom-Up Partition . . . . . . . . . . . . . . . . . . . . . . . . . 48
5.2.1 Trim P . . . . . . . . . . . . . . . . . . . . . . . . 49
5.2.2 Proper Partition . . . . . . . . . . . . . . . . . . . . . . . 50
5.2.3 Earliest P . . . . . . . . . . . . . . . . . . . . . . . 54
5.2.4 Uni ed Partition . . . . . . . . . . . . . . . . . . . . . . . 58
5.2.5 Congruence Relation . . . . . . . . . . . . . . . . . . . . . 64
5.2.6 Minimal Partition . . . . . . . . . . . . . . . . . . . . . . 72
viiviii CONTENTS
6 Myhill-Nerode Theorem 83
6.1 Minimization of Bottom-Up Transducers . . . . . . . . . . . . . . 84
6.1.1 Proper Transducers . . . . . . . . . . . . . . . . . . . . . 85
6.1.2 Earliest T . . . . . . . . . . . . . . . . . . . . . 89
6.1.3 Uni ed Transducers . . . . . . . . . . . . . . . . . . . . . 93
6.1.4 Minimal T . . . . . . . . . . . . . . . . . . . . . 100
6.2 From Transducers to Partitions . . . . . . . . . . . . . . 108
6.3 From Partitions to Minimal Transducers . . . . . . . . . . . . . . 111
7 Conclusion 131
7.1 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
II Type Checking Tree Walking Transducers 133
8 Introduction 135
9 Tree Walking Transducers 139
9.1 Notes and References . . . . . . . . . . . . . . . . . . . . . . . . . 147
10 Type Checking 149
10.1 Type Checking by Forward Type Inference . . . . . . . . . . . . 149
10.2 Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150
10.3 Basic Properties of BTAs . . . . . . . . . . . . . . . . . . . . . . 152
10.4 Notes and References . . . . . . . . . . . . . . . . . . . . . . . . . 153
11 Type Checking of Tree Walking Transducers 155
11.1 Intersecting 2TTs with Output Types . . . . . . . . . . . . . . . 155
11.2 Deciding Emptiness of 2TTs . . . . . . . . . . . . . . . . . . . . . 157
11.3 E cient Subcases . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
11.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
11.5 Notes and References . . . . . . . . . . . . . . . . . . . . . . . . . 167
12 Macro Tree Walking Transducers 169
12.1 Type Checking 2MTTs . . . . . . . . . . . . . . . . . . . . . . . . 174
12.2 Deciding Emptiness of 2MTTs . . . . . . . . . . . . . . . . . . . 178
12.3 Input-Linear 2MTTs . . . . . . . . . . . . . . . . . . . . . . . . . 178
12.4 Notes and References . . . . . . . . . . . . . . . . . . . . . . . . . 182
13 Macro Forest Walking Transducers 185
13.1 Intersecting 2MFTs with Output Types . . . . . . . . . . . . . . 188
13.2 Deciding Emptiness of 2MFTs . . . . . . . . . . . . . . . . . . . 192
13.3 Notes and References . . . . . . . . . . . . . . . . . . . . . . . . . 194
14 Conclusion 197Chapter 1
Introduction
Tree transducers are a formal model to describe transformations of tree struc-
tured data. Such transformations occur in various elds. Early formal ap-
proaches were inspired by compiler development. Internal representations (of
the syntax or the semantics) of programs are trees. Separating the syntax of
a program language from assigning semantics to the source language led to
the analysis of the model of syntax-directed translations [Iro61]. More gener-
ally, program analysis, like evaluations and optimizations, are tree transforma-
tions. Further works also based on the theory of tree languages, nite tree au-
tomata, and the associated algebraic formulation (e.g., [Tha69, Rou70, Tha70,
+CDG 07]). The formal models of tree transducers are more abstract. Input
trees are not only syntax trees of program languages, but trees over a ranked
alphabet. Already in the year 1969, Thatcher stated that the abstract models
of tree transducers are not only generalizations of transformations of program
languages, but also of translations of natural languages:
\It appears to be an area with considerable promise of application
to questions of syntax and semantics of programming languages and
to the analysis of natural languages." [Tha69]
In the beginning of this century, tree transducers were rediscovered in the con-
text of natural language processing [KG05]. In addition to the string- and
phrase-based models, tree-based transformation models are considered in many
areas, e.g., in machine translation [Wu97, ADB00, Eis03], i.e., automatic trans-
lation from one natural language (like Chinese) into another (like English). Fur-
ther tasks are, for instance, automatically answering a human-language question
[HG01, EM03a], generating natural language from information stored in com-
puter databases [BR00], and automatic summarization [MM99, KM02], i.e., to
automatically abstract the relevant information of (multiple) documents.
Due to the inherent syntax and semantics of natural language, sentences
will be represented by syntax trees, for instance like the two in Figure 1.1.
A transformation model may, for instance, translate passive voice into active
12 1. Introduction
(a) Passive voice: \This book was read by many people."
(b) Active voice: \Many people read this book."
Figure 1.1: Syntax trees of the sentence \This book was read by many people."
and its active counterpart \Many people read this book.".