1

Expressive Power of Safe HORS
Examined Through Decomposition ofHigher Order Programs to Garbage Free 1st Order Form

Kazuhiro Inaba
Joint work with Sebastian Manethat Shonan Meeting on
Automated Techniques for Higher-Order Program Verification2011

2Background• HORS (Higher Order Recursion Scheme)is very powerful and expressive.

• n-EXPTIME hard problems!

3Computational Complexity w.r.t.
Grammar Size and Data Size
• MSO on words/trees:– Emptiness checking is non elementary (HYPEREXP)
for the size of the formula.
– The class of languages it represents is regular.
• O(n) time, O(1) space membership wrt the word length“MSO on words is a verrrrrrrrry concise
representation for relatively simple languages.”4

How about HORS?
• HORS:– Emptiness, Model Checking, Containment byRegular Languages, ... are n-EXPTIME hard.
– What is known about the languages it describes?
• The class of languages it represents is ????.
• ???? time, ???? space membership wrt the word length.

5[Greibach 70]

Today’s talk verifies the statement(even for wider class of languages).
[Gr70] S. A. Greibach, “Full AFLs and Nested Iterated Substitution”, Inf. Ctrl. 16

6Our Approach
Intermediate Data SizeOutputHORS
If they are at most of size M at any point, O(M) space & O(2M) time.

7

Outline of This Talkλ• Target Language

λ λ– Higher-order Tree Transducers• 1st-order Decomposition

τ1

τ2

τn

τ'del
τ'1
– Derived consequences– Sketch of the constructions

τ'2

τ'n– Sketch of the construction• Garbage Free Form0s1

s2 Sn-1t8

HTT [Engelfriet&Vogler 88]
Higher-order “single-input” “safe” tree transducer
Mult :: Tree  Tree

Mult(Pair(x1,x2))

 Iter(x1)(Add(x2))(Z)

Iter :: Tree  (Tree  Tree)  Tree  Tree

Iter(S(x))(f)(y)Iter(Z)(f)(y) Iter(x)(f)(f(y))
 yAdd :: Tree  Tree  Tree

Add(S(x))(y)Add(Z)(y) Add(x)(S(y))
 y

9HTT
• Set of mutually recursive functions– Defined in terms of induction on a single input tree
• Input trees are always consumed, not newly constructed• Output trees are always created, but not destructed– Rest of the parameters are ordered by the order• Multiple parameters of the same order is ok but in uncurried form
Inductive Input Param Order-1 Param(s)Iter :: Tree

(Tree  Tree)

Iter(S(x))(f)(y)Iter(Z)(f)(y)Order-0 Param(s) Result

Tree

Tree

 Iter(x)(f)(f(y))
 y10HTT
Nondeterminism (∥and ⊥)Subseq :: Tree  Tree

Subseq(Cons(x,xs))  Cons(x, Subseq(xs))∥ Subseq(xs)Subseq(Nil) Nil
Subseq(Other)  ⊥In this talk, evaluation strategy is unrestricted (= call-by-name).
But call-by-value can also be dealt with.11HTT• Notation: n-HTT– is the class of TreeTree functions
representable by HTTs of order ≦ n.
– {Subseq} is 0-HTT, {Mult, Iter, Add}∈2-HTT
Subseq :: Tree  Tree
Mult :: Tree  Tree
Iter :: Tree  (Tree  Tree)  Tree  Tree
Add :: Tree  Tree  Tree

12

Order-n to Order-1
THEOREM [EV88] [EV86](n-HTT) ⊆ (1-HTT)nn-th order tree transducer is representable
by a n-fold composition of 1st-order treetransducers. (“= or ⊊ ?” is left open, as far as I know.)[EV86] J. Engelfriet & H. Vogler, “Pushdown Machines for Macro Tree Transducers”, TCS 42[EV88] ─, “High Level Tree Transducers and Iterated Pushdown Tree Transducers”, Acta Inf. 26

13

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

