Higher-Order Tree Transducers
andTheir Expressive Power
Kazuhiro Inaba
at Dagstuhl Seminar, May 2013

Regular
Tree Grammar••••

input tree

Δ = {a, b, c, ...}
N = {F, G, H, ..., S, T, ...}
R = set of rules
S∈N

SaTT
Sb
TcSS

•
•
•
•
•

a
c

b

b

Each nonterminal generates(a set of) trees.
F:O(Top-Down)
Tree Transducer

c

a

b

Σ = {s, t, u, ...}
Δ = {a, b, c, ...}
N = {F, G, H, ..., S, T, ...}
R = set of rules
S∈N

S (s x1 x2)  a (T x1) (T x2)
S (t)b
T (s x1 x2)  c (S x1) (S x2)
Each nonterminal takes aninput tree and generates(a set of) trees.
F:IO

Regular
Tree Grammar

input tree

tree
parameter

Context-Free
Tree Grammar(Top-Down)
Tree Transducer
treeparameter

input tree

Macro
Tree TransducerSTdd
T y1 y2  T (b y1) (c y2)
T y1 y2  a y1 y2S (s x1)
 T x1 d d
T (s x1) y1 y2  T x1 (b y1) (c y2)
T z
y1 y2  a y1 y2

Each nonterminal takes
parameter trees andgenerates (a set of) trees.
F : Ok  O

Each nonterminal takes aninput tree and parametertrees, and generates trees.
F : I Ok O

Regular
Tree Grammar

input tree

tree
parameter

Context-Free
Tree Grammar

treeparameter

input tree

Macro
Tree Transducer
higher-orderparameter

higher-orderparameter

Higher-Order
Tree Grammar(Top-Down)
Tree Transducer

input tree

Higher-Order
Tree Transducer

multiple
input trees

HMTT

Example of a higher-order transducer
pairMult : I  OMult (pair x1 x2)  Iter x1 (Add x2) z

S

S

S

S

S

S

Z

S

Iter : I  (O  O)  O  O

Iter (s x1) f y  Iter x1 f (f y)Iter zfyyZS

Add : I  O  O

S

Add (s x1) y  Add x1 (s y)
Add z
yy

S
S
Z

(Examples of) problems we should be interested in
Membership
Given a higher-order grammar G and a tree t,
decide whether t ∈ [G] or not.
Type Checking
Given a higher-order tree transducer f and regular tree
languages S and T, decide whether f(S)⊆T or not.
Model Checking
Given a deterministic higher-order grammar G
representing a (possibly infinite) single tree t, and a
MSO sentence φ, decide whether t satisfies φ.

Equi-Expressivity
What is the automata-like of the models?
Can they be “decomposed” to simpler models?

Agenda• Introduction• Two notions of “higher-order” types.
• Review of known results.
• Context-sensitiveness of “safe” higher-orderlanguages [I. and Maneth, 2008]

Two Notions of “Higher Order” Types (1)D0 = O“Trees” are order-0.

Di+1 = { Dik  Di | k ∈ N }Functions from order-i objects toorder-i objects are order-(i+1).

order(t) = i

if t ∈ Di• “Derived Types”– OI-Hierarchy [Damm 82]– High-Level Tree Tranducer [Engelfriet & Vogler 88]

Two Notions of “Higher Order” Types (2)• Recently actively studied in context of program
verification [Ong 06, ...] or linguistics[Kobele&Salvati 13, ...].

D ::= O | DD“Trees” are order-0, and ...

order(O) = 0
order(t1t2) =max(order(t1)+1, order(t2))

The Difference• Functions parameters of “Derived Types” havedecreasing orderDn  (Dn-1  (Dn-2  ... (O  O) ...))

which does not contain, e.g.,
λx. λf. λy. f x : O  (OO)  O  O
It implies:
Safety [Knapik&Niwinski&Urzyczyn 01, 02]
No order-k subterm can contain order <k free variables.

Safety
Safety [KNU 01, 02]
No order-k subterm can contain order <k free variables.
[KNU 01, 02] [Blum&Ong 09]
In safe grammars/λ-calculus, you don’t need to careabout variable capturing while substitution.
!!

