{'fraction_non_alphanumeric': 0.050387653491801604, 'fraction_numerical': 0.009680386631429864, 'mean_word_length': 4.013542200424566, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 35, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Linearity in higher-order recursion schemes

Higher-order recursion schemes (HORS) have recently emerged as a promising foundation for higher-order program verification. We examine the impact of enriching HORS with linear types. To that end, we introduce two frameworks that blend non-linear and linear types: a variant of the λY -calculus and an extension of HORS, called linear HORS (LHORS). First we prove that the two formalisms are equivalent and there exist polynomial-time translations between them. Then, in order to support model-checking of (trees generated by) LHORS, we propose a refined version of alternating parity tree automata, called LNAPTA, whose behaviour depends on information about linearity. We show that the complexity of LNAPTA model-checking for LHORS depends on two type-theoretic parameters: linear order and linear depth. The former is in general smaller than the standard notion of order and ignores linear function spaces. In contrast, the latter measures the depth of linear clusters inside a type. Our main result states that LNAPTA model-checking of LHORS of linear order n is n-EXPTIME-complete, when linear depth is fixed. This generalizes and improves upon the classic result of Ong, which relies on the standard notion of order. To illustrate the significance of the result, we consider two applications: the MSO model-checking problem on variants of HORS with case distinction (RSFD and HORSC) on a finite domain and a call-by-value resource verification problem. In both cases, decidability can be established by translation into HORS, but the implied complexity bounds will be suboptimal due to increases in type order. In contrast, we show that the complexity bounds derived by translations into LHORS and appealing to our result are optimal in that they match the respective hardness results.


INTRODUCTION
Higher-order recursion schemes (HORS) are typed grammars that generate potentially infinite ranked trees. Their history can be tracked back to early research in semantics in the 1970s [Damm 1977;Nivat 1972], but recently they have become a successful foundation for program verification, in the functional paradigm [Kobayashi 2009] and beyond [Tsukada and Kobayashi 2010].
At the theoretical level, the approach takes advantage of the fact that monadic second-order logic (MSO) over trees generated by HORS is decidable [Ong 2006]. In practice, though, various restricted versions of the problem are being considered [Kobayashi 2009;Kobayashi and Ong 2011], notably reachability. Numerous verification tools, e.g. [Broadbent et al. 2013;Murase et al. 2016;Ramsay et al. 2014], have been constructed to test the approach, exploring both type-based and automata-theoretic techniques. Krivine machines have also been exploited in that context [Salvati and Walukiewicz 2016] as well as finite models [Aehlig 2007;Grellois and Melliès 2015a;Hofmann and Ledent 2017;Salvati and Walukiewicz 2015]. Despite the rather disappointing worst-case complexity (n-EXPTIME for MSO model-checking of order-n HORS), experiments paint a more promising story and there is need for identifying better complexity indicators than standard type-theoretic order.
In order to adapt the original results on HORS to more advanced scenarios, it is often necessary to encode desirable features or evaluation mechanisms into the rather crude language of (call-byname) HORS. This often leads to increases in type order, e.g. due to CPS transformations, suggesting drastic changes to expected worst-case complexity. In this paper we introduce linear higher-order recursion schemes (LHORS) that facilitate a more refined type-theoretic analysis and, consequently, make it possible to derive more accurate complexity bounds. This is achieved by mixing linear and non-linear types [Girard 1987]. In order to model-check such schemes, we introduce a special notion of linear non-linear alternating parity automaton (LNAPTA), which are a refinement of alternating parity automata that is sensitive to linearity.
We find that the complexity of LNAPTA model-checking for LHORS is governed by two crucial parameters: linear order and linear depth. In particular, the linear order of a type remains unaffected by linear function spaces and, consequently, can be much smaller than the corresponding standard order of a type. Linear depth, in turn, measures the depth of linear clusters inside a type (by a linear cluster we mean, roughly, a segment of contiguous linear type constructors, separated by non-linear arrows). Our main result states that LNAPTA model-checking of LHORS of linear order n is n-EXPTIME-complete, when linear depth is fixed. This subsumes the result of Ong [2006], as the linear depth of any intuitionistic (non-linear) type is always equal to 0.
Our proof extends the intersection-type approach of Kobayashi [2009] to linear and product types, and takes advantage of the observation that, when it comes to counting type refinements, standard function spaces induce exponential blow-ups in the search space while linear ones do not.
HORS are well known to be equivalent in expressivity to Böhm trees of ground-type λY -calculus terms, under the assumption that their free variables are of at most order 1, which makes it possible to represent leaves and nodes [Salvati and Walukiewicz 2016]. Accordingly, we start our analysis by introducing a calculus, called the λℓY -calculus, that combines the expressivity of λY with a linear type system. The λℓY -calculus will turn out convenient as the target language of translations that aim to take advantage of our type system. To match the calculus, we define linear higher-order recursion schemes (LHORS) and show that they induce the same trees as the λℓY -calculus in a way that preserves linear order and depth. The translations in both directions are of polynomial-time complexity, meaning that the two formalisms can be used interchangeably for the purpose of calculating complexity bounds.
Using the new developments, one can study model-checking problems for formalisms different and richer than HORS by translation into LHORS. We demonstrate this by generalizing several results from the literature. Without the refined analysis afforded by our result, the relevant translations would imply exponential or doubly-exponential cost. In contrast, the complexity bounds that we can derive by translation are optimal and match the respective hardness results.
As applications of the new result, we first revisit two other formalisms used in higher-order model-checking: recursive schemes over finite data domains (RSFD) ] and higher-order recursion schemes with cases (HORSC) [Neatherway et al. 2012]. In both cases, we show how one can translate the associated terms into LHORS in such a way that the linear order will be unaffected by the translation, even though the standard type-theoretic order would. The linear depth will grow during the translation, but only by a constant. This makes it possible to extend Ong's result for order-n HORS [Ong 2006] (i.e. n-EXPTIME-completeness of MSO model-checking) to RSFD and HORSC simply by translation.
Finally, we investigate a call-by-value framework. Here the associated reachability problem was shown to be n-EXPTIME-complete for programs of depth-n in Tsukada and Kobayashi [2014]. We consider the more general resource usage verification problem and also show its n-EXPTIMEcompleteness. In contrast to Tsukada and Kobayashi [2014], our result is obtained through a linear variant of a CPS transformation, which maps call-by-value programs of depth n to call-by-name λℓY -terms of linear order n. CPS translations are known to cause an increase in type order, but in our case linear order does not increase. As the linear depth of the types involved turns out to be constant (equal to 2), our result for LHORS implies the desired complexity.
To sum up, we present a new unifying framework, founded on linear types. The addition of linearity is shown to have far-reaching consequences: (1) our results subsume the original ones on HORS for non-linear types, (2) they provide much more accurate complexity-theoretic bounds than any earlier work, (3) many existing results can be unified and extended simply by translating into the framework.
Consequently, we believe our framework to be highly suitable as a metalanguage for future work in higher-order verification.

THE λℓY -CALCULUS
We start off by introducing the λℓY -calculus, which is a simply-typed λ-calculus extended with a fixpoint combinator (in the spirit of the λY -calculus [Statman 2004]) and refined with a linear-nonlinear type system (in the style of [Barber and Plotkin 1996]). We refer to its types as kinds to avoid collision with the intersection type system to come.