F(Z)(y)  S(S(y))

F :: Tree  Tree

F(Z)  S(S(Y))

Represent 1st-order application symbolically, too.
…  F(x)(Z)…  @(F(x), Z)

14

Proof: n-HTT = 1-HTT ∘ (n-1)-HTTRepresent 1st-order things symbolically.
F :: Tree  Tree

F(Z)  S(S(Y))…  @(F(x), Z)

Then a 1-HTT performs the actual “application”.
Eval(@(f, b))(y)  Eval(f, Eval(b)(y))
Eval(Y)(y) yEval(S(x))(y) S(Eval(x)(y))
Eval(Z)(y)
 Z

15

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

@@
YIter(Z)(Add(S(Z)))

ZYS

Add(S(Z))
Y
Add(S(Z))

Y@Y@YExample

16

Eval(@(f, b))(y)  Eval(f, Eval(b)(y))
Eval(Y)(y) yEval(S(x))(y) S(Eval(x)(y))
Eval(Z)(y) Z
Eval( @ ,y= Z )S@
Z

Eval( @ , y=⊥)
@@Y
@Y

Y

Eval( @ , y=Z

Y

Z@YS)

Y

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

@Y

Y
S

Y

@YS
YY

YSY

17

Why That Easy
• Relies on the ordered-by-order condition.
– No variable renaming is required! [Blum&Ong 09]
Eval( Y ,y=Eval( @ ,y= Z )@YYSY[BO09] W. Blum and C.-H. L. Ong, “The Safe Lambda Calculus”, LMCS 5

18Now, Decomposed.
1-HTT nn-HTTλ λ λ

τ1

τ2τn

19

Next, Make Intermediate Trees Small.
1-HTT nτ1s

τ2

τ'delτnt

τ'1s0s

τ'2s1

τ'ns2 Sn-1t

20

THEOREM [I. & Maneth 08] [I. 09](+ improvement)∀τ1, ..., τn∈1-HTT, ∃τ’del∈0-LHTT, τ’1, ..., τ’n ∈1-HTT,for any(τn ∘ ... ∘ τ1)(s) ∋ t,there exist τ’del(s)∋s0, τ’i(si)∋si+1, |si|≦|si+1|, sn=t.
τ1sτ2

τ'delτnt

τ'1s0s

τ'2s1

τ'ns2 Sn-1t|s| = number of nodes[IM08] K. Inaba & S. Maneth, “The complexity of tree transducer output languages”, FSTTCS[Inaba09] K. Inaba, “Complexity and Expressiveness of Models of XML Transformations”, Dissertation

21Consequences : Range Membership
Membership problem forthe class Range(1-HTT n) of languages is・ in DLINSPACE
・ in NPThat is, given (τn ∘ ... ∘ τ1) and t, we can determine“∃s. (τn ∘ ... ∘ τ1)(s)∋t”

in O( f(|τ1|+...+|τn|)・|t| ) space andin O( g(|τ1|+...+|τn|)・ poly(|t|) ) nondeterministic time.

22Consequences : Range Membership
Membership problem forthe class Range(1-HTT n) of languages is・ in DLINSPACE
・ in NP
PROOF
Guess (in NP) or
exhaustively try (in DLINSPACE)
all the intermediate trees: s0 ... sn-1.

τ'delsτ'1s0Then check Range(τ’del)∋s0 and τ’i(si)∋si+1,both turn out to be feasible in DLINSPACE ∩ NP.

τ'2s1

τ'ns2 Sn-1t23Consequences : Range Membership
Membership problem forthe class Range(1-HTT n) of languages is・ in DLINSPACE・ in NPRE

COROLLARY

Higher-order safe recursion scheme, also
known as OI-hierarchy, HO-PDA language,
Maslov hierarchy, generalized indexedlanguage, etc., is Context-Sensitive.

CSL (NLINSPACE)
order-nIndexed (order-2)
CFL (order-1)
Regular (order-0)24Consequences : Linear-Size Inverse
For all τn∘...∘τ1∈1-HTTn , t∈Range(τn∘...∘τ1)
there exists s such thatf(s)∋t and |s| < h(|τn∘...∘τ1|)・|t|COROLLARY (by our constructive proof)

Right inverse of 1-HTTn is computable in DLINSPACE∩NP.

25

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

τn-1

τnt

τn-1

τ’nt

26

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

τnt

τn-1 τ’del τ’nt

27

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τnt

τ’n-1+del

τ’nt

28

τ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

29

Key Part
Separate the “deleting” transformation

τn==τ’del; τ’n

30

Key PartSlogan: Work on every node
(τ’n must generate at least one node for each input node)τ’del; τ’n31Work on Every Node ⇒ Visit All Nodes
Deleting HTTs
G(Z)(y1)  Z ∥ y1
F(S(x1,x2))  F(x1)n∥ F(x2)∥ G(x1)(F(x2))τmay not recurse down to a subtree.

32

Work on Every Node ⇒ Visit All Nodes
F(S(x1,x2))  G(x1)(F(x2))

Nondeterministically delete every subtree!

τn

τ’del

Del(S(x1,x2)) S12(Del(x1),Del(x2)) ∥ S1_(Del(x1))∥ S_2(Del(x2)) ∥ S__()At least one choiceof nodeterminism“deletes correctly”.

F(S12(x1,x2))
F(S1_(x1))
F(S_2(x2))
F(S__())

 G(x1)(F(x2))
 G(x1)(⊥)
 ⊥ ⊥τ’n33Work on Every Node ⇒ Work on Leaf
Erasing HTTs
F(S(x))  G(x)(Z)
G(Z)(y)  yτnmay be idle at leaves.

34Work on Every Node ⇒ Work on Leaf
Erasing HTTs
F(S(x))  G(x)(Z)
G(Z)(y)  y

Inline Expansionτn

F(S(Z))  Z

τ’n

35

Work on Every Node⇒ Work on Monadic Nodes
Skipping HTTs
F(S(x))(y1,y2,y3)  F(x)(y2,y3,y1)
F(Z)(y1,y2,y3)
 Done(y1,y2,y3)τnare good at juggling.

36

Work on Every Node⇒ Work on Monadic Nodes
Skipping HTTs
F(S(x))(y1,y2,y3)  F(x)(y2,y3,y1)
F(Z)(y1,y2,y3)
 Done(y1,y2,y3)τnNondeterministic deletion again.
Remember how argugments would’ve been shuffled.

F(Z123)(y1,y2,y3)  Done(y1,y2,y3)
F(Z231)(y1,y2,y3)  Done(y2,y3,y1)
F(Z312)(y1,y2,y3)  Done(y3,y1,y2)

τ’n

37

Simple Arithmetic• Input size = #leaf + #monadic + #others– For each leaf on the input, generate ≧1 node.
– For each monadic node, generate ≧1 node.
– Thus, #leaf + #monadic ≦ Output size.

• For any tree, #others < #leaf ≦ Output size.
• Add: #leaf + #monadic + #others ≦ Output size*2• So, Input size < Output Size * 2

38Work on Nodes with Rank-2,3,...
• Input size < Output Size * 2
Fr(Bin(x1,x2))(y)  Fr(x1)(Fr(x2)(y))Fr(A)(y)  A(y)Fr(B)(y)  B(y)This bound is sufficient for deriving the results,
but we can improve this to Input size ≦ Output Size,by deterministic deletion of leaves + inline expansion.39Done!

τ’del; τ’n40Summary• Order-n HTT  (Order-1 HTT)n• Garbage Free Formλλ λ– L( Safe-HORS ) is context-sensitive.

• Future Direction– Extend it to Unsafe HTT– Or, use it for proving
safe ⊊ unsafe

τ'dels0

τ1

τ2

τn

τ'1

τ'2

τ'n

s1

s2 Sn-1t