Lorenzo Clemente
email: l.clemente@mimuw.edu.pl

Paweł Parys
email: parys@mimuw.edu.pl

Sylvain Salvati
email: sylvain.salvati@labri.fr

Igor Walukiewicz

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Keywords: downward closure, separability problem, diagonal problem, higher-order recursion schemes, higher-order OI grammars

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.

Introduction

The diagonal problem is a decision problem with a number of interesting algorithmic consequences. It is a central subproblem for computing the downward closure of languages of words [START_REF] Zetzsche | An approach to computing downward closures[END_REF], as well as for the problem of separability by piecewise-testable languages [START_REF] Czerwiński | A characterization for decidable separability by piecewise testable languages[END_REF]. It is used in deciding reachability of a certain type of parameterized concurrent systems [START_REF] Torre | Safety of parametrized asynchronous shared-memory systems is almost always decidable[END_REF]. In its original formulation over finite words, the problem asks, for a given set of letters Σ and a given language of words L, whether for every number n there is a word in L where every letter from Σ occurs at least n times. In this paper, we study a generalization of the diagonal problem for languages of finite trees recognized by non-deterministic higherorder recursion schemes.

Higher-order recursion schemes are algorithmically manageable abstractions of higher-order programs. Higher-order features are now present in most mainstream languages like Java, JavaScript, Python, or C++. Higher-order schemes, or, equivalently, simply typed lambda-calculus with a fixpoint combinator, are a formalism that can faithfully model the control flow in higher-order programs. In this paper, we consider non-deterministic higher-order recursion schemes as recognizers of languages of finite trees. In other [Copyright notice will appear here once 'preprint' option is removed.] words we consider higher-order OI grammars [START_REF] Damm | The IO-and OI-hierarchies[END_REF][START_REF] Kobele | The IO and OI hierarchies revisited[END_REF]. This is an expressive formalism covering many other models such as indexed grammars [START_REF] Aho | Indexed grammars -an extension of context-free grammars[END_REF], ordered multi-pushdown automata [START_REF] Breveglieri | Multipush-down languages and grammars[END_REF], or the more general higher-order pushdown automata with collapse [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] (cf. also the equivalent model of ordered tree-pushdown automata [START_REF] Clemente | Ordered treepushdown systems[END_REF]).

Our main result is a procedure for solving the diagonal problem for higher-order schemes. This is a missing ingredient to obtain several new decidability results for this model. It is well-known that schemes have a decidable emptiness problem [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF], and it can be shown that they are closed under rational linear transductions, and in particular they form a full trio when restricted to finite word languages. In this context, a result by Zetzsche [START_REF] Zetzsche | An approach to computing downward closures[END_REF] entails computability of the downward closure of languages of words recognized by higher-order schemes. Moreover, a recent result by Czerwiński, Martens, van Rooijen, and Zeitoun [START_REF] Czerwiński | A note on decidable separability by piecewise testable languages[END_REF] entails that the separability by piecewise testable languages is decidable for languages recognized by higher-order schemes. Finally, a third example comes from La Torre, Muscholl, and Walukiewicz [START_REF] Torre | Safety of parametrized asynchronous shared-memory systems is almost always decidable[END_REF] showing how to use downward closures to decide reachability in parameterized asynchronous shared-memory concurrent systems where every process is a higher-order scheme.

While the examples above show that the diagonal problem is intimately connected to downward closures 1 , the computation of the downward closure is an important problem in its own right. The downward closure of a language offers an effective abstraction thereof. Since the subword relation is a well quasi-order [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF], the downward closure of a language is always a regular language determined by a finite set of forbidden patterns. This abstraction is thus particularly interesting for complex languages, like those not having a semilinear Parikh image. While the downward closure is always regular, it is not always possible to effectively construct a finite automaton for it. This is obviously the case for classes with undecidable emptiness (since the downward closure preserves emptiness), but it is also the case for relatively better behaved classes for which the emptiness problem is decidable, such as Church-Rosser languages [START_REF] Gruber | The size of Higman-Haines sets[END_REF], and lossy channel systems [START_REF] Mayr | Undecidable problems in unreliable computations[END_REF].