Unsafe example: λy. ((λx. λy. a x y) y) λy. ( (λy. a x y)[x/y] ) λy. ( λy. a y y )this is wrong

“Safe” :: Di+1 = {Dik  Di}
Grammars• MSO model checking isdecidable. [KNU 01, 02]• Hierarchy is strict. [Damm 82]• Equivalent to “iterated
pushdown automata” [Da 82](= (stack of)* stacks)• Context-sensitive.
[Maneth 02][I.&Maneth 08]

Transducers [EV88]• n-DHTT = (1-DHTT) n• n-NHTT ⊆ (1-NHTT) n“Unsafe” :: DD• MSO model checking isdecidable. [Ong 06, Kobayashi 09]• Hierarchy is strict.
[Kartzow&Parys 12]• Equivalent to “collapsible
pushdown automata”[Hague&Murawski&Ong&Serre 08]• ????

• ????

“Safe” :: Di+1 = {Dik  Di}
Grammars• MSO model checking isdecidable. [KNU 01, 02]• Hierarchy is strict. [Damm 82]• Equivalent to “iterated
pushdown automata” [Da 82](= (stack of)* stacks)• Context-sensitive.
[Maneth 02][I.&Maneth 08]

Transducers [EV88]• n-DHTT = (1-DHTT) n• n-NHTT ⊆ (1-NHTT) n“Unsafe” :: DD• MSO model checking isdecidable. [Ong 06, Kobayashi 09]• Hierarchy is strict.
[Kartzow&Parys 12]• Equivalent to “collapsible
pushdown automata”[Hague&Murawski&Ong&Serre 08]• ????

• ????

“Safe” :: Di+1 = {Dik  Di}
Grammars• MSO model checking isdecidable. [KNU 01, 02]• Hierarchy is strict. [Damm 82]• Equivalent to “iterated
pushdown automata” [Da 82](= (stack of)* stacks)• Context-sensitive.
[Maneth 02][I.&Maneth 08]

Transducers [EV88]• n-DHTT = (1-DHTT) n• n-NHTT ⊆ (1-NHTT) n“Unsafe” :: DD• MSO model checking isdecidable. [Ong 06, Kobayashi 09]• Hierarchy is strict.
[Kartzow&Parys 12]• Equivalent to “collapsible
pushdown automata”[Hague&Murawski&Ong&Serre 08]• ????

• ????

“Collapsible” Pushdown Automata[Hague at al. 08]• Order-n collapsible pushdown store is– (stack of)n symbols– with each symbol associated with “links”• Push1• Dupk• Popk• Collapse: pushes a symbol and link to the top.
: duplicates the top order-k stack.
: pops the top order-k stack.
: moves the top to the pointee of the top link.

“Safe” :: Di+1 = {Dik  Di}
Grammars• MSO model checking isdecidable. [KNU 01, 02]• Hierarchy is strict. [Damm 82]• Equivalent to “iterated
pushdown automata” [Da 82](= (stack of)* stacks)• Context-sensitive.
[Maneth 02][I.&Maneth 08]

Transducers [EV88]• n-DHTT = (1-DHTT) n• n-NHTT ⊆ (1-NHTT) n“Unsafe” :: DD• MSO model checking isdecidable. [Ong 06, Kobayashi 09]• Hierarchy is strict.
[Kartzow&Parys 12]• Equivalent to “collapsible
pushdown automata”[Hague&Murawski&Ong&Serre 08]• ????

2-unsafe = 2-safe [Aehlig&Miranda&Ong 05]
2-unsafe-det ⊄ n-safe-det [Parys 11, 12]• ????

“Safe” :: Di+1 = {Dik  Di}
Grammars• MSO model checking isdecidable. [KNU 01, 02]• Hierarchy is strict. [Damm 82]• Equivalent to “iterated
pushdown automata” [Da 82](= (stack of)* stacks)• Context-sensitive.
[I.&Maneth 08]

