A formal model for an expressive fragment of XSLT.
The extension of the eXtensible Style sheet Language (XSL) by variables and passing of data values between template rules has generated a powerful XML query language: eXtensible Style sheet Language Transformations (XSLT). An informal introduction to XSTL is given, on the bases of which a formal model of a fragment of XSLT is defined. This formal model is in the spirit of tree transducers, and its semantics is defined by rewrite relations. It is shown that the expressive power of the fragment is already beyond that of most other XML query languages. Finally, important properties such as termination and closure under composition are considered.
Introduction
XSL [6] is a current W3C [8] proposal for an XML extensible stylesheet lan-
guage. Its original primary role was to allow users to write transformations of
XML to HTML, thus describing the presentation of XML documents. Nowadays,
many people use XSL as their basic tool for XML to XML transformations which
renders XSL into an XML query language. It has been noted by the database
community [9, 1], though, that the transformations XSL can express are rather
limited. For instance, XSL does not have joins or skolem-functions (and, hence
cannot do sophisticated grouping of output data). In other words, XSL lacks the
most basic property any query language should have: it is not relationally com-
plete. However, as the language is still under development, some features have
changed over time. Recently various extensions were added to the language [7].
The most apparent ones being the addition of variables and parameter passing
between template rules. We show that these additions, together with the use of
modes (which are actually states as used in nite state machines and which were
already dened in earlier versions of XSL) render XSL into a powerful query
language. Indeed, XSL not only becomes relationally complete, but it can do explicit
grouping (with or without skolem functions), it can simulate regular path
expressions, and it can simulate all other current XML query languages.
? The work of this author was supported by the EC TMR Network GETGRATS.
?? Research Assistant of the Fund for Scientic Research, Flanders. Work partly performed
while visiting the University of California San Diego. Contact author of this
submission.
Actually together with the addition of the new features, XSL was split into
two parts: XSL Transformations (XSLT) [7] and XPath [5]. The latter contains
the description of XSL's associated pattern language, while the former denes
the real transformation language. To emphasize that we are focusing on the
transformation part, with the new features, we refer to XSL by XSLT in the rest
of this paper.
The main source for the denition of XSLT is its specication [7] which is a
bit dicult to read, especially when one only wants an impression of how the
language works or what it is capable of. To remedy this, we dene an abstract
formal model of XSLT incorporating most of its features, but all of those which
are necessary to simulate, say, XML-QL. The purpose of this model is two-fold:
(i) the clean and formal semantics provides the necessary mathematical model
for studying properties of XSLT;
(ii) our formal model abstracts away from the actual syntax of XSLT and emphasizes
on its features in such a way that the interested reader can get a
feeling of the language and what it is capable of.
Next, we use this model to gain some insight in XSLT. First, we obtain that
XSLT can compute all unary monadic second-order (MSO) structural properties.
In brief, MSO is rst-order logic (FO) extended with set quantication and
is an expressive and versatile logic: on trees, for instance, it captures many
robust formalisms, like regular tree languages [25], query automata [20], nite-
valued attribute grammars [22, Moreover, MSO can take the inherent
order of children of vertices into account, a desirable property for XML pattern
languages [13, 24]. By structural patterns we mean MSO without joins, that is, we
cannot check whether the values of two attributes are the same (see Section 4 for
details). In fact, Neven and Schwentick [19] showed that, already w.r.t. structural
patterns, MSO is more expressive than FO extended with various kinds of regular
path expressions. Thus, as most current XML query languages are based on FO
extended with regular path expressions, this already indicates that XSLT cannot
be simulated by, say, XML-QL.
Next, we show that XSLT can simulate most existing XML query languages.
To study decidability of type checking, Milo, Suciu, and Vianu [16] dened the k-
pebble tree-transducer as a formalism capturing the expressiveness of all existing
query languages, including XML-QL [9], XQL [23], Lorel [2], StruQL [14],
UnQL [4] and the previous version of XSL. Their model does not take value
equation into account (needed for joins, for instance) but can easily be modied
to do so. We obtain that XSLT can simulate this model, thereby establishing
XSLT to be more expressive than all of the above. For more concrete simulations,
we refer the interested reader to [3], were we show how the XML-QL queries in
[9] can be expressed in actual XSLT.
We want to emphasize that we do not provide a model for all of XSLT. For
instance, we excluded for-loops and variables can only be instantiated by data
values (not by result tree fragments). The idea is that we want to use variables
as a look-ahead or to fetch data values occurring 'far' from the current node. The
resulting language is, hence, not Turing complete and, hopefully, more ecient
to evaluate. The study of the properties of our formal model, however, is beyond
the scope of the present paper. The most important fact is that the dened
language is more expressive than, say, XML-QL, as opposed to the previous
version of XSL [9, 1]. 1
The rest of the paper is structured as follows. In Section 2, we introduce the
important features of XSLT by means of two examples. In Section 3, we dene
our formal model. Finally, in Section 4 we obtain our expressibility results.
2 XSLT by Example
A basic XSLT program is a collection of template rules where each such rule
consists of a matching pattern, a mode (which indicates the (nite) state the
computation is in), and a template (see, for example, the program in Figure 2).
The computation on a document t starts at its root in the starting mode 2 and
proceeds roughly as follows. When the computation arrives at a node, say u, in
a certain mode, say q, the program tries to nd a template rule with mode q
and whose matching pattern matches u. 3 If it nds such a template rule, the
program executes the corresponding template. The latter usually instructs XSLT
to produce some XML output and at various positions in this XML output to
selects lists of nodes for further processing (we refer to patterns that select nodes
for further processing as selecting patterns). Each of these selected nodes are then
processed independently as before. Finally, the documents that are constructed
by these subprocesses are inserted in at the positions where the subprocesses
were generated.
To illustrate the new features of XSLT we use the DTD in Figure 1. It
describes an organization as a sequence of groups together with a list of top
managers. Each group has an id, consists of a manager and a list of other groups,
or just consists of a list of employees. For simplicity we identify employees by
their id. The XSLT program in Figure 2 computes pairs
of employees,
is a top manager dierent from Bill and is a direct or indirect manager
of e 2
. Pairs are encoded simply by a pair element with attributes topmgrID and
employeeID.
On the face of it, the program just makes a join between the list of top
managers and the group managers, that is, the ones occurring in the top manager
list and the ones occurring as a manager of a group. However, it does
so in a rather direct and procedural way. In brief, the XSLT program starts
by applying the rst template rule at the root in mode start. This rule selects
each top manager (in mode selecttopmgr). In particular, the pattern
/organization/topmgr/employee is matched against the current node which
In previous work we dened a formal model for the version of XSL not incorporating
data values [15].
Actually, modes are optional, but for convenience we assume every template has a
one and that there is a start mode.
3 Usually, and in all our examples, such a matching pattern only refers to the label of
the current node. In fact, we show in Section 4 that such patterns suce.
organization [
<!ELEMENT organization group+ topmgrs>
<!ELEMENT topmgrs employee+>
<!ELEMENT group (mgr group+) | employee+>
<!ELEMENT mgr employee>
<!ATTLIST group id ID #REQUIRED>
Fig. 1. A DTD describing an organization.
is labeled by organization and then selects all employee children of all topmgr
children (the means 'child of'). For each selected employee (in mode
selecttopmgr), the second template rule is applied which stores the employee's
ID, say e
, in the variable varID and veries, by using the latter, whether e 1
is dierent from Bill. If so, it selects all the descendants of the group manager
who have an ID e 1
(in mode display). In particular, the selection pattern in the
second template rule says 'select all employees that are descendants of a group
that itself is a child of a group whose manager has the same ID as the one stored
in the variable varID (the symbol == means 'descendant of', the expression between
the brackets a lter on group elements). In this latter selection
the XSLT program passes the ID e 1
along as a parameter. Next, for each employee
selected by the latter selection, the program outputs an element pair
with attribute values e 1
and e 2
for the attributes topmgrID and employeeID,
respectively.
The above program is not the 'best' way in XSLT to compute the desired
query, but it nicely illustrates the three most important features of XSLT: modes,
variables, and passing of data values. Let us discuss these brie
y:
(i) Modes enables XSLT to act dierently upon arrival at the same element
types. For instance, as described above, when our program arrives at an employee
element, its action depends on the actual mode, select or display,
this element was selected in.
(ii) Variables can be used for two purposes. The most apparent one, which is
illustrated by the above query, is that they allow to perform joins between
data values. A less apparent application is to use them as a 'look-ahead'.
In

Figure

5, we give a fragment of an XSLT program evaluating a binary
tree, representing a Boolean circuit, to its truth value. Essentially, the use
of variables allows for a bottom-up computation. The restriction to binary
trees is just for expository purposes. In fact, it can be shown that XSLT can
evaluate any bottom-up tree automaton over unranked trees [17]. In brief,
when arriving at an or-labeled node, the program returns the correct truth
value based upon the truth values of the rst and second subtree.
(iii) Passing of data values to other template rules can be crucial for performing
joins if the items that have to be joined are 'far' apart. Moreover, when
<xsl:template match="organization" mode="start">

<xsl:apply-templates select="/organization/topmgr/employee"
mode="selecttopmgr"/>

</xsl:template>
<xsl:template match="employee" mode="selecttopmgr">
<xsl:variable name="varID">
<xsl:value-of select="@id"/>
</xsl:variable>
<xsl:if test="$varID != 'Bill'">
<xsl:apply-templates mode="display"
select="//group[mgr/employee[@id=$varID]]/group//employee">
<xsl:with-param name="varID" select="$varID"/>
</xsl:apply-templates>
</xsl:if>
</xsl:template>
<xsl:template match="employee" mode="display">
<xsl:param name="varID"/>

<xsl:attribute name="topmgrID">
<xsl:value-of select="$varID"/>
</xsl:attribute>
<xsl:attribute name="employeeID">
<xsl:value-of select="@id"/>
</xsl:attribute>

</xsl:template>
Fig. 2. An XSLT program computing the query of Section 2.

<group id="HR">
<employee id="Bill"/>
<group id="HR-prod">
<employee id="Edna"/>
<group id="HR-prod-empl">
<employee id="Kate"/>
<employee id="Ronald"/>

<group id="HR-QA">
<employee id="John"/>
<group id="HR-QA-empl">
<employee id="Jane"/>
<employee id="Jake"/>

<employee id="Bill"/>
<employee id="John"/>

Fig. 3. An XML document conforming to the DTD of Figure 1.

<pair topmgrID="John" employeeID="Jane"/>
<pair topmgrID="John" employeeID="Jake"/>

Fig. 4. The output of the XSLT program of Figure 2 on the document of Figure 3.
node IDs are present in the XML document, 4 we can use this mechanism to
place 'pebbles' on the input document which enables us to do complicated
grouping operations.
It are exactly these three features which render XSLT into a quite powerful
transformation language.
<xsl:template match="or">
<xsl:variable name="arg1">
<xsl:apply-templates select="./*[1]"/>
</xsl:variable>
<xsl:variable name="arg2">
<xsl:apply-templates select="./*[2]"/>
</xsl:variable>
<xsl:choose>
<xsl:when
<xsl:value-of select="'false'"/>
</xsl:when>
<xsl:otherwise>
<xsl:value-of select="'true'"/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
Fig. 5. The fragment of an XSLT program evaluating tree-structured Boolean circuits
that takes care of or-nodes.
In the next section, we give an abstract formal syntax for XSLT. First of all,
we restrict matching patterns to test only the label of the current node (as is
already the case in Figure 2). This is no restriction, as Theorem 8 shows that
we can test many properties of the current node in the body of the template
rule. Further, we divide a template rule into two parts: the variable denition
part and the construction part. Variables can only be assigned data values. In
particular, a variable can be dened as the value of some attribute of the current
node or by an XSLT apply-templates statement that will return exactly one data
value. We will refer to such special templates as selection template rules. In the
construction part of the template rule, the actual output is dened relative to
some conditions on the values of the variables, the parameters, and the attribute
values of the current node, and possibly whether the current node is the root, a
leaf, or the rst or last child of its parent.
4 If not, XSL is capable of generating them itself (see Section 4).
3 A formal Model for XSLT
3.1 Trees and forests
We start with the necessary denitions regarding trees and forests over a nite
alphabet  (the symbols in  correspond to the element names of the XML
document the tree represents). To use these trees as adequate abstractions of
actual XML documents, we extend them with attributes that take values from
an innite domain
g.
The set of -forests, denoted by F , is inductively dened as follows: every
2  is a -forest; if  2  and f 2 F then (f) is a -forest; if f 1
F then f 1
fn is a -forest. A -tree is a -forest of the form (f ). We
denote the set of all -trees by T . Note that there is no a priori bound on the
number of children of a node in a forest. In the following, whenever we say tree
or forest, we always mean -tree and -forest.
The reason we consider forests is that even when we use XSL for tree to tree
transformations only, we sometimes need to specify template rules that construct
forests.
For every forest f 2 F , the set of nodes of f, denoted by Nodes(f ), is the
subset of N  inductively dened as follows: if
)g. Thus, for a
tree the node " represents its root and ui represents the i-th child of u. Further,
for a forest the node iu represents the node u of the i-th tree in the forest.
Next, we add XML attributes to the above dened attributes. To this end,
for the rest of the paper, we x a nite set of attributes A. An attributed forest
with domain S is a pair (f; ( f
a and where for each a 2 A,
is a function assigning a value in S to each node of f .
The set of all attributed forests with domain S, is denoted by F S
. For S we
will usually take D. However, to create output in template rules we will use
attributed forests over D[fx 1
where the variables refer to those dened
by the variable dening part of the template. Of course, in real XML documents,
usually, not all element types have the same set of attributes. Obviously, this is
just a convenient, not a necessary restriction. In an analogous way one can dene
the set of attributed trees, denoted by T D
. For a set B, F D
denotes the set
of attributed forests f over  [ B such that symbols of B may only appear at
the leaves of f .
In our formal model we abstract away from a particular selection pattern
language. Recall that XSLT uses the pattern language described in XPath [5]
(see [26], for a formal semantics). Patterns can be rather involved as illustrated
by the second template rule in Figure 2 where the pattern depends on the value
of the variable varID. In addition, patterns can also be moving instructions
like select parent, left sibling, right sibling, or rst child. Actually, the proof
of Theorem 9 indicates that such local selections only are enough to simulate
all existing XML query languages. In the following, we assume an innite set
of variables X . We dene a pattern over the variables X  X as a function
and denote the set of all patterns over X by
. The idea is as follows. Let p be a pattern, t be a tree, and
be a variable
assignment (for the variables in p). Then p(t;
)(u) is the set of selected nodes
when the pattern is applied at node u.
3.2 Syntax
Denition 1. An XSLT program is a tuple
{  is an alphabet of input symbols ;
{  is an alphabet of output symbols;
{ M c and M s are nite sets of construction and selection modes ;
{ start 2 M c is the start mode; and
{ R is a nite set of construction and selection template rules (to be dened
below).
As mentioned at the end of section 2, we distinguish between two types of template
rules: constructing and selecting ones. The former are used to create output.
So, the result of applying these is a forest. The latter are used to fetch data val-
ues. So, each one returns exactly one domain element. The mode will determine
the nature of the template: constructing or selecting.
Denition 2. A construction apply-templates-expression r (at-expression for
short) is of the form q(p;  z); where q 2 M c , p is a pattern and  z is a possibly
empty sequence of variables in X and domain elements in D. A selection at-
expression is dened as a constructing one with the restriction that p only selects
single nodes, that is, for every tree t, each assignment of variables
, and each
node u of t, p(t;
)(u) is a singleton set. We denote the set of construction
(selection) at-expression by AT c (AT s ).
For instance, the apply-templates expression in the second template of Figure 2
is a constructing one and corresponds in our model to the expression
with p the pattern
//group[mgr/employee[@id=varID]]/group//employee.
Note that application of this pattern eventually leads to the generation of a
element. So the expression is constructing in the sense that it eventually
will produce output.
Denition 3. An attribute expression is an expression of the form a(:) where
a is an attribute. An atomic test is one of the following: (i) an expression of
the are attribute expressions, variables, or domain
or, (ii) an expression of the form root, leaf, rst-child, or last-child.
Finally, a test is a Boolean combination of atomic tests.
During a computation the expressions a(:) will evaluate to the value of the
attribute a of the current node. Further, root, leaf, rst-child, last-child evaluate
to true whenever the current node is the root, a leaf, the rst or the last child
of its parent. Selection template rules are dened next. Recall that they output
one domain element.
Denition 4. Let q 2 M c and  2 . A (q; )-selection template rule is of the
template (q; x 1
return
{ all x's and y's are variables (the former are parameters while the latter are
local
{ each r i 2 AT s or is an attribute expression; further, if r i 2 AT s then every
variable occurring in it is among y 1
{ all c i are tests containing only variables in X := fx
and
{ every z i is a domain element, a variable in X , or a selecting at-expression
with the restriction that all variables occurring in it should belong to X .
Denition 5. Let q 2 M c and  2 . A (q; )-construction template rule is of
the same form as a selection rule only now each z i is a forest in F D[X
(recall that these are forests where attributes take values in D [ X and where
leaves may be labeled with constructing at-expression) with the restriction that
each variable occurring in an at-expression occurring at a leaf of z i should be in
X .
To keep the model total and deterministic we require the existence of exactly
one (q; )-template rule for each mode and each . Further, to ensure that an
XSLT program generates tree to tree translations, we require that each z i in a
(start; )-construction template rule is a tree (rather than a forest).
Example 6. We illustrate the above by translating the program in Figure 2 into
our syntax. The patterns p 1
and
refer to the patterns in the rst and second
template rule, respectively. In the second template rule display(p 2 ,varID) is the
tree consisting of one node labeled with display(p 2 ,varID); further, " denotes the
empty tree. In the last rule pair[topmgr!varID; employeeID!myID] denotes
the tree t consisting of one node where  t
topmgrID
employeeID
myID. For readability, we omitted the test 'if true then'. All modes are constructing

template organization(start)
return
template employee(selecttopmgr)
return
if varID 6= Bill then display(p 2
template employee(display,varID)
return
3.3 Semantics
To dene the semantics we need the following. Let
w consist of a sequence of
variables of X and domain elements. For a function
D, we denote
by
the sequence of domain elements obtained from
w by replacing each
occurrence of the variable x in
w by
(x). By x 1 nd
d we denote
the function that maps each x i to d i .
We next dene the semantics of an XSLT program P on a tree t. Thereto,
we need the following concept. A local conguration is an element of Nodes(t)
Intuitively,  := (u; q; d means that the program has
selected node u in mode q with values
d as parameters. For ease of presentation,
we dene the result of P on , denoted by P t (), in a direct and procedural
way. The latter has the advantage over the usual denition, in terms of rather
complicated but formally more correct rewrite relations, that it is more trans-
parent. The drawback is that it does not deal with the border case when XSLT
programs get into innite cycles. However, it should be clear that P t () is un-
dened whenever one of the generated subprocesses computes forever. We defer
the formal semantics in terms of rewrite relations to the full version of the paper.
We distinguish between two cases. In both of these, let the label of u be .
{ Suppose q is a selection mode. Then P t () 2 D. Let the (q; )-template rule
be of the form as specied in Denition 4, where each r i is q i (p
or the
attribute expression a i (:).
Intuitively, this template is evaluated as follows. First, the values of the
variables y 1 are dened. Such a value can be an attribute value of
the current node or can be dened by invoking an at-rule that will compute
the desired data value. The output then is determined by z i where c i is the
rst test that evaluates to true.
Suppose the variables y 1
assigned the domain values e 1
is an at-expression, then e
maps each
x j to d j , for is the
node selected by p i , that is, p i (t;
is an attribute expression, then e i :=  t
a i
(u).
Next, suppose c i is the rst condition that evaluates to true by interpreting
each y j by e j , x j by d j , a(:) by  t
a (u), and root, leaf, rst-child, last-child
by true i u is the root, a leaf, the rst or the last child of its parent,
respectively. To ensure that the translation is total, we require that at least
one such c i exists. 5 Then, z i determines the output value in the following
way. If z i is a constant, a variable, or an attribute expression then P t ()
equals the corresponding value. If z i is a selecting at-expression q 0 (p;
w),
then
w[xn
d;
yne]) where v is the node selected by p, that
is, p(t; [xn
d;
fvg.
{ Suppose q is a construction mode. Then P t
. Let the (q; )-template
rule be of the form as specied in Denition 5. Suppose the variables y 1
get assigned the values e 1
is the rst
condition that evaluates to true. Then z i determines the output value in
the following way. Recall that z i is forest in F D[X
(AT c ), that is, a forest
where attributes take values in D [ X and where leaves may be labeled
with constructing at-expression. Now, P t () is the forest obtained from z i
by replacing
every occurrence of a y j and a x j as the value of some attribute by the
data values e j and d j , respectively;
every occurrence q 0 (p
w) of an at-expression at a leave of z i by the forest
w[xn
d;
w[xn
d;
d;
denotes document order). Recall that each P t
w[xn
d;  yne]) returns
an attributed forest.
The initial local conguration is dened as  start
Denition 7. The result of an XSLT program P on a tree t, denoted by P (t),
is dened as P t ( start ).
3.4 Some remarks
We conclude this section with some remarks. First, we note that XSLT does not
make the explicit distinction between constructing and selecting template rules,
5 Obviously, one could also add an 'otherwise' construct rather than having this condition

or even, between the variable denition part and the constructing part of a template
rule. However, we feel that by making this explicit, programming becomes
more structured. On the other hand, we did not incorporate everything XSLT
has to oer. For instance, we refrained from including for-loops. Nevertheless,
we show in the next section that we have captured a powerful fragment capable
of simulating most existing XML query languages and even more.
4 Expressiveness
We next show that XSLT is capable of computing very expressive structural
patterns. Thereto, we rst say how we view attributed trees as logical structures
(in the sense of mathematical logic [10]) over the binary relation symbols E
and <, and the unary relation symbols (O  ) 2 . The domain of t, viewed as
a structure, equals the set of nodes of t, i.e., Nodes(t). E is the edge relation
and equals the set of pairs (v; v  i) for every v; v  i 2 Nodes(t). The relation
< species the ordering of the children of a node, and equals the set of pairs
(v Nodes(t). For each , O  is the set of nodes that
are labeled with a . The logic MSO  is MSO over the above vocabulary (with
MSO dened in the usual way, see, e.g., [10]) extended with atomic formulas of
the form d, where a is an attribute and d 2 D. Denote the latter atomic
formula by '. Its semantics is then dened as follows t
a d, that
is, the attribute a of u has value d. Note that we do not allow atomic formulas
of the form so we do not allow joins.
Clearly, MSO  can dene all XPath matching patterns (they are even FO
denable). The next theorem says that XSLT is capable of expressing all unary
MSO  patterns. In particular, this means that one does not need matching patterns
in templates. That is, XSLT actually allows to specify rules like
<xsl:template match="p" mode="q">
where p is a pattern rather than just a label. It means that a rule can only be
applied on nodes that satisfy p. The next theorem implies that one can test for
p in the body of the template rule and, hence, does not need matching patterns.
Theorem 8. Let '(x) be an MSO  formula. There exists an XSLT program P
and a mode q ' such that P t (u; q '
Proof. Due to space limitations we can only give a brief hint of the proof. We
refer the interested reader to [17]. We start with some terminology. The subtree
of t rooted at v is denoted by t v . The envelope of t at v, denoted by t v , is the
tree obtained from t by deleting the subtree rooted at v but keeping v. Note that
t v and t v have v in common. Let the quantier-depth of ' be k and denote by
all the unary MSO  formulas '(x) up to quantier-depth k that hold in
t with x interpreted by v. It is well known that  k (t; v) is nite for all t and v
(for xed k). Further, whether t depends only on  k
6 This would not be the case if atomic formulas of the form
can be computed by unranked tree automata
working on (t v ; v) and t v , respectively [20]. Here, (t v ; v) is the tree t v with v as a
distinguished node. Hence, it remains to show how XSLT programs can compute
bottom-up unranked tree automata. In brief, this can be done by using variables
as look-ahead like the XSLT program in Figure 5.
To study decidability of type checking, Milo, Suciu, and Vianu [16] dened
the k-pebble tree-transducer as a formalism capturing the expressiveness of most
existing XML query languages. Such transducers transform binary trees into
other binary trees. 7 We next describe such deterministic transducers with equality
tests on data values. The k-pebble deterministic tree-transducer uses up to
k pebbles to mark certain nodes in the tree. Transitions are determined in a
unique way by the current node symbol, the current state (or mode), the pres-
ence/absence of the various pebbles on the current node, and equality tests on the
attribute values of the nodes the pebbles are located on. Pebbles are ordered and
numbered from 1 to k. The machine can place pebbles on the root, move them
around, and remove them (actually, the use of the pebbles is restricted by a stack
discipline which ensures that the model does not become too powerful, that is,
accepts non-tree-regular languages). There are move transitions and output tran-
sitions. Move transitions are of the following kind: move-to-parent, move-to-rst-
child, move-to-last-child, move-to-left-sibling, move-to-right-sibling, remain-and-
change-state, place-new-pebble, and pick-current-pebble. There are two kinds of
output transitions. A binary output outputs a -symbol , possibly with attributes
dened as an attribute value of a pebbled node, and spawns two computation
branches that compute, independently of each other, the left and the
right subtree of . Both branches inherit the positions of all pebbles on the input
and do not communicate with each other, that is, each branch moves the pebbles
independently of the other. In a nullary output, the node being output is a leaf
of the output tree, again possibly with attributes, and the computation halts.
It should be clear that, apart from the pebbles, the above described model
is extremely close to XSLT: XSLT is equiped with modes (states), can do local
movements and the simple output transitions. Under the assumption that each
node has a unique id, XSLT can also simulate pebbles. 8 Indeed, we just use k
variables x 1
up to x k , where at each time instance x i contains the id of the node
on which the i-th pebble is located. The above discussion immediately leads
to the next theorem which implies that XSLT can simulate most other current
query languages, like for instance, XML-QL [16] . We refer the interested
7 When proving properties of XML transformations, restricting to binary trees is usually
sucient as unranked ones can be encoded into ranked ones; of course, this is
not the case when one tries to dene a formal model for XSLT which works directly
on unranked trees.
8 Actually, this assumption is not necessary as XSLT is equiped with the function
generate-id(.) which generates a unique id for the current node. Furthermore, this id
only depends on the current node, that is, when invoked for the same node several
times it will return the same value. So there is no need to store the node id's; they
can be computed on demand.
reader to [3] were we show how the XML-QL queries in [9] can be expressed in
actual XSLT.
Theorem 9. XSLT can simulate k-pebble deterministic tree-transducers with
equality tests on data values.
We point out that non-deterministic tree-transducers can be simulated by giving
a non-deterministic semantics to XSLT in the obvious way.
Although by the above discussion k-pebble transducers seem extremely close
to our formal model of XSLT, it is not clear whether the former can simulate
the latter. Indeed, Theorem 8 shows that XSLT can check any MSO property of
the root of the tree. We do not know whether deterministic k-pebble transducers
can do this. In fact, this problem is closely related to a seemingly dicult open
problem in formal language theory: can tree-walking automata (with or without
pebbles) dene all MSO denable tree languages [11, 12, 21]. On the other hand,
Theorem 8 does hold for non-deterministic k-pebble transducers. Furthermore,
it is not clear whether all deterministic transformations they can express can be
simulated by XSLT. Regardless of the above, it is known that query languages
based on rst-order logic extended with regular path expressions, like XML-QL,
are weaker than MSO [19], hence, by Theorem 8 and Theorem 9, weaker than
XSLT.

Acknowledgements

The last author thanks Bertram Ludascher and Victor Vianu for encouraging
and helpful discussions.



--R

Data on the Web
The lorel query language for semistructured data.
Examples of translations from XML-QL to XSLT
A query language and optimization techniques for unstructured data.
XML Path Language (XPath).
Extensible stylesheet language (XSL).
XSL transformations version 1.0.
World Wide Web Consortium.
Querying XML data.
Finite Model Theory.

Trips on trees.

Catching the boat with strudel: Experiences with a web-site management system
Structured document transformations based on XSL.
Type checking for XML transformers.
Design and Analysis of Query Languages for Structured Documents
Extensions of attribute grammars for structured document queries.
Expressive and e
Query automata.
On the power of tree-walking-automata

The design of XQL.
Semistructured data and XML.

A formal semantics of patterns in XSLT.
--TR
A query language and optimization techniques for unstructured data
Languages, automata, and logic
Expressiveness of structured document query languages based on attribute grammars
Catching the boat with Strudel
Query automata
Macro tree transducers, attribute grammars, and MSO definable tree translations
Data on the Web
Typechecking for XML transformers
Expressive and efficient pattern languages for tree-structured data (extended abstract)
Quilt
Structured Document Transformations Based on XSL
Extensions of Attribute Grammars for Structured Document Queries

--CTR
Frank Neven, Automata theory for XML researchers, ACM SIGMOD Record, v.31 n.3, September 2002
Michael Benedikt , Wenfei Fan , Gabriel Kuper, Structural properties of XPath fragments, Theoretical Computer Science, v.336 n.1, p.3-31, 25 May 2005
Joost Engelfriet , Hendrik Jan Hoogeboom , Bart Samwel, XML transformation by tree-walking transducers with invisible pebbles, Proceedings of the twenty-sixth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 11-13, 2007, Beijing, China
Andreas Maletti , Heiko Vogler, Incomparability results for classes of polynomial tree series transformations, Journal of Automata, Languages and Combinatorics, v.10 n.4, p.535-568, January 2005
Maarten Marx , Maarten de Rijke, Semantic characterizations of navigational XPath, ACM SIGMOD Record, v.34 n.2, June 2005
Martens , Frank Neven, Frontiers of tractability for typechecking simple XML transformations, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 14-16, 2004, Paris, France
Martens , Frank Neven, On the complexity of typechecking top-down XML transformations, Theoretical Computer Science, v.336 n.1, p.153-180, 25 May 2005
Frank Neven , Thomas Schwentick, On the power of tree-walking automata, Information and Computation, v.183 n.1, p.86-103, May 25,
Frank Neven, On the power of walking for querying tree-structured data, Proceedings of the twenty-first ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 03-05, 2002, Madison, Wisconsin
Makoto Onizuka , Fong Yee Chan , Ryusuke Michigami , Takashi Honishi, Incremental maintenance for materialized XPath/XSLT views, Proceedings of the 14th international conference on World Wide Web, May 10-14, 2005, Chiba, Japan
Martens , Frank Neven, Frontiers of tractability for typechecking simple XML transformations, Journal of Computer and System Sciences, v.73 n.3, p.362-390, May, 2007
Frank Neven , Thomas Schwentick , Victor Vianu, Finite state machines for strings over infinite alphabets, ACM Transactions on Computational Logic (TOCL), v.5 n.3, p.403-435, July 2004
Jan Hidders , Philippe Michiels , Jan Paredaens , Roel Vercammen, LiXQuery: a formal foundation for XQuery research, ACM SIGMOD Record, v.34 n.4, p.21-26, December 2005
Thomas Schwentick, Automata for XML---A survey, Journal of Computer and System Sciences, v.73 n.3, p.289-315, May, 2007
XSLT;expressiveness;logic;XML;databases;tree transducers;query languages