The problem of computing the downward closure of a language has attracted a considerable attention recently. Early results show how to compute it for context-free languages [START_REF] Courcelle | On constructing obstruction sets of words[END_REF][START_REF] Van Leeuwen | Effective constructions in well-partially-ordered free monoids[END_REF] (cf. also [START_REF] Bachmeier | Finite automata for the sub-and superword closure of CFLs: Descriptional and computational complexity[END_REF]), for Petri-net languages [START_REF] Habermehl | The downward-closure of Petri net languages[END_REF], for stacked counter automata [START_REF] Zetzsche | Computing downward closures for stacked counter automata[END_REF], and context-free FIFO rewriting systems and 0L-systems [START_REF] Abdulla | Effective lossy queue languages[END_REF]. More recently, Zetzsche [START_REF] Zetzsche | An approach to computing downward closures[END_REF] has given an algorithm for indexed grammars, or equivalently for second-order pushdown automata. Hague, Kochems, and Ong [START_REF] Hague | Unboundedness and downward closures of higher-order pushdown automata[END_REF] have made an important further advance by showing how to compute the downward closure of the language of pushdown automata of arbitrary order. In this paper, we complete the picture by giving an algorithm for the more general model of higher-order pushdown automata with collapse [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. We use the fact that these automata recognize the same class of languages as higher-order recursion schemes, and we work with the latter model instead.

Let us briefly outline our approach. While are mainly interested in higher-order recursion schemes (HORSes) generating finite words, for technical reasons we also need to consider narrow trees, i.e., trees with a bounded number of paths. In this we follow an idea of Hague et al. [START_REF] Hague | Unboundedness and downward closures of higher-order pushdown automata[END_REF] who have used this technique for higher-order pushdown automata (without collapse). For a HORS S and a set of letters Σ, the diagonal problem asks whether for every n ∈ N there is a tree generated by S in which every letter from Σ appears at least n times. Our goal is an algorithm solving this problem. When S is of order 0, we have a regular grammar, for which the diagonal problem can be solved by direct inspection. For higher orders, apply a transformation that decreases the order by one. The order is decreased in two steps. First, we ensure that the HORS generates only narrow trees: we construct a HORS S , of the same order as S, generating only narrow trees and such that the diagonal problems for S and S are equivalent. Then, in the narrow HORS S we lower the order by one: we create a HORS S that is of order smaller by one than S (but no longer narrow), and such that the diagonal problems for S and S are equivalent.

While narrowing the HORS is relatively easy to achieve, the main technical difficulty is order reduction. This point is probably better explained in terms of higher-order pushdown automata. If a higher-order pushdown automaton of order n accepts with an empty stack then an accepting computation has no choice but to pop out level-n stacks one by one. In other words, for every configuration the level-n return points are easily predictable. Using this we can eliminate them obtaining an automaton of order n -1. When we allow the collapse operation the situation changes completely: a configuration may have arbitrary many level-n return points, and different computations may use different return points.

In this paper we prefer to use HORSes rather than higher-order pushdown automata with collapse. Our solution resembles the one from [START_REF] Asada | On word and frontier languages of unsafe higher-order grammars[END_REF], where a word-generating HORS is turned into a treegenerating HORS of order lower by one, whose frontier language (the language of words written from left to right in the leaves) is exactly the language of the original word-generating HORS. If our narrow trees were of width one (i.e., word-generating), we could just invoke [START_REF] Asada | On word and frontier languages of unsafe higher-order grammars[END_REF], since their transformation preserves in particular the cardinality of the produced letters. While in general we need to handle narrow trees instead of words (a more general input than in [START_REF] Asada | On word and frontier languages of unsafe higher-order grammars[END_REF]), we only prove that our construction preserves the number of their occurrences (and not their order, thus having a result weaker than in [START_REF] Asada | On word and frontier languages of unsafe higher-order grammars[END_REF]). While the two results are thus formally incomparable, it is worth remarking that our construction does actually preserve the order of symbols belonging to the same branch of the narrow tree.

After some preliminaries in Section 2, we state formally our main result and some of its consequences in Section 3. The rest of the paper is devoted to the proof. In Section 4, we present a transformation of a scheme to a narrow one that preserves the order, and in Section 5 we present the reduction of a narrow scheme to a scheme of a smaller order (but not necessarily narrow). Both reductions preserve the diagonal problem. Finally, in Section 6, we conclude with some further considerations.

Preliminaries

Higher-order recursion schemes. We use the name "sort" instead of "simple type" or "type" to avoid confusion with the types introduced later. The set of sorts is constructed from a unique basic sort o using a binary operation →. Thus o is a sort, and if α, β are sorts, so is α → β. The order of a sort is defined by: ord (o) = 0, and ord (α → β) = max(1 + ord (α), ord (β)). By convention, → associates to the right, i.e., α → β → γ is understood as α → (β → γ). Every sort α can be uniquely written as

α1 → α2 → . . . → αn → o. The sort o → • • • → o → α with r occurrences of o is denoted o r → α, where o 0 → α is simply α.
The set of terms is defined inductively as follows. For each sort α there is a countable set of variables x α , y α , . . . and a countable set of nonterminals A α , B α , . . . ; all of them are terms of sort α. There is also a countable set of letters a, b, . . . ; out of a letter a and a sort α of order at most 1 one can create a symbol a α that is a term of sort α. Moreover, if K and L are terms of sort α → β and α, respectively, then (K L) β is a term of sort β. For α = (o r → o) we often shorten a α to a r , and we call r the rank of a r . Moreover, we omit the sort annotation of variables, nonterminals, or terms, but note that each of them is implicitly assigned a particular sort. We also omit some parentheses when writing terms and denote (. . . (K L1) . . . Ln) simply by KL1 . . . Ln. A term is called closed if it uses no variables.

We deviate here from usual definitions in the detail that letters itself are unranked, and thus out of a single letter a one may create a symbol a r for every rank r. This is convenient for us, as during the transformations of HORSes described in Sections 4 and 5 we need to change the rank of tree nodes, without changing their labels. Notice, however, that in terms a letter is used always with a particular rank.

A higher-order recursion scheme (HORS for short) is a pair S = (Ainit , R), where Ainit is the initial nonterminal that is of sort o, and R is a finite set of rules of the form

A α x α 1 1 . . . x α k k → K o where α = α1 → • • • → α k → o and K is a term that uses only variables from the set {x α 1 1 , . . . , x α k k }.
The order of S is defined as the highest order of a nonterminal for which there is a rule in S. We write R(S) to denote the set of rules of a HORS S. Observe that our schemes are non-deterministic in the sense that R(S) can have many rules with the same nonterminal on the left side. A scheme with at most one rule for each nonterminal is called deterministic.

Let us now describe the dynamics of HORSes. Substitution is defined as expected:

A[M/x] = A, a r [M/x] = a r , x[M/x] = M, y[M/x] = y if y = x, (K L)[M/x] = K[M/x] L[M/x].
We shall use the substitution only when M is closed, so there is no need to perform α-conversion. We also allow simultaneous substitutions: we write K[M1/x1, . . . , M k /x k ] to denote the simultaneous substitution of M1, . . . , M k respectively for x1, . . . , x k . We notice that when the terms Mi are closed, this amounts to apply the substitutions [Mi/xi] (with i ∈ {1, . . . , k}) in any order. A HORS S defines a reduction relation →S on closed terms:

(A x1 . . . x k → K) ∈ R(S) A M1 . . . M k →S K[M1/x1, . . . , M k /x k ] K l →S K l for some l ∈ {1, . . . , r} Ki = K i for all i = l a r K1 . . . Kr →S a r K 1 . . . K r
We thus apply some of the rules of S to one of the outermost nonterminals in the term.

We are interested in finite trees generated by HORSes. A closed term L of sort o is a tree if it does not contain any nonterminal. A HORS S generates a tree L from a term K if K → * S L; when we do not mention the term K we mean generating from the initial nonterminal of S. Since a scheme may have more than one rule for some nonterminals, it may generate more than one tree. We can view a HORS of order 0 essentially as a finite tree automaton, thus a HORS of order 0 generates a regular language of finite trees.

Let ∆ be a finite set of symbols of rank 0 (called also nullary symbols). A tree K is ∆-narrow if it has exactly |∆| leaves, each of them labeled by a different symbol from ∆. A HORS is called ∆-narrow if it generates only ∆-narrow trees, and it is called narrow if it is ∆-narrow for some ∆. We are particularly interested in ∆narrow HORSes for |∆| = 1; trees generated by them consist of a single branch and thus can be seen as words.

Transductions. A (bottom-up, nondeterministic) finite tree transducer (FTT) is a tuple A = (Q, QF , δ), where Q is a finite set of control states, QF ⊆ Q is the set of final states, and δ is a finite set of transitions of the form a r (p1, x1) . . . (pr, xr) -→ q, t or p, x1 -→ q, t (ε-transition)

where a is a letter, p, q, p1, . . . , pr are states, x1, . . . , xr are variables of sort o, and t is a term built of variables from {x1, . . . , x k } ({x1}, respectively) and symbols, but no nonterminals. An FTT A defines in a natural way a binary relation T (A) on trees [START_REF] Comon | Tree automata techniques and applications[END_REF]. We say that an FTT is linear if no term t on the right of transitions contains more than one occurrence of the same variable.

We show that HORSes are closed under linear transductions. The construction relies on the reflection operation [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF], in order to detect unproductive subtrees. A family of word languages is a full trio if it is effectively closed under rational (word) transductions. Since rational transductions on words are a special case of linear tree transductions, we obtain the following corollary of Theorem 2.1.

Corollary 2.2. Languages of finite words recognized by HORSes form a full trio.

The Main Result

We formulate the main result and state some of its consequences. Definition 3.1 (Diagonal problem). For a higher-order recursion scheme S, and a set of letters Σ, the predicate Diag Σ (S) holds if for every n ∈ N there is a tree t generated by S with at least n occurrences of every letter from Σ. The diagonal problem for schemes is to decide whether Diag Σ (S) holds for a given scheme S and a set Σ.

Theorem 3.1. The diagonal problem for higher-order recursion schemes is decidable.

Proof. The proof is by induction on the order of a HORS S. It relies on results from the next two sections. If S has order 0, then S can be converted to an equivalent finite automaton on trees, for which the diagonal problem can be solved by direct inspection. For S of order greater than 0, we first convert S to a narrow HORS S such that Diag Σ (S) holds iff Diag Σ (S ) holds (Theorem 4.1). Then, we employ the construction from Section 5 and obtain a HORS S of order smaller by 1 than the order of S . By Lemmata 5.1 and 5.2: Diag Σ (S ) holds iff Diag Σ (S ) holds.

The main theorem allows to solve some other problems for higher-order schemes. The downward closure of a language of words is the set of its (scattered) subwords. Since the subword relation is a well quasi-order [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF], the downward closure of any language of words is regular. The main theorem implies that the downward closure can be computed for HORSes generating languages of finite words, or, in our terminology, {e 0 }-narrow HORSes, where e 0 is a nullary symbol acting as an end-marker.

Corollary 3.2.

There is an algorithm that given an {e 0 }-narrow HORS S computes a regular expression for the downward closure of the language generated by S.

Proof. By Corollary 2.2, word languages generated by schemes are closed under rational transductions. In this case, Theorem 3.1 together with a result of Zetzsche [START_REF] Zetzsche | An approach to computing downward closures[END_REF] can be used to compute the downward closure of a language generated by a HORS.

Piecewise testable languages of words are boolean combinations of languages of the form Σ * a1Σ * a2 . . . Σ * a k Σ * for some a1, . . . , a k ∈ Σ. Such languages talk about possible orders of occurrences of letters. The problem of separability by piecewise testable languages asks, for two given languages of words, whether there is a piecewise testable language of words containing one language and disjoint from the other. A separating language provides a simple explanation of the disjointness of the two languages [START_REF] Hofman | Separability by short subsequences and subwords[END_REF].

Corollary 3.3.

There is an algorithm that given two {e 0 }-narrow HORSes decides whether there is a piecewise testable language separating the languages of the two HORSes.

Proof. This is an immediate consequence of a result of Czerwiński et al. [START_REF] Czerwiński | A characterization for decidable separability by piecewise testable languages[END_REF] who show that for any class of languages effectively closed under rational transductions, the problem reduces to solving the diagonal problem.

The final example concerns deciding reachability in parameterized asynchronous shared-memory systems [START_REF] Hague | Parameterised pushdown systems with non-atomic writes[END_REF]. In this model one instance of a process, called leader, communicates with an undetermined number of instances of another process, called contributor. The communication is implemented by common registers on which the processes can perform read and write operations; however, operations of the kind of test-and-set are not possible. The reachability problem asks if for some number of instances of the contributor the system has a run writing a designated value to a register.

Corollary 3.4. The reachability problem for parameterized asynchronous shared-memory systems is decidable for systems where leaders and contributors are given by {e 0 }-narrow HORSes.

Proof. La Torre et al. [START_REF] Torre | Safety of parametrized asynchronous shared-memory systems is almost always decidable[END_REF] show how to use the downward closure of the language of the leader to reduce the reachability problem for a parameterized system to the reachability problem for the contributor. Being a full trio is sufficient for this reduction to work.

Narrowing the HORS

The first step in our proof of Theorem 3.1 is to convert a scheme to a narrow scheme. The property of being narrow is essential for the second step, as lowering the order of a scheme works only for narrow schemes. This approach through narrowing has been used by Hague et al. [START_REF] Hague | Unboundedness and downward closures of higher-order pushdown automata[END_REF] for higher-order pushdown automata. Here we deal with recursion schemes, which are equivalent to higher-order pushdown automata with collapse.

The idea behind narrowing is quite intuitive. Consider a binary tree, and suppose that we are interested in the number of occurrences of a certain letter a, that may appear only in leaves. Consider a path that, at each node, selects the subtree containing the larger number of a's, and let's label the node by a if the successor of the node that is not on the path has an a-labeled descendant. Then, if the original tree had n occurrences of a, then on the selected path we put between log n and n labels a. The lower bound holds since, whenever a subtree is selected, at most half of the a's is discarded (on the other subtree), and this happens a number of times equal to the number of a's on the resulting path. This observation implies it suffices to convert a scheme S generating trees to a scheme S generating all paths (words) in the trees generated by S with the additional labeling. Then Diag {a} (S) will be equivalent to Diag {a} (S ).

The general situation is a bit more complicated since we are interested in the diagonal problem not just for a single letter, but for a set of letters Σ. In this case, different letters may have different witnessing paths, so S should generate not a single path but a narrow tree whose number of paths is bounded by |Σ|. Theorem 4.1. For a HORS S and a set of letters Σ, one can construct a set of nullary symbols ∆ of size |Σ| and a ∆-narrow HORS S of the same order as S, such that Diag Σ (S) holds if, and only if, Diag Σ (S ) holds.

Proof. We start by assuming that S uses only symbols of rank 2 and 0, where additionally letters from Σ appear only in leaves. The general situation can be easily reduced to this one, by applying a tree transduction that replaces every node by a small fragment of a tree built of binary symbols, with the original label in a leaf.

Then, we consider a linear bottom-up transducer A from trees produced by S to narrow trees. As labels in the resulting trees we use: (i) new leaf symbols ∆ = {e 0 1 , . . . , e 0 |Σ| }, (ii) unary symbols a 1 for all a ∈ Σ, and (iii) new auxiliary symbols • k (of rank k ≥ 1). For each set of letters Γ ⊆ Σ, A contains a state p ? Γ making sure that each letter from Γ occurs at least once in the input tree. Moreover, for each nonempty set of leaf labels ∆ ⊆ ∆, A contains a state p ∆ that outputs only ∆ -narrow trees. The final state of A is p∆. Transitions are as follows:

(Branch) a 2 (p∆ 1 , x1) (p∆ 2 , x2) -→ p∆ 1 ∪∆ 2 , • 2 x1 x2 , (Leaf) a 0 -→ p {e i 1 ,...,e i k } , • k ei 1 . . . ei k , (Choose1) a 2 (p∆ 1 , x1) (p ? Γ , x2) -→ p∆ 1 , a 1 1 (• • • (a 1 k x1)) , (Choose2) a 2 (p ? Γ , x1) (p∆ 2 , x2) -→ p∆ 2 , a 1 1 (• • • (a 1 k x2)) .
where ∆1 and ∆2 are disjoint subsets of ∆, where i1 < • • • < i k , and where Γ = {a1, . . . , a k } ⊆ Σ. Intuitively, rules of types (Branch) and (Leaf) make sure that we output narrow trees, and rules of types (Choosei) select a branch and output (only) letters that appear at least once in the discarded subtree. States p ?

Γ check that each letter in Γ occurs at least once, as follows:

(Check2) a 2 (p ? Γ 1 , x1) (p ? Γ 2 , x2) -→ p ? Γ 1 ∪Γ 2 , e 0 1 (Check0) a 0 -→ p ? {a} , e 0 1
The set T (p ? Γ )({t}) is either a single leaf or ∅, depending on whether t satisfies the condition or not. The choice of e 0 1 on the right side of the transitions is not important, since, in the way states p ?

Γ are used, it only matters whether the input can be successfully parsed, and not what the output actually is.

It is clear that the image of state p ∆ is always a language of ∆ -narrow trees. Correctness follows from the following claim.

Claim. Let t be an input tree. Then, (i) if t has at least n occurrences of every letter a ∈ Σ, then T (A)(t) contains a tree with at least log n occurrences of every letter a ∈ Σ, and (ii) if T (A)(t) contains a tree with at least n occurrences of every letter a ∈ Σ, then t has at least n occurrences of every letter a ∈ Σ.

To conclude the proof, let T be the transduction T (A) realized by A. By Theorem 2.1, there exists a HORS S of the same order as S with L(S ) = T (L(S)). First, it is clear that L(S ) is a language of ∆-narrow trees. Second, thanks to the claim above, Diag Σ (S) holds if, and only if, Diag Σ (S ) holds.

Lowering the Order

Let S be a ∆-narrow HORS of order k ≥ 1, and let Σ be a finite set of letters. The goal of this section is to construct a HORS S of order k -1 s.t. Diag Σ (S) holds if and only if Diag Σ (S ) holds.

Let • be a fresh letter, not used in S, and not in Σ. We will use it to label auxiliary nodes of trees generated by S . We say that two trees K1, K2 are equivalent if, for each letter a = •, they have the same number of occurrences of a. The resulting HORS S will have the property that for every tree generated by S there exists an equivalent tree generated by S , and for every tree generated by S there exists an equivalent tree generated by S. Then surely Diag Σ (S) holds if and only if Diag Σ (S ) holds.

Let us explain the idea of lowering the order of a scheme on two simple examples. Consider the following transformation on sorts that removes arguments of sort o:

o ↓= o, and (β → γ) ↓= γ ↓ if β = o, (β ↓) → (γ ↓) otherwise.
We have that the order of α ↓ is max(0, ord (α) -1).

Very roughly our construction will take a scheme and produce a scheme of a lower order by changing every nonterminal of sort α to a nonterminal of sort α ↓. This is achieved by outputting immediately arguments of sort o instead of passing them to nonterminals.

Example 1. Consider the scheme

S → F e 0 , F x → x, F x → F (b 1 x) .
This scheme generates words of the form (b 1 ) n e 0 . It can be transformed to an equivalent scheme:

S → • 2 F e 0 F → • 0 F → • 2 F b 0
where we have used a graphical notation for terms; in standard notation the first rule would be S → • 2 F e 0 . Now both b and e are used with rank 0; we have also used auxiliary symbols • 2 and • 0 . Observe that the new scheme has smaller order as the sorts of S and F are o. The new scheme is equivalent to the initial one since a derivation of (b 1 ) n e 0 can be matched by the derivation of a tree with one e 0 and b 0 appearing n times:

• 2 • 2 • 2 • 2 • 0 b 0 b 0 b 0 e 0 n Example 2.
Let us now look at a more complicated example. This time we take the following scheme of order 2:

S → F b 1 e 0 , F g x → g x, F g x → a 1 (F (B g) (c 1 x)), B g x → b 1 (g x) .
Here g has sort o → o, and x has sort o. This scheme generates words of the form (a 1 ) n (b 1 ) n+1 (c 1 ) n e 0 . We transform it into a scheme of order 1:

S → • 2 F b 0 e 0 F g → g F g → • 3 a 0 F (B g ) c 0 B g → • 2 b 0 g
The latter scheme generates trees of the form:

• 2 • 3 a 0 • 3 a 0 t n b c 0 c 0 e 0 n t n b = • 2 b 0 • 2 b 0 • 2 b 0 b 0 n
The intuition behind the above two examples is as follows. Consider some closed term K of sort o, and its subterm L of sort o. In a tree generated by K, the term L will be used to generate some subtrees. Take a tree where L generates exactly k subtrees. Then we can create a new term starting with a symbol • k+1 : in the first subtree we put K with L replaced by • 0 , and in the k remaining subtrees we put L. From this new term we can generate a tree similar to the initial one: the subtrees generated by L are moved closer to the root, but the multisets of letters appearing in the tree do not change. We do this with every subterm of sort o on the right hand side of every rule of S. In the obtained system, whenever an argument has sort o then it is • 0 . Because of this, we can just drop arguments of sort o. This is what our translation α ↓ on sorts does, and this is what happens in the two examples above. Since the original schemes from the two examples generated words, and all arguments were eventually used to generate a subword, for every subterm of sort o the multiplication factor k was always 1.

The crucial part of this argument was the information on the number of times L will be used in K. This is the main technical problem we need to address. We propose a special type system for tracking the use of closures of sort o. It will non-deterministically guess the number of usages, and then enforce derivations that conform to this guess. The reason why such a finite type system can exist is that S is Σ0-narrow, which, in turn, implies that L can be used to generate at most |Σ0| subtrees of a tree.

In the sequel we assume w.l.o.g. that in S the only rule from the initial nonterminal is Ainit → A e 0 1 . . . e 0 |∆| (for some nonterminal A) where ∆ = {e 0 1 , . . . , e 0 |∆| }, and no other rule uses a nullary symbol nor the initial nonterminal Ainit . To ensure this condition, we perform the following simple transformation of the HORS. Every rule B x1 . . .

x k → K in R(S) is replaced by B y1 . . . y |∆| x1 . . . x k → K ,
where K is obtained by replacing in K every use of a symbol e 0 i ∈ ∆ by yi, and every use of a nullary symbol not being in ∆ by an arbitrary yi (this symbol anyway does not appear in any tree generated by S), and every use of a nonterminal C by C y1 . . . y |∆| (the sort of every nonterminal is changed from α to o |∆| → α). Additionally a new rule Ainit → A e 0 1 . . . e 0 |∆| is added, where Ainit is a fresh nonterminal that becomes initial, and A is the nonterminal that was initial previously. It is easy to see that this transformation does not change the set of generated trees. It also does not increase the order, since in this section we assume that S has order at least 1.

Type System

We now present a type system whose main purpose is to track nullary symbols that eventually will end as leaves of a generated tree. The type of a term will say which nullary symbols are already present in the term and which will come from each of its arguments.

For every sort α = (α1

→ • • • → α k → o)
we define the set T α of types of sort α and the set LT α of labeled types of sort α by induction on α. Labeled types in LT α are just pairs (S, τ ) ∈ P(∆) × T α , where if α = o we require that S = ∅. The support of a set Λ of labeled types is the subset Λ =∅ of its elements (S, τ ) ∈ Λ with S = ∅. A set of labeled types Λ is separated if there are no two distinct (S, τ ) and

(S , τ ) in Λ s.t. S ∩ S = ∅. Types in T α are of the form Λ1 → • • • → Λ k → r, where r is a distinguished type corresponding to sort o, Λi is a subset of LT α i for each i ∈ {1, . . . , k} s.t. {Λ =∅ 1 , . . . , Λ =∅ k } are pairwise disjoint and Λ1 ∪ • • • ∪ Λ k is separated.
Let us emphasize that Λi for αi = o can only contain pairs (S, τ ) with S = ∅. We fix some (arbitrary) order < on elements of LT α for every sort α.

Types do not describe all the possible trees generated by a term, but rather restrict the generating power of a term. Intuitively, a labeled type (S0, r) assigned to a closed term of sort o says that we are interested in generating trees that are S0-narrow. A functional type (S0, Λ → τ ) says that the term becomes of type (S, τ ) when taking an argument that will be used only with labeled types from Λ. Here, S equals S0 plus the symbols S1 ∪ • • • ∪ S k generated by an argument of type Λ = {(S1, τ1), . . . , (S k , τ k )}.

A type environment Γ is a set of bindings of variables of the form x α : λ, where λ ∈ LT α ; we may have multiple bindings x α : λ1, . . . , x α : λn for the same variable (which we also abbreviate as x α : {λ1, . . . , λn}), however {λ1, . . . , λn} must be separated in the sense above. A type judgment is of the form Γ M α : λ, where again λ ∈ LT α .

The rules of the type system are given in Figure 1. A derivation is a tree whose nodes are labeled by type judgments constructed according to the rules of the type system (we draw a parent below its children, unlikely the usual convention for trees). For the proof it will be convenient to assume that a derivation is an ordered tree: in the application rule the premise with L is the first sibling followed by the premises with M ordered using our fixed ordering on (Si, τi), without repetitions. We say that D is a derivation for Γ M : λ, or that D derives Γ M : λ, if this type judgment labels the root of D. All the nodes of derivations are required to be labeled by valid type judgments, thus all the restrictions on types from the definition of T α stay in force; in particular, in the application rule for LM , the sets S1, . . . , S k are disjoint.

Transformation

Once we have the type system, we can show how the HORS S is transformed into the HORS S .

A term of type τ will be transformed into a term of sort tr (τ ). This sort is defined by induction on the structure of τ , as follows:

• tr (r) = o, and

• if τ = (Λ → τ ) ∈ T α→β with Λ = {(S1, τ1) < . . . < (S k , τ k )}, then we have tr (τ ) = tr (τ1) → • • • → tr (τ k ) → tr (τ ) if α = o, tr (τ ) if α = o.
We see that if τ ∈ T α , then ord (tr (τ )) = max(0, ord (α) -1). This translation is a refined version of the translation α ↓ on sorts that we have seen earlier in the examples. The nonterminals of S will be the nonterminals of S labeled with types. For every nonterminal A from S, of some sort α, and for every τ such that (∅, τ ) ∈ LT α , in S we consider a nonterminal A τ of sort tr (τ ). Moreover, for every variable x used in S, being of some sort α = o, and for every λ = (S, τ ) ∈ LT α , in S we consider a variable x λ of sort tr (τ ).

Before defining the rules of S , we need to explain how to transform terms to match the transformation on types. This transformation is guided by derivations. We define a term tr (D), where D is a derivation for Γ K : λ, as follows:

• If K = a r is a symbol, then tr (D) = a 0 . • If K = x α is a variable, then tr (D) = • 0 if α = o, and
tr (D) = x λ otherwise.

• If K = A is a nonterminal, then tr (D) = A τ provided that λ = (∅, τ ).

• Suppose that K = L M is an application. Then in D we have a subtree D0 deriving Γ L : (S0, Λ → τ ), where We notice that for λ = (S, τ ) the sort of tr (D) is indeed tr (τ ).

Λ = {λ1 < • • • < λ k },
We see that arguments of sort o are ignored while transforming an application. Because of that, we need to collect the result of the

}, r)} → • • • → {({e 0 |∆| }, r)} → r.
For every other rule of S of the form