Transducers [EV88]• n-DHTT = (1-DHTT) n• n-NHTT ⊆ (1-NHTT) n“Unsafe” :: DD• MSO model checking isdecidable. [Ong 06, Kobayashi 09]• Hierarchy is strict.
[Kartzow&Parys 12]• Equivalent to “collapsible
pushdown automata”[Hague&Murawski&Ong&Serre 08]• ????

• ????

1st order Decomposition of Safe HTT[Engelfrier&Vogler 86,88] [Caucal 02]

Safe-n-DHTT = (Safe-1-DHTT)n
Safe-n-NHTT ⊆ (Safe-1-NHTT)nn-th order tree transducer is representable by a nfold composition of 1st-order tree transducers.
Note: Higher order grammars can be simulated by Out(HTT).

Proof: n-HTT = (n-1)-HTT ; 1-HTT
Idea:
Represent 1st-order term TreeTree by a Tree.
F :: Tree  TreeTree

F z y  s (s y)F :: Tree  TreeF z  s (s y)Represent 1st-order application symbolically, too.
…  F x z

…  @ (F x) z

Proof: n-HTT = (n-1)-HTT ; 1-HTT
Represent 1st-order things symbolically.
F :: Tree  TreeF z  s (s y)…  @ (F x) z

Then a 1-HTT performs the actual “application”.
Eval (@ f b) y
Eval y yEval (s x) y
Eval z y Eval f (Eval b y)
 y
 s (Eval x y) zMult (pair x1 x2)  @ (Iter x1 (Add x2)) z
Iter (s x) f
 @ (Iter x f) (@ f y)Iter z f
 y
Add (s x)
 @ (Add x) (s y)
Add z
 y
@

Mult (Pair (s z) (s z))@

Iter (s z) (Add (s z))

@

Z

Z

@
@

Z

@
@

y

@
@
y

Iter z (Add (s z))

ZyS

Add (s z)y
Add (s z)

y

@

y

@
y

ExampleEval (@ f b) y
Eval y yEval (s x) y
Eval z y Eval f (Eval b y)
 y
 s (Eval x y) z
Eval( @ ,y= Z )S@
Z

Eval( @ , y=⊥)
@
@

y
@
y

y

Eval( @ , y=

Z

y

Z

@
y

S

)

y

