Higher-Order Multi-Parameter Tree Transducers
and Recursion Schemes for Program Verification
Naoki Kobayashi

Naoshi Tabuchi

Hiroshi Unno

Tohoku University
koba@ecei.tohoku.ac.jp

Tohoku University
tabee@kb.ecei.tohoku.ac.jp

Tohoku University
uhiro@kb.ecei.tohoku.ac.jp

Abstract
We introduce higher-order, multi-parameter, tree transducers(HMTTs, for short), which are kinds of higher-order tree transducers that take input trees and output a (possibly infinite) tree.
We study the problem of checking whether the tree generated bya given HMTT conforms to a given output specification, provided
that the input trees conform to input specifications (where both input/output specifications are regular tree languages). HMTTs subsume higher-order recursion schemes and ordinary tree transducers, so that their verification has a number of potential applications
to verification of functional programs using recursive data structures, including resource usage verification, string analysis, and exact type-checking of XML-processing programs.
We propose a sound but incomplete verification algorithm for
the HMTT verification problem: the algorithm reduces the verification problem to a model-checking problem for higher-order recursion schemes extended with finite data domains, and then uses (anextension of) Kobayashi’s algorithm for model-checking recursion
schemes. While the algorithm is incomplete (indeed, as we show inthe paper, the verification problem is undecidable in general), it issound and complete for a subclass of HMTTs called linear HMTTs.
We have applied our HMTT verification algorithm to various program verification problems and obtained promising results.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meaningof Programs]: Specifying and Verifying and Reasoning about Programs
General Terms Languages, Verification

1.

Introduction

Kobayashi [20] has recently proposed a verification method forhigher-order functional programs based on Ong’s decidability result on model-checking recursion schemes [32]. A higher-order recursion scheme (recursion scheme, for short) is a grammar for generating a (possibly infinite) tree. It is an extension of regular treegrammars, where non-terminal symbols can take trees and higherorder functions on trees as parameters. For example, the following grammar G0 is an order-1 recursion scheme, where the non-© ACM, 2010. This is the author’s version of the work. It is posted here by permissionof ACM for your personal use. Not for redistribution. The definitive version was
published in the Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL 2010)

a
c

a
b
c

a
a

b
...

...

...

Figure 1. The tree generated by G0 .
terminal F takes a tree as an argument.
S→Fc

F x → a x (F (b x))

Here, each non-terminal has exactly one rewrite rule. By infinitary
rewriting of the start symbol S:
S −→ F c −→ a c (F (b c)) −→ · · · ,we obtain the infinite tree shown in Figure 1. Ong [32] has shownthat modal mu-calculus model-checking of recursion schemes(“Given a recursion scheme G and a modal mu-calculus formula φ,does the tree generated by G satisfy φ?”) is n-EXPTIME-complete(where n is the order of the recursion scheme G). The idea of
Kobayashi’s verification method [20] is to translate a functional
program into a recursion scheme that generates a tree whose paths
represent all the possible event sequences of the program, so that
temporal properties of the functional program can be verified bymodel-checking the recursion scheme. For example, consider thefollowing program that accesses a file (where * denotes a randomboolean value):let x = open_in "foo" in
let rec f() = if * then close(x) else read(x); f()in f()
It can be translated into the following recursion scheme G1 :S→FeF k → br (c k) (r (F k))

Here, r, c, br and e denote a read operation, a close operation, a non-deterministic branch, and program termination respectively. The recursion scheme generates the tree shown in Figure 2,
which represents all the possible event (i.e. read, write, branch,and termination) sequences of the program. Kobayashi [20] applied the verification method to resource usage verification [14](the problem of checking whether a program accesses resources
such as files in a valid manner), and showed that it is sound andcomplete for the simply-typed λ-calculus extended with recursion, resource creation/access primitives, and booleans. The completeness follows intuitively because recursion schemes are essentially terms of the simply-typed λ-calculus with recursion and

br
c

r

e

br

order functions can be used. The function merge above is expressedas the following HMTT T2 :

c

r

e

...

Figure 2. The tree generated by G1 .

tree constructors, so that they are already almost as expressive
as the source language (of the simply-typed λ-calculus with resources), and no information is lost by the translation. Although themodel-checking of recursion schemes has extremely high worstcase time complexity (n-EXPTIME-complete for the full modal
mu-calculus), Kobayashi [18] constructed a model-checker for recursion schemes, and showed that it works well for realistic inputs.
Thus, the verification method based on recursion schemes seems to
be one of the promising methods for higher-order program verification.
The main limitation of recursion schemes from a programming language point of view is that there are tree constructors but
not destructors. Because of this limitation, one cannot naturally
model programs operating over infinite data domains such as integers, lists, and trees.1 For example, consider the following function
merge:
let rec merge x y =case x of [] => copy y| a::x’ => merge_a x’ y
| b::y’ => merge_b x’ yand merge_a x y =case y of [] => a::(copy x)| a::y’ => a::a::(merge x y’)| b::y’ => a::(merge_b y’ x)
and merge_b x y =case y of [] => b::(copy x)| a::y’ => b::(merge_a y’ x)| b::y’ => b::b::(merge x y’)
and copy x =case x of [] => []| a::x’ => a::(copy x’)| b::y’ => b::(copy y’)
The function merge merges two lists consisting of a and b. It
recursively destructs x and y, which cannot be expressed by arecursion scheme. Functions operating over recursive data structures are ubiquitous in functional programming, so that not being able to handle them is a great limitation for the approach ofmodel-checking functional programs by modeling them as recursion schemes.
To relax the limitation above, we introduce an extension of recursion schemes called higher-order, multi-parameter tree transducers (HMTTs, for short). As in other (top-down) tree transducers [7, 8], we classify trees into input and output trees: only constructors can be applied to output trees, and only destructors can beapplied to input trees. Unlike in ordinary tree transducers, however,each function symbol (non-terminal) can take multiple input trees
as arguments (as in the function merge above). Furthermore, asin recursion schemes (and high-level tree transducers [8]), higher1 It is possible to encode trees as functions instead of using primitive tree

constructors. The tree operations realized in this way is however limited, as
recursion schemes must be simply-typed.

Merge x y ->case(x,Copy y, x’.Merge_a x’ y, x’.Merge_b x’ y).
Merge_a x y ->case(y,a(Copy x),y’.a(a(Merge x y’)),y’.a(Merge_b y’ x)).
...
Here, strings are expressed as linear trees (consisting of only terminal symbols of arity 1 or 0). case(e, xe1 .e1 , . . . , x
en .en ) matches atree e with a pattern ai et, and reduces to [et/exi ]ei . HMTTs subsume both higher-order recursion schemes and various kinds oftree transducers (such as macro tree transducers and high-level treetransducers [7, 8]).
For HMTTs, we consider the following verification problem(T , M1 , . . . , Mk , M): “Given an HMTT T that takes k (possibly
infinite) input trees, and Büchi tree automata with a trivial acceptance condition (where all the states are final) M1 , . . . , Mk , M,does T always output a (possibly infinite) tree accepted by M,
given trees accepted by M1 , . . . , Mk as inputs?” For example, let
M be a tree automaton that accepts linear trees labeled by elementsof a∗ b∗ e + aω + a∗ bω (where a, b and e are terminal symbols
of arity 1, 1, and 0 respectively). Then, the verification problem(T , M, M, M) is the problem of deciding whether T produces alinear tree labeled by an element of a∗ b∗ e + aω + a∗ bω (thus, a tree
like b(a(e)) is excluded), given two input trees labeled by elementsof a∗ b∗ e + aω + a∗ bω .
In the present paper, we give a sound but incomplete algorithm for the HMTT verification problem. The algorithm consistsof two phases. First, we transform the HMTT verification problem into a model-checking problem for recursion schemes extended
with constructors and destructors for finite data domains (such as
booleans). We then solve the model-checking problem for the recursion scheme by using an extension of Kobayashi’s model checking algorithm for recursion schemes [18]. The idea of the first phaseis to approximate an input tree by an automaton state. For example,
recall the HMTT T2 (corresponding to the merge function). The
automaton M has two states q0 and q1 , with transition δ(q0 , a) =q0 , δ(q0 , b) = q1 , δ(q0 , e) = ϵ, δ(q1 , b) = q1 , δ(q1 , e) = ϵ. Thus,
the output of T2 applied to linear trees in L(M) is approximated by
the following recursion scheme with finite data domains {q0 , q1 }:S -> Merge q0 q0.
Merge x y ->case(x,br3 (Copy y) (Merge_a q0 y) (Merge_b q1 y),
br (Copy y) (Merge_b q1 y)).
Merge_a x y ->case(y,br3 (a(Copy x)) (a(a(Merge x q0)))(a(Merge_b q1 x))
br (a(Copy x)) (a(Merge_b q1 x))).
...
Here, the non-terminal Merge now takes elements of{q0 , q1 } as arguments instead of trees, and the case statement case(e, e0 , e1 ) reduces to e0 if the value of e0 is
q0 , and reduces to e1 otherwise. The three branches ofbr3 (Copy y) (Merge_a q0 y) (Merge_b q1 y)forthe case x = q0 simulates the cases where the input tree x is of
the form e, a t1 , and b t2 respectively. The tree generated by therecursion scheme (with finite data domains) constructed in thismanner contains all the possible outputs of the HMTT (for valid

inputs). Thus, if the recursion scheme generates only valid trees,
so does the HMTT.
As mentioned above, our verification algorithm is sound but
incomplete: it does not accept an invalid HMTT, but may rejecta valid HMTT. As we show in the paper, the HMTT verification
problem is undecidable in general, so that we cannot hope to finda complete algorithm. We show, however, that the proposed algorithm is complete for a subclass of HMTTs called linear HMTTs(with certain additional assumptions). Intuitively, an HMTT is linear if it traverses each input tree at most once. (For example, themerge function above is linear since it traverses x and y just once.)
Note that, even for the decidable class of linear HMTTs, our verification problem subsumes the model checking problem for recursion schemes (where properties are restricted to those describedby Büchi tree automata with a trivial acceptance condition). Linear HMTTs also subsume (deterministic and total) high-level treetransducers [8] in the sense that any high-level tree transducer canbe transformed into a linear HMTT by using a standard programtransformation technique (see [23]).
There are many potential applications of our HMTT verification method. As HMTTs subsume recursion schemes and highlevel tree transducers, immediate applications include (i) the resource usage verification considered by Kobayashi [20], and (ii)exact type-checking of XML-processing programs [25, 27, 28, 34].
For (i), while Kobayashi [18, 20] considered closed programs, we
can now deal with programs that take recursive data structures asarguments. For (ii), unlike previous approaches to using macro or
high-level tree transducers, we can verify programs that take multiple XML documents as inputs. Furthermore, thanks to the efficientmodel-checking algorithm for recursion schemes, our HMTT verification algorithm is reasonably fast even for higher-order cases;on the other hand, previous approaches based on transducers do
not seem to scale well for higher-order cases [34]. Other applications include: (iii) string analysis [3, 29], and (iv) verification ofprograms that use other recursive data types (e.g. the list-ness ofthe output of the function “flatten” converting nested lists into flat
lists). For (iii), the goal is to check that a program always generates
a valid string as output. Web applications often generate HTMLfiles, and it is important to check that there is no cross-site scripting vulnerabilities and also that the output conforms to the HTML
format [29]. Previous approaches [3, 29] use a kind of control flow
analysis to approximate the output string as a regular or contextfree language, and then compare it with the output specification.
By using HMTT, we can more precisely approximate the output
string (and indeed, no approximation is required in certain cases).
The rest of this paper is structured as follows. Section 2 introduces HMTTs and defines their verification problems. Section 3 introduces higher-order recursion schemes extended with finite data
domains. Section 4 gives a transformation of HMTT verification
problems into model-checking problems for recursion schemeswith finite data domains. Section 5 extends Kobayashi’s type-based
method for model-checking recursion schemes [18, 20], to deal
with finite data domains. Section 6 discusses the complexity of our
HMTT verification algorithm. Section 7 discusses applications ofour verification method, and Section 8 reports preliminary experiments. Section 9 discusses related work, and Section 10 concludes
the paper. A longer version of this paper [23], containing proofs
and more details on the experiments, is available from http://www.kb.ecei.tohoku.ac.jp/~koba/papers/hmtt.pdf.