A α x α 1 1 . . . x α k
k → K we create a rule in S for every derivation of K. More precisely, for each i ∈ {1, . . . , k} consider the (separated) set of labeled types Λi = {λi,1 < • • • < λi,n i }, where λi,j = (Si,j, τi,j) for every i, j. For every derivation D of the form x1 : Λ1, . . . , x k : Λ k K : ( i∈{1,...,k} j∈{1,...,n i } Si,j, r) we create a rule The correctness of the transformation is described by the following two lemmata, which are proved in the next two subsections. Their statements refer to the notion of equivalence introduced at the beginning of this section.

Aτ x1 . . . x k → merge(tr cum (D)) , where τ = (Λ1 → • • • → Λ k → r) ∈ T α ,
Lemma 5.1 (Soundness). For every tree generated by S there exists an equivalent tree generated by S. Lemma 5.2 (Completeness). For every tree generated by S there exists an equivalent tree generated by S .

Soundness

To prove Lemma 5.1, we follow a sequence of reductions of S , and we construct corresponding reductions of S. We however need to assume that the sequence of reductions in S is leftmost. We write P → lf S P to denote that this is the leftmost reduction: in • k P1 . . . P k we can reduce inside Pi only when in P1, . . . , Pi-1 there are no more nonterminals. Not surprisingly, the order of reductions does not influence the final result, as stated in the following lemma.

