Towards Practical Typechecking for Macro Tree
Transducers
Alain Frisch — Haruo Hosoya

N° ????
Janvier 2007

apport
de recherche

ISRN INRIA/RR--????--FR+ENG

Thème SYM

ISSN 0249-6399

arXiv:cs/0701176v1 [cs.PL] 26 Jan 2007

INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE

Towards Pra ti al Type he king for Ma ro Tree Transdu ers

∗

Alain Fris h

†

, Haruo Hosoya

Thème SYM  Systèmes symboliques
Projet Gallium
Rapport de re her he

Abstra t:

n° ????  Janvier 2007  28 pages

Ma ro tree transdu ers (mtt) are an important model that both

overs many useful

XML transformations and allows de idable exa t type he king. This paper reports our rst step
toward an implementation of mtt type he ker that has a pra ti al e ien y. Our approa h is to
represent an input type obtained from a ba kward inferen e as an alternating tree automaton,
in a style similar to Tozawa's XSLT0 type he king. In this approa h, type he king redu es to
he king emptiness of an alternating tree automaton. We propose several optimizations (Cartesian fa torization, state partitioning) on the ba kward inferen e pro ess in order to produ e
mu h smaller alternating tree automata than the naive algorithm, and we present our e ient
algorithm for

he king emptiness of alternating tree automata, where we exploit the expli it rep-

resentation of alternation for lo al optimizations. Our preliminary experiments
algorithm has a pra ti al performan e that

onrm that our

an type he k simple transformations with respe t

to the full XHTML in a reasonable time.

Key-words:

∗
†

tree automata, tree transdu ers, exa t type he king, alternating automata

INRIA, projet Gallium
University of Tokyo

Unité de recherche INRIA Rocquencourt
Domaine de Voluceau, Rocquencourt, BP 105, 78153 Le Chesnay Cedex (France)
Téléphone : +33 1 39 63 55 11 — Télécopie : +33 1 39 63 53 30

Vers un typage prati able pour les ma ro transdu teurs d'arbre

Résumé :

Les ma ro transdu teurs d'arbre (mtt)

onstituent un modèle important, dans la

mesure où ils permettent de réaliser de nombreuses transformations XML et où ils admettent
un typage exa t dé idable.

Cet arti le rend

ompte d'une première étape en dire tion de

l'implémentation d'un typeur pour les mtt e a e en pratique.

Notre appro he

onsiste à

représenter le type d'entrée obtenu par inféren e inverse sous la forme d'un automate d'arbre
alternant, dans un style similaire à

elui introduit par Tozawa pour le typage de XSLT0.

problème de la véri ation du bon typage du transdu teur se réduit alors à

Le

elui du test de

vide pour un automate d'arbre alternant. Nous proposons plusieurs optimisations (fa torisation
artésienne, partionnement des états) pour le pro essus d'inféren e inverse, ave
produire des automates alternants signi ativement plus petits qu'ave

l'obje tif de

l'algorithme naïf. Nous

dé rivons également un algorithme e a e pour le test de vide pour un automate d'arbre alternant, dans lequel nous exploitons la représentation expli ite de l'alternation pour permettre
des optimisations lo ales. Nos expérien es préliminaires

onrment que notre algorithme atteint

des performan es susantes pour typer des transformations par rapport à la DTD XHTML
omplète, en un temps raisonnable.

Mots- lés :

automates d'arbre, transdu teurs d'arbre, typage exa t, automates alternants

Pra ti altion
Type
1Towards
Introdu
Stati

he king for Ma ro Tree Transdu ers

3

type he king for XML transformations is an important problem that has expe tedly a

