S Salvati

I Walukiewicz

Evaluation is MSOL compatible

We consider simply-typed lambda calculus with fixpoint operators. Evaluation of a term gives as a result the Böhm tree of the term. We show that evaluation is compatible with monadic second-order logic (MSOL). This means that for a fixed finite vocabulary of terms, the MSOL properties of Böhm trees of terms are effectively MSOL properties of terms themselves. Theorems of this kind have been known for some graph operations: unfolding, and Muchnik iteration. Similarly to those results, our main theorem has diverse applications. It can be used to show decidability results, to construct classes of graphs with decidable MSOL theory, or to obtain MSOL formulas expressing behavioral properties of terms. Another application is decidability of a control-flow synthesis problem.

Introduction

Rice theorem tells us that no non-trivial property of the behaviour of a Turing machine can be decided by looking at the machine itself. In this paper we consider a much simpler abstract computing system: simply-typed lambda-calculus with fixpoint operators. We denote it λY . A behaviour of a λY -term is its Böhm tree. Since not all λY -terms have normal forms, Böhm tree is a standard choice for the result of a computation of a term. To express properties of results we use monadic second-order logic (MSOL) because it is a fundamental logic over trees. The transfer theorem we prove says that every MSOL property of Böhm trees is effectively an MSOL property of terms. In other words, we show that MSOL is compatible with evaluation.

The λY -calculus is a standard formalism in the lambda-calculus community. It can be seen as a simplification of the programming language PCF introduced by Plotkin [START_REF] Plotkin | LCF considered as a programming language[END_REF]. It is much simpler than the full, untyped, lambda-calculus. For example, it is decidable if a λY -term has a normal form, while the same question for untyped lambda-calculus is undecidable. Still, λY -calculus has some nontrivial computational power. For example, the problem of deciding if two λY -terms are equivalent is undecidable [START_REF] Statman | On the λy calculus[END_REF]. By now, it is usual [START_REF] Barendregt | The Lambda Calculus[END_REF] to approach the semantics of the lambda-calculus through infinite Böhm trees. Such a tree is just a normal form of the term, if the term has one. Otherwise it is a potentially infinite tree representing the visible part of the infinite computation of the term. In this paper we consider also infinite λY -terms. This is less standard but introduces relatively few complications while bringing real strengthening of the main theorem.

Under a different syntax λY -calculus has also been intensively studied by language theoretic community. One can cite the PhD thesis of Fisher [START_REF] Fischer | Grammars with macro-like productions[END_REF] on macro languages, the work of Engelfriet and Schmidt on IO and OI [START_REF] Engelfriet | IO and OI[END_REF][START_REF] Engelfriet | IO and OI[END_REF], or the work of Damm on (safe) recursive schemes [START_REF] Damm | The IO-and OI-hierarchies[END_REF]. More recently Knapik, Niwinski and Urzyczyn [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] considered recursive schemes as generators of infinite trees, and studied the model-checking problem for such trees. After a series of intermediate results [AdMO05, [START_REF] Knapik | Unsafe grammars and pannic automata[END_REF][START_REF] Aehlig | A finite semantics of simply-typed lambda terms for infinite runs of automata[END_REF]; Ong [START_REF] Ong | On model-checking trees generated by higherorder recursion schemes[END_REF] has shown that the modelchecking problem of MSOL properties for such trees is decidable. It has been already clear to Engelfriet and Schmidt as well as to Damm that the grammars, or recursive schemes they study are a different representation of λY -terms (and their subclasses). Indeed, trees generated by recursive schemes are just Böhm trees of the corresponding terms of λY -calculus. So, for example, the theorem of Ong can be rephrased as saying that Böhm trees of finite λY -terms have a decidable MSOL theory. The transfer theorem presented in this paper implies this decidability result.

Our transfer theorem says that for a fixed finite vocabulary of terms, an MSOL formula ϕ can be effectively transformed into an MSOL formula ϕ such that for every term M over the fixed vocabulary: M satisfies ϕ iff the Böhm tree of M satisfies ϕ. The result is stronger than Ong's theorem in at least two aspects. First, it holds also for infinite λY -terms. Second, and more importantly, the theorem gives an effective reduction of one theory to another. For example, since finiteness of a tree is definable in MSOL, we immediately obtain that if we restrict to λY -terms over a fixed finite vocabulary then the set of terms having a (finite) normal form is MSOL definable. In the last section of the paper we give several other applications of additional power provided by the transfer theorem.

In terminology of Courcelle [START_REF] Courcelle | Monadic second-order graph transductions: A survey[END_REF], our result says that evaluation of λY -terms is MSOL-compatible. A flagship example of a result of this kind is MSOL-compatibility of the unfolding operation [START_REF] Courcelle | Monadic second-order logic, graphs and unfoldings of transition systems[END_REF]. A finite automaton, i.e. a graph, can be unfolded into a tree of all its possible executions: this tree can be seen as the evaluation of the automaton. The MSOLcompatibility of the unfolding means that the MSOL theory of this tree can be effectively reduced to MSOL theory of the automaton itself. The more powerful Muchnik iteration [START_REF] Semenov | Decidability of monadic theories[END_REF][START_REF] Walukiewicz | Monadic second-order logic on tree-like structures[END_REF] allows to get a similar result for pushdown automata and higher-order pushdown automata. This way we obtain the pushdown hierarchy of trees with a decidable MSOL theory. Here we consider λY -terms instead of automata as a computational model, and show the analogous result for evaluation instead of unfolding or Muchnik iteration. The operation of evaluation cannot be directly compared to the other two since it works on different objects (trees with back edges instead of graphs). Yet in a well-known context where these operations can be compared, the evaluation operation is strictly stronger. Indeed, every tree in the pushdown hierarchy [START_REF] Caucal | On infinite terms having a decidable monadic theory[END_REF] is a Böhm tree of some term, but not vice versa [START_REF] Parys | On the significance of the collapse operation[END_REF].

Related work: This work can be seen as generalization of Ong's theorem, in the same way as compatibility of MSOL with unfolding is a generalization of Rabin's theorem. Moreover the unfolding theorem is in some sense also a special cases of our main theorem. Knapik and Courcelle [START_REF] Courcelle | The evaluation of firstorder substitution is monadic second-order compatible[END_REF] have used the unfolding theorem to prove a special case of our theorem for infinite terms of order 1. The proof presented here is based on our proof of Ong's theorem using Krivine machines [START_REF] Salvati | Krivine machines and higherorder schemes[END_REF].

MSOL properties of higher-order systems are an active area of research. After the seminal paper of Knapik, Niwinski and Urzyczn [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF]; Caucal has introduced the pushdown hierarchy [START_REF] Caucal | On infinite terms having a decidable monadic theory[END_REF] that since has been an object of intensive study from logical point of view [START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF]. It has been shown that many interesting properties of higher-order programs can be analyzed with recursive schemes and automata [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF][START_REF] Kobayashi | Higher-order program verification and languagebased security[END_REF][START_REF] Kobayashi | Types and recursion schemes for higher-order program verification[END_REF][START_REF] Kobayashi | Complexity of model checking recursion schemes for fragments of the modal mucalculus[END_REF][START_REF] Ong | Verifying higherorder functional programs with pattern-matching algebraic data types[END_REF]. The decidability result of Ong has been revisited in a number of ways [HMOS08, [START_REF] Kobayashi | A type system equivalent to modal mu-calculus model checking of recursion schemes[END_REF][START_REF] Salvati | Krivine machines and higherorder schemes[END_REF][START_REF] Christopher | A saturation method for collapsible pushdown systems[END_REF].

The study of MSO-compatible operations has a long history. Following a result of Feferman and Vaught for products [START_REF] Feferman | The first order properties of products of algebraic systems[END_REF], Shelah has introduced and extensively used MSO-compatibility of sums [START_REF] Shelah | The monadic second order theory of order[END_REF]. Later Stupp proposed an iteration operator, and showed that it is MSO-compatible [START_REF] Stupp | The lattice-model is recursive in the original model[END_REF]. Rabin's theorem [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] on decidability of MSOL on infinite binary trees is an immediate corollary of this result. Much later Muchnik has proposed a strengthening of Stupp's iteration, and sketched the proof of MSOLcompatibility of this operation [START_REF] Semenov | Decidability of monadic theories[END_REF]. Courcelle and Walukiewicz have shown MSOL-compatibility of the unfolding operation [START_REF] Courcelle | Monadic second-order logic, graphs and unfoldings of transition systems[END_REF] not using Muchnik iteration. Later Walukiewicz has given a detailed proof of MSOLcompatibility of Muchnik iteration [START_REF] Walukiewicz | Monadic second-order logic on tree-like structures[END_REF]. This result has then been extended and adapted to other logics [BK05, [START_REF] Kuske | Monadic chain logic over iterations and applications to pushdown systems[END_REF][START_REF] Kuske | Compatibility of Shelah and Stupp's and Muchnik's iteration with fragments of monadic second order logic[END_REF]. For a survey of compatible operations and their applications we refer the reader to [START_REF] Blumensath | Logical theories and compatible operations[END_REF] Plan of the paper: In the next section we introduce infinitary λYcalculus: a simply typed λ-calculus of infinite terms with fixpoint operators. Extensions of untyped lambda-calculus to infinite terms are rather delicate [START_REF] Kennaway | Term Rewriting Systems[END_REF]. Here we have made some design choices that together with the use of typing allow to retain the fundamental properties in a relatively straightforward way. We prove that Böhm trees are still the canonical values for infinite λY -terms. We also adapt Krivine machine to compute Böhm trees of infinite terms. More precisely, the machine computes Lévy-Longo trees of terms, but for terms we are interested in the two notions coincide.

Finally, we introduce the notion of canonical form of a term.

Section 3 presents the main theorem. For this it describes how terms are represented as logical structures so that we can talk about their MSOL properties. Our representation requires that we have a fixed finite set of λ-variables. At the same time we do not need to restrict the number of Y -variables. We show that the theorem is not likely to hold if the number of λ-variables in not fixed. The overview of the proof of the theorem is given in the following section.

Section 5 gives three applications of transfer theorem. We explain how to obtain formulas expressing computational properties of terms. We show decidability of higher-order matching for terms over a fixed vocabulary [START_REF] Schmidt-Schauß | Decidability of arity-bounded higherorder matching[END_REF]. We present a synthesis result that allows to construct λY -programs from λY -modules.

In the conclusion section we give more relations between the transfer theorem and other results in the literature.

The extended version of the paper [START_REF] Salvati | Evaluation is MSOL compatible[END_REF] presents all the proofs as well as some more comments and discussions.

Infinitary λY -calculus

In this paper, we work with infinitary simply typed λY -calculus with fixpoints. We refer to it as infinitary λY -calculus, sometimes omitting the adjective "infinitary". In rare cases when we want terms to be finite, we say it explicitly. This section introduces infinitary simply typed λY -calculus as a rather straightforward generalization of finitary λY -calculus. We start with the notion of infinitary terms together with the operational semantics of the infinitary λY -calculus. We adopt a slightly modified syntax where Y is used as a variable binder rather than as a combinator. This allows us to distinguish between the variables that may be bound by Y from those that may be bound by λ. Such a distinction is of a little importance for the calculus itself, but it will allow us to get a more general theorem later when we will put restrictions on the number of variables. Next, we define the notion of Böhm trees. As it can be expected, Böhm trees are actual normal forms of infinitary terms, and every infinitary term has a normal form. Afterwards, we introduce a particular class of terms, that will be useful in the proof of the main theorem: terms in canonical form. Finally, we introduce a slight extension of the Krivine machine that is able to compute the normal forms of infinitary λY -terms, thus giving an actual computational content to infinitary λY -terms. The notion of Krivine machine we use is tailor-made so as to work on terms in canonical form.

Syntax and operational semantics

The set of types is constructed from a unique basic type 0 using a binary operation →. Thus 0 is a type and if α, β are types, so is (α → β). As usual, so as to use less parentheses, we consider that → associates to the right. For example, 0 → 0 → 0 stands for (0 → (0 → 0)). We will write 0 i → 0 as short notation for 0 → 0 → • • • → 0 → 0, where there are i + 1 occurrences of 0. The order of a type is defined by: order (0) = 1, and order (α → β) = max(1 + order (α), order (β)).

A signature, denoted Σ, is a set of typed constants, that is symbols with associated types. Of special interest to us will be tree signatures where all constants other than the special constant Ω have order at most 2. Observe that types of order 2 have the form 0 i → 0 for some i. For simplicity of notation we will always assume that i = 2, but of course our results do not depend on this convention. The terms will be built over two disjoint countable sets of typed variables: λ-variables and Y -variables. We shall write x α for a λ-variable of type α, and x α for a Y -variable of type α. In this paper, we work with potentially infinite λY -terms. We assume that for every type α we have a constant Ω α to denote the undefined term of type α. We will also have typed application symbols @ α , and typed binders Y α as well as λ α→β . For all types α we define simultaneously the sets of infinite terms of type α as trees satisfying the following conditions.

• A node labelled by Ω α , x α , x α , or c α is a term of type α.

• A tree with the root labelled @ β having as the left subtree a term of type α → β and as a right subtree a term of type α, is a term of type β.

• A tree with the root labelled λ α→β x α with the unique immediate subtree being a term of type β, is a term of type α → β.

• A tree with a root labelled Y α x α with the unique immediate subtree being a term of type α, is a term of type α.

Some examples of infinitary λY -terms, as well as trees that are not terms, are presented in Figure 2.1.

Notice that all variables and constructors carry type labeling that makes typing of a term unique. We shall often omit those labels when they are unnecessary for the understanding or when they can be inferred from the context. We will also use standard conventions and write (M N ) for M @ N , and N 0 N 1 . . . N p for (. . . (N 0 N 1 ) . . . N p ).

We assume the usual notions of free and bound variables. Moreover, in general, we work up to the renaming of bound variables, that is up to α-conversion of terms. On infinitary terms, this convention is not really innocent since a term may contain infinitely many free variables. Nevertheless, a careful use of de Bruijn indices is, as in the finite case, a way to represent equivalence classes of terms modulo α-conversion. However, in the sequel, we are going to work sometimes on particular representatives of αequivalence classes assuming certain properties on the naming of variables such as the Barendregt convention on Y -variables (every Y -binders binds a distinct Y -variable), and the use of finitely many λ-variables. To make things clear, when working up to α-conversion, we will speak about terms, and when working on particular instances of α-equivalence classes, we will speak about concrete terms.

This definition of infinitary terms comes with two main differences with respect to the usual one given for the untyped infinitary calculus. First, the typing discipline rules out terms with infinite sequences of λ-abstractions (cf. Figure 2.1). The second difference is that we use the Y combinator as a binder and we distinguish between Y -variables and λ-variables. Notice that the definition of infinitary terms allows infinite sequences of Y -abstractions (cf. Figure 2.1).

The reason why we need to distinguish between λ-variables and Yvariables is that the main theorem we prove is about terms which use finitely many λ-variables but possibly infinitely many Y -variables. As a small remark, if the main theorem did not need to make this assumption, we could simply get rid of Y -binders. Indeed the term Y x.N has the same Böhm tree (see section 2.2) as the term rec(λx.N [x/x]) where rec = λf.f (f (f (f . . . ))). This shows that λ-abstraction, or parameter instantiation, is more powerful than recursive definition in the context of the infinitary λ-calculus.

Terms Y x. Y x. Y x. @ @ x x Y x. λz. @ @ z x Non-term λx. λx. λx.

Figure 1: Examples of infinitary terms and non-terms

The notion of capture-avoiding substitution can be easily extended to infinitary λ-calculus. Given two terms M and N we shall write M [x := N ] (resp. M [x := N ]) for the result of the capture-avoiding substitution of N for the free occurrences of x (resp. x) in M . It is important to notice that x or x may have infinitely many free occurrences in M , and that computing the result of M [x := N ] or of M [x := N ] may require an infinite amount of work. This is why, following a suggestion made in Terese [], we will use the Krivine machine later on so as to compute substitutions explicitly and to avoid the infinite overhead of computation that each substitution may require if it were to be completely performed.

We may now define β-contraction on infinitary terms as the straightforward extension of β-contraction on finite terms. Concerning δ-contraction, we need to adapt its definition to our slightly modified syntax. The relation of δ-contraction → δ is the smallest relation that is compatible with the syntax of infinitary λY -calculus and so that Y x.M δ-contracts to M [x := Y x.M ]. We let βδ-contraction, → βδ to be the union of the relations → β and → δ . Of course, the subject reduction property for simple types transfers from finite terms to infinite ones so that the reduction preserves typing. As we are interested in infinitary terms as computational devices, we need to choose what we consider to be a value or the output of the computation performed by those terms. We thus introduce the notion of weak head normal form and of weak head reduction.

Definition 1 An infinitary term M is in weak head normal form, if it is of the form λx α .N for some term N , or if it is of the form hN 1 . . . N n , with h being either a variable or a constant different from Ω.

When M is an infinitary term of the form (λx. P )P 1 . . . P n or of the form (Y x. P )P 1 . . . P n , then M has a head-redex. Reducing M to P [x := P 1 ]P 2 . . . P n or to P [x := Y x.P ]P 1 . . . P n , respectively, is called head-contracting M . We write M → h N when M head-contracts to N ; we write M → * h N for head-reduction in some finite number of head-contraction steps.

The reason why, we wish to use weak-head normal forms for values instead of the usual notion of head-normal form is that we are going to use the Krivine machine to compute values. Krivine machine computes weak-head normal forms of terms and not head-normal forms.

Böhm trees

Now that we have settled a reduction strategy together with a notion of value, we may define a notion of normal form for infinitary terms, namely Böhm trees. We also show that in a strong sense Böhm trees are actual normal forms of infinitary terms. There is no particular difficulty to define the notions of this subsection for all infinite λY -terms. Yet, since we consider infinitary λY -terms as generators of infinite trees, we are really interested only in closed terms of type 0. We choose to present the definitions only for such terms. In order to further simplify the notation we will from the start consider only terms over a tree signature, and assume that all the constants are binary.

Definition 2 (Böhm trees) Given a closed term M of type 0 over tree signature, we define its Böhm tree, BT (M ), as follows:

1. if M → * h bN 1 N 2 where b is a constant different from Ω, then BT (M ) is a tree with root labelled b and with BT (N 1 ) and BT (N 2 ) as its subtrees.

otherwise BT

(M ) = Ω α .
Observe that in our case Böhm trees are just labelled infinite binary trees. In a sense that can be made precise, Böhm trees are normal forms of terms. As such they are terms too, but due to their special shape we do not need to use application nodes to represent them. In Figure 2 we present a Böhm tree and its representation as a term.

The reader may be surprised that we talk about Böhm trees while in general Krivine machines compute Lévy-Longo trees. It turns out that the two notions coincide when working with tree signatures and terms of type 0. This is why we have preferred to use the better known notion. Even though we have defined Böhm trees (or Lévy-Longo trees) using a particular reduction strategy, they really are the unique normal forms of infinitary terms modulo βδ-reductions of arbitrary ordinal length provided we add the reduction rule that allows to reduce terms without weak head normal form to Ω. We are using the end of this section to establish this fact.

The results we are about to show are known in the literature on untyped infinitary λ-calculus (see Kennaway et al. [KKSdV97] and Terese [START_REF] Kennaway | Term Rewriting Systems[END_REF]). We here adapt those results to the simply typed λY -calculus and we present them in way that suits better our needs. Notice that, even though we have defined Böhm trees only for closed terms of atomic types built on a tree signature, all the results we mention here hold without those restrictions.

As we are working with infinite terms, computing their possible normal forms may require an infinite number of βδ-contraction steps. For example the term that is defined as the solution of the equation u = (λz 0 .az 0 )u that can be depicted as: @ (λz o .az o ) @ (λz o .az o ) @ (λz o .az o ) requires to reduce ω redices so a to obtain the term that is the solution of the equation v = av: @ a @ a @ a If we were to reduce the term (λx 0 .bx 0 )u we may first reduce u in ω steps to v and we would obtain a term (λx 0 .bx 0 )v that can be reduced to bv with one more step. With this example we have constructed a reduction of length ω + 1. It thus appears natural to define reductions of arbitrary ordinal length. The natural way of defining such sequences of reductions is to define them as continuous functions from ordinals to λ-terms. This is one of the reason why we need the constants Ω α as part of our language for defining infinitary terms. The constants Ω α stands for the undefined term of type α and allows us to define a natural partial order on infinitary terms. This is the least order that is compatible with the syntax and so that for every term M in Λ α,∞ (Ω), Ω α M . Notice that, whenever M N , M and N need to be terms that have the same types.

Definition 3 Given a relation R on λ-terms and an ordinal γ, a γ, Rreduction sequence of type α is a function ϕ that maps ordinals δ ≤ γ to infinitary terms of Λ α,∞ (Ω) so that:

1. if δ < γ, we have ϕ(δ) R ϕ(δ + 1),
2. if δ ≤ γ is a limit ordinal, then for every term M ϕ(δ) there is an ordinal θ < δ so that M ϕ(θ).

When R =→ βδ , and there is a α, → βδ -sequence ϕ such that ϕ(0

) = M and ϕ(α) = N we write that M α -→ ∞ N , or we write M -→ ∞ N when there is α such that M α -→ ∞ N .
The notion of reduction sequences we use is called weakly convergent in the literature.

It is already known that in the untyped case infinitary β-reduction is not Church-Rosser. Typing does not fix this problem and it is easy to adapt the examples of the untyped case to the typed case. Indeed, if we take the terms I = λx 0 .x 0 , M = λx 0 .I(f 0→0 x 0 ) and J = λx 0 .f 0→0 x 0 , then the term (Y f 0→0 .M )x 0 we can be reduced in the following ways:

(Y f 0→0 .M )x 0 -→ ∞ λx 0 .I(Y f 0→0 .M x 0 ) -→ ∞ (λx 0 .I((λx 0 .I(Y f 0→0 .M x 0 ))x 0 ))x 0 -→ ∞ I(I(Y f 0→0 .M x 0 ) -→ ∞ I ω
where I ω is the term satisfying the syntactic identity II ω = I ω and I ω can be depicted by: @ I @ I @

I

The term (Y f 0→0 .M )x 0 can also be reduced as follows:

(Y f 0→0 .M )x 0 -→ ∞ (λx o .(Y f 0→0 .J)x 0 )x 0 -→ ∞ (λx 0 .(Y J)x 0 )x 0 ω -→ ∞ u
where u is the infinite term verifying the syntactic identity u = (λx 0 .u)x 0 and that is depicted by: @ λx 0 . @ λx 0 .

x 0

x 0

Since, for any redex that is contracted in I ω the result of the contraction is I ω again and similarly u can only be reduced to u, it is obvious that there is no term P so that I ω -→ ∞ P and u -→ ∞ P . Nevertheless we do not assume that those terms are meaningful values, we rather assume that meaningful values are terms in weak-head normal forms. With this notion of value we may enrich the our operational semantics with a reduction to Ω for terms that do not yield a value.

Definition 4 We introduce the relation → Ω , the Ω-contraction, so that, given a term M of Λ α,∞ (Ω 0 ), if there is no term N in weak-head normal from so that M -→ ∞ N , then M → Ω Ω α . We let → βδΩ be the union of → βδ and → Ω .

When there is a α, → βδΩ -sequence ϕ such that ϕ(0) = M and ϕ(α

) = N we write that M α -→ Ω,∞ N , or we write M -→ Ω,∞ N when there is α such that M α -→ Ω,∞ N .
The operational semantics -→ Ω,∞ on infinitary terms has nice properties, and in particular it has the Church-Rosser property (it is a consequence of Terese [] Theorem 12.9.6 p.699).

Theorem 5 If M -→ Ω,∞ N 1 and M -→ Ω,∞ N 2 , then, there is P so that N 1 -→ Ω,∞ P and N 2 -→ Ω,∞ P .
This confluence property is partially grounding the fact that Böhm trees of terms are their normal forms in proving that every term has a unique normal form. It remains to see that these unique normal forms are the Böhm trees. The main problem is that there is a gap between the relation → Ω which may reduce a term M to Ω only when there is no infinitary reduction that turns M into a weak-head normal form while the Böhm tree of a term M is Ω when there is no finite head-reduction that turns M into a weak-head normal form. This is precisely this gap that Lemma 6 is filling. We now give its proof.

Lemma 6 Given M in Λ α,∞ (Ω), if there a term N in weak-head normal form so that M -→ ∞ N , then there is k < ω and P in weak-head normal form so that M k -→ h,∞ P .

Proof

Let γ be an ordinal so that M γ -→ ∞ N and let ϕ be the γ, → βδ -reduction sequence reducing M to N . In case γ < ω, it is easy to see that there is a finite term M M which can be put in finitely many steps of headcontraction in weak-head normal form P . Therefore preforming those headcontraction steps on M allows to obtain a term P so that P P , and therefore P is also in weak-head normal form.

In case γ ≥ ω, there is a finite ordinal k and a limit ordinal γ so that γ = γ + k. Let P = ϕ(γ ), we have that P k -→ ∞ N . As N is in weakhead normal form, there is a finite term P so that P P so that P head-reduces in finitely many steps to P which is in weak-head normal form. By definition of γ, → βδ -reduction sequences, there is θ < γ so that P ϕ(θ). As a consequence, ϕ(θ) head-reduces in finitely many steps to a weak-head normal form. Thus, by transfinite induction, M head-reduces to a weak-head normal form in finitely many steps.

We can now state that Böhm trees are normal forms of infinitary term and that they may be computed with at most ω steps of βδΩ-contraction (this is also a consequence of Corollary 12.9.15 p.701 in Terese [START_REF] Kennaway | Term Rewriting Systems[END_REF]). This also gives Böhm trees an actual computational content since it shows that, provided an infinitary term is given in some effective manner, its Böhm tree can be computed. Hereafter, we use the Krivine machine as an actual device performing this computation.

Theorem 7 Given M in Λ α,∞ (Ω), there an ordinal γ ≤ ω so that M γ -→ Ω,∞ BT (M ).

Canonical terms

Infinitary terms may contain infinitely many free λ-variables. But, as we already said, we are interested in closed terms and the subterms of closed terms contain only finitely many free λ-variables. Thus, from now on, we restrict our attention to terms with finitely many free λ-variables.

It will be convenient to work with terms in what we call canonical form. This form permits to separate λ-variables from Y -variables making recursion and parameter instantiation isolated in a way that will prove useful.

Definition 8 An infinitary term M is in a canonical form when none of its subterms of the form Y x. N contains a free λ-variable.

There is a simple process, that transforms every term M with a finite set of free λ-variables into a canonical form. For this it suffices to abstract away free λ-variables in every subterm Y x. N of M . More precisely, if {x 1 , . . . , x n } is the set of free λ-variables of N (which is necessarily finite) we perform the replacement

Y x. N → (Y y.λx 1 . . . λx n .N [x := yx 1 . . . x n ])x 1 . . . x n
With standard techniques based on approximations, it is rather direct to show that the new term has the same Lévy-Longo tree as M .

Proposition 1 For every infinite closed λY -term M of type 0 over tree signature the result of the above operation is a canonical term generating the same Böhm tree.

Krivine machine

We are now going to introduce the notion of Krivine machine that will allow us to compute the normal forms of infinite terms. Since we wish to treat δ-contraction in a particular manner, we use the Krivine machine to reduce a particular concrete canonical closed term M of type 0. This means that the names of bound variables do matteractually they will matter only for Y -variables. We make this choice to avoid the introduction of environments for Y -variables that would induce some unnecessary notational burden. If we were to be completely rigorous, we should parametrize each notion related to the Krivine machine with this term M , and we should speak about M -Krivine machine, M -environments, M -closures, M -configurations. . . As M will be always clear from the context we will mention it explicitly only if necessary.

Let us fix for this section a concrete canonical term M of type 0. Working with concrete terms gives us some control over Y -variables. We will assume that in the term M every Y -binder binds a distinct Y -variable and that there is no occurrence of Ω. This assumption on the names of Y -variables allows us to stipulate the existence of a function term that maps a Y -variable x α to the subterm Y x α .N of M where it is bound. In later sections, we will represent terms as infinite graphs and the function term will be implemented directly with an edge between Y -binders and the positions they bind in the term.

The Krivine machine [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF], is an abstract machine that computes the weak head normal form of a term, using explicit substitutions, called environments. Environments are functions assigning closures to variables, and closures themselves are pairs consisting of a term and an environment. This mutually recursive definition is schematically represented by the grammar:

C ::= (N, ρ) ρ ::= ∅ | ρ[x → C] .
As in this grammar, we will use ∅ for the empty environment. The notation ρ[x → C] represents the environment which associates the same closure as ρ to variables except for the variable x that it maps to C. The terms N that can be used to form a closure must be subterms of the term M we are considering. This restriction is harmless since, when computing the normal form of M , the Krivine machine only needs closures made with subterms of M (see Theorem 11).

Since we work within a typed context, these two notions follow the typing discipline: in an environment the types of a variable and the closure it is assigned to must be the same. The type of a closure (N, ρ), is simply the type of the term N . We require that in a closure (N, ρ), the environment is defined for every free λ-variable of N , while the values of Y variables are given by term function.

Intuitively a closure C denotes a closed λ-term E(C) as follows. A closure (N, ρ) denotes a λ-term obtained by substituting: (i) for every free λ-variable x of N the term denoted by the closure ρ(x), and (ii) for every free Y -variable x the term term(x). It is important to note that the definition of an environment is inductive, so every environment has finite depth. More precisely this means that every sequence of the form:

ρ 0 (x 0 ) = (N 1 , ρ 1 ), ρ 1 (x 1 ) = (N 2 , ρ 2 ), . . .

is finite and ends in the empty environment.

A stack S ≡ C 1 . . . C n is a possibly empty sequence of closures. We use ⊥ to denote the empty stack.

A configuration of a Krivine machine is a triple (N, ρ, S) where:

1. N is a term (a subterm of M ); 2. ρ is an environment defined for all free variables of N ;

3. S is a stack C 1 . . . C k ,
where k and the types of the closures are determined by the type of N : the type of C i is α i where the type of N is

α 1 → • • • → α k → 0.
A configuration (N, ρ, S) represents an infinitary term:

E((N, ρ, S)) = E(N, ρ)E(C 1 ) . . . E(C n )
where C 1 . . . C n are the closures on the stack S. Notice that the third condition in the definition of configurations implies that E(N, ρ, S) needs to be a term of type 0. Observe also that E(N, ρ, S) may not be a subterm of M even though N as well as every term appearing in ρ, C 1 ,. . . ,C n is. The transition rules of the Krivine machine are:

(λx.N, ρ, (K, ρ )S) →(N, ρ[x → (K, ρ )], S) (Y x.N, ρ, S) →(N, ρ, S) (N K, ρ, S) →(N, ρ, (K, ρ)S) (x, ρ, S) →(N, ρ , S) where (N, ρ ) = ρ(x) (x, ρ, S) →(term(x), ∅, S)
It is rather straightforward to check that these computation rules transform configurations of the Krivine machine into configurations of the Krivine machine. This means that the typing properties of environments and the fact that only subterms of M are used in a closure or as the main term of configuration is preserved by those reduction rules. The first two rules do β-contraction and δ-contraction respectively. The application rule creates a closure and puts it on the stack. The λ-variable rule looks up the meaning of the variable in the environment. The Y -variable rule replaces the variable by its definition. Since we work with concrete canonical terms, there are no free λ-variables in term(x) so the environment can be discarded.

Notice that the terms reduced by the Krivine machine, that are in its environment or on its stack are in general infinite terms which are inspected with respect to their syntax. A more concrete, but equivalent way of representing the same thing would be to build the Krivine machine with addresses in the infinite term and a call to an external mechanism so as to read its labels.

We use the Krivine machine to compute a tree that, as we will see, is the Böhm tree of the term. Recall that we consider only terms over tree signatures and we assume that all the constants are binary (cf. page 5).

Definition 9 Let (N, ρ, ⊥) be a configuration of the Krivine machine, with N a term of type 0. We define the tree KT (N, ρ, ⊥) as follows:

1. if started in (N, ρ, ⊥) the machine reaches a configuration (b, ρ, C 1 C 2 )
where b is a constant and C i = (N i , ρ i ) are closures of type 0, then KT (N, ρ, ⊥) is a tree with the root labelled by b and two subtrees:

KT (N 1 , ρ 1 , ⊥) and KT (N 2 , ρ 2 , ⊥).
2. in the other case KT (N, ρ, ⊥) = Ω 0 .

We write KT (M ) for KT (M, ∅, ⊥).

The next lemma says that Krivine machine computes the weak head normal form (that is the same as head normal form in our case).

Lemma 10 Let (N, ρ, ⊥) be a configuration of the Krivine machine. Term E(N, ρ, ⊥) has a head normal form iff Krivine machine reduces (N, ρ, ⊥) to a configuration (b, ρ, S) for some constant b.

Proof

Recall that Lemma 6 guarantees that head reduction reaches a weak head normal form if a term has one. We also know that Krivine machine performs the head reduction. It suffices to examine in what configurations the machine gets blocked. Looking at the rules we can see that there can be only two kinds of configurations when no rule is applicable. The first is (λx.N, ρ, ⊥), but it is excluded by the third condition on configurations of Krivine machine. The second is (h, ρ, S) where h is either a constant or a variable that is not in the domain of definition of ρ. The case of a variable is also excluded by the second condition on the form of configurations of the Krivine machine. Hence the machine stops when it reaches a constant that is the head of the normal form of E(N, ρ, ⊥).

Lemma 10 entails that the Krivine machine gives an effective way of computing the Böhm tree of an infinitary term. The second statement of the following theorem follows by a direct inspection.

Theorem 11 For a fixed tree signature Σ. For every concrete canonical and closed λY -term M of type 0, we have BT (M ) = KT (M ). All the terms appearing in configurations of the Krivine machine during the computation of KT (M ) are subterms of M .

Transfer theorem for evaluation

In this section we will investigate logical theories of terms and Böhm trees. We will consider monadic-second order logic (MSOL) on such objects. For this, it will be essential to restrict to some finite set of λ-variables: both free and bound. On the other hand, we will be able to handle infinitely many Y -variables. Once we make it clear how to represent terms and Böhm trees as logical structures, we will state our main theorem. We will justify our representation of terms by showing two facts: (i) the set of all terms is definable in MSOL, (ii) unless the polynomial-time hierarchy collapses, the main theorem is false when we do not fix the number of bound λ-variables.

Terms will be represented as labelled, potentially infinite, graphs. For us here such a graph is a structure of the form M = V, {E i } i=1,2 , {P i } i=1,...,n , where V is the set of vertices, every E i is a binary relation on vertices, and every P i is a subset of vertices. We will have two edge relations representing left and right successor. In our case predicates P i will be a partition of V . So every vertex will have a unique label given by the predicate it belongs too.

Monadic second-order logic (MSOL) is an extension of first-order logic with quantification over sets of elements and the membership predicate x ∈ Z, where x is a variable ranging over elements, and Z is a variable ranging over sets of elements. The definition of satisfiability of a formula ϕ in a structure M, denoted M ϕ, is standard.

Let us fix a tree signature Σ with finitely many constants other than Ω. As postulated at the beginning of Section 2.1, for simplicity of notation all the constants are binary. We would like to consider terms as models of formulas of monadic second-order logic. We will work with terms over some arbitrary but finite vocabulary. We take a finite set of typed λ-variables X = {x α1 1 , . . . , x α k k }, and a finite set of types T . We denote by Terms(Σ, T , X ) the set of infinite closed concrete terms 1 M over the signature Σ such that M uses only λ-variables from X , and every subterm of M has a type in T . We also write CTerms(Σ, T , X ) for the terms M of Terms(Σ, T , X ) that are in canonical form. Observe that bound λ-variables in M should come from X . In contrast we do not put restrictions on the use Y -variables. It will be convenient to assume that every Y -variable in M is bound at most once: for every Y -variable x there is at most one occurrence of Y x in M .

A term from Terms(Σ, T , X ) can be seen as a labelled tree where the labels come from finite alphabet, but for the Y -variables and Y binders. We will now eliminate the possible source of infiniteness of labels related to Y -variables and Y binders. Take a closed term M considered as a tree. For every node of this tree labelled by a Y -variable x α we put an E 1 -edge from the node to the node labelled Y x α . Since M is closed, such a node exists and is an ancestor of the node labelled by x; such a node is also unique since we assume that every Y -variable is bound at most once. In the next step we introduce a new symbol α and for every node labelled with a Y -variable of type α, we change its label to α . Finally, we replace all labels of the form Y x α by just Y α . This way we have eliminated all occurrences of Y -variables from labels, but now a term is represented not as a labelled tree but as a labelled graph. Let us denote it by Graph(M ). Observe that the nodes of Y x.

Talph(Σ, T , X ) = Σ ∪ {@ α , Y α , α : α ∈ T } ∪ X ∪ {λ α→β x α : α ∈ T ∧ α → β ∈ T ∧ x α ∈ X } .
There are two edge relations, E 1 and E 2 , in Graph(M ) since nodes labelled by application symbol have both left and right successor. The nodes with other labels have no successor (nodes labeled with labels from Σ ∪ X ) or just one successor, given by E 1 . The example of Graph(M ) is presented in Figure 3.

Since Graph(M ) is a labelled graph over a finite alphabet it makes sense to talk about satisfiability of an MSOL formula in this graph. We will just write M ϕ instead of Graph(M ) ϕ. The first easy, but important, observation is that for fixed Σ, T , X , there is an MSOL formula determining if a graph is of the form Graph(M ) for some M ∈ Terms(Σ, T , X ). Indeed, in this case we deal with models over the signature consisting of two binary relations E 1 , E 2 and a unary relation P b for every b ∈ Talph(Σ, T , X ). The formula should say that P b form the partition of the set of vertices and then express conditions from the definition of infinite λY -terms on page 5. These conditions are clearly expressible in MSOL as they talk about dependencies between labels of a node and its successors.

For a closed term M ∈ Terms(Σ, T , X ) of type 0, its Böhm tree is a tree with nodes labelled by symbols from Σ. Hence one can talk about satisfiability of MSOL formulas in BT (M ). The transfer theorem says that the MSOL-theory of BT (M ) is recursive in the MSOL-theory of M .

Theorem 12 (Transfer theorem) Let Σ be a finite tree signature, X a finite set of typed variables, and T a finite set of types. For every MSOL formula ϕ one can effectively construct an MSOL formula ϕ such that for every λY -term M ∈ Terms(Σ, T , X) of type 0:

BT (M ) ϕ iff M ϕ.
Notice that the formula ϕ is independent from M .

In principle, it is possible to represent terms with an unbounded number of λ-variables by using the same trick for λ-binder as the one we have used for the Y -binder. However, we conjecture that the transfer theorem does not hold when we allow infinitely many λ-variables. Below we give a simple argument under the hypothesis that the polynomial hierarchy is strict.

It is customary to represent booleans with the λ-terms of type 0 → 0 → 0: true is represented by λxy.x and false by λxy.y. This permits the definition of the boolean connectives as terms too: This allows us to represent in a direct manner every quantified boolean formula θ as a simply typed finite closed term M θ such that M θ reduces to true iff θ is true. Observe that M θ has a linear size with respect to that of θ. So if we assume that we are given two distinct terms N true , N false of type 0 we get M θ N true N false reduces to N true iff θ is true. Take an MSOL formula ϕ that is true exactly in Graph(N true ). The transfer theorem without any restriction on the number of λ-variables would give an MSOL formula ϕ such that, for every quantified boolean formula θ: θ is true iff M θ ϕ. The model-checking problem for the fixed formula ϕ belongs to the polynomial hierarchy: the level of the hierarchy is bounded from the above by the alternation of quantifiers in ϕ. So the extension of the transfer theorem to infinite number of λ-variables would imply that QBF satisfiability problem is in the polynomial hierarchy.

Using finite terms to prove that the transfer theorem does not hold in case an unbounded number of λ-variables is allowed cannot give a better result than the example we have given with QBF since the evaluation in a fixed finite model of finite terms that use only types from a finite set T can easily be proved to be in Pspace. Thus, so as to get rid of the hypothesis that the polynomial hierarchy is strict to prove that the transfer theorem does not hold when an unbounded number of λ-variables is allowed, it seems that we need to use an infinite term.

Proof of the transfer theorem

This section presents a proof of the transfer theorem. Before we give the proof we need to introduce parity automata which recognize infinite trees satisfying MSOL formulas. We then give an overview of the the proof. We first prove the transfer theorem for terms in canonical form. We then remove this assumption by observing that transformation of a term into a canonical form is MSOL definable.

Parity autamata and MSOL on infinite binary trees

Recall that Σ is a fixed set of constants of type 0 → 0 → 0. For a closed term M of type 0, these constants label nodes in BT (M ). Since BT (M ) is an infinite binary tree we can use standard non-deterministic parity automata to define sets of Böhm trees. Such an automaton has the form

A = Q, Σ, q 0 ∈ Q, δ : Q × Σ → P(Q 2 ), rk : Q → {1, . . . , d} (1)
where Q is a finite set of states, q 0 is the initial state, δ is the transition function, and rk is a function assigning a rank (a number between 1 and d) to every state. In general, an infinite binary tree is a function t : {0, 1} * → Σ. A run of A on t is a function r : {0, 1} * → Q such that r(ε) = q 0 and for every sequence w ∈ {0, 1} * : (r(w0), r(w1)) ∈ δ(q, t(w)). The run is accepting if for every infinite path in the tree, the sequence of states assigned to this path satisfies the parity condition determined by rk ; this means that the maximal rank of a state seen infinitely often should be even.

Formally, it may be the case that BT (M ) contains also nodes labelled with rk 0 . We will simply assume that every tree containing rk 0 is rejected by the automaton. This is frequently done in this context. Handling rk 0 would not be difficult but would require to add one more case in all the constructions. The other, more difficult, solution is to convert a term to a term not generating rk 0 .

Structure of the proof

The proof of this theorem will use games. The core of the proof will work with concrete terms M in canonical form. Since we have assumed that all our constants are binary, BT (M ) is a binary tree. There is a non-deterministic parity automaton A on infinite binary trees that recognizes binary trees that are models of ϕ. For a concrete canonical term M we will define a game K(A, M ). This game will be presented in terms of configurations of the Krivine machine. Eve will win in K(A, M ) iff BT (M ) is accepted by A. Then we will define a reduced game G(A, M ) with the property that Eve wins in the later game iff she wins in K(A, M ). Finally, we will show that G(A, M ) is MSOL definable inside M (considered as the graph Graph(M )). Since there is an MSOL formula γ win describing games where Eve wins, this gives the desired formula φ. The last step is to remove the assumption that M is in canonical forms. For this it is enough to observe that the translation of M into a canonical form is an MSOL transduction. The schema of the proof is presented in Figure 4.

Game K(A, M )

We now give the definition of RT (A, M ), the runs of the automaton A on the graph of configurations of the Krivine Machine computing BT (M ). The actual runs of A on BT (M ) can easily be read off RT (A, M ).

Definition 13 For a given M ∈ CTerms(Σ, T , X) of type 0 , and a parity automaton A we define the tree of runs RT (A, M ) of A on the graph of configurations of the execution of the Krivine Machine on M :

1. The root of the tree is labeled with q 0 : (M, ∅, ⊥) 2. A node labeled q : (a, ρ, S) has a successor (q 0 , q 1 ) : (a, ρ, S) for every (q 0 , q 1 ) ∈ δ(q, a).

3. A node labeled (q 0 , q 1 ) : (a, ρ, (v 0 , N 0 , ρ 0 )(v 1 , N 1 , ρ 1 )) has two successors q 0 : (N 0 , ρ 0 , ⊥) and q 1 : (N 1 , ρ 1 , ⊥).

4. A node labeled q : (λx.N, ρ, CS) has a unique successor labeled q : (N, ρ[x → C], S).

5.

A node q : (Y x.N, ρ, S) has a unique successor q : (N, ρ, S).

6. A node v labeled q : (x, ρ, S), for x a recursive variable, has a unique successor q : (term(x), ∅, S).

7. A node v labeled q : (N K, ρ, S) has a unique successor labeled q : (N, ρ, (v, K, ρ)S). We say that here a v-closure is created.

8. A node v labeled q : (x, ρ, S), for x a λ-variable and ρ(x) = (v , N, ρ ), has a unique successor labeled q : (N, ρ , S). We say that the node v uses a v -closure.

The definition is as expected but for the fact that in the rule for application we store the current node in the closure. When we use the closure in the variable rule or constant rule (rules 8 and 3), the stored node does not influence the result. The stored node allows us to detect what is exactly the closure that we are using. This will be important in the proof. Notice also that the rules 2,3,4 rely on the typing properties of the Krivine machine ensured by the definition of its configurations (cf. page 13). Indeed, when the machine reaches a configuration of the form (a, ρ, S) then, since we are working with tree signature, a is of type 0 → 0 → 0. In consequence, the stack S consists of two closures of type 0. The environment ρ plays no role in such a configuration as a is a constant. Also from typing invariant we get that, when the machine is in a configuration like (λx.N, ρ, S), S cannot be the empty stack.

Definition 14 We use the tree RT (A, M ) to define a game between two players: Eve chooses a successor in nodes of the form q : (a, ρ, S), and Adam in nodes (q 0 , q 1 ) : (a, ρ, S). We set the parity rank of nodes labeled q : (a, ρ, S) to rk (q), and the parity ranks of all the other nodes to 1. We can use max parity condition to decide who wins an infinite play. Let us call the resulting game K(A, M ).

The following is a direct consequence of the definitions and Theorem 11.

Proposition 2 For every parity automaton A and concrete canonical term M . Eve has a strategy from the root position in K(A, M ) iff A accepts BT (M ).

The only interesting point to observe is that it is important to disallow rank 0 in the definition of parity automaton since we assign rank 1 to all "intermediate" positions. This is linked to our handling of infinite sequences of reductions of the Krivine machine without reaching a head normal form. Such a sequence results in a node labeled rk in a Böhm tree, hence the tree should not be accepted by the automaton. Indeed, in the game K(A, M ) this will give an infinite sequence of states of rank 1.

Hence deciding whether BT (M ) is accepted by A is reduced to deciding who has a winning strategy from the root of K(A, M ). We will introduce a "smaller" game G(A, M ), and show that the winner in the two games is the same. While G(A, M ) will still be infinite, it will be definable by MSOL formula inside the term M itself.

Game G(A, M )

The game K(A, M ) may have infinitely many positions because M is infinite, but also because there may be infinitely many closures that are created.

We reduce this game to G(A, M ) where we remove the second source of infiniteness. The idea of the reduction is to eliminate stacks and environments using alternation. Consider situation in Figure 5. On the top left we have a position v in the game K(A, M ) where the application rule is used. This means that the new closure (K, ρ) is put on the stack of the Krivine machine (node v 1 ). In some descendant v of v 1 the closure may be used. This means that the machine gets to the variable x whose value is the closure in question. Let us consider the simplest case when K is of type 0. Due to the typing invariants on configurations of the Krivine machine, we know that the stack is empty in v . So the configuration in the successor v 1 of v is constructed just from the closure. This observation allows to shortcut the path from v to v 1 . This is what we do in the game G(A, M ).

The right part of Figure 5 represents the result of taking these shortcuts. In a set R, that we call residual of the closure (K, ρ), we have collected all states q which appear when the closure (K, ρ) is used: as in the node v 1 . For every such state we add directly a successor of v labeled with the corresponding configuration. So the edge from v to v 1 in the right picture simulates the path from v to v 1 in the left picture. Now the question is where we get R from. We actually just guess it and check if it is big enough. This is the task of the leftmost transition in the right picture. The gray triangle is the same as in the original game. But this time instead of a closure we have put R on the stack. When we get to v we just check that the state in v is in R. This check guarantees that we have put all uses of the closure into R.

The successive level of complication comes from the fact that K(A, M ) is a parity game and not a reachability game. This complication is not just cosmetic: the same problem for reachability games can be solved using much lighter methods. In order to deal with parity conditions we need not only to remember the state in which the closure is used, but also the biggest rank on the path from creation of the closure to its use. This is symbolized by r in the left part of the figure. We use the same r as the rank of the edge in the reduced game.

The final level of complication comes from the fact that till now we have assumed that K is of type 0, but in general we need to deal with terms K of types of any order. The difference is that if K is not of type 0 then the configuration in v on the left will be of the form q : (x, ρ , S) for some stack S whose type is determined by the type of x, that is the same as the type of K. Observe that the typing invariant of Krivine machine tells us that the orders of types of closures on the stack are always strictly smaller than that of K. So by induction on types we can assume that S is composed of residuals and not of closures. Since there are finitely many residuals, the residual for K will be now a function from sequences of residuals representing possible stacks S to a set of states with ranks as in the case when K had type 0.

After these explanations we will proceed to define residuals, the lifting operation on residuals, and finally the game G(A, M ). The lifting operation on residuals will permit us to deal with all the book-keeping required by the parity condition in an elegant way.

Definition 15 (Residuals) Recall that Q is the set of states of A and d is the maximal value of the rank function of A. Let [d] stand for the set {1, . . . , d}. For every type τ

= τ 1 → • • • → τ k → 0, the set of residuals D τ is the set of functions D τ 1 → • • • → D τ k → P(Q × [d]). For example, D 0 is P(Q × [d]) and D 0→0 is P(Q × [d]) → P(Q × [d]
). The meaning of residuals will become clearer when we will define the game.

A position of the game G(A, M ) will be of one of the forms:

q : (N, ρ, S), or (q 0 , q 1 ) : (N, ρ, S), or (q, R) : (N, ρ, S)

where q, q 0 , q 1 are states of A, N is a subterm of M ; ρ is a function assigning a residual to every λ-variable that has a free occurrence in N , and S is a stack of residuals. Of course the types of residuals will agree with the types of λ-variables/arguments they are assigned to. Notice that we use the same letter ρ to denote an environment as well as an assignment of residuals. Similarly for S. It will be always clear from the context what object is denoted by these letters. We need one more operation before defining the game. Indeed, when a set of residuals is guessed in G(A, M ), it is, as mentioned above, the role of the left transition on the right of figure 5 to check that the guess covers all the possibilities. In the particular case where the term K is of type 0, checking that the residual is correct makes it necessary to verify that the biggest ranks guessed on the paths from the node where the closure is created to the nodes where it is used are correct. The role of the lifting operation we introduce here is to perform this verification. Of course this operation is defined for residuals of any orders.

Definition 16 A lifting of a residual R : D τ 1 → • • • → D τ k → D 0
by a rank r is a residual R r of the same type as R satisfying for every sequence of arguments S: R r (S) = {(q 1 , r 1 ) ∈ R(S) : r 1 > r}∪{(q 1 , r 2 ) : (q 1 , r 1 ) ∈ R(S), r 2 ≤ r 1 = r} Recall that D 0 = P(Q× [d]) so what R r does is to modify the set of pairs R(S) which is the value of R on the sequence of residuals S of appropriate type. The operation leaves unchanged all pairs (q 1 , r 1 ) with r 1 > r. For every pair (q 1 , r 1 ) with r 1 = r it adds pairs (q 1 , r 2 ) for all r 2 ≤ r. All pairs (q 1 , r 1 ) of R(S) with r 1 < r do not contribute to the result.

Example Let's take the residual R = {(q 1 , 1); (q 2 , 2); (q 3 , 3)} of type 0. We have that R 1 ={(q 1 , 0); (q 1 , 1); (q 2 , 2); (q 3 , 3)}, R 2 ={(q 2 , 0); (q 2 , 1); (q 2 , 2); (q 3 , 3)}, R 3 ={(q 3 , 0); (q 3 , 1); (q 3 , 2); (q 3 , 3)}, and

R 4 =∅.
If we take a residual R of type 0 → 0 that maps {(q 1 , 1)} to {(q 2 , 2); (q 3 , 3)} and {(q 2 , 1)} to {(q 1 , 1); (q 3 , 1)}, and all other residuals to ∅ then R 2 maps {(q 1 , 1)} to {(q 2 , 0); (q 2 , 1); (q 2 , 2); (q 3 , 3)} and all other residuals to ∅.

Lemma 17 For every residual R and ranks r 1 , r 2 : (R r 1 ) r 2 = R max(r 1 ,r 2 ) .

If ρ is an environment then ρ r is an environment such that for every x:

(ρ r )(x) = ρ(x) r .
We have all ingredients to define the transitions of the game G(A, M ). Most of the rules are just reformulation of the rules in K(A, M ):

q : (λx.N, ρ, R • S) → q : (N, ρ[x → R], S) q : (a, ρ, R 0 R 1 ) → (q 0 , q 1 ) : (a, ρ, R 0 R 1 )
for (q 0 , q 1 ) ∈ δ(q, a) q : (Y x.N, ρ, S) → q : (N, ρ, S) q : (x, ρ, S) → q : (term(x), ρ, S)

x a recursion variable

We now proceed to the rule for application (cf. Figure 6). Consider q : (N K, ρ, S) with K of type τ = τ 1 → • • • → τ l → 0. We have a transition q : (N K, ρ, S) → (q, R) : (N K, ρ, S) for every residual R :

D τ 1 → • • • → D τ l → D 0 .
From this position we have transitions (q, R) : (N K, ρ, S) → q : (N, ρ, R rk (q) •S)

(q, R) : (N K, ρ, S) → q : (K, ρ r , R 1 • • • R l ) for every R 1 ∈ D τ 1 ,. . . ,R l ∈ D τ l and (q , r ) ∈ R rk (q) (R 1 , . . . , R l ).
In the last line R rk (q) is needed to "normalize" the residual, so that it satisfies the invariant described below.

Since we are defining a game, we need to say who makes a choice in which vertices. Eve chooses a successor from vertices of the form q : (N K, ρ, S), and q : (a, ρ, R 0 R 1 ). It means that she can choose a residual, and a transition of the automaton. This leaves for Adam the choices in nodes of the form (q, R) : (N K, ρ, S). So he decides whether to accept (by choosing a transition of the first type) or to contest residuals proposed by Eve.

Observe that we do not have a rule for nodes with a term being a λvariable. Also positions of the form (q 0 , q 1 ) : (a, ρ, R 0 R 1 ) are terminal. This means that we need to say who is the winner in nodes of these two forms.

For the case of a variable, Eve wins in a position

q : (x, ρ, S) with ρ(x) = R x and S = R 1 • • • R k . if (q, rk (q)) ∈ R x (R 1 , . . . , R k ).
For the case of a constant, Eve wins in a position (q 0 , q 1 ) : (a, ρ, R 0 R 1 ) if (q 0 , rk (q 0 )) ∈ R 0 rk (q 0 ) and (q 1 , rk (q 1 )) ∈ R 1 rk (q 1 ) . Observe that in this case both R 0 and R 1 are necessarily residuals of type 0. Finally, we need to define ranks. It will be much simpler to define ranks on transitions instead of nodes. All the transitions will have rank 1 but for transitions of the form (q, R)

: (N K, ρ, S) → q : (K, ρ r , R 1 • • • R k ) that have rank r .
A play is winning for Eve iff the sequence of ranks on transitions satisfies the parity condition: the maximal rank appearing infinitely often is even.

• We put (q i , max(v, v )) ∈ R(v) when there is v in T labelled q i : (K, ρ, ⊥) having a parent labelled (q 0 , q 1 ) : (a, ρ , C 0 C 1 ) with C i = (v, K, ρ); for i = 0 or i = 1.

For the induction step, suppose that K is of type τ 1 → • • • → τ k → 0 and that we have already calculated residuals for all closures of types τ 1 , . . . , τ k . Suppose that we have a closure (v, K, ρ) created at a node v. This time

R(v) : D τ 1 → • • • → D τ k → P(Q × [d]
). Consider a node v using the closure. Its label has the form q : (x, ρ , S ) for some x, ρ and S such that

ρ (x) = (v, K, ρ). The stack S has the form (v 1 , N 1 , ρ 1 ) . . . (v k , N k , ρ k ) with N i of type τ i . We put (q , max(v, v )) ∈ R(v)(R(v 1 ) max(v 1 ,v ) , . . . , R(v k ) max(v k ,v ) ) .
We now give a formal definition of R(v). By structural induction on types it is easy to see that such an assignment of residuals exists and is unique for T .

Definition 18 (R(v) and res(v, v 1 )) Given T a subtree of K(A, M ), we define a residual R(v) for every application node v of T .

For more clarity we will write res(v, v 1 ) for R(v) max(v,v 1 ) . For a closure (v, K, ρ) we define res((v, K, ρ), v ) = res(v, v ). We then extend this operation to stacks: res(S, v ) is S where res(•, v ) is applied to every element of the stack.

Let v be a node of T labelled by q : (N K, ρ, S) with

K of type τ 1 → • • • → τ k → 0. The residual R(v) is a function D τ 1 → • • • → D τ k → D 0 such
that for every sequence of residuals R of appropriate types the set R(v)( R) contains

• (q , max(v, v )) for every node v of T with the label of the form q : (x, ρ , S ) for some x, ρ , S such that ρ (x) = (v, K, ρ), and res(S , v ) = R.

• (q i , max(v, v )), for every node v labelled q i : (K, ρ, ⊥) having a parent labelled (q 0 , q 1 ) : (a, ρ , C 0 C 1 ) with C i = (v, K, ρ); for i = 0 or i = 1. Notice that this case applies only if K is of type 0.

Transferring Eve's strategy in

K(A, M ) to G(A, M )
Let's assume that Eve has a winning strategy σ on K(A, M ) defining the subtree K σ of K(A, M ). Let's also assume that we have computed the residuals for K σ as in Definition 18. We will use the residuals to define a winning strategy for Eve in G(A, M ).

Proof

Take two sequences S 1 and S 2 of the correct type with respect to R 1 and R 2 and such that Comp(S 1 , S 2 ). Since Comp(R 1 , R 2 ), we have R 1 (S 1 ) ∩ R 2 (S 2 ) = ∅. Let's suppose that (q 1 , r 1 ) is in R 1 r (S 1 ), then either r 1 > r and (q 1 , r 1 ) is in R 1 (S 1 ) so that (q 1 , r 1 ) is neither in R 2 (S 2 ) nor in R 2 r (S 2 ); or r 1 ≤ r and (q 1 , r) is in R 1 (S 1 ) so that (q 1 , r) is not in R 2 (S 2 ) and (q 1 , r 1 ) is not in R 2 r (S 2 ). Similarly we get that whenever (q 2 , r 2 ) is in R 2 r (S 2 ) it is not in R 1 r (S 1 ). Therefore R 1 r (S 1 ) ∩ R 2 r (S 2 ) = ∅. Since S 1 , S 2 were arbitrary, we get Comp(R 1 r , R 2 r ).

As in the case for Eve, the strategy for Adam will take a pair of vertices (v 1 , v 2 ) from G(A, M ) and K(A, M ), respectively. It will then consult the strategy θ for in K(A, M ) and calculate a new pair (v 1 , v 2 ). All the pairs will satisfy the invariant: v 1 labeled by q : (N, ρ 1 , S 1 ) and v 2 labeled by q : (N, ρ 2 , S 2 ); where Comp(ρ 1 , res(ρ 2 , v 2 )) and Comp(S 1 , res(S 2 , v 2 ));

The strategy We define the strategy by considering one by one the rules for constructing the tree K(A, M ). The only case where Adam makes a choice is the application rule.

A node labeled q : (N K, ρ 1 , S 1 ) is a node of Eve and it has successors labeled (q, R) : (N K, ρ 1 , S 1 ) for every residual R of appropriate type. Suppose Eve chooses some R and in consequence such a node v 1 . Then Adam has a choice between the children of v 1 that have labels of the form: q :(N, ρ 1 , R rk (q) •S 1 ) (4)

q :(K, ρ 1 r , R 1 • • • R l ) for (q , r ) ∈ R rk (q) (R 1 , . . . , R l ) (5)
At the same time the node v 2 of K(A, M ) is an application node so it has assigned residual R(v 2 ). We have two cases. Suppose Comp(R rk (q) , R(v 2 )) holds. In this case Adam chooses for v 1 the node labeled q : (N, ρ 1 , R rk (q) •S 1 ). This works since the successor v 2 of v 2 is labeled by q : (N, ρ 2 , (v 2 , K, ρ)S 2 ); hence the pair (v 1 , v 2 ) satisfies the invariant.

The other case is when Comp(R rk (q) , R(v 2 )) does not hold. This means that there are (R 1,1 , . . . , R 1,l ) and (R 2,1 , . . . , R 2,l ) such that Comp(R 1,i , R 2,i ) for all i = 1, . . . , l and R rk (q) (R 1,1 , . . . , R 1,l ) ∩ R(v 2 )(R 2,1 , . . . , R 2,l ) = ∅. Let (q , r ) be the element from the intersection. Examining the definition of R(v 2 ), Definition 18, there are two reasons why (q , r ) ∈ R(v 2 )(R 2,1 , . . . , R 2,l ).

The first case (see figure 8) is when there is in K θ a node v 2 labeled by q : (x, ρ 2 , S 2 ) such that ρ 2 (x) = (v 2 , K, ρ 2 ), res(S 2 , v 2 ) = (R 2,1 , . . . , R 2,l ) and r = max(v 2 , v 2 ). In that case, we choose for v 1 the node labeled q : (K, ρ 1 r , R 1,1 • • • R 1,l ). As its companion node we choose the successor v 2 of v 2 labelled by q : (K, ρ 2 , S 2 ). So the new position becomes (v 1 , v 2 ). We need to show that Comp(ρ 1 r , res(ρ 2 , v 2 )) holds. For this take an arbitrary variable y for which ρ 1 (y) is defined. Since Comp(ρ 1 , res(ρ 2 , v 2 )) we have Comp(ρ 1 (y), res(ρ 2 (y), v 2 )). As r = max(v 2 , v 2 ) = max(v 2 , v 2 ) we have res(ρ 2 (y), v 2 ) = res(ρ 2 (y), v 2 ) r , and then by Lemma 19 we get the required Comp(ρ 1 (y) r , res(ρ 2 (y), v 2 ) r ). And of course, by hypothesis we have Comp(R 1,i , R 2,i ) for all i = 1, . . . , l so that the new configuration satisfies the invariant.

v 1 v 1 v 1 q : (N K, ρ 1 , S 1 ) (q, R rk (q) ) : (N K, ρ 1 , S 1 ) q : (K, ρ 1 r , ⊥) r = max(v 2 , v 2 ) v 2 v 2 v 2 q : (N K, ρ 2 , S 2 ) q : (N, ρ 2 , (v 2 , K, ρ 2 )S 2 ) q : (x, ρ 2 , S 2 ) where ρ 2 (x) = (v 2 , K, ρ 2 ) res(S 2 , v 2 ) = R 2,1 . . . R 2,l , and
Comp(R 1,i , R 2,i ) q : (K, ρ 2 , S 2 ) Figure 8: First case when (q , r ) ∈ R rk (q) (R 1,1 , . . . , R 1,l ) ∩ R(v 2 )(R 2,1 , . . . , R 2,l )
The second case (see Figure 9) is when K has type 0 and there is in K θ a node v 2 labelled q i : (K, ρ 2 , ⊥), with q i = q , having a parent labelled (q 0 , q 1 ) : (a, ρ , C 0 C 1 ) with C i = (v, K, ρ 2 ); for i = 0 or i = 1 (Figure 9 represents the case where i = 0); and r = max(v 2 , v 2 ). For v 1 take the node labelled q : (K, ρ 1 r , ⊥), and for its companion take the node v 2 . We need to show that Comp(ρ 1 r , res(ρ 2 , v 2 )) holds. For this take arbitrary variable y for which ρ 1 (y) is defined. Since Comp(ρ 1 , res(ρ 2 , v 2 )) we have Comp(ρ 1 (y), res(ρ 2 (y), v 2 )). As r = max(v 2 , v 2 ) we have res(ρ 2 (y), v 2 ) = res(ρ 2 (y), v 2 ) r , and then by Lemma 19 we get the required Comp(ρ 1 (y) r , res(ρ 2 (y), v 2 ) r ).

v 1 v 1 v 1 q : (aK, ρ 1 , S 1 ) (q, R rk (q) ) : (aK, ρ 1 , S 1 ) q : (K, ρ 1 r , ⊥) r = max(v 2 , v 2 ) v 2 v 2 q : (N K, ρ 2 , S 2 ) q : (N, ρ 2 , (v 2 , K, ρ 2 )S 2 ) (q 0 , q 1 ) : (a, ρ 2 , (v 2 , K, ρ 2 )C 1 )
q : (K, ρ 2 , ⊥) with q = q 0 Figure 9: Second case when (q , r ) ∈ R r ∩R(v 2 ) (with i = 0)

The strategy is winning As in the case of the strategy for Eve, it is easy to show that every infinite play is winning. It remains to check what happens if v 1 is a variable node or a constant node.

A variable node is labeled by q : (x, ρ 1 , S 1 ). To show that Adam wins here we need to prove that (q, rk (q)) ∈ R x (S 1 ) where R x = ρ 1 (x).

By the invariant, the companion node v 2 is labeled by q : (x, ρ 2 , S 2 ) and satisfying

Comp(R x , res(ρ 2 , v 2 )(x)), Comp(S 1 , res(S 2 , v 2 )) .
Suppose ρ 2 (x) = (v, N, ρ). Then (q, max(v, v 2 )) ∈ R(v)(res(S 2 , v 2 )) by the definition of R(v) (Definition 18). Hence we also have

(q, max(v, v 2 )) ∈ R(v)(res(S 2 , v 2 )) max(v,v 2 ) ,
and in consequence

(q, rk (q)) ∈ R(v)(res(S 2 , v 2 )) max(v,v 2 ) . As R(v) max(v,v 2 ) = res(ρ 2 , v 2 )(x) we get Comp(R x , R(v) max(v,v 2 ) (x))
, from the invariant. As Comp(S 1 , res(S 2 , v 2 )) we can obtain (q, rk (q)) ∈ R x (S 1 ) by the definition of Comp.

A constant node is labelled by (q 0 , q 1 ) : (a, ρ 1 , R 0 R 1 ). To show that Adam wins here we need to prove that (q i , rk (q i )) ∈ R i rk (q i ) for i = 0 or i = 1. By the invariant, the companion node v 2 is labeled by (q 0 , q 1 ) : (a, ρ 2 , C 0 C 1 ) and satisfying Comp(R i , res(C i , v 2 )) for i = 0, 1. The node v 2 must have a successor in K θ . Let it be q 0 : (N, ρ, ⊥) where C 0 = (v, N, ρ). We will show that (q 0 , rk (q 0 )) ∈ R 0 rk (q 0 ) . We have Comp(R 0 , res(C 0 , v 2 )) so also Comp(R 0 rk (q 0 ) , res(C 0 , v 2 ) rk (q 0 ) ) by Lemma 19. But then we have res(C 0 , v 2 ) rk (q 0 ) is (R(v) max(v,v 2 ) ) rk (q 0 ) . Let m = max((max(v, v 2 ), rk (q 0 )). By definition of R(v), Definition 18, (q 0 , m) ∈ R(v). Then (q 0 , m) ∈ R(v) max(v,v 2 ) and (q 0 , m) ∈ (R(v) max(v,v 2 ) ) rk (q 0 ) so that (q 0 , rk (q 0 )) ∈ (R(v) max(v,v 2 ) ) rk (q 0 ) . By the definition of Comp predicate (q 0 , rk (q 0 )) ∈ R 0 rk (q 0 ) .

Transductions

In this subsection we will finish the proof of the theorem. We know that for every term M in concrete canonical form: BT (M ) ϕ iff Eve has a winning strategy in the game K(A, M ). We have also shown that the later condition is equivalent to Eve having a winning strategy in G(A, M ). To conclude we will construct a formula ϕ such that M ϕ iff Eve has a winning strategy in G(A, M ). We will also show how to get rid of the assumption that M is in a canonical form.

In order to construct the formula ϕ we will examine the definition of the game and use MSOL transductions. Positions of G(A, M ) (cf. Section 4.4) are subterms of M together with some information of a bounded size: a state of A, an environment ρ assigning residuals to λ-variables, and a stack of residuals. We make it precise in the following lemma.

Lemma 20 There is a number, call it maxpos, depending only on Σ, T and X such that for every subterm N of a term M ∈ Terms(Σ, T , X ), the number of positions in G(A, M ) of the form q : (N, ρ, S) is bounded by maxpos.

Proof

First observe that the number of residuals of a given type is finite. A residual of type 0 is a subset of Q × [d] where Q is the set of states of A and d is the maximal value of the rank function of A. A residual of type α → β is a function from residuals of type α to residuals of type β. Recall that ρ is a function assigning residuals to free λ-variables of N . So the number of possible ρ is bounded since λ-variables come from a fixed finite set X , and the type of the residual assigned to a λ-variable is determined by the type of the λ-variable. For the stack S, we know that the type of N determines the type of S in the sense that it determines the length of the sequence S and the type of each element of the sequence. Since the type of N belongs to the finite set of types T we have that the number of possible stacks depends on T and not on N .

We will argue that it is possible to define G(A, M ) inside Graph(M ) by means of formulas of MSOL. In other words, that for a fixed A, the mapping from M to G(A, M ) is a monadic second-order transduction. Having done this, the desired formula ϕ will come from the inverse image determined by this transduction of the formula defining games where Eve has a winning strategy.

First observe that the game G(A, M ) can be represented with a structure over a signature depending only on A. To represent G(A, M ), we need a predicate determining the transitions in the game, a predicate distinguishing the positions for Eve, and a predicate for every rank in order to encode the parity condition. So the signature depends only on ranks and these come from A. We will write G(A, M ) ψ to mean that ψ holds in the structure representing G(A, M ). Recall that for every fixed set of ranks, there is an MSOL formula defining the set of parity games where Eve has a winning strategy. Let γ win be such a formula for the set of ranks determined by A. We have:

G(A, M ) γ win iff Eve wins in G(A, M ) (6)
In order to define G(A, M ) inside Graph(M ), we will need a transduction that duplicates a given structure a certain number of times. Take a natu-ral number k and let [k] stand for {1, . . . , k}. Consider a structure M = V, E 1 , E 2 , P 1 , . . . , P l , in our case it will be a graph of a term. A k-fold duplication of M is a structure M×[k] = V ×[k], E 1 , E 2 , eq, P 1 , . . . , P l , C 1 , . . . , C k whose elements are pairs (v, i) ∈ V × [k]; we think of (v, i) as of v in the i-th copy. The relations E 1 , E 2 are as in M, that is they hold between elements of the same copy: E 1 ((v, i), (v , j)) iff E 1 (v, v ) and i = j. The eq predicate says that two elements are copies of the same element: eq((v, i), (v , j)) iff v = v . Predicates P 1 , . . . , P l are as in M: P i (v, j) if P i (v). Finally, predicate C i holds for all elements of copy i: C i (v, j) iff i = j.

It is well-known [START_REF] Courcelle | Monadic second-order graph transductions: A survey[END_REF] that for every k and MSOL formula ψ there is a formula ψ/[k] such that for every structure M:

M × [k] ψ iff M ψ/[k] (7)
Let M be a term and maxpos the constant from the Lemma 20. We will show how to define G(A, M ) in Graph(M ) × [maxpos]. A configuration of G(A, M ) has a form q : (N, ρ, S). We will think of it as consisting of a term N and a context q : (•, ρ, S). To every possible context q : (•, ρ, S) we can associate a number from [maxpos]. So a node (v, i) in Graph(M )×[maxpos] is a configuration q : (N v , ρ, S) where N v is the term rooted in v and q : (•, ρ, S) is the context number i. We write C q:(•,ρ,S) for C i where i is the number of the context. With this convention one can directly express the transitions of the game G(A, M ) with MSOL formulas over M × [k]. We give two examples. For all N the transitions :

q : (λx.N, ρ, R • S) → q : (N, ρ[x → R], S) are defined by next λ (z, z ) ≡ C q:(•,ρ,R•S) (z) ∧ P λx (z)∧ ∃z . E 1 (z, z ) ∧ eq(z , z ) ∧ C q(•,ρ[x →R],S) (z )
The transitions on Y -variables are defined by

next (z, z ) ≡ C q:(•,ρ,S) (z) ∧ P (z) ∧ ∃z .E 1 (z, z ) ∧ eq(z , z ) ∧ C q:(•,∅,S)
Observe that the formulas depend on A but not on M . These formulas define G(A, M ) inside Graph(M ) × [maxpos]. We obtain that for every formula ψ there is a formula ψ int such that for all M :

G(A, M ) ψ iff Graph(M ) × [k] ψ int . (8)
We now have all ingredients to prove the following lemma.

Lemma 21 For a fixed A, T and X . There is a formula ϕ A such that for every term M ∈ CTerms(Σ, T , X )

Even wins in G(A, M ) iff Graph(M ) ϕ A Indeed it is enough to use the properties from (6), ( 7), (8). The formula ϕ A from the lemma is (γ int win )/[maxpos]. Recall that the automaton A was supposed to be equivalent over trees to our initial formula ϕ. If M is a concrete canonical term then Proposition 2 tells us that BT (M ) ϕ iff Eve wins in K(A, M ). By Proposition 3, the later condition is equivalent to Eve winning in G(A, M ). The lemma above says that this is equivalent to Graph(M ) ϕ A . Thus we can take ϕ A as our formula ϕ in Theorem 12. Observe that this formula does not depend on M .

The last step in the proof is to remove the hypothesis of M being concrete canonical. The translation presented in Section 2.3 is actually an MSOL transduction. So we have that for every formula ψ there is a formula ψ C such that for every term M :

Can(M ) ψ iff M ψ C
Putting this together we get that for if we start with M not in canonical form we should take ϕ C .

Consequences of the transfer theorem for evaluation

The objective of this short section is to present several corollaries of the transfer theorem. The first consequence is the decidability of the MSOL theory of BT (M ) for every finite term M of λY -calculus. This gives another proof of the result of Ong [START_REF] Ong | On model-checking trees generated by higherorder recursion schemes[END_REF], since for every higher-order recursive scheme F there is a finite term M such that BT (M ) is the tree generated by F (see [START_REF] Salvati | Recursive schemes, Krivine machines, and collapsible pushdown automata[END_REF]).

Corollary 22 For every finite term M of λY -calculus, the MSOL theory of BT (M ) is decidable.

The part of the strength of the transfer theorem comes from the fact that the formula ϕ does not depend on M but just on Σ, T and X . This has an immediate consequence that once Σ, T and X are fixed, every MSOL property of Böhm trees is an MSOL property of terms. For example, since the set of finite trees is MSOL definable, the set of terms from Terms(Σ, T , X ) having a normal form, i.e. that reduce to a finite term in a normal form, is also MSOL definable.

Decidability of higher-order matching restricted to Terms(Σ, T , X ) without fixpoint operators follows also by the same type of reasoning. The problem is stated as follows. Given a finite term M , and a closed finite term K with no occurrence of Y : can one replace free variables of M with terms in such a way that the result is β-equal to K.

Corollary 23 Fix Σ, T , X . For every pair of terms M, K ∈ Terms(Σ, T , X ) such that K is closed and does not have fixpoint operators. It is decidable if there is a substitution σ such that M σ = β K.

Let us briefly sketch the argument. For a term M we will write shape(M ) for an MSOL formula defining the set of terms that can be obtained from M by substitutions. This formula just states that the top of the tree is the term M , but in places where M has free variables the tree is arbitrary, but without Y binders. Since K is a term without Y binder, it has a normal form K that is a finite term. Since K does not have free variables, shape(K) defines exactly one term. Suppose that shape(K) is our formula ϕ and take ϕ given by the theorem. Consider the formula shape(M ) ∧ ϕ

We have that a term satisfying this formula is obtained from M by a substitution, and that its normal form is K . So the higher-order matching problem for M and K reduces to satisfiability of this formula. Observe that in principle the substitution can use infinite terms. Nevertheless, recall that if there is a tree satisfying an MSOL formula then there is a regular one. This means that if there is a solution to a matching problem then there is one that is a finite term. Here we allowed both M and σ to use fixpoint operators, we can disallow this by adding one more conjunct to the formula above. The decidability of the case without fixpoints has already been shown by Schmidt-Schauß [START_REF] Schmidt-Schauß | Decidability of arity-bounded higherorder matching[END_REF] (see also [START_REF] Salvati | Recognizability in the simply typed lambdacalculus[END_REF]).

Next, we would like to present a kind of synthesis result. The task is to construct a program satisfying a given specification from a given finite set of modules. The specification is given by an MSOL formula ϕ. Every module is a finite λY -term.

Corollary 24 Given a formula ϕ and finite set of closed λY -terms M 1 . . . , M l . It is decidable if there is a closed term K constructed from M 1 . . . , M l by means of application, Y -variables and Y -binders, such that BT (K) ϕ. If there is a such a term then there exists a finite one.

The requirement that K does not use constants from the signature is essential, since otherwise we could get a trivial solution ignoring the modules. For the proof of the corollary consider terms of the form (λx 1 . . . x l .N )M 1 . . . M l where N is constructed only with applications, Y -variables and Y -binders. Indeed, after reducing this term l-times we get a term as required in the corollary. So the restriction on the shape of K can be expressed by a formula shape((λx 1 . . . x l .z)M 1 . . . M l ) ∧ γ, where γ is a formula saying that the only labels appearing in the subtree starting in the node corresponding to z are variables x 1 , . . . , x l , application, Y -variables, and fixpoint binders. Summing-up, the solution to the problem states in the corollary is to decide the satisfiability of the formula ϕ ∧ shape((λx 1 . . . x l .z)M 1 . . . M l ) ∧ γ .

This formula asks for a term of the particular shape such that when evaluated gives a Böhm tree satisfying ϕ. Once again, if there is a solution then there is a regular solution, that is a finite term.

Conclusion

We have shown that every MSOL property of Böhm trees is effectively an MSOL property of terms. The possibility that such a transfer theorem may hold has been indicated by a number of results in the literature: Ong's Theorem [START_REF] Ong | On model-checking trees generated by higherorder recursion schemes[END_REF] stating that the MSOL properties of Böhm trees of λY -terms is decidable; Courcelle and Knapik's [START_REF] Courcelle | The evaluation of firstorder substitution is monadic second-order compatible[END_REF] result showing a similar theorem for a variant of evaluation of first-order terms; and finally, a result of Salvati [START_REF] Salvati | Recognizability in the simply typed lambdacalculus[END_REF] demonstrating that in the context of λ-calculus, recognizability is preserved under inverse homomorphism.

The translation we propose for going form MSOL properties of Böhm trees to MSOL properties of λY -terms not only works for infinite terms but also depends on very few properties of terms themselves. We just need to fix a finite set of λ-variables that a term can use as well as a finite set of types that the subterms of a term may have. Apart from this, the translation does not depend on any other structural properties of terms. This is rather surprising as the set of terms that use a fixed number of λ-variables does not form a set that is closed under βδ-reduction. For this reason the method of Courcelle and Knapik could not be extended to higher-order types, since due to α-conversion intermediate results of evaluation could need an unbounded number of λ-variables. The invariants on reduction that we express with the Krivine machine and residuals overcome this difficulty.

The obvious question is the relation of our transfer theorem concerning βδ-reduction to two other transfer results concerning unfolding operation [START_REF] Courcelle | Monadic second-order logic, graphs and unfoldings of transition systems[END_REF] and for Muchnik iteration [START_REF] Semenov | Decidability of monadic theories[END_REF][START_REF] Walukiewicz | Monadic second order logic on tree-like structures[END_REF], respectively. Recall that while Muchnik iteration is strictly stronger than unfolding, the two operations can be used to define the classes of trees forming so called pushdown hierarchy [START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF].

We cannot compare directly the three results since the transfer theorems for unfolding [START_REF] Courcelle | Monadic second-order logic, graphs and unfoldings of transition systems[END_REF] and Muchnik iteration [START_REF] Semenov | Decidability of monadic theories[END_REF][START_REF] Walukiewicz | Monadic second order logic on tree-like structures[END_REF] work on graphs, while our theorem works with λY -terms that seen as graphs are trees with back edges. For this reason we cannot say that our result implies the other two. Yet, if restricted to trees with back edges, the result on unfolding is a special case of our result: the unfolding can be simulated by δ-reduction. We do not know if it is possible to simulate Muchnik iteration directly using βδ-reduction. Nevertheless, it is well-known that, up to simple MSOL-interpretations, every tree in the pushdown hierarchy is a result of a βδ-reduction of a finite term. Hence, similarly to Muchnik's iteration, βδ-reduction allows to obtain all trees in the pushdown hierarchy [START_REF] Caucal | On infinite terms having a decidable monadic theory[END_REF]. Moreover, thanks to the recent result of Parys [START_REF] Parys | On the significance of the collapse operation[END_REF], we know that βδreduction can give trees that do not belong to the pushdown hierarchy. This shows that our transfer theorem is not a consequence of the Muchnik's theorem. The study of relations between Muchnik iteration and βδ-reduction, as well as constructing new hierarchies using the new transfer theorem, are interesting directions for further research.

Figure 2 :

 2 Figure 2: Böhm tree and the associated term

Figure 3 :

 3 Figure 3: M and Graph(M )

  and = λb 1 b 2 xy.b 1 (b 2 xy)y, or = λb 1 b 2 xy.b 1 x(b 2 xy) and neg = λbxy.byx. One can also define propositional quantifiers All = λf.and (f true)(f false) and Ex = λf.or (f true)(f false).

Figure 4 :

 4 Figure 4: Schema of the proof

Figure 5 :

 5 Figure 5: Game K(A, M ) on the left, and G(A, M ) on the right.

Figure 6 :

 6 Figure 6: Dealing with application in G(A, M ).

Recall that concrete terms are particular elements of α-equivalence classes.

Equivalence of G(A, M ) and K(A, M )

We are now going to prove the central property relating G(A, M ) and K(A, M ).

Proposition 3 For every parity automaton A and concrete canonical term M . Eve wins in K(A, M ) iff Eve wins in G(A, M ).

The proof of this lemma proceeds as follows. For the direction from left to right we take a winning strategy for Eve in K(A, M ) and define residuals for every closure with respect to this strategy. Then we show how Eve is winning in G(A, M ) using these residuals. The winning strategy in G(A, M ) will simulate the one in K(A, M ). For the other direction we will calculate residuals with respect to Adam's winning strategy in K(A, M ) and use them to define Adam's winning strategy in G(A, M ). As parity games are determined, we obtain Proposition 3.

Residuals in K(A, M )

We here introduce the key notion of the proof, the notion of residuals of nodes. Given a subtree T of K(A, M ), i.e. a tree obtained from K(A, M ) by pruning some of its subtrees, we calculate the residuals R T (v) and res T (v, v ) for some nodes and pair of nodes of T . In particular, T may be taken as being a strategy of Eve or a strategy of Adam. When T is clear from the context we will simply write R(v) and res(v, v ).

Recall that a node v in K(A, M ) is an application node when its label is of the form q : (N K, ρ, S). We will assign a residual R(v) to every application node v. Thanks to typing, this can be done by induction on the order of type. We also define a variation of this notion: a residual R(v) seen from a node v , denoted res(v, v ). The two notions are the main technical tools used in the proof of the theorem.

Before giving a formal definition we will describe the assignment of residuals to nodes in concrete terms. We will need one simple abbreviation. If v is an ancestor of v in T then we write max(v, v ) for the maximal rank appearing on the path between v and v , including both ends.

Consider an application node v in T . It means that v has a label of the form q : (N K, ρ, S), and its unique successor has the label q : (N, ρ, (v, K, ρ)S). That is the closure (v, K, ρ) is created in v. We will look at all the places where this closure is used and summarize the information about them in R(v). We will do this by induction on the type of K.

First, suppose that the closure, or equivalently the term K, is of type 0.

We have two cases

The invariant Will use positions in the game K(A, M ) and the strategy σ as hints. The strategy in G(A, M ) will take a pair of positions (v 1 , v 2 ) with v 1 in G(A, M ) and a v 2 in K(A, M ). It will then give a new pair of positions (v 1 , v 2 ) such that v 1 is a successor v 1 , and v 2 is reachable from v 2 using the strategy σ. Moreover, all visited pairs (v 1 , v 2 ) will satisfy the following invariant:

• v 1 is labeled by q : (N, ρ 1 , S 1 ) and v 2 is labeled by q : (N, ρ 2 , S 2 ), where

• v 1 is labeled by (q 0 , q 1 ) : (a, ρ 1 , S 1 ) and v 2 is labeled by (q 0 , q 1 ) :

The strategy The initial positions in both games have the same label q 0 : (M, ∅, ⊥), so the invariant is satisfied. In order to define the strategy we will consider one by one the rules defining the transitions in G(A, M ). The two cases where Eve needs to decide which successor to chose are the nodes with a constant or with an application. A node with a constant is of the form q : (a, ρ 1 , R 0 R 1 ). Eve should then simply take the same transition of the automaton as taken from v 2 . So it advances to a node labelled (q 0 , q 1 ) : (a, ρ 1 , R 0 R 1 ). It is clear that the invariant is satisfied as the environment and the stack do not change. This implies moreover that no matter what Adam's next move is, the new position also satisfies the invariant.

The strategy and its analysis in the case of application node is more complicated. Suppose that the term in the label of v 1 is an application, say q : (N K, ρ 1 , S 1 ). By our invariant we have a position v 2 labeled by q : (N K, ρ 2 , S 2 ), where ρ 1 = res(ρ 2 , v 2 ) and S 1 = res(S 2 , v 2 ). To satisfy the invariant, the strategy in G(A, M ) needs to choose R(v 2 ), that is the residual assigned to v 2 . This means that from v 1 the play proceeds to the node v 1 labeled (q, R(v 2 )) : (N K, ρ 1 , S 1 ). From this node Adam can choose either

The unique successor v 2 of v 2 is labeled by q : (N, ρ 2 , (v 2 , K, ρ 2 )S 2 ). So the pair (v 1 , v 2 ) satisfies the invariant.

Let us now examine the case where Adam chooses for v 1 a node of the form (3) for some q , r and R 1 . . . R l (see Figure 7). Looking at the definition of R(v 2 ), Definition 18, the first possible case is that in K σ the node v 2 has a descendant v 2 labeled q : (x, ρ 2 , S 2 ) with ρ 2 (x) = (v 2 , K, ρ 2 ), res(S 2 , v 2 ) = R 1 . . . R l and moreover r = max(v 2 , v 2 ). The successor v 2 of v 2 is labeled by q : (K, ρ 2 , S 2 ). We can take it as a companion for v 1 since ρ 1 r = res(ρ 2 , v 2 ) max(v 2 ,v 2 ) = res(ρ 2 , v 2 ) by Lemma 17. Hence the pair (v 1 , v 2 ) satisfies the invariant.

Figure 7: Adam chooses a node of the form (3)

The second possibility for (q , r ) ∈ R(v 2 ) rk (q) is when K has type 0, and there is a node v 2 labelled q i : (K, ρ, ⊥) having a parent labelled (q 0 , q 1 ) : (a, ρ , C 0 C 1 ) with C i = (v, K, ρ); for i = 0 or i = 1. By definition of R(v 2 ) we have that r = max(v 2 , v 2 ). We can take v 2 as a companion of v 1 since ρ 1 r = res(ρ 2 , v 2 ) max(v 2 ,v 2 ) = res(ρ 2 , v 2 ) by the invariant and Lemma 17. Hence the pair (v 1 , v 2 ) satisfies the invariant.

The strategy is winning We need to show that the strategy defined above is winning. Consider a sequence of nodes (v 1 1 , v 1 2 ), (v 2 1 , v 2 2 ), . . . consistent with the strategy. Suppose that this sequence is infinite. By construction we have that v 1 2 , v 2 2 , . . . is a path in K σ , hence a play winning for Eve. We have defined the strategy in such a way that a rank of a transition from v i 1 to v i+1 1 is the same as the maximal rank of a node on the path between v i 2 and v i+1 2 . Hence v 1 1 , v 2 1 , . . . is winning for Eve too. It remains to check what happens when a maximal play is finite. This means that the path ends in a pair (v 1 , v 2 ) where v 1 is a variable node or a constant node.

A variable node is labeled by q : (x, ρ 1 , S 1 ). To show that Eve wins here we need to prove that (q, rk (q)) ∈ R x (S 1 ) where R x = ρ 1 (x).

By the invariant we have that the companion node v 2 is labeled by q : (x, ρ 2 , S 2 ) and

. This is the required statement (q, rk (q)) ∈ R x (S 1 ).

A constant node is labeled by (q 0 , q 1 ) : (a, ρ 1 , R 0 R 1 ). We need to show that (q i , rk (q i )) ∈ R i rk (q i ) , for i = 0, 1. Let i = 0, the argument is the same for i = 1. By the invariant we have that the companion node v 2 is labeled by (q 0 , q 1 ) : (a, ρ 2 , C 0 C 1 ). Suppose C 0 is (v, N, ρ). So v 2 has a successor v 2 labelled with q 0 : (N, ρ, ⊥). We have that R 0 = R(v) max(v,v 2 ) , since S 1 = res(S 2 , v 2 ) by the invariant. By definition of R(v) we get (q 0 , m) ∈ R(v); where m = max(v, v 2 ). From the definition m operation: (q 0 , m) ∈ R(v) m . Which implies (q 0 , rk (q 0 )) ∈ R(v) m as rk (q 0 ) ≤ m. Since m = max(max(v, v 2 ), rk (q 0 )) we get R(v) m = (R(v) max(v,v 2 ) ) rk (q 0 ) = R 0 rk (q 0 ) , and we are done.

Transferring Adam's strategy from

We will show how to get a winning strategy for Adam in G(A, M ) form his winning strategy in K(A, M ). Once again we will use residuals. Let us fix a winning strategy θ of Adam in K(A, M ), and consider the tree K θ of plays respecting this strategy. This is a subtree of K(A, M ). Consider the assignment of residuals to application nodes in K θ as in Definition 18. We will define a strategy in G(A, M ) that will preserve the invariant described below.

The invariant In order to formulate the invariant for the strategy we introduce complementarity predicate Comp(R 1 , R 2 ) between a pair of residuals:

) for all i = 1, . . . , k we get R 1 (R 1,1 , . . . , R 1,k ) ∩ R 2 (R 2,1 , . . . , R 2,k ) = ∅.

Remark: Comp predicate is a logical relation (see [START_REF] Amadio | Domains and Lambda-Calculi[END_REF]), but we have prefer to formulate the definition in a form that will be more useful for proofs.

For two closures (v, N, ρ) and (v , N, ρ ) we will say that the predicate Comp((v, N, ρ), (v , N, ρ )) holds if Comp(R(v), R(v )) is true. For two environments ρ, ρ we write Comp(ρ, ρ ) if the two environments have the same domain and for every x, the predicate Comp(ρ(x), ρ (x)) holds. Finally, Comp(S, S ) holds if the two sequences are of the same length and the predicate holds for every coordinate.

It is important to observe that Comp behaves well with respect to r operation Lemma 19 If Comp(R 1 , R 2 ) then also Comp(R 1 r , R 2 r ) for every rank r.