Lemma 5.3. Suppose that a tree Q can be reached from a term P using some sequence of reductions of S . Then Q can be reached from P using a sequence of reductions of S of the same length in which all reductions are leftmost.

We need to generalize the definition of equivalence from trees to (lists of) terms of sort o possibly containing nonterminals. We say that two lists of terms of sort o are merge-equivalent if one can be obtained from the other by:

• permuting its elements,

• adding or removing the • 0 term,

• merging/unmerging some list elements using the symbol • k .

The following property of merge-equivalent lists should be clear. Lemma 5.4. Let list and list be two merge-equivalent lists of terms of sort o. Suppose that a tree Q can be generated by S from merge(list). Then some tree Q equivalent to Q can be generated by S from merge(list ) using a sequence of reductions of the same length.

The next lemma contains an important observation, needed later in the proof of Lemma 5.6. Proof. Induction on the structure of K. We consider three cases.

The trivial case is when K is a nonterminal, or a symbol, or a variable other than x. Then K[N/x] = K, so as D we can take DK . Notice that we have m = 0 and that the substitution η does not change neither tr cum (DK ) nor tr (DK ) since variables x λ i do not appear in these terms.

Another easy case is when K = x, and thus (S, τ ) = λ l for some l ∈ {1, . . . , k}. We have m = 1, and i1 = l, and K[N/x] = N . The required derivation D is obtained from D l by prepending the type judgment in every its node by the type environment Γ. A more involved case is when K = L α L M α M . Then in DK , below its root, we have a subtree C0 deriving Γ L : (S0, {(S1, τ1), . . . , (Sn, τn)} → τ ), and for each j ∈ {1, . . . , n} a subtree Cj deriving Γ M : (Sj, τj), where (S1, τ1) < • • • < (Sn, τn), and S0 ∩ (S1 ∪ • • • ∪ Sn) = ∅, and S = S0 ∪ • • • ∪ Sn. We apply the induction assumption to all these subtrees, obtaining a derivation C 0 for Γ L[N/x] : (S0, {(S1, τ1), . . . , (Sn, τn)} → τ ) and for each j ∈ {1, . . . , n} a derivation C j for Γ M [N/x] : (Sj, τj). We compose these derivations into a single derivation D for Γ K[N/x] : (S, τ ) using the application rule. It remains to prove the required equalities about tr cum and tr .

Let us first see that tr Next, we prove that tr cum (D ) is merge-equivalent to the list tr cum (DK )[η]; tr cum (Di 1 ); . . . ; tr cum (Di m ). For each j ∈ {0, . . . , n}, let ij,1 < • • • < ij,m j be those among i ∈ {1, . . . , k} for which in Cj there is a node labeled by Γ

x : λi. By definition tr cum (D ) consists of tr cum (C j ) for j ∈ {0, . . . , n}, and if αK = o then also of tr (D ). The induction assumption implies that tr cum (C j ) is merge-equivalent to tr cum (Cj)[η]; tr cum (Di j,1 ); . . . ; tr cum (Di j,m j ) for each j ∈ {0, . . . , n}. It remains to observe that the concatenation of the lists tr cum (Di j,1 ); . . . ; tr cum (Di j,m j ) for j ∈ {0, . . . , n} is mergeequivalent to tr cum (Di 1 ); . . . ; tr cum (Di m ). By definition every i j,l equals to some i l and every i l equals to some i j,l ; the only question is about duplicates on these lists. Let us write λi = (Ti, σi) for every i ∈ {1, . . . , k}. When some i l is such that Ti l = ∅, then the list tr cum (Di l ) is empty (Lemma 5.5), so anyway we do not have to care about duplicates. On the other hand, when Ti l = ∅ and a node labeled by Γ x : λi l appears in some Cj, then Ti l ⊆ Sj. Since the sets S0, . . . , Sn are disjoint, such node appears in Cj only for one j, and thus such i l equals to only one among the i j,l 's.

We can now formulate and prove the key lemma of this section, allowing us to simulate a single step of S by a single step of S. Proof. We proceed by induction on the structure of L.

Suppose first that L = a r M1 . . . Mr (where surely r ≥ 1). Then D starts with a sequence of r application rules followed by a single-node derivation for a r : (∅, {(S1, r)} → • • • → {(Sr, r)} → r), and by derivations Di for Mi : (Si, r), for each i ∈ {1, . . . , r}. In particular, S1, . . . , Sr are disjoint and their union is S. It holds that tr cum (D) = (a 0 ; tr cum (D1); . . . ; tr cum (Dr)). The reduction merge(tr cum (D)) → lf S P concerns one of terms on one of the lists tr cum (Di), and thus we can write P = merge(a 0 ; list 1 ; . . . ; list r ), where for some l ∈ {1, . . . , r} we have merge(tr cum (D l )) → lf S merge(list l ), and tr cum (Di) = list i for i = l. We apply the induction assumption to M l , obtaining a term M l and a derivation D l for M l : (S l , r) such that M l →S M l and that tr cum (D l ) is merge-equivalent to list l . Taking D i = Di and M i = Mi for i = l, and L = a r M 1 . . . M r , we have L →S L . Out of a node labeled by a r : (∅, {(S1, r)} → • • • → {(Sr, r)} → r) and of derivations D i for i ∈ {1, . . . , r} we compose a derivation D , using the application rule r times. We have tr cum (D ) = (a 0 ; tr cum (D 1 ); . . . ; tr cum (D r )), and thus tr cum (D ) is merge-equivalent to P .

The remaining possibility is that

L = A N α 1 1 . . . N α k k .
Then D starts with a sequence of application rules ending in a single-node derivation for A : (∅, τ ) with τ = {λ1,1, . . . , λ1,n 1 } → . . . , → {λ k,1 , . . . , λ k,n k } → r, and in derivations Di,j for Ni : λi,j, for each i ∈ {1, . . . , k}, j ∈ {1, . . . , ni}. Suppose λi,1 < • • • < λi,n i for every i ∈ {1, . . . , k}, and λi,j = (Si,j, τi,j) for every i, j. Since we consider the leftmost reduction of merge(tr cum (D)), it necessarily concerns its part tr (D) (which is the first term in the list tr cum (D)), that consists of the nonterminal A τ to which some of the terms tr (Di,j) are applied (namely, terms tr (Di,j) for those i for which αi = o). This reduction uses some rule Aτ x1 . . . x k → merge(tr cum (DK )), where in S we have a rule A x1 . . . x k → K, and we have a derivation DK for Γ K : (S, τ ) with Γ = i∈{1,...,k} j∈{1,...,n i } {xi : λi,j}, and where xi denotes xi λ i,1 . . . xi λ i,n i if αi = o and the empty sequence of variables if αi = o (for i ∈ {1, . . . , k}).

As L we take the result of applying the rule A x1 . . .

x k → K to L, i.e. L = K[N1/x1, . . . , N k /x k ].
To construct a derivation for it, we construct derivations Di,K, for K[N1/x1, . . . , N/xi], for i = 1, . . . , k. We take D0,K = DK . To obtain Di,K we apply Lemma 5.6 to Ni, Di-1,K and Di,1, . . . , Di,n i . The derivation D k,K derives Γ L : (S, r). Let D be the derivation for L : (S, r) obtained from D k,K by removing the type environment Γ from type judgments in all its nodes; we obtain a valid derivation since L is closed.