Eval( y ,y=Eval( @ ,y= Z )

@

y
y

S

y

@

y
S
y

y

y
S
y

If it’s unsafe...
SFa
F y  b (H (G y) c)
G x y  ...
H f y  d (f e) y

@
b

@

F

a

a

H (G y) c

@

S
F
G
Hf

@Fa
 b (@ (H (@ G y)) c) ..
 d (@ f e) yab@d ((G y) e) yc

Consequences of First-Order
Decomposition[EV88]

f-1(T) ∈ REG

if

f∈Safe-HTT and T∈REG• Proof: because MTT (1-HTT) has the property.
• This gives decidable “type checking”.
– f(S)⊆T  f-1(T)⊆S : inclusion of REG is decidable.

Consequences of First-Order
Decomposition[I. and Maneth 08]

f(T) ∈ DCS

if

f∈Safe-HTT and T∈REG• DCS = Deterministic-Context-Sensitive= DLINSPACE membership• Proof: in a next few slides...
• Corollary : Safe Higher-order languages (aka. OIHierarchy) are context-sensitive.

Proof: Out(1-HTT n) ∈DLINSPACEThe Key Idea
n-HTT
λ λ λ
1-HTT nτ1sτ2

“garbage free” 1-HTT n
τn

τ'del

transform

t

τ'1

s0

s

τ'2

s1

τ'n

s2 Sn-1tHow to Construct the “Garbage-Free” Form
Make each 1-HTT “productive”

τn-1

τn

t

τn-1

τ’n

t

How to Construct the “Garbage-Free” Form
Make each 1-HTT “productive”
by separating its “deleting” partτn = τ’del τ’n
τn-1

τn

t

τn-1 τ’del τ’ntHow to Construct the “Garbage-Free” Form
Make each 1-HTT “productive”
by separating its “deleting” part,and fuse the deleter to the left [En75,77][EnVo85][EnMa02]

τn-1

τn

t

τ’n-1+del

τ’n

t

τ1

τ2

τ1

τ2

τ3 τ’4d τ’4

τ1

τ2

τ34d

τ’4

τ1

τ2

τ’34d

τ’3

τ’4

τ1

τ234d

τ’3

τ’4

Fuse

τ1 τ’234d
τ1234d

τ’2
τ’2

τ’3
τ’3

τ’4
τ’4

τ’1234d

τ’1

τ’2

τ’3

τ’4

Repeat

Split
Fuse

Split
Fuse
Split

Split

τ3

τ4

Summary: Out(Safe-n-HTT) is context sensitive.
1.

λDecompose n-HTT to (1-HTT)n.

λ λ

2. Split each 1-HTT to (LT; 1-HTT).
= deleting and productive part

3. Fuse deleting part ahead.

τ1

τ2

τn

1-HTT ; LT ⊆ 1-HTT
τ'del

τ'1
τ'2
4. Now all intermediate
trees must be small.
s0
s1 s2 S
Try them all in DLINSPACE.

τ'n

n-1

t

“Safe” :: Di+1 = {Dik  Di}
Grammars• MSO model checking isdecidable. [KNU 01, 02]• Hierarchy is strict. [Damm 82]• Equivalent to “iterated
pushdown automata” [Da 82]“Unsafe” :: DD• MSO model checking isdecidable. [Ong 06, Kobayashi 09]• Hierarchy is strict. [Kartzow&Parys

Open Questions(= (stack of)* stacks)

12]• Equivalent to “collapsible
pushdown automata”[Hague&Murawski&Ong&Serre 08][Maneth 02][I.&Maneth 08]• Is unsafe higher-orderlanguages context-sensitive?

Transducers [EV88]• n-DHTT = (1-DHTT) n• n-NHTT ⊆ (1-NHTT) n• Does unsafe higher-ordertransducers have first-orderdecompositions?

• Context-sensitive.

Idea: Stack-TT• 1-HTT has difficulty in implementing captureavoiding substitution.
• How about extending them with a stack
POP m values• f (a x1 ... xn) y1 ... ym ys  RHS
where RHS ::= d RHS ... RHS| yi| f xi RHS ... RHS ys
PUSH

Unsafe substitution 
De-Bruijn index + Stack-TT(λx. λy. (A x y)) B C

Eval

A

s

(λ. λ. (A 0 1)) B C

B

C

s

z

@
@
A
s

C
B

s
z

PUSH!
Eval (@ f a) ys
 Eval f (Eval a ys) ys
Eval (s x) y ys  Eval x ys
POP!
Eval zy ys  yEven if it’s unsafe...
SFa
F y  b (H (G y) c)
G x y  ...
H f y  d (f e) y

S
F
G
Hf

@Fa
 b (@ (H (@ G 2)) c) ..
 d (@ (k1d2 f) e) 0
Eval (k1d2 x) y1 y2 y3 ys= Eval x y1 ys

S
F
G
Hf

@Fa
 b (@ (H (@ G y)) c) ..
 d (@ f e) y

@
a

b
@

d ((G y) e) yc

Pros & Cons
• Good:• Good:Found an error in
the proof during
discussion in theseminar... X(

Theorem: Unsafe-n-HTT ⊆ (Stack-TT)nTheorem: (Stack-TT ; LT) ⊆ Stack-TT• Bad: it is hard to make it garbage-free.
– There can be a sequence of significant stack
operations not generating output.

• Bad: it may be overly powerful.
Theorem: Stack-TT ⊄ Unsafe-n-HTT

Proof: inverse of stack-TT does not preserve
regularity, while unsafe-n-HTT does.

Summary• “Safe” and “unsafe” HTT are different.
• Can we transfer results in “safe” case to “unsafe”?
– Can we decompose an unsafe-HTT to 1st order machines?
– Can we show context-sensitivity of the output language?

• See http://www.kmonos.net/pub/tmp/smtt.pdf for
the technical development.