Kinds and Terms
2.1.1 Kinds and Their Measures. The kinds include a ground kind o (the kind of trees), two arrow constructors → (standard non-linear arrow) and ⊸ (linear arrow [Girard 1987]), and products &. Furthermore, we define the kinds as having the following restricted shape.
Definition 1. Kinds are generated by either of φ or ϖ in the following grammar.
with I any finite set ś we write φ & ψ for the binary case.
We refer to kinds generated by φ as functional kinds, and those generated by ϖ as product kinds. Note that any functional kind can be regarded as a (singleton) product kind, so ϖ, κ, ι, . . . really range over arbitrary kinds. Abusing notation, we sometimes identify a functional kind φ and the unary product & {⋆} φ. This allows us to write expressions such as & i ∈I φ i ⇝ ψ , where ⇝ is either ⊸ or → (it is then understood that I is singleton if ⇝=→).
Our restriction on kinds amounts to forbidding products on the left of a non-linear arrow, and on the right of any arrow. However, any non-restricted kind built from {o, ⊸, →, &} is isomorphic to a kind from Definition 1 through the isomorphisms (of Intuitionistic Linear Logic [Girard 1987]): The first two equations hide a combinatorial explosion: converting a non-restricted kind to one in Definition 1 may cause an exponential blow-up. For some of our developments, it will be important that we opt for the notion of kind in Definition 1, with no such hidden complexity.
Measures. The size |κ | and linear order ℓo(κ) of a kind κ are defined inductively: While the definition of size is straightforward, that of linear order deserves a comment. If we ignore the clauses for ⊸ and &, we simply obtain the standard notion of order of a simple type, see e.g. [Salvati and Walukiewicz 2016]. The order is extended to ⊸ and & simply by ignoring the constructors and taking the maximum of the linear order of their operands. This should be natural to the reader familiar with linear logic [Girard 1987]: indeed, recall that the call-by-name Girard translation interprets φ → ψ as !φ ⊸ ψ in linear logic. Hence, one can understand the definition of linear order above as simply counting the maximal nesting of exponentials in the corresponding linear logic formula. A key inspiration for this work is the idea that the main source of complexity in the higher-order model-checking problem is the exponential, and not the arrow in itself.
While our main theorem will substantiate this claim, there will be a proviso because linear kinds, to an extent, do impact complexity. Consequently, to arrive at our asymptotic bounds, we will need to control the use of linear kinds by bounding the extent to which purely linear type constructors can occur contiguously (without being separated by the left-hand side of a non-linear arrow, i.e. by a !). For that purpose we introduce the notion of linear depth of a kind.
Definition 2. The local linear depth lld(κ) of a kind κ is defined inductively as follows The linear depth of κ, written ℓd(κ), is the maximum of lld(ι), taken over all subkinds ι of κ.
Observe that purely non-linear kinds have linear depth 0. We shall see that, even though bounded linear depth increases expressivity, this does not affect the asymptotic complexity of model-checking. In particular, our translations of Sections 5 and 6 will yield kinds with bounded linear depth.

Kinded Terms and Their Measures.
Definition 3. Raw terms are defined as follows.
After Definition 1, we wrote that we will sometimes identify a functional kind φ with the unary product & {⋆} φ. Accordingly, we will also identify a (non-product) term t and the unary tuple ⟨t | i ∈ {⋆}⟩ ś this will enable more uniform notations later on. Our abstractions explicitly carry kinds: the language is à la Church. For notational convenience we have two different function abstractions: one for the linear arrow (ℓ) and another for the nonlinear arrow (λ). This is a superficial distinction: as in this paper we will only consider well-kinded terms, the information of whether an abstraction is linear or not is redundant with the kinds. Now, we give the kinding rules for terms. The kinding judgements of λℓY have the form Γ | ∆ ⊢ u :: κ, where Γ = x 1 :: κ 1 , . . . , x n :: κ n is a non-linear context and ∆ = y 1 :: κ 1 , . . . , y p :: κ p is a linear context. The rules are given in Figure 1. The non-linear context may comprise variables of product kinds ś though these cannot be abstracted, they can be used to compute a fixpoint. Empty contexts are denoted as _. In particular, note that λℓY contains the standard λY -calculus [Statman 2004] as a sub-language: any λY -term Γ ⊢ t : φ can be kinded in λℓY with Γ | _ ⊢ t :: φ.
From now on, all terms are implicitly kinded. We write KT Γ |∆ (κ) for the set of terms Γ | ∆ ⊢ t :: κ. Every subterm of a kinded term t automatically comes with a kind, so we can say whether a subterm u 1 u 2 of t is a linear application (if u 1 has kind ϖ ⊸ φ) or a non-linear one (if u 1 has kind φ → ψ ).
Measures. The linear order of t ∈ KT Γ |∆ (κ), written ℓo(t), is the maximum of all ℓo(κ), where κ ranges over the kinds of subterms of t. The local linear depth of t (written lld(t)) is defined to be lld(ϖ 1 ⊸ . . . ⊸ ϖ n ⊸ κ) where ∆ = x 1 :: ϖ 1 , . . . , x n :: ϖ n . The linear depth ℓd(t) of t is taken to be the maximum of all lld(u), where u ranges over subterms of t. We also define the size of t, written |t |, as follows.
Representing trees. In the λY -calculus or Higher-Order Recursion Schemes, trees are usually represented as normal terms of kind o, using variables of first-order kind. For instance, a variable b : o → · · · → o n → o can be used to represent n-ary branching, i.e. tree nodes with n descendants.
Let Σ be a finite set of such variables. Salvati and Walukiewicz [2016] have shown that Böhm trees of λY -terms of the form Σ ⊢ u : o coincide with the trees generated by order-n recursion schemes, where Σ is taken to be the set of terminal symbols of the scheme.
In λℓY , there is more flexibility as to how branching may be kinded. The role of the first-order kinds of λY (or HORS) will be played by the more general notion of tree kinds, defined below, which Likewise, by applying the above transformation to each kind of a tree signature Σ, we can obtain a first-order signature in the standard sense, written {|Σ| }.
If Σ is a tree signature, any finite tree on {|Σ| } can be presented as a finite term Σ | _ ⊢ t :: o, the latter possibly containing tuples to represent different branches. Note that tuples of terms were introduced to match the linear specification of Σ. Next we define notions of reduction on λℓYterms, and explain how to use them to generate infinite trees represented in an analogous way.

Reduction and Böhm Trees
In this section, we study operational properties of the λℓY -calculus. We define notions of reduction, state its basic properties, and define the Böhm tree (infinite normal form) of a term.
2.2.1 β-reduction and η-contraction. We define as usual a context as a term with a hole, i.e. a term defined by the following grammar: The basic reductions are β-reduction (for linear and non-linear functions, and for products), and η-contraction (again, for all three constructors). The rules are in Figure 2 ś fv(t) denotes the set of free variables in t, either linear or non-linear. We will occasionally refer to η-expansion, the opposite of η-contraction, only defined for terms of appropriate kind. We write ▷ βη for the union of ▷ β , ▷ η . Without any rules for unfolding fixpoints, reduction is strongly normalizing: Proposition 6. The reduction ▷ βη is confluent, and strongly normalizing.
Proof. Immediate by embedding into the simply-typed λ-calculus with surjective pairing, which is well-known to be strongly normalizing [Pottinger 1981]. □ 2.2.2 Unfolding Fixpoints to Böhm Trees. For simplicity, when computing the Böhm tree of a term we will only expand fixpoints in head position. We define the head contexts as follows.
The fixpoint expansion rule is then defined to be Let us write ▷ βηδ for the union of ▷ βη and ▷ δ . Clearly, ▷ δ and ▷ βηδ are no longer normalizing: for instance, we have Yx o . x ▷ δ Yx o . x. However, we retain confluence.
Proof. Elementary reasoning, using determinism of ▷ δ (by construction there is at most one ▷ δ -redex in a term), confluence of ▷ βη and easy commutations properties between ▷ δ and ▷ βη . □ While ▷ βηδ does not necessarily terminate, it will produce a head normal form (i.e. a ▷ βηnormal term of the form H [x] for a variable x) whenever it does. If ▷ βηδ terminates on t, we also say that it is solvable, following standard terminology in λ-calculus. We are now in position to define the Böhm tree of a kinded term.
Böhm trees give a notion of infinite normal forms for λℓY -terms. In this paper, we primarily use it to define the infinite tree generated by a λℓY -term of ground kind with a tree signature.

