Verification of Tree-Processing Programs via
Higher-Order Model Checking
Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi
Tohoku University

Abstract. We propose a new method to verify that a higher-order, treeprocessing functional program conforms to an input/output specification.
Our method reduces the verification problem to multiple verification
problems for higher-order multi-tree transducers, which are then transformed into higher-order recursion schemes and model-checked. Unlike
previous methods, our new method can deal with arbitrary higher-orderfunctional programs manipulating algebraic data structures, as long as
certain invariants on intermediate data structures are provided by a programmer. We have proved the soundness of the method and implemented
a prototype verifier.

1

Introduction

The model checking of higher-order recursion schemes [20], or higher-order model
checking for short, has been extensively studied recently. Ong [20] has shown thedecidability of higher-order model checking. Kobayashi [12, 13] then developed apractical model checking algorithm and applied it to program veriﬁcation. The
present work is an extension of that line of work, trying to apply higher-ordermodel checking to veriﬁcation of a wider range of higher-order programs.
From a programming language point of view, recursion schemes are termsof the simply-typed λ-calculus with recursion and tree constructors (but not
destructors). One can also encode ﬁnite data domains (such as booleans) byusing Church encoding. Based on this observation, Kobayashi [13] applied model
checking to resource usage veriﬁcation of simply-typed functional programs withrecursion, booleans, and resource primitives. The limitation of this approach
was that programs manipulating inﬁnite data domains such as lists and trees
could not be handled. To relax this limitation, in our previous work [15], wehave introduced higher-order multi-parameter tree transducers (HMTTs) as anextension of recursion schemes with tree destructors. HMTTs are a kind of treetransducers that take (possibly inﬁnite) input trees, which can be destructed,
and outputs a (possibly inﬁnite) tree. However, there still remains a gap between
HMTTs and ordinary functional programs that use recursive data structures
since HMTTs do not support intermediate data structures: an HMTT cannot
destruct trees constructed by the HMTT itself.
In this paper, we propose a veriﬁcation method for an extension of HMTTs
called EHMTTs. In essence, EHMTTs are higher-order, simply-typed functional

Thepresentwork

Functional
Program

EHMTTaddingcoercionannotations

Previouswork(POPL2010)
HMTT

HigherͲOrder
ModelChecking

HMTT

HigherͲOrder
ModelChecking

HMTT

HigherͲOrder
ModelChecking

Fig. 1. Overall Structure of EHMTT Verification Method

programs with recursion and tree primitives. Unlike our previous HMTTs [15],there is no fundamental restriction on tree constructors/destructors, except thatspecial annotations (called coercion) are required for destructing trees constructed in a program. Our method can check whether the output trees generated by a given EHMTT conform to a given output speciﬁcation whenever
the input trees conform to given input speciﬁcations. We can apply our method
to veriﬁcation of ordinary functional programs that manipulate algebraic data
structures by encoding them as trees and adding annotations to the programs.
The overall structure of our method is shown in Figure 1. A given EHMTT
veriﬁcation problem is reduced to multiple HMTT veriﬁcation problems, which
are then solved by an HMTT veriﬁcation method presented in our previous
work [15]. The HMTT veriﬁcation method further reduces the HMTT veriﬁcation problems to model checking problems of recursion schemes, which are
ﬁnally solved by Kobayashi’s higher-order model checker TRecS [12]. In thispaper, we have formalized the reduction from an EHMTT veriﬁcation problem
to HMTT veriﬁcation problems, and proved the soundness of the reduction.
Our veriﬁcation method is not complete, however, since the veriﬁcation problem
is undecidable in general. We have implemented a prototype veriﬁer and veriﬁed functional programs that manipulate XML and user-deﬁned recursive data
structures.
The rest of the paper is organized as follows. Section 2 presents some preliminary deﬁnitions and notations. In Section 3, we introduce EHMTTs. Section 4
formalizes our veriﬁcation method for EHMTTs. Section 5 reports on the experimental results. We compare our method with related work in Section 6, andconclude the paper with some remarks on future work in Section 7.

2

Preliminaries

We write dom(f ) for the domain of a map f , and f {x → v} for the map f  suchthat dom(f  ) = dom(f ) ∪ {x}, f  (x) = v and f  (y) = f (y) for y ∈ dom(f ) \ {x}.
We write X ∗ for the set of sequences of elements of X. We write  for theempty sequence, and v1 · · · vn for the sequence consisting of v1 , . . . , vn . We writes1 · s2 for the concatenation of sequences s1 and s2 . A sequence v1 · · · vn is often
abbreviated to v.
A ranked alphabet Σ is a map from a ﬁnite set of symbols to non-negative
integers. For each symbol a ∈ dom(Σ), Σ(a) denotes the arity of a. We writeAΣ to denote the largest arity of the symbols in dom(Σ). A Σ-labeled ranked
tree T is a map from a subset of {1, · · · , AΣ }∗ to dom(Σ) such that:– dom(T ) is preﬁx-closed, i.e. if π · i ∈ dom(T ), then π ∈ dom(T ); and– if T (π) = a, then {i | π · i ∈ dom(T )} = {1, . . . , Σ(a)}.

3Extended HMTTs