2.

Higher-Order, Multi-Parameter Tree
Transducer

This section defines higher-order, multi-parameter tree transducers(HMTTs) and their verification problems. From a programming

language point of view, an HMTT is a term of the simply-typed λcalculus extended with recursion and tree constructors/destructors.
Trees are classified into input trees, which can only be destructed,
and output trees, which can only be constructed.
D EFINITION 2.1 (sorts). The set of sorts is given by:κ ::= i | o | κ1 → κ2
The sort i describes input trees, while o describes output trees. The
sort κ1 → κ2 describes a function that takes an element of sort κ1
and returns an element of sort κ2
D EFINITION 2.2. A higher-order, multi-parameter tree transducer(HMTT for short) T is a quadruple (Σ, N , R, S), where:• Σ is a ranked alphabet. i.e. a map from a finite set{a1 , . . . , aN } of symbols called terminals to non-negative integers.
• N is a map from a finite set of symbols called non-terminals
to sorts.
• R is a set of rewriting rules of the form F x1 · · · xn → t,
where F ∈ dom(N ) is a non-terminal and t is a term. Here, theset of terms is defined by:t ::= a | x | F | t1 t2 | case(x, ye1 .t1 , . . . , yeN .tN ),where yei abbreviates a sequence of variables, whose length mustcoincide with the arity of ai .
• S is a non-terminal called the start symbol. N (S) must be of
the form i → · · · → i → o.
Furthermore, each rule F x1 · · · xn → t must be well-sorted, i.e.
⊢ F x1 · · · xm → t must be derivable by using the following sortassignment rules:
K ⊢ F : N (F )K⊢a:o· · → o} → o| → ·{zΣ(a)K, x : κ ⊢ x : κK ⊢ t 1 : κ1 → κ2
K ⊢ t 2 : κ1
K ⊢ t 1 t 2 : κ2K⊢x:iK, yei : e
i ⊢ ti : oK ⊢ case(x, ye1 .t1 , . . . , yeN .tN ) : o
N (F ) = κ1 → · · · → κm → o
x 1 : κ1 , . . . , x m : κm ⊢ t : o⊢ F x1 · · · xm → t
Note that in the sort assignment rule for case-expressions, x must
be of sort i; thus, pattern matching on trees are only allowed on
input trees (of sort i).
R EMARK 2.1. Each terminal symbol is used as a constructor for
input trees (of sort i) as well as for output trees (of sort o). In thesort assignment rule above, however, only the sort o → · · · → o →o is assigned, as input trees cannot be constructed in a recursion
scheme. In an environment ρ introduced below, a terminal of arity
k has sort i· · → i} → i.
□
| → ·{zkA Σ-labeled ranked tree, written T , is a mapping from
{1, . . . , A}∗ (where A is the largest arity of symbols in Σ) todom(Σ), such that (i) dom(T ) is closed under the prefix operation,and (ii) if T (x) = a, then {i | xi ∈ dom(T )} = {1, . . . , Σ(a)}.
The set of evaluation contexts is defined by:
E ::= [ ] | a t1 · · · tj−1 [ ] tj+1 · · · tΣ(a)Let ρ be a mapping from a finite set of variables (of sort i) to a setof pairs consisting of a Σ-labeled ranked tree and a non-negative
integer. (The second element of such a pair, called uses, will later beused for defining the linearity condition.) Let T = (Σ, N , R, S).
The reduction relation (t, ρ) −→T (t′ , ρ′ ) is defined by:

E XAMPLE 2.2. Recall the merge function in Section 1. It is expressed as the following HMTT T = (Σ, N , R, Merge).
Σ = {a 7→ 1, b 7→ 1, e 7→ 0}
R = {Merge x y →case(x, x′ .Merge a x′ y, x′ .Merge b x′ y, Copy y)
Merge a x y → case(y,y ′ .a(a(Merge x y ′ )), y ′ .a(Merge b y ′ x), a(Copy x)),Merge b x y → case(y,y ′ .b(Merge a y ′ x), y ′ .b(b(Merge x y ′ )), b(Copy x)),
Copy x → case(x, x′ .a(Copy x′ ), x′ .b(Copy x′ ), e), } □We introduce an important subclass of HMTTs.

F x1 · · · xm → t ∈ R(E[F t1 · · · tm ], ρ) −→T (E[[t1 /x1 , . . . , tm /xm ]t], ρ)ρ′ = ρ{x 7→ (ai Te, j + 1), ye′ 7→ (Te, e0)}(ey ′ are fresh)(E[case(x, ye1 .t1 , . . . , yeN .tN )], ρ) −→T (E[[ey ′ /eyi ]ti ], ρ′ )ρ(x) = (ai Te, j)

Here, [et/ex]t′ denotes the term obtained from t′ by simultaneously
replacing x
e with et. In the rule above, Te denotes a sequence of(possibly infinite) trees, and ai Te denotes a tree whose root islabeled by ai and children are Te.
Suppose that t is a term of type |i → ·{z· · → i} → o. We writek[[T , t, I1 , . . . , Ik ]] for the tree obtained by infinitary rewriting of(t x1 · · · xk , {x1 7→ (I1 , 0), . . . , xk 7→ (Ik , 0)}). More precisely,
it is defined as follows. Given a term t, we write t⊥ for the finite
tree inductively defined by (i) (as1 · · · sn )⊥ = a(s1 ⊥ ) · · · (sn ⊥ )(where n ≥ 0), and (ii) t⊥ = ⊥ if t is of the from F s1 · · · sn orcase(x, ye.t1 , . . . , ye.tn ). For example, (a c (F (b c)))⊥ = a c ⊥.
We define [[T , t, I1 , . . . , Ik ]] as the (possibly infinite) (Σ ∪ {⊥ 7→
F ⊥· · xk , {x1 7→ (I1 , 0),0})-labeled tree {t′ | (t x1 ·F
F . . . , xk 7→′′∗(I
Fk , 0)}) −→T (t , ρ )}, where i Ti is∗ defined by ( i Ti )(π) =i (Ti (π)) for every π ∈ {1, . . . , A} (where A is the largest
arity), with ⊥ ⊔ a = a for every a ∈ dom(Σ).
E XAMPLE 2.1. Consider the HMTT T = (Σ, N , R, Rev) where:Σ = {a1 7→ 1, a2 7→ 1, a3 7→ 0}
N = {Rev 7→ i → o, RevSub 7→ i → o → o}
R = {Rev x → RevSub x a3 ,RevSub x y →case(x, x′ .RevSub x′ (a1 y), x′ .RevSub x′ (a2 y), y)}
T computes the reverse of (the tree representation of) a string over
{a1 , a2 }. If u1 , . . . , un ∈ {a1 , a2 }, then[[T , Rev, u1 (u2 · · · (un−1 (un a3 )) · · · ))]] is:un (un−1 (· · · (u2 (u1 a3 )) · · · )).
Here, the terminal symbol a3 is used to denote the end of a string.
For example, (Rev x, {x 7→ (a1 (a2 a3 ), 0)}) is reduced as follows:(Rev x, ρ = {x 7→ (a1 (a2 a3 ), 0)})−→T (RevSub x a3 , ρ)−→T (case(x,x′ .RevSub x′ (a1 a3 ), x′ .RevSub x′ (a2 a3 ), a3 )), ρ)−→T (RevSub x′′ (a1 a3 ),{x 7→ (a1 (a2 a3 ),1),x′′ 7→ (a2 a3 ,0)})−→∗T (a2 (a1 a3 ), ρ′ )□D EFINITION 2.3 (linear HMTT). An HMTT T = (Σ, N , R, S)
is linear if, for all Σ-labeled ranked trees I1 , . . . , Ik (where kis the arity of S) and for all ρ and t, (S x1 · · · xk , {x1 7→(I1 , 0), . . . , xk 7→ (Ik , 0)}) −→∗T (t, ρ) and ρ(y) = (I, j) imply j ≤ 1, for every y ∈ dom(ρ).
Note that the linearity is a semantic condition. It is possible toconstruct a sound (but incomplete) type system for guaranteeing thelinearity of HMTTs, but the semantic condition is sufficient (andactually more convenient) for our purpose. For order-1 case, thelinearity condition is almost the same as the syntactic condition of
linearity (or, 1-bounded copying) introduced by Maneth et al. [27].
For higher-order cases, one can define a linear type system for(conservatively) guaranteeing the linearity condition.
R EMARK 2.2. The reader may think that the linearity condition is
too restrictive. Actually, however, the class of tree transformations
expressed by linear HMTTs is at least as large as those expressed byvariations of deterministic macro/high-level tree transducers studied in the literature. That follows from the following facts. First,
to our knowledge, all the variations of macro tree transducers (including pebble tree transducers [28] and stay macro tree transducers [27]) studied in the literature can be expressed by compositionsof macro tree transducers (see [6] for the case of pebble tree transducers). Secondly, by the result of Engelfriet [8], any compositionof deterministic, total macro tree transducers can be expressed by asingle deterministic high-level tree transducer. Third, as discussed
in Appendix A, any deterministic high-level tree transducer canbe translated to a linear HMTT by using the tupling transformation [13].
We use a variant of tree automaton called a trivial automaton [2,20] for describing properties on (possibly infinite) input and output
trees of HMTT.
D EFINITION 2.4 (trivial automaton). A Büchi automaton with atrivial acceptance condition (a trivial automaton, for short) M is aquadruple:(Σ, Q, ∆, q0 )where Σ is a ranked alphabet, Q is a set of states, ∆, called atransition function, is a finite subset of Q × dom(Σ) × Q∗ suchthat if (q, a, q1 · · · qk ) ∈ ∆, then k = arity(a). A dom(Σ)labeled tree T is accepted by M if there is a Q-labeled tree R
such that (i) dom(T ) = dom(R); (ii) For every x ∈ dom(R),(R(x), T (x), R(x1) · · · R(xm)) ∈ ∆ where m = arity(T (x)).
R is called a run tree of M over T . A trivial automaton is deterministic if the set {s | (q, a, s) ∈ ∆} is empty or a singleton set forevery q ∈ Q and a ∈ dom(Σ).
(Assuming that ⊥ does not occur in the alphabet of M) we
write M⊥ for the trivial automaton obtained from M by adding
the special symbol ⊥ (of arity 0) to the alphabet, and replacing thetransition relation ∆ with ∆ ∪ {(q, ⊥, ϵ)|q ∈ Q}.