Infinite
Trees Generated by λℓY -terms. As hinted in Section 2.1.2, all finite ▷ βηδ -normal terms Σ | _ ⊢ t :: o with Σ a tree signature are representations of finite trees on {|Σ| }. This motivates: Definition 9. For any Σ | _ ⊢ t :: o, the infinite tree generated by t is defined as BT(t).
Let us identify tuples with branching and view, for instance, a tree b ⟨T 1 , . . . T n ⟩ as equivalent to the tree b T 1 · · · T n (such transformations will be formalized later as delinearizations of trees). Then, an infinite tree can be generated by a λℓY -term iff it can be generated by a λY -term, or a HORS ś it is straightforward to establish this by providing translations in both directions. However, the trees generated are different if one takes the (linear) order into account. Let us write BT ℓ n for the set of (possibly infinite) trees generated by a λℓY -term of linear order n. We will write BT n for the set of (possibly infinite) trees generated by a λY -term of order n. By [Salvati and Walukiewicz 2016], BT n is equal to the set of trees generated by higher-order recursion schemes of order n. Because any λY -term of order n is also a λℓY -term of linear order n, we can immediately conclude the following: Proposition 10. For all n, we have BT n ⊆ BT ℓ n . However, the other inclusion fails. In particular, we have BT ℓ 0 ⊈ BT 1 . Consider the λℓY -term t given below.
All subterms of t have purely linear kinds, so its linear order is 0. The infinite tree BT(t) generated starts as pictured on the left. The maximal branches of this infinite tree have the form b n c n d n e for all n ∈ N, which is not context-free. Thus, due to the correspondence between order-1 higher-order recursion schemes and pushdown automata (e.g. [Hague et al. 2008]), BT(t) cannot belong to BT 1 . However, it does belong to BT 2 : it is generated by the order-2 HORS and R contains the following rules: Remark 12. As shown above, for schemes, a fixed linear order may turn out to be more expressive than the corresponding standard order. This extra expressivity will turn out to have surprisingly little cost in terms of complexity: we will still be able to show that (under certain constraints) the corresponding model-checking problem is in n-EXPTIME, where n is the linear order. However, there will be a price to pay in terms of the kind of properties that can be verified, as captured by the forthcoming definition of automata (Definition 21).

AN ALTERNATIVE: LINEAR HIGHER-ORDER RECURSION SCHEMES
Higher-order model-checking can be expressed in terms of the λY -calculus, or in terms of higherorder recursion schemes [Salvati and Walukiewicz 2016]. The new framework described earlier was introduced as a generalization of the λY -calculus. Now, we show that it can also be presented as a generalization of HORS, which we call linear higher-order recursion schemes (LHORS).

