Higher-Order Symb Comput
DOI 10.1007/s10990-013-9097-8

Polynomial-time inverse computation for accumulative
functions with multiple data traversals
Kazutaka Matsuda · Kazuhiro Inaba · Keisuke Nakano© The Author(s) 2013. This article is published with open access at Springerlink.com

Abstract The problem of inverse computation has many potential applications such as serialization/deserialization, providing support for undo, and test-case generation for software
testing. In this paper, we propose an inverse computation method that always terminates fora class of functions known as parameter-linear macro tree transducers, which involve multiple data traversals and the use of accumulations. The key to our method is the observationthat a function in the class can be regarded as a non-accumulative context-generating transformation without multiple data traversals. Accordingly, we demonstrate that it is easy toachieve terminating inverse computation for the class by context-wise memoization of theinverse computation results. We also show that when we use a tree automaton to express theinverse computation results, the inverse computation runs in time polynomial to the size ofthe original output and the textual program size.
Keywords Program inversion · Inverse computation · Program transformation · Functional
programming · Tree automata · Tree transducers

A preliminary summary of this article appeared in Proceedings of PEPM 2012, pp. 5–14, 2012.

B

K. Matsuda ( )Graduate School of Information Science and Technology, The University of Tokyo, 7-3-1 Hongo,
Bunkyo-ku, Tokyo, 113-0033 Japane-mail: kztk@is.s.u-tokyo.ac.jp
K. Inaba
National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo, 101-8430 Japane-mail: kiki@kmonos.net
Present address:
K. Inaba
Google Inc., PO Box 22, 6-10-1 Roppongi, Minato-ku, Tokyo, 106-6126 JapanK. NakanoCenter for Frontier Science and Engineering, The University of Electro-Communications,
1-5-1 Chofugaoka, Chofu, Tokyo, 182-8585 Japane-mail: ksk@cs.uec.ac.jp

Higher-Order Symb Comput

1 Introduction
The problem of inverse computation [1, 2, 20, 21, 23, 30, 37, 40, 49]—finding an input s
for a program f and a given output t such that f (s) = t —has many potential applications,
including test-case generation in software testing, supporting undo/redo, and obtaining adeserialization from a serialization program.
Let us illustrate the problem with an example. Suppose that we want to write an evaluator for a simple arithmetic expression language defined by the following datatype. (Webasically follow the Haskell syntax [6] even though we target an untyped first-order functional language with call-by-value semantics.)
data Val = Z | S(Val)data Exp = Zero | One | Add(Exp, Exp) | Dbl(Exp)Informally, Z and Zero represent 0, One represents 1, S(n) means n + 1 (the successor of n),
Add(n1 , n2 ) adds the numbers n1 and n2 , and Dbl(n) doubles the number n.
An evaluator eval :: Exp → Val of the expressions can be implemented as follows.
eval(x) = evalAcc(x, Z)=yevalAcc(Zero, y)= S(y)
evalAcc(One, y)evalAcc(Add(x1 , x2 ), y) = evalAcc(x1 , evalAcc(x2 , y))= evalAcc(x, evalAcc(x, y))evalAcc(Dbl(x), y)
Here, eval uses evalAcc that uses accumulations. The function evalAcc satisfies the invariant that evalAcc(e, m) = eval(e) + m, where “+” is the addition operator for values. Thisinvariant enables us to read the definition intuitively; e.g., the case of Dbl can be read aseval(Dbl(x)) + y = eval(x) + eval(x) + y.
The inverse computation of eval, which enumerates the inputs {s | eval(s) = t} for a givent , is sometimes useful for testing computations on E. For example, suppose that we write annoptimizer f that converts all the expressions e satisfying eval(e) = S2 (Z) into Dbln (One),nand we want to test if the optimizer works correctly or not, i.e., whether eval(e) = S2 (Z)n1implies f (e) = Dbl (One) or not. A solution would involve randomly generating or enun
merating expressions e, filtering out the es that do not satisfy eval(e) = S2 (Z), and checking f (e) = Dbln (One). However, it is unsatisfactory because it is inefficient; the majority
nof the expressions do not evaluate to S2 (Z). Inverse computation enables us to generate
only the test-cases that are relevant to the test. A test with inverse computation can be efn
ficiently performed by (1) picking up a number m of the form S2 (Z), (2) picking up an
expression e from the set obtained from the inverse computation for m, and (3) checking if
the optimizer f converts e into Dbln (One). Here, all the picked up (randomly generated or
enumerated) data are relevant to the final check in the Step (3). Lazy SmallCheck [43] andEasyCheck [9] use inverse computation for efficient test-case generation, which of course
has to be supported by efficient inverse computation.
However, there are as yet no systematic efficient inverse computation methods that canhandle eval. One reason is that evalAcc contains accumulations and multiple data traversals.
It is so far unclear how to perform tractable terminating inverse computation for functions
1 We use the shorthand notation g n (x) to stand for g(. . . (g (x)) . . . ).

  
n

Higher-Order Symb Comput

with accumulations and multiple data traversals (Sect. 2). Some of the existing methods [1,2, 21, 37] do not terminate for functions with accumulations. Some approaches [20, 39,40] can handle certain accumulative computations efficiently, but they do not work for noninjective functions such as eval. Although some inverse computation methods terminate foraccumulative functions [17, 32], the complexity upper bound is unclear when there are also
multiple data traversals.
In this paper, we propose an inverse computation method that can handle a class of accumulative functions like eval that have multiple data traversals, namely deterministic macro
tree transducers [15] with the restriction of parameter-linearity (Sect. 3). In this class offunctions, variables for accumulation (such as y in evalAcc) cannot be copied but inputs(such as x, x1 and x2 in evalAcc) can be traversed in many times (as x). Our method computes the set {s | f (s) = t} as a tree automaton [10] for a given function f and an output
y in time polynomial to the size of y (Sect. 4). The key to our inverse computation is theobservation that a program in the parameter-linear macro tree transducers is indeed a nonaccumulative transformation that generates contexts (i.e., trees with holes) without multiple
data traversals. From this viewpoint, we can do the inverse computation through a variantof the existing inverse computation methods [1, 2, 4]. Note that viewing a program as acontext-generating transformation is not new. What is new in our paper is to use this view toachieve polynomial-time inverse computation for the class of accumulative functions withmultiple data traversals.
Our main contributions are summarized as follows.
– We demonstrate that simply viewing a function as a context-generating transformation
helps us to achieve a systematic inverse computation method for accumulative functions.
After converting a program into a context-generating one, it is easy to perform inverse
computation for the program.
– We show that, for parameter-linear macro tree transducers, our inverse computation
method runs in time polynomial to the size of the output and the textual program size,
and in time exponential to the number of the functions in the program.
The rest of the paper is organized as follows. Section 2 shows an overview of our proposal. Section 3 defines the target language, parameter-linear macro tree transducers. Section 4 formally presents our inverse computation method. Section 5 reports and discusses theexperimental results with our prototype implementation. Section 6 shows four extensions ofour proposal, and Sect. 7 shows the relationship between ours and the other research. Section 8 concludes the paper and outlines future work.
The preliminary version of this article has appeared in [36]. The main difference fromthe version is that we have implemented the proposed algorithm and performed some experiments (Sect. 5). We also have added discussions on the two further extensions of our
proposed method (Sects. 6.3 and 6.4) and some explanations in several places.

2 Overview
In this section, we give a brief overview of our proposal.
2.1 Review: when inverse computation terminates
Let us begin with an illustrative example showing when a simple inverse computation [1, 4]
terminates. The following function parity takes a natural number n and returns n mod 2.

Higher-Order Symb Comput

parity(Z)=Z
parity(S(x)) = aux(x)= S(Z)= parity(x)aux(Z)
aux(S(x))

What should we do for inverse computation of parity given an original output t ?
Abramov and Glück [1, 2] used a symbolic computation method called (needed) narrow?
?
ing2 [4] as a simple way to find a substitution θ such that parity(x)θ = t , where = represents?
an equivalence check of (first-order) values defined in a standard way (e.g., Z = Z ≡ ). The
same idea is also shared among logic programming languages such as Curry and Prolog.3
Roughly speaking, a narrowing is a substitution followed by a reduction, and it can reducean expression with free variables. For example, parity(x) is not reducible, but, if we substitute Z to x, we can reduce the expression to Z. Such a reduction after a substitution is anarrowing that can be written as parity(x) ;x→Z Z. The notion can naturally be extended?
?
to equivalence checks, such as (parity(x) = Z) ;x→Z (Z = Z) ≡ . By using narrowing, we
can obtain the corresponding input by collecting the substitutions used in the narrowing. For
example, consider the inverse computation of parity for an output Z. Since we have4?

(parity(x) = Z) ;x→Z 
we know that parity(Z) = Z, and since we have?

?

?

(parity(x) = Z) ;x→S(x) (aux(x) = Z) ;x→S(x) (parity(x) = Z) ;x→Z 
we know that parity(S(S(Z))) = Z.
Sometimes, the simple inverse computation does not terminate; this happens especiallywhen we give it an output that has no corresponding inputs. For example, the simple inverse
computation of parity for an output S(S(Z)) runs infinitely:?

?

(parity(x) = S2 (Z)) ;x→S(x) (aux(x) = S2 (Z))?

;x→S(x) (parity(x) = S2 (Z)) ;x→S(x) . . .
?

One might notice that the check (parity(x) = S2 (Z)) occurs twice in the sequence.
Actually, with memoization, the simple inverse computation for parity always terminates.
For the above narrowing sequence, by memoizing all the checks in the sequence, we can tell?
that the same check (parity(x) = S2 (Z)) occurs twice, and hence the narrowing sequence
cannot produce any result. In general, the number of equality checks occurring in the inverse?
computation is finite because it always has the form f (x) = t (up to α-renaming), where t isa subterm of the original output given to the inverse computation. Thus, the simple inverse
computation always terminates with memoization for parity.
This observation also gives an upper bound of the worst-case complexity of inverse computation of parity; it runs in constant time regardless the size of the original output because
2 Precisely speaking, they used driving [45] instead of narrowing; these notions are developed independently

in the different context, but they essentially have the same mechanism [3].
3 See [22] for the correspondence between driving and SLD-resolution.
?
4 Here, we implicitly apply the reduction rules of =as much as possible.

Higher-Order Symb Comput?

?

the checks in the narrowing have the form of either parity(x) = t or aux(x) = t , only wheret is the original output.
2.2 Problem: non-termination due to accumulations and multiple data traversals
Consider a simplified version of eval:= evA(x, Z)ev(x)= S(y)evA(One, y)evA(Add(x1 , x2 ), y) = evA(x1 , evA(x2 , y))= evA(x, evA(x, y))evA(Dbl(x), y)Though simplified, this function still contains the challenging issues: accumulations andmultiple data traversals. Since we have {s | ev(s) = S2 (Z)} = {Dbl(One), Add(One, One)}for example, the inverse computation of ev for S2 (Z) should result in the set above.
Unlike parity, the simple inverse computation method does not always terminate. For
example, the simple inverse computation of ev for Z does not terminate.
?

?

(ev(x) = Z) ; (evA(x, Z) = Z)?

;x→Dbl(x) (evA(x, evA(x, Z)) = Z) ;x→Dbl(x) . . .

Memoization is no longer useful for making the simple inverse computation terminate because there are no repeated checks in the infinite sequence.
The following issues make it difficult for the inverse computation to terminate and evenharder to run it in polynomial time.
– Accumulations, a sort of call-time computation commonly used in tail recursion, increase
the size of the terms in the narrowing process. For example, evA contains the accumulations
evA(Dbl(x), y) = evA(x, evA(x, y))which increase the term-size in the following narrowing steps.
?

?

(evA(x, Z) = Z) ;x→Dbl(x) (evA(x, evA(x, Z)) = Z)
We can see that the second argument of evA (underlined above) gets bigger in narrowing.
– Multiple data traversals make things much worse. It prevents us from considering function calls separately. For example, we have to track the two calls evA(x, evA(x, y)) simultaneously. We can see that the number of function calls we have to track simultaneously
increases in narrowing. To clarify the problem caused by multiple data traversals, we will
look at the issue of accumulations in the absence of multiple data traversals. Supposethat ev does not have the case for Dbl and thus does not contain multiple data traversals.
Although there are still an infinite narrowing sequence?

?

(ev(x) = Z) ; (evA(x, Z) = Z)?