E XAMPLE 2.3. Consider a(Σ, {q0 , q1 }, ∆, q0 ) where

trivialautomaton

M

The rewriting relation t −→G t′ is defined by:=Σ = {a1 7→ 2, a2 7→ 1, a3 7→ 0}∆ = {(q0 , a1 , q0 q0 ), (q0 , a2 , q1 q1 ),(q0 , a2 , q1 ), (q1 , a2 , q1 ), (q0 , a3 , ϵ), (q1 , a3 , ϵ)}F x1 · · · xm → t ∈ R
E[F t1 · · · tm ] −→G E[[t1 /x1 , . . . , tm /xm ]t]

M accepts Σ-ranked trees whose paths are labeled by elements ofωa∗1 a∗2 a3 + a∗1 aω
□
2 + a1 .

E[case(di , t1 , . . . , tl )] −→G E[ti ]We now define the HMTT verification problem, which is themain subject of the rest of this paper.

Here, E denotes an evaluation context, whose syntax is given by:

D EFINITION 2.5 (HMTT verification problem). Let T be an
HMTT with N (S) = k. We write |= (T , M1 , . . . , Mk , M) if[[T , S, I1 , . . . , Ik ]]∈L(M⊥ ) holds for every I1∈
L(M1 ), . . . , Ik ∈ L(Mk ). An HMTT verification problem(T , M1 , . . . , Mk , M) is the problem of deciding whether|= (T , M1 , . . . , Mk , M) holds.

E ::= [ ] | a t1 · · · tj−1 [ ] tj+1 · · · tΣ(a)The value tree of G, written by [[G]], is the (Σ ∪ {⊥ 7→ 1})labelled ranked tree obtained by infinitary rewriting of S, i.e.
F ′⊥{t | S −→∗G t′ }.
E XAMPLE 3.1. Consider the following RSFD G = ({a 7→ 1, b 7→1}, N , {d1 , d2 }, R, S), where:

The problem of model-checking higher-order recursion
schemes [32] (where properties are restricted to those described bytrivial automata) is a special case of the HMTT verification problem (where k = 0).
R EMARK 2.3. Note that the above definition allows ⊥ to occur
in [[T , S, I1 , . . . , Ik ]]. Given finite trees as input, an HMTT may
produce ⊥ when it does not terminate. Thus, the above problem
is slightly different from the problem of exact type checking oftree transducers studied in the literature. They usually check that,given an input tree in L(M1 ), a transducer does terminate andproduces a tree in L(M), while our definition allows the casewhere the program does not terminate. This difference is analogous
to partial vs total correctness in program verification. We consider
only partial correctness, leaving the termination verification as aseparate problem.

3.

Recursion Schemes with Finite Data Domains