Definition of LHORS
Though based on terms of λℓY , LHORS are superficially different: rather than having fixpoint operators, they handle recursion through a list of mutually recursive function definitions. Whereas the λℓY -calculus comes from the tradition of the λ-calculus, LHORS (like HORS) are inspired by grammars [Damm 1977] and program schemes [Nivat 1972].
is called applicative if one can derive Γ | ∆ ⊢ ap t :: κ using the kinding rules from Figure 3. An applicative term is necessarily ▷ βηδ -normal. It does not contain any fixpoints or abstractions, and only consists of pairing and applying (projections of) variables from the contexts. We write App Γ |∆ (κ) for the set of applicative terms t such that Γ | ∆ ⊢ ap t :: κ. A linear HORS will associate to every non-terminal a term of the form We call such terms function definitions of kind φ in context Γ, and write Def Γ (φ) for the corresponding set.
Definition 13. A linear HORS (LHORS) is a 4-tuple G = ⟨Σ, N, R, S⟩ where: • Σ is a tree signature, • N is a finite set of kinded non-terminals, with a functional kind; we use upper-case letters F , G, H, . . . to range over them. We denote N (F ) the functional kind of F and write F :: We define some measures on LHORS: the linear order (resp. linear depth) of a LHORS G = ⟨Σ, N, R, S⟩, written ℓo(G) (resp. ℓd(G)), is the maximal linear order (resp. linear depth) of the kinds of its non-terminals in N . Its size is Example 14. The HORS of Figure 11 can be given linear kinds and presented as a LHORS G = ⟨Σ, N, R, S⟩ where Σ is the tree signature given in Example 11, the non-terminals N = {S :: are kinded simply by replacing the non-linear arrows with linear arrows in the HORS of Example 11; and, finally: Given a LHORS G = ⟨Σ, N, R, S⟩ we now define the infinite tree it generates: its value tree. It is possible to do so using an ω-CPO of trees, or using Böhm evaluation, but we favour here an alternative presentation which underlies our proof of soundness and completeness of the intersection type system to come. It is a variant of a relation introduced by Kobayashi and Ong [2009] for proving soundness and completeness of their system. The value tree is computed by iterating a rewriting relation ▷ on applicative terms.
We begin by defining tree contexts: where a is a terminal symbol in Σ. We give a reduction on applicative terms t ∈ App Σ, N |_ (o) by: Definition 15. A linear HORS G is productive when the limit of any potentially infinite sequence of reductions S ▷ R(S) ▷ t 2 ▷ · · · which is fair, i.e. which eventually rewrites everything that can be rewritten, exists. This limit is then called the value tree V(G) of G.
On productivity. In the traditional definition of the value tree of a higher-order recursion scheme as the limit of a sequence of trees, see e.g. [Kobayashi and Ong 2009], the value tree always exists, but may contain a divergence symbol Ω, in which case the HORS is said to be unproductive. Various techniques to detect and enforce productivity exist, one of them using an interpretation of the HORS in an appropriate model [Haddad 2013]. Another possibility, which we adapt here from [Serre 2013, p.61], is to introduce a new unary symbol ε : & {⋆} o ⊸ o in the tree signature Σ, and to replace every reduction rule R(F ) = lx 1 . . . lx n . t with R(F ) = lx 1 . . . lx n . ε t. This can also be applied to a linear HORS G, and always results in a productive linear HORS G ε .
To do model-checking, it then remains to lift the property we want to specify over the tree V(G) and checked by an APTA A to a property checked by an extended APTA A ε over V(G ε ). Several choices are possible. One can, for instance, choose to reject all branches of the form a 1 · · · a n · ε ω (where a n ε), which correspond to branches ending in diverging computation. Dually, one may wish to accept them. We shall take a more liberal approach and let the specifier choose whether a diverging branch a 1 · · · a n · ε ω should be accepted or not depending on the state in which the APTA is when it visits a n . Each of these options can be implemented by building A ε from A through simple modifications, such as additions of new states.
In what follows, we therefore suppose that all linear HORS are productive, replacing G with G ε if needed. This will allow us to build on [Kobayashi and Ong 2009], in which (standard) HORS are all supposed to be productive.

Equivalence of λℓY and LHORS
In the rest of this section, we show that there are polynomial-time transformations between λℓY and LHORS, preserving the linear order and the generated infinite tree.
3.2.1 From LHORS to λℓY . Consider a LHORS G = ⟨Σ, N, R, S⟩, and write N = F 1 :: φ 1 , . . . , F n :: φ n , with S = F i 0 . We are going to emulate the recursive definitions via a single use of the fixpoint, exploiting product kinds in λℓY . We define a term Σ | _ ⊢ R * : & 1≤i ≤n φ i by: Proof. The first equality follows e.g. by co-induction, as the chains of reductions are essentially the same (with a few additional β-reduction steps for G ⊛ ). The second and third conditions can be verified directly. For the last one, we have |G ⊛ | = O(|G| 2 ) because of the substitution. □ This translation from LHORS to λℓY is particularly simple, because the shape of the LHORS recursive definition along with its dynamics can be directly replicated in λℓY thanks to products. In contrast, the correspondence between the λY -calculus and standard HORS is much less direct. In the absence of products, Salvati and Walukiewicz [2016] show how to emulate a HORS by a sequence of fixpoint definitions. However, the approach involves a sequence of substitutions that may cause an explonential blow-up, meaning that the outcome need not be of polynomial size.
3.2.2 From λℓY to LHORS. The translation from λℓY to LHORS will proceed along the lines of [Salvati and Walukiewicz 2016], with complications due to linear variables and products. Another difference is that op. cit. performs β-reduction first, in order to focus on translating β-normal terms. In contrast, we do not rely on prior β-reduction, so as to obtain a polynomial-time transformation.
Lemma 17. For any Σ, Γ | ∆ ⊢ t :: κ, there exist t ⊙ , N, F such that N = {F 1 :: φ 1 , . . . , F n :: φ n } is a set of kinded non-terminals, t ⊙ is an applicative term satisfying Σ, Γ, N | ∆ ⊢ ap t ⊙ :: φ, and F associates to each Proof. For the transformation to LHORS, it suffices to have the above transformation for terms Σ | _ ⊢ t :: o, but the more general statement given permits a direct proof by induction on t.
Given Σ | _ ⊢ t :: o, for every subterm u of t of the form λx φ . u ′ , ℓx κ . u ′ or Yx κ . u ′ , we are going to introduce a non-terminal F u in N , so as to replace u with F u . However, we cannot quite do that, because u ′ is not closed (not counting variables in Σ). Hence, we perform λ-lifting on the fly. □ As a consequence, we obtain: Proof. By Lemma 17, there are (t ⊙ , N, F ) as above (write N = F 1 :: φ 1 , . . . , F n :: φ n ). Set We almost got a linear recursion scheme, except that the F (F i ) are not necessarily η-expanded. We can perform η-expansion in polynomial time, This completes the proof of the equivalence between λℓY and LHORS. Not only have we proved that, for any linear order n, the λℓY -terms and the LHORS of linear order n generate the same trees, but also we have established that the translations in both directions preserve linear depth and cause only a polynomial increase in size. We stress that they can be computed in polynomial time. Therefore, λℓY and LHORS are completely interchangeable from the point of view of the higherorder model-checking problem. When developing the model-checking algorithm via intersection type in the next section, we will work with LHORS. As their structure is more constrained, they provide a more comfortable setting for our analysis. On the other hand, when using the result, we will appeal to the more liberal λℓY -calculus as a target for translations, in Sections 5 and 6.

Linear-Nonlinear Alternating Parity Tree Automata
From alternating parity tree automata to intersection types. Higher-order model-checking has traditionally considered the verification of MSO (equivalently, modal µ-calculus) formulñ over the infinite trees generated by HORS. The problem is typically solved by translating the formula of interest into an equivalent alternating parity tree automaton (APTA), and then lifting the behaviour of this APTA from trees to HORS. Below we recall the connection between APTA and intersection types, which was first made in [Kobayashi 2009] for Büchi automata and then extended to APTA in [Kobayashi and Ong 2009]. A typical transition of an APTA over a binary symbol a :: , meaning that when the APTA encounters a in state q, it can choose nondeterministically between the following: • (1, q 0 ), which visits only the first subtree (the left child of a) in state q 0 , and drops the other subtree so that the run-tree will have only one child at the current position; • (2, q 1 ) ∧ (2, q 2 ), which drops the first subtree and visits the second one twice, duplicating it in the run-tree (starting an execution from state q 1 in one copy and from state q 2 in the other). This behaviour allowing duplication or erasure during the run of an automaton is called alternation. Its connections with linear logic have been studied in [Grellois and Melliès 2015b]. In addition, APTAs use a parity condition: a function Ω attributes a colour Ω(q) ∈ N to each state q ∈ Q. Then, a run-tree is accepting if and only if the maximal colour seen infinitely often along each branch is even. When there is an accepting run-tree, the tree over which the APTA runs satisfies the MSO property checked by the automaton. Kobayashi and Ong observed that the transition mentioned above amounts to typing the symbol a with the intersection types a : □ Ω(q i ) q i → q in a type system that we are about to define (our precise formulation is informed by later work [Grellois and Melliès 2015b]). In this way, they gave a correspondence between APTAs and sets of intersection types for terminals. Accordingly, every (accepting) run-tree of an APTA over a tree t can be translated to a (winning) typing derivation in the intersection type system, see for instance [Grellois 2016]. In what follows, exploiting this type-theoretic intuition, we redefine APTA and define LNAPTA as sets of typings rather than usual transition-based definitions.
Intersection types refining kinds. In [Kobayashi and Ong 2009], the intersection types that describe APTA behaviour over symbol a are required to refine the kinding Σ(a) of the tree constructor a. We extend the approach, taking into account the fact that our system of kinds is more elaborate (we can form products and take linear arrows). This results in a richer set of intersection types.
Definition 19 (Intersection types). Let Q be a finite set of states and Col a finite set of colours. The intersection types σ over Q and Col are defined by the grammar below.
We say that a type is product-free if it is generated by the grammar σ ::= q | A → σ (q ∈ Q). The intersection connective is assumed to be associative, commutative and idempotent. We suppose also that it is stable under reindexing, and we identify intersection types modulo reindexing.
A refinement relation ensures that types formed by intersection share a common structure: Definition 20 (Refinement). The refinement relation between intersection types and kinds is defined by the following rules.
q ∈ Q q :: o P :: ϖ σ :: φ P ⊸ σ :: ϖ ⊸ φ E :: ϖ σ :: φ We may now define the new notion of linear-nonlinear APTA in a way reminiscent of the connection between APTA and intersection types discussed above.
Definition 21 (Linear-nonlinear APTA). A linear-nonlinear APTA (LNAPTA) is a tuple ⟨Σ, Q, δ, q 0 ⟩, where Σ is a tree signature, Q is a finite set of states, q 0 ∈ Q is the inital state, and δ is a map from Σ to sets of intersection types over Q and Col such that σ :: Σ(a) for any a ∈ Σ and σ ∈ δ (a).
The usual notion of APTA (without colouring) can now be recovered as follows.
Suppose there is Ω : Q → Col such that, for all a ∈ Σ, each σ ∈ δ (a) has the shape where c i j = Ω(q i j ) for all 1 ≤ j ≤ n and i j ∈ I j . Then this type-theoretic definition is precisely equivalent to the usual notion of APTA, as defined, for instance, in [Kobayashi and Ong 2009]. In the remainder of the paper, we shall assume that APTA always come with such Ω so that we can write ⟨Σ, Q, δ, q 0 , Ω⟩. Similarly, we shall only consider LNAPTA whose delinearizations into APTA (to be introduced) satisfy this assumption.
It should be noted that, on signatures whose kindings have particular shapes, LNAPTA correspond to various known classes of APTA. It has already been remarked by Melliès [Grellois and Melliès 2015b;Melliès 2014] that APTA restricted according to linearly kinded signatures would correspond to non-deterministic parity tree automata. In the more general framework of LNAPTA, this observation amounts to saying that LNAPTA over signatures with kinds of the shape . Given a LHORS over this signature, suppose we want to check that, on any branch, after a c is encountered, we never encounter b again and we eventually encounter e (call this property P). By the remark above, any LNAPTA over Σ is disjunctive and, hence, cannot express P, which is not a disjunctive property [Kobayashi and Ong 2011]. However, we can express the disjunctive property that some branch satisfies ¬P by the LNAPTA A = ⟨Σ, {q 0 , q 1 }, δ, q 0 ⟩, where: The reader may convince themselves that this LNAPTA expresses the correct property by considering the corresponding disjunctive APTA. Following [Kobayashi and Ong 2011], such a disjunctive APTA expressing ¬P on branches may be obtained systematically by complementing a deterministic parity word automaton for P and reformulating it as a (disjunctive) APTA running on branches. Using our model-checking algorithm to come, we may then check that a LHORS satisfies P by checking that it is rejected by A.
LNAPTA run-tree. A LNAPTA can be seen as an APTA in the traditional sense, but defined in a more structured way and running over trees containing tuples. In fact, we shall define LNAPTA run-trees using the standard notion of run-trees for a traditional APTA. The idea is that a LNAPTA running over the tree a T 1 ⟨T 2 , T 3 ⟩ is constrained with respect to a usual APTA: it can pick a transition nondeterministically but then, while it can duplicate or drop T 1 , it has to run over exactly one copy of either T 2 or T 3 . For instance, the type a : i ∈ {1,2} □ Ω(q i ) q i → ⟨□ Ω(q 3 ) q 3 , ∅⟩ ⊸ q corresponds to a transition whose effect on the production of a run-tree will be: where the automaton duplicates T 1 and explores T 2 exactly once. Consequently, the resulting runtree is a tree in the usual sense: there are no products, which correspond to choices that must be resolved during the execution of a LNAPTA. Observe that the previous transition could have been performed by an APTA in the traditional sense, executed on the tree a T 1 T 2 T 3 . This tree will be called the delinearization of a T 1 ⟨T 2 , T 3 ⟩ over which we shall execute the delinearization of the LNAPTA in question to extract a run-tree.
• The delinearization {|φ| } of a kind is defined as follows.
where n can be 0 and where we used the convention that unary tuples of terms can be written instead of a term to uniformize notation.
We note the following consequences, which are easy to verify. LNAPTA run-trees are now defined following the intuition that LNAPTAs are traditional APTAs obeying additional constraints on duplication and linearity in their executions.
Definition 26. Let A be a LNAPTA and t ∈ KT Σ |_ (o) be a ground term over the same signature Σ. A (accepting) run-tree of the delinearized APTA {|A| } over the delinearized term {|t | } will be called a (accepting) run-tree of A over t.

The Intersection Type System L(A) for Linear-Nonlinear APTA Model-Checking
In this section, we define a generalization of the type system from [Kobayashi and Ong 2009] taking advantage of our finer notion of a kind. The intersection types we consider are the ones of Section 4.1. A nonlinear context Γ (resp. a linear context ∆) is a sequence of bindings Γ = x 1 : A 1 :: κ 1 , . . . , x n : A n :: κ n resp. ∆ = y 1 : P 1 :: κ ′ 1 , . . . , y m : P m :: κ ′ m where A i :: κ i (resp. P j :: κ ′ j ). We write x : □ c σ ∈ Γ when the intersection type for x contains □ c σ . We also rely on two partial operations on contexts. The union ∆ 1 , ∆ 2 of two linear contexts is defined if and only if they have disjoint domains, and contains the variables of ∆ 1 and of ∆ 2 with the unique intersection type and kind they have in ∆ 1 and ∆ 2 . The intersection (or contraction) Γ 1 ∧ Γ 2 of nonlinear contexts contains: • the variables of Γ 1 (resp. Γ 2 ) which are not in Γ 2 (resp. Γ 1 ) with the intersection type and kind they have in Γ 1 (resp. Γ 2 ), σ ∈ δ (a) _ | _ ⊢ A a : σ :: Σ(a) x Σ x : • and the variables x which appear in both Γ 1 and Γ 2 if they have the same kind κ in both; otherwise, the operation is undefined. We exploit stability of intersection types under reindexing to write A i = j ∈J i □ c j σ j for the type of x in Γ i , with J 1 ∩ J 2 = ∅. Then x appears in Γ 1 ∧ Γ 2 as x : j ∈J 1 ⊎J 2 □ c j σ j :: κ (by idempotence some of these types may collapse).
We also define the operation □ c , for c ∈ Col, on types of the shape A, P and E and on contexts as follows: where □ c applied to the empty context is again the empty context and □ c E = E.
Given a LNAPTA A, the intersection type system is defined in Figure 4. Sequents are of the shape Γ | ∆ ⊢ A t : σ :: φ, where we assume Γ and ∆ to have disjoint domains.
As such, the type system is only a way to type the terms R(F ), to which non-terminals of the given recursion scheme rewrite. To account for recursion, Kobayashi and Ong define a parity game that we extend to our setting. Note that, following [Grellois and Melliès 2015b], we introduce a neutral colour ε in the parity game, which is smaller than all others and losing.
Definition 27 (Typing game). Let G be a linear HORS and A be a linear-nonlinear APTA with an associated colouring function Ω. We define the typing game Typ(G, A) as the parity game (V ∀ , V ∃ , (S, q 0 , ε) , E, Ω), where: The edges of the shape (Γ, (F , σ , c)) have colour c and the edges of the shape ((F , σ , c), Γ) have neutral colour ε.
The idea is that two players, Adam (who owns the vertices from V ∀ ) and Eve (who owns those from V ∃ ), build incrementally a typing as follows: • Eve starts from (S, q 0 , ε), and must answer with a context Γ such that Γ | _ ⊢ A R(S) : q 0 :: o. Γ contains typings for the nonterminals introduced when rewriting S to R(S). • If Γ is empty, Eve wins. Otherwise, Adam picks a typed nonterminal F : □ c σ :: N (F ) ∈ Γ and outputs the colour c. • Then Eve provides a context Γ ′ such that Γ ′ | _ ⊢ A R(F ) : σ :: N (F ), and so on.
The interaction stops if Eve can answer with the empty context (she wins), if she cannot answer (she loses) or if the play is infinite (Eve wins iff the parity condition is satisfied). We can use the parity game to obtain a refined version of Kobayashi and Ong's soundness-and-completeness theorem.
Theorem 28 (Soundness and Completeness). Let G be a linear HORS and A be a LNAPTA. Eve has a winning strategy in the typing game Typ(G, A) if and only if there is an accepting run-tree of A over the tree V(G) produced by G.
Proof. For Soundness, suppose that Eve has a winning strategy in Typ(G, A). One can define a series of notions of delinearization and, notably, one for proofs, which allows Eve to translate her moves in Typ(G, A) into moves of Typ({|G| } , {|A| }), opening the same (up to delinearization of types) moves for Adam. It can be shown that Eve obtains a winning strategy in Typ({|G| } , {|A| }) this way. Then we observe that the delinearized typing derivations that Eve uses are precisely typing derivations of the Kobayashi-Ong system, modulo the fact that sequents are written Γ | _ ⊢ A t : σ :: κ instead of Γ ⊢ t : σ :: κ. It follows that the definition of our parity game Typ({|G| } , {|A| }) coincides with their parity game for {|G| } and {|A| } (more precisely, it coincides with its modal rephrasal by Grellois and Melliès given in [Grellois 2016]). As a consequence of the original result of soundness of [Kobayashi and Ong 2009], there is an accepting run-tree of {|A| } over the tree V({|G| }). By definition, there is an accepting run-tree of A over the tree V(G).
For Completeness, one can carefully adapt the argument from [Kobayashi and Ong 2009]. The main changes necessary concern product constructions and the presence of linear contexts. □ Example 29. Consider the LHORS G from Example 14 and the LNAPTA A from Example 23. Despite the linear typing, Typ(G, A) is still too big to be presented fully.
On the left, we display its small fragment, where circled nodes belong to Eve and rectangles to Adam. This diagram follows a strategy for Eve in which she declares a typing that only explores the infinite branch on the right of the infinite tree from Example 14, encountering only occurrences of b; and a counter-strategy for Adam exploring only F . The infinite loop visits colour 1 infinitely often, therefore it is losing for Eve. In fact, Adam has a winning strategy in Typ(G, A): accordingly, G is rejected by A, which corresponds to the fact that it satisfies the original property P considered in Example 23.
The parity game Typ(G, A) is finite; therefore, the LNAPTA model-checking problem for infinite trees generated by LHORS is decidable. Of course, that in itself is not new since a LHORS can be easily translated to a HORS generating the same infinite tree (but with higher order). The value of the development above will appear more clearly in the next section with the complexity analysis.

Complexity Analysis
We have seen that given a LHORS G and a LNAPTA A, the model-checking problem is reduced to the existence of a winning strategy for Eve in the parity game Typ(G, A). Since the parity game is played on typing judgements of our intersection type system, the key element of the complexity analysis will be finding an upper bound on the number of intersection types refining a given kind. As pointed out before, linear kinds will affect the complexity in a relatively small manner.
4.3.1 Bounding the Size of Refinements. First, let us explain briefly why only non-linear arrows are expected to cause an exponential blow-up. Fix a LHORS G and a linear-nonlinear APT A. The source of the tower of exponentials in the complexity of higher-order model-checking is the following refinement rule for non-linear arrows: i ∈I □ c i σ i → σ :: φ → ψ (which combines two refinement rules of Definition 20), where for all i ∈ I , σ i :: φ and σ :: ψ . The intersection types are idempotent, so assuming φ and ψ have only finitely many refinements it follows that the same holds for φ → ψ . Writing ♯κ for the number of distinct intersection type refinements of κ, we get ♯(φ → ψ ) ≤ 2 C ♯φ ♯ψ , where C is the number of colours. It should be clear to the reader how non-linear arrows nested on the left will iterate this exponential, culminating in a tower of height equal to the order of the kind. The impact of the other kind constructors is milder: where Q is the number of states of A. None of these cause directly an exponential blow-up. However, it would be naive to ignore their effect. From our discussions, one might expect that, for purely linear kinds κ, ♯κ will be linear in |κ |. Unfortunately, it is easy to see that this is not the case: the kind o ⊸ . . . ⊸ o ⊸ o has size O(n), but admits O(Q n ) refinements. To circumvent the apparent issue, we introduce the notion of linear depth, capturing the maximal depth of isolated linear chunks of kinds.
In the purely non-linear case [Kobayashi and Ong 2009], the bound also involves the maximal arity of kinds. The presence of linear kinds forces us to switch to a generalized notion of arity.
Definition 30. We define the local generalized arity ga(σ ) for a kind σ by: We say that σ has generalized arity A iff for all subkind ι of σ , we have ga(ι) ≤ A.
Assume from now on that kinds in G have linear depth D, and generalized arity A. For the key lemma below, we assume that the number of colours of A is bounded by Q (from the definition it is bounded by Q + 1 as the intersection type system uses an additional colour ε, but the requirement is easy to ensure with no loss of generality, for instance, by adding a dummy state) ś we find it more convenient to give a bound expressed in Q than in C and Q, which can be proved by induction on κ.
From there, it is relatively easy to derive the following by arithmetic reasoning: Corollary 32. If G has linear order n, linear depth D and generalized arity A, then for all κ in G: The tower is two steps higher than usual if one considers D as a variable. It is easy to come up with a sequence of purely linear kinds showing that the additional double exponential is unavoidable. However, if D is fixed, we get bounds of the form exp n (O(poly(AQS))) for refinements of kinds of linear order n, generalized arity A, size S, with types built from Q states ś as hoped. We will see later that this is not an unreasonable assumption, as our translations yield a small linear depth.
Finally, from the above one can deduce complexity bounds for solving Typ(G, A).
Proposition 33. Given a LHORS G with N non-terminals, kinds of maximal size S, linear depth D and linear order n; and a linear-nonlinear APT A with colours bounded by p and states bounded by Q ≥ p. For n ≥ 1, the time complexity for solving Typ(G, Proof. The following inequalities follow immediately from the definition of Typ(G, A) and Corollary 32 (using also that the generalized arity of a kind is always bounded by its size).
The result follows by applying the algorithm from [Jurdziński 2000]. □ Finally, let us fix some D ≥ 1. A LHORS is D-deep if its linear depth does not exceed D. Our main theorem then follows as a corollary of the above: Theorem 34. Assume n ≥ 1. The time complexity of checking whether a LNAPTA A = ⟨Σ, Q, δ, q 0 ⟩ accepts the value tree of a D-deep LHORS G of linear order n is exp n (O(poly(|Q||G|))). In particular, the problem is n-EXPTIME complete (hardness follows from [Ong 2006]).

IMMEDIATE CONSEQUENCES
Although recent developments in higher-order program verification were prompted by a decidability result for HORS [Ong 2006], subsequent complexity results for richer formalisms did not appeal to the result directly. Instead, their authors were developing dedicated decision procedures.
There are at least two reasons for this. Firstly, HORS represent only the part of the control flow of a program coming from higher-order computation, while programs typically manipulate data, and their behaviour depends on the data. Secondly, programs typically follow a different evaluation strategy, such as call-by-value. Both problems can be dealt with using plain HORS: data types can be represented via their Church encoding, e.g. with B * = o → o → o, while call-by-value programs can be translated to HORS (call-by-name) with CPS. Unfortunately, both translations increase type order and suggest increases in complexity.
In contrast, we are going to show that, thanks to Theorem 34, LHORS (equivalently, the λℓYcalculus) are a suitable target for such translations. First, in this section, we shall derive optimal bounds for MSO model-checking in two extensions of HORS by translation into LHORS. In the next section, we shall follow the same methodology (translation into the λℓY -calculus) to handle accurately a resource verification problem in the call-by-value setting.

Recursion Schemes Over Finite Data Domains
Recursive schemes over finite data domains (RSFD) ] extend standard (nonlinear) HORS with a new ground kind d representing a finite domain whose elements correspond to constants d 1 , · · · , d k of that kind. Terms of RSFDs are those of standard HORS extended with constants d i :: d, case o :: d → o → · · · → o k → o and the reduction rule case o d i u 1 . . . u k ▷ u i . Importantly, RSFD kinding rules force u 1 , . . . , u k to have the ground kind o. Terminals b are kinded as usual by o → · · · → o → o. For RSFDs, we prove: Proposition 35. Given a RSFD G = ⟨Σ, N, R, S⟩, we construct a λℓY -term Σ | _ ⊢ G * :: o as follows. First, we define the translation on kinds and terms.
. . x k In this way, for each θ = N (F ), we obtain Σ, N * | _ ⊢ R(F ) * :: θ * . Next let us take a fixpoint over the product of the non-terminals as in Proposition 16. Then, (−) * sends an RSFD G of order n (note that ord(d) = 0) to a λℓY -term G * of linear order n, of size linear in that of G, and linear depth k; producing the same tree.
This allows us to conclude that: Corollary 36. For a fixed finite domain d, the MSO model-checking problem on infinite trees generated by RSFDs of order n is n-EXPTIME complete.
Proof. Hardness is obvious, since regular HORS are RSFDs. For the upper bounds, by Proposition 35 and Theorem 34, we get that LNAPTA model-checking is in n-EXPTIME. But the expressiveness of LNAPTA depends on non-terminals. Since they are kinded non-linearly, (as we observed in Section 4.1) they concide with regular APTAs in this case. Therefore, they can express arbitrary MSO properties. □ Note for completeness that Kobayashi et al. [2010] prove (n − 1)-EXPTIME completeness for reachability, but do not address general MSO properties. Note also that the n-EXPTIME bounds only hold under the requirement that d is fixed, because the linear depth depends on the size of d ś a constraint that will be lifted in the next subsection with a different translation.

Higher-Order Recursion Schemes with Cases
Higher-order recursion schemes with cases (HORSC) [Neatherway et al. 2012] are similar to RSFD, with a few significant distinctions. Firstly, branching is allowed on d as well as on o, i.e. we have case o as well as case d :: d → d → · · · → d k → d. Furthermore, the elements d i ∈ d are themselves terminal symbols, and can appear in the value tree. Of course, this means that terminal symbols can have kind d as well as o. In general, terminal symbols that are not in d have kinds of the form: a :: β 1 → · · · → β n → o where β i ∈ {o, d}; so in particular they have return kind o.
Translating HORSCs to LHORS/λℓY is slightly more elaborate than for RSFDs, though it remains rather simple. Given a HORSC G = ⟨Σ, N, R, S⟩, we first observe that Σ is many-sorted. In contrast, the translated LHORS will have terminal symbols in Σ * , defined as having the same symbols as Σ but rekinded by replacing every occurrence of d with o. Then, we prove: Proposition 37. Given a HORSC G = ⟨Σ, N, R, S⟩ we construct a λℓY -term Σ | _ ⊢ G * :: o as follows. First, we define the translation on kinds and terms.
Dealing with the recursive definition as before, this yields Σ * | _ ⊢ G * :: o of linear order n, linear depth 2, size linear in that of G; and the same value tree.
Note the usage of product kinds, essential in order to represent the generalized case distinction of HORSC. As for RSFDs, from Proposition 37 and Theorem 34 we obtain: Corollary 38. The MSO model-checking problem on HORSC of order n is n-EXPTIME complete.
Note that, unlike for our translation of RSFDs, the one for HORSC yields λℓY -terms of constant linear depth thanks to the use of products. This eliminates the need for a fixed data domain assumption in the corollary above. A posteriori, of course, the same holds for RSFDs: an RSFD is in particular a HORSC.

Kinding of Terminals
As demonstrated above, Theorem 34 can often be used to obtain better worst-complexity bounds than those implied by the classic result [Ong 2006], provided we can introduce linearity into the underpinning types. This could also be done by typing terminals (i.e. tree nodes) through linear types, such as o ⊸ o ⊸ o and o&o ⊸ o. Every regular HORS can be transformed into an equivalent LHORS (wrt the induced value tree) with terminals rekinded linearly, either multiplicatively (i.e. As we have seen in Section 4.1, the kinding of terminals affects properties expressible with linearnonlinear APTAs. In particular, if we adopt the additive linear kinding for terminals mentioned above, then LNAPTAs correspond to disjunctive APTAs [Kobayashi and Ong 2011], which admit (n − 1)-EXPTIME model-checking on standard HORS of order n. Therefore, it is tempting to conjecture that rekinding the terminals as suggested above always reduces the linear order, saving one exponential. Unfortunately, that is not the case. It turns out that there exist HORS that (even with terminals kinded linearly) do not admit a refined linear kinding reducing the linear order. Thus, the linearity information conveyed by linear kinding in λℓY is too rough to reproduce the argument of [Kobayashi and Ong 2011], which exploits the flexibility of intersection types to reduce the search space. Still, terminals kinded with additive types will play an important role in the next section, where we tackle a less immediate application of our main result to call-by-value programs.

CALL-BY-VALUE PROGRAMS
To avoid the complexity blow-up due to CPS translation, Tsukada and Kobayashi [2014] gave a direct intersection type system to show that the reachability problem for depth-n call-by-value programs is n-EXPTIME-complete. We show that, using Theorem 34, one can recover their result through a linear CPS transformation, and the refined complexity analysis afforded by the Theorem does yield the optimal bound. Moreover, we show that the same complexity bound applies to the more general problem of resource verification [Kobayashi 2009] in the call-by-value setting.

A Call-By-Value Language
We consider a language L, extending the simply-typed call-by-value calculus with primitives for resource generation and access.
Definition 39 (Types). L-types are defined by the grammar where B is the type of booleans, U is the unit type, and R is a type for resources, which could be used to model e.g. file, network or memory accesses. B and U (but not R) will be referred to as base types.
Let us fix a set Act of actions. We write Act ∞ for the set of possibly infinite words on Act, i.e. it contains both finite and infinite words. We fix a deterministic parity automaton A = ⟨Q, Act, δ, q 0 , Σ, F ⟩, which describes the allowed ways to use the resource. Note that this automaton recognizes both finite and infinite words: a finite word w is recognized if the automaton reaches F after reading w, and it recognizes an infinite word according to the parity acceptance condition. We write L q (A) for the set of words (both finite and infinite) accepted by A from state q.
Definition 40 (Terms). L-terms are defined by the grammar t, u, v : where a ∈ Act, q ∈ Q and all the tuplings are non-empty.
L-terms will be typed using typing judgements of the form E; Γ ⊢ L t : A, where E is the environment comprising typed function names, which are to be defined later in the whole program, and Γ is a standard typing context. The typing rules appear in Figure 5.
Definition 42 (Programs). A L-program is a pair (P, D), where D is a function definition and P is a term satisfying E; _ ⊢ L P : B, where B is a base type.

39:22
Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski  Our operational semantics will track, throughout execution, access to resources. It is defined via two sets of rules: standard (small-step) call-by-value reduction rules and a collection of rules for tracking resource usage. First we present the rules for plain call-by-value computation. For the rest of this section, we fix a function definition D, as it is not affected by reduction.
6.1.1 Call-By-Value Reduction. Values are terms of one of the forms: t t, ff, skip, λ⟨x 1 , . . . , x n ⟩. t; or resources, represented by natural numbers. We use v, w, . . . to range over values, or r in case the value is a resource. The call-by-value evaluation contexts are generated as described below.
Recursively defined variables f i are treated as values ś by definition of our programs, we know that they are always bound to non-empty abstractions, i.e. values. Treating them as values forces the evaluation of arguments before substitution of D(f i ) for f i . This will later allow for a closer match with the CPS translation.
In Figure 6 we present the rules for pure call-by-value reduction, not taking into account resource usage and non-deterministic choice. Keep in mind that these rules operate on programs, i.e. terms E; _ ⊢ P : B with B a base type. We write D v for the union of v and D . 6.1.2 Resource Usage. Now, we enrich our operational semantics to track resource usage. As in [Tsukada and Kobayashi 2014], resources can be dynamically created and the properties we aim to verify are resource-conscious: each resource, taken separately, must be accessed according to A. To track usage of the r th initialized resource we build a labelled transition system L(r ).
Definition 43. Fix D and r ∈ N. The configurations of L(r ) are pairs (P, n), where n ∈ N is the index of the next resource to be created and (P, D) is a program. Transitions are given in Figure 7.
The operational semantics is well-behaved, as can be proved by an induction on P: Lemma 44. For each (P, n), either P is a value; or exactly one of the rules of Figures 6 and 7 applies.
The labels of L(r ) are taken from L = Act ⊎ Q ⊎ {τ }. For w ∈ L ∞ (possibly an infinite word on alphabet L), we write tr(w) for w with occurrences of τ removed. We can finally formulate: Definition 45 (Correct program). Let (P, D) be an L-program and r ∈ N be a tracked resource. A maximal (possibly infinite) reduction sequence ρ in L(r ) is correct either if tr(ρ) = tr(v 1 v 2 . . . v i . . . ) = ε (the resource tracked is never initialized), or tr(ρ) = qa 1 a 2 . . . a j . . . , where a 1 a 2 . . . a j · · · ∈ L q (A). The program (P, D) is called correct if, for all r ∈ N, any reduction sequence in L(r ) starting from (P, 0) is correct.
Definition 46 (Resource correctness problem). The resource correctness problem asks whether a given L-program is correct.
Next we state the main result of this section, about the complexity of the resource correctness problem in our setting. The next subsection will be devoted to its proof, by a linear CPS translation into the λℓY -calculus.
The depth of a program (P, D) is the maximal depth of the type of a subterm of P or of a term occurring in D. In the remainder of the section, we will prove: Theorem 47. The resource correctness problem is n-EXPTIME-complete for programs of depth n.

Linear CPS Translation
We now detail the CPS translation from L to the λℓY -calculus, which accommodates the translation better than LHORS. Thanks to the translations between LHORS and λℓY , we will be able to take advantage of Theorem 34, though.
Our translation exploits the observation that in the CPS of call-by-value into call-by-name, the continuations carried around are actually linearly used, in the sense of [Berdine et al. 2002]. Hence we can exploit the linearity offered by our target language, and give the terms obtained by translation a more precise kinding. Technically, our translation is a variant of the linear CPS (e.g. [Laird 2005]) extended with products and recursive definitions.
6.2.1 Translation of Terms. The types of L are translated to types of the λℓY -calculus as follows.
⊸ o To all terms E; Γ ⊢ L t : A, the translation will associate a Y -free term of the λℓY -calculus Note that the translation of a term will not have any free linear variables, though it does have some linear kinding. In Figure 8, we give the translation for the basic λ-calculus primitives. For the resource primitives, we fix the tree signature to be Σ, defined as: To any program (P, D) we will associate a λℓY -term of ground type in context Σ, whose Böhm tree is a representation of the tree of all executions of P. The binary constructor ⊕ will track nondeterministic choice and each action a ∈ Act will be recorded via a unary constructor a :: o ⊸ o.
The terminal e will be used to terminate branches, corresponding to completed computations. Finally, the remaining primitives ν q , t, nt are used to handle dynamic creation of resources, following a trick from [Kobayashi 2009]. Each creation of a resource will be recorded as an occurrence of ν q in the tree. The constructor ν q is binary. In a tree generated by (the CPS translation of) a program, both sub-trees of ν q will be almost identical. Their only difference will be that in the left branch, the accesses to the generated resource will be tracked (all accesses to that resource will be prefixed with t), whereas in the right branch, the accesses to the generated resource will be non-tracked (all accesses to that resource will be prefixed with nt). Later, when verifying properties of this tree, we will make sure to explore branches visiting the left sub-tree of a ν q at most once, ensuring that at most one resource is tracked. We can finally complete the CPS-translation. In Figure 9, we give the translation for all the primitives pertaining to resource access. This wraps up the definition of the translation of terms of our language: for each E; Γ ⊢ L t : A, we obtain Σ, E * , Γ * | _ ⊢ t * :: (A * → o) ⊸ o.

Translation of Definitions and Programs. Assume we have a definition
with types as indicated before. Note that we insisted (as in [Tsukada and Kobayashi 2014]) that in such definitions, each abstraction be non-empty, i.e. for all 1 ≤ i ≤ n, p i ≥ 1. This means, in particular, that each term in the definition is a value. As is usual with CPS translations, translations of values have a particular shape, which can be confirmed directly from the definitions: Lemma 48. Let E; Γ ⊢ L v : A be a value. Then, v * has the shape: for some E * , Γ * | _ ⊢ v • :: A * . Lemma 51. Let E; Γ, x : A ⊢ L t : B be any term of L, and E; Γ ⊢ L v : A be a value of type A. Then, (t[v/x]) * = t * [v • /x], where v * = ℓk A * →o . k v • as given by Lemma 48.
From that, we can easily deduce that the translation is a simulation with respect to β-reduction. Now that we have established our simulation result without recursion, we add recursion to the mix. It will be useful to note that the redexes that come from the translation of CBV redexes always appear in head position: we define the head contexts in the λℓY -calculus, as follows: . Consider a program (P, D), interpreted as in Section 6.2.2. We observe that the use of recursive calls in P matches fixpoint unfoldings in the translated term. Leveraging Lemma 53, we have: Lemma 54. Fix a definition D. Then, if P 1 D P 2 , we have (P 1 , D) * βη ▷ δ βη (P 2 , D) * , where βη is βη-equivalence. From there, we can finally prove the adequacy of the translation.
Proposition 55 (Adeqacy). For (P, D) a program, D v terminates on P iff (P, D) * is solvable. Proof. The translation is designed so that recursion matches on both sides of the translations: precisely, the translation induces a bisimulation between the relation * v D on programs-indefinition, and relation ▷ δ on βη-equivalence classes of λℓY -terms.
That it is a simulation is Lemma 54. Assume (P, D) * βη ▷ δ , thus the βη-normal form of (P, D) * has a Y x . t subterm in head position. Reduce P via * v as much a possible ś this terminates. If it terminates on anything else than a D -redex, then the βη-normal form of the translation has a variable in head position, contradicting that it is a ▷ δ -redex. So it is indeed a D -redex, and necessarily firing it translates to firing the unique ▷ δ -redex of (the normal form of) (P, D) * .
The proposition follows easily from this bisimulation. □ 6.2.5 Resource Verification as λℓY Model-Checking. Finally, using the adequacy of the translation, we study its action on the resource usage primitives. For that, we construct a second LTS, this time from λℓY -terms Σ | _ ⊢ t :: o, matching L(r ) from Definition 43. Its configurations are pairs (t, n) where t is a βηδ -equivalence class of λℓY -terms (we will often write such equivalence classes as {t }, for t a representative), and where as before, n ∈ N represents the next resource index to be initialized. The transitions, labeled again by L, are given in Figure 10. We write L ′ (r ) for this LTS.
Paths in this LTS starting from ({t }, 0) perform an exploration of BT(t) (with the proviso that BT(t) is such that each occurrence of a is preceeded by t or nt, which will be true in the translation), branching non-deterministically at occurrences of ⊕, and turning left exactly once at occurrences of ν q : when the required index has been reached. L ′ (r ) satisfies the following key property.
Proof. From the definition of translation and using Lemma 53, it is a simulation. The other direction follows by Proposition 55: if (P, n) B ({t }, n) and {t } makes one of the transitions of Figure 10, then t is solvable. Hence, D v terminates on P; eventually reducing to Q. But from Lemma 44, either Q is a value (absurd or that would contradict that {t } makes a transition), or a rule from Figure 7 applies ś but only the rule matching the transition of {t } is possible. □ For every closed E; _ ⊢ L P : B with B base type, we have (P, 0) B ((P, D) * , 0), so the trees of L(r ) and L ′ (r ) respectively reachable from those are weakly bisimilar: their maximal branches have the same traces. By definition of L(r ), P is correct if for all r ∈ N, the maximal branches of L(r ) have correct trace. Likewise, by definition of L ′ (r ), its maximal branches correspond to the maximal branches of BT((P, D) * ) taking the left sub-tree of a ν q exactly once, when encountering a ν q for the r -th time. Hence, P is correct iff all the branches of BT((P, D) * ) visiting the left subtree of a ν q exactly once are correct. As this property is MSO definable, it follows that: Corollary 57. For any program (P, D) and deterministic parity automaton A there exist • a λℓY -term Σ | _ ⊢ (P, D) • :: o of linear order equal to the depth of (P, D), of size linear in that of (P, D), and linear depth 2, • a linear-non-linear APTA A ′ of size linear in that of A such that P is correct iff A ′ rejects BT((P, D) • ).
The construction of A ′ from A proceeds as in [Kobayashi and Ong 2011]. Theorem 47 now follows.

FURTHER DIRECTIONS
Our results demonstrate the potential of λℓY and LHORS to serve a unifying framework for studies into higher-order verification. The significant body of literature on connections between linear logic and programming languages opens up many avenues for future work. Verification algorithms for LHORS have, by design, quite a wide application range, and the translations we considered exploit linearity to a small extent only.
Some obvious and short-term directions beyond model-checking include global model-checking [Broadbent et al. 2010] and selection [Carayol and Serre 2012], which we expect (as in the standard case) to enjoy the same complexity, with respect to the same measures.
Amongst other more open-ended questions, we would like to understand better the additional expressiveness contributed by the addition of linear kinds. What new infinite trees can we get, while retaining efficient verification algorithms? What is the trade-off between the complexity boost coming from linear typing and properties expressible by LNAPTAs?
Finally, it would be interesting to explore the practical impact of our work, for instance, by using type inference to obtain more refined linear-non-linear typings for functional programs, so as to improve the complexity of verification.