;x→Add(x1 ,x2 ) (evA(x1 , evA(x2 , Z)) = Z) ; . . . ,Higher-Order Symb Comput

one can make the simple inverse computation terminate by decomposing the check?
?
?
(evA(x1 , evA(x2 , Z)) = Z) into evA(x1 , z) = Z ∧ evA(x2 , Z) = z and by observing that,?
for evA(x1 , z) = z , we only need to consider the substitutions that map z and z to subterms of the output fed to the inverse computation, i.e., Z. Thus, we can substitute a?
?
concrete subterm to z and check evA(x1 , Z) = t and evA(x2 , t) = Z separately for a concrete t (a more refined idea can be found in [17, 32]), and we can bound the complexityof inverse computation in a similar way as we did for parity. However, this idea does notscale for functions with multiple data traversals, in which many function calls are tracked
simultaneously in narrowing. Although the existing approaches [17, 32] achieve terminating inverse computation of certain accumulative functions with multiple data traversals,
it is unclear whether there are polynomial-time inverse computations for functions withmultiple data traversals.
2.3 Our idea
One might have noticed that the result of evA(s, t) can be written as Ks [t] whatever t is,where Ks is a context (i.e., a tree with holes like S(•)) determined by s and Ks [t] is thetree obtained from Ks by replacing • with t . For example, we have evA(One, Z) = S(Z),evA(One, S(Z)) = S(S(Z)), where we have underlined the hole position of the context. Moregenerally, for a context KOne = S(•), we have evA(One, t) = KOne [t] for any t . Thus, we
can define a context-generating version evAc of evA that satisfies evAc (One) = S(•), forexample. The functions evc and evAc can be defined as follows.
= k[Z] where k = evAc (x)evc (x)= S(•)
evAc (One)evAc (Add(x1 , x2 )) = k1 [k2 [•]] where {ki = evAc (xi )}i=1,2
evAc (Dbl(x))= k[k[•]] where k = evAc (x)There are no accumulations or multiple data traversals. That is, evAc is indeed a nonaccumulative and input-linear context-generating transformation. Note that evc (x) = ev(x)holds for any x.
Now the simple inverse computation terminates again. For example, the inverse computation of evc for S2 (Z) is as follows.
?

(evc (x) = S2 (Z));?

?

{because (k[Z] = S2 (Z)) ≡ (k = S2 (•))}?

(evAc (x) = S2 (•))
;x→Dbl(x)?

?

{because (k[k[•]] = S2 (•)) ≡ (k = S[•])}?

;x→One(evAc (x) = S(•))
?

The only difference is that now = takes care of the contexts. Notice that the checks occurring?
in the narrowing have the form fc (x) = K, where K is a subcontext of the original output.
Since this generally holds for evc , the termination property of the simple inverse computation
is now recovered.
Besides the new point of view, our approach also involves a new way to express the memoized narrowing computation. Instead of using (a variant of) the existing method directly, weHigher-Order Symb Comput