N = {S : o, F : d → o}
R = {S → F d1 ,F x → case(x, a(F d2 ), b(F d1 ))}The value tree [[G]] is the infinite tree a(b(a(b(· · · )))).
D EFINITION 3.3 (RSFD model checking problem). Let G be an
RSFD and M be a trivial automaton. The RSFD model checking problem (G, M) is the problem of deciding whether [[G]] ∈L(M⊥ ) holds. We write |= (G, M) if [[G]] ∈ L(M⊥ ) holds.
The RSFD model checking problem is decidable: as sketched in[20], any recursion scheme with finite data domains can be encoded
into an ordinary recursion scheme, and the model checking problem for ordinary recursion schemes is decidable. Instead, it is also
possible to encode an element di of a finite base type {d1 , . . . , dk }into a function of sort o· · → o} → o: λx1 . · · · .λxk .xi . Then,| → ·{zk

In this section, we introduce an extension of higher-order recursion
schemes with finite data domains (RSFD, for short), and define amodel-checking problem for RSFD, into which the HMTT verification problem in the previous section will be transformed.

case(x, t1 , . . . , tk ) can be encoded into x t1 · · · tk . In Section 5,
we given an alternative, direct proof of the decidability, which reduces the RSFD model checking problem into a type checking
problem.

D EFINITION 3.1 (sorts for RSFD). The set of (RSFD) sorts isgiven by:
κ ::= d | o | κ1 → κ2

R EMARK 3.1. Unlike the original definition of the model checking
problem for recursion schemes [32], we here allow [[G]] to generatea tree containing ⊥ for a technical convenience. The problem ofchecking [[G]] ∈ L(M) is also decidable.

D EFINITION 3.2. A higher-order recursion scheme with finite data
domain (RSFD for short) G is a quintuple (Σ, N , D, R, S), where:• Σ is a ranked alphabet.
• N is a map from a finite set of symbols called non-terminals
to sorts.
• D is a finite set {d1 , . . . , dl }.
• R is a set of rewriting rules of the form F x1 · · · xn → t,
where F ∈ dom(N ) is a non-terminal and t is a term. Here, theset of terms is defined by:t ::= a | di | x | F | t1 t2 | case(t, t1 , . . . , tl )The sort assignment rules for terms are the same as those of HMTT,
except the following rules.
K⊢d:d
K⊢t:d
K ⊢ ti : o (for each i)K ⊢ case(t, t1 , . . . , tl ) : o• S is a non-terminal called the start symbol, with N (S) = o.

4.

From HMTT Verification to RSFD
Model-Checking

This section reduces the HMTT verification problem to the modelchecking problem for RSFD. The reduction is sound but incomplete in general: For any HMTT verification problem P1 , if the corresponding model checking problem P2 for RSFD has a positive
answer, then so does P1 , but not vice versa. For linear HMTTs,
however, the reduction is sound and complete.
As mentioned in Section 1, the idea of the transformation is to
use the state of a trivial automaton as an abstraction of an input
tree (of sort i). Let (T , M1 , . . . , Mk , M) be an HMTT verification problem. One can construct a trivial automaton M1,...,k =(ΣI , QI , ∆I , q1 ) such that L(M1,...,k , qi ) = L(Mi ). Here,
L(M1,...,k , qi ) is the set of trees accepted by (ΣI , QI , ∆I , qi ).
Let QI be {q1 , . . . , ql }. We also assume that for every q ∈ QI ,L(M1,...,k , q) ̸= ∅, i.e. there is no garbage state (from which notree can be accepted).
For an HMTT verification problem (T , M1 , . . . , Mk , M)
where T = (Σ, N , R, S) and M = (Σ, Q, ∆, q0 ), we write

br

We now discuss the correctness of the transformation. The following theorem guarantees that (the first element of) the output of
the transformation is indeed a recursion scheme.

br

br

br

br

br

..
.

br
..
.

a2

br

a1
a3

..
.

a2

a1

a2

a3

a3

a3
a2
a3

T HEOREM 4.1 (well-formedness of the recursion scheme).
Let (T , M1 , . . . , Mk , M) be an HMTT verification problem.
If (T , M1 , . . . , Mk , M)# = (G, M′ ), then G is a recursion
scheme.
Proof It suffices to show that each rule of G is well-sorted. We
define a translation of sorts of HMTT into those of RSFD by:
i# = dFigure 3. The tree generated by G of Example 4.1(T , M1 , . . . , Mk , M)# for the pair (G, M′ ), where:
G = (Σ ∪ {br 7→ 2}, N # ∪ {S ′ 7→ o}, QI , R′ , S ′ )R′ = {S ′ → S q1 · · · qk }∪{F x
e → t# | F x
e → t ∈ R}′
M = (Σ ∪ {br 7→ 2}, Q, ∆′ , q0 )∆′ = ∆ ∪ {(q, br, qq) | q ∈ Q}.
Here, N # just replaces each occurrence of sort i in N with d. The
translation t# of a term t is defined by:#

a# = ax# = xF# = F(t1 t2 ) = t1 # t2 #case(x, ye1 .t1 , . . . , yeN .tN )# = case(x, u′1 , . . . , u′l )q1,1 /ey1 ]t1 # ) · · · ([eq1,ki,1 /ey1 ]t1 # )where u′i = br ([e#· · · ([eqN,1 /eyN ]tN ) · · · ([eqN,ki,N /eyN ]tN # )∆(qi , aj ) = {eqj,1 , . . . , qej,ki,j }(Here ∆(q, a) denotes {eq | (q, a, qe) ∈ ∆})In the definition above, br t1 · · · tn is an abbreviated form of:
br t1 (br t2 (br · · · (br tn−1 tn ) · · · ))Note that case analysis on an input tree x is replaced by caseanalysis on the corresponding automaton state x. For each caseqi ∈ Q of x, the case expression reduces to a term of the form
br t1 · · · tm , where t1 , . . . , tm are reducts for all the possible trees
abstracted by qi .
E XAMPLE 4.1. Recall Example 2.1. Let M1 and M be trivial
automata (Σ, Q, ∆1 , q1 ) and (Σ, Q, ∆, q1 ) where:Σ = {a1 7→ 1, a2 7→ 1, a3 7→ 0}
Q = {q1 , q2 }∆1 = {(q1 ,a1 ,q1 ), (q1 ,a2 ,q2 ), (q2 ,a2 ,q2 ), (q1 ,a3 ,ϵ), (q2 ,a3 ,ϵ)}∆ = {(q1 ,a2 ,q1 ), (q1 ,a1 ,q2 ), (q2 ,a1 ,q2 ), (q1 ,a3 ,ϵ), (q2 ,a3 ,ϵ)}Then, (T , M1 , M2 )# = (G, M′ ) whereG = (Σ ∪ {br}, N , {q1 , q2 }, R, S ′ )
R = {S ′ → S q1 , S x → RevSub x a3 ,RevSub x y → case(x, t1 , t2 )}t1 = br (RevSub q1 (a1 y)) (br (RevSub q2 (a2 y)) y)t2 = br (RevSub q2 (a2 y)) yM′ = (Σ ∪ {br 7→ 2}, {q1 , q2 }, ∆, q1 )∆ = ∆ ∪ {(q1 , br, q1 q1 ), (q2 , br, q2 q2 )}Note that input trees have been replaced by states of M1 , and caseanalyses on an input tree have been replaced by case analyses on
the corresponding state of M1 . The value tree of G is illustrated in
Figure 3. □o# = o (κ1 → κ2 )# = κ1 # → κ2 #The translation (·)# is pointwise extended to sort environments.
We can show by induction on the derivation that K ⊢ t : κ impliesK# ⊢ t# : κ# . Thus, any well-sorted rule of T is transformed intoa well-sorted rule of G. □The following theorem guarantees the soundness of our transformation.
T HEOREM 4.2 (soundness). Let (T , M1 , . . . , Mk , M) be an
HMTT verification problem. If |= (T , M1 , . . . , Mk , M)# , then|= (T , M1 , . . . , Mk , M).
Proof Sketch Let (G, M′ ) be (T , M1 , . . . , Mk , M)# . We firstnote that by the definitions of [[G]] and [[T , S, I1 , . . . , Ik ]], we have:(I) [[G]] ∈ L(M′⊥ ) if, and only if, u⊥ ∈ L(M′⊥ ) for every u suchthat S ′ −→∗G u, and (II) [[T , S, I1 , . . . , Ik ]] ∈ L(M⊥ ) if, and only
if, t⊥ ∈ L(M⊥ ) for every t such that ∃ρ.((S x1 · · · xk , ρ0 ) −→∗T(t, ρ)), where ρ0 = {x1 7→ (I1 , 0), . . . , xk 7→ (Ik , 0)}.
We define the relation u ; u′ on RSFD terms of sort o inductively by: (i) br u1 · · · un ; u′i if ui ; u′i , (ii) au1 · · · un ;e;F ue,au′1 · · · u′n if ui ; u′i for each i ∈ {1, . . . , n}, (iii)F u
and (iv) case(u, u1 , . . . , ul ) ; case(u, u1 , . . . , ul ). Intuitively,an RSFD term u represents a set of terms (where br denotes aunion), and u ; u′ means that u′ is an element of the set represented by u.
Suppose that |= (G, M′ ) and (S x1 · · · xk , ρ0 ) −→∗T (t, ρ)with Ii ∈ L(Mi ) for each i ∈ {1, . . . , k}. It suffices to show thatt⊥ ∈ L(M⊥ ). One can prove that (S x1 · · · xk , ρ0 ) −→∗T (t, ρ)⊥
implies S ′ −→∗G u ; u′ and t⊥ = u′ for some u and u′(which intuitively means that G is a correct abstraction of T ). By
the assumption |= (G, M′ ), we have u⊥ ∈ L(M′⊥ ). By the⊥⊥construction of M′ , we have u′ ∈ L(M⊥ ) (note that u′ does⊥⊥
not contain br), which implies t ∈ L(M ) as required. See [23]for more details. □As shown by the following example, the converse of the above
theorem does not hold in general.
E XAMPLE 4.2. Consider an HMTT T = (Σ, N , R, S) where:Σ = {a1 7→ 0, a2 7→ 0, a3 7→ 2}
N = {S 7→ i → o}
R = {S x → case(x, a3 a1 (C x), a2 , · · · ),C x → case(x, a1 , a2 , · · · )}We have omitted the case for a3 since it does not matter. Let M1 be the trivial automaton (Σ, {q0 }, ∆1 , q0 ) where∆1 = {(q0 , a1 , ϵ), (q0 , a2 , ϵ)}. Note that L(M1 ) accepts{a1 , a2 }. Let M be another trivial automaton (Σ, {q0 , q1 }, ∆, q0 ),where ∆ = {(q0 , a2 , ϵ), (q0 , a3 , q1 q1 ), (q1 , a1 , ϵ)}, which accepts {a3 a1 a1 , a2 }. Obviously, |= (T , M1 , M) holds. However,(T , M1 , . . . , Mk , M)# is (G, M′ ) where:
G = (Σ, N , {q0 }, R, S ′ )
R = {S ′ → S q0 , S x → case(x, br (a3 a1 (C q0 )) a2 ),C x → case(x, br a1 a2 )}M′ = (Σ, {q0 , q1 }, ∆′ , q0 )∆′ = {(q0 , br, q0 q0 ), (q1 , br, q1 q1 )} ∪ ∆[[G]] = br (a3 a1 (br a1 a2 )) a2 is not accepted by M′ .
The reason why the transformation above does not preserve thevalidity is that both of the input trees a1 and a2 are abstracted toq0 , and independent choices between a1 and a2 are made in the twocase analyses on x of the recursion scheme (once in the rule for S,
and the other time in the rule for C). □If we restrict ourselves to linear HMTTs and make certain
additional assumptions, then our transformation is complete.
T HEOREM 4.3 (completeness for linear HMTT).
Let (T , M1 , . . . , Mk , M) be an HMTT verification problem. Suppose also that one of the following conditions holds.
1. M = (Σ, Q, ∆, q0 ) is deterministic.
2. If (T , M1 , . . . , Mk , M)# = (G, M′ ), the symbols br only
occur at the top-level of [[G]], i.e. in every path of [[G]] from theroot, br does not occur after other terminal symbols occur.
If T is linear and |= (T , M1 , . . . , Mk , M),
then |= (T , M1 , . . . , Mk , M)# .
Proof Sketch Suppose that |= (T , M1 , . . . , Mk , M) andS ′ −→∗G u. It suffices to show u⊥ ∈ L(M′⊥ ) (recall the firstparagraph of the proof sketch of Theorem 4.2).
By the assumption that T is linear, one can prove that S ′ −→∗Gu ; u′ implies (S x1 · · · xk , {x1 7→ (I1 , 0), . . . , xk 7→⊥(Ik , 0)}) −→∗T (t, ρ) and u′ = t⊥ for some t, ρ, and I1 , . . . , Ik
such that Ii ∈ L(Mi ) for every i ∈ {1, . . . , k}. (This intuitively
means that G is an abstraction of T that is precise enough to capture only the reductions possible in T .) For such t, we have t⊥ ∈L(M⊥ ) by the assumption |= (T , M1 , . . . , Mk , M). By the con⊥⊥struction of M′ and the fact u′ = t⊥ , we have u′ ∈ L(M′⊥ ).
′⊥′′⊥Thus, we have u ∈ L(M ) for every u such that u ; u′ .
We therefore have u⊥ ∈ L(M′⊥ ) if one of the two conditions inthe statement of the theorem holds.
See [23] for more details. □R EMARK 4.1. If neither of the two conditions in Theorem 4.3
holds, the last step of the above proof does not go through. In thatcase, the completeness does not hold indeed. Consider the HMTT
T = (Σ, N , R, S) where:Σ = {a1 7→ 1, a2 7→ 0, a3 7→ 0}
N = {S 7→ i → o}
R = {S x → case(x, x′ .a1 (S x′ ), a2 , a3 )}It just generates a copy of a given input tree. Let us consider(non-deterministic) automata M1 = (Σ, {q1 , q2 }, ∆1 , q1 ) andM = (Σ, {q1 , q2 }, ∆, q1 ) where∆1 = {(q1 , a1 , q2 ), (q2 , a2 , ϵ), (q2 , a3 , ϵ)}∆ = {(q1 , a1 , q2 ), (q1 , a1 , q3 ), (q2 , a2 , ϵ), (q3 , a3 , ϵ)}.
Since both automata accept {a1 a2 , a1 a3 }, |= (T , M1 , M) holds.
Our transformation algorithm generates the recursion scheme G =(Σ ∪ {br 7→ 2}, N , {q1 , q2 }, R, S ′ ) and the automaton M′ =(Σ ∪ {br 7→ 2}, Q, ∆ ∪ {(q1 , br, q1 , q1 ), (q2 , br, q2 , q2 )}, q1 )where R consists of:
S ′ → S q1

S x → case(x, a1 (S q2 ), br a2 a3 )It generates a finite tree a1 (br a2 a3 ). The tree is NOT accepted by
M′ : note that no state can be assigned to the subtree br a2 a3 .
The second condition of Theorem 4.3 can be guaranteed byapplying the CPS transformation, which ensures that an output
tree is returned only after all the non-deterministic branches havebeen made. For example, the HMTT can be transformed into thefollowing equivalent HMTT (where only the rewriting rules areshown).
S x → S1 x I
Ix→x
C k x y → k(x(y))
S1 x k → case(x, x′ .S1 x′ (C k a1 ), k a2 , k a3 )It generates the tree br (a1 a2 ) (a1 a3 ), which is accepted by M′ .
The HMTT verification problem is undecidable in general, since
we can encode Post correspondence problem.
T HEOREM 4.4. The HMTT verification problem is undecidable.
Proof Let A be {a1 , ..., an } and consider a Post correspondence
problem(u1 , v1 ), ..., (um , vm ) ∈ A∗ × A∗
Without loss of generality, we may assume that m = n, since if
m < n, we can add dummy pairs (ϵ, ϵ) as (uk , vk ) for m < k ≤n. The Post correspondence problem is the problem of deciding
whether there exists a sequence i1 · · · iℓ such thatui1 ui2 · · · uiℓ = vi1 vi2 · · · viℓ .
We shall construct an HMTT that takes a candidate of such asequence, and checks whether the candidate satisfies the condition
above. Let T be an HMTT (Σ, N , R, S) where:Σ = {a1 7→ 1, . . . , an 7→ 1, e 7→ 0, yes 7→ 0, no 7→ 0}
N = {S 7→ i → o}∪{Subu,v 7→ i → i → o |u, v are suffixes of ui and vj for some i and j}∪{IsNullu 7→ i → o | u is a suffix of ui for some i}
R = {S x → Subε,ε x x}∪{Subε,s x y →case(x, x′ .Subu1 ,s x′ y, . . . , x′ .Subun ,s x′ y, IsNulls y)| s ∈ {a1 , . . . , an }∗ }∪{Subs,ϵ x y →case(y, y ′ .Subs,v1 x y ′ , . . . , x.Subs,vn x y ′ , IsNulls x)| s ∈ {a1 , . . . , an }+ }∪{Subau′ ,av′ , x y → Subu′ ,v′ , x y | a ∈ A, u′ , v ′ ∈ A∗ }∪{Subau′ ,bv′ , x y → no | a, b ∈ A, u′ , v ′ ∈ A∗ , a ̸= b}∪{IsNullϵ x → case(x, x′ .no, · · · , x′ .no, yes)}∪{IsNulls x → no | s ∈ A+ }Here, we assume that yes and no do not occur in input trees, andomit cases for yes and no in case expressions.
The above HMTT takes as input (the tree representation of)a sequence ai1 ai2 · · · aiℓ ∈ A∗ , and checks whether the strings
ui1 ui2 · · · uiℓ and vi1 vi2 · · · viℓ are the same, by comparing theirelements one by one. In Subu,v, x y, x and y are bound to suffixesof ai1 ai2 · · · aiℓ , and it is checked whether uuiℓ+1−|x| · · · uiℓ andvviℓ+1−|y| · · · viℓ are the same. Thus, the HMTT outputs yes if thesequence is a solution for the Post correspondence problem and nootherwise. Let M1 and M2 be trivial automata:
M1 = (Σ, {q0 }, ∆1 , q0 )∆1 = {(q0 , ai , q0 ) | ai ∈ A} ∪ {(q0 , b, ϵ)}M2 = (Σ, {q0 }, ∆2 , q0 )∆2 = {(q0 , no, ϵ)}Then, |= (T , M1 , M2 ) if and only if the Post correspondence
problem {(u1 , v1 ), . . . , (un , vn )} has no solution. Since Post correspondence problem is undecidable, the HMTT verification problem is also undecidable. □5.

Type System for Model-Checking Recursion
Schemes with Finite Data Domains

This section gives a type system for recursion schemes with finite
data domains (which is parameterized by a trivial automaton M),
such that an RSFD G is well-typed in the type system if, and only
if, |= (G, M) holds. Thus, the RSFD model checking problem
is reduced to a type checking problem, which can be solved byextending Kobayashi’s type inference algorithms [18, 20].
Let M be a trivial automaton (Σ, Q, ∆, q0 ), and D be a finite
set {d1 , . . . , dk }. The set of types is given by:Vτ ::= di | qj | n
i=1 τi → τ
Intuitively, di ∈ D is a singleton type, describing the value di .
The type qj ∈ Q describes
V trees accepted from qj (i.e. elements ofL(M, qj )). The type n
i=1 τn → τ describes functions that takean element having types τ1 , . . . , τn and return an element of typeτ.
A type judgment for terms (where a non-terminal is treated asa variable) is of the form Γ ⊢M t : τ , where Γ, called a typeenvironment, is a finite set of bindings of the form x : τ . Γ may
contain more than one bindings for each variable.
The typing rules are given by:
Γ, x : τ ⊢M x : τΓ ⊢M d i : d i(q, a, q1 · · · qn ) ∈ ∆Γ ⊢M a : q1 → · · · → qn → qVΓ ⊢M t0 : n
i=1 τi → τΓ ⊢M t1 : τi (for each i = 1, . . . , n)
Γ ⊢M t 0 t 1 : τΓ ⊢M t : diΓ ⊢M ti : q(for some i)Γ ⊢M case(t, t1 , . . . , tk ) : q
Γ, x : τ1 , . . . , x : τn ⊢M t : τx not occur in ΓVΓ ⊢M λx.t : n
τ
→
τ
i
i=1
Let G be a recursion scheme with finite domains(Σ, N , D, R, S). We write ⊢M G : Γ if Γ ⊢ R(F ) : τholds for every F : τ ∈ Γ. A recursion scheme G is well-typed,
written ⊢M G, just if there exists Γ such that (i) ⊢M G : Γ,(ii)S : q0 ∈ Γ, and (iii) for each F : τ ∈ Γ, τ :: N (F ) holds (i.e.
the sorts declared in N are respected). Here, the relation τ :: κ,which means thatV τ is a type of sort κ, is defined by: (i) q :: o, (ii)q :: d, and (iii) ki=1 τi → τ :: κ′ → κ if τ :: κ and τi :: κ′ for eachi ∈ {1, . . . , k}.
The following theorem is an extension of the result of
Kobayashi [20]. The proof is almost the same as that of the soundness and completeness of the type system for recursion schemes(without finite data domains) [20], hence is omitted.
T HEOREM 5.1. Let M be a trivial automaton, and G be a recursion scheme with finite domains, If [[G]] is well-defined, then ⊢M G
if and only if |= (G, M).
C OROLLARY 5.2. The RSFD model-checking problem is decidable.

6.

Complexity of the Verification Algorithm

We briefly discuss the complexity of our HMTT verification algorithm, which consists of two phases: transformation into a recursion scheme (with finite data domains) and model checking of therecursion scheme.
Let (T , M1 , . . . , Mk , M) be an HMTT verification problem. We may assume that Mi = (Σ, Q0 , ∆0 , qi ) for each i(i.e. M1 , . . . , Mk differ only in their initial states). Let |T |be the size of the rewriting rules of T . We also assume thatthe rewriting rules of T are normalized, so that each bodyof a rewriting rule contains at most one case-expression. Let(T , M1 , . . . , Mk , M)# be (G, M′ ). The size |G| of the rewriting rules of G is O(|Q0 |AΣ +1 |T |) where AΣ is the largest arityof terminal symbols: note that only the sizes of case expressions
may increase, and for each body of a case expression, at most|{(q, qe) | (q, a, qe) ∈ ∆}| (which are bounded by |Q|A+1 ) copies
are created.
As for the time complexity of model-checking G, we can apply the same argument as [20, 22] to obtain an upper-boundO(|G|expn ((A(|Q0 | + |Q′ |))1+ϵ )) for arbitrary ϵ > 0 for n ≥ 2,
where n is the order of the recursion scheme G and |Q′ | is the number of states of M′ , and A is the largest arity of symbols in G. Here,
expn (x) is defined by: exp0 (x) = x and expn+1 (x) = 2expn (x) .
Thus, the time complexity of our HMTT verification algorithmis O(|T |expn ((A(|Q0 | + |Q|))1+ϵ )) for n ≥ 2, where |Q| isthe number of states of M. If the largest arity and the number of
automaton states are fixed, it is linear in the size of HMTT. (Note,however, that the constant factor is huge.)
Theorem 4.3 implies that if the HMTT is linear and the automaton M is deterministic, then the HMTT verification problem is decidable. For this decidable fragment, the verification problem itself
is (n − 1)-EXPTIME complete for n ≥ 2 (in the combined size ofa recursion scheme and an automaton), as described below. First,
from a deterministic trivial automaton M, one can construct a disjunctive alternating parity tree automaton (disjunctive APT) [21]that accepts the complement of L(M) and the size of the disjunctive APT is linear in that of M. Thus, the model checking problem
for the class of deterministic trivial automaton can be reduced tothat for the class of disjunctive APT [21], which gives the upperbound of (n − 1)-EXPTIME. Secondly, it follows from the resultof [21] (more precisely, from the (n − 1)-EXPTIME hardness of
the reachability problem) that the problem of model-checking recursion schemes for the class of deterministic trivial automata is(n − 1)-EXPTIME hard. For n = 1, by a similar argument, if we
assume that the largest arity of terminals and non-terminals is fixed,
the HMTT verification problem is polynomial-time.2

7.

Applications

This section discusses applications of our HMTT verification
framework.
7.1

Resource Usage Verification

As mentioned in Section 1, the goal of resource usage verification [14] is to check whether a given program accesses each resource in a valid manner. In our previous work [20], we considered
2 This result is similar to, but should not be confused with the result of[27], which shows that the exact type checking of linear MTT is polynomial
time under a similar assumption about arities and the assumption that the
specification is given by a deterministic bottom-up tree automaton. The
class of languages of finite trees accepted by deterministic trivial automata
is strictly less expressive than the class of those accepted by deterministicbottom-up tree automata. Thus, our result is weaker in this sense. On theother hand, we allow multiple input trees as arguments of non-terminals.

resource usage verification of a closed program. Our HMTT verification framework allows us to perform resource usage verificationof an open program, which is a function that takes some parameters
as input.
For example, consider the following program:let rec accfile cmds = match cmds with[] -> close(fp)| r::cmds’ -> read(fp); accfile cmds’ fp| w::cmds’ -> write(fp); accfile cmds’ fp
It takes a list of “commands” consisting of r and w, and accesses
the resource x according to the list of commands, and then closesit.
We can covert the above program into the following HMTT T(only the rewriting rules are shown):
AccFile cmds = case cmds of e => close| r(cmds’) => read(AccFile cmds’)| w(cmds’) => write(AccFile cmds’).
For the sake of readability, throughout this section, we use ordinary
pattern matching constructs, which can be easily translated intocase expressions of HMTT. We also write = instead of ->. To
verify that if the list of commands only consists of r, then the file
pointer fp is only read and then closed, it suffices to consider the
HMTT verification problem (T , M1 , M), where M1 accepts thelanguage consisting of linear trees labeled by elements of r∗ (e) +rω and M accepts the language consisting of linear trees labeledby elements of read∗ (close) + readω .
7.2

Verification of XML-Processing Programs

Another application domain of our HMTT verification algorithm isexact type checking of XML-processing programs [25, 27, 28, 34].
We assume below that XML documents (which are unranked
trees) are represented as binary trees in the standard manner: theleft and right children of a node in the binary tree representation
stand for the leftmost child and the leftmost sibling respectively.
An obvious advantage of our approach over previous work
based on macro/high-level tree transducers is that we can handle
programs that take multiple XML documents. Let Σ = {addr 7→
2, doc 7→ 1, e, pc 7→ 0} and M = (Σ, {q0 , q1 , q2 }, ∆, q0 ) where∆ = {(q0 , doc, q1 ), (q1 , addr, q2 q1 ), (q2 , pc, ϵ), (q1 , e, ϵ)}.
M accepts (the binary tree representation of) trees of the form
doc(addr(pc)∗ ), i.e. documents containing a sequence of address
data addr(pc) (the terminal e represents the end of a sequence).
Consider the following HMTT:
MergeAddr x y = case x of
doc x1 => doc(MergeAddr x1 y)| addr x1 x2 => addr (M x1) (MergeAddr x2 y)| e => M y | pc => pc.
M x = case x of doc x1 => M x1
| addr x1 x2 => addr (M x1) (M x2)| e => e | pc => pc.
It takes two documents of the form doc(addr(pc)∗ ) as input, andmerges them into one document. One can verify that, given two
valid documents (of type doc(addr(pc)∗ )), T produces anothervalid document, by checking that |= (T , M, M, M) holds.
For another example, consider the following HMTT T , whichremoves all the b nodes occurring as descendants of a nodes.
RemoveB x = F x G.
F x g = case x of doc y => doc (F y g)
| a x y => a (g x) (F y g)
| b x y => b (F x g) (F y g)
| pc => pc | e => e.

G x = case x of doc y => doc (G y)| b x y => (G y)| a x y => a (G x) (G y)| pc => pc | e => e.
The non-terminal F represents a higher-order function, which takes
a tree x and a function g, and applies g to the child of each a node.
Let M1 be an automaton that accepts binary tree representation oftrees of the form doc(t∗ ) (where doc does not occur in t), and M
be an automaton that accepts only trees in which b does not occur
below a (in the corresponding unranked representation). Then, it
can be verified that |= (T , M1 , M) holds.
7.3

String Analysis

Our HMTT verification algorithm is also applicable to string analysis, whose goal is to statically check that, given valid strings as
input, a program generates a valid string. String analyses havebeen extensively studied in the context of Web applications, toguarantee the well-formedness of output HTMLs [29] or detectsecurity vulnerabilities such as SQL-injection or cross-site scripting [12, 15, 38]. They are also applicable to other application domains such as static resolution of dynamically specified resource
names [24, 33].
A (regular) string analysis problem can be encoded to an HMTT
verification problem by representing strings as linear trees. For
example, the function replace that takes three strings sa , sb andx and returns the string obtained by replacing each occurrence ofa and b in x with sa and sb respectively, can be represented as thefollowing HMTT:
Replace sa sb x = Conv sa (C1 sb x).
C1 sb x u = Conv sb (Repl x u).
Repl x u v = case x ofa(y) => u(Repl y u v)
| b(y) => v(Repl y u v)
| e => e.
Conv x k = case x of a(y) => Conv y (C2 k a)| b(y) => Conv y (C2 k b)
| e => k I.
C2 k y z = k(Concat y z).
Concat x y z = x(y z).
I x = x.
Here, Conv and Concat are generic functions to express a stringprocessing program as an HMTT. Conv converts an input string toa function of type o → o, which is used as an internal representation of strings. For example, a string ab (represented as a(b e)) isconverted to a function λx.a(b x). By using the internal representation, string concatenation is expressed as Concat as defined above.
Let A and B be regular word languages. Then one can verify that
T : A → B → a∗ b∗ e → A∗ B ∗ e (i.e. given elements of A and B,
and an element of of a∗ b∗ e, T produces an element of A∗ B ∗ e).
The function Replace sa sb is equivalent to the word homomorphism h(a) = sa , h(b) = sb .
We can also encode an arbitrary non-deterministic finite statetransducer (FST) by linear HMTT. Homomorphisms and FSTs subsume a large class of practical sanitization; For example, let Σ ={a 7→ 1, b 7→ 1, ♯ 7→ 1, e 7→ 0} and suppose ♯ stands for a “dangerous” meta-character (such as tag-markers < and > of XHTML).
Then, replace s♯ x, replacement of ♯ by s♯ , represents the sanitization of ♯. One can verify the image (replace a b s♯ )(A∗ ) does
not contain an occurrence of ♯ as long as s♯ does not. Sanitizationof sequences (such as the <script> tag of XHTML) can also beverified by encoding FSTs.
Interestingly, we can allow arbitrary use of string homomorphisms in a string-processing program (even inside recursion), bychoosing an appropriate internal representation of strings. Con-sider strings over {a, b}∗ . Then, we can use a function of type
str = (o → o) → (o → o) → o → o as the internal representation of a string. Intuitively, the first two parameters of typeo → o represent the homomorphism images of a and b respectively, while the last parameter is the suffix of a string. (Thus, it issimilar to the Church encoding of natural numbers.)
We can define primitive functions on strings as follows.
A xa xb z = xa z.
B xa xb z = xb z.
Empty xa xb z = z.
Concat s1 s2 xa xb z = s1 xa xb (s2 xa xb z).
I2Str x = case x of e => Empty| a(y) => Concat A (I2Str y)| b(y) => Concat B (I2Str y).
Str2O s = s a b e.
Hom sa sb s xa xb z= s (sa xa xb) (sb xa xb) z.
A, B, and Empty are internal representations of a, b, and an empty
string respectively. The non-terminal Concat represents the concatenation of (internal representations of) two strings. I2Str and
Str2O convert an input string to the internal representation, and theinternal representation to an output string, respectively. The nonterminal Hom represents a generic homomorphic function, such that
Hom sa sb is a string homomorphism that replaces a and b with sa
and sb respectively. Consider the following HMTT:
HomRep n s = F n (Hom (Concat B B) A) (I2Str s).
F n h s = case n of zero => (Str2O s)| succ(m) => F m h (h s).
It takes a natural number n and a string s as an argument, and applies the homomorphism {a 7→ bb, b 7→ a} n times. We can verify,
for example, that if n is even and s is an element of a∗ (b∗ (e)), thenso is the output.
7.4

Verification of Programs Manipulating Other Algebraic
Data Structures

Our verification framework is also applicable to functional programs manipulating other algebraic data structures.
The following HMTT takes two natural numbers as input andreturns the multiplication.
Mult x y = case x of zero => zero
| succ(z) => Add y (Mult z y).
Add x y = case x of zero => y| succ(z) => succ(Add z y).
By using our algorithm, we can verify that, given an even number
and an odd number, the HMTT returns an even number.
The following HMTT takes nested lists (of elements a and b) as
inputs, and returns a flat list.
Flatten x = F x nil.
F x z = case x of nil => z
| cons x1 x2 => F x1 (F x2 z)| a => cons a z| b => cons b z.
We can verify that, given an arbitrary nested list, the HMTT returns
a flat list.

8.

Preliminary Experiments

To evaluate the effectiveness of our verification framework, wehave extended the implementation of TR EC S [18, 19], a model
checker for recursion schemes, to handle recursion schemes withfinite data domains.
The transformation from HMTT to recursion schemes with finite data domains has not been implemented yet, so that we have

manually translated HMTTs in the experiments below. For the experiments on XML processing programs, automata have been automatically generated from DTD-like definitions.
Table 1 shows the result of preliminary experiments. The experiments were conducted on a machine with Intel(R) Xeon(R) CPU
3GHz and 2GB memory. The columns “O”, “R”, “S” show theorder, the number of rules, and the size of HMTTs respectively.
Here, the order of an HMTT is the largest order of the sorts of nonterminals. The order of a sort is defined by:order (i) = order (o) = 0
order (κ1 → κ2 ) = max (order (κ1 ) + 1, order (κ2 ))The size of an HMTT is measured by the number of symbols occurring in the righthand side of the rewriting rules. The column “L”
shows whether the HMTT is linear (L) or not (NL). The column“Q” shows the sum of the numbers of the states of automata for
the input specification (M1,...,k ) and the output specification (M).
All the automata used for the experiments are deterministic. The
column “Y/N” shows whether the HMTT was verified (Y) or rejected (N) (note that because of the incompleteness for non-linear
HMTTs, a valid HMTT verification problem may be rejected). The
column “T” shows the running time of TR EC S (thus, excluding thetime for transformation from HMTT to RSFD, which is currently
manual), measured in milli-seconds.
The programs in the first group (from Rev to Flatten) havebeen taken from the examples already shown in the paper; the nameof each program indicates the start symbol of the corresponding
example in the paper. All of them have been correctly verified ina few milliseconds, except that it took 29 milliseconds for HomRep(the last example in Section 7.3).
R EMARK 8.1. Note that Mult is non-linear, but it is verified correctly. If the property of Mult were “Given an even number x anda number y, Mult x y returns an even number”, then our verifier
would report a false alarm. To avoid the false alarm, we need toeither swap the arguments x and y, or transform Mult into a linear
HMTT.
□
The programs in the second group have been taken from
Tozawa’s experiments [34] (which are the only experimental results on exact type checking of high-level tree transducers in theliterature, to our knowledge) and rewritten in HMTTs. The program app fo takes a document of the following DTD:
type Input
type Preface
type Header
type P
type Div
type Note= doc[Preface, (Div|P|Note)*]= preface[Header, P*]= header[]= p[]= div[(Div|P|Note)*]= note[P*]Then, it inserts an appendix node to the end of the document,
and moves preface and note nodes in the original document tothe appendix. The program appx fo works almost the same as
appendix except that it transforms the document into an XHTML
document. The program gapid takes a document of the DTD of
appendix extended with a nodes, as well as another tree as arguments. It checks whether the children of each node are empty,
and if so, replaces the empty children with a hole. The program
then inserts a given tree to the holes. The programs xml rep1
and xml rep2 are the same, and differ only in their output specifications. They take a document of the same type as gapid anda tree with a hole, and then replace each div node of the document with a tree obtained from the input tree with a hole by inserting the child of div node to the hole. The output specification of
xml rep2 is not satisfied, so the model checker (correctly) rejected
it with a counterexample. All the programs in the second group

Programs
Rev
Merge
AccFileMergeAddr
RemoveB
Replace
HomRepMult
Flattenapp foappx fogapid
xml rep1
xml rep2
XhtmlS id
XhtmlS div
XhtmlS m
XhtmlS div’XhtmlS a
XhtmlM id
XhtmlM div
XhtmlM m
XhtmlM div’XhtmlM a
XhtmlF id

O
1
1
1
1
2
2
4
1
1
1
1
3
3
3
1
1
1
1
1
1
1
1
1
1
1

R
2
5
2
3
4
8
10
3
3
6
5
10
8
8
1
1
1
2
2
1
1
1
2
2
1

S
14
47
9
26
36
45
53
18
17
171
174
94
84
84
113
110
110
161
161
168
165
165
232
232
398

L
L
L
L
L
L
L
L
NL
L
NL
NL
L
L
L
L
L
L
L
L
L
L
L
L
L
L

Q
4
3
4
6
7
4
4
4
4
21
19
30
23
23
24
24
24
24
24
64
64
64
64
64
100

Y/N
Y
Y
Y
Y
Y
Y
Y
Y
Y
Y
Y
Y
Y
N
Y
N
Y
N
Y
Y
N
Y
N
Y
Y

T
1
1
1
1
1
1
29
1
1
5
6
87
3
1
11
2
18
2
17
395
4
138
5
291
13,889

Table 1. Experimental Results

Model checking of recursion schemes have been extensively
studied [1, 2, 11, 16, 17, 32]. Higher-order grammars (where nonterminals can generate “functions” rather than words or trees) related to higher-order recursion schemes have been introduced inearly 70’s [35, 37], and actively studied in 80’s. [4]. Knapik et
al. [17] studied the model checking problem for recursion schemesin the present form, and showed that the modal mu-calculus model
checking of safe recursion schemes is decidable. Ong [32] extended
the decidability result to arbitrary recursion schemes (without thesafety condition). Kobayashi [20] showed that the resource usage
verification of functional programs [14] (which subsumes otherstandard verification problems such as reachability and control flow
analysis) can be reduced to model-checking problems for recursion schemes. Kobayashi [18] then constructed a model-checker
for recursion schemes, demonstrating that the program verification
method based on recursion schemes may be feasible in practice,despite the extremely high worst-case time complexity. The present
work is built on these results, and extend them to deal with higherorder, multi-parameter tree transducers (while recursion schemes
are just tree generators, instead of tree transformers). The extension significantly widens application domains of the verification
framework, as discussed in the present paper.
In the context of exact type-checking of XML processing programs, a lot of variations of macro/high-level tree transducers havebeen studied [25, 27, 28, 34]. A nice feature of those tree transducers is that the class of regular tree languages is closed under the inverse of transducers, and that the inverse image is indeed computable. Thus, given a transducer verification problem?

T (L1 ) ⊆ L2 (where L1 and L2 are regular languages), one can?

have been correctly verified (or rejected) in less than 100 milliseconds. Tozawa [34] reported that it took from 600 milliseconds to
2.2 seconds for his system to check programs of the same functionality.3
The programs in the third group are those manipulating
XHTML documents. We have used two subsets of XHTML specification (indicated by XhtmlS and XhtmlM in the table), and the full
XHTML specification (indicated by XhtmlF in the table). The subset XhtmlS consists of the tags <div>, <p>, <a>, <img/>, <br/>and <h1> to <h6>, which are most commonly used. XhtmlM additionally has the tags <table> <ol>,<ul>,<li>,<dl>,<dt>, <dd>,and <form>. We have tested five operations: * id just outputs acopy of a given input document, * div removes all the nodes labeled by div (hence the output is an invalid document), and * mremoves all the meta nodes in the header. The program * div’ removes only the tags div, instead of removing all the nodes under
div, and * a removes the tags a.
For the subsets of XHTML (XhtmlS and XhtmlM), all the examples have been verified or rejected correctly in less than a second. For the full XHTML, it took more than 10 seconds even for
the identity function. This indicates that there is a problem in thescalability of our verification technique to large input/output specifications. For MTTs, Frisch and Hosoya [10] report that they could
verify MTTs on the full XHTML in about a second.

9.

Related Work

From the viewpoint of program verification, there are at least three
threads of related work: model checking of higher-order recursion
schemes, exact type-checking for macro/high-level tree transducers, and string analysis.
3 This is according to Tozawa’s slides presented at the conference;the pa-

per [34] does not report experimental results.

reduce it to the inclusion problem L1 ⊆ T −1 (L2 ) between theregular languages T −1 (L2 ) and L1 . This inverse inference approach is applicable to composition of transducers, and also to thehigher-order case (called high-level transducers [8, 34]). On theother hand, our approach can be considered a forward inference approach. Given an input language and an HMTT, our transformation
essentially approximates (or precisely models, in the case of linear HMTTs) the output language by using a recursion scheme. We
then check that the language represented by the recursion scheme
conforms to the output specification.4 Maneth et al. [27] take a forward inference approach for exact type checking of linear macro
tree transducers, and uses a context-free tree grammar to approximate the output language. Our approach may be considered a generalization of that approach to higher-order, multi-parameter transducers. Advantages of our approach using HMTTs are: (i) HMTTs
can take multiple input trees, and there is no such restriction thatthe first argument must be an input tree, and (ii) our verification
method seems more efficient than the previous approach based on
the inverse inference for higher-order transducers [34]. For (ii), theinverse inference approach suffers from extremely high time complexity for the higher-order transducers [34] or compositions ofmultiple transducers. On the other hand, limitations of our verification method are: (i) we have to impose the linearity restriction
to ensure completeness, and (ii) the method is not directly applicable to composition of HMTTs (unless specification of interme4 Interestingly, many of the previous papers on inverse type inference(e.g. [26]) argue that forward type inference does not work because theimage of the transformation is not a regular language. For the purpose ofchecking types, however, it is actually unnecessary to compute the image L
as a regular language; it is sufficient that L ⊆ R is decidable for any regular
language R. Combined with the tupling transformation discussed in [23],we can exactly express the image of a high-level tree transducer as a recursion scheme, and since the model checking problem for recursion schemesis decidable, the forward inference approach actually works for high-leveltransducers (which subsume most of the other transducers in the literature)!

diate trees are given). As discussed in Remark 2.2, however, linear
HMTTs are already at least as expressive as compositions of (deterministic) macro/high-level tree transducers studied in the literature.
Furthermore, for (ii), one can sometimes use fusion (or deforestation) transformation [36] to compose multiple HMTTs into a single
HMTT, and then apply our verification method.
As already mentioned, our method can also be applied tostring analysis, by representing strings as linear trees. Previous approaches to string analysis [3, 29] extract a context-free grammarfrom a flow graph or SSA form of a program, and then matches itwith an output specification. In such approaches, information about
the output string is approximated at join points of the flow graph,
especially at function calls. Our approach instead models a program as an HMTT, which naturally models higher-order functions
and is more expressive than context free grammars (indeed, order-1
recursion schemes are already as expressive as context-free grammars). Thus, our verification technique would be more precise foranalyzing higher-order programs. Another interesting advantage of
our approach is that string homomorphisms can be expressed andfreely used inside recursion (recall Section 7.3). On the other hand,the previous approaches [3, 29] return very conservative approximations when string homomorphisms are used in a loop.
Refinement types [5, 9] have been used for verification of programs manipulating algebraic data structures (the application domain discussed in Section 7.4). To our knowledge, most of the previous studies on refinement types rely on explicit type annotations(except perhaps the first work on refinement types [9], which uses
a naive fixedpoint algorithm for type inference and does not seemto scale for higher-order functions). A limitation of our approachis that data structures must be strictly classified into sorts i and o.
One way to overcome the limitation is to use predicate abstraction
for intermediate data structures, as suggested in [20]. Another way
would be to introduce an explicit coercion operation from trees ofsort o to sort i, and force a programmer to annotate each coercion with a refinement type specification. Then, refinement typechecking of such a program can be reduced to multiple HMTT verification problems. For example, let us consider a type checking
problem of the following insertion sort:
let rec insert x y = ...
let rec isort x =case x ofnil => nil∗ ∗ ∗| cons x1 x2 => insert x1 (coerceoa→bi c (isort x2))
Here, suppose that we want to verify that isort takes a sequence
consisting of a, b, c and returns a sequence of the form a∗ b∗ c∗ .
The coercion converts the result of isort x2 to an input tree.
Thanks to the annotation, we should be able to split the above
verification problem into the verification problems of the following
two HMTTs (Isort1 and Isort2):
Isort1 x z = case x of nil => nil| cons x1 x2 => Insert x1 z.
Isort2 x z = case x of cons x1 x2 => Isort1 x2 z.
Isort1 is obtained from the original isort function by replacing the∗ ∗ ∗part (coerceao→bi c (isortx2)) with z. Isort2 corresponds to thepart isort x2. Then, it suffices to check that Isort1 and Isort2
both conform to the specification (a + b + c)∗ → a∗ b∗ c∗ →a∗ b∗ c∗ . The formalization of this idea is left for future work.
Intersection type systems equivalent to model-checking havebeen studied by Naik and Palsberg [30, 31]. They considered intersection an imperative language and did not treat higher-orderprograms.

10.

Conclusion

We have introduced a new class of tree transducers called higherorder multi-parameter tree transducers, and proposed a verification algorithm for them. Compared with our previous verification
framework based on recursion schemes [20], our new approach significantly increases application domains. The result of preliminary
experiments is promising, although there is still a problem in scalability (especially with respect to the size of specifications). It is left
for future work to investigate whether it is a fundamental limitationof our verification framework, or it is just a limitation of the current
implementation of the underlying model checker TR EC S.

References[1] K. Aehlig. A finite semantics of simply-typed lambda terms for infinite
runs of automata. Logical Methods in Computer Science, 3(3), 2007.
[2] K. Aehlig, J. G. de Miranda, and C.-H. L. Ong. The monadic second
order theory of trees given by arbitrary level-two recursion schemes isdecidable. In TLCA 2005, volume 3461 of Lecture Notes in Computer
Science, pages 39–54. Springer-Verlag, 2005.
[3] A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise analysis of string expressions. In Static Analysis, 10th International Symposium, SAS 2003, volume 2694 of Lecture Notes in Computer Science,
pages 1–18. Springer-Verlag, 2003.
[4] W. Dam. The io- and oi-hierarchies. Theoretical Computer Science,
20:95–207, 1982.
[5] R. Davies. Practical refinement-type checking. PhD thesis, Pittsburgh,
PA, USA, 2005.
[6] J. Engelfriet and S. Maneth. A comparison of pebble tree transducers
with macro tree transducers. Acta Inf., 39(9):613–698, 2003.
[7] J. Engelfriet and H. Vogler. Macro tree transducers. J. Comput. Syst.
Sci., 31(1):71–146, 1985.
[8] J. Engelfriet and H. Vogler. High level tree transducers and iterated
pushdown tree transducers. Acta Inf., 26(1/2):131–192, 1988.
[9] T. Freeman and F. Pfenning. Refinement types for ML. In Proceedingsof ACM SIGPLAN Conference on Programming Language Design and
Implementation, pages 268–277. ACM Press, 1991.
[10] A. Frisch and H. Hosoya. Towards practical typechecking for macro
tree transducers. In Database Programming Languages, 11th International Symposium (DBPL 2007), volume 4797 of Lecture Notes in
Computer Science, pages 246–260. Springer-Verlag, 2007.
[11] M. Hague, A. Murawski, C.-H. L. Ong, and O. Serre. Collapsible
pushdown automata and recursion schemes. In Proceedings of 23rd
Annual IEEE Symposium on Logic in Computer Science, pages 452–
461. IEEE Computer Society, 2008.
[12] W. G. J. Halfond and A. Orso. Amnesia: analysis and monitoring
for neutralizing sql-injection attacks. In ASE ’05: Proceedings ofthe 20th IEEE/ACM international Conference on Automated software
engineering, pages 174–183, New York, NY, USA, 2005. ACM.
[13] Z. Hu, H. Iwasaki, M. Takeichi, and A. Takano. Tupling calculation
eliminates multiple data traversals. In Proceedings of International
Conference on Functional Programming, pages 164–175, 1997.
[14] A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Transactions on Programming Languages and Systems, 27(2):264–313,
2005.
[15] N. Jovanovic, C. Kruegel, and E. Kirda. Precise alias analysis for static
detection of web application vulnerabilities. In PLAS ’06: Proceedingsof the 2006 workshop on Programming languages and analysis forsecurity, pages 27–36, New York, NY, USA, 2006. ACM.
[16] T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories
of hyperalgebraic trees. In TLCA 2001, volume 2044 of Lecture Notes
in Computer Science, pages 253–267. Springer-Verlag, 2001.
[17] T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown
trees are easy. In FoSSaCS 2002, volume 2303 of Lecture Notes in
Computer Science, pages 205–222. Springer-Verlag, 2002.

[18] N. Kobayashi. Model-checking higher-order functions. In Proceedings of PPDP 2009. ACM Press, 2009.

conference on Software engineering, pages 171–180, New York, NY,
USA, 2008. ACM.

[19] N. Kobayashi. TR EC S. http://www.kb.ecei.tohoku.ac.jp/~koba/trecs/, 2009.

Acknowledgments[20] N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages,
pages 416–428, 2009.

We would like thank Akihiko Tozawa and Yasuhiko Minamde fordiscussions and information about their work. We would also liketo thank Luke Ong and anonymous reviewers for useful comments.

[21] N. Kobayashi and C.-H. L. Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In Proceedingsof ICALP 2009, volume 5556 of Lecture Notes in Computer Science.
Springer-Verlag, 2009.
[22] N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal
mu-calculus model checking of higher-order recursion schemes. In
Proceedings of LICS 2009, pages 179–188. IEEE Computer Society
Press, 2009.
[23] N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multiparameter tree transducers and recursion schemes for program verification. A longer version, available from http://www.kb.ecei.
tohoku.ac.jp/~koba/papers/hmtt.pdf, 2009.
[24] M. Koganeyama, N. Tabuchi, and T. Tateishi. Reducing unnecessary conservativeness in access rights analysis with string analysis. In
APSEC ’07: Proceedings of the 14th Asia-Pacific Software Engineering Conference, pages 438–445, Washington, DC, USA, 2007. IEEE
Computer Society.
[25] S. Maneth, A. Berlea, T. Perst, and H. Seidl. XML type checking withmacro tree transducers. In Proceedings of the Twenty-fourth ACM
SIGACT-SIGMOD-SIGART Symposium on Principles of Database
Systems (PODS 2005), pages 283–294, 2005.
[26] S. Maneth and K. Nakano. Xml type checking for macro tree transducers with holes. In Programming Language Technologies for XML(PLAN-X), 2008.
[27] S. Maneth, T. Perst, and H. Seidl. Exact XML type checking in
polynomial time. In ICDT 2007, volume 4353 of Lecture Notes in
Computer Science, pages 254–268. Springer-Verlag, 2007.
[28] T. Milo, D. Suciu, and V. Vianu. Typechecking for XML transformers.
J. Comput. Syst. Sci., 66(1):66–97, 2003.
[29] Y. Minamide. Static approximation of dynamically generated web
pages. In Proceedings of the 14th international conference on World
Wide Web (WWW 2005), pages 432–441. ACM Press, 2005.
[30] M. Naik. A type system equivalent to a model checker. Master Thesis,
Purdue University.
[31] M. Naik and J. Palsberg. A type system equivalent to a model checker.
In ESOP 2005, volume 3444 of Lecture Notes in Computer Science,
pages 374–388. Springer-Verlag, 2005.
[32] C.-H. L. Ong. On model-checking trees generated by higher-orderrecursion schemes. In LICS 2006, pages 81–90. IEEE Computer
Society Press, 2006.
[33] J. Sawin and A. Rountev. Improving static resolution of dynamic classloading in java using dynamically gathered environment information.
Automated Software Engg., 16(2):357–381, 2009.
[34] A. Tozawa. XML type checking using high-level tree transducer.
In Functional and Logic Programming, 8th International Symposium(FLOPS 2006), volume 3945 of Lecture Notes in Computer Science,
pages 81–96. Springer-Verlag, 2006.
[35] R. Turner. An infinite hierarchy of term languages - an approach tomathematical complexity. In Proceedings of ICALP, pages 593–608,
1972.
[36] P. Wadler. Deforestation: Transforming programs to eliminate trees.
Theoretical Computer Science, 73(2):231–248, 1990.
[37] M. Wand. An algebraic formulation of the chomsky hierarchy. In
Category Theory Applied to Computation and Control, volume 25 ofLecture Notes in Computer Science, pages 209–213. Springer-Verlag,
1974.
[38] G. Wassermann and Z. Su. Static detection of cross-site scripting
vulnerabilities. In ICSE ’08: Proceedings of the 30th internationalA.

High-Level Tree Transducers and Linear
HMTTs

This section shows that high-level tree transducers [8] (which subsume macro tree transducers) can be transformed into a linear
HMTT. In essence, a (deterministic) high-level tree transducer isa higher-order function on trees (of sort o) defined by induction on
input trees (of sort i).
Let us fix the input alphabet ΣI = {a1 7→ k1 , . . . , an 7→ kn }.
A high-level tree transducer (N , ΣI , ΣO , R, F1 ) is a restriction of
HMTT, where the rewriting rules are only of the form:
F1 x ye1 → case(x, x
e1 .t1,1 , . . . , x
en .t1,n )···Fm x yem → case(x, x
e1 .tm,1 , . . . , x
en .tm,n )Here, x has sort i and it may not occur in
t1,1 , . . . , t1,n , . . . , tm,1 , . . . , tm,n . The sort of each non-terminalmust be of the form i → κ1 → · · · → κl → o, where i does
not occur in κ1 , . . . , κl . F1 has sort i → o (so, ye1 is the empty
sequence). Furthermore, input trees are restricted to finite ones. In
the original definition of higher-level tree transducers, there is afurther restriction that κ1 → · · · → κl → o must be “derived
types” [8]; We do not impose that restriction.
By using the tupling transformation [13], we can transform theabove HTT into the following linear HMTT:
S x → G x Proj
Proj y1 · · · ym → y1
G x k → case(x, x
e1 .H1 x
e1 k, . . . , x
en .Hn x
en k)
Hi x
ei k → G xi,1 (λy1,1 , . . . , y1,m .
G xi,2 (λy2,1 , . . . , y2,m . · · ·G xi,ki (λyki ,1 , . . . , yki ,m .
k [y1,1 /F1 x1,1 , . . . , yki ,m /Fm xki ,m ]t1,i· · · [y1,1 /F1 x1,1 , . . . , yki ,m /Fm xki ,m ]tm,i ) · · · ))(i = 1, . . . , n)Here, we have λ-abstractions for clarity; they can be removed bylambda-lifting. The term [y1,1 /F1 x1,1 , . . . , yki ,m /Fm xki ,m ]t1,idenotes the term obtained by replacing Fj x1,j in t1,i with y1,j .
(Note that by the restriction on the sorts of Fj , x1,j may occur
only as the first argument of Fj .) In the above rules, G x k computes a sequence of values of F1 x, . . . , Fm x and applies k tothem (so, G x k is intuitively the same as k (F1 x) · · · (Fm x)).
To compute G x k, it first performs a case analysis on x. If
x is ai eti , Hi is called. Hi eti k first computes the values of
F1 , . . . , Fm for t1,1 , . . . , ti,ki . It then computes F1 x, . . . , Fm x
(i.e., t1,i , . . . , tm,i ), and passes it to k.
The HMTT obtained by the above transformation is linear, andoutputs the same tree as the original HTT, given a finite tree as input. (That is not always the case if an input tree is infinite, since theevaluation order has been changed by the tupling transformation.)