signi ant impa t on real-world XML developments. To this end, several resear h groups have
made eorts in building typed XML programming languages [8, 3℄ with mu h inuen e from
the tradition of typed fun tional languages [2, 10℄.

While this line of work has su

essfully

treated general, Turing- omplete languages, its approximative nature has resulted in an even
trivial transformation like the identity fun tion to fail to type he k unless a large amount of
ode dupli ates and type annotations are introdu ed [7℄.
attention to

Su h situation has led us to pay

ompletely dierent approa hes that have no su h de ien y, among whi h

type he king has emergingly be

been investigated for years [12, 20, 16, 23, 26, 24, 11, 15, 1, 13, 18, 14℄, in whi h

transdu ers (mtt) have been one of the most important models sin

type he king [5℄, yet

ma ro tree

e they allow de idable exa t

over many useful XML transformations [5, 11, 4, 19℄. Unfortunately, these

studies are mainly theoreti al and their pra ti ality has never been
ases [23, 26℄.
This paper reports our rst step toward a
As a basi

exa t

ome promising. The exa t type he king approa h has extensively

lear ex ept for some small

pra ti al implementation

part, we follow an already-established s heme

of type he ker for mtts.

alled ba kward inferen e, whi h

putes the preimage of the output type for the subje t transformation and then

om-

he ks it against

the given input type. This is be ause, as known well, the more obvious, forward inferen e does
not work sin e the image of the input type is not always a regular tree language in general. Our
proposal is, on top of this s heme, to use a representation of the preimage by an

tree automaton

alternating

[21℄, extending the idea used in Tozawa's type he king for XSLT0 [23℄. In this

approa h, type he king redu es to

he king emptiness of an alternating tree automaton.

Whereas normal tree automata use only disjun tions in the transition relation, alternating
tree automata

an use both disjun tions and

ompa t representation (they

onjun tions. This extra freedom permits a more

an be exponentially more su

in t than normal tree automata)

and make them a good intermediate language to study optimizations. Having expli it representation of transitions as Boolean formulas allowed us to derive optimized versions of the rules
for ba kward inferen e, su h as Cartesian de omposition or state partitioning (Se tion 4.1).
These optimizations allow our algorithm to s ale to large types. We also use Boolean reasoning
to derive an e ient emptiness algorithm for alternating tree automata (Se tion 4.2). For instan e, this algorithm uses the following fa t as an e ient short ut: when

φ = φ1 ∧ φ2 ,

if

φ1

turns out to denote an empty set, then so is

even need to look at

φ2 .

φ, and

onsidering a formula

thus the algorithm doesn't

Note that the exploited fa t is immediately available in alternating tree

automata, while it is not in normal tree automata.
We have made extensive experiments on our implementation. We have written several sizes
of transformations and veried against the full XHTML automati ally generated from its DTD
(in reality, transformations are often small, but types that they work on are quite big in many
ases; ex ellent statisti al eviden es are provided in [17℄.) The results show that, for this s ale
of transformations, our implementation has su
time even with XHTML, whi h is

essfully

ompleted type he king in a reasonable

onsidered to be quite large.

We have also

performan e of our implementation with Tozawa and Hagiya's [26℄ and

ompared the

onrmed that ours has

omparable speed for their small examples that are used in their own experiments.
On the theoreti al side, we have established an exa t relationship with two major existing
algorithms for mtt type he king, a

lassi al algorithm based on fun tion enumeration [4℄ and

an algorithm proposed by Maneth, Perst, and Seidl (MPS algorithm) [12℄. Con retely, we have

RR

n° 0123456789

4
proved that (1) the

Alain Fris h , Haruo Hosoya

lassi al algorithm is identi al to our algorithm followed by determinization

of an alternating tree automaton, and that (2) MPS algorithm is identi al to our algorithm
followed by emptiness test of an alternating tree automaton. A parti ular impli ation is that our
algorithm inherits one of useful properties of MPS algorithm: polynomial-time
the restri tion of a bounded number of
time

omplexity under

opying [12℄ (mtt type he king is in general exponential-

omplete). The proofs appear in the appendix, however, sin e this paper is fo used rather

on the pra ti al side.

Related work

Numerous te hniques for exa t type he king for XML transformations have

been proposed.

Many of these take their target languages from the tree transdu er family.

Those in lude te hniques for ma ro tree transdu ers [12, 4℄, for ma ro forest transdu ers [20℄,
for

k-pebble

tree transdu ers [16, 4℄, for subsets of XSLT [23, 26℄, for high-level tree transdu ers

[24℄, and a tree transformation language TL [11℄. Other te hniques treat XML query languages
in the sele t- onstru t style [15, 1, 13℄ or even simpler transformations [18, 14℄. Most of the above
mentioned work provides only theoreti al results; the only ex eptions are [23, 26℄, where some
experimental results are shown though we have examined mu h bigger examples (in parti ular
in the size of types).
Several algorithms in pragmati

approa hes have been proposed to address high

problems related to XML type he king.

omplexity

A top-down algorithm for in lusion test on tree au-

tomata has been developed and used in XDu e type he ker [9℄; an improved version is proposed
in [22℄.

A similar idea has been exploited in the work on

alternating tree automata [6℄; the emptiness

CDu

e on the emptiness

he k for

he k algorithm in our present work is strongly

inuen ed by this. Tozawa and Hagiya have developed BDD-based algorithms for in lusion test
on tree automata [25℄ and for satisability test on a

ertain logi

related to XML type he king

[26℄.

Overview

This paper is organized as follows. In Se tion 2, we re all the

lassi al denitions

of ma ro tree transdu ers (mtt), bottom-up tree automata (bta), and alternating tree automata
(ata). In Se tion 3, we present the two

omponents of our type he king algorithm: ba kward

type inferen e (whi h produ es an ata from an mtt and a deterministi
for alternating tree automata. In Se tion 4, we revisit these two

bta) and emptiness

he k

omponents from a pra ti al

point of view and we des ribe important optimizations and implementation te hniques.

In

Se tion 5, we report the results of our experiments with our implementation of the type he ker
for several XML transformations. In Se tion 6, we
Appendix A is devoted to a pre ise

on lude this paper with our future dire tion.

omparison between our algorithm and the

lassi al algorithm

or the Maneth-Perst-Seidl algorithm for type he king mtt. We show that ea h of these algorithms
an be retrieved from ours by

omposing with a know algorithm. In Appendix B, we propose

the notion of bounded-traversing alternating tree automata, whi h is a natural

ounterpart of

synta ti al bounded- opying mtts as proposed in [12℄. We show in parti ular that this notion
ensures that the emptiness

2
2.1

he k runs in polynomial time.

Preliminaries
Ma ro Tree Transdu ers

We assume an alphabet

a(n) to denote a symbol

Σ where ea h symbol a ∈ Σ is asso iated with its arity; often we write
a with arity n. We assume that there is a symbol ǫ with zero-arity.

INRIA

Towards
Pra over
ti al by
Type
he. .king
fordened
Ma roasTree
Transdu ers
Trees
, ranged
v, w,
. , are
follows:

5

v ::= a(n) (v1 , . . . , vn )
ǫ() and ~v = (v1 , . . . , vn ) to represent a tuple of trees. Assume a set of variables,
ranged over by x, y, . . .. A ma ro tree transdu er (mtt) T is a tuple (P, P0 , Π) where P is a nite
set of pro edures, P0 ⊆ P is a set of initial pro edures, and Π is a set of (transformation) rules
We write

ǫ

for

ea h of the form

p(k) (a(n) (x1 , . . . , xn ), y1 , . . . , yk ) → e
yi is alled (a umulating) parameter and e is a (n, k)-expression. We will abbreviate
(x1 , . . . , xn ) and (y1 , . . . , yk ) to ~x and ~y. Note that ea h pro edure is asso iated with
(k) to denote a pro edure p with arity k . An
its arity, i.e., the number of parameters; we write p
(n, k)-expression e is dened by the following grammar
where ea h
the tuples

e ::= a(m) (e1 , . . . , em ) | p(l) (xh , e1 , . . . , el ) | yj
where only

yj

with

1≤j≤k

and

xh

with

1≤h≤n

an appear as variables. We assume that

ea h initial pro edure has arity zero.

(P, P0 , Π) by a denotation fun tion [[·]]. First, the
a(n) (v1 , . . . , vn ) and parameters w
~ = (w1 , . . . , wk ) and
resulted from evaluating any of p's body expressions.
[
[[p(k) ]](a(n) (~v ), w)
~ =
[[e]](~v , w)
~

We des ribe the semanti s of an mtt
semanti s of a pro edure
returns the set of trees

p(k)

takes a tree

(p(k) (a(n) (~
x),~
y )→e)∈Π

(n, k)-expression e takes a urrent n-tuple ~v = (v1 , . . . , vn ) of trees
parameters w
~ = (w1 , . . . , wk ), and returns the set of trees resulted from the

Then, the semanti s of an
and a

k-tuple

of

evaluation. It is dened as follows.

′ ) | v ′ ∈ [[e ]](~
~ for i = 1, . . . , m}
[[a(m) (e1 , . . . , em )]](~v , w)
~
= {a(m) (v1′ , . . . , vm
i v , w)
i
(l)
(l)
′
~ for j = 1, . . . , l}
[[p (xh , e1 , . . . , el )]](~v , w)
~ = {[[p ]](vh , (w1 , . . . , wl′ )) | wj′ ∈ [[ej ]](~v , w)
[[yj ]](~v , w)
~
= {wj }

a(m) (e1 , . . . , em ) evaluates ea

ei and re onstru ts a tree
node with a and the results of these subexpressions. A pro edure all p(xh , e1 , . . . , el ) evaluates
the pro edure p under the h-th subtree vh , passing the results of e1 , . . . , el as parameters. A
variable expression yj simply results in the orresponding parameter's value wj . Note that an mtt
A

onstru tor expression

h subexpression

is allowed to inspe t only the input tree and never a part of the output tree being
Also, parameters only a

onstru ted.

umulate subtrees that will potentially be ome part of the output and

never point to parts of the input.

v is dened by T (v) =
T (v) has at most one element for any v ; also,
T is total when T (v) has at least one
any v . We will also use the lassi al denition
S element for−1
T
(v)
,
T
(V ′ ) = {v | ∃v ′ ∈ V ′ .v ′ ∈ T (v)}.
of images and preimages: T (V ) =
v∈V
The whole semanti s of the mtt with respe t to a given input tree

S

p0 ∈P0 [[p0 ]](v).

2.2
A

An mtt

T

is deterministi

Tree Automata and Alternation

(bottom-up) tree automaton

QF ⊆ Q

RR

when

is a set of nal states,

n° 0123456789

M is a
and ∆ is

(bta)

tuple

(Q, QF , ∆)

where

Q

is a nite set of states,

a set of (transition) rules ea h of the form

q ←

6
a(n) (q

1 , . . . , qn ) where ea h

qi

is from

Q.

We will write

~q

Alain(qFris
h , Haruo Hosoya
1 , . . . , qn ). Given a bta

for the tuple

M = (Q, QF , ∆), a eptan e of a tree by a state is dened indu tively as follows: M a epts
(n) (~
a tree a
v ) by a state q when there is a rule q ← a(n) (~q) in ∆ su h that ea h subtree vi is
a epted by the orresponding state qi . M a epts a tree v when M a epts v by a nal state
q ∈ QF . We write [[q]]M for the set of trees that the automaton
M a epts by the state q (we
S
drop the subs ript M when it is lear), and L(M) =
[[q]]
for the set of trees a epted
q∈QF
by the automaton M. Also, we sometimes say that a value v has type q when v is a epted by
(n) and
the state q . A bta (Q, QF , ∆) is omplete and deterministi when, for any onstru tor a
(n)
n-tuple of states ~q, there is exa tly one transition rule of the form q ← a (~q) in ∆. Su h a bta
is alled deterministi bottom-up tree automaton (dbta). For any value v , there is exa tly one
state q su h that v ∈ [[q]]. In other words, the olle tion {[[q]] | q ∈ Q} is a partition of the set of
trees.
An

alternating tree automaton (ata) A is a tuple (Ξ, Ξ0 , Φ) where Ξ is a nite set of states,

Ξ0 ⊆ Ξ is
an n-ary

a set of initial state, and
onstru tor to an

Φ

is a fun tion that maps ea h pair

n-formula,

where

n-formulas

(X, a(n) )

of a state and

are dened by the following grammar.

φ ::= ↓i X | φ1 ∨ φ2 | φ1 ∧ φ2 | ⊤ | ⊥
(with

1 ≤ i ≤ n). In parti ular, note that a 0-ary formula evaluates naturally to a Boolean.
A = (Ξ, Ξ0 , Φ), we dene a eptan e of a tree by a state. A a epts a tree a(n) (~v )
state X when ~
v ⊢ Φ(X, a(n) ) holds, where the judgment ~v ⊢ φ is dened indu tively as

Given an ata
by a

follows:

 ~v ⊢ φ1 ∧ φ2

if

~v ⊢ φ1

and

 ~v ⊢ φ1 ∨ φ2

if

~v ⊢ φ1

or

~v ⊢ φ2 .

vi

by

~v ⊢ φ2 .

 ~v ⊢ ⊤.
 ~v ⊢↓i X

if

A

a

epts

X.

~v ⊢ φ intuitively means that φ holds by interpreting ea h ↓i X as  vi has type X . We
write [[X]] for the set of trees a epted by a state X and [[φ]] = {~
v | ~v ⊢ φ} for the set of n-tuples
S
[[X
]]
for
the language a epted by the
a epted by an n-formula φ. We write L(A) =
0
X0 ∈Ξ0
ata A. Note that a bta M = (Q, QF , ∆) an be seen as an ata with the same set of states
W
V
(n) ) =
and nal states by dening the fun tion Φ as Φ(q, a
(q←a(n) (~
q ))∈∆ i=1,..,n ↓i qi , and the
That is,

denitions for the semanti s of states and the language a
bta or an ata then

oin ide. We will use the notation

≃

epted by the automaton seen as a

to represent semanti al equivalen e of

pairs of states or pairs of formulas.

3
3.1

Type he king
Ba kward inferen e

Given a dbta

Mout

Min (input type), and an mtt T , the goal
T (L(Min )) ⊆ L(Mout ). It is well known that T (L(Min ))

(output type), a bta

type he king is to verify that

of
is

in general beyond regular tree languages and hen e the forward inferen e approa h (i.e., rst
al ulate an automaton representing
not work.

T (L(Min ))

and

he k it to be in luded in

L(Mout ))

does

Therefore an approa h usually taken is the ba kward inferen e, whi h is based on

the observation that

T (L(Min )) ⊆ L(Mout ) ⇐⇒ L(Min ) ∩ T −1 (L(M)) = ∅,

where

M

is

INRIA

Towards
Pra ti al
Type he king
for
Ma ro Tree Transdu ers
omplement
automaton
of M
out . Intuitively, if the interse

the

not empty, then it is possible to exhibit a tree
that

v ∈ L(Min )

T (v) 6⊆ L(Mout ),

and

v

tion

L(Min ) ∩ T −1 (L(M))

in this interse tion.

it means that there is a

Sin e this tree satises

ounter-example of the well-

typedness of the mtt with respe t to the given input and output types.
approa h
that

A

onsists of

an ee tively be

Sin e the language

M = (Q, QF , ∆)

whi h denotes the
time sin e

Mout

A representing T
T −1 (L(M)) is regular

he king

and indeed su h automata

omputed, the above disjointness is de idable.

The originality of our approa h is to
dbta

Algorithmi ally, the

−1 (L(M)) and then

omputing an automaton

L(Min ) ∩ L(A) = ∅.

7
is

and an mtt

ompute

T = (P, P0 , Π)

A

as an alternating tree automaton.

Mout , an be obtained from Mout in a
T , we build an ata A = (Ξ, Ξ0 , Φ) where

omplement of the output type

is deterministi . From

M

and

Let a

be given. Here, note that the automaton

M,

linear

Ξ
= {hp(k) , q, ~qi | p(k) ∈ P, q ∈ Q, ~q ∈ Qk }
Ξ0
= {hp0 , qi _
| p0 ∈ P0 , q ∈ QF }
(k)
(n)
Φ(hp , q, ~
q i, a ) =
Inf(e, q, ~q).
(p(k) (a(n) (~
x),~
y )→e)∈Π

Here, the fun tion

Inf

is dened indu tively as follows.

Inf(b(m) (e1 , . . . , em ), q, ~
q)

_

=

Inf(ej , qj′ , ~q)

j=1,..m
~′
(q←b(m)
(q ))∈∆

_

Inf(p(l) (xh , e1 , . . . , el ), q, ~
q) =
Inf(yj , q, ~
q)

^

~′ ∈Ql
q

↓h hp(l) , q, q~′ i ∧

^

j=1,..,l

⊤ (q = qj )
⊥ (q =
6 qj )

=



Inf(ej , qj′ , ~q)

Let us explain why this algorithm works. Sin e a pre ise dis ussion is

riti al for understand-

ing subsequent se tions, we summarize our justi ation here as a formal proof.

Theorem 1

L(A) = T −1 (L(M)).

Intuitively, ea h state

hp, q, ~
qi

represents the set of trees

may transform

of type

q,

wi

v to some tree u
type qi . Formally, we

prove the following invariant

Proof:

ea h of

where

w
~ ∈ [[~
q ]]

su h that the pro edure

p

yi

are bound to trees

∀v. ∀w
~ ∈ [[~
q ]]. v ∈ [[hp(k) , q, ~qi]] ⇐⇒ [[p(k) ]](v, w)
~ ∩ [[q]] 6= ∅

(1)

means

w1 ∈ [[q1 ]], . . . , wk ∈ [[qk ]].

hand side does not depend on the spe i
will be

v

assuming that the parameters

Note that this invariant implies that the right-

hoi e of the values

ru ial later. From this invariant, the initial states

Ξ0

wi

from the sets

[[qi ]];

this point

represent the set of trees that we

want and hen e the result follows:

S
L(A) =
{[[hp0 , qi]] | p0 ∈ P0 , q ∈ QF }
= {v | [[p0 ]](v) ∩ [[q]] 6= ∅, p0 ∈ P0 , q ∈ QF }
= {v | T (v) ∩ L(M) 6= ∅}
= T −1 (L(M))
The proof of the invariant (1) pro eeds by indu tion on the stru ture of
rst need to

RR

onsider an invariant that holds for the fun tion

n° 0123456789

Inf .

v.

For the proof, we

Informally,

Inf(e, q, ~q)

infers

8
an

n-formula

representing the set of

some tree of type

q,

n-tuples ~v

Alain Fris
h , Haruo
Hosoya
e may
transform
~v to

su h that the expression

assuming that the parameters

yi

are bound to trees

wi

ea h of type

qi .

Formally, we prove the following:

∀~v . ∀w
~ ∈ [[~
q ]]. ~v ∈ [[Inf(e, q, ~q)]] ⇐⇒ [[e]](~v , w)
~ ∩ [[q]] 6= ∅
Indeed, this implies the invariant (1). Let

v ∈ [[hp(k) , q, ~
q i]]

v = a(n) (~v );

for all

w
~ ∈ [[~q]]:

⇐⇒

~v ∈ [[Φ(hp(k) , q, ~qi, a(n) )]]

⇐⇒

∃(p(k) (a(n) (~x), ~y ) → e) ∈ Π. ~v ∈ [[Inf(e, q, ~q)]]

⇐⇒

by(2)

∃(p(k) (a(n) (~x), ~y ) → e) ∈ Π. [[e]](~v , w)
~ ∩ [[q]] 6= ∅

⇐⇒

[[p]](v, w)
~ ∩ [[q]] 6= ∅

The invariant (2) is in turn proved by indu tion on the stru ture of

Case

e = b(m) (e1 , . . . , em ).

(2)

e.

of type q to be produ ed from the onstru tor
q ← b(m) (q~′ ) ∈ ∆. In addition, u's ea h subtree
′
must have type qi and must be produ ed from the orresponding subexpression ei . For
~ ∈ [[~q]]:
the latter ondition, we an use the indu tion hypothesis for (2). Formally, for all w
_
^
~v ∈ [[Inf(e, q, ~
q )]]
⇐⇒
~v ∈ [[
Inf(ej , qj′ , ~q)]]
In order for a tree

u

expression, rst, there must be a transition

q→b(m) (q~′ )∈∆ j=1,...,m

∃(q ← b(m) (q~′ )) ∈ ∆. ∀j = 1, . . . , m. ~v ∈ [[Inf(ej , qj′ , ~q)]]

⇐⇒
byI.H.for(2)

Case

⇐⇒

∃(q ← b(m) (q~′ )) ∈ ∆. ∀j = 1, . . . , m. [[ej ]](~v , w)
~ ∩ [[qj′ ]] 6= ∅

⇐⇒

[[e]](~v , w)
~ ∩ [[q]] 6= ∅

e = p(l) (xh , e1 , . . . , el ). In order for a tree u of type q to be produ ed from the pro edure
′
′
all, rst, a tree wj of some type qj must be yielded from ea h parameter expression
ej . In addition, the h-th input tree must have type hp(l) , q, (q1′ , . . . , ql′ )i sin e the result
(l) from the h-th input tree with parameters
tree u must be produ ed by the pro edure p
′
′
′
′
w1 , . . . , wl of types q1 , . . . , ql . We an use the indu tion hypothesis for (2) for the former
ondition and that for (1) for the latter ondition. Formally, for all w
~ ∈ [[~q]]:
_
^
~v ∈ [[Inf(e, q, ~
q )]]
⇐⇒
~v ∈ [[
↓h hp, q, q~′ i ∧
Inf(ej , qj′ , ~q)]]
q~′ ∈Ql

⇐⇒
byI.H.for(2)

⇐⇒

⇐⇒

We

an show that the last

j=1,...,l

∃q~′ ∈ Q . vh ∈ [[hp, q, q~′ i]] ∧ ∀j = 1, . . . , l. ~v ∈ [[Inf(ej , qj′ , ~q)]]
l

∃q~′ ∈ Ql . vh ∈ [[hp, q, q~′ i]] ∧ ∀j = 1, . . . , l. [[ej ]](~v , w)
~ ∩ [[qj′ ]] 6= ∅
(3)
∃q~′ ∈ Ql . vh ∈ [[hp, q, q~′ i]]
′
′
′
~
∧ ∃w . ∀j = 1, . . . , l. wj ∈ [[ej ]](~v , w)
~ ∧ wj ∈ [[qj′ ]]
ondition holds i

~ ′ . [[p(l) ]](vh , w
~ ′ ) ∩ [[q]] 6= ∅ ∧ ∀j = 1, . . . , l. w′ ∈ [[ej ]](~v , w)
∃w
~
j

(4)

INRIA

Towards
al Type he
ers
whi Pra
h is ti
equivalent
to king
[[p(xhfor
, e1 Ma
, . . . ,roemTree
)]] ∩ Transdu
[[q]] 6= ∅. Indeed,
for the only if 
apply the indu tion hypothesis for (1) where we instantiate

w
~

⇐⇒ 

~′
w

with the spe i

w
~

this is exa tly the pla e that uses the fa t that the quanti ation on
the 

9
dire tion, we
in (3)

appears outside

in (1)and obtain the following:

~ ′ . [[p(l) ]](vh , w
~ ′ ) ∩ [[q]] 6= ∅
∃q~′ ∈ Ql . ∃w
∧ ∀j = 1, . . . , l. wj′ ∈ [[ej ]](~v , w)
~ ∧ wj′ ∈ [[qj′ ]]
By dropping the

ondition

wj′ ∈ [[qj′ ]]

(and the unused quanti ation on

For the if  dire tion, sin e that the automaton
state

q

for any value

w

w ∈ [[q]],

su h that

M

is

q~′ ),

(5)

we obtain (4).

omplete, i.e., there is in general a

we obtain (5) from (4). Then, the indu tion

hypothesis for (1) yields (3).

Case

e = yj .

q to be produ ed from the variable expression, yj must
q . Formally, rst note that ~v ∈ [[Inf(e, q, ~q)]] ⇐⇒ q = qj , for any ~v . Note also
′
that, sin e M is deterministi bottom-up, all the states are pair-wise disjoint: [[q]]∩[[q ]] = ∅
′
whenever q 6= q . Therefore, for all w
~ ∈ [[~q]]:
In order for a tree of type

have type

~v ∈ [[Inf(e, q, ~q)]]

⇐⇒

q = qj

⇐⇒

wj ∈ [[q]]

⇐⇒

[[e]](~v , w)
~ ∩ [[q]] 6= ∅


In the proof above, the

ase for variable expressions

riti ally uses the determinism

M

Indeed, the statement of the theorem does not ne essarily hold if
example,

onsider the nondeterministi

bta

M

onstraint.

is nondeterministi . For

with the transition rules

q0 ← b(q1 , q2 ) q1 ← ǫ q2 ← ǫ
(q0 is the initial state) and type he k the mtt

T

with the transformation rules

p0 (a(x1 )) → p(x1 , ǫ)
p(ǫ, y1 )
→ b(y1 , y1 )
(p0 is the initial pro edure) with respe t to the result type
translates to

b(ǫ, ǫ), whi

h is a

epted by

M.

q0 .

With this mtt, the input value

a(ǫ)

However, our algorithm will infer an input type that

denotes the empty set, whi h is in orre t. To see this more

losely,

onsider inferen e on the body

p with the result type q = q0 and the parameter type ~q = (q1 ). The ondition (2) does not hold
sin e the only hoi e of w
~ ∈ [[~
q ]] is w
~ = (ǫ) and, in this ase, the right hand side holds whereas the
left hand side does not sin e Inf(b(y1 , y1 ), q0 , (q1 )) = Inf(y1 , q1 , (q1 )) ∧ Inf(y1 , q2 , (q1 )) = ⊤ ∧ ⊥ =
⊥. The same argument an be done with the parameter type ~q = (q2 ). Now, in inferen e on the
body of p0 with the result type q0 , the all to p must have parameter type q1 or q2 sin e only
these an a ept ǫ. From the previous inferen e, we on lude that the input type inferred for
of

the

all is again the empty set type; so is the whole input type.
However, the variable

ase is the only that uses determinism.

Therefore, if the mtt uses

no parameter, i.e., is a simple, top-down tree transdu er, then the same algorithm works for
a non-deterministi
1

output type.

1 Moreover, if the mtt

is deterministi

and total, we have

Completeness of the output type is not needed for our algorithm to work on top-down tree transdu ers.

This is be ause the only pla e where we use

ompleteness in the proof is the

ompleteness is a tually not ne essary if there is no parameter.

RR

T

n° 0123456789

ase for pro edure

alls, in whi h

Alain Fris h , Haruo Hosoya

10
T −1 (L(M

−1 (L(M
−1 (L(M
out )) = T
out )). It su es to he k L(Min ) ⊆ T
out )) instead of
−1
L(Min ) ∩ T (L(Mout )) = ∅. This ould be advantageous sin e a dire t onversion from an
XML s hema yields a non-deterministi

automaton, and determinizing it has a potential blow-

up (though this step is known to take only a reasonable time in pra ti e) whereas in lusion
be tested more e iently by using known
of a deterministi

automaton [9, 22, 25℄.

an

lever algorithms that avoid a full materialization
Tozawa presents in his work [23℄ a ba kward infer-

en e algorithm based on alternating tree automata for deterministi

forest transdu ers with no

parameters where he exploits the above observation to obtain a simple algorithm.
Finally, it remains to
representing

he k

L(Min ) ∩ L(A)

L(Min ) ∩ L(A) = ∅,

(this

for whi h we rst

an easily be done sin e an ata

al ulate an ata

A′

an freely use interse tions)

A′ . The next se tion explains how to do this. The size of the
′
ata A is polynomial in the sizes of Mout and of T . The size of A is thus polynomial in the sizes
of Min , Mout , and T .
and then

he k the emptiness of

3.2

Emptiness

Let

A = (Ξ, Ξ0 , Φ)

is empty or not.

he k
an alternating tree automaton.

We rst dene the following system of impli ations

propositional variables

Here,

We want to de ide whether the set

X

onsisting of all subsets of

ρ

L(A)

where we introdu e

Ξ:

V
ρ = {X ⇐ X 1 ∧ . . . ∧ X n | ∃a(n) . (X 1 , . . . , X n ) ∈ DNF( X∈X Φ(X, a(n) ))}}

DNF(φ)

omputes

φ's

disjun tive normal form by pushing interse tions under unions and

regrouping atoms of the form

↓i X

for a xed

i;

the result is formatted as a set of

n-tuples

of

state sets. More pre isely:

DNF(⊤)
DNF(⊥)
DNF(φ1 ∧ φ2 )
DNF(φ1 ∨ φ2 )
DNF(↓h X)

=
=
=
=
=

{(∅, . . . , ∅)}
∅
{(X 1 ∪ Y 1 , . . . , X n ∪ Y n ) | (X 1 , . . . , X n ) ∈ DNF(φ1 ), (Y 1 , . . . , Y n ) ∈ DNF(φ2 )}
DNF(φ1 ) ∪ DNF(φ2 )
{(∅, . . . , ∅, {X}, ∅, . . . , ∅)}
(the h-th element is {X})

ρ ⊢ {X} for some X ∈ Ξ0 . The
ρ ⊢ X here is dened su h that it holds when it an be derived by the single rule: if
ρ ontains X ⇐ X 1 ∧ . . . ∧ X n and ρ ⊢ X i for any i = 1, . . . , n, then ρ ⊢ X .
Ea h propositional variable X intuitively denotes that the interse tion of the sets denoted
T
by all the states in X is non-empty:
X∈X [[X]] 6= ∅. Thus, we an prove the following.
Then, with the system of impli ations above, we verify that

judgment

Proposition 1

L(A) 6= ∅

i ρ ⊢ {X} for some X ∈ Ξ0 .
v∈

T

Proof:

The result follows by showing that

dire tion

an be proved by indu tion on the stru ture of

indu tion on the derivation of
This emptiness

he k

X∈X

[[X]] for some v i ρ ⊢ X .
v . The if  dire tion an

The only if 
be proved by

ρ ⊢ X.

an be implemented in linear size with respe t to the size of

itself is exponential in the size of


ρ,

whi h

A.

INRIA

Pra ti al Type
he optimizations
king for Ma ro Tree
4Towards
Algorithm
and

Transdu ers

11

As we explained above, our algorithm splits the type- he king pro ess in two phases: rst, we
ompute an alternating tree automaton from the output type and the mtt; se ond, we
emptiness of this tree automaton.

he k

In this se tion, we are going to des ribe some details and

optimizations about these two phases.

4.1

Ba kward inferen e

A simple algorithm to
naively the formal

ompute the input type as an alternating tree automaton is to follow

onstru tion given in Se tion 3. A rst observation is that it is possible to

build the automaton lazily, starting from the initial states, produ ing new states and

Φ(_)

only on demand.

This is sometimes useful sin e the emptiness

omputing

he k algorithm we are

going to des ribe in the next se tion works in a top-down way and will not always materialize
the whole automaton.

Inf

The dening equations for the fun tion

as given in Se tion 3 produ e huge formulas.

We will now des ribe new equations that produ e mu h smaller formulas in pra ti e.
des ribing them, it is

q ⊆Q

onvenient to generalize the notation

Inf(e, q, ~q) by allowing

a

Before

set of states

Wq ∈ Q for the output type. Intuitively, we want Inf(e, q, ~q) to
q ). We obtain a dire t denition of Inf(e, q, ~q) by
be semanti ally equivalent to
q∈q Inf(e, q, ~
q ):
adapting the rules for Inf(e, q, ~
_
^
Inf(b(m) (e1 , . . . , em ), q, ~
q)
=
Inf(ej , {qj′ }, ~q)
instead of a single state

q) =
Inf(p(l) (xh , e1 , . . . , el ), q, ~
Inf(yj , q, ~
q)

=

j=1...,m
~′
(q←b(m)
(q ))∈∆,q∈q

_

~′ ∈Ql
q

↓h hp(l) , q, q~′ i ∧

^

j=1,...,l

⊤ (qj ∈ q)
⊥ (qj ∈
6 q)



Inf(ej , {qj′ }, ~q)

↓h hp(l) , q, q~′ i. Intuitively, this should be semanti ally equivalent to
(l)
~′
q∈q ↓h hp , q, q i. Instead of using this as a denition, we prefer to hange the set

We have used the notation
the union

W

of states of the automaton:

Ξ
= {hp(k) , q, q1 , . . . , qk i | p(k) ∈ P, q ⊆ Q, ~q ∈ Qk }
Ξ0
= {hp0 , QF i | p0 ∈ P0 }
W
q i, a(n) ) =
q ).
Φ(hp(k) , q, ~
(p(k) (a(n) (~
x),~
y )=e)∈R Inf(e, q, ~
In theory, this new alternating tree automaton

ould have exponentially many more states.

However, in pra ti e, and be ause of the optimizations we will des ribe now, this a tually redu es
signi antly the number of states that need to be

omputed.

The se tions below will use the semanti al equivalen e
tioned above in order to simplify formulas.

W

q∈q

Inf(e, {q}, ~q) ≃ Inf(e, q, ~q)

4.1.1 Cartesian fa torization
The rule for the

onstru tor expression

b(m) (e1 , . . . , em )

Inf(b(m) (e1 , . . . , em ), q, ~q) =

_

an be written:

^

q~′ ∈∆(q,b(m) ) j=1...,m

RR

n° 0123456789

Inf(ej , {qj′ }, ~q)

men-

Fris h ,that
Haruo
∆(q, b(m) ) = {q~′ | q ← b(m) (q~′ ) ∈ ∆, q ∈ q} ⊆ Qm . Alain
Now assume
weHosoya
have a
(m)
) as a union of l Cartesian produ ts:
omposition of this set ∆(q, b

12
where
de

∆(q, b(m) ) = (q 11 × . . . × q 1m ) ∪ . . . ∪ (q l1 × . . . × q lm )
where the

q ij

are sets of states.

It is always possible to nd su h a de omposition: at worst,

i
using only singletons for the q j , we will have as many terms in the union as m-tuples in
∆(q, b(m) ). But often, we an produ e a de omposition with fewer terms in the union. Let
(m) ) for su h a de omposition (seen as a subset of (2Q )m ). One an then
us write Cart(∆(q, b
use the following rule:

_

Inf(b(m) (e1 , . . . , em ), q, ~
q) =

^

Inf(ej , q j , ~q)

(q 1 ,...,q m )∈Cart(∆(q,b(m) )) j=1,..,m

4.1.2 State partitioning
Intuition The rule for pro
rameters of the

|Q|l

edure

all enumerates all the possible states for the value of pa-

alled pro edure. In its

terms. However, it may be the

urrent form, this rule always produ es a big union with

ase that we don't need fully pre ise information about the

value of a parameter to do the ba kward type inferen e.
Let us illustrate that with a simple example. Assume that the

p(1)

has a

y1 than opying it (that is, any rule
(1)
(a(n) (x1 , . . . , xn ), y1 ) = y1 ). Clearly,
for p whose right-hand side mentions y1 is of the form p
′
′
′′
all the states hp, q, q1 i with q1 ∈ q are equivalent, and similarly for all the states hp, q, q1 i with
′′
q1 6∈ q . This is be ause whether the result of the pro edure all will be or not in q only depends
on the input tree (be ause there might be other rules whose right-hand side don't involve y1
at all) and on whether the value for the parameter is itself in q or not. In parti ular, we don't
single parameter

y1

alled pro edure

and that it never does anything else with

know to know exa tly in whi h state the a

umulator is. So the rule for

alling this pro edure

ould just be:

Inf(p(x_
q)
h , e1 ), q, ~
=
↓h hp, q, q1′ i ∧ Inf(e1 , {q1′ }, ~q)
′

q1 ∈Q
 

_
_
↓h hp, q, q1′ i ∧ Inf(e1 , {q1′ }, ~q) ∪ 
=
′′

q1′ ∈q

=

↓h hp, q, q1′ i

where in the last line

A new rule
all the

q1′

l-tuples

↓h hp, q, q1′′ i ∧ Inf(e1 , {q1′′ }, ~q)

q1 ∈Q\q


∧ Inf(e1 , q, ~
q ) ∨ ↓h hp, q, q1′′ i ∧ Inf(e1 , Q\q, ~q)
(resp.

q1′′ )

is

hosen arbitrarily in

More generally, in the rule for a

q~′ ,



p(l)

(resp.

all to a pro edure

but only a subset of them that

assume that for given pro edure

q

Q\q ).

p(l) , we don't need to

onsider

apture all the possible situations. First, we

and output type

q,

one

an

ompute for ea h

j = 1, .., l

an

(l)
equivalen e relation Ehp , q, ji su h that:

(∀j = 1, .., l. (qj′ , qj′′ ) ∈ Ehp(l) , q, ji) ⇒ hp(l) , q, q~′ i ≃ hp(l) , q, q~′′ i (∗)

INRIA

Towards Pra ti al Type he king for Ma ro Tree Transdu ersInf(p(l) (xh , e1 , . . . , el ), q, ~q):

13

Let us look again at the right-hand side of the denition for

Inf(p(l) (xh , e1 , . . . , el ), q, ~
q) =



_

q~′ ∈Ql
Let us split this union a

↓h hp(l) , q, q~′ i ∧

ording to the equivalen e

lass of the



^

j=1,...,l

qj′

Inf(ej , {qj′ }, ~q)
Ehp(l) , q, ji.
qj ⊳
× . . . × q l )i,

modulo the relations

(l)
If for ea h j , we hoose an equivalen e lass q j for the relation Ehp , q, ji (we write
Ehp(l) , q, ji), then all the states hp(l) , q, q~′ i with q~′ ∈ q 1 ×. . .×q l are equivalent to hp(l) , q, C(q 1
where

C

is a

hoi e fun tion (it pi ks an arbitrary element from its argument).

We

an thus

rewrite the right hand-side to:



_

q 1 ⊳Ehp(l) ,q,1i,...,ql ⊳Ehp(l) ,q,li

↓h hp(l) , q, C(q 1 × . . . × q l )i ∧

The union of all the formulas

V

q ).
j=1,..,l Inf(ej , q j , ~

′
q ) for
j=1,..,l Inf(ej , {qj }, ~

V

_

q~′ ∈q 1 ×...×q l j=1,...,l

In the worst



Inf(ej , {qj′ }, ~q)

q~′ ∈ q 1 × . . . × q l

is equivalent to

Consequently, we obtain the following new rule:

Inf(p(l) (xh , e1 , . . . , el ), q, ~
q) 
=
_
↓h hp(l) , q, C(q 1 × . . . × q l )i ∧
q1

^

⊳Ehp(l) ,q,1i,...,q

l

⊳Ehp(l) ,q,li

Ehp(l) , q, ji

ase, all the equivalen e relations

side is the same as for the old rule.

But if we

^

j=1,...,l



Inf(ej , q j , ~q)

are the identity, and the right-hand

an identify larger equivalen e

lasses, we

an

signi antly redu e the number of terms in the union on the right-hand side.

Computing the equivalen e relations

(k) , q, ji satisfying the
relations Ehp

E[e, q, j]

for any

(n, k)-expression e

Now we will give an algorithm to

(∗). We
j = 1, .., k), su

ondition
(with

ompute the

will also dene equivalen e relations
h that:

(∀j = 1, .., k.(qj′ , qj′′ ) ∈ E[e, q, j]) ⇒ Inf(e, q, q~′ ) ≃ Inf(e, q, q~′′ )
We

an use the rules used to dene the formulas

Inf(e, q, ~q) in order to obtain su

to be satised so that these properties hold. We will express these

as subsets of

Q2 ).

Q,

we write

E1 ⊑ E2

E2 ⊆ E1

equivalen e relations

E1 , E2 ,

we

an dene their least upper bound

with the partition it indu es

E

E . Abusing
on Q, we will

lass modulo

the relation with the two equivalen e

and a set of states

E2

are two

q,

E1 ⊔ E2

we write

Q.

For two

as the set-theoreti

q⊳E

if

q

is one of

the notation by identifying an equivalen e relation
write

lasses

q

{Q}

and its

derived from the rules used to dene the fun tion

n° 0123456789

and

lass. The largest equivalen e relation is the identity on

interse tion. For an equivalen e relation

RR

E1

(when equivalen e relations are seen

The smallest equivalen e relation for this ordering is the equivalen e relation

with a single equivalen e

the equivalen e

if

onditions

onditions by a system of

equations. Before giving this system, we need to introdu e some notations. If
equivalen e relations on

ient

Inf :

for the smallest relation and

{q, Q\q}

for

omplement. The system of equations is

Alain Fris h , Haruo Hosoya

14

G
{E[ej , q j , i] | (q 1 , . . . , q m ) ∈ Cart(∆(q, b(m) )), j = 1..m}
G
E[p(l) (xh , e1 , . . . , el ), q, i] ⊒
{E[ej , q j , i] | q j ⊳ Ehp(l) , q, ji, j = 1..l}

{q, Q\q} (i = j)
E[yj , q, i]
⊒
{Q}
(i 6= j)
G
(k)
Ehp , q, ji
⊒
{E[e, q, j] | p(k) (a(n) (~x), ~y ) = e) ∈ R}
E[b(m) (e1 , . . . , em ), q, i]

⊒

Let us explain why these

onditions imply the required properties for the equivalen e rela-

tion and how they are derived from the rules dening

Inf .

We will use an intuitive indu -

tion argument (on expressions), even though a formal proof a tually requires an indu tion
on trees.

Consider the rule for the pro edure

all.

The new rule we have obtained above

Inf(p(l) (xh , e1 , . . . , el ), q, q~′ ) ≃ Inf(p(l) (xh , e1 , . . . , el ), q, q~′′ ), it is
~′ ) ≃ Inf(ej , q j , q~′′ ) for all j = 1, .., l and for all q j ⊳ Ehp(l) , q, ji,
su ient to have Inf(ej , q j , q
′ ′′
and thus, by indu tion, it is also su ient to have (qi , qi ) ∈ E[ej , q j , i] for all i, for all
j = 1, .., l and for all q j ⊳ Ehp(l) , q, ji. In other words, a su ient ondition is (qi′ , qi′′ ) ∈
T
{E[ej , q j , i] | q j ⊳ Ehp(l) , q, ji, j = 1..l}, from whi h we obtain the equation above (we reall that ⊔ orresponds to set-theoreti interse tion of relations). The reasoning is similar for

implies that in order to have

the

onstru tor expression. Indeed, the rule we have obtained in the previous se tion tells us

Inf(b(m) (e1 , . . . , em ), q, q~′ ) ≃ Inf(b(m) (e1 , . . . , em ), q, q~′′ ), it is su ient
′
~
Inf(ej , q j , q ) ≃ Inf(ej , q j , q~′′ ) for all (q 1 , . . . , q m ) ∈ Cart(∆(q, b(m) )) and j = 1, .., m.

that in order to have
have

As we explained before, it is desirable to
lasses (that is, small for the

⊑

ompute equivalen e relations with large equivalen e

ordering). Here is how we

relations satisfying the system of equations above.
mapping a triple

(e, q, i)

x

element of the CPO, and we

ompute su

f

onsider the CPO of fun tions

Q and we reformulate the system of
f (x) ⊑ x, where f is obtained from the
h an element, we start from x0 the smallest
e dened by xn+1 = xn ⊔ f (xn ). Sin e this

onsider the sequen

and the CPO is nite, the sequen e rea hes a
This value

x

satises

element is a tually a smallest xpoint for
fun tion

ompute a family of equivalen e

of this CPO su h that

right-hand sides of the equations. To

number of iterations.

an

First, we

to an equivalen e relation on

equation as nding an element

sequen e is monotoni

to

f,

f (x) ⊑ x

onstant value after a nite

as expe ted.

We

onje ture that this

but we have no proof of this fa t (note that the

is not monotoni ).

4.1.3 Sharing the omputation
Given the rules dening the formulas
several times. A very

Inf(e, q, ~q),

lassi al optimization

we might end up

omputing the same formula

onsists in memoizing the results of su h

omputa-

tions. This is made even more ee tive by hash- onsing the expressions. Indeed, in pra ti e, for
a given mtt pro edure, many

onstru tors have identi al expressions.

4.1.4 Complementing the output
In the example at the beginning of the previous subse tion, we have displayed a formula where
both

Inf(e, q, ~
q)

and

Inf(e, Q\q, ~
q)

appear. One may wonder what is the relation between these

two sub-formulas. Let us re all the required properties for these two formulas:

[[Inf(e, q, ~
q )]] = {v | [[p]](~v , w)
~ ∩ [[q]] 6= ∅}
[[Inf(e, Q\q, ~
q )]] = {v | [[p]](~v , w)
~ ∩ [[Q\q]] 6= ∅}

INRIA

Towards
Pra
al Type
king for
Ma omplement
ro Tree Transdu
w
~ ∈ [[~
q ]]). tiNote
thathe
[[Q\q]]
is the
of [[q]]ers
. As

(for

deterministi

fun tion (that is, if

[[Inf(e, q, ~
q )]].

omplement of

[[p]](~v , w)
~

a

15
[[p]] is a total
[[Inf(e, Q\q, ~q)]] is the

onsequen e, if

is always a singleton), then

If we extend the syntax of formula in alternating tree automata

with negation (whose semanti s is trivial to dene), we

an thus introdu e the following rule:

Inf(e, q, ~q) = ¬Inf(e, Q\q, ~q)
to be applied e.g. when the

ardinal of

q is stri

tly larger than half the

we observed a huge impa t of this optimization: the number of

ardinal of

Q.

In pra ti e,

onstru ted states is divided

by two in all our experien es, and the emptiness algorithm runs mu h more e iently.

Also,

be ause of the memoization te hnique mentioned above, this optimization allows us to share
more

omputation. That said, we don't have a

lear explanation for the very important impa t

of this optimization.
The rule above

an only be applied when the expression

fun tion. We use a very simple synta ti
pro edures

p(k)

to have exa tly one rule

a(n) .
4.2

e

denotes a total and deterministi

riterion to ensure that: we require all the rea hable

p(k) (a(n) (x1 , . . . , xn ), y1 , . . . , yk ) → e

for ea h symbol

Emptiness algorithm

In this se tion, we des ribe an e ient algorithm to

he k emptiness of an alternating tree

automaton. Instead of giving dire tly the nal version of the algorithm whi h would look quite
obs ure, we prefer to start des ribing formally a simple algorithm and then explain various
optimizations.
Let

A = (Ξ, Ξ0 , Φ)

tion 4.1.4) will be
a powerset

be an ata as dened in Se tion 2.2.

Negation (as introdu ed in Se -

onsidered later when des ribing optimizations. The basi

onstru tion to translate

A

algorithm relies on

M = (Q, QF , ∆). We
Q represents the inter-

into a bottom-up tree automaton

2Ξ . Intuitively, a state X = {X1 , . . . , Xm } in
(n) , one must thus onsider the formula
se tion of the ata states Xi . For su h a state and a tag a
V
(n)
(n)
ϕ(X, a ) = i=1,..,m Φ(Xi , a ), and put in ∆ transitions of the form X ← a(n) (X 1 , . . . , X n )
(n) ). First, we put ϕ(X, a(n) ) in disjun tive normal form, using the
to mimi the formula ϕ(X, a
DNF fun tion introdu ed in Se tion 2:
dene

Q

as the powerset

ϕ(X, a(n) ) ≃
(X 1 ,...,X n

_

)∈DNF(ϕ(X,a(n) ))

^

^

↓i X

i=1,..,n X∈X i

∆ onsists of all the transitions X ← a(n) (X 1 , . . . , X n ) su h that
(n)
(X 1 , . . . , X n ) ∈
TDNF(ϕ(X, a )). One denes QF = {{X} | X ∈ Ξ0 }. One an easily establish
that [[X]]M =
X∈X [[X]]A and thus that L(M) = L(A).
The transition relation

It is well-known that de iding emptiness of a bottom-up tree automaton

linear time. The

lassi al algorithm to do so works in a bottom up way and thus requires to

fully materialize the automaton (whi h is of exponential size
However, the

X,

the

an be done in

ompared to the original ata).

onstru tion above produ es the automaton in a top-down way: for a given state

onstru tion gives all the transitions of the form

X ← . . ..

We

an exploit this fa t to

M to be built. The
state X and returns true

derive an algorithm that doesn't ne essarily require the whole automaton
algorithm is given below in pseudo- ode. The fun tion

empty takes a
false otherwise. The test is done under a number of assertions represented by
variables P,N whi h stores sets of M-states. The set stored in P (resp. N) represents

if it is empty or
two global

RR

n° 0123456789

Alain Fris h , Haruo Hosoya

16
positive (resp. negative) emptiness assumptions: states whi h are assumed to be empty (resp.
non-empty). When the state
empty (added to

P).

X

under

transitions (for all possible tags and all
to this tag) and if a

X

onsideration is neither in

This assumption is then

P or N, it is rst

assumed to be

he ked re ursively by exploring all the in oming

omponents of the disjun tive normal form

orresponding

ontradi tion is found, the set of positive assumptions is ba ktra ked and

is added to the set of negative assumptions. This memoization-based s heme is standard for

oindu tive algorithms.

fun tion empty (X )
if X ∈ P then return true
if X ∈ N then return false
let P_saved = P in
P ← P ∪ {X};
forea h a(n) ∈ Σ
if not (empty_formula (ϕ(X, a(n) ))) then
P ← P_saved
N := N ∪ {X}
return false
return true
fun tion empty_formula (φ)
forea h (X 1 , . . . , X n ) ∈ DNF(φ)
if not (empty_sub (X 1 , . . . , X n )) then
return false
return true
fun tion empty_sub (X 1 , . . . , X n )
forea h 1 ≤ i ≤ n
if (empty X i ) then
return true
return false
This algorithm is not linear in the size of the automaton
This ba ktra king

M be

ause of the ba ktra king on

P.

an be avoided (as des ribed in [6℄, Chapter 7 or in [22℄), but the te hnique is

rather involved and would make the presentation of the optimizations quite obs ure. Moreover,
we have indeed implemented the non-ba ktra king version (with all the optimizations) but we
did not observe any noti eable speedup in our tests.
A rst optimization improves the ee tiveness of the memoization sets

P and N. It is based on
′
′
[[X 2 ]] ⊆ [[X 1 ]]. As a onsequen e, if X ⊆ X for some X ∈ P, then
′
′
empty(X) an immediately return true. Similarly, if X ⊆ X for some X ∈ N, then empty(X)
an immediately return false.
the fa t that if

X1 ⊆ X2

then

Enumeration and pruning of the disjun tive normal form

The disjun tive normal form

of a formula

Our rst improvement

an be exponentially larger than the formula itself.

on-

sists in not materializing it but enumerating it lazily with a pruning te hnique that avoids the
exponential behavior in many

ases.

fun tion empty_formula (φ)

INRIA

Towards
ti al Type([heφ℄,(
king∅, for
return Pra
(empty_dnf
. . . ,Ma
∅)))ro Tree Transdu ers

17

fun tion empty_dnf (l,((X 1 , . . . , X n ) as a)) =
mat h l with
| [℄ -> return false
| ⊤ :: rest -> return (empty_dnf (rest,a))
| ⊥ :: rest -> return true
| φ1 ∨ φ2 :: rest ->
if not (empty_dnf (φ1 :: rest,a)) then return false
return (empty_dnf (φ2 :: rest,a))
| φ1 ∧ φ2 :: rest ->
return (empty_dnf (φ1 ::φ2 ::rest,a))
| ↓h X :: rest ->
if empty (X h ∪ {X})) then return true
return (empty_dnf (rest,(X 1 , . . . , X h ∪ {X}, . . . , X n )))
The rst argument of

empty_dnf

is a list of formula whose

disjun tive normal form. The se ond argument is an
symbol) whi h a

umulates a prex of the

built. When an atomi
the a

formula

↓1 X ∧ φ

where

X

a

As a

X

is added to the

h-th

omponent of

turns out to be empty, the enumeration will not even look at

onsequen e, when the fun tion

omponent of the a

empty_dnf

The order in whi h we

φ.

This

umulator denotes an empty

rea hes an empty list of formulas, the

false.

φ1 ∨ φ2

X h ∪ {X}

an prune the enumeration. For instan e, for a formula of the

umulator represents an element of the disjun tive normal form for whi h

return

urrent

urrent term of the disjun tive normal form being

is found, the state

optimization enfor es the invariant that no
set.

is the arity of the

umulator. Here we have in luded an important optimization: if the new state

denotes an empty set, then one
form

↓h X

onjun tion must be put in

n-tuple (where n

onsider the two sub-formulas

φ1

and

φ2

empty_sub

in the formulas

would

φ1 ∧ φ2

and

might have a big impa t on performan es. It might be worthwhile to look for heuristi s

guiding this

Witness

hoi e.

It is not di ult to see that the algorithm

produ e a witness for non-emptiness (that is, when

an be further instrumented in order to

false, it also returns a
N a witness, and we also
atta h a witness to ea h omponent of the a umulator (X 1 , . . . , X n ) in the enumeration for
the disjun tive normal form. When he king for the emptiness of X h ∪ {X}, we know that X h
is a non-empty state, and we have at our disposal a witness v for this state. Before doing the
re ursive all to empty, we an rst he k whether this witness v is in [[X]] (this an be done
very e iently). If this is the ase, we know that X h ∪ {X} is also non-empty. In pra ti e, this
optimization avoids many alls to empty.
tree

v

whi h belongs to

[[X]]).

Negation and reexivity

empty(X)

returns

To do so, we keep for ea h state in

We have mentioned in Se tion 4.1.4 an optimization whi h intro-

du es alternating formulas with negation. Using De Morgan's laws, we
down and thus assume that it

an push the negation

an only appear immediately above an atomi

formula

ourse, it is possible to get rid of the negation by introdu ing for ea h state

¬X

whose transition formula (for ea h tag) is the negation of the one for

X;

X

↓i X .

Of

a dual state

this only doubles

the number of states. However, we prefer to support dire tly in the algorithm negated atomi

RR

n° 0123456789

18
formulas

¬ ↓i X , be
↓i X . The

ause we

Alain Fris h , Haruo Hosoya

an use the very simple fa t that it denotes a set whi h does not

algorithm is thus modied to work with pairs of sets of A-states, written
interse t
T
S
(X, Y ), whi h intuitively represents the set X∈X [[X]]A \ Y ∈Y [[Y ]]A . We dene ϕ((X, Y ), a(n) )
V
V
(n) )∧
(n) ). The fa t mentioned above translates itself into a shortas
X∈X Φ(X, a
Y ∈Y ¬Φ(Y, a
ut ase in the empty fun tion: if the input is (X, Y ) with X ∩ Y 6= ∅, then the result is true
(meaning that (X, Y ) trivially denotes an empty set of trees).
The interesting

ases for enumeration of the normal form are:

| ↓h X :: rest ->
if empty (X h ∪ {X})) then return true
return (empty_dnf (rest,((X 1 , Y 1 ), . . . , (X h ∪ {X}, Y h ), . . . , (X n , Y n ))))
| ¬ ↓h Y :: rest ->
if empty (Y h ∪ {Y })) then return true
return (empty_dnf (rest,((X 1 , Y 1 ), . . . , (X h , Y h ∪ {Y }), . . . , (X n , Y n ))))

Prepro essing

Note the following trivial fa ts:

φ1

or

φ2

For a formula

φ1 ∨ φ2

φ1 ∧ φ2

to be empty, it is

φ1
(n)
and φ2 empty; for a formula ↓i X to be empty, it is su ient to have all the formulas Φ(X, a
)
(n) )
empty; for a formula ¬ ↓i X to be empty, it is su ient to have all the formulas ¬Φ(X, a
su ient to have

empty; for a formula

to be empty, it is su ient to have

empty.
Using these su ient

onditions and a largest xpoint

e ient approximation of emptiness for formulas (it returns
empty, but it may also return
any subformula
empty with
or

∧).

⊤

φ whi

false

is this

only if the formula is indeed

ase). We use this approximate

riterion to repla e

⊥ and any subformula φ su h that ¬φ is trivially
tautologies to eliminate ⊥ and ⊤ as arguments of ∨

h is trivially empty with

(and then apply Boolean

In pra ti e, this optimization is very ee tive in redu ing the size and

formulas involved in the real (exa t) emptiness

5

omputation, we get a sound and

true

omplexity of

he k.

Experiments

We have experimented on our type he ker with various XML transformations implemented as
mtts.

Although we did not try very big transformations, we did work with large input and

output tree automata automati ally generated from the XHTML DTD (without taking XML
attributes into a

ount). Note that be ause this DTD has many tags, the mtts a tually have

many transitions sin e they typi ally

opy tags, whi h requires all

onstru tors

orresponding to

these tags to be enumerated. They do not have too many pro edures, though. The bottom-up
deterministi

automaton that we generated from the XHTML DTD has 35 states.

Table 1 gives the elapsed times spent in type he king several transformations and the number
of states of the inferred alternating tree automaton that have been materialized. The experiment
was

ondu ted on an Intel Pentium 4 pro essor 2.80Ghz, running Linux kernel 2.4.27, and the

type he king time in ludes the whole pro ess (determinization of the output type, ba kward
inferen e, interse tion with the input type, emptiness
in and

he k). The type he ker is implemented

ompiled by Obje tive Caml 3.09.3.

We also indi ate the number of pro edures in ea h mtt, the maximum number of parameters,
and the minimum integer
itively, the integer

b

b,

if any, su h that the mtt is synta ti ally

b-bounded

opying. Intu-

aptures the maximum number of times the mtt traverses any node of the

input tree. This notion has been introdu ed in [12℄ where the existen e of

b

is shown to imply

INRIA

Towards Pra ti al Type he king for Ma ro Tree Transdu ers

19
the polynomiality of the algorithm des ribed in that paper (see also Appendix A.2). Here, we
observe that even unbounded- opying mtts
Transformation:

an be type he ked e iently.

(1)

(2)

(3)

(4)

(5)

(6)

(7)

# of pro edures:

2

2

3

5

4

6

6

Max # of parameters:

1

1

1

1

2

2

2

Bounded

1

1

2

∞

∞

2

1

1057

1042

0373

0377

0337

0409

0410

147

147

43

74

37

49

49

opying:

Type- he king time (ms):
# of states in the ata:

Table 1: Results of the experiments
Unless otherwise stated, transformations are
input and output types are

XHTML).

he ked to have type

XHTML→XHTML (i.e.,
<b> tags, keeping

Transformation (1) removes all the

ontents. Transformation (2) is a variant that drops the
dete ts that the latter doesn't have type

XHTML→XHTML

<div>

both
their

tags instead. The type he ker

by produ ing a

ounter-example:

<html><head><title/></head><body><div/></body>
Indeed, removing the

<div>

element may produ e a

whi h is not valid in XHTML. Transformation (3)
sponding subtrees) into a new

<div>

<body>

element and prepends

Transformation (4) groups together adja ent

element with an empty

ontent,

<a> elements (and their orrethe <div> to the <body> element.

opies all the

<b> elements,

on atenating their

ontents. Trans-

formation (5) extra ts from an XHTML do ument a tree of depth 2 whi h represents the
tual nesting stru ture of

<h1>

and

<h2>

on ep-

heading elements (note that, in XHTML, the stru ture

among headings is at). Transformation (6) builds a tree representing a table of

ontents for

the top two levels of itemizations, giving se tion and subse tion numbers to them (where the
numbers are

onstru ted as Peano numerals), and prepends the resulting tree to the

element. Transformation (7) is a variant that only returns the table of
We have also translated some transformations (that

<body>

ontents.

an be expressed as mtts) used by

html opy, inventory, pref2app, pref2html, pref opy).
2ms and 6ms to type he k these mtts, ex ept for inventory

Tozawa and Hagiya in [26℄ (namely
Our implementation takes between

for whi h it takes 22 ms. Tozawa and Hagiya report performan e between 5ms and 1000ms on
a Pentium M 1.8 Ghz for the satisability

he k (whi h

orresponds to our emptiness

he k and

ex ludes the time taken by ba kward inferen e). Although these results indi ate our advantages
over them to some extent, sin e the numbers are too small and they have not undertaken
experiments as big as ours, it is hard to draw a meaningful

6

on lusion.

Con lusion and Future Work

We have presented an e ient type he king algorithm for mtts based on the idea of using
alternating tree automata for representing the preimage of the given mtt obtained from the
ba kward type inferen e.

This representation was useful for deriving optimization te hniques

on the ba kward inferen e phase su h as state partitioning and Cartesian fa torization, and
was also ee tive for speeding up the subsequent emptiness
equivalen es among formulas.

Our experimental results

he k phase by exploiting Boolean

onrmed that our te hniques allow

us to type he k small sizes of transformations with respe t to the full XHTML type. Finally,

RR

n° 0123456789

20
we have also made an exa t

Alainlassi
Frisalh one
, Haruo
Hosoya
and Maneth-

onne tion to two known algorithms, a

Perst-Seidl's, the latter implying an important polynomial

omplexity under a bounded- opying

restri tion.
The present work is only the rst step toward a truly pra ti al type he ker for mtts.

In

the future, we will seek for further improvements that allow type he king larger and more
ompli ated transformations. In parti ular, transformations with upward axes
by

ompositions of mtts as proved in [11℄ and a

apability to type he k su h

an be obtained

ompositions of mtts

in a reasonable time will be important. We have some preliminary ideas for the improvement
and plan to pursue them as a next step. In the end, we hope to be able to handle (at least a
reasonably large subset of ) XSLT.

Referen es
[1℄ N. Alon, T. Milo, F. Neven, D. Su iu, and V. Vianu. XML with data values: Type he king
revisited. In

Pro eedings of Symposium on Prin iples of Database Systems (PODS), 2001.

[2℄ A. W. Appel and D. B. Ma Queen.

Standard ML of New Jersey.

In

Third Int'l Symp.

on Prog. Lang. Implementation and Logi Programming, pages 113. Springer-Verlag, Aug.

1991.
[3℄ V. Benzaken, G. Castagna, and A. Fris h. CDu e: An XML- entri
guage. In

general-purpose lan-

Pro eedings of the International Conferen e on Fun tional Programming (ICFP),

pages 5163, 2003.
[4℄ J. Engelfriet and S. Maneth.
transdu ers.

A

omparison of pebble tree transdu ers with ma ro tree

A ta Informati a, 39(9):613698, 2003.

[5℄ J. Engelfriet and H. Vogler. Ma ro tree transdu ers.

J. Comput. Syst. S i., 31(1):710146,

1985.
[6℄ A. Fris h.

Théorie, on eption et réalisation d'un langage de programmation adapté à XML.

PhD thesis, Universit Paris 7, 2004.
[7℄ H. Hosoya.

Regular expression lters for XML.

16(6):711750, 2006.

Journal of Fun tional Programming,

Short version appeared in Pro eedings of Programming Te hnolo-

gies for XML (PLAN-X), pp.1327, 2004.

ACM Transa tions
on Internet Te hnology, 3(2):117148, 2003. Short version appeared in Pro eedings of Third

[8℄ H. Hosoya and B. C. Pier e. XDu e: A typed XML pro essing language.

International Workshop on the Web and Databases (WebDB2000), volume 1997 of Le ture
Notes in Computer S ien e, pp. 226244, Springer-Verlag.

ACM Transa tions on Programming Languages and Systems, 27(1):4690, 2004. Short version appeared in

[9℄ H. Hosoya, J. Vouillon, and B. C. Pier e. Regular expression types for XML.

Pro eedings of the International Conferen e on Fun tional Programming (ICFP), pp.11-22,
2000.
[10℄ X. Leroy, D. Doligez, J. Garrigue, J. Vouillon, and D. Rémy. The Obje tive Caml system.
Software and do umentation available on the Web,

http://pauilla .inria.fr/o aml/,

1996.

INRIA

Towards Pra ti al Type he king for Ma ro Tree Transdu ers he king with ma ro tree trans21
du ers. In Pro eedings of Symposium on Prin iples of Database Systems (PODS), pages

[11℄ S. Maneth, T. Perst, A. Berlea, and H. Seidl. XML type
283294, 2005.
[12℄ S. Maneth, T. Perst, and H. Seidl.

Exa t XML type

he king in polynomial time.

International Conferen e on Database Theory (ICDT), pages 254268, 2007.

In

[13℄ W. Martens and F. Neven. Type he king top-down uniform unranked tree transdu ers. In

Pro eedings of International Conferen e on Database Theory, pages 6478, 2003.

[14℄ W. Martens and F. Neven. Frontiers of tra tability for type he king simple XML transformations. In

Pro eedings of Symposium on Prin iples of Database Systems (PODS),

pages

2334, 2004.

Pro eedings of
Symposium on Prin iples of Database Systems, pages 215226, Philadelphia, May 1999.

[15℄ T. Milo and D. Su iu. Type inferen e for queries on semistru tured data. In

Pro eedings
of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on Prin iples of Database
Systems, pages 1122. ACM, May 2000.

[16℄ T. Milo, D. Su iu, and V. Vianu.

Type he king for XML transformers.

[17℄ A. Møller, M. Ø. Olesen, and M. I. S hwartzba h. Stati

validation of XSL Transformations.

Te hni al Report RS-05-32, BRICS, O tober 2005. Draft, a

epted for TOPLAS.

[18℄ M. Murata. Transformation of do uments and s hemas by patterns and
tions. In

In

ontextual

ondi-

Prin iples of Do ument Pro essing '96, volume 1293 of Le ture Notes in Computer

S ien e, pages 153169. Springer-Verlag,

1997.

[19℄ K. Nakano and S.-C. Mu. A pushdown ma hine for re ursive XML pro essing. In

APLAS,

pages 340356, 2006.
[20℄ T. Perst and H. Seidl. Ma ro forest transdu ers.

Information Pro essing Letters, 89(3):141

149, 2004.
[21℄ G. Slutzki. Alternating tree automata.

Theoreti al Computer S ien e, 41:305318, 1985.

[22℄ T. Suda and H. Hosoya. Non-ba ktra king top-down algorithm for
ontainment.

In

he king tree automata

Pro eedings of Conferen e on Implementation and Appli ations of Au-

tomata (CIAA), pages 8392, 2005.
[23℄ A. Tozawa. Towards stati

type

on Do ument Engineering, 2001.

[24℄ A. Tozawa. XML type

he king for XSLT. In

Pro eedings of ACM Symposium

he king using high-level tree transdu er. In

Programming (FLOPS), pages 8196, 2006.

[25℄ A. Tozawa and M. Hagiya. XML s hema

ontainment

Fun tional and Logi

he king based on semi-impli it te h-

8th International Conferen e on Implementation and Appli ation of Automata,
volume 2759 of Le ture Notes in Computer S ien e, pages 213225. Springer-Verlag, 2003.
niques. In

[26℄ A. Tozawa and M. Hagiya. E ient de ision pro edure for a logi
manus ipt, 2004.

RR

n° 0123456789

for XML. unpublished

22
A

Alain Fris h , Haruo Hosoya

Comparison

In this se tion, we

ompare our algorithm with two existing algorithms, the

lassi al one based

on fun tion enumeration and the Maneth-Perst-Seidl algorithm.

A.1
The

Classi al Algorithm
lassi al algorithm presented here is known as a folklore.

literature for deterministi
a dbta

M = (Q, QF , ∆)

Variants

an be found in the

mtts [4℄ and for ma ro forest transdu ers [20℄. The algorithm takes

and an mtt

T = (P, P0 , Π)

and builds a dbta

N ′ = (D, DF , δ)

where:

= {hp(m) , ~
q i | p(m) ∈ P, ~q ∈ Qm } → 2Q
= {d ∈ D | p0 ∈ P0 , d(hp0 i) ∩ QF 6= ∅}
~ | d(hp(m) , ~qi) = S (m) (n)
~ q )}
= {d ← a(n) (d)
(p
(a (~
x),~
y )→e)∈Π DInf(e, d, ~

D
DF
δ

Here, the fun tion

DInf

is dened as follows.

~~
~ ~q) ∀j = 1, . . . , m }
DInf(b(m) (e1 , . . . , em ), d,
q ) = {q ′ | q ′ ← b(m) (q~′ ) ∈ ∆, qj′ ∈ DInf(ej , d,
S
′
~~
~ ~q), i = 1, . . . , l}
DInf(p(xh , e1 , . . . , el ), d,
q) =
{dh (hp, q~′ i) | qi ∈ DInf(ei , d,
~
DInf(yj , d, ~
q)
= {qj }
The

onstru ted automaton

N′

has, as states, the set of all fun tions that map ea h pair of a

d represents the set of
p(m) and states ~q, the set of results of evaluating p with
~ of types ~q is exa tly des ribed by the states d(hp, ~qi). Thus, the
the tree v and parameters w
initial states DF represent the set of trees v su h that the set of results from evaluating an initial
pro edure p0 with v ontains a tree a epted by the given dbta M.
~ from D , and states ~q from Q,
The fun tion DInf omputes, from given expression e, states d
v of trees
the set of states that exa tly des ribes the set of results of evaluating e with a tuple ~
~ for all
~ and parameters of types ~
q . Then we an olle t in δ transitions d ← a(n) (d)
of types d
(n)
(m)
~
a and all d su h that d is omputed for all p
and all ~
q by using DInf with the expression
pro edure and parameter types to a set of states. Intuitively, ea h state

trees

on

v

su h that, given a pro edure

p(m) 's

ea h rule for the symbol

a(n) .

By this intuition, ea h of the three

ases for

DInf

an

be understood as follows.



The set of results of evaluating the

~′ that have a transition q ′
the set of states q
results of evaluating the



evaluating

p

with the

qi′

b(m) (q~′ )

orresponding subexpression

h-th

input tree

an be obtained by

where ea h



←

The set of results of evaluating the pro edure
This set

b(m) (e1 , . . . , em ) is des ribed by
∈ ∆ su h that ea h qi′ des ribes the
ei .

onstru tor expression

vh

all

p(xh , e1 , . . . , el )

is the set of results of

and parameters resulted from evaluating ea h

olle ting the results of applying the fun tion

is one of the states that des ribe the set of results of

The set of results of evaluating the variable expression

yj

dh

to

p

and

ei .
q~′

ei .

is exa tly des ribed by its type

qj .
Thus, the intuition behind is rather dierent from our approa h.
that the resulting automaton from the

Nevertheless, we

lassi al algorithm is isomorphi

an prove

to the one obtained from

our approa h followed by determinization.

INRIA

Towards
Pra ti al Type
kinganforbeMa
ro as
Tree
Transdu
ers an
Determinization
of anhe
ata
done
follows.
From
dbta

N = (R, RF , Γ)

A = (Ξ, Ξ0 , Φ),

ata

we build23
a

where

= 2Ξ
= {r ∈ Ξ | r ∩ Ξ0 6= ∅}
= {r ← a(n) (~r) | r = {X | ~r ⊢ Φ(X, a(n) )}}.

R
RF
Γ
Here, the judgment

~r ⊢ φ

 ~r ⊢ φ1 ∧ φ2

if

~r ⊢ φ1

and

 ~r ⊢ φ1 ∨ φ2

if

~r ⊢ φ1

or

is dened indu tively as follows.

~r ⊢ φ2 .

~r ⊢ φ2 .

 ~r ⊢ ⊤.
 ~r ⊢↓i X

if

~r ⊢ φ
ri .

That is,
the set

X ∈ ri .

intuitively means that

φ

holds by interpreting ea h

↓i X

as  X is a member of

The intuition behind determinization of an ata is the same as that of a nondeterministi

r

in

N

and do not have type

Y

for all non-members

tree automaton. That is, ea h state
members

X

of

r

[[r]] =

\

annot have type

[

[[X]] \
r

of

that have type

[[Y ]]

and

r′

X

for all

(6)

r 6= r ′ . Thus, the
trees, that is, N is omplete and
between A and N sin e ea h nal

at the same time when

states of the tree automaton

N

deterministi . From this, we

an understand the equivalen e

form a partition of all the

A and therefore the set of su h nal states
A. Then, by using the formula (6),
r ⊢ φ implies that [[ri ]] ⊆ [[X]].
the interpretation  X is ontained in ri  of ↓i X in the judgment ~
Here, we an see a parallelism between the intuition of the judgment ~
v ⊢ φ (where ↓i X is
r ⊢ φ. Indeed, a key property to the proof below is: ~v ⊢ φ if
interpreted  vi ∈ [[X]]) and that of ~
and only if ~
r ⊢ φ for some ~r su h that ~v ∈ [[~r]].
state in

N

Y

Y 6∈r

X∈r
This implies that any tree

v
r.

denotes the set of trees

ontains an initial state in the original ata

forms a partition of the sets denoted by the initial states of

Proposition 2
Proof:

A

and N are equivalent.

To prove the result, it su es to show the following.

v ∈ [[r]] ⇐⇒ r = {X | v ∈ [[X]]}.

(7)

(Note that this is a rewriting of the equation (6).) Indeed, this implies

v ∈ L(N )

⇐⇒
by(7)

v ∈ [[RF ]]

⇐⇒

∃r. (r ∩ Ξ0 6= ∅ ∧ r = {X | v ∈ [[X]]})

⇐⇒

∃X ∈ Ξ0 . v ∈ [[X]]

⇐⇒

v ∈ L(A).

The proof pro eeds by indu tion on the stru ture of

v.

To show (7), the following is su ient

(∃~r. ~v ∈ [[~r]] ∧ ~r ⊢ φ) ⇐⇒ ~v ⊢ φ.

RR

n° 0123456789

(8)

Alain Fris h , Haruo Hosoya

24
sin e this implies (7):

a(n) (~v ) ∈ [[r]]

⇐⇒

∃(r ← a(n) (~r)) ∈ Γ. ~v ∈ [[~r]]

⇐⇒

∃~r. r = {X | ~r ⊢ Φ(X, a(n) )} ∧ ~v ∈ [[~r]]

⇐⇒

by(8)

r = {X | ~v ⊢ Φ(X, a(n) )}

⇐⇒

r = {X | a(n) (~v ) ∈ [[X]]}.
φ.
ri = {X | vi ∈ [[X]]}

The proof of (8) itself is done by indu tion on the stru ture of
straightforward.

For the if  dire tion, let

indu tion hypothesis, (7) gives

vi ∈ [[ri ]].



Case

φ = ⊥.

This never arises.



Case

φ = ⊤.

This

Case

φ =↓h X .



rh .


The rest is

The only if  dire tion is
for

ase analysis on

i = 1, . . . , n.

By the

φ.

ase trivially holds.

From

~v ⊢ φ,

we have

vh ∈ [[X]]

and therefore

X ∈ rh

by the denition of

This implies the result.

φ = φ1 ∧ φ2 . By the indu
r~′′ ⊢ φ2 for some r~′ and r~′′ . Sin

tion hypothesis,

Case

e

N

~v ∈ [[r~′ ]]

and

is deterministi , both

r~′

r~′ ⊢ φ1 with ~v ∈ [[r~′′ ]] and
and r~′′ a tually equal to ~
r.

Hen e the result follows.



Case

φ = φ1 ∨ φ2 .

Similar to the previous



ase.

Proposition 3 Let N be obtained by determinizing the ata from the last se tion. Then, N and
N′

are isomorphi .

Dene the fun tion

Proof:

β

from

D

to

R

as follows:

β(d) = {hp(m) , q, ~
q i | p(m) ∈ P, ~q ∈ Qm , q ∈ d(hp, ~qi)}
Clearly,

β

is bije tive:

isomorphism between

β −1 (r)(hp, ~
q i) = {q | hp(m) , q, ~qi ∈ r}. It remains to show that β is an
′
N and N , that is, (1) β(DF ) = RF and (2) β(δ(d)) = Γ(β(d)) for ea h

d.
The

ondition (1)

learly holds sin e

d(p0 ) ∩ QF 6= ∅

i

hp0 , qi ∈ β(d)

for some

q ∈ QF .

To

prove (2), it su es to show

~~
q ∈ DInf(e, d,
q)
Here,

β(d1 , . . . , dk )

i

~ ⊢ Inf(e, q, ~q).
β(d)

stands for

(β(d1 ), . . . , β(dk )).

The proof is by indu tion on the stru ture of

e.


Case

e = b(m) (e1 , . . . , em ).
~~
q ∈ DInf(e, d,
q)

⇐⇒

~ ~q)
∃(q ← b(m) (q~′ )) ∈ ∆. ∀j. qj′ ∈ DInf(ej , d,

byI.H.

~ ⊢ Inf(ej , q ′ , ~q)
∃(q ← b(m) (q~′ )) ∈ ∆. ∀j. β(d)
j
_
^
′
~
β(d) ⊢
Inf(ej , qj , ~q)

⇐⇒

⇐⇒

(q←b(m) (q~′ ))∈∆ j=1...,m

⇐⇒

~ ⊢ Inf(e, q, ~q)
β(d)

INRIA

Towards
al hType
for Ma ro Tree Transdu ers
 CasePra
e =tip(x
, e1 , . .he
. , eking
l ).
~~
q ∈ DInf(e, d,
q)

⇐⇒
⇐⇒
byI.H.

⇐⇒

⇐⇒

25

[
~ ~q), i = 1, . . . , l}
{dh (p, q~′ ) | qi′ ∈ DInf(ei , d,
∃q~′ . q ∈ dh (p, q~′ )

and

~ q~′ )
∀i. qi′ ∈ DInf(ei , d,

~ ⊢ Inf(ei , q, q~′ )
∃q~′ . hp, q, q~′ i ∈ β(dh ) and ∀i. β(d)
_ ^
~ ⊢
β(d)
Inf(ei , q, q~′ )∧ ↓i hp, q, q~′ i
q~′ ∈Ql i=1,...,l

⇐⇒


Case

e = yj .

~ ~q) i q = qj . If q = qj , then Inf(e, q, ~q) = ⊤ and
q ∈ DInf(yj , d,
holds. If q 6= qj , then Inf(e, q, ~
q ) = ⊥ and therefore the RHS does not


First,

therefore the RHS
hold.

A.2

~ ⊢ Inf(e, q, ~q)
β(d)

Maneth-Perst-Seidl Algorithm

First, for simpli ity in

omparing the two algorithms, following [12℄, we

onsider an mtt where

the input type is already en oded into pro edures. That is, instead of the original mtt
take an mtt

T

′ and a bta

Min

T (v) =
T′

that

{v | T



behaves exa tly the same as

the other inputs. See [12℄ for a

′ (v)

we

su h that

′

That is,

T,

on rete

T (v) (v ∈ L(Min ))
∅
(otherwise).

T

for the inputs from

L(Min )

but returns no result for

onstru tion. Having done this, we only need to

he k

∩ L(M) 6= ∅} = ∅.

In Maneth-Perst-Seidl algorithm, we
to the output-type dbta
an be done by

onstru

U from T ′ = (P, P0 , Π) spe ialized
U (v) = T ′ (v) ∩ L(M) for any tree v . This

onstru t a new mtt

M = (Q, QF , ∆) su h that
ting the mtt U = (S, S0 , Ω) where
(m)

S = {hp(m) , q, ~
qi
| p(m) ∈ P, q, ~q ∈ Qm }
S0 = {hp0 , qi | p0 ∈ P0 , q ∈ QF }
Ω = {hp(m) , q, ~
q i(a(n) (~x), ~y ) → e′ | (p(m) (a(n) (~x), ~y ) → e) ∈ Π, e′ ∈ Spec(e, q, ~q)}.
Here, we dene the fun tion

Spec

as follows.

Spec(a(e1 , . . . , en ), q, ~
q)
= {a(e′1 , . . . , e′n ) | q ← a(q1′ , . . . , qn′ ) ∈ ∆, ∀i. e′i ∈ Spec(ei , qi′ , ~q)}
Spec(p(xh , e1 , . . . , el ), q, ~
q ) = {hp, q, q~′ i(xh , e′1 , . . . , e′l ) | q~′ ∈ Ql , ∀i. e′i ∈ Spec(ei , qi′ , ~q)}
Spec(yi , q, ~q)
= {yi }
Intuitively, ea h pro edure
parameters

w
~

of types

q,
~

hp, q, ~
qi

in the new mtt

the same results as

p

U

yields, for any input value

but restri ted to type

v

and for any

q:

[[hp(m) , q, ~
q i]](v, w)
~ = [[p(m) ]](v, w)
~ ∩ [[q]]
Spec(e, q, ~
q ) yields, for any input
results as e but restri ted to type q :

Similarly,
same

values

~v

and for all parameters

[[Spec(e, q, ~q)]](~v , w)
~ = [[e]](~v , w)
~ ∩ [[q]]

RR

n° 0123456789

w
~

of types

~q,

the

26
After thus

onstru ting the mtt

U (v) = ∅ for any
ρ′ where

i.e.,

impli ations

value

v.

U,

the remaining is to

This

Alain Fris h , Haruo
U isHosoya
empty,

he k that the translation of

an be done as follows. Dene rst the following system of

we introdu e propositional variables

X

onsisting of all subsets of

S:

ρ′ = {X ⇐ X 1 ∧ . . . ∧ X n | ∃a(n) . ∃e1 , . . . , ek . ∀s(m) ∈ X. ∃j. (s(m) (a(n) (~x), ~y ) → ej ) ∈ Ω,
∀i = 1, . . . , n. X i = {s′ ∈ S | ∃j = 1, . . . , k. s′ (xi , . . .) o urs in ej }}
and then verify that

ρ′ ⊢ {s}

whether there is some input

for some

v

s ∈ S0 .

Intuitively, ea h propositional variable

from whi h any pro edure in the set

X

X

denotes

translates to some value

with some parameters:

∃v. ∀s(m) ∈ X. ∃w.
~ [[s(m) ]](v, w)
~ 6= ∅
Now, we

an prove that the system of impli ations obtained from the MPS and the one from

our algorithm are exa tly the same. From this, we

an dire tly

arry over useful properties found

for the MPS algorithm to our algorithm. In parti ular, our algorithm has the same polynomial
time

omplexity under the restri tion of a nitely bounded number of

Proposition 4 Given an input type that a epts all trees and the mtt

opying [12℄.

dened above, let A
and ρ be the ata and the system of impli ations obtained by the algorithm in Se tion 3. Let Ξ0
be A's initial states. Then, (ρ, Ξ0 ) and (ρ′ , S0 ) are identi al.
Proof:

T′

ρ and ρ′ onsist of all variables X where X is from the set P × Q × Qm .
′
showing X ⇐ X 1 ∧ . . . ∧ X n ∈ ρ i X ⇐ X 1 ∧ . . . ∧ X n ∈ ρ . It su es to

Note that both

The result follows by
show for any

X

and

i,

∃e1 , . . . , ek . ∀s ∈ X. ∃j. (s(a(~x), ~y ) → ej ) ∈ Ω, X i = {s′ ∈ S | ∃j = 1, . . . , k. s′ (xi , . . .)

o

urs in

ej }

i

(X 1 , . . . , X n ) ∈ DNF(

^

Φ(s, a)).

s∈X
This follows by showing that, for all

(X 1 , . . . , X n ) ∈ DNF(Inf(e1 , q1 , ~q1 ) ∧ . . . ∧ Inf(ek , qk , ~qk )),

∃j = 1, . . . , k. s′ (xi )
This

an be proved by indu tion on

o

urs in

Spec(ej , qj , ~qj ) ⇐⇒ s′ ∈ X i .

|e1 | + . . . + |ek |

where

|e|

is the size of

e.



Corollary 1 For any b-bounded opying mtt, our algorithm runs in polynomial time.
B

Alternating tree automata with bounded traversing

The

orollary in the last se tion depends on the proof of polynomiality from [12℄. It gives the

information that the emptiness

he k for alternating automata has polynomial time

when the alternating automata is obtained by the basi
Se tion 3 when applied to a
the notion of

b-bounded

of the emptiness
Let

b[X]

b-bounded

omplexity

ba kward inferen e algorithm from

opying mtt. It seems natural to look for a

ounterpart of

opying for alternating automata that dire tly ensures the polynomiality

he k.

A = (Ξ, Ξ0 , Φ) be an ata.

as the least xpoint of a

X ∈ Ξ, we dene the maximal traversal number
system over N = {1 < 2 < . . . < ∞}, the omplete

For ea h state

onstraint

INRIA

Towards Pra ti al Type he king for
Tree Transdu
ersonsists of all the
∞. Ma
Theroonstraint
system

latti e of naturals extended with

27
onstraints of the

form:

b[X] ≥ bi [Φ(X, a(n) )]
for

a(n) ∈ Σ

and

1 ≤ i ≤ n,

where

bi [φ]

is dened indu tively:

bi [⊤]
bi [⊥]
bi [φ1 ∧ φ2 ]
bi [φ1 ∨ φ2 ]
bi [↓h X]
The ata

A

is (synta ti ally)

b-bounded

=
=
=
=

0
0
bi [φ1 ] + bi [φ2 ]
max(b
i [φ1 ], bi [φ2 ])

b[X] if i = h
=
0 if i 6= h

traversing if

b[X] ≤ b

for all

X ∈ X0 .

We mention without proving it formally that when we apply our ba kward inferen e algo-

b-bounded opying mtt, then the resulting ata is b-bounded traversing. More pre isely,
b[hp(k) , q, ~
q i] ≤ b[p(k) ] where b[p(k) ] denotes the maximal opy number for the
(k) , as dened in [12℄. As a matter of fa t, the optimizations given in Se tion 4.1
edure p

rithm to a
we
pro

an show that

preserve this property (but the ata formally has exponentially many more states, even if in
pra ti e only a fra tion of them is going to be materialized).
he k for a b-bounded traversing ata runs
ΣX∈X b[X]. For any b-formula φ and (X 1 , . . . , X n ) ∈
DNF(φ) and 1 ≤ i ≤ n, we observe that b[X i ] ≤ bi [φ]. The
V proof is by(n)indu tion on the stru ture
)), we have b[X i ] ≤ b[X].
of φ. As a onsequen e, for any (X 1 , . . . , X n ) ∈ DNF( X∈X Φ(X, a
So, if the ata is b-bounded traversing, then the emptiness he k algorithm will only onsider set
of states X su h that b[X] ≤ b. Sin e b[X] is a lower bound for the ardinal of X (be ause
b[X] ≥ 1 for all X ), we see that the algorithm only looks at a polynomial number of set of states
X.
To on lude this se tion, we observe that the interse tion of a b-bounded traversal ata and
′
′
a b -bounded traversal ata is a (b + b )-bounded traversal ata, and that a non-deterministi tree
automaton is isomorphi to a 1-bounded traversal ata. This is useful to type he k a b-bounded
opying mtt, be ause we need to ompute the interse tion of the inferred ata, whi h is b-bounded
Now it remains to establish that the emptiness

in polynomial time.

We dene

b[X]

as

traversal, and of the input type, whi h is given by a non-deterministi
result, we obtain a

RR

n° 0123456789

(b + 1)-bounded

ata.

tree automaton.

As a

Alain Fris h , Haruo Hosoya

28
Contents

1 Introdu tion

3

2 Preliminaries

4

2.1

Ma ro Tree Transdu ers

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

2.2

Tree Automata and Alternation . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

3 Type he king

6

3.1

Ba kward inferen e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.2

Emptiness

he k

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4 Algorithm and optimizations
4.1

4.2

6
10

11

Ba kward inferen e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11

4.1.1

Cartesian fa torization . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11

4.1.2

State partitioning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

12

4.1.3

Sharing the

4.1.4

Complementing the output

omputation . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Emptiness algorithm

14

. . . . . . . . . . . . . . . . . . . . . . . . . .

14

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

15

5 Experiments

18

6 Con lusion and Future Work

19

A Comparison

22

A.1

Classi al Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

22

A.2

Maneth-Perst-Seidl Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

25

B Alternating tree automata with bounded traversing

26

INRIA

Unité de recherche INRIA Rocquencourt
Domaine de Voluceau - Rocquencourt - BP 105 - 78153 Le Chesnay Cedex (France)
Unité de recherche INRIA Futurs : Parc Club Orsay Université - ZAC des Vignes
4, rue Jacques Monod - 91893 ORSAY Cedex (France)
Unité de recherche INRIA Lorraine : LORIA, Technopôle de Nancy-Brabois - Campus scientifique
615, rue du Jardin Botanique - BP 101 - 54602 Villers-lès-Nancy Cedex (France)
Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu - 35042 Rennes Cedex (France)
Unité de recherche INRIA Rhône-Alpes : 655, avenue de l’Europe - 38334 Montbonnot Saint-Ismier (France)
Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles - BP 93 - 06902 Sophia Antipolis Cedex (France)

Éditeur
INRIA - Domaine de Voluceau - Rocquencourt, BP 105 - 78153 Le Chesnay Cedex (France)
http://www.inria.fr

ISSN 0249-6399