It remains to see that tr cum (D ) is merge-equivalent to P . Let list be the concatenation of lists tr cum (Di,j) for all i ∈ {1, . . . , k}, j ∈ {1, . . . , ni} and let Q = merge(tr cum (DK ))[η1, . . . , η k ] where ηi = (tr (Di,1)/xi λ i,1 , . . . , tr (Di,n i )/xi λ i,n i

) for i ∈ {1, . . . , k}; we see that Q is the result of applying the considered rule to tr (D) (substitutions ηi for i such that αi = o can be skipped, since anyway variables xi λ i,j for such i do not appear in tr (DK )). For i ∈ {1, . . . , k}, let ji,1 < • • • < ji,m i be those among j ∈ {1, . . . , ni} for which in DK there is a node labeled by Γ x : λi,j. By definition tr cum (D) = (tr (D); list), and thus P = merge(Q; list). On the other hand Lemma 5.6 says that tr cum (D ) is merge-equivalent to Q; list , where list is the concatenation of tr cum (Di,j 1 ); . . . ; tr cum (Di,j m i ) for i ∈ {1, . . . , k}. We notice, however, that list = list . Indeed, if

7 2016/5/4
Si,j = ∅ for some i, j, then tr cum (Di,j) is empty by Lemma 5.5. Suppose that Si,j = ∅. The rules of the type system ensure that the subset of ∆ in the root of DK (that is S) is the union of those subsets in all leaves of DK . We have assumed that symbols from ∆ do not appear in K (they are allowed to appear only in the rule from the initial nonterminal). Moreover, Si,j ⊆ S, and all other sets S i ,j are disjoint from Si,j (by the definition of types). Thus necessarily a node labeled by Γ xi : λi,j appears in DK (this is the only way the elements of Si,j can be introduced in S). This means that our j is listed among ji,1, . . . , ji,m i , and hence tr cum (Di,j) appears in list . This proves that list = list , and in consequence that tr cum (D ) is merge-equivalent to P .

Lemma 5.8. Let D be a derivation for L : (S, r) such that merge(tr cum (D)) is a tree. Then L is a tree, and is equivalent to merge(tr cum (D)).

Proof. Induction on the structure of L. If L was of the form A M1 . . . M k , then in D we would necessarily have a node for the nonterminal A, which would imply that merge(tr cum (D)) is not a tree, i.e., it contains a nonterminal. Thus L is of the form a r M1 . . . Mr. Looking at the type system we notice that D necessarily starts with a sequence of r application rules followed by a single-node derivation for a r : (S0, τ0), and derivations Di for Mi : (Si, r), for i ∈ {1, . . . , r}. Recall that tr cum (D) = (a 0 ; tr cum (D1); . . . ; tr cum (Dr)). For i ∈ {1, . . . , r} we know that merge(tr cum (Di)) is a tree; the induction assumption implies that Mi is a tree, and is equivalent to merge(tr cum (Di)). It follows that L is a tree, and is equivalent to merge(tr cum (D)).

Corollary 5.9. Let D be a derivation for L : (S, r), where L does not contain the initial nonterminal. If a tree Q can be generated by S from merge(tr cum (D)), then a tree equivalent to Q can be generated by S from L.

Proof. Induction on the smallest length of a sequence of reductions merge(tr cum (D)) → * S Q. If this length is 0, we apply Lemma 5.8. Suppose that the length is positive. Thanks to Lemma 5.3 we can write merge(tr cum (D)) → lf S P → * S Q (without changing the length of the sequence of reductions). Using Lemma 5.7 we obtain a term L and a derivation D for L : (S, r) such that L →S L and that tr cum (D ) is merge-equivalent to P . The initial nonterminal does not appear in L since by assumption it does not appear on the right side of any rule. Because P → * S Q, by Lemma 5.4 we also have a sequence of reductions of the same length merge(tr cum (D )) → * S Q to some tree Q equivalent to Q; to this sequence of reductions we apply the induction assumption.

Proof of Lemma 5.1. Let n = |∆|. Consider the rule Ainit → A e 0 1 . . . e 0 n from the initial nonterminal of S. Let D be a derivation for A e 0 1 . . . e 0 n : (∆, r) that consists of a node labeled by A : (∅, τ ) with τ = {({e 0 1 }, r)} → . . . → {({e 0 n }, r)} → r, and of nodes labeled by e 0 i : ({e 0 i }, r) for i ∈ {1, . . . , n}, joined together by application rules. We see that tr cum (D) = (Aτ ; e 0 1 ; . . . ; e 0 n ). Take a tree Q generated by S . Since the only rule of S from the initial nonterminal is Ainit → merge(Aτ ; e 0 1 ; . . . ; e 0 n ), the tree Q is generated by S also from merge(tr cum (D)). By Corollary 5.9 a tree Q equivalent to Q can be generated by S from A e 0 1 . . . e 0 n , and thus also from the initial nonterminal.

Completeness

The proof of Lemma 5.2 is similar to the one of Lemma 5.1; we just need to proceed in the opposite direction. Namely, we take a sequence of reductions of S finishing in a finite tree, and then working from the end of the sequence we construct backwards a sequence of reductions of S .

There is one additional difficulty that was absent in the previous subsection: we need some kind of uniqueness of derivations. Indeed, while proceeding forwards from A N1 . . . N k to K[N1/x1, . . . , N k /x k ], we take a derivation for N1 from the single place where N1 appears in the first term, and we put it in multiple places where N1 appears in the second term. This time we proceed backwards, so there are multiple places in the second term where we have a derivation for N1. Our type system can accommodate different derivations for the occurrences of N1 having different types, but for each type we have to ensure that in different occurrences of N1 with this type the derivations are the same. Because of that we only consider maximal derivations.

A derivation D is called maximal if for every internal node of D the following holds: if the label of this node is Γ L M : (S, τ ) and it is possible to derive Γ M : (∅, σ) for some σ, then necessarily this node has a child labeled by Γ M : (∅, σ). The following two lemmata say that it is enough to consider only maximal derivations, and that maximal derivations are unique if we restrict ourselves to labeled types with empty subset of ∆. We will see later that for other types the multiple occurrence problem mentioned above does not occur. Lemma 5.10. If K : (S, τ ) can be derived, then it can be derived by a maximal derivation.

Proof. Let τ = Λ1 → . . . → Λn → r and suppose D is a derivation for K α : (S, τ ). We prove a stronger statement: if T1, . . . , Tn are such that τ = ((Λ1∪({∅}×T1)) → . . . → (Λn∪({∅}×Tn)) → r) is a type in T α then there exists a maximal derivation D for K : (S, τ ). This is shown by induction on the structure of K. Surely K is not a variable, as then a type judgment with empty type environment could not be derived. If K is a nonterminal, then S = ∅, and K : (S, τ ) (for any τ ∈ T α ) can be derived by a single-node derivation; this is a maximal derivation. If K is a symbol, its sort is o n → o; by definition of LT o we know that Ti = ∅ for every i ∈ {1, . . . , n}, which implies τ = τ . Thus D derives K : (S, τ ) and is maximal, since it consists of a single node.

Finally, suppose that K = L M . Then in D we have a subtree Di deriving L : (S0, Λ0 → τ ), and for every λ ∈ Λ0 a subtree D λ deriving M : λ. Let T0 contain those σ for which we can derive M : (∅, σ) but (∅, σ) ∈ Λ0. Then by the induction assumption there exists a maximal derivation D 0 for L : (S0, (Λ0 ∪ ({∅} × T0)) → τ ), and for every λ ∈ (Λ0 ∪ ({∅} × T0)) there exists a maximal derivation D λ for M : λ. By composing these derivations together, we obtain a maximal derivation D for K : (S, τ ): the side condition of the application rule still holds since we have added only derivations for labeled types of the form (∅, σ). Lemma 5.11. For every type judgment of the form Γ K : (∅, τ ) there exists at most one maximal derivation D deriving it.

Proof. By induction on the structure of K. If K is a variable, a symbol, or a nonterminal, then D necessarily consists of a single node labeled by the resulting type judgment, so it is unique. Suppose that K = L M . Then below the root of D, labeled by Γ K : (∅, τ ), we have a subtree D0 deriving Γ L : (∅, {∅} × T → τ ), and for every σ ∈ T a subtree Dσ deriving Γ M : (∅, σ). By maximality, whenever we can derive Γ M : (∅, σ) for some σ, there should be a child of the root of D labeled by Γ M : (∅, σ), and then σ ∈ T . This fixes the set T , and thus the set of child labels. The derivations D0 and Dτ for τ ∈ T are unique by the induction assumption.

After these preparatory results about derivations we come back to our proof. The next lemma deals with the base case: for the last term in a sequence of reductions in S (this term is a narrow tree) we create an equivalent term that will be the last term in the corresponding sequence of reductions in S . Lemma 5.12. Let S ⊆ ∆, and let K be an S-narrow tree. Then there exists a maximal derivation D for K : (S, r) such that merge(tr cum (D)) is a tree equivalent to K.

Proof. We proceed by induction on the structure of K, which is necessarily of the form a r M1 . . . Mr. If r = 0, then S = {a 0 } and we take D to be the single-node derivation for a 0 : ({a 0 }, r); we have tr cum (D) = a 0 . Suppose that r ≥ 1. Then S can be represented as a union of disjoint sets S1, . . . , Sr s.t. Mi is a Si-narrow tree for each i ∈ {1, . . . , r}. By induction, ∀i ∈ {1, . . . , r} we obtain a maximal derivation Di for Mi : (Si, r) s.t. merge(tr cum (Di)) is a tree equivalent to Mi. The derivation D is obtained by deriving a r : (∅, {(S1, r)} → . . . → {(Sr, r)} → r) and attaching D1, . . . , Dr using the application rule r times. Because the Mi's are of sort o, and LT o does not contain pairs of the form (∅, σ), the definition of maximality requires no additional children for the new internal nodes of D, and hence D is maximal. Thus tr cum (D) = (a 0 ; tr cum (D1); . . . ; tr cum (Dr)).

We now describe what happens during a substitution. Proof. We proceed by induction on the structure of K. By Lemma 5.10, for λ ∈ Λ ∅ , there exists a maximal derivation for N : λ, which is unique by Lemma 5.11. We denote this unique derivation by D λ .

We consider three cases. First suppose that K is a nonterminal, or a symbol, or a variable other than x. In this case K[N/x] = K. We take Λ = Λ ∅ , and to obtain DK we just extend the type environment in the only node of D by {x : λ | λ ∈ Λ}. Points 1-2 hold trivially. For points 3-4 we observe that neither tr (DK ) nor tr cum (DK ) contains a variable x λ (so the substitution η does not change these terms); additionally tr cum (D λ ) for λ ∈ Λ are empty (Lemma 5.5).