In this section, we introduce extended HMTTs (EHMTTs). From a programming
language point of view, an EHMTT is a simply-typed, call-by-name, higherorder functional program that takes possibly inﬁnite trees as input and outputs
a possibly inﬁnite tree. The main diﬀerences from ordinary functional programsis that trees are classiﬁed into input and output trees. Input trees can only
be destructed, and output trees can only be constructed in a program, as inother tree transducers. Special annotations (coerceL (·) introduced below) are
however provided to convert output trees to input trees, so that, unlike ordinary
tree transducers, trees constructed in a program can be destructed again in thesame program. Thus, the class of EHMTTs is actually Turing complete.
We ﬁx below a ranked alphabet Σ. We call elements of dom(Σ) terminal
symbols, and use the meta-variable a for them.
Definition 1 (EHMTT). An EHMTT P is a pair (D, S) where D is a set
1 = t1 , . . . , Fn x
n = tn }, and S is aof function definitions of the form {F1 xfunction name. Here, t ranges over the set of terms, given by:t ::= a | x | F | t1 t2 | case t of {ai yi ⇒ ti }ni=1 | coerceL (t) | genL
Here, L denotes a set of trees. An EHMTT (D, S) is well-sorted under K if
S : i → · · · → i → o ∈ K and  D : K is derivable by using the sort assignment
rules in Figure 2. An HMTT is an EHMTT that does not contain coerceL (t).
In the ﬁgure, the sorts i and o describe input and output trees respectively.
The sort κ1 → κ2 denotes functions that take a tree or tree function of sort κ1
and return a tree or tree function of sort κ2 . κ → o and x
:κ are shorthandforms of κ1 → · · · → κk → o and x1 : κ1 , . . . , xk : κk respectively. We consider
only well-sorted EHMTTs below.

Syntax of Sorts:
κ ::= i | o | κ1 → κ2

Sort Assignment Rules:

K  F : K(F ) (T-Fun)Ka:o· · → o} → o| → ·{zΣ(a)Kt:iK, yei : ei  ti : o(for all i = 1, . . . , N )(T-Con)K  genL : iKt:oK, x : κ  x : κ (T-Var)
K  t 1 : κ1 → κ2
K  t 2 : κ1
K  t 1 t 2 : κ2

K  coerceL (t) : i(T-App)(T-Case)K  case t of {ai yei ⇒ ti }ni=1 : o(T-Gen)(T-Coerce)

e1 → o, . . . , Fn : κ
e1 → o}K = {F1 : κei  ti : o (for each i)K, xei : κ
 {F1 xe1 = t1 , . . . , Fn x
en = tn } : K(T-Def)Operational Semantics
t (extended terms) ::= · · · | a | o2i(t) | assertL (t)E (evaluation contexts) ::= [ ] | a t1 · · · tj−1 E tj+1 · · · tΣ(a)L| case E of {ai yei ⇒ ti }ni=1 | o2i(E) | assert (E)

F x
e=t∈D
E[F e
t] −→P E[[e
t/e
x]t]

(E-App)e yi ]ti ]t of {ai yei ⇒ ti }nE[case ai ei=1 ] −→P E[[t/e(E-Case)a ∈ {a1 , . . . , an }E[case a et of {ai yei ⇒ ti }ni=1 ] −→P E[fail]a L 1 · · · Ln ⊆ L
E[genL ] −→P E[a genL1 . . . genLn ](E-Case-Fail)(E-Gen)E[coerceL (t)] −→P assertL (t)(E-Coerce-Assert)

E[coerceL (t)] −→P E[o2i(t)](E-Coerce-Input)t)]t)] −→P E[ai o2i(eE[o2i(ai e(E-Input)t⊥ ∈ L⊥L

assert (t) −→P Error(E-Assert-Error)

Fig. 2. Sort Assignment Rules and Call-by-Name Operational Semantics

The term case t of {ai yi ⇒ ti }ni=1 is reduced to [ui /
yi ]ti if t evaluates toai u
i . If t does not match any pattern, the term evaluates to a special terminal
symbol fail.1 The term coerceL (t) asserts that the tree generated by t belongs
to a set L of trees, and converts the tree to an input tree. genL generates anelement of L non-deterministically.
Example 1. Consider the EHMTT Prev = (D, Reverse), where D consists of:Reverse x = case x of e ⇒ e∗ ∗| a x ⇒ Append (coerceb a e (Reverse x )) (a e)∗| b x ⇒ Append (coerceb e (Reverse x )) (b e).
Append x y = case x of e ⇒ y| a x ⇒ a (Append x y)| b x ⇒ b (Append x y).
Prev takes a tree of the form am (bn (e)) as input, and outputs a tree bn (am (e)).
∗ ∗∗The coercions coerceb a e (·) and coerceb e (·) assert that their arguments belong to {bm (an (e)) | m, n ≥ 0} and {bm (e) | m ≥ 0} respectively, and convert them to input trees. Note that Reverse and Append have sorts i → o andi → o → o respectively, so that Reverse x returns an output tree. 
Figure 2 shows the formal semantics of the language. In the semantics, theset of terms are extended as follows. An underlined symbol a denotes an input
tree constructor (which, by the restriction of EHMTT, occurs only at run-time,
not in source programs). o2i(t) and assertL (t) are used to deﬁne the semantics
of coerceL (t): the former converts an output tree to an input tree, and the latter
asserts that the tree generated by t belong to L. In the rule E-Assert-Error,t⊥ is a ﬁnite (Σ ∪ {⊥ → 0})-labeled ranked tree, deﬁned by: ⊥a t1 · · · t ⊥⊥n (if t = a t1 · · · tn )t =⊥(otherwise)T  ∈ L}, where T
L⊥ is the set {T | T

T by replacing some nodes of T  with ⊥.

T  means that T is obtained from

Remark 1. Note that EHMTT is call-by-name. This is because our veriﬁcation
method is based on the model checking of higher-oder recursion schemes, whose
semantics is call-by-name. To deal with call-by-value programs, it suﬃces toapply CPS transformation before applying our veriﬁcation method. The reasons
why we allow inﬁnite trees as inputs and outputs for EHMTTs are as follows.
First, we would like to verify programs that manipulate not only ﬁnite but also
inﬁnite data structures (such as streams). Secondly, we would like to model a1

Thus, verification of the absence of pattern match errors can be encoded as a problemof checking that the tree generated by EHMTT does not contain fail, which is an
instance of EHMTT verification problems considered below.

program that contains non-deterministic branches (which is typically obtainedby abstracting branching information of a user program) as an EHMTT thatgenerates a single tree describing all the possible outputs of the program. In
that case, even if a program manipulates only ﬁnite data structures, the outputof the EHMTT can be an inﬁnite tree.
The goal of our veriﬁcation is to check that a given EHMTT conforms to agiven speciﬁcation on input and output. As EHMTTs manipulate inﬁnite trees,
we use top-down tree automata called trivial automata (which are Büchi tree
automata with a trivial acceptance condition) as speciﬁcations (as well as forannotations L in coerceL (·) and genL ).
Definition 2 (trivial automaton). A trivial automaton M is a quadruple(Σ, Q, Δ, q0 ), where:– Σ is a ranked alphabet.
– Q is a finite set of states.
– Δ is a finite subset of Q × dom(Σ) × Q∗ called a transition relation suchthat if (q, a, q) ∈ Δ, then the length of the sequence q is Σ(a).
– q0 is a state called an initial state.
A Σ-labeled ranked tree T is accepted by M if there is a Q-labeled tree R suchthat:
– dom(T ) = dom(R).
– For any π ∈ dom(R), (R(π), T (π), R(π · 1) · · · R(π · Σ(T (π)))) ∈ Δ.
– R() = q0 .
We write L(M) for the set of Σ-labeled ranked trees accepted by M.
When restricted to ﬁnite trees, the class of languages recognized by trivial automata is equivalent to the class of regular tree languages.
Example 2. Recall Example 1. A trivial automaton for accepting b∗ a∗ e is deﬁnedby (Σ, {q0 , q1 }, Δ, q0 ), where:Σ = {a → 1, b → 1, e → 0}
Δ = {(q0 , b, q0 ), (q0 , a, q1 ), (q0 , e, ), (q1 , a, q1 ), (q1 , e, )}We now formalize our veriﬁcation problem:
Definition 3. Given an EHMTT P = (D, S) and trivial automata M1 , . . . , Mk ,M = (Σ, Q, Δ, q0 ), we write |= (P, M1 , . . . , Mk , M) if for all T1 ∈ L(M1 ), . . . ,Tk ∈ L(Mk ),1. S T1 · · · Tk −→∗P t implies t⊥ ∈ L(M⊥ ), and
2. S T1 · · · Tk −→∗P Error.
Here, M⊥ is the trivial automaton (Σ ∪ {⊥ → 0}, Q, Δ ∪ {(q, ⊥, ) | q ∈ Q}, q0 ).
An EHMTT verification problem (P, M1 , . . . , Mk , M) is the problem to checkthat |= (P, M1 , . . . , Mk , M).

The ﬁrst condition of an EHMTT veriﬁcation problem says that given input treesthat conform to the input speciﬁcation, the EHMTT generates a valid tree.2 The
second condition means that the EHMTT in fact never causes a coercion error.
In [15], we have presented a (sound but incomplete) method for the restrictedcase (which we call HMTT verification problems) where P is an HMTT (i.e., forthe case where P does not contain coerceL (·)). In the next section, we reduce
an EHMTT veriﬁcation problem to HMTT veriﬁcation problems.

4

Verification Method for EHMTTs

We now present a method for reducing an EHMTT veriﬁcation problem to
HMTT veriﬁcation problems (which can then be solved by the previous method[15]). The idea is to reduce each of the two conditions in Deﬁnition 3 to HMTT
veriﬁcation problems.
Let (P, M1 , . . . , Mk , M) be a given EHMTT veriﬁcation problem, and suppose that P contains m occurrences of coercions: coerceL1 (·), . . . , coerceLm (·).
We construct HMTTs P A , P B1 , . . . , P Bm such that:– P A approximates the output of P, by assuming that coercions never fail.
– P Bi approximates all the possible arguments of coerceLi (·).
Then, the veriﬁcation problem (P, M1 , . . . , Mk , M) can be reduced to m + 1
HMTT veriﬁcation problems: (P A, M1 , . . . , Mk , M), (P B1, M1 , . . . , Mk , B(L1 )),. . . , (P Bm , M1 , . . . , Mk , B(Lm )) (where B(L) is an automaton for accepting trees
representing subsets of L; see Section 4.2 below). Sections 4.1 and 4.2 below show
the constructions of P A and P Bi respectively.

4.1

Construction of P A

Let P A be the HMTT obtained by just replacing every occurrence of coerceLi (·)
in P with genLi . Then, P A approximates the output of P, assuming that no
coercion error occurs.
Theorem 1. Let P = (D, S) be an EHMTT such that |= (P A , M1 , . . . , Mk , M)
holds. For any T1 ∈ L(M1 ), . . . , Tk ∈ L(Mk ), if S T1 · · · Tk −→∗P Error andS T1 · · · Tk −→∗P t, then t⊥ ∈ L(M⊥ ).
A proof is given in Appendix A.
2

Because of the presence of ⊥, only safety properties are guaranteed; there is no
guarantee that the EHMTT eventually generates a tree that belongs to L(M).

A
Example 3. Recall Prev in Example 1. Prev
is (D, ReverseA ) where D is givenby:ReverseA xA = case xA of e ⇒ e∗ ∗| a xA ⇒ AppendA genb a e (a e)∗| b xA ⇒ AppendA genb e (b e)AppendA xA y A = case xA of e ⇒ y A| a xA ⇒ a (AppendA xA y A )| b xA ⇒ b (AppendA xA y A )4.2

Construction of P Bi

The construction of P Bi is more involved, for the following reasons.
1. Given an input, P may invoke coerceLi (·) more than once. For example,∗
given b(b(e)) as input, Prev in Example 1 invoke coerceb e (·) twice, with
diﬀerent parameters e and b(e). Thus, P Bi should approximate the set oftrees that are passed to coerceLi (·).
2. How a function invokes coerceLi (·) may depend on its arguments. For example, consider a higher-order function F deﬁned by F g x = g(x). Obviously,
how coerceLi (·) is invoked during evaluation of F t1 t2 depends on t1 andt2 .
To address the ﬁrst issue, we represent a (possibly inﬁnite) set of trees bya single (possibly inﬁnite) tree. We use special terminal symbols br and emp,
which represent the set union and an empty set respectively. For example, theset {e, b(e)} is represented by br e (b(e)). P Bi outputs such a tree representationof (an over-approximation of) the set of trees passed to coerceLi (·).
To address the second issue, we duplicate each parameter x of a function
into xA and xB . The parameter xA is used to compute (an approximation of)
the original value of x, while the parameter xB computes (an approximationof) the set of trees passed to coerceLi (·) during evaluation of x. For example,
F g x = g(x) is transformed to: F B g A g B xA xB = g B xA xB . Here, F B
computes an approximation of the set of trees passed to coerceLi (·) by callingg B with duplicated parameters xA and xB .
We give below more concrete examples to explain the construction of P Bi .
Example 4. Recall Prev in Example 1. For the ﬁrst coercion coerceL1 (Reverse x )B1:
(where L1 = b∗ a∗ e), we construct the following HMTT Prev

ReverseB xA xB =br xB (case xA of e ⇒ emp∗∗| a xA ⇒ AppendB genb a e (br (ReverseA xA )(ReverseB xA emp))
A|bx(a e) emp∗
⇒ Append genb e (ReverseB xA emp)
B(b e) emp)
B

A

Append x
B

B

x y

A

y =

A

br x (case xBof e ⇒ y B| a xA ⇒ AppendB xA emp y A y B| b xA ⇒ AppendB xA emp y A y B )As mentioned above, the parameters of Reverse and Append have been duplicated. When Reverse t is called in Prev , there are two cases where coerceL1 (·)
may be called: the case where t contains coerceL1 (·) and it is called when t isevaluated by the case statement (note that our language is call-by-name); andthe case where coerceL1 (·) is called in a case branch. In the body of the deﬁnition of ReverseB , the part xB approximates the set of trees passed to coerceL1 (·)
in the former case, and the part case xA of · · · approximates the set of trees
for the latter case.
In the clause for a(xA ), AppendB is used to compute an approximation of
the set of trees passed to coerceL1 (·). The ﬁrst and third parameters approximate the values of the original parameters of Append. The second parameter(br (ReverseA xA ) (ReverseB xA emp)) approximates the set of trees passed tocoerceL1 (·) during the computation of coerceL1 (Reverse x ). Here, there are
two cases where coercion can occur: (i) the value of Reverse x is computed andpassed to coerceL1 (·) and (ii) coerceL1 (·) is invoked during the computation ofReverse x . The parts (ReverseA xA ) and (ReverseB xA emp) cover the former
and the latter cases respectively. In the latter, the second parameter of (ReverseB
is an empty set, as the trees passed to coerceL1 (·) during the computation ofx are already covered by xB .
The reduction works similarly for EHMTTs with higher-order functions.
Example 5. Let us consider a higher-order version of the list reverse program:Reverse x = Reverseh Append x
Reverseh f x = case x of e ⇒ e∗∗| a x ⇒ f (coerceb a e (Reverseh f x )) (a e)∗| b x ⇒ f (coerceb e (Reverseh f x )) (b e)∗∗

We get the following HMTT for the ﬁrst coercion coerceb a e (Reverseh f x ):ReverseB xA xB = ReversehB AppendA AppendB xA xB
ReversehB f A f B xA xB =br xB (case xA of e ⇒ emp∗∗| a xA ⇒ f B genb a e (br (ReversehA f A xA )(ReversehB f A f B xA emp))
A

|bx

⇒f

B

(a e) emp∗
genb e (ReversehB f A f B xA emp)(b e) emp)

Here, AppendA is the one obtained in Example 3. Note that ReversehB requires
an additional argument f B , which generates all the trees passed to the coercion
by f . 
Formally, given an EHMTT P = (D, S), P Bi is (Bi (D), S) where:
Bi (D) = {S x1 · · · xk = S Bi x1 emp · · · xk emp}∪
Bi
Bi
Bi
Bi
A
{aBi xA
1 x1 · · · xΣ(a) xΣ(a) = br x1 · · · xΣ(a) | a ∈ dom(Σ)}∪
A A
A{F x1 · · · xn = A(t) | F x1 · · · xn = t ∈ D}∪
Bi
A Bi{F Bi xA
1 x1 · · · xn xn = Bi (t) | F x1 · · · xn = t ∈ D}
Bi (x) = xBi
Bi (F ) = F Bi
Bi (a) = aBi
Bi (t1 t2 ) = Bi (t1 ) A(t2 ) Bi (t2 )Bi (case t of {aj yj ⇒ tj }nj=1 ) =br Bi (t) (case A(t) of {aj yjA ⇒ [emp/yjBi ]Bi (tj )}nj=1 )L
Bi (gen ) = emp 
br A(t) Bi (t) (if i = j)
Bi (coerceLj (t)) =(otherwise)
Bi (t)
Here, A(t) is the term obtained by replacing every coercion coerceL (·), variable
x, and function name F in t with genL , xA , and F A respectively. br t1 · · · tn
stands for br t1 (br t2 (br · · · (br tn−1 tn ))) if n ≥ 2, t1 if n = 1, and emp if
n = 0. For each terminal a ∈ dom(Σ), we obtain the new function aBi thatgenerates all the trees passed to the i-th coercion by the actual arguments of a.
Given a trivial automaton M(Li ) = (Σ, Q, Δ, q0 ) for accepting Li , the output
speciﬁcation for P Bi is the trivial automaton B(Li ) = (Σ  , Q, Δ , q0 ), where:Σ  = Σ ∪ {br → 2, emp → 0}
Δ = Δ ∪ {(q, br, q · q), (q, emp, ) | q ∈ Q}
The following theorem states the correctness of the construction of P Bi . See
Appendix B for the proof.
Theorem 2. Let P = (D, S) be an EHMTT and suppose that the coercions in P
are coerceL1 (·), . . . , coerceLm (·). If |= (P Bi , M1 , . . . , Mk , B(Li )) holds for eachi ∈ {1, . . . , m}, for any T1 ∈ L(M1 ), . . . , Tk ∈ L(Mk ), S T1 · · · Tk −→∗P Error.

Our reduction from EHMTT to HMTT veriﬁcation problems is incomplete,
however, i.e. there is a case that an EHMTT satisﬁes a given speciﬁcation, but
the generated HMTTs do not satisfy the required properties. There are two main
reasons for this.
– Coercion annotations may not be good enough. For example, if coercions areannotated with the empty language ∅, the derived HMTTs obviously do notsatisfy the property. Actually, there may be no good way to annotate coercions. For example, consider the EHMTT S x = Zip (coerceL (Unzip x)),where Unzip takes an input sn z that encodes a natural number n and returns an output tree pair (sn z) (sn z), and Zip takes an input tree of theform pair (sn1 z) (sn2 z) and outputs fail if and only if n1 = n2 . To verify
that S x never outputs fail for any x ∈ {sn z | n ≥ 0}, we need the coercion
annotation L = {pair (sn z) (sn z) | n ≥ 0}, which cannot be expressed bya trivial automaton or a regular language. As another example, consider thefollowing variant of a reverse function:Reverse x = case x of e ⇒ e| cons z x ⇒ Append (coerceL (Reverse x )) (cons z e)
Append x y = · · ·Here, we have used a list-like representation of sequences of a, b. In this case,the appropriate annotation depends on the value of z (L should be b∗ a∗ e if z
is a while b∗ e if z is b), which cannot be expressed in our language. One way
to avoid this problem is to duplicate a part of the code so that appropriate
annotations can be inserted.
– The output speciﬁcation B(Li ) for P Bi is too restrictive. When the automaton for accepting Li is non-deterministic, B(Li ) does not accept all the tree
representations of subsets of Li . This problem can easily be remedied, however, by using a more elaborate construction of B(Li ), hence not a fundamental limitation.
Our overall method is also incomplete because of the incompleteness of the
HMTT veriﬁcation method [15] (unsurprisingly, as the HMTT veriﬁcation problem is undecidable in general).

5

Experiments

We have implemented the reduction method from an EHMTT veriﬁcation problem to HMTT veriﬁcation problems presented in Section 4. For solving the
HMTT veriﬁcation problems, we adopted an HMTT veriﬁcation method in [15]and Kobayashi’s higher-order model checker TRecS [12].
Table 1 shows the results of preliminary experiments. The column “O” shows
the order of each EHMTT which is the largest order of the sorts of the functions.
The order of a sort is deﬁned by:order (i) = order (o) = 0

order (κ1 → κ2 ) = max (order (κ1 ) + 1, order (κ2 ))Programs
O C R S SumR SumS QI QO TRed Y/N TMC
Reverse1 2 3 3223
222 4 21Y
4
Isort
1 1 4 2916
115 3 21Y
3Msort
2 4 8 131
88 1,731 3 2
2Y 224
HomRep-Rev 4 1 12 90
43362 6 2
1
Y 31
Split
2 1 6 12633
572 23 9
3Y 132
Bib2Html
2 1 13 493
126 2,303 59 50
52
Y 52
XMarkQ12 1 12 454
118 2,136 99 23
29
Y 168
XMarkQ2
1 2 9 461
207 3,797 99 477
Y 92
Gapid-Html 3 1 17 374
75 1,642 16 72
Y 112
JWIG-guess 2 1 6 465
98 2,331 64 50 588
Y 50
JWIG-cal1 2 12 475
222 4,045 60 50
72
Y 73
MinCaml-K
2 8 19 605
563 16,117 5 3
5Y 647
Split’
2 1 6 12633
572 23 9
3N 27
JWIG-guess’ 2 1 6 465
98 2,331 64 50 586
N 49
JWIG-cal’1 2 12 475
222 4,045 60 50
2
N 55
Table 1. Experimental Results

The column “C” shows the number of coercions in each EHMTT. The columns“R” and “S” are the number of rules and the size of each EHMTT respectively.
The size of an EHMTT is measured by the number of symbols occurring in theright-hand side of the rewriting rules. “SumR ” and “SumS ” respectively are thesum of the numbers of the rules and the sum of the sizes of all HMTTs derived from each EHMTT. “QI ” and “QO ” respectively show the numbers of thestates of trivial automata for the input and output speciﬁcations. The column“TRed ” shows the elapsed time, in milliseconds, of reduction from an EHMTT
veriﬁcation problem to HMTT veriﬁcation problems. The column “Y/N” indicates whether each EHMTT was proved correct (Y) or rejected (N). The column“TMC ” shows the total running time of the higher-order model checker TRecS
to solve all the HMTT veriﬁcation problems derived from each EHMTT.
The program Reverse is the same as the one presented in the paper. Isort
performs insertion sort on the lists encoded as linear trees over Σ = {a →
1, b → 1, e → 0}. Msort performs merge sort instead of insertion sort on thesame linear trees. HomRep-Rev takes a word homomorphism h over linear trees(a + b)∗ e, a number n and a word w ∈ (a + b)∗ e, and produces the reverse of
the image hn (w). We let h = {a → bb, b → a} and veriﬁed that if n is an evennumber and w ∈ a∗ b∗ e, then the reversed image is in b∗ a∗ e. The program Splitpresented in Figure 3 is taken from sample programs of CDuce [2], a higher-order
XML-oriented functional language. Split takes a list of persons, and splits it
into two lists of men and women. Bib2Html also simulates a CDuce programthat transforms a list of bibliography into an XHTML. XMarkQ1 and XMarkQ2
taken from Q1 and Q2 of XMark benchmark suite [21] simulate simple XQuery
queries. The program Gapid-Html is a composition of Tozawa’s high-level treetransducers [22]. It takes a document of the following DTD:

type Doctype Preface
type Header
type P
type Div
type Note
type A= doc[Preface, (Div|P|Note)*]= preface[Header, P*]= header[A*]= p[A*]= div[(Div|P|Note|A)*]= note[(P|A)*]= a[A*]

and another tree as inputs. It checks whether the children of each node of the
document are empty, and if so, replaces the empty children with a “hole”. The
program then inserts the given tree into the holes. The program ﬁnally transforms the result to an XHTML. The programs JWIG-guess and JWIG-cal aretaken from sample programs of JWIG (http://www.brics.dk/JWIG/), a programming language for interactive Web services. A main feature of JWIG is
document templates. For example, the following document template represents
an HTML document with a hole named x:<html><head><title> ... </title></head><body><[x]></body></html>We can instantiate the template by substituting another document or templatefor x. In EHMTTs, the template can be encoded as the following rule for afunction T with an argument x:
T x → html (head (title (text leaf leaf) leaf) (body x leaf)) leaf
The program JWIG-guess is a number guessing game. The program JWIG-cal
is a web-based calendar service. MinCaml-K simulates the K-normalization routine of the MinCaml compiler (http://min-caml.sourceforge.net/index-e.
html). Finally, Split’, JWIG-guess’ and JWIG-cal’ are respectively the sameas Split, JWIG-guess and JWIG-cal except that they involve wrong coercions
which lead to an Error to see that programs with wrong coercions are rejected.
These programs (except for Reverse, Isort, Msort and HomRep-Rev) are manually translated from original source codes to EHMTTs.
All the valid programs have been proved correct by our veriﬁcation method
despite its incompleteness, while wrong programs are correctly rejected. The
number of coercions (thus the number of annotations required by our method)is much smaller than the number of rules (functions) in all cases. Though thesenumbers depend on the particular encoding, this result witnesses that our veriﬁcation method usually requires fewer annotations than existing veriﬁcation
methods [2, 4, 9], which require type annotations for every function deﬁnition.
Further comparison with the existing methods on this point is given in Section 6.
All the programs were proved correct within 1 second. From this, we can
expect that our method can verify non-trivial programs reasonably fast despite
the high time complexity (n-EXPTIME complete, where n is the order) of higherorder model checking.

Split x = case x of person g n c =>case c of children cs => case g of gender gend =>Let gend n (coerce qPair (MakePair cs nil nil))
Let gend n x = case gend of
m => Make man (Copy n) x
| f => Make woman (Copy n) x
MakePair ps ms fs = case ps of nil => pair ms fs| cons p sib => case p of person g n c => case g of gender gend =>case gend of
m => MakePair sib (cons (person (gender m) (Copy n) (Copy c)) ms) fs|f => MakePair sib ms (cons (person (gender f) (Copy n) (Copy c)) fs)
Make tag name sdpair = case sdpair of pair s d =>tag name (sons (RevMap Split s nil))(daughters (RevMap Split d nil))
RevMap f l ac =case l of nil => ac | cons x xs => RevMap f xs (cons (f x) ac)
Fig. 3. Split

6

Related WorkAs shown in Section 1, our veriﬁcation method is based on recent advances onhigher-order model checking [1, 11, 14, 20]. Ong [20] has proven the decidability ofthe model checking problem for recursion schemes, and Kobayashi has developedand implemented a type-based model checking algorithm [14].
As we have shown in Section 5, our EHMTT veriﬁcation method can be applied to veriﬁcation of functional programs that manipulate various data structures such as strings, lists, trees, XML, and user-deﬁned recursive data structuresby encoding them as trees and adding coercion annotations to the programs. We
compare our method with existing veriﬁcation methods below.
Reﬁnement types [4, 7] can be used for veriﬁcation of functional programs
that manipulate user-deﬁned recursive data structures. The original reﬁnement
type system [7] uses a naı̈ve least ﬁxed-point algorithm to infer the most precise
reﬁnement types of functions, and does not seem to scale for higher-order functions. Another reﬁnement type system proposed by Davies [4] requires users towrite type annotations for each function. For example, for Prev in Example 1,
Reverse and Append need to be annotated with the following intersection types:
Reverse : (a∗ b∗ e → b∗ a∗ e) ∧ (b∗ e → b∗ e)
Append : (b∗ a∗ e → a∗ e → b∗ a∗ e) ∧ (b∗ e → b∗ e → b∗ e)∗ ∗In contrast, our method requires only the annotations coerceb a e (Reverse x )∗and coerceb e (Reverse x ) in the deﬁnition of Reverse. As in this case, we
expect that coercion annotations required in our approach tends to be simpler
than reﬁnement type declarations. Because of the limitation of our approach
discussed at the end of Section 4, however, it may be useful to combine both
approaches.

Several research groups have proposed typed XML processing languages [2, 9].
Their type systems can be used for veriﬁcation of XML processing programs. As
in the Davies’s reﬁnement type system, these type systems require type annotations for each function for type checking. Thus, our method can be used as analternative for a veriﬁcation purpose. Meanwhile their type systems support advanced programming features such as parametric polymorphism [8] and regularexpression pattern matching [10]. Extensions of our method with these features
are left for future work. While the type checking of the XML processing languages are incomplete, extensive work has been done on complete type checkingof various tree transducers [17, 18]. They are not Turing-complete, however, andthus less expressive than our EHMTTs. As shown in [16], ordinary macro andhigh-level tree transducers [5, 6] are subsumed by linear HMTTs, for which our
EHMTT veriﬁcation method is sound and complete.
String analysis [3, 19] can verify programs that manipulate strings by approximating a string-processing program as a regular or a context-free grammar. In
contrast, our method is more precise since we can naturally model programs as
EHMTTs, which are strictly more expressive than context-free grammars.
Our approach of reducing EHMTT veriﬁcation to simpler veriﬁcation problems based on coercion annotations is a reminiscent of program veriﬁcation techniques for imperative languages based on veriﬁcation condition generation fromloop invariants: coercion annotations are invariants, and generated HMTT veriﬁcation problems can be considered veriﬁcation conditions. The main diﬀerences
are that our target is a higher-order functional language and that not all recursions (or loops) need to be annotated with invariants.

7

Conclusion

We have proposed a veriﬁcation method for tree-processing programs based on
reduction to higher-order model checking, and shown its eﬀectiveness through experiments. We plan to investigate techniques for inferring coercion annotations,which would enable fully automatic veriﬁcation of tree-processing programs. If
the derived HMTTs are ordinary macro or high-level tree transducers [5, 6], annotations can indeed be inferred by the inverse inference technique. For general
EHMTTs, we plan to apply techniques of machine learning. Addressing the limitations discussed at the end of Section 4 is also left for future work.
Acknowledgment
We would like to thank anonymous referees for useful comments.

References
1. Aehlig, K., de Miranda, J.G., Ong, C.H.L.: The monadic second order theory oftrees given by arbitrary level-two recursion schemes is decidable. In: TLCA ’05.
LNCS, vol. 3461, pp. 39–54. Springer (2005)

2. Benzaken, V., Castagna, G., Frisch, A.: CDuce: an XML-centric general-purpose
language. In: ICFP ’03. pp. 51–63. ACM (2003)
3. Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: SAS ’03. LNCS, vol. 2694, pp. 1–18. Springer (2003)
4. Davies, R.: Practical refinement-type checking. Ph.D. thesis, Carnegie Mellon University (2005), chair-Pfenning, Frank
5. Engelfriet, J., Vogler, H.: Macro tree transducers. Journal of Computer and System
Sciences 31(1), 71–146 (1985)
6. Engelfriet, J., Vogler, H.: High level tree transducers and iterated pushdown treetransducers. Acta Informatica 26(1/2), 131–192 (1988)
7. Freeman, T., Pfenning, F.: Refinement types for ML. In: PLDI ’91. pp. 268–277.
ACM (1991)
8. Hosoya, H., Frisch, A., Castagna, G.: Parametric polymorphism for XML. ACM
Transactions on Programming Languages and Systems 32(1), 1–56 (2009)
9. Hosoya, H., Pierce, B.C.: XDuce: A statically typed XML processing language.
ACM Transactions on Internet Technology 3(2), 117–148 (2003)
10. Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. In: ICFP
’00. pp. 11–22. ACM (2000)
11. Knapik, T., Niwinski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In:
FoSSaCS ’02. LNCS, vol. 2303, pp. 205–222. Springer (2002)
12. Kobayashi, N.: Model-checking higher-order functions. In: PPDP ’09. pp. 25–36.
ACM (2009)
13. Kobayashi, N.: Types and higher-order recursion schemes for verification of higherorder programs. In: POPL ’09. pp. 416–428. ACM (2009)
14. Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus
model checking of higher-order recursion schemes. In: LICS ’09. pp. 179–188. IEEE
(2009)
15. Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: POPL ’10. pp. 495–508.
ACM (2010)
16. Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. An extended version, available
from http://www.kb.ecei.tohoku.ac.jp/∼koba/papers/hmtt.pdf (2010)
17. Maneth, S., Berlea, A., Perst, T., Seidl, H.: XML type checking with macro treetransducers. In: PODS ’05. pp. 283–294. ACM (2005)
18. Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. Journal ofComputer and System Sciences 66(1), 66–97 (2003)
19. Minamide, Y.: Static approximation of dynamically generated web pages. In:
WWW ’05. pp. 432–441. ACM (2005)
20. Ong, C.H.L.: On model-checking trees generated by higher-order recursion
schemes. In: LICS ’06. pp. 81–90. IEEE (2006)
21. Schmidt, A., Waas, F., Kersten, M., Carey, M.J., Manolescu, I., Busse, R.: XMark:a benchmark for XML data management. In: VLDB ’02. pp. 974–985. VLDB Endowment (2002)
22. Tozawa, A.: XML type checking using high-level tree transducer. In: FLOPS ’06.
LNCS, vol. 3945, pp. 81–96. Springer (2006)

Appendix
A

Proof of Theorem 1

To prove Theorem 1, we use a variant =⇒ of the evaluation relation −→ in Figure 2 which adopts the following rule instead of E-Coerce-Input and E-Input:t =⇒∗P tt⊥ ∈ L⊥E[coerceL (t)] =⇒P E[t⊥ ](E-Coerce)

Lemma 1. If S T1 · · · Tk −→∗P Error and S T1 · · · Tk −→∗ t, then S T1 · · · Tk =⇒∗t is derivable for some t such that t⊥ = t⊥ .
The term translation A(t) is formally deﬁned by:
A(a) = a A(x) = xA A(F ) = F A A(t1 t2 ) = A(t1 ) A(t2 )A(case t of {ai yi ⇒ ti }ni=1 ) = case A(t) of {ai yiA ⇒ A(ti )}ni=1

A(genL ) = genLA(coerceL (t)) = genL

A(a) = a

We prepare lemmas for Theorem 1.
Lemma 2. A([t /x]t) = [A(t )/xA ]A(t)Lemma 3. If t =⇒ t is derivable without using E-Coerce-Assert, thenA(t) =⇒∗ A(t ) holds.
Proof. We prove the lemma by case analysis for the last rule used to derivet =⇒ t :E-App
We havet = E[F t]t = E[[t/x]t ]F x
 = t ∈ D
We get F A x
A = A(t ) ∈ A(D). We haveA(t) = A(E)[A(F t)]A= A(E)[F A(t)]=⇒ A(E)[[A(t)/
xA ]A(t )](By E-App)= A(E)[A([t/x]t )]
(By Lemma 2)= A(E[[t/x]t ])= A(t )E-CaseWe havet = E[case ai t of {ai yi ⇒ ti }ni=1 ]t/
yi ]ti ]t = E[[We obtain
A(t) = A(E)[A(case ai t of {ai yi ⇒ ti }ni=1 )]t) of {ai yiA ⇒ A(ti )}ni=1 ]= A(E)[case ai A(=⇒ A(E)[[A(t)/yiA ]A(ti )](By E-Case)= A(E)[A([t/yi ]ti )](By Lemma 2)= A(E[[t/
yi ]ti ])= A(t )E-Case-FailWe havet = E[case a t of {ai yi ⇒ ti }ni=1 ]t = E[fail]a ∈ {a1 , . . . , an }We obtain

A(t) = A(E)[A(case a t of {ai yi ⇒ ti }ni=1 )]= A(E)[case a A(t) of {ai yiA ⇒ A(ti )}ni=1 ]=⇒ A(E)[fail](By E-Case-Fail)= A(E[fail])= A(t )E-Gen
We havet = E[genL ]t = E[a genL1 . . . genLn ]a L1 · · · Ln ⊆ L

A(t) = A(E)[A(genL )]= A(E)[genL ]=⇒ A(E)[a genL1 . . . genLn ]= A(E[a gen= A(t )L1. . . gen

Ln])

(By E-Gen)

E-Coerce
We havet = E[coerceL (t1 )]t = E[t⊥2]
t1 =⇒∗ t2
⊥
t⊥
2 ∈L

A(t) = A(E)[A(coerceL (t ))]= A(E)[genL ](By E-Gen and gen∅ = ⊥)=⇒∗ A(E)[t⊥2]= A(E[t⊥2 ])= A(t )E-Coerce-Assert
This case is impossible
E-Assert-Error
This case is impossible
We now prove Theorem 1.
Proof of Theorem 1 Assume that S T1 · · · Tk −→∗ Error and S T1 · · · Tk −→∗ t.
By Lemma 1, S T1 · · · Tk =⇒∗ t is derivable for some t such that t⊥ = t⊥ .
If the derivation of S T1 · · · Tk =⇒∗ t uses T-Coerce-Assert, we have t⊥ =t⊥ = ⊥ ∈ L(M⊥ ). Otherwise, by Lemma 3, we have S A T1 · · · Tk =⇒∗ A(t ).
Thus, we get t⊥ = t⊥ = A(t )⊥ ∈ L(M⊥ ). 

B

Proof of Theorem 2

Lemma 4. If S T1 · · · Tk =⇒P Error, then S T1 · · · Tk −→∗P Error.
The term translation Bi (t) is extended with:Bi (a) = aBi

Bi (assertL (t)) = Bi (t)Lemma 5. Bi ([t /x]t) = [A(t )/xA , Bi (t )/xBi ]Bi (t).
We write t1 ⊆ t2 if the set of trees generated by t1 is a subset of that of t2 .
Lemma 6. br t [emp/x]t ⊇ [t/x]t .
Lemma 7. If t1 ⊇=⇒ t2 , then t1 =⇒⊇ t2 .

We deﬁne Bi (E)[tA ][tBi ] by:
Bi ([ ])[tA ][tBi ] = tBi
Bi (a t1 · · · tj−1 E tj+1 · · · tΣ(a) )[tA ][tBi ]= aBi A(t1 ) Bi (t1 ) · · · A(tj−1 ) Bi (tj−1 ) tA Bi (E)[tA ][tBi ] A(tj+1 ) Bi (tj+1 ) · · · A(tΣ(a) ) Bi (tΣ(a) )Bi (case E of {aj yj ⇒ tj }nj=1 )[tA ][tBi ]emp/
yjBi ]Bi (tj )}nj=1 )= br Bi (E)[tA ][tBi ] (case A(E)[tA ] of {aj yjA ⇒ [Bi (assertL (E)) = Bi (E)[tA ][tBi ]Lemma 8. If t =⇒ t , then Bi (t) =⇒∗ ⊇ Bi (t ).
Proof. We prove the lemma by case analysis for the last rule used to derivet =⇒ t :E-App
We havet = E[F t1 . . . tn ]t = E[[t1 /x1 , . . . , tn /xn ]t ]F x1 . . . xn = t ∈ D
Bi
A

Bi
A Bi

xA
We get F A xA
1 . . . xn = A(t ) ∈ Bi (D). F
1 x1 . . . xn xn = Bi (t ) ∈Bi (D). We have

Bi (t) = Bi (E)[A(F t1 . . . tn )][Bi (F t1 . . . tn )]= Bi (E)[A(F t1 . . . tn )][F Bi A(t1 ) Bi (t1 ) . . . A(tn ) Bi (tn )]
Bi
A
Bi

=⇒ Bi (E)[A(F t1 . . . tn )][[A(t1 )/xA
1 , Bi (t1 )/x1 , . . . , A(tn )/xn , Bi (tn )/xn ]Bi (t )](By E-App)= Bi (E)[A(F t1 . . . tn )][Bi ([t1 /x1 , . . . tn /xn ]t )](By Lemma 5)
=⇒ Bi (E)[A([t1 /x1 , . . . , tn /xn ]t )][Bi ([t1 /x1 , . . . tn /xn ]t )](By E-App)= Bi (E[[t1 /x1 , . . . tn /xn ]t ])= Bi (t )E-CaseWe havet of {aj yj ⇒ tj }nj=1 ]t = E[case aj t = E[[t/
yj ]tj ]We obtain

t of {aj yj ⇒ tj }nj=1 )][Bi (case aj t of {aj yj ⇒ tj }nj=1 )]Bi (t) = Bi (E)[A(case aj t/yj ]tj )][Bi (case aj =⇒ Bi (E)[A([t of {aj yj ⇒ tj }nj=1 )]=(By E-Case)t/yj ]tj )][br Bi (aj t) of {aj yjA ⇒ [emp/yjBi ]Bi (tj )}nj=1 )]t) (case aj A(Bi (E)[A([=⇒ Bi (E)[A([t/yj ]tj )][br Bi (aj mp/
yjBi ]Bi (tj )]t) [A(t)/yjA , et/yj ]tj )][[A(t)/yjA , Bi (t)/
yjBi ]Bi (tj )]⊇ Bi (E)[A([= Bi (E)[A([t/yj ]tj )][Bi ([t/yj ]tj )]
= Bi (E[[t/yj ]tj ])(By E-Case)(By Lemma 6)(By Lemma 5)= Bi (t )E-Case-FailWe havet = E[case a t of {aj yj ⇒ tj }nj=1 ]t = E[fail]a ∈ {a1 , . . . , an }We obtain
Bi (t) = Bi (E)[A(case a t of {aj yj ⇒ tj }nj=1 )][Bi (case a t of {aj yj ⇒ tj }nj=1 )]=⇒ Bi (E)[fail][Bi (case a t of {aj yj ⇒ tj }nj=1 )]⊇ Bi (E)[fail][emp](By E-Case-Fail)= Bi (E)[A(fail)][Bi (fail)]= Bi (E[fail])= Bi (t )E-Gen
We havet = E[genL ]t = E[a genL1 . . . genLn ]a L1 · · · Ln ⊆ L
Bi (t) = Bi (E)[A(genL )][Bi (genL )]=⇒ Bi (E)[A(a genL1 . . . genLn )][Bi (genL )](By E-Gen)
L1
Ln= Bi (E)[A(a gen . . . gen )][emp]= Bi (E)[A(a genL1 . . . genLn )][Bi (a genL1 . . . genLn )]= Bi (E[a genL1 . . . genLn ])= Bi (t )E-Coerce
We havet = E[coerceLj (t1 )]t = E[t⊥2]∗
t1 =⇒ t2⊥t⊥2 ∈LBi (t) = Bi (E)[A(coerceLj (t1 ))][Bi (coerceLj (t1 ))]Lj(By E-Gen)=⇒∗ Bi (E)[A(t⊥2 )][Bi (coerce (t1 ))]⊥⊇ Bi (E)[A(t2 )][emp]⊥= Bi (E)[A(t⊥2 )][Bi (t2 )]= Bi (E[t⊥2 ])= Bi (t )E-Coerce-Assert
We havet = E[coerceLj (t )]t = assertLj (t )Bi (t) = Bi (E)[A(coerceLj (t ))][Bi (coerceLj (t ))]⊇ Bi (E)[A(coerceLj (t ))][Bi (t )]⊇ Bi (t )= Bi (assertLj (t ))= Bi (t )E-Assert-Error
This case is impossible
Proof of Theorem 2 Assume that |= (P Bi , M1 , . . . , Mk , B(Li )) holds for each i ∈{1, . . . , m} and S T1 · · · Tk =⇒∗ E[coerceLj (t)] for some T1 ∈ L(M1 ), . . . , Tk ∈L(Mk ). By Lemma 8, we obtain S Bj T1 emp · · · Tk emp(=⇒∗ ⊇)∗ Bj (E[coerceLj (t)])
By Lemma 7, we get S Bj T1 emp · · · Tk emp =⇒∗ ⊇ Bj (E[coerceLj (t)]). Thus, forLj∗
any t such that t =⇒∗ t , t⊥ ∈ B(Lj ) = L⊥
j . Therefore, E[coerce (t)] =⇒Error. By Lemma 4, we get E[coerceLj (t)] −→∗ Error.