use a tree automaton [10]; it is more suitable for a theoretical treatment than side-effectful
memoized narrowing, and can express an infinite set of inputs (note that in general the number of corresponding inputs is infinite as in the case of parity). For example, the inverse
computation of evc for S2 (Z) can be expressed by the following automaton where each stateis of the form qf −1 (K) .
← qevA−1
qev−1
22
c (S (Z))
c (S (•))
qevA−1← Add(qevA−1, qevA−1)22
c (S (•))
c (•)
c (S (•))← Add(qevA−1, qevA−1)
qevA−12c (S (•))
c (S(•))c (S(•))
qevA−1
2 (•)) ← Add(qevA−1 (S2 (•)) , qevA−1 (•) )
(
S
c
c
c
← Dbl(qevA−1)
qevA−12c (S (•))
c (S(•))
qevA−1← One
c (S(•))
qevA−1← Add(qevA−1, qevA−1)c (S(•))c (•)
c (S(•))← Add(qevA−1, qevA−1)
qevA−1c (S(•))c (S(•))c (•)
qevA−1c (•)
qevA−1c (•)?

← Add(qevA−1, qevA−1
)
c (•)
c (•)
← Dbl(qevA−1
)
c (•)
?

Note that f (x) = K can be regarded as x = f −1 (K). We write qf −1 (K) for a state instead
because an automaton constructed in this way can be regarded as all the possibleof qf (x)=K?

reductions starting with f −1 (K). This automaton contains the state qevA−1
that accepts noc (•)−1trees, which intuitively means that the evaluation of evAc (•) fails; i.e., the narrowing from?

evAc (x) = • fails. The size of the resulting automaton is bounded linearly by the size of theoriginal output of ev. It is also worth noting that we can extract a tree from an automaton intime linear to the size of the automaton [10].
All of the above results are obtained by just a simple observation: a program like ev is a
non-accumulative context-generating transformation without multiple data traversals.
3 Target language
In this section, we formally describe the programs we target, which are written in an (untyped) first-order functional programming language with certain restrictions.
3.1 Values: trees
The values of the language are trees consisting of constructors (i.e., a ranked alphabet).
Definition 1 (Trees) A set of trees TΣ over constructors Σ is defined inductively as follows: for every σ ∈ Σ (0) , σ ∈ TΣ , and for every σ ∈ Σ (n) and t1 , . . . , tn ∈ TΣ (n > 0),
σ (t1 , . . . , tn ) ∈ TΣ , where Σ (n) is the set of the constructors with arity n.
For constructors Z, Zero, One, Nil ∈ Σ (0) , S ∈ Σ (1) and Cons, Add ∈ Σ (2) , examples oftrees are S(Z), Cons(Z, Nil), and Add(Add(Zero, One), Zero). We shall fix the set Σ of theconstructors throughout the paper for simplicity of presentation. The size of a tree t is thenumber of the constructor occurrences in t . For example, the size of S(Z) is 2.
In what follows, we shall use vector notation: t represents a sequence t1 , . . . , tn and |t|
denotes its length n.

Higher-Order Symb Comput
Fig. 1 Syntax of the target
language: σ is an n-ary
constructor, and f is an(m + 1)-ary function

program ::= rule1 . . . rulen
rule::= f (p, y1 , . . . , ym ) = ep::= x | σ (x1 , . . . , xn )(Constructor Application)e::= σ (e1 , . . . , en )(Function Call)| f (x, e1 , . . . , em )| y(Parameter Use)

3.2 Programs: macro tree transducers
The syntax of the language is shown in Fig. 1. A program consists of a set of rules, and eachrule has the form of either f (σ (x1 , . . . , xn ), y1 , . . . , ym ) = e or f (x, y1 , . . . , ym ) = e. There
are two kinds of variable: input and output. Input variables, denoted by x in Fig. 1, can be
decomposed by pattern-matching but cannot be used to compose a result. Output variables,
denoted by y in Fig. 1, can be used to compose a result but cannot be decomposed. Output
variables are sometimes called (accumulation) parameters. A program in the language isnothing but a (stay) macro tree transducer (MTT) [15]. Thus, a program written in the target
language is called an MTT in this paper.
Example 1 (reverse) A simple example of an accumulative function written in the target language is reverse. The following function reverse reverses a list of natural numbers expressedby S and Z.
reverse(x)= rev(x, Nil)=yrev(Nil, y)rev(Cons(a, x), y) = rev(x, Cons(nat(a), y))nat(Z)
nat(S(x))=Z= S(nat(x))

The function nat just copies an input. This function is necessary because we prohibit using
an input directly to produce a result in the language (see Fig. 1).
Example 2 (eval) The eval program in Sect. 1 is an example of an MTT program. So is its
simplified version ev.
Example 3 (mirror) The following function mirror mirrors a list.
mirror(x)= app(x, rev(x, Nil))= yapp(Nil, y)app(Cons(a, x), y) = Cons(nat(a), app(x, y))We omit the rules for rev and nat because they are the same as those in Example 1. Unlike
ev and eval, mirror traverses an input twice with the different functions (app and rev). The
function app is the so-called “append” function.
The size of a program is defined by the total number of function, constructor, and variableoccurrences in the program. The intuition behind this definition is to approximate the sizeof program code in text. Note that the number of function or constructor occurrences isdifferent from the number of functions or constructors. For example, the number of functions
in reverse is 3, whereas the number of function occurrences is 9.

Higher-Order Symb Comput{Γ ; Δ
Γ ;Δf (x, y) = e{y → t}{Γ ; ΔΓf (σ (x), y) = e

s = σ (s)
Γ

y↓t

Γ ;Δ

ei ↓ ti }1≤i≤|e|{x → s} ; Δ{Γ ; Δσ (e) ↓ σ (t){x → s} ; y → t

e ↓ t

f (x, e) ↓ t 

ei ↓ ti }1≤i≤|e|{x → s} ; Δei ↓ ti }1≤i≤n{x → s} ; y → t

e ↓ t

f (x, e) ↓ t 

Fig. 2 Call-by-value semantics of the target language: here, we abuse the notation to write {x → s} for{x1 → s1 , . . . , xn → sn } where n = |x| = |s|

The language has a standard call-by-value semantics, as shown in Fig. 2. A judgment
Γ ; Δ e ↓ t means that under an input-variable environment Γ and output-variable environment Δ, an expression e is evaluated to a value t . Programs are assumed to be deterministic; i.e., for each f , either f has at most one rule of the form f (x, y1 , . . . , ym ) = e or has
at most one rule of the form f (σ (x1 , . . . , xn ), y1 , . . . , ym ) = e for each σ . The semantics ofa function f is defined by tif {x → s} ; ∅ f (x, t) ↓ t  for fresh x,[[f ]](s, t) =⊥ otherwise.
Note that we allow partial functions; e.g., we have [[nat]](Nil) = ⊥. We shall sometimes abuse the notation and simply write f for [[f ]]. The semantics is nothing but IOproduction [15].
In addition, we also assume that programs are nondeleting, i.e., every input variable mustoccur in the corresponding right-hand-side expression. This restriction does not change
the expressiveness; we can convert any program to one satisfying this restriction by introducing the function ignore satisfying [[ignore]](s, t) = t for any s and t and defined byignore(σ (x1 , . . . , xn ), y) = ignore(x1 , . . . ignore(xn , y) . . . ) for every σ ∈ Σ . The restriction
simplifies the discussions in Sects. 4.3, 6.1 and 6.2. All the previous examples are deterministic and nondeleting.
A program is called parameter-linear if every output variable y occurring on the lefthand side occurs exactly once on the corresponding right-hand side of each rule.5 All theprevious examples are parameter-linear. Our polynomial time inverse computation depends
on parameter-linearity.

4 Polynomial-time inverse computation
In this section, we formally describe our inverse computation. As briefly explained in Sect. 2,
first, we convert an MTT program into a non-accumulative context-generating program(a program that generates contexts instead of trees) without multiple data traversals, such as
evc in Sect. 2.3. Then, we perform inverse computation with memoization. More precisely,
we construct a tree automaton [10] that represents the inverse computation result, whose
run implicitly corresponds to (a context-aware version of) the existing inverse computation
process with memoization [1, 4].
5 Our definition of parameter-linearity is stronger than “single-use restricted on the parameters” [12] and“non-copying” [47]; they require that each parameter is used at most once.

Higher-Order Symb Comput

Our inverse computation consists of three steps:
1. We convert a parameter-linear MTT into a non-accumulative context-generating program.
2. We apply tupling [8, 25] to eliminate multiple data traversals.
3. We construct a tree automaton that represents the inverse computation result.
The first two steps are to obtain a non-accumulative context-generating program without
multiple data traversals. The third step represents memoized inverse computation. The restof this section explains each step in detail.
4.1 Conversion to context-generating program
The first and most important step is to convert an MTT program into a non-accumulative
context-generating program. This transformation is also useful for removing certain multiple
data traversals, as shown in the example of ev in Sect. 2. Moreover, this makes it easy toapply tupling [8, 25] to programs. Note that viewing MTT programs as non-accumulative
context-generating transformations is not a new idea (see Sect. 3.1 of [12] for example). The
semantics of the context-generating programs shown later is nothing but using Lemma 3.4of [12] to evaluate MTT programs.
First, we will give a formal definition of contexts.
Definition 2 An (m-hole) context K is a tree in K ∈ TΣ∪{•1 ,...,•m } where •1 , . . . , •m are
nullary symbols such that •1 , . . . , •m ∈ Σ .
An m-hole context K is linear if each •i (1 ≤ i ≤ m) occurs exactly once in K. We
write K[t1 , . . . , tm ] for the tree obtained by replacing •i with ti for each 1 ≤ i ≤ m. For
example, K = Cons(•1 , •2 ) is a 2-hole context and K[Z, Nil] is the tree Cons(Z, Nil). For
1-hole contexts, •1 is sometimes written as •.
We showed that ev is indeed a non-accumulative context-generating transformation in
Sect. 2. In general, any MTT program can be regarded as a non-accumulative contextgenerating transformation in the sense that, since output variables cannot be patternmatched, the values bound to the output variables appear as-is in the computation result.
Formally, we can state the following fact (Engelfriet and Vogler [15]; Lemma 3.19).
Fact 1 [[f ]](s, t) = t if and only if there is K such that [[f ]](s, •) = K and t = K[t].
Accordingly, we can convert an MTT program into a non-accumulative contextgenerating program, as shown below.
Algorithm 1 Conversion to context-generating programs
Input: An MTT program
Output: A non-accumulative context-generating program
Procedure:
For each rule f (p, y1 , . . . , ym ) = e of the input program, construct a rulefc (p) = e where kg1 ,x1 = g1 c (x1 ), . . . , kgn ,xn = gn c (xn )where– g1 c (x1 ), . . . , gn c (xn ) are obtained from all the function calls that occur as gi (xi , . . . ) in e,

Higher-Order Symb Comput– kgi ,xi (1 ≤ i ≤ n) represents a fresh variable name determined by gi and xi , and– e is obtained by e = cg(e) where cg is defined as follows.
cg(σ (e1 , . . . , en )) = σ (cg(e1 ), . . . , cg(en ))cg(g(x, e1 , . . . , en )) = kg,x [cg(e1 ), . . . , cg(en )]cg(yj )= •j (1 ≤ j ≤ m)

As a result of the above, in a converted program, the arguments of every function arevariables, and the return value of a function cannot be traversed again. This rules out any
accumulative computation.
The algorithm above is very similar to that used for deaccumulation [19, 31]. Unlike
deaccumulation, we treat contexts as first-class objects, which enables us to adopt special
treatment for contexts in our inverse computation method.
Example 4 (reverse) The reverse program is converted into the following program.
reversec (x)= k[Nil] where k = revc (x)= •1revc (Nil)revc (Cons(a, x)) = k2 [Cons(k1 , •1 )]where k1 = natc (a), k2 = revc (x)natc (Z)natc (S(x))=Z= S(k) where k = natc (x)The converted program has no accumulative computation.
Example 5 (eval) The eval program in Sect. 1 is converted into the following program.
evalc (x)= k[Z] where k = evalAc (x)= •1evalAc (Zero)evalAc (One)= S(•1 )evalAc (Add(x1 , x2 )) = k1 [k2 [•1 ]]where k1 = evalAc (x1 ), k2 = evalAc (x2 )= k[k[•1 ]] where k = evalAc (x)evalAc (Dbl(x))
Note that the two occurrences of the function call evalAcc(x, . . . ) on the right-hand side of
the rule evalAcc(Dbl(x)) = . . . are unified into the single call k = evalAccc (x). Recall that
Algorithm 1 generates a new variable kf,x for a pair of a function f and its input x, but notfor its occurrence. Applying the same function to the same input results in the same context
in a context-generating program, even though different accumulating arguments are passedin the original program. As a side effect, certain multiple data traversals, i.e., traversals of
the same input by the same function, are eliminated through this conversion.
Example 6 (mirror) The mirror program in Sect. 3 is converted into the following program.
= k1 [k2 [Nil]]mirrorc (x)where k1 = appc (x), k2 = revc (x)= •1appc (Nil)appc (Cons(a, x)) = Cons(k1 , k2 [•1 ])where k1 = natc (a), k2 = appc (x)Higher-Order Symb Comput

SyntaxSemantics

prog ::= rule1 . . . rulen
rule ::= f (p) = e where k1 = f1 (x1 ), . . . , kn = fn (xn )p::= x | σ (x1 , . . . , xn )e::= •j | σ (e1 , . . . , en ) | k[e1 , . . . , en ]f (x) = e where k = g(z) l = |k = g(z)|{{x → s} c gi (zi ) ↓ Ki }1≤i≤l Θ = {k → K} K  = eΘΓ{x → s} c f (x) ↓ K f (σ (x)) = e where k = g(z) s = σ (s) l = |k = g(z)|{{x → s} c gi (zi ) ↓ Ki }1≤i≤l Θ = {k → K} K  = eΘΓ{x → s} c f (x) ↓ K 

Fig. 3 Syntax and semantics of the converted programs: here, we abuse the notation to write k = g(z) for
sequence k1 = g1 (z1 ), . . . , kl = gl (zl ) where l = |k = g(z)| and write {x → s} as in Fig. 2

We have omitted the definitions of revc and natc because they are the same as in Example 4.
Some multiple data traversals still remain as k1 = appc (x), k2 = revc (x). However, thanks tothe conversion, this sort of multiple data traversal is easy to eliminate by tupling [8, 25] (seethe next subsection).
For formal discussion, we define the syntax and the semantics of the non-accumulative
context-generating programs in Fig. 3. Since contexts are bound to context variables k,
the semantics uses second-order substitutions [12] that are mappings from variables tocontexts. The application eΘ of a second-order substitution Θ to a term e is inductively
defined by: σ (e1 , . . . , en )Θ = σ (e1 Θ, . . . , en Θ) and k[e1 , . . . , en ]Θ = K[e1 Θ, . . . , en Θ]
where K = Θ(k). Similarly to MTT, we write [[f ]] for the semantics of f .
Now, we can show that the conversion is sound; it does not change the semantics of thefunctions.
Lemma 1 For any tree s, [[f ]](s, •) = [[fc ]](s).
Together with Fact 1, we have [[f ]](s, t) = K[t] with K = [[fc ]](s) for every tree s and t .
4.2 Tupling
Tupling is a well-known semantic-preserving program transformation that can remove someof the multiple data traversals [8, 25].
Roughly speaking, tupling transforms a ruleh(x) = . . . k1 . . . k2 . . . where k1 = f (x), k2 = g(x)intoh(x) = . . . k1 . . . k2 . . . where (k1 , k2 ) = f, g(x).
Here, f, g is a function name introduced by tupling, and it is expected to satisfy
f, g(x) = (f (x), g(x)). Tupling tries to find a recursive definition of f, g(x) recursively.

Higher-Order Symb Comput

For example, the following program for mirror is obtained by tupling.
= k1 [k2 [Nil]]mirrorc (x)where (k1 , k2 ) = appc , revc (x)= (•1 , •1 )
appc , revc (Nil)appc , revc (Cons(a, x)) = (Cons(k1 , k2 [•1 ]), k3 [Cons(k1 , •1 )])where k1 = natc (a), (k2 , k3 ) = appc , revc (x)We shall not explain the tupling in detail because it has been well-studied in the literature offunctional programming [8, 25]. Moreover, we shall omit the formal definition of the syntax
and the semantics of tupled programs because they are straightforward.
Note that we tuple only the functions that need to be tupled, i.e., the functions that traverse
the same input, for the sake of simplicity of our inverse computation method that we will
discuss later. For example, appc and revc are tupled because they traverse the same input,
whereas natc and appc are not tupled. Thus, the tupling step does not change the reversec
and evalc programs. In the tupled program obtained in this way, for any call of a tupledfunction (k1 , . . . , kn ) = f1 , . . . , fn (x), each variable ki (1 ≤ i ≤ n) occurs at least once inthe corresponding expression.
Thanks to the conversion described in the previous section, tupling can eliminate all themultiple data traversals from the converted programs. After tupling, a rule has the form ofeitherf (x) = e where k = g(x)orf (σ (x1 , . . . , xn )) = e where k1 = g1 (x1 ), . . . , kn = gn (xn ).
Here, f , g, g1 , . . . , gn are tupled functions. In other words, the tupled programs are always
input linear; that is, every input variable occurring on the left-hand side also occurs exactly
once on the corresponding right-hand side of each rule.
Tupling may cause size blow-up of a program: a tupled program is at worst 2F -times
as big as the original program; F here is the number of functions in the original program.
Recall that we tuple only the functions that traverse the same input, not all the functions in a
program. Note that only one of revc , appc  and appc , revc  can appear in a tupled program.
Thus, the tupled functions f1 , . . . , fn  are as numerous as the sets of the original functions{f1 , . . . , fn }.
4.3 Tree automata construction as memoized inverse computation
We perform inverse computation with memoization after all the preprocessing steps havebeen completed. However, as mentioned in Sect. 2, unlike the existing inverse computation methods [1, 2, 4], we use a tree automaton [10] to express the memoized-inversecomputation result for the following reasons.
– A tree automaton is more suitable for a theoretical treatment than a side-effectful memoization table.
– The set {s | f (s) = t} may be infinite (e.g., eval).
– We can extract a tree (in DAG representation) from an automaton in time linear to the sizeof the automaton [10].
– In some applications such as test-case generation, it is more useful to enumerate the setof the corresponding inputs instead of returning one of the corresponding inputs.

Higher-Order Symb Comput

Thus, the use of memoization is implicit in our inverse computation, and we shall not men?
tion narrowing ; and check = in this formal development. Note that tree automata areused in the inverse computation because they are convenient rather than necessary; even
without them, we can use (a memoized and context-aware version of) the existing inverse
computation methods [1, 2, 4].
First of all, we review the definition of tree automata. A tree automaton [10] A is a triple(Σ, Q, R), where Σ is a ranked alphabet, Q is a finite set of states, and R is a finite set oftransition rules each having the form of either q ← q  or q ← σ (q1 , . . . , qn ) where σ ∈ Q(n) .
We write [[q]]A for the trees accepted by state q in A, i.e., {t | q ←∗ t} where we take ← as
rewriting.
We shall roughly explain the construction of a tree automaton as inverse computation byusing the example of evc given in Sect. 2. We construct an automaton whose states have theform qf −1 (K) that represents the evaluation of f −1 (K), or the inverse computation result off for K. Consider inverse computation of evc for S2 (Z). The idea behind the construction
is to track the evaluation of ev−1 (S2 (Z)). Since the right-hand side of evc is k[Z], where−12
k = evAc (x), the evaluation ev−1c (S (Z)) invokes the evaluation of evAc (k) for k such that22k[Z] = S [Z]. In this case, we have only such a k = S (•). Thus, we generate a transition
rule,
qev−1
← qevA−1.
22
c (S (Z))
c (S (•))
2
Next, let us focus on how evA−1
c (S (•)) is evaluated. There are three rules of evAc . The first
one has the right-hand side S(•), the second one has the right-hand side k1 [k2 [•]] wherek1 = evAc (x1 ) and k2 = evAc (x2 ), and the third one has the right-hand side k[k[•]] where k =evAc (x). Then, we shall consider the (second-order) matching between the context S2 (•),
the argument of evA−1
c , and the right-hand sides. The right-hand side of the first rule does notmatch the context. For the second rule, there are possibly three (second-order) substitutions
obtained from matching S2 (•) with k1 [k2 [•]]: k1 = •, k2 = S2 (•); k1 = S(•), k2 = S(•); andk1 = S2 (•), k2 = •. Recall that k1 and k2 are defined by k1 = evAc (x1 ) and k2 = evAc (x2 ),and x1 and x2 come from the pattern Add(x1 , x2 ). Thus, we generate the following rules.

qevA−1← Add(qevA−1, qevA−1)22
c (S (•))
c (•)
c (S (•))
qevA−1
2 (•)) ← Add(qevA−1 (S(•)) , qevA−1 (S(•)) )
(
S
c
c
c
← Add(qevA−1, qevA−1)
qevA−12
2
c (S (•))
c (S (•))
c (•)
Similarly, for the third rule, since there is only one substitution k = S(•) obtained frommatching S2 (•) with k[k[•]], we generate the following rule.
qevA−1← Dbl(qevA−1)
2c (S (•))
c (S(•))
2
Now that we have obtained the transition rules corresponding to the call evA−1
c (S (•)), we−1
focus on evAc (S(•)). A similar discussion to the one above enables us to generate thefollowing rules.

qevAc (S(•))−1 ← One
qevA−1← Add(qevA−1, qevA−1)c (S(•))c (•)
c (S(•))
←
Add
(q
,
q
qevA−1−1−1
evAc (S(•)) evAc (•) )c (S(•))

Higher-Order Symb Comput

After that, we move to the rules of evA−1
c (•) and generate the following rules.
qevA−1← Add(qevA−1, qevA−1
)
c (•)
c (•)
c (•)
←
Dbl
(q
)
qevA−1−1
evAc (•)
c (•)
Thus, the inverse computation of evc for S2 (Z) is complete. Let AI be the automa]] =ton constructed by gathering the generated rules. We can see that [[qev−1
2
c (S (Z)) AI{Dbl(One), Add(One, One)}. Note that the state qevA−1
accepts no trees.
c (•)
This automaton construction is formalized as follows.
Algorithm 2
Input: A tupled program and a tree t .
Output: A tree automaton AI = (Σ, Q, R).
Procedure: Construct Q and R as follows.
– Q is the set of states of the form qf1 ,...,fn −1 (K1 ,...,Kn ) , where f1 , . . . , fn  is a function
occurring in the tupled program, Ki (1 ≤ i ≤ n) is a (ai − 1)-hole linear subcontext of t ,and ai is the arity of fi . Here, K is called a subcontext of t if t = K  [K[t1 , . . . , tm ]] holds
for some linear context K  and trees t1 , . . . , tm .
– R is the set of transition rules constructed from the rules of the tupled program and thetuples of the linear subcontexts of t , in the following way.
– For each rule of the form f (x) = e where k = g(x) and subcontexts K of t , and forevery second-order substitution Θ such that eΘ = K, we construct a ruleqf −1 (K) ← qg−1 (K  )where K  = kΘ.
– For each rule of the form f (σ (x1 , . . . , xn )) = e where k1 = g1 (x1 ), . . . , kn = gn (xn )and contexts K, and for every second-order substitution Θ such that eΘ = K, weconstruct a ruleqf −1 (K) ← σ (qg−1 (K  ) , . . . , qgn−1 (Kn ) )1

1

where Ki = ki Θ for each 1 ≤ i ≤ n.
The problem of finding Θ satisfying eΘ = K for given e and K is called second-order(pattern) matching, and there have been proposed some algorithms to the problem [11, 26,27]. In the actual construction of the automaton, we do not generate any state that cannot
reach qf −1 (t) , where f is the function to be inverted and t is the original output. The examples that will be discussed below use this optimization. Note that a tree is a 0-hole context.
The nondeleting property is used in the above algorithm for simplicity. If a program is notnondeleting, some input variable x may not have the corresponding function call g(x) ina rule of the tupled program. Then, we have to adopt special treatment for such a x in theconstruction of R in the algorithm.

Higher-Order Symb Comput

Example 7 (reversec ) The following automaton AI is obtained from reversec and t =Cons(S(Z), Cons(Z, Nil)).
← qrev−1
qreverse−1c (t)c (Cons(S(Z),Cons(Z,•1 )))qrev−1← Cons(qnat−1, qrev−1)c (Cons(S(Z),Cons(Z,•1 )))c (Z)c (Cons(S(Z),•1 ))
←
Cons
(q
,
q
)
qrev−1−1−1
natc (S(Z)) revc (•1 )c (Cons(S(Z),•1 ))← Nilqrev−1c (•1 )
qnat−1← S(qnat−1)c (S(Z))c (Z)←Z
qnat−1c (Z)We have [[qreverse−1]] = {Cons(Z, Cons(S(Z), Nil))}, which means that there is only one
c (t) AI
input s = Cons(Z, Cons(S(Z), Nil)) satisfying reverse(s) = reversec (s) = t .
Example 8 (evalc ) The following automaton AI , where qi stands for state qevalA−1, isic (S (•1 ))obtained from eval and S2 (Z).
← q2qeval−12c (S (Z))
q2 ← Add(q2 , q0 )q2 ← Add(q1 , q1 )q2 ← Add(q0 , q2 )q2 ← Dbl(q1 )q1 ← Oneq1 ← Add(q1 , q0 )q1 ← Add(q0 , q1 )q0 ← Zeroq0 ← Add(q0 , q0 )q0 ← Dbl(q0 )Intuitively, qi represents the set of the arithmetic expressions that evaluate to Si (Z).
Example 9 (mirrorc ) The following automaton AI is obtained from mirrorc and Cons(Z,Cons(Z, Nil)).

← qappc ,revc −1 (Cons(Z,Cons(Z,•1 )),•1 )qmirror−1c (Cons(Z,Cons(Z,Nil)))qmirror−1← qappc ,revc −1 (Cons(Z,•1 ),Cons(Z,•1 ))c (Cons(Z,Cons(Z,Nil)))qmirror−1← qappc ,revc −1 (•1 ,Cons(Z,Cons(Z,•1 )))
(
Cons
(
Z
,
Cons
(
Z
,
Nil
)))
c
qappc ,revc −1 (Cons(Z,•1 ),Cons(Z,•1 )) ← Cons(qnat−1, qappc ,revc −1 (•1 ,•1 ) )c (Z)qappc ,revc −1 (•1 ,•1 ) ← Nil
qnat−1←Zc (Z)We have [[qmirror−1]] = {Cons(Z, Nil)}. Note that some states occurring onc (Cons(Z,Cons(Z,Nil))) AI
the right-hand side do not occur on the left-hand side. An automaton with such states commonly appear when we try to construct an automaton for a function f and a tree t that is notin the range of f . For example, the following automaton AI is obtained from mirrorc andCons(Z, Nil).
qmirror−1← qappc ,revc −1 (Cons(Z,•1 ),•1 )c (Cons(Z,Nil))qmirror−1← qappc ,revc −1 (•1 ,Cons(Z,•1 ))c (Cons(Z,Nil))
We have [[qmirror−1]]c (Cons(Z,Nil))

AI

= ∅.

Our inverse computation is correct in the following sense.

Higher-Order Symb Comput

Theorem 1 (Soundness and completeness) For an input-linear tupled program, s ∈[[qf −1 (K) ]] if and only if [[f ]](s) = (K).
AI

Proof Straightforward by induction.



4.4 Complexity analysis of our inverse computation
We show that the inverse computation runs in time polynomial to the size of the original
output and the size of the program, but in time exponential to the number of functions andthe maximum arity of the functions and constructors. We state as such in the following
theorem.
Theorem 2 Given a parameter-linear MTT program that defines a function f anda tree t , we can construct an automaton representing the set {s | f (s) = t} in timeO(2F m(2F nMF )N+1 nNMF ) where F is the number of the functions in the program, n is
the size of t , N is the maximum arity of constructors in Σ , m is the size of the program, andM is the maximum arity of functions.
Proof First, let us examine the cost of our preprocessing. The conversion into contextgenerating transformation does not increase the program size and can be done in time linear
to the program size. In contrast, the tupling may increase the program size to 2F m. Thus,
the total worst-case time complexity for preprocessing is O(2F m).
Next, let us examine the cost of the inverse computation. The constructed automaton
has at most 2F nMF states because every state is in the form g1 , . . . , gl −1 (K1 , . . . , Kl ), thenumber of g1 , . . . , gl  is smaller than 2F , the number of Ki is smaller than nM , and l is
no more than F . Note that the number of k-hole subcontexts in t is at most nk+1 and thecontexts occurring in our inverse computation have at most (M − 1) kinds of holes. Since
the number of the states in an automaton is bounded by P = 2F nMF and the transition rules
are obtained from the rules of the tupled programs that are smaller than 2F m, the numberof the transition rules is bounded by 2F mP N+1 . Each rule construction takes O(nNMF ) time
because, for the second-order matching to find Θ such that eΘ = K, the size of the solution
space is bounded by O(nNMF ); note that e contains at most N F context variables that haveat most (M − 1) kind of holes. Thus, an upper bound of the worst-case cost of the inverse
computation is O(2F m(2F nMF )N+1 nNMF ).
Therefore, the total worst-case time complexity of our method is bounded byO(2F m(2F nMF )N+1 nNMF ).
Note that, if we start from input-linear tupled context-generating programs, the cost isO(m(F nMd )N+1 nMc ), where c is the maximum number of context variables in the rules, andd is the maximum number of components of the tuples in the program. Also note that theabove approximation is quite rough. For example, our method ideally runs in time linear tothe size of the original output for reverse and mirror for eval, assuming some sophisticatedsecond-order pattern matching algorithm under some sophisticated context representation
depending on programs, which will be discussed in Sect. 5.5.
Each step of our inverse computation itself shown in Sects. 4.1, 4.2 and 4.3 does not use
the parameter-linearity of an MTT. We only use the parameter-linearity to guarantee that
our inverse computation is performed in polynomial time. For parameter-linear MTTs, weonly have to consider linear contexts; the number of linear subcontexts of a tree t of sizen is a polynomial of n, which leads our polynomial-time results. Our inverse computation

Higher-Order Symb Comput

indeed terminates for MTTs without restrictions in exponential time because the number ofpossibly-non-linear m-hole subcontexts of a tree t is at most |t|(m + 1)|t| .

5 Experiments and discussions
In this section, we report our prototype implementation of the proposed algorithm and experimental results with the prototype system. The actual complexity of our inverse computationis unclear due to the two points: second-order matching and the automaton states actually
generated by the automaton construction. By investigating several programs, we estimate
the complexity of our method and clarify how these two points affect the computation cost.
After the experiments, we discuss how can we improve the complexity of our method
for the investigated programs. For example, it is true that ideally we can achieve linear-timeinverse computation for reverse, the linear-time inverse computation is hard to achieve with
the naive implementation, as shown by the experimental result that we will describe later.
We discuss what causes the gap and how we can remove the gap.
5.1 Implementation and environment
Our prototype system is written in Haskell, and is implemented as an inverse interpreter [1],i.e., a program that takes a program and its output, and returns the corresponding inputs,
rather than an inverse compiler (program inverter) [20]. Usually, inverse computation done
by a inverse compiler runs faster than that done by an inverse interpreter. However, it isexpected that the effect is rather small for our case which uses rather heavy computations,
i.e., the second-order pattern matching and the automaton construction. For the second-ordermatching, we used the algorithm in [44] without heuristics, which is a variant of Huet’s
algorithm [26] specialized to linear λ-terms.
The experiments below were carried out on Ubuntu Linux 12.04 (for i686) on a machinewith Intel(R) Core(TM) i5 660 (3.33 GHz) and 8 GB memory. The prototype implementation is complied by Glasgow Haskell Compiler 7.4.16 under the flags -O2 -rtsopts andexecuted under the flags +RTS -H.
5.2 Experiments
To estimate how fast inverse computation can be performed by the prototype system in termsof the asymptotic complexity, we examined running time of the system by changing the sizeof original outputs fed to the inverse computation. The following programs and original
outputs were tested.
– reverse in Example 1 and a list of Zs.
– eval in Sect. 1 and a natural number.
– mirror in Example 3 and a list of Zs.

6 http://www.haskell.org/ghc/.

Higher-Order Symb Comput– The function toc, which construct the table-of-contents of a document and which will be
discussed in Sect. 6.3, expressed as an MTT as below,
toc(x) = UL(mkToc(x, E), E)= LI(copy(c), mkToc(s, y))
mkToc(Title(c, s), y)
mkToc(Section(c, s), y) = LI(UL(mkToc(c, E), E), mkToc(s, y))
mkToc(Paragraph(c, s), y) = ignore(c, mkToc(s, y))copy(A) = A
ignore(A, y) = y
and horizontally-repeated sequence representing (X)HTML fragments like:<ul><li>A</li><li>A</li>...</ul>
Here, a fragment <li>x</li>y and <ul>x</ul>y are represented by LI(x, y) andUL(x, y) respectively, the text A is represented by A, and the empty sequence is represented by E.
– The program toc above and vertically-repeated (nested) (X)HTML fragments like<ul><li>...<ul><li>A</li></ul>...</li></ul>
In the experiment, we only focus on estimation of the asymptotic complexity. For example,
we do not focus on the overhead from manually-written inverse programs or the preprocessing cost.
Figure 4 shows the log-log plot of the experimental results. In a log-log plot, a function
y = cx b is plotted as a straight line, because y = cx b implies log y = b log x + log c. To show
the estimated asymptotic complexity orders of the inverse computations, we also plotted an
additional line in each plot. Note that these additional line are not obtained by fitting; they
are added manually just to show how steeply the running time increases.
In the following, we discuss the experimental results one by one. Throughout the discussions, we use n for the size of the original output tree fed to the inverse computation that we
focus on.
5.2.1 reverse
The running time of the inverse computation for reverse is estimated as O(n2 ) from Fig. 4.
One might think that this result is strange because we know that the inverse of reverse isreverse and thus can be executed in linear time. This gap comes from the two points: theconstruction of the tree automaton and the second-order pattern matching.
Regarding the construction of the automaton described in Sect. 4.3, we just used a pair(f , K) to represents a state qf −1 (K) in the automaton. Since in the construction we check if
the transitions that go to a state are already generated or not and we used a balanced searchtree7 for the check, the checks takes O(|q| log |q|) for q = (f , K). For reverse, since the constructed automaton contains O(n) states and each state has the size O(n), the construction
itself takes O(n2 log n).

7 Concretely, we used Data.Map.

Higher-Order Symb Comput

Fig. 4 Experimental results for reverse, mirror, eval, and toc for two kinds of outputs

In construction of the transitions of each state, we solve the following second-ordermatching problems.
k[Cons(k  , Nil)] = t
?

?

and

k[Cons(k  , •)] = K?

Here, we abuse the notation to use = for the second-order matching problems. The implemented algorithm takes O(n) time to find the solutions, because it searches Cons( , Nil)/Cons( , •) from the top of t /K. Thus, since we solve similar second-order matching problems for each state, the cost that comes from the second-order matching is O(n2 ).
One might notice that the experiment indicates that the time cost of inverse computationof O(n2 ) while the above discussion indicates that it is O(n2 log n). Note that it is hard toobserve the difference by log n because the factor is too small for the problem size. Thus,
this is not a contradiction.

Higher-Order Symb Comput

5.2.2 mirror
The running time of the inverse computation of mirror is estimated as O(n3 ) from Fig. 4.
Note that the generated automaton contains O(n2 ) states because we do not know whichpart of the list is generated by app or rev. The constructed automaton contains statesof the form qapp,rev−1 (K l−k ,K m−k ) where l + m is equal to the length of an output list
(thus, l + m = (n − 1)/2) and k ≤ l, k ≤ m, and K i denotes the context of the form ofCons(Z, Cons(Z, . . . , Cons(Z, •) . . . )) containing i occurrences of Zs.
The effects of the automaton construction and the second-order matching are similar to
those of reverse; the automaton construction and the second-order matching take O(n log n)
and O(n) time for each state, respectively.
5.3 eval
The inverse computation of eval is estimated to run in time O(n3 ) from Fig. 4. The constructed automaton contains O(n) states and O(n2 ) transition rules.
In contrast to reverse and mirror, the implemented second-order pattern matching takes?
O(n2 ) time for each state. The matching k[k[•]] = K takes O(|K|2 ) time; the implemented
algorithm guesses K1 such that K1 [K2 ] = K, in which there are |K| candidates of such?
K1 , and then checks K1 = K2 , which takes O(|K|) time. The matching k1 [k2 [•]] = K also
2
takes O(|K| ) time; the algorithm guesses K1 such that K1 [K2 ] = K (similarly, there are|K| candidates of such K1 ) and takes O(|K|) to check K2 has the form k2 [•].
5.4 toc
From Fig. 4, the estimated complexity of the inverse computation of toc depends on whatkind of trees we give to the inverse computation. The constructed automaton contains O(n)states and O(n2 ) transitions for horizontally-repeated outputs, and contains O(n2 ) states andO(n3 ) transitions for vertically-repeated outputs. Note that the program of toc is converted
to the following context-generating program.
tocc (x) = UL(k[E], E) where k = mkTocc (x)= LI(k1 , k2 [•])
mkTocc (Title(c, s))where k1 = copyc (x), k2 = mkTocc (s)mkTocc (Section(c, s)) = LI(UL(k1 [E], E), k2 [•])
where k1 = mkTocc (c), k2 = mkTocc (s)mkTocc (Paragraph(c, s)) = k1 [k2 [•]]
where k1 = ignorec (c), k2 = mkTocc (s)copyc (A) = A
ignorec (A) = •In horizontally-repeated outputs, which has the form t = UL(LI(A, LI(A, . . . , LI(A, E) . . . )),E), there are at most one k such that UL(k[E], E) = t , while, in a vertically repeated outputs,
which has the form t = UL(LI(. . . UL(LI(A, E), E) . . . , E), E), there are n candidates of k suchthat UL(k[E], E) = t . This difference causes the difference in the number of states.
?

The second-order matching took O(n2 ) time for each state because we solve k1 [k2 [•]] =K which takes O(|K|2 ) time, similar to that in eval.

Higher-Order Symb Comput

5.5 Discussions
In this section, we discuss how we can improve the asymptotic complexity of the implemented algorithm. Again, we use n for the size of an output tree that we focus on.
5.5.1 Pointer-representation of contexts
The prototype implementation uses very naive representation of contexts, i.e., a tree withholes, which takes O(n) space and the check of the equivalence also takes O(n) time. Dueto this cost, the running time of the inverse computation is usually no better than O(n|Q|)
where |Q| is the number of states in the constructed automaton. For example, even for nat in
Example 1, the inverse computation takes O(n2 ) time, in which the second-order matching?
S(k) = t —this is nothing but a first-order matching—can be solved in O(1).
A possible solution to the problem is to represent a m-hole context by (m + 1) pointers(1 for its root and m for its holes). Since a pointer to the output tree t can be expressed inO(log n) space rather than n, it is expected that the representation reduces the cost of introduction of a state of a constructing automaton. Actually, this representation, combined withthe “jumping” technique that will be discussed in Sect. 5.5.2, reduces the cost of the inverse
computation for nat, reverse, while it may increase the cost in some cases as described later.
The procedure for the second-order pattern matching is changed according to the changeof the representation of contexts. Note that we can see a pointer of an output tree as a stateof an automaton representing the output tree. For example, a tree S(S(Z)) can be expressedas an automaton below and each state o of the automaton is essentially a pointer of the tree
(here we subscript each state by the path from the root).
oε ← S(o1 )o1 ← S(o11 )o11 ← Z

Then, a context represented by pointers o0 , o1 , . . . , om where o0 represents its root becomes?
a type o1 → · · · → om → o0 , and the second-order matching problem e = K becomes thetyping problem—finding all the type environment Γ such that Γ e :: τ where τ is a pointerrepresentation of K—in the intersection type system used by Kobayashi [29] with an additional restriction that Γ can have multiple entries of k like k :: τ1 , k :: τ2 ∈ Γ only if τ1
and τ2 represent the same context. Note that the intersection types do not appear explicitly
here because we only consider linear contexts. For example, for e = k1 [k2 [Z]] and τ = oε inthe automaton above, we find the three solutions Γ = {k1 :: oε → oε , k2 :: o11 → oε }, Γ ={k1 :: o1 → oε , k2 :: o11 → o1 } and Γ = {k1 :: o11 → oε , k2 :: o11 → o11 }, and for e = k[k[Z]]and the same τ , we find only one solution Γ = {k :: o1 → oε , k :: o11 → o1 }, which denotes
k is used twice to generate the original output tree where one is used to generate a context
used to generate a tree at oε substituting a tree at o1 to its hole and the other is used to generate a context used to generate a tree at o1 substituting a tree at o11 to its hole, and these twocontexts are the same. Again, the number of the solutions Γ is bounded by a polynomialof the number of the contexts, and thus a polynomial of n. Note that in the above example
we can discard either one of k :: o1 → oε and k :: o11 → o1 because they represent the samecontext.
With this pointer representation, the inverse computation for nat runs in time O(n). To
reduce the cost from O(n) to O(1), we have to know that nat is the identity function on
natural numbers and is surjective, which is an orthogonal story to the discussions in thispaper.

Higher-Order Symb Comput

Note that there is a trade-off between this representation and the naive representation:a context can have n pointer-representations at worst. Thus, although this representation
works effectively for reverse, mirror and toc, the constructed automaton for eval now hasO(n2 ) states and O(n3 ) transitions in the pointer representation. Recall that it has O(n) states
and O(n2 ) transitions in the naive context representation. In the pointer representation, thesame contexts S(•) occurring in different positions are distinguished.
5.5.2 Jumping to arbitrary subtrees
As described above, the pointer representation is sometimes useful to reduce the cost of theautomaton construction. However, to reduce the cost of the inverse computation, we have to
reduce the cost of the second-order matching.
The pointer representation also sheds light on the problem, which enables us to traverse
a tree or context from a leaf or arbitrary positions, while we have to traverse a tree or context from a top in the naive representation. For example, for reverse in which we solve?
the second-order matching problem k1 [Cons(k2 , •)] = t , we have to search Cons(k2 , •) in t
from the top in the naive representation. In contrast, in the pointer representation, the corresponding problem Γ k1 [Cons(k2 , •)] :: o → o can be solved in constant time because wecan “jump” to the hole position by searching transition rule o ← Cons(o , o ).
Finding a good strategy for typing would lead to an efficient second-order matching.
Assuming some strategies such as performing “jumping” as possible, we can find that theinverse computation for reverse runs in time O(n) and that for mirror runs in time O(n2 ).
On the other hand, this technique does not reduce the inverse computation cost for eval.
5.5.3 Special treatment for monadic trees
More optimization can be applicable when the outputs are monadic trees, i.e., trees built
only from unary and nullary constructors such as S(S(Z)) and A(B(A(E))). For monadic
trees we can use integers for pointers.
Sometimes this integer-representation is useful to solve the second-order matching more?
efficiently. Consider the second-order matching k[k[•]] = Sn (•), which, in the integerrepresentation, can be translated to a problem that enumerating Γ such that Γ k[k[•]] ::n → 0 where n represents a pointer to the subtree occurring at depth n, or the subtree accessible from the root by a path with length n. Since the pattern is k[k[•]], weknow that k splits the context n → 0 in the middle. That is, n must be even and Γ ={k :: n/2 → 0, k :: n → n/2}. Thanks to the integer representation, we can find this uniquecandidate of k without investigating the context Sn (•) at all; unlike the pointer representation, we can divide or multiply a “pointer” by a constant in the integer representation. Notethat we still have to check if the types n/2 → 0 and n → n/2 represent the same context ornot. The cost of the second-order matching is reduced from O(n2 ) to O(n).
?
In general, for a second-order matching problem e = K, with the integer representationof contexts, we can represent constraints on “shape”s of the free variables in e by linear
equations and inequalities. For example, from {k :: x0 → x1 , k :: x2 → x3 } k[k[•]] :: x4 →x5 , we obtain a constraint on shape as x1 = x5 ∧ x2 = x4 ∧ x3 = x0 ∧ (x3 − x2 ) = (x1 − x0 ) ∧x0 ≤ x1 ∧ x2 ≤ x3 ∧ x4 ≤ x5 . Solving the constraint for x0 , x1 , x2 , x3 , we get x1 = x5 , x2 =x4 , 2x0 = 2x3 = x4 + x5 . By using the technique, the cost of the second-order matching in
the inverse computation of eval becomes O(n), and thus the cost of the inverse computationof eval becomes O(n3 ) again. This kind of technique is also applicable to list-generating
programs like reverse and mirror, and functions of which outputs are partly monadic.

Higher-Order Symb Comput

The similar optimization technique has been discussed also in the context of parsing of
range concatenation grammars [7] in which users can represent arbitrary number of repetitions of a string. By using the technique, their parsing algorithm accepts 2n repetitions of a,ni.e., a2 , in O(2n ) time.
A much more specialized representation of contexts is applicable for natural numbers
represented by S and Z, i.e., trees built from one unary constructor and one nullary constructor. In this situation, we can represent a context by one natural number; for example,
we can represents a context S(S(•)) by 2. For eval, since there are no more redundant statesin the representation and we can also apply the above optimization techniques to this representation, the inverse computation of eval runs in O(n2 ) time in this representation.
5.5.4 Estimation of shape
In the second-order matching, we have not used the fact that a variable k represents a return
value of a function. Sometimes, we can perform for efficient inverse computation by using
this information.
Consider the following rule of mkTocc , which is one of the auxiliary functions used by
tocc .
mkTocc (Paragraph(c, s)) = k1 [k2 [•]] where k1 = ignorec (c), k2 = mkTocc (s)According to this rule, the inverse computation of toc solves the second-order matching?
k1 [k2 [•]] = K, which has as many solutions as the size of the context K. However, by using
the fact that k1 represents a return value of ignore, we know that k1 must be •. Combining
the fact with other techniques described above, we can solve the second-order matching inconstant time.
Exploiting this kind of information, we can achieve the linear time inverse computation
for mirror. Recall that, even by using pointer representation, the inverse computation of
mirror takes O(n2 ) time because the constructed tree automaton contains O(n2 ) states. ThisO(n2 ) numbers of states come form the rule
mirrorc (x) = k1 [k2 [Nil]] where (k1 , k2 ) = appc , revc (x)According to the rule, the inverse computation of mirror solves the second-order matching?
k1 [k2 [Nil]] = t , which has as many solutions as the size of the output tree t , i.e., O(n) solutions. This is problematic because the inverse computation of each result takes O(n) time,
and the most of them produce no answers but introduce O(n) states to the automaton. By
using the information that app and rev generate the contexts of the same size, we can knowthat there is at most one solution for the matching, which makes the time complexity of theinverse computation of mirror be O(n).
It would be a good future direction to discuss how can we estimate the shape and how
can we use the estimated shape.

6 Extensions
We shall discuss four extensions of the inverse computation.

Higher-Order Symb Comput

6.1 Pattern guards
Sometimes it is useful to define a function with pattern guards. For example, let us consider
extending the simple arithmetic-expression language shown in Sect. 1 to include a conditional expression that branches by checking if a number is even or odd:
data Exp = · · · | CaseParity(Exp, Exp, Exp)
According to the change, eval can also be naturally extended by using pattern guards:eval(x) = evalAcc(x, Z)..
.
evalAcc(CaseParity(x, x1 , x2 ), y) | even(x) = evalAcc(x1 , y)evalAcc(CaseParity(x, x1 , x2 ), y) | odd(x) = evalAcc(x2 , y)Here, we have omitted the definition of even/odd that evaluates n and checks if the result iseven/odd or not. We shall not discuss how they are defined at this point.
This extension can be achieved by using the known notion of MTT called lookahead [15]. With regular look-ahead, we can test an input by using a tree automaton before
we choose a rule. For example, even and odd can be seen as look-ahead because they can be
expressed by the following tree automaton.
even ← Zeroodd ← Oneeven ← Add(even, even)
even ← Add(odd, odd)
odd ← Add(even, odd)
odd ← Add(odd, even)
even ← Dbl(even)
even ← Dbl(odd)even ← CaseParity(even, even, even)
even ← CaseParity(even, even, odd)
even ← CaseParity(odd, even, even)
even ← CaseParity(odd, odd, even)odd ← CaseParity(even, odd, even)odd ← CaseParity(even, odd, odd)
odd ← CaseParity(odd, even, odd)
odd ← CaseParity(odd, odd, odd)

Some pattern guards can be expressed by using regular look-ahead.
To handle regular look-ahead, we have to change the inverse computation method a bit.
Consider a rule of the form,f (x) | q(x) = g(x).
What transition rule should we produce from this f and a given K? Producing a ruleqf −1 (K) ← qg−1 (K) as the method discussed in Sect. 4.3 is unsatisfactory because the rulef (x) | q(x) = g(x) is applicable only if x is accepted in q. Thus, we must embed the lookahead information in the transition rule. This embedding can be naturally expressed by using
an alternating tree automaton [10]:qf −1 (K) ← qg−1 (K) ∧ q
However, using an alternating tree automaton does not fit our purpose because extracting
a tree from an alternating tree automaton takes at worst time exponential to the size of thealternating tree automaton [10]; thus, it is difficult to bound the cost of our inverse computation polynomially to the original output size. Moreover, it also reduces the simplicity of theinverse computation method.

Higher-Order Symb Comput

To keep our inverse computation method simple, we can specialize [35] the functions
in a program to look-ahead as a preprocess. In a specialized program, for any function callg(x, e) in a rule f (p, . . . ) | . . . q(x) · · · = . . . g(x, e) . . . , the domain of the function mustbe accepted by the look-ahead; i.e., [[g]](s, t) = t implies s ∈ [[q]]. Thus, in a specialized
program, look-ahead cannot affect the inverse computation results (recall that programs are
assumed to be nondeleting). For example, the specialized version of evalAcc is
evalAcc(Zero, y) = y..
.
evalAcc(CaseParity(x, x1 , x2 ), y)| even(x) = ignoree (x, ignore(x2 , evalAcc(x1 , y)))| odd(x)= ignoreo (x, ignore(x1 , evalAcc(x2 , y)))Recall that we use ignore because of the restriction that a program must use every input
variable at least once. The functions ignoree and ignoreo are specialized versions of ignore(to even and odd respectively):
ignoree (Zero, y) = yignoree (Add(x1 , x2 ), y)| even(x1 ) ∧ even(x2 ) = ignoree (x1 , ignoree (x2 , y))| odd(x1 ) ∧ odd(x2 ) = ignoreo (x1 , ignoreo (x2 , y))ignoree (Dbl(x), y) = ignore(x)ignoree (CaseParity(x, x1 , x2 ), y)| even(x) ∧ even(x1 ) = ignoree (x, ignoree (x1 , ignore(x2 , y)))| odd(x) ∧ even(x2 ) = ignoreo (x, ignore(x1 , ignoree (x2 , y)))ignoreo (One, y) = y..
.
Here, we have omitted most of the definition of ignoreo . The above program has been simplified by using the fact that every input is either even or odd.
The specialization of a program increases the program size [33, 35]. In the worst case,a specialized program is |Q|N times as big as the original one and the specialization takes
time proportional to the size of the specialized program, assuming that look-ahead is definedby a deterministic [10] tree automaton with the states Q, where N is the maximum arity of
the constructors. Since this only increases the program size, our method still runs in timepolynomial to the size of the original output.
6.2 Bounded use of parameters
The notion of look-ahead can relax the parameter-linearity restriction to finite-copying-inparameter [12]. An MTT is called finite-copying-in-parameter [12] if there is a constant b
such that K obtained by [[f ]](s, •1 , . . . , •m ) = K uses each hole •j (1 ≤ j ≤ m) at mostb times for every function f of arity m + 1 and s. It is known that every finite-copyingin-parameter MTT can be converted into a parameter-linear MTT with look-ahead (see theproof of Lemma 6.3 in [12]). For example, the following MTT copies a parameter zero times
or twice.
f (x) = g(x, A)

g(A, y) = C(y, y) g(B, y) = D

Higher-Order Symb Comput

By using look-ahead, we can convert it into a parameter-linear MTT.
f (x) | q2 (x) = g2 (x, A, A)
f (x) | q0 (x) = g0 (x)g2 (A, y1 , y2 ) = C(y1 , y2 ) q2 ← A
q0 ← Bg0 (B) = D
Here, gi means g that copies the output variable i times and qi means the set of the inputs
for which g copies the output variable i times.
We can easily extend the method in Lemma 6.3 of [12] to generate specialized functions.
A converted program can be (b + 1)MF (N+1) -times as big as the original one, where b is thebound of the parameter copies, N is the maximum arity of the constructors, F is the numberof functions, and M is the maximum arity of the functions.
6.3 Parameter-linear macro forest transducers
A macro forest transducer [41], which is an important extension of a macro tree transducer,
generates forests (roughly speaking, sequences of trees) instead of trees, which enables us
to express XML transformations and serialization programs more directly. Our polynomialtime inverse computation results can be lifted to parameter-linear macro forest transducers.
Unlike macro tree transducers, in macro forest transducers, we can use the sequenceconcatenation “·” in right-hand sides. The function toc defined below is an example of amacro forest transducer, which makes the table-of-contents of a document:
toc(x) = UL(x)mkToc(ε)=ε= LI(copy(x1 )) · mkToc(x2 )mkToc(Title(x1 ) · x2 )mkToc(Paragraph(x1 ) · x2 ) = mkToc(x2 )mkToc(Section(x1 ) · x2 ) = LI(UL(mkToc(x1 ))) · mkToc(x2 )Here, ε denotes the empty sequence, and copy is defined as copy(σ (x1 ) · x2 ) = σ (copy(x1 )) ·copy(x2 ) for any symbol σ and copy(ε) = ε. For an input Title(A) · Section(Title(B) ·Paragraph(. . . )) · Title(C), which represents an XML fragment<title>A</title><section><title>B</title><paragraph>...</paragraph></section><title>C</title>
toc produces an output UL(LI(A) · UL(LI(B)) · LI(C)), which represents the XML fragment
below.
<ul><li>A</li><ul><li>B</li></ul><li>C</li></ul>
In general, a rule of a (stay) macro forest transducer has the form of eitherf (ε, y) = e,f (σ (x1 ) · x2 , y) = e,orf (x, y) = e,where each expression e is defined by the following BNF.
e ::= σ (e1 ) | e1 · e2 | y | f (x, e1 , . . . , em )Higher-Order Symb Comput

A transformation like toc, which does not use accumulation parameters, can be expressedby a macro tree transducer, under some encoding of forests. However, this is not possible
in general [41]; in general two macro tree transducers are required: one generates a forest
in which the concatenations “·” are frozen [47] and the other thaws the frozen concatenations [41]. Thus, an extension is needed if we extend our results to parameter-linear macro
forest transducers.
We also can perform polynomial time inverse computation for (deterministic) parameterlinear macro forest transducers. Recall that the following points are the keys to ourpolynomial-time result.
1. We can see a program as a linear non-accumulative context-generating program.
2. The number of contexts in a given output is bounded by a polynomial to the size of theoutput.
3. The substitutions of eΘ = K can be enumerated in polynomial time. Since the solution
space is bounded polynomially by the second item, the existence of the polynomial-time
checking of the equivalence of two contexts is sufficient.
Regarding Item 1, it is rather clear that we can apply the transformations discussed in
Sect. 4.1 and Sect. 4.2 for macro forest transducers. Regarding Item 2, the number ofm-hole linear contexts in a forest is bounded by O(n2m+2 ) where n is the size of the forest; there are O(n2 ) subforests in a forest of size n similarly to the number of substrings
in a string, and a linear m-hole context can be seen as a forest in which m subforests are
replaced by holes. Item 3 is clear in the standard context representation in which a context
is expressed as a forest with special symbols representing holes.
Note that, for linear macro forest transducers, where the uses of the both input and output variables are linear, polynomial-time inverse computation can be performed simply by
preprocessing. For a linear macro forest transducer, the size of an output forest is boundedlinearly by the size of the input forest, i.e., the transformation is linear size increase [14].
Thus, a linear macro forest transducers is MSO-definable because it is expressed as compositions of MTTs and linear size increase [14]. Since MSO-definable tree transformation
can be represented by a MTT that is both finite-copying-in-the-inputs and finite-copying-inparameter [12], our method becomes applicable with some extra preprocessing as noted in
Sect. 6.2.
6.4 Composing with inverse-image computation
Recall that our inverse computation method returns a set of corresponding inputs as a tree
automaton. To enlarge the class of functions for which polynomial-time inverse computation
can be performed, it is natural to try composing our inverse computation with inverse-image
computation—computation of the set {s | f (s) ∈ T } for a problem f and a given set of
outputs T —which has been studied well in the context of tree transducers (for example,[15, 17, 32]).
However, there are several difficulties on this attempt:– Usually, the inverse-image computation is harder than P. For example, it is known thatthe complexity of the inverse-image computation is EXPTIME-complete even for MTTs
without output variables, which are thus non-accumulative, when T and the result set are
given in tree automata [34].
– A few results are known on polynomial time inverse-image computation. However, somemethod [17] requires that a set of output trees must be given in a deterministic tree automaton; in general, converting a tree automaton to a deterministic one causes exponential
size-blow-up.

Higher-Order Symb Comput– For some programs, polynomial-time inverse-image computation is possible even if we
use a non-deterministic tree automaton to represents a set of outputs. However, composing
these methods sometimes does not increase the expressive power. For example, although
it is not difficult to see that polynomial-time inverse-image computation can be performed
for MSO-definable transducers, the composition of a MSO-definable transducer followed
by a parameter-linear MTT can also be expressed in a parameter-linear MTT [12].
We have to overcome the problems to enlarge the applicability of our method. Luckily, we
can overcome the problems listed above.
– The inverse-image computation method proposed by Frisch and Hosoya [17] runs inpolynomial-time for MTTs with the restriction of finite-input-copying-in-the-inputs [12].
– The method requires deterministic tree automata, but the automata obtained by our inverse computation can be converted to deterministic ones in polynomial time; there is no
exponential size blow-up.
– The composition of a finite-input-copying-in-the-inputs MTT followed by a parameterlinear MTT can express a transformation that cannot be expressed in a single MTT, although the resulting class is artificial.
The following program multiply, which performs multiplication of two natural numbers, isan example for the third item.
multiply(x) = sum(dist(x))
dist(P(x1 , x2 )) = makeList(x1 , nat(x2 ))= NilmakeList(Z, y)
makeList(S(x), y) = Cons(y, makeList(x, y))=Zsum(Nil)sum(Cons(a, x)) = add(a, sum(x))=yadd(Z, y)add(S(x), y) = S(add(x, y))Here, the function nat is the same as that in reverse and mirror. The function multiply defines
a mapping P(Sn (Z), Sm (Z)) → Smn (Z). Note that multiply is defined by a composition of thetwo functions: the one is sum written in a parameter-linear MTT, the other is dist written ina finite-input-copying-in-the-inputs MTT [12].
In the following, we show that the automata obtained by our inverse computation canbe converted to deterministic ones in polynomial time. A tree automaton is called -free if
it contains no rules of the form of q ← q  . A tree automaton is called deterministic [10]if it is -free and its transition rules contain no two different rules q ← σ (q1 , . . . , qn ) andq  ← σ (q1 , . . . , qn ) for any σ and q1 , . . . , qn . Note that we can convert a automaton to an-free one in polynomial-time [10].
A key property here is that, in an automaton obtained by our inverse computation, eachstate has the form qf −1 (K) and it satisfies that s ∈ [[qf −1 (K) ]] if and only if [[f ]](s) =AI(K) (Theorem 1). Using the fact, we obtain the following lemma:
Lemma 2 For any K, K  , f and f  satisfying Ki = Ki and fi = fi for some i,[[qf −1 (K) ]]AI

holds.

∩ [[qf  −1 (K  ) ]]AI=∅

Higher-Order Symb Comput

Proof We prove the lemma by contradiction. Suppose that we have [[qf −1 (K) ]]


AI

∩



[[qf  −1 (K  ) ]]i = fi and Ki = Ki for some i. AcAI

cording to Theorem 1, there exists some s such that [[f ]](s) = K and [[f ]](s) = K  . That ∅ for some f , f , K and K  such that f=

is [[fi ]](s) = Ki and [[fi ]](s) = Ki . Since fi = fi and [[fi ]] is a function because we consider deterministic MTTs, we have Ki = Ki , which contradicts the assumption Ki = Ki . 
The lemma guarantees that the naive subset-construction [10], which converts a tree automaton to a deterministic one, runs in polynomial-time. In the subset-construction, we construct an automaton whose states are represented by sets of states of the input automaton.
A key property is that, in the constructed automaton, every state accepts at least one tree.
Thus, if we apply the subset construction to the resulting automaton of our inverse computation, each state P in the generated automaton does not contain two states qf −1 (K) andqf  −1 (K  ) with Ki = Ki and fi = fi in P . Therefore, the number of states in the constructed
automaton is bounded by the number of mappings from a function f in the original program
to a context K, which is O(nF M ) where n is the size of an original output fed to the inverse
computation, F is the number of functions in the original program and M is the maximum
arity of the functions. Note that the number of states in the resulting automaton of our inverse
computation is also O(nF M ) (see the proof of Theorem 2).
Since we can convert an automaton obtained by our inverse computation to a deterministic one in polynomial-time, we can perform polynomial-time inverse computation for atransformation that is defined by a finite-copying-in-the-inputs MTT followed by a finitecopying-in-parameter MTT.
Note that the class of the transformations defined by a finite-copying-in-the-inputs MTT
followed by a finite-copying-in-parameter MTT is incomparable with that defined by a MTT.
In MTT, we can write a transformation that increases the size of a tree double-exponentiallyas belowdexp(x) = expBin(x, L)= N(y, y)
expBin(Z, y)
expBin(S(x), y) = expBin(x, expBin(x, y))while we cannot express such a transformation in the class of the transformations defined bya finite-copying-in-the-inputs MTT followed by a finite-copying-in-parameter MTT. For a
finite-copying-in-the-inputs MTT, it is not difficult to show that the height of an output tree
is bounded linearly by the size of the input tree, and for a parameter-linear MTT (with lookahead), it is known that the size of an output tree is bounded exponentially by the height of
the input tree [47]. Thus, for the class of the composed transformations, the size of an output
tree is bounded exponentially by the size of the input tree, which excludes dexp.

7 Related work
7.1 Inverse computation
There have been many studies on the inverse computation problem [1, 20, 21, 23, 30,
37, 40, 49]. They can be categorized into those on left-inverse computation and those on
right-inverse computation. Left-inverse computation [20, 21, 23, 30, 40] focuses on injective functions and tries to make an efficient inverse computation based on injectivity analysis, but it can only handle provably-injective functions. Right-inverse computation [1, 37,

Higher-Order Symb Comput

49] including ours can handle more functions than left-inverse computation does—it works
even for non-injective functions—but the yielded inverse-computation process is usuallymuch slower than that of left-inverse computation. Another important difference is that leftinverse computation is compositional; if we have effective left-inverse computation methods
for f and g, we have an effective left-inverse computation method for f ◦ g. On the other
hand, right-inverse computation may not be compositional; even if we have right-inverse
computation methods for f and g, then right-inverse computation may happen to be undecidable for f ◦ g. Left-inverse computation is suitable for applications in which efficiency
is the biggest concern, such as in serialization/deserialization. On the other hand, rightinverse computation is suitable for applications in which one wants to invert non-injectivefunction to enumerate all the corresponding inputs, such as in test-case generation [9, 43].
It is worth noting that checking the injectivity of a function is generally undecidable. For
parameter-linear MTTs in particular, the injectivity check is undecidable even if it has no
output-variables [18] or it has no multiple data traversals (we can reduce the ambiguity checkof a context-free grammar, which is known to be undecidable [24], to the problem). Thus,
any left-inverse computation method essentially has a function written in parameter-linear
MTT that cannot be inverted by it.
To the best of our knowledge, there are few discussions on the topic of multiple data
traversals, except for Eppstein’s work [16]. He demonstrated the usefulness of tupling [8,25] that can make an injective function from non-injective functions.
Regarding accumulations, studies on left-inverse computation have treated them heuristically [20, 39, 40] because the injectivity check is usually undecidable with them. Glück and
Kawabe [20] use the LR-parsing technique. In their system, if the grammar obtained froma program is LR-parsable, inverse program based on LR-parsing is derived. Note that theiruse of grammar is different from our use of tree automaton: their grammar represents a setof possible instruction sequences (traces) of a program while our tree automaton represents
a set of inverse computation results. Nishida and Vidal [40] and Mogensen [39] focus on
the special tail-recursive (thus usually accumulative) pattern and discuss the inverse computation of the pattern. Regarding right-inverse computation, although there are few studies
focusing on accumulative functions, the approaches [17, 32] regarding the inverse-image
computation have a strong connection to this work and will be discussed later in this section.
7.2 Results on tree transducers
We assumed that the programs are deterministic and showed that a tractable inverse computation is possible for parameter-linear MTTs. However, this result does not scale to nondeterministic programs. Even for MTTs without output variables, the problem of checking
whether an inverse-computation result is empty or not is known to be NP-complete [42].
This means the complexity of the inverse computation problem of the nondeterministic MTTs even without output variables is NP-hard. For compositions of (deterministic/nondeterministic) macro tree transducers, checking whether an inverse-computation result is empty or not is known to be in NP [28]; thus the problem is NP-complete for compositions of nondeterministic macro tree transducers. It is still open whether the problem is
NP-hard or not for compositions of deterministic macro tree transducers.
The problem of inverse computation takes a function f and an output tree t and returns the trees s such that f (s) = t . A similar problem, the inverse-image computation
problem—computation of the set {s | f (s) ∈ T } for a given f and T —has been studied ontree transducers (for example, [15, 17, 32]). The difference from the inverse computation

Higher-Order Symb Comput

problem is that the inverse computation takes one tree but inverse-image computation takes
a set of trees, and this difference is a key to our polynomial-time result. The complexity of
the inverse-image computation is EXPTIME-complete even for the parameter-linear MTTs
without output variables which are thus non-accumulative, when T and the result set are
given in tree automata [34]. Roughly speaking, their EXPTIME-hard result is caused by intersections; for an expression like . . . f (x) . . . f (x) . . . we essentially have to compute theintersection {s | f (s) ∈ T1 } ∩ {s | f (s) ∈ T2 } in the inverse-image computation [34]. On theother hand in our method, we do not need to compute the intersection because, for trees t1
and t2 , {s | f (s) = t1 } ∩ {s | f (s) ∈ t2 } equals {s | f (s) = t1 } if t1 = t2 , and otherwise it isempty. This is implicitly expressed by the transformation in Sect. 4.1, in which we replace. . . f (x) . . . f (x) . . . by . . . k . . . k . . . where k = f (x); a multiple data traversal is replacedby an output copying.
The observation that an MTT program is a non-accumulative context-generating transformation plays an important role in our method. A similar but different idea is exploited
in inverse-image computation [17, 32]. Unlike our approach, the idea is to view an MTT
program as a non-accumulative mapping-generating transformation, where a mapping isrepresented by input-output pairs. A context is different from a mapping; it contains more
information than a mapping, e.g., the information about the positions of holes. This difference results in the difference in inverse computation between our context-generation viewand the mapping-generation view. The mapping-generation view considers mappings froma tuple of subtrees of t to a subtree of t for the original output t , which are indeed partiallyapplied functions such as λy.[[f ]](s, y) used to generate t . However, the number of m-ary
mappings on the subtrees of t is exponential to the size of t [17, 32]. Although the inverse
computation based on the mapping-generation view can be performed in polynomial-time
if there are no multiple data traversals [17], it is unclear whether polynomial-time inverse
computation for functions with multiple-data traversals can be achieved or not. In contrast,
we exploit the linearity of the holes—a context contains this information but a mapping does
not—to achieve polynomial-time inverse computation for parameter-linear MTTs, in whicha function can have multiple data traversals. Note that, like m-ary functions, the numberof non-linear m-hole subcontexts in a tree is bounded exponentially by the size of the tree,
whereas the number of linear ones is bounded polynomially by the size.
Regarding inverse computation of general MTTs, there is another polynomial-time inverse computation method besides ours that works for a subset of MTTs. The method of[17], as mentioned in the previous paragraph, runs in polynomial time for MTTs without multiple data traversals, i.e., MTTs with the restriction of finite-input-copying-in-theinputs [12]. In the restricted class of MTTs, we can copy an output unboundedly manytimes but we can traverse an input in only a bounded number of times. For example, reverseand mirror are finite-copying-in-the-inputs, but eval is not. In contrast, our method runsin polynomial time for (deterministic) MTTs with the restriction of finite-copying-in-theoutput (Sect. 6.2), in which we can traverse an input unboundedly many times but we cancopy an output only a bounded number of times. Whether we can perform polynomial-timeinverse computation for general deterministic MTTs or not is still an open problem. It is
worth noting that many useful functions can be written as an MTT in which both the input traversals and the output copies are bounded [12–14, 32], and thus inverse computation
for the functions can be performed in polynomial time both by theirs and ours. Thus, thedifference in expressiveness between ours and other methods is rather small, though not
negligible. However, we claim that our method stands out by being systematic and simple.

Higher-Order Symb Comput

7.3 (Formal) Grammars
In previous work [37], we have suggested an idea for inverse computation: We first find agrammar representing the possible outputs of a program, and then perform inverse computation through the parsing of the grammar. For left-inverse computation, we use an unambiguous grammar that over-approximates the possible outputs of a program, and for right-inverse
computation, we use a grammar that exactly represents the possible outputs of a program
but the grammar need not to be unambiguous. In [37], we have mainly discussed inverse
computation using regular tree grammars [10], and showed that linear-time (right-)inverse
computation is possible for affine and treeless [48] programs. For some subclass of MTTs,
we can achieve polynomial-time inverse computation via parsing; for example, we can use
context-free tree grammars for linear macro tree transducers and we can use IO macro grammars [5] for input-linear MTTs. However, to the best of our knowledge, there is no (tree)grammar that is powerful enough to express the possible outputs (range) of parameter-linear
MTTs and is parsable in polynomial time.
However, this paper borrows the ideas from formal grammars in inverse computation.
In this sense this work is also “grammar-based” as our previous work [37]. Concretely,
we borrow the idea from the parsing algorithm of range concatenation grammars (RCG) [7].
RCG can mimic the ranges of some parameter-linear MTTs. Note that the following programexp, which is a simplified version of ev and eval, is a typical example of transformations thatcannot be handled by the existing inverse computation methods
exp(x) = ex(x, Z)
ex(One, y) = S(y)ex(Dbl(x), y) = ex(x, ex(x, y))We focus on RCG because it can express the possible outputs of exp and there is polynomialtime parsing algorithm. In RCG, we define a grammar by using Horn clauses as follows.
φexp (XY ) ⇐ φexp (X), φexp (Y ), eq(X, Y ).
φexp (a).
eq(aX, aY ) ⇐ eq(X, Y ).
eq(ε, ε).
nThis grammar expresses a set of strings {a2 | n ∈ N}. One might notice that the first rule ofthis grammar has a similar structure to the inverse computation for the rule of exc for Dbl
ex(Dbl(x)) = k[k[•]] where k = ex(x)where ex−1 (K) try to find K  such that K = K  [K  [•]] and then try to compute ex−1 (K  ).
Only the difference is that RCG uses eq explicitly in some reason. (Note that this use of eq
is mandatory in RCG because variables such as X and Y ranges over occurrences of strings(called ranges in [7]) instead of strings themselves, similar to the pointer-representation
discussed in Sect. 5.5.1. But, this difference is ignorable if we do not use the same variable
twice in the left-hand sides and do not allow concatenations in the right-hand sides.) In RCG,
polynomial-time parsing is performed by range-wise memoization. We follow the idea andachieve the polynomial-time inverse computation by context-wise memoization.
One would notice that the idea of the parsing with range-wise memoization is alreadyused Cocke-Younger-Kasami (CYK) parsing [24] for context-free grammars. Indeed, both

Higher-Order Symb Computof the parsing algorithm of RCG and our inverse computation method are extensions of
CYK parsing. We can see a context-free grammar as a transformation from a concrete syntax
tree to the corresponding string, and we can write the transformation by a parameter-linear
MTT. Then, our inverse computation for the transformation behaves as CYK parsing forthe grammar, although the time complexity of the inverse computation depends on what
second-order matching algorithm we use.
It is known that RCG is P-complete, i.e., RCG can express any set of strings of which
membership test is performed in polynomial-time [7]. However, we have not used the fullexpressive power of RCG. Filling this gap is a future direction.

8 Conclusion
We have shown that viewing a function as a context-generating transformation simplifies
inverse computation of accumulative functions with multiple data traversals. Accordingly,
we can achieve systematic polynomial-time inverse computation with small modifications
to the existing techniques.
A future direction is to develop a systematic program inversion method for accumulative
functions based on the view point. Since now an accumulative function can be viewed as
non-accumulative context-generating functions, we hope that we can extend usual rangeanalysis-based program-inversion methods [21, 30, 37] to those functions, and hope that a
program-inversion method developed in this way would be a good alternative to the existing approaches [20, 39, 40]. Another future direction is to develop an inverse computation
method that can handle more kinds of copying. One sort of the interesting copying in practice is those introduced by “join” operation in database query. Although this study is thefirst one to tackle the problem of “copies” in inverse computation, still there is a large gap
between our results and the general “join” functions used in practice. Since tree transducers are hardly able to express “join”-like transformation [38], the next step in our researchwould be to identify what “join”s we should treat by designing an appropriate language.
Acknowledgements We wish to thank Akimasa Morihata, Meng Wang, and Soichiro Hidaka, who gave
us many valuable comments on an earlier version of this work. The discussions in Sect. 5.5.1 are hinted from
Naoki Kobayashi and Takeshi Tsukada. We also thank Janis Voigtländer who pointed out the relationshipbetween Sect. 4.1 and deaccumulation. This work was partially supported by Japan Society for the Promotionof Science, Grant-in-Aid for Research Activity Start-up 22800003, when the first author was in Tohoku
University, and this work is partially supported by Japan Society for the Promotion of Science, Grant-in-Aid
for Young Scientists (B) 24700020.
Open Access This article is distributed under the terms of the Creative Commons Attribution License
which permits any use, distribution, and reproduction in any medium, provided the original author(s) and thesource are credited.

References
1. Abramov, S.M., Glück, R.: Principles of inverse computation and the universal resolving algorithm. In:
Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. Lecture Notes in
Computer Science, vol. 2566, pp. 269–295. Springer, Berlin (2002)
2. Abramov, S.M., Glück, R., Klimov, Y.A.: An universal resolving algorithm for inverse computation oflazy languages. In: Virbitskaite and Voronkov [46], pp. 27–40
3. Albert, E., Vidal, G.: The narrowing-driven approach to functional logic program specialization. New
Gener. Comput. 20(1), 3–26 (2001)
4. Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000)

Higher-Order Symb Comput
5. Asveld, P.R.: Time and space complexity of inside-out macro languages. Int. J. Comput. Math. 10(1),
3–14 (1981)
6. Bird, R.: Introduction to Functional Programming Using Haskell, 2nd edn. Prentice Hall, New York(1998)
7. Boullier, P.: Range concatenation grammars. In: Bunt, H., Carroll, J., Satta, G. (eds.) New Developments
in Parsing Technology. Text, Speech and Language Technology, vol. 23. Kluwer Academic, Dordrecht(2004). Chap. 13
8. Chin, W.-N., Khoo, S.-C., Jones, N.: Redundant call elimination via tupling. Fundam. Inform. 69(1–2),
1–37 (2006)
9. Christiansen, J., Fischer, S.: EasyCheck—test data for free. In: Garrigue, J., Hermenegildo, M.V. (eds.)
FLOPS. Lecture Notes in Computer Science, vol. 4989, pp. 322–336. Springer, Berlin (2008)
10. Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.:
Tree automata techniques and applications (2007). http://www.grappa.univ-lille3.fr/tata
11. Dowek, G.: A second-order pattern matching algorithm for the cube of typed lambda-calculi. In: MFCS,
pp. 151–160 (1991)
12. Engelfriet, J., Maneth, S.: Macro tree transducers, attribute grammars, and MSO definable tree translations. Inf. Comput. 154(1), 34–91 (1999)
13. Engelfriet, J., Maneth, S.: A comparison of pebble tree transducers with macro tree transducers. Acta
Inform. 39(9), 613–698 (2003)
14. Engelfriet, J., Maneth, S.: Macro tree translations of linear size increase are MSO definable. SIAM J.
Comput. 32(4), 950–1006 (2003)
15. Engelfriet, J., Vogler, H.: Macro tree transducers. J. Comput. Syst. Sci. 31(1), 71–146 (1985)
16. Eppstein, D.: A heuristic approach to program inversion. In: IJCAI, pp. 219–221 (1985)
17. Frisch, A., Hosoya, H.: Towards practical typechecking for macro tree transducers. In: Arenas, M.,
Schwartzbach, M.I. (eds.) DBPL. Lecture Notes in Computer Science, vol. 4797, pp. 246–260. Springer,
Berlin (2007). Full version is available as Research Report, RR-6107, INRIA, 2007
18. Fülöp, Z.: Undecidable properties of deterministic top-down tree transducers. Theor. Comput. Sci.
134(2), 311–328 (1994)
19. Giesl, J., Kühnemann, A., Voigtländer, J.: Deaccumulation techniques for improving provability. J. Log.
Algebr. Program. 71(2), 79–113 (2007)
20. Glück, R., Kawabe, M.: Derivation of deterministic inverse programs based on LR parsing. In:
Kameyama, Y., Stuckey, P.J. (eds.) FLOPS. Lecture Notes in Computer Science, vol. 2998, pp. 291–
306. Springer, Berlin (2004)
21. Glück, R., Kawabe, M.: Revisiting an automatic program inverter for lisp. SIGPLAN Not. 40(5), 8–17
(2005)
22. Glück, R., Sørensen, M.H.: Partial deduction and driving are equivalent. In: Hermenegildo, M.V., Penjam, J. (eds.) PLILP. Lecture Notes in Computer Science, vol. 844, pp. 165–181. Springer, Berlin (1994)
23. Gries, D.: The Science of Programming. Springer, Heidelberg (1981). Chap. 21 “Inverting programs”
24. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Prentice Hall, New York (2006). Chap. 7
25. Hu, Z., Iwasaki, H., Takeichi, M., Takano, A.: Tupling calculation eliminates multiple data traversals. In:
ICFP, pp. 164–175 (1997)
26. Huet, G.P.: Résolution d’équations dans les langages d’ordre 1, 2, . . . , ω. PhD thesis, Université de Paris
VII (1976)
27. Huet, G.P., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Inform. 11, 31–55 (1978)
28. Inaba, K., Maneth, S.: The complexity of tree transducer output languages. In: Hariharan, R., Mukund,M., Vinay, V. (eds.) FSTTCS. LIPIcs, vol. 2, pp. 244–255. Schloss Dagstuhl—Leibniz-Zentrum fuer
Informatik (2008)
29. Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In:
Shao, Z., Pierce, B.C. (eds.) POPL, pp. 416–428. ACM, New York (2009)
30. Korf, R.E.: Inversion of applicative programs. In: Hayes, P.J. (ed.) IJCAI, pp. 1007–1009. Kaufmann,
Los Altos (1981)
31. Kühnemann, A., Glück, R., Kakehi, K.: Relating accumulative and non-accumulative functional programs. In: Middeldorp, A. (ed.) RTA. Lecture Notes in Computer Science, vol. 2051, pp. 154–168.
Springer, Berlin (2001)
32. Maneth, S., Nakano, K.: XML type checking for macro tree transducers with holes. In: PLAN-X (2008)
33. Maneth, S., Perst, T., Seidl, H.: Exact XML type checking in polynomial time. In: Schwentick, T., Suciu,
D. (eds.) ICDT. Lecture Notes in Computer Science, vol. 4353, pp. 254–268. Springer, Berlin (2007)
34. Martens, W., Neven, F.: On the complexity of typechecking top-down XML transformations. Theor.
Comput. Sci. 336(1), 153–180 (2005)

Higher-Order Symb Comput
35. Matsuda, K., Hu, Z., Takeichi, M.: Type-based specialization of XML transformations. In: Puebla, G.,
Vidal, G. (eds.) PEPM, pp. 61–72. ACM, New York (2009)
36. Matsuda, K., Inaba, K., Nakano, K.: Polynomial-time inverse computation for accumulative functions
with multiple data traversals. In: Kiselyov, O., Thompson, S. (eds.) PEPM, pp. 5–14. ACM, New York(2012)
37. Matsuda, K., Mu, S.-C., Hu, Z., Takeichi, M.: A grammar-based approach to invertible programs. In:
Gordon, A.D. (ed.) ESOP. Lecture Notes in Computer Science, vol. 6012, pp. 448–467. Springer, Berlin(2010)
38. Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. J. Comput. Syst. Sci. 66(1), 66–97(2003)
39. Mogensen, T.Æ.: Report on an implementation of a semi-inverter. In: Virbitskaite and Voronkov [46],pp. 322–334
40. Nishida, N., Vidal, G.: Program inversion for tail recursive functions. In: Schmidt-Schauß, M. (ed.) RTA.
LIPIcs, vol. 10, pp. 283–298. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik (2011)41. Perst, T., Seidl, H.: Macro forest transducers. Inf. Process. Lett. 89(3), 141–149 (2004)
42. Rounds, W.C.: Complexity of recognition in intermediate-level languages. In: FOCS, pp. 145–158. IEEE
Press, New York (1973)
43. Runciman, C., Naylor, M., Lindblad, F.: SmallCheck and lazy SmallCheck: automatic exhaustive testingfor small values. In: Gill, A. (ed.) Haskell, pp. 37–48. ACM, New York (2008)
44. Salvati, S., de Groote, P.: On the complexity of higher-order matching in the linear lambda-calculus.
In: Nieuwenhuis, R. (ed.) RTA. Lecture Notes in Computer Science, vol. 2706, pp. 234–245. Springer,
Berlin (2003)
45. Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. 8(3), 292–325 (1986)
46. Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics, 6th International Andrei Ershov
Memorial Conference, PSI, Revised Papers, Novosibirsk, Russia, June 27–30, 2006. Lecture Notes in
Computer Science, vol. 4378, Springer, Berlin (2007)
47. Voigtländer, J., Kühnemann, A.: Composition of functions with accumulating parameters. J. Funct. Program. 14(3), 317–363 (2004)
48. Wadler, P.: Deforestation: transforming programs to eliminate trees. Theor. Comput. Sci. 73(2), 231–248(1990)
49. Yellin, D.M.: Attribute Grammar Inversion and Source-to-Source Translation. Lecture Notes in Computer Science, vol. 302. Springer, Berlin (1988)