Next, suppose that K = x. We take Λ = Λ ∅ ∪ {(S, τ )}. As DK we take the single-node derivation for Γ

x : (S, τ ), and as D (S,τ ) we take D in which we remove the type environment from every node. Since N is closed, D (S,τ ) remains a valid derivation and it remains maximal (when (S, τ ) ∈ Λ ∅ , we have already defined D (S,τ ) previously, but these two definitions give the same derivation). Points 1-2 hold trivially. We have tr (D ) = tr (D (S,τ ) ) and tr cum (D ) = tr cum (D (S,τ ) ). We see that tr Finally suppose that K = L α L M α M , which is a more involved case. In D , below its root, we have a subtree C 0 deriving Γ L[N/x] : (S0, {(S1, τ1), . . . , (Sn, τn)} → τ ), and for each j ∈ {1, . . . , n} a subtree C j deriving Γ M [N/x] : (Sj, τj), where (S1, τ1) < • • • < (Sn, τn), and S0 ∩ (S1 ∪ • • • ∪ Sn) = ∅, and S = S0 ∪ • • • ∪ Sn. We apply the induction assumption to all these subtrees, obtaining a maximal derivation C0 for Γ ∪ {x : λ | λ ∈ Λ0} L : (S0, {(S1, τ1), . . . , (Sn, τn)} → τ ) and for each j ∈ {1, . . . , n} a maximal derivation Cj for Γ ∪ {x : λ | λ ∈ Λj} M : (Sj, τj), and for each j ∈ {0, . . . , n} and λ ∈ Λj a maximal derivation D j,λ for N : λ.

Let Λ = j∈{0,...,n} Λj. For λ ∈ Λ ∅ we have already defined D λ , and we have D λ = D j,λ for every j ∈ {0, . . . , n}. Recall that for every λ ∈ Λj \ Λ ∅ there is a node in Cj deriving the labeled type λ, and hence the set on the first coordinate of λ is a subset of Sj (point 2). Since the sets Sj are disjoint, for every λ ∈ Λ \ Λ ∅ there is exactly one j for which λ ∈ Λj, and we define D λ to be D j,λ for this j.

We extend the type environment in every node of every Cj to Γ = Γ ∪ {x : λ | λ ∈ Λ}, and we compose these derivations into a single derivation DK for Γ K : (S, τ ) using the rule for application. In order to see that DK is maximal, take some internal node of DK . Suppose first that this node is contained inside some Cj and it is labeled by Γ P Q, and it is possible to derive Γ Q : (∅, σ). Then it is as well possible to derive Γ ∪ {x : λ | λ ∈ Λj} Q : (∅, σ), because Λ \ Λj contains only labeled types with nonempty set on the first coordinate and they anyway cannot be used while deriving a labeled type with empty set on the first coordinate. Thus by maximality of Cj our node has a child labeled by Γ Q : (∅, σ). Next, consider the root of DK , and suppose that it is possible to derive Γ M : (∅, σ). Then by Lemma 5.6 it is as well possible to derive Γ M [N/x] : (∅, σ), so also Γ M [N/x] : (∅, σ) (since x does not appear in M [N/x]), which by maximality of D means that (∅, σ) is one of (Sj, τj), and thus the root of DK has a child labeled by Γ M : (∅, σ) (created out of the root of Cj).

Points 1, 2 follow from the induction assumption. It remains to prove points 3, 4

. Let Λ = {λ1 < • • • < λ k } and η = (tr (D λ 1 )/x λ 1 , . . . , tr (D λ k )/x λ k ). Similarly, let Λj = {λj,1 < • • • < λ j,k j } and ηj = (tr (D λ j,1 )/x λ j,1 , . . . , tr (D λ j,k )/x λ j,k j
).

Let us first see that tr ; tr cum (D λ j,1 ); . . . ; tr cum (D λ j,k j ) for all j ∈ {0, . . . , n}. We can replace here ηj by η, since tr cum (C j ) does not contain variables x λ with λ ∈ Λ\Λj. To finish the proof it is enough to observe that the concatenation of the lists tr cum (D λ j,1 ); . . . ; tr cum (D λ j,k j ) for j ∈ {0, . . . , n} is mergeequivalent to tr cum (D λ 1 ); . . . ; tr cum (D λ k ). Indeed, for λ ∈ Λ ∅ by Lemma 5.5 tr cum (D λ ) is empty, and, as we have already shown, every λ ∈ Λ \ Λ ∅ belongs to exactly one Λj.

Lemma 5.14. Let D be a maximal derivation for L : (S, r), and let L be a term that does not contain the initial nonterminal of S and such that L →S L . Then there exists a maximal derivation D for L : (S, r) and a term P that is merge-equivalent to tr cum (D ) and such that merge(tr cum (D)) → S P .

The lemma is proved by induction on the structure of L; cf. App. B. The case when L starts with a nonterminal uses Lemma 5.13. Corollary 5.15. Let L be a term that is of sort o and does not contain the initial nonterminal of S, and let M be an S-narrow tree generated by S from L. Then there exists a maximal derivation D for L : (S, r) such that a tree equivalent to M can be generated by S from merge(tr cum (D)).

Proof. We proceed by induction on the smallest length of the sequence of reductions L → * S M . If L = M , we just apply Lemma 5.12. Suppose that the length is positive, and write L →S L → * S M . The initial nonterminal does not appear in L since by assumption it does not appear on the right side of any rule. By induction we obtain a maximal derivation D for L : (S, r) such that a tree Q equivalent to M can be generated by S from merge(tr cum (D )). Then, from Lemma 5.14 we obtain a maximal derivation D for L : (S, r) and a term P that is merge-equivalent to tr cum (D ) and such that merge(tr cum (D)) → S P . By Lemma 5.4 a tree equivalent to Q (and hence to M ) can be generated by S from P , and hence also from merge(tr cum (D)).

Conclusions

This work leaves open the question of the exact complexity of the diagonal problem. The only known lower bound is given by the emptiness problem, that is the same as for the model-checking problem [START_REF] Kobayashi | Complexity of model checking recursion schemes for fragments of the modal mu-calculus[END_REF]. Our procedure is probably not optimal, one of the reasons being the use of reflection in operation Theorem 2.1.

A. Closure under linear transductions and full trio

In this section we prove that finite tree languages generated by HORSes are closed under linear bottom-up tree transductions. An FTT is complete if every variable xi appearing on the left side of any transition also appears in the term t on the right side of the transition, i.e., no subtree is discarded. A restriction is a special case of an FTT where there is only one control state, and where every transition is of the form a r (q,x1) . . . (q, xr) -→ q, b n xi 1 . . . xi n with 1 ≤ i1 < • • • < in ≤ r, i.e., it relabels the tree and discards some its subtrees. Clearly, every FTT is the composition of a complete FTT with a restriction.

A higher-order recursion scheme with states (HORSS) is a triple H = (Q, (qinit , Ainit ), R), where Q is a finite set of control states, (qinit , Ainit ) is the initial process with qinit the initial control state and Ainit the initial nonterminal that is of sort o, and R is a finite set of rules of the form

(I) p, A α 1 →•••→α k →o x α 1 1 • • • x α k k → q, K o (II) p, a r x o 1 • • • x o r → a r (p1, x1) • • • (pr, xr)
where the term K uses only variables from the set {x α 1 1 , . . . , x α k k }. Rules of type (I) are as in standard HORS except that they are guarded by control states. Rules of type (II) correspond to a finite top-down tree automaton reading the tree produced by the HORS. The order of S is defined as the highest order of a nonterminal for which there is a rule in S. Let us now describe the dynamics of HORSSes. A process is a pair (p, M ) where M is a closed term of sort o and p is a state in Q. A process tree is a tree built of symbols and processes, where the latter are seen as symbols of rank 0. K l →H K l for some l ∈ {1, . . . , r} Ki = K i for all i = l a r K1 . . . Kr →H a r K 1 . . . K r We are interested in finite trees generated by HORSSes. A process tree T is a tree if it does not contain any process. A HORSS H generates a tree T from a process (p, M ) if (p, M ) → * H T . The language L(H) is the set of trees generated by the initial process (qinit , Ainit ).

A HORS can be seen as a special case of a HORSS where Q has only one state p with the trivial rule p, a x1

• • • x k → a (p, x1) • • • (p, x k ).
It is well known that this extension does not increase expressive power of HORS, in the sense that given a HORSS H it is possible to construct a (standard) HORS S of the same order as H (but where the arity of nonterminals is increased) such that L(H) = L(S) [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. However, while combining a HORS with an FTT it is convenient to create a HORSS, as its states can be used to simulate states of the FTT.

On the other hand, it is also useful to have the input HORS in a special normalized form, defined next. We say that a HORS is normalized if every its rule is of the form where r ≥ 0, h is either one of the xi's, a nonterminal, or a symbol, and the Bj's are nonterminals. The arity p may be different in each rule. We will not detail the rather standard procedure of transforming any HORS into a normalized HORS without increasing the order.

It amounts to splitting every rule into multiple rules, using fresh nonterminals in the cut points.

Lemma A.1. HORSes are affectively closed under complete linear tree transductions.

Proof. Let S be a HORS and let A be a linear FTT. We construct a HORSS H s.t. L(H) = T (A)(L(S)). The set of control states of H is taken to be the set of control states of the FTT A. As noted above, we can assume w.l.o.g. that S is normalized.

First, if S contains a rule A x → h M1 • • • Mr with h not a symbol, then H contains the rule p, A x → p, h M1 • • • Mr for every control state p.

Next, for every such rule with h being a symbol a r , and for every transition of A having a r on the left side, we take to H one rule illustrated by means of a representative example: if A contains a transition

a 2 (p1, x1) (p2, x2) -→ p, b 2 (c 1 x1) x2
and S contains a rule A y → a 2 (B1 y) (B2 y), then H contains the rule p, A y → b 2 (c 1 (p1, B1 y)) (p2, B2 y) Technically speaking, this is not a HORSS rule, but it can be turned into one type (I) rule and several type (II) rules by adding new states.

Finally, we also add rules corresponding to ε-transitions of A, what is again defined by an example: if A contains a transition p, x1 -→ q, a 1 x1 then, for every nonterminal A of S, H contains the rule q, A y → a 1 (p, A y)

The two inclusions needed to show that L(H) = T (A)(L(S)) can be proved straightforwardly by induction on the length of derivations.

The difficulty in proving closure under possibly non-complete FTTs is that when combining a (non-complete) FTT transition of the form e.g. a 2 (p, x1) (p, x2) -→ p, b 1 x1 with a HORS rule of the form e.g. A y → a 2 (B1 y) (B2 y), we cannot simply discard the subterm B2 y, but we have to make sure that it generates at least one tree on which the FTT has some run. While concentrating on closure only under restrictions, one think becomes easier: a restriction has a run almost on every tree. There is, however, one exception: a restriction A does not have a run on a tree that uses a symbol for which A has no transition. We deal with this in Lemma A.2, below. However, knowing that on every tree there is a run of A is not enough; we also need to know that B2 y generates at least one tree. This problem is resolved by Lemma A.3.

Lemma A.2. For every set of (ranked) symbols Θ and every HORS S we can build a HORS S of the same order, such that L(S ) contains those trees from L(S) which use only symbols from Θ.

Proof. We start by assuming w.l.o.g. that S is normalized. Then, we simply remove from S all rules that use symbols not in Θ. Then surely trees in L(S ) use only symbols from Θ. On the other hand, since S was normalized, every removed rule was of the form A y → a r (B1 y) . . . (Br y) (with a r ∈ Θ), so whenever such a rule was used, an a r -labeled node was created. In consequence, removing these rules has no influence on generating trees that use only symbols from Θ.

A HORS S = (Ainit , R) is productive if, whenever we can reduce Ainit to a term M (which may contain nonterminals), then M can be reduced to some finite tree. By using the reflection operation [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF], we can easily turn a HORS into a productive one.

Theorem 2 . 1 .

 21 HORSes are effectively closed under linear tree transductions.

  and for each i ∈ {1, . . . , k} a subtree Di deriving Γ M : λi. If the sort of M is o, then we take tr (D) = tr (D0); otherwise, tr (D) = tr (D0) tr (D1) . . . tr (D k ).

Figure 1 .Figure 2 .Example 3 .

 123 Figure 1. Type system for tracing nullary symbols in a term

Lemma 5 . 5 .

 55 If D derives K : (∅, τ ), then tr cum (D) is empty. Proof. By induction on the structure of D. Recall that LT o does not contain pairs with ∅ on the first coordinate, so the sort of K is not o, and thus tr cum (D) is defined as the concatenation of tr cum (•) for the subtrees of D starting in the children of the root. When D consists of a single node, we immediately have that tr cum (D) is empty. Otherwise K = L M , and the subtrees of D starting in the children of the root are D0 deriving L : (S0, {(S1, τ1), . . . , (S k , τ k )} → τ ) and Di deriving M : (Si, τi) for i ∈ {1, . . . , k}. Since ∅ = S0 ∪ • • • ∪ S k , we have Si = ∅ for every i ∈ {0, . . . , k}. The induction assumption implies that tr cum (Di) is empty for every i ∈ {0, . . . , k}, and thus tr cum (D) is empty. Before relating reductions in the HORSes, we analyze what happens during a substitution. Lemma 5.6. Consider a derivation DK for Γ K α K : (S, τ ). Suppose all bindings for a variable x αx in Γ are (x : λ1), . . . , (x : λ k ), where λ1 < • • • < λ k , and ({λ1, . . . , λ k } → r) is a type in T αx→o . Suppose also that we have a closed term N αx with, for every i = 1, . . . , k, a derivation Di for N : λi. Then there is a derivation D for Γ K[N/x] : (S, τ ) such that tr cum (D ) is merge-equivalent to tr cum (DK )[η]; tr cum (Di 1 ); . . . ; tr cum (Di m ) where η = (tr (D1)/x λ 1 , . . . , tr (D k )/x λ k ), and i1 < • • • < im are those among i ∈ {1, . . . , k} for which in DK there is a node labeled by Γ x : λi. Moreover, if αK = o then tr (D ) = tr (DK )[η].

  Clearly D remains a valid derivation, and tr (D ) = tr (D l ) and tr cum (D ) = tr cum (D l ). We see that tr cum (DK ) is either the empty list (when αK = o) or • 0 (when αK = o), so attaching tr cum (DK )[η] does not change the class of merge-equivalence. If αK = o, we have tr (DK )[η] = x λ l [η] = tr (D l ).

  (D ) = tr (DK )[η] (not only if αK = o, but also if αK = o). From the induction assumption we know that tr (C 0 ) = tr (C0)[η], as surely αL = o. If αM = o, we simply have tr (D ) = tr (C 0 ) and tr (DK ) = tr (C0), so clearly tr (D ) = tr (DK )[η] holds. If αM = o, from the induction assumption we also know that tr (C j ) = tr (Cj)[η] for every j ∈ {1, . . . , n}; we have tr (D ) = tr (C 0 ) tr (C 1 ) . . . tr (C n ) and similarly tr (DK ) = tr (C0) tr (C1) . . . tr (Cn), so we also obtain tr (D ) = tr (DK )[η].

  Similarly, tr cum (DK )[η] consists of tr cum (C0)[η]; . . . ; tr cum (Cn)[η], and of tr (DK )[η] if αK = o. We have already shown that tr (D ) = tr (DK )[η].

Lemma 5 . 7 .

 57 Let D be a derivation for L : (S, r), where L does not contain the initial nonterminal of S. If merge(tr cum (D)) → lf S P , then there exists a term L and a derivation D for L : (S, r) such that L →S L and tr cum (D ) is merge-equivalent to P .

Lemma 5 . 13 .

 513 Suppose that D is a maximal derivation for Γ K α K [N/x αx ] : (S, τ ), where N is closed. Let Λ ∅ be the set of those (∅, σ) ∈ LT αx for which N : (∅, σ) can be derived. Then there exists a set Λ ∈ LT αx , a maximal derivation DK for Γ K : (S, τ ) with Γ = Γ ∪ {x : λ | λ ∈ Λ}, and for each λ ∈ Λ a maximal derivation D λ for N : λ, such that 1. Λ ∅ ⊆ Λ, 2. for every λ ∈ Λ\Λ ∅ in DK there is a node labeled by Γ x : λ, 3. the list tr cum (D ) is merge-equivalent to the list tr cum (DK )[η]; tr cum (D λ 1 ); . . . ; tr cum (D λ k ), where Λ = {λ1, . . . , λ k } with λ1 < • • • < λ k , and η = (tr (D λ 1 )/x λ 1 , . . . , tr (D λ k )/x λ k ), and 4. if αK = o then also tr (D ) = tr (DK )[η].

  cum (DK ) is either an empty list (when αK = o) or • 0 (when αK = o), so attaching tr cum (DK )[η] does not change the class of merge-equivalence. Moreover tr cum (D λ ) for λ ∈ Λ ∅ are empty (Lemma 5.5), which gives point 3. If αK = o, we have tr (DK )[η] = x (S,τ ) [η] = tr (D (S,τ ) ) = tr (D ) (point 4).

  (D ) = tr (DK )[η] (not only if αK = o, as in point 4, but also if αK = o). By induction we know that tr (C 0 ) = tr (C0)[η0], as surely αL = o. Thus tr (C 0 ) = tr (C0)[η], since tr (C 0 ) (hence also tr (C0)[η0]) does not contain variables x λ , so substituting for them does not change anything. If αM = o, we simply have tr (D ) = tr (C 0 ) and tr (DK ) = tr (C0), so clearly tr (D ) = tr (DK )[η] holds. If αM = o, by induction we also know that tr (C j ) = tr (Cj)[ηj] ∀j ∈ {1, . . . , n}, and thus also tr (C j ) = tr (Cj)[η]; we have tr (D ) = tr (C 0 ) tr (C 1 ) . . . tr (C n ) and similarly tr (DK ) = tr (C0) tr (C1) . . . tr (Cn), so we also obtain tr (D ) = tr (DK )[η]. To show point 3 we prove that tr cum (D ) is merge-equivalent to the list tr cum (DK )[η]; tr cum (D λ 1 ); . . . ; tr cum (D λ k ). By definition tr cum (D ) consists of tr cum (C j ) for j ∈ {0, . . . , n}, and if αK = o then also of tr (D ). Similarly, tr cum (DK )[η] equals to tr cum (C0)[η]; . . . ; tr cum (Cn)[η], prepended by tr (DK )[η] if αK = o. We have already shown that tr (D ) = tr (DK )[η]. By the induction assumption, the list tr cum (C j ) is merge-equivalent to the list tr cum (Cj)[ηj]

Proof of Lemma 5 . 2 .

 52 Consider a tree M generated by S, and a sequence of reductions of S leading to M . In the first step the initial nonterminal reduces to A e 0 1 . . . e 0 |∆| . Corollary 5.15 gives us a derivation D for A e 0 1 . . . e 0 |∆| : (∆, r) such that merge(tr cum (D)) generates a tree equivalent to M . Necessarily tr cum (D) = (Aτ 0 ; e 0 1 ; . . . ; e 0 |∆| ), so merge(tr cum (D)) is obtained as the result of the initial rule of S .

  A HORSS H defines a reduction relation →H on process trees:(p, A x1 . . . x k → q, K) ∈ R(H) (p, A M1 . . . M k ) →H (q, K[M1/x1, . . . , M k /x k ]) (p, a r x1 • • • xr → a (p1, x1) • • • (pr, xr)) ∈ R(H) (p, a r M1 • • • Mr) →H a (p1, M1) • • • (pr, Mr)

A

  x1 . . . xp → h (B1 x1 . . . xp) . . . (Br x1 . . . xp) ,

  and xi denotes xi λ i,1 . . . xi λ i,n i if αi = o, and the empty sequence of variables if αi = o (for i ∈ {1, . . . , k}).

In fact, the diagonal problem, separability by piecewise testable languages, and computing the downward closure are inter-reducible for full trios[START_REF] Czerwiński | A characterization for decidable separability by piecewise testable languages[END_REF].

2016/5/4

2016/5/4

2016/5/4

2016/5/4 Γ, x : λ x : λΓ A : (∅, τ ) Γ a 0 : ({a 0 }, r) r ≥ 1 Γ a r : (∅, {(S1, r)} → • • • → {(Sr, r)} → r) Γ L : (S0, {(S1, τ1), . . . , (S k , τ k )} → τ ) Γ M : (Si, τi) for each i ∈ {1, . . . , k} Γ L M : (S0 ∪ S1 ∪ • • • ∪ S k , τ ) provided that S0 ∩ (S1 ∪ • • • ∪ S k ) = ∅

2016/5/4

2016/5/4

2016/5/4

2016/5/4

2016/5/4

* This work was partially supported by the Polish National Science Centre grant 2013/09/B/ST6/01575. † This work was partially supported by the National Science Center (decision DEC-2012/07/D/ST6/02443). 1 2016/5/4

Lemma A.3. For every HORS S we can build a productive HORS S of the same order generating the same trees.

Proof. First, we construct a deterministic scheme T from the nondeterministic scheme S. To T we will be then able to apply a reflection transformation. We use a letter + to eliminate nondeterminism. For every nonterminal A of S we collect all its rules: A x1 . . . xp → K1, . . . , A x1 . . . xp → Km, and add to T the single rule: A x1 . . . xp → + 2 K1 (+ 2 K2 (. . . (+ 2 Km-1 Km) . . . )) .

The (possibly infinite) tree generated by T represents the language of trees generated from S since the non-deterministic choices that can be made in S are represented by nodes labeled by + in the tree generated by T . In this latter tree, we can find every tree generated by S using a finite number of rewriting steps consisting of replacing a subtree rooted in + by one of its children.

We now take the monotone applicative structure (see [START_REF] Kobele | The IO and OI hierarchies revisited[END_REF][START_REF] Salvati | Using models to model-check recursive schemes[END_REF]) M = (Mα)α∈Sorts where Mo is the two element lattice, with maximal element and minimal element ⊥. Intuitively, means nonempty language and ⊥ means empty language. We interpret + 2 as the join (max) of its arguments, and every other symbol a r as the meet (min) of its arguments; in particular symbols of rank 0 are interpreted as . This allows us to define the semantics [[M, χ, ν]] of a term given a valuation χ for nonterminals and ν for variables (these valuations assign to a variable/nonterminal a value in M of an appropriate sort). The definition of

The meaning of nonterminals in T is given by the least fixpoint computation. For a valuation χ of the nonterminals of T , we write T (χ) for the valuation χ such that

Then the meaning of nonterminals is given by the valuation that is the least fixpoint of this operator: χT = {χ : T (χ) ⊆ χ}. Having χT we can define the semantics of a term M in a valuation ν of its free variables as

Least fixed point models of schemes induce an interpretation on infinite trees by finite approximations. An infinite tree has value iff it represents a non-empty language [START_REF] Kobele | The IO and OI hierarchies revisited[END_REF]. The important point is that the semantics of a term and that of the infinite tree generated from the term coincide.

We can now apply to T the reflection operation [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF] with respect to the above interpretation M. The result is a scheme T that generates the same tree as T but where every node is additionally marked by a tuple (a1, . . . , ar, b) where a1, . . . , ar is the semantics of the arguments of that node (i.e., subtrees rooted at its children) and b is the semantics of the subtree rooted at that node. What is important here is that T has the same order as T which is the same as that of S. The additional labels allow us to remove unproductive parts of the tree generated by T . For this we introduce two more nonterminals Π1 and Π2 of sort o → o → o. We then add the rules Π1 x1 x2 → x1, Π2 x1 x2 → x2. Now we replace every occurrence of + 2 labeled by ( , ⊥, ) by Π1, and every occurrence of + 2 labeled by (⊥, , ) by Π2. After these transformations we obtain a scheme T generating a tree which contains exactly those nodes of T that are labeled with ( , . . . , , ).

We convert T into a HORS S whose language is the same as that of S. For this we replace every remaining occurrence of + 2 (thus labeled by ( , , )) by a nonterminal C of sort o → o → o, and we add two rewrite rules C x y → x and C x y → y. We also remove the additional labels from symbols. By construction, S is productive and L(S ) ⊆ L(S). Moreover, since we only eliminated non-productive nonterminals, L(S ) = L(S).

Lemma A.4. Let S be a productive HORS, and A a restriction such that for every symbol a r appearing in any tree generated by S there is a transition of A having a r on the left side. Then we can build a HORS S whose language is T (A)(L(S)).

Proof. First, w.l.o.g. we assume that S is normalized (notice that while converting a productive HORS to a normalized one, it remains productive). Every rule S y → h (B1 y) . . . (Br y) of S in which h is not a symbol is also taken to S . If h = a r is a symbol, we consider every transition of A having a r on the left side. Since A is a restriction, this transition is of the form

Then, to S we take the rule

In general, T (A)(L(S)) ⊆ L(S ). Since S is productive, the subterms Bi y obtained by rewriting the initial nonterminal Ainit produce at least one tree, and since for every symbol in this tree there is a transition of A having this symbol on the left side, A has some run on this tree. Thus T (A)(L(S)) = L(S ).

Theorem 2.1. HORSes are effectively closed under linear tree transductions.

Proof. A transduction A realized by an FTT is the composition of a complete one B and a restriction C. We first apply Lemma A.1 to the complete transduction realized by B. Then, using Lemma A.2 we remove from the generated language all trees that use symbols not appearing on the left side of any transition of C. Next, we turn the resulting HORS into a productive one by Lemma A.3, and, finally, we apply Lemma A.4 to the resulting productive HORS and the restriction realized by C. We end up with a HORS producing the image of A applied to the original HORS, and being of the same order.

B. Proof of Lemma 5.14

We recall the the statement of the lemma. Lemma 5.14. Let D be a maximal derivation for L : (S, r), and let L be a term that does not contain the initial nonterminal of S and such that L →S L . Then there exists a maximal derivation D for L : (S, r) and a term P that is merge-equivalent to tr cum (D ) and such that merge(tr cum (D)) → S P .

Proof. We proceed by induction on the structure of L.

Suppose first that L = a r M1 . . . Mr (where surely r ≥ 1). Then L = a r M 1 . . . M r , where M l →S M l for some l ∈ {1, . . . , r}, and Mi = M i for all i = l. The derivation D contains a node labeled by a r : (∅, {(S1, r)} → • • • → {(Sr, r)} → r), and for each i ∈ {1, . . . , r} a subtree D i deriving M i : (Si, r) (they are merged together by using the application rule r times), where S1, . . . , Sr are disjoint and their union is S. We apply the induction assumption to M l , obtaining a derivation D l for M l : (S l , r) and a term P l mergeequivalent to tr cum (D l ) and such that merge(tr cum (D l )) → S P l . We can write P l = merge(list l ) (where the length of list l and tr cum (D l ) is the same). We take Di = D i for i = l, and out of the single-node derivation for a r : (∅, {(S1, r)} → • • • → {(Sr, r)} → r) and of derivations Di for i ∈ {1, . . . , r} we compose a derivation D, using the application rule r times. We see that tr cum (D) = (a 0 ; tr cum (D1); . . . ; tr cum (Dr)), and tr cum (D ) = (a 0 ; tr cum (D 1 ); . . . ; tr cum (D r )). Moreover, taking list i = tr cum (Di) for i = l we get merge(tr cum (D)) → S merge(a 0 ; list 1 ; . . . ; list r ), where merge(a 0 ; list 1 ; . . . ; list r ) is merge-equivalent to tr cum (D ). It remains to observe that D is For i ∈ {1, . . . , k}, consecutively, we apply Lemma 5.13 to Di-1,K and Ni, creating sets Λi ⊆ LT α i and maximal derivations Di,K and D i,λ for λ ∈ Λi. Let DK = D k,K ; it derives Γ K : (S, r), where Γ = {xi : λ | i ∈ {1, . . . , k}, λ ∈ Λi}. By point 2 of Lemma 5.13 we know that for every λ ∈ Λi with a nonempty set on the first coordinate, in DK there is a node labeled by Γ xi : λ. On the one hand, since our type systems requires that subsets of Σ0 coming from different children are disjoint, we can be sure that the sets on the first coordinate of labeled types in Λ1, . . . , Λ k are disjoint. It follows that τA = Λ1 → • • • → Λ k → r is a type. On the other hand, nodes labeled by Γ xi : λ give the only possibility for introducing elements of S to our derivation DK (by assumption in K we do not have nullary symbols, since A is not the initial nonterminal), which means that the union of the sets on the first coordinate of labeled types in Λ1, . . . , Λ k is S. Since (S, r) ∈ LT o , we have S = ∅, and thus k ≥ 1, which means that (∅, τA) is a labeled type.

In order to obtain the required derivation D for L : (S, r), we start with the single-node derivation for A : (∅, τA), and using the application rule k times we attach derivations D i,λ for each i ∈ {1, . . . , k} and λ ∈ Λi. This derivation is maximal, since D i,λ were maximal, and by point 1 of Lemma 5.13 the newly created internal nodes have all required children (whenever it is possible to derive a type judgment Ni : (∅, σ), we are deriving it in D).

Recall that tr cum (D) is a concatenation of tr (D) and of tr cum (D i,λ ) for every i ∈ {1, . . . , k} and λ ∈ Λi. For i ∈ {1, . . . , k} let ηi be the substitution that maps xi λ to tr (D i,λ ) for every λ ∈ Λi. In S we have the rule Aτ x1 . . . x k → merge(tr cum (DK )), where xi lists variables xi λ for λ ∈ Λi if αi = o, and is empty if αi = o (for i ∈ {1, . . . , k}). Notice that this rule applied to tr (D) gives merge(tr cum (DK ))[η1, . . . , η k ] (substitutions ηi for i such that αi = o can be skipped, since anyway variables xi λ i,j for such i do not appear in tr cum (DK )). As P we take merge(•) of the concatenation of this term and of all tr cum (D i,λ ); as we have said merge(tr cum (D)) → S P . From point 3 of Lemma 5.13 it follows that tr cum (D ) is mergeequivalent to P , what finishes the proof.