We prove the decidability of the logic T→ of Ticket Entailment. Raised by Anderson and Belnap within the framework of relevance logic, this question is equivalent to the question of the decidability of type inhabitation in simply-typed combinatory logic with the partial basis BB ′ IW. We solve the equivalent problem of type inhabitation for the restriction of simply-typed lambda-calculus to hereditarily right-maximal terms.

The partial bases built upon the atomic combinators B, B ′ , C, I, K, W of combinatory logic are well-known for being closely connected with propositional logic. The types of their combinators form the axioms of implicational logic systems that have been studied for well over 70 years [START_REF] Trigg | Combinatory abstraction using B, B ′ and friends[END_REF]. The partial basis BB ′ IW corresponds, via the types of its combinators, to the system T → of Ticket Entailment introduced and motivated in [START_REF] Anderson | Entailment: The Logic of Relevance and Necessity[END_REF][START_REF] Anderson | Entailment: The Logic of Relevance and Necessity[END_REF]. The system T → consists of modus ponens and four axiom schemes that range over the following types for each atomic combinator:

-B : (χ → ψ) → ((φ → χ) → (φ → ψ)) -B ′ : (φ → χ) → ((χ → ψ) → (φ → ψ)) -I : φ → φ -W : (φ → (φ → χ)) → (φ → χ)
The type inhabitation problem for BB ′ IW is the problem of deciding for a given type whether there exists within this basis a combinator of this type. This problem is equivalent to the problem of deciding whether a given formula can be derived in T → .

Surprisingly, the question of the decidability of T → has remained unsolved since it was raised in [START_REF] Anderson | Entailment: The Logic of Relevance and Necessity[END_REF], although the problem has been thoroughly explored within the framework of relevance logic with proofs of decidability and undecidability for several related systems. For instance the system R → of Relevant Implication (which corresponds to the basis BCIW) and the system E → of Entailment [START_REF] Anderson | Entailment: The Logic of Relevance and Necessity[END_REF] are both decidable [START_REF] Kripke | The problem of entailment[END_REF] whereas the extensions R, E, T of R → , E → , T → to a larger set of connectives (→, ∧, ∨) are undecidable [START_REF] Urquhart | The undecidability of entailment and relevant implication[END_REF].

In 2004, a partial decidability result for the type inhabitation problem was proposed in [START_REF] Broda | The decidability of a fragment of BB ′ IW -logic[END_REF]) for a restricted class of formulas -the class of 1-unary formulas in which every maximal negative subformula is of arity at most 1. Broda, Dams, Finger and Silva e Silva's approach is based on a translation of the problem into a type inhabitation problem for the hereditary right-maximal (HRM) terms of lambda calculus [START_REF] Trigg | Combinatory abstraction using B, B ′ and friends[END_REF][START_REF] Bunder | Lambda Terms Definable as Combinators[END_REF][START_REF] Broda | The decidability of a fragment of BB ′ IW -logic[END_REF]). The closed HRM-terms form the closure under βreduction of all translations of BB ′ IW-terms, accordingly the type inhabitation problem within the basis BB ′ IW is equivalent to the type inhabitation problem for HRM-terms.

We use in this paper the same approach as Broda, Dams, Finger and Silva e Silva's. We prove that the type inhabitation problem for HRM-terms is decidable, and conclude that the logic T → is decidable † .

Summary

In Section 1, we recall the definition of hereditarily right-maximal terms and the equivalence between the decidability of type inhabitation for BB ′ IW and the decidability of type inhabitation for HRM-terms. The principle of our proof is depicted on Figure 1.

In Sections 2 and 3 we provide for each formula φ a partial characterisation of the inhabitants of φ in normal form and of minimal size. We show that all those inhabitants belong to two larger sets of terms, the set of compact and locally compact inhabitants of φ.

In Section 4 we show how to associate, with each locally compact inhabitant M of a formula φ, a labelled tree with the same tree structure as M . We call this tree the shadow of M . We define for shadows the analogue of compactness for terms and prove that the shadow of a compact term is itself compact.

Finally, in Section 5, we prove that for each formula φ the set of all compact shadows of inhabitants of φ is a finite set (hence the set of compact inhabitants of φ is also a finite set), and that this set is effectively computable from φ. The proof appeals to Higman Theorem and Kruskal Theorem -more precisely, to Melliès' Axiomatic Kruskal Theorem. The decidability of the type inhabitation problem for HRM-terms and the decidability of T → follow from this last key result: given an arbitrary formula φ, this formula is inhabited if and only if there exists a compact shadow with the same tree structure as an inhabitant of φ, and our key lemma proves that the existence of such a shadow is decidable.

Preliminaries

The first section of this paper assumes some familiarity with pure and simply-typed lambda-calculus and with the usual notions of α-conversion, β-reduction and β-normal form (Barendregt 1984;[START_REF] Krivine | Lambda-calculus, types and models[END_REF]. The last three notions are not essential to our discussion, as we later focus exclusively on a particular set of simply-typed terms in β-normal form. We shall briefly recall the definitions and results used in Section 1. The set of terms of pure lambda-calculus (λ-terms) is inductively defined by:

every variable x is a λ-term, -if M is a λ-term and x is a variable, then (λxM ) is a λ-term, -if M, N are λ-terms, then (M N ) is a λ-term.

Terms yielded by the second and third rules are called abstractions and applications respectively. The parentheses surrounding applications and abstractions are often omitted if unambiguous. We let λx 1 . . . x n .M N 1 . . . N p abbreviate (λx 1 (. . . (λx n (((M N 1 ) . . .)N p )) . . .)). For instance, λxy.x(xy)z stands for (λx(λy((x(xy))z))).

The bound variables of M are all x such that λx occurs in M . A variable x is free in M if and only:

-M = x, or, -M = λy.N , y = x and x is free in N , or, -M = N P and x is free in N or free in P .

A closed term is a term with no free variables. The raw substitution of N for x in M , written M x ← N , is the term obtained by substituting N for every free occurrence of x in M (every occurrence of x that is not in the scope of a λx). We require this substitution to avoid variable capture (for all y free in N , no free occurrence of x in M is in the scope of a λy):

if y = x, then y x ← N is equal to N , otherwise it is equal to y, -(λx.M ) x ← N = λx.M , -if y = x and y is free in N , then (λy.M ) x ← N is undefined, -if y = x, y is not free in N and M x ← N = M ′ , then (λy.M )

x ← N = λy.M ′ , -if M 1 x ← N = M ′ 1 and M 2 x ← N = M ′ 2 , then (M 1 M 2 ) x ← N = (M ′ 1 M ′ 2
). The α-conversion is defined as the least binary relation ≡ α such that:

-x ≡ α x, -if M ≡ α M ′ , y is not free in M ′ and M ′ x ← y = M ′′ , then (λx.M ) ≡ α (λy.M ′′ ) -if M 1 ≡ α M ′ 1 and M 2 ≡ α M ′ 2 , then (M 1 M 2 ) ≡ α (M ′ 1 M ′ 2 )
. For instance λx.y ≡ α λz.y ≡ α λy.y. It is a common practice to consider λ-terms up to α-conversion, however we will not follow this practice in our exposition.

The β-reduction is the least binary relation β satisfying:

if M ≡ α (λx.N )P and N x ← P = N ′ , then M βN ′ .

-

if M βM ′ , then (λx.M )β(λx.M ′ ), (M N )β(M ′ N ) and (N M )β(N M ′ ).
In the first rule, x is not necessarily free in N , so we may have N = N ′ -in particular, free variables may disappear in the process of reduction. We write β * for the reflexive and transitive closure of β.

A term M is in β-normal form -or β-normal -if there is no M ′ such that M βM ′ . A term M is normalising if there is a normal N -called normal form of M -such that M β * N . It is strongly normalising if there is no infinite sequence M = M 0 βM 1 βM 2 . . .
It is well-known that β-conversion enjoys the Church-Rosser property: if M β * N and M β * N ′ , then there exist two α-convertible P, P ′ such that N β * P and N ′ β * P ′ . As a consequence, if a term is normalising then its normal form is unique up to α-conversion.

The judgment "assuming x 1 , . . . , x n are of types ψ 1 , . . . ψ n , the term M is of type φ", written {x 1 : ψ 1 , . . . , x n : ψ n } ⊢ M : φ, where ψ 1 , . . . , ψ n , φ are formulas of propositional calculus and x 1 , . . . , x n are distinct variables, is defined by:

-Γ ⊢ x : ψ for each x : ψ ∈ Γ, -if Γ ∪ {x : φ} ⊢ M : ψ, then Γ ⊢ λx.M : φ → ψ. -if Γ ⊢ M : φ → ψ and Γ ⊢ N : φ, then Γ ⊢ (M N ) : ψ
The simply-typable terms are all M for which there exist Γ, φ such that Γ ⊢ M : φ. Note that Γ contains all variables free in M . The following properties are well-known:

1 (Strong normalisation) If Γ ⊢ M : φ, then M is strongly normalising. 2 (Subject reduction) If Γ ⊢ M : φ and M βN , then Γ ⊢ N : φ. 1. From BB ′ IW to simply-typed lambda-calculus
The aim of this first section is to provide a precise characterisation of simply-typable terms that are typable with inhabited types in BB ′ IW, so as to transform the problem of type inhabitation in BB ′ IW into a type inhabitation problem in lambda-calculus. The types of atomic combinators in BB ′ IW are also types for their respective counterparts λf gx.f (gx), λf gx.g(f x), λx.x, λhx.hxx in lambda-calculus, hence to each inhabited type φ in BB ′ IW corresponds at least one closed λ-term of type φ. Moreover, subject reduction and strong normalisation (see above) also ensure the existence of a closed normal λ-term of type φ. What we lack is a criterion to distinguish amongst all typed normal forms the ones that are reducts of translations of combinators within BB ′ IW.

The material and the results of this section are not new [START_REF] Bunder | Lambda Terms Definable as Combinators[END_REF][START_REF] Broda | The decidability of a fragment of BB ′ IW -logic[END_REF]). The reader may as well skip the contents of Sections 1.3 and 1.4 entirely, accept Lemma 1.10 then go on with the study of stable parts and blueprints in Section 2.

The definition of hereditarily right-maximal terms is an adaptation of the definition given in [START_REF] Bunder | Lambda Terms Definable as Combinators[END_REF]. The proof of Lemma 1.6 (subject reduction for HRM-terms) is similar to the proof of Property 2.4, p.375 in [START_REF] Broda | The decidability of a fragment of BB ′ IW -logic[END_REF]. The right-to-left implication of Lemma 1.10 can be deduced from Property 2.20, p.390 in [START_REF] Broda | The decidability of a fragment of BB ′ IW -logic[END_REF], although our proof method seems to be simpler.

Lambda-calculus

Let X be a countably infinite set of variables x, y, z . . . together with a one-to-one function O from X to N . For all x, y in X , we write x < y when O(x) < O(y). Throughout the sequel, by term we always mean a term of lambda-calculus built over those variables. For each term M , we write Free(M ) for the strictly increasing sequence of all free variables of M .

Terms are not identified modulo α-conversion -apart from Section 1, all considered terms will be in normal form, and the Greek letters α, β will be even used with new meaning at the beginning of Section 2. We adopt however the usual convention according to which two distinct λ's may not bound the same variable in a term, and no variable can be simultaneously free and bound in the same term.

Hereditarily right-maximal terms

Definition 1.1. The set of hereditarily right-maximal (HRM) terms is inductively defined as follows:

1 Each variable x is HRM. 2 If M is HRM and x is the greatest free variable of M then λx.M is HRM. 3 If M, N are HRM, and for each free variable x of M there exists a free variable y of N such that x ≤ y, then (M N ) is HRM.

The second rule ensures that all HRM-terms are λ I -terms, that is, terms in which every subterm λx.M is such that x is free in M . As a consequence the set of free variables of an HRM-term is preserved under β-reduction. As we shall see below (Lemma 1.6), rightmaximality can also be preserved at the cost of appropriate bound variable renamings.

In the third rule, if N is closed then so is M . When M and N are non-closed terms, the greatest free variable of M is less than or equal to the greatest free variable of N . For instance, if f < g < x and h < x, then λf gx.f (gx), λf gx.g(f x), λx.x, λhx.hxx are HRM, whereas λyz.zy is not, no matter if y < z or y > z.

Definition 1.2. Let Ω be a function mapping each variable to a formula, in such a way that Ω -1 (φ) is an infinite set for each φ. We extend this function to the set of all strictly increasing finite sequences of variables, letting Ω(x 1 , . . . , x n ) = (Ω(x 1 ), . . . , Ω(x n )).

Definition 1.3. The judgment M : φ, in words "M is of type φ w.r.t Ω", is defined by:

-if Ω(x) = φ, then x : φ, -if x : χ, M : ψ and λx.M is HRM, then λx.M : χ → ψ, -if M : χ → ψ, N : χ and (M N ) is HRM, then (M N ) : ψ.
The function Ω will remain fixed throughout our exposition. Accordingly the type of a term M w.r.t Ω will be called the type of M , without any further reference to the choice of Ω. Note that every typed term is HRM.

Definition 1.4. We write Λ NF for the set of all typed terms in β-normal form. We call Λ NF -inhabitant of φ every closed term M ∈ Λ NF of type φ.

The next lemma is the well-known subformula property of simply-typed lambda-calculus: Lemma 1.5. (Subformula Property) Let M be a Λ NF -inhabitant of φ. The types of the subterms of M are subformulas of φ.

Subject reduction of hereditarily right-maximal terms

Lemma 1.6. Suppose there exists a closed M : φ. Then φ is Λ NF -inhabited.

Proof.

(1) We leave to the reader the proof of the fact that for every variable y and for every N : φ, there exists N ′ ≡ α N such that N ′ : φ and every bound variable of N ′ is strictly greater than y.

(2) We prove the following proposition by induction on P . Let P, Q be typed HRMterms. Suppose:

-x and Q are of the same type, -if Q is closed and x ∈ Free(P ), then x = min(Free(P )) -if Q is not closed, then for all z ∈ Free(P ): if z < x then z ≤ max(Free(Q)), if x < z then max(Free(Q)) < z. -if Q is not closed, then max(Free(Q))
< z for all bound variables z of P .

Then R = P x ← Q is defined, HRM and of the same type as P . The proposition is clear if P is a variable.

Suppose P = λz.P ′ . Then Free(P ′ ) = Free(P ) • (z). By induction hypothesis R ′ = P ′ x ← Q is defined, HRM and of the same type as P ′ . The variable z is still the greatest free variable of R ′ and z is not free in Q, hence R = λz.R ′ .

Suppose P = (P 1 P 2 ). By induction hypothesis R i = P i x ← Q is defined, HRM and of the same type as P i for each i ∈ {1, 2}. It remains to check that R = (R 1 R 2 ) is HRM. Assume x is free in P and P 1 is not closed.

Suppose max(Free(P 1 )) > x. Then max(Free(P 1 )) = max(Free(R 1 )) ≤ max(Free(P 2 )) = max(Free(R 2 )).

Suppose max(Free(P 1 )) < x. The term Q cannot be closed, and max(Free(P 1 )) = max(Free(R 1 )) ≤ max(Free(Q)). We have either max(Free(P 2 )) = x and max(Free(R 2 )) = max(Free(Q)), or max(Free(P 2 )) > x and max(Free(P 2 )) = max(Free(R 2 )).

Otherwise max(Free(P 1 )) = x. Suppose max(Free(P 2 )) > x. Then max(Free(P 2 )) = max(Free(R 2 )). If Q is closed, then Free(P 1 ) = (x) and R 1 is closed. Otherwise we have max(Free(R 1 )) = max(Free(Q)) ≤ max(Free(P 2 )). The remaining case is max(Free(P 2 )) = x. If Q is closed then Free(P 1 ) = Free(P 2 ) = (x) and R 1 , R 2 are closed. Otherwise max(Free(R 1 )) = max(Free(R 2 ) = max(Free(Q)).

(3) Assume N : φ and N is not in normal form. We prove by induction on N the existence of N ′ : φ such that N βN ′ . If N = λx.P , or if N = (N 1 N 2 ) with N 1 or N 2 not in normal form, then the existence of N ′ follows from the induction hypothesis and the fact that β-reduction preserves the set of free variables of an HRM-term. Otherwise N = (λx.P )Q where for each free variable z of λx.P , we have z < x and there exists a free variable y of Q such that z < y. By (1) there exists P ′ ≡ α P such that P ′ : φ and no bound variable of P ′ is less than or equal to a free variable of Q. The variable x is the greatest free variable of P ′ . By (2), the term N ′ = P ′ x ← Q is well-defined, HRM and of the type φ. Moreover N βN ′ .

(4) We now prove the lemma. The term M is a simply-typable HRM-term. The strong normalisation property implies the existence of a normal form N of M . The term N is still a closed term. By (1), there exists 1.4. Equivalence between inhabitation in BB ′ IW and Λ NF -inhabitation

N ′ ≡ α N such that N ′ : φ, that is, φ is Λ NF -inhabited,
In the next three lemmas by φ 1 . . . φ n → ψ we mean the formula (φ 1 → (. . . (φ n → ψ) . . .)) if n > 0, and otherwise the formula ψ. We write ⊢ BB'IW φ for the judgment "there exists within the basis BB ′ IW a combinator of type φ".

Lemma 1.7. If ⊢ BB'IW φ, then φ is Λ NF -inhabited.
Proof. If f < g < x and h < x, then λx.x, λf gx.f (gx), λf gx.g(f x) and λhx.hxx are HRM. For each type φ of an atomic combinator, the variables f, g, h, x can be chosen so that one of those terms is of type φ. The set of all formulas φ for which there exists a closed M of type φ is closed under modus ponens. By Lemma 1.6, every such formula is Λ NF -inhabited.

Lemma 1.8. If ⊢ BB'IW χ → ψ, then ⊢ BB'IW (φ 1 . . . φ n → χ) → (φ 1 . . . φ n → ψ) for all φ 1 , . . . , φ n .

Proof. By induction on n, using left-applications of B.

Lemma 1.9. Suppose (i 1 , . . . , i n ), (j 1 , . . . , j m ), (k 1 , . . . , k p ) are strictly increasing sequences of integers, {k 1 , . . . , k p } = {i 1 , . . . , i n , j 1 , . . . , j m }, n = 0 or (n > 0, m > 0,

i n ≤ j m ). If 1 ⊢ BB'IW ω i1 . . . ω in → (χ → ψ), 2 ⊢ BB'IW ω j1 . . . ω jm → χ, then ⊢ BB'IW ω k1 . . . ω kp → ψ.
Proof. By induction on n+m. The proposition is true if n = m = 0. Assume n+m > 0. Then m > 0.

Suppose n = 0. Then (j i , . . . , j m ) = (k 1 , . . . , k p ). We have:

(i) ⊢ BB'IW (χ → ψ) → ((ω jm → χ) → (ω jm → ψ)) (ii) ⊢ BB'IW (ω jm → χ) → (ω jm → ψ)
where: (i) is a type for B; (ii) follows from (i), (1) and modus ponens. If m = 1 then ⊢ BB'IW ω j1 → ψ follows from (ii), (2) and modus ponens. Otherwise ⊢ BB'IW ω j1 . . . ω jm → ψ follows from (ii), (2) and the induction hypothesis.

We now assume n > 0. Suppose m > 1 and

i n ≤ j m-1 . Then (iii) ⊢ BB'IW (χ → ψ) → ((ω jm → χ) → (ω jm → ψ)) (iv) ⊢ BB'IW (ω i1 . . . ω in → (χ → ψ)) → (ω i1 . . . ω in → ((ω jm → χ) → (ω jm → ψ))) (v) ⊢ BB'IW ω i1 . . . ω in → ((ω jm → χ) → (ω jm → ψ))
where: (iii) is a type for B; (iv) follows from (iii) and Lemma 1.8; (v) follows from (iv), (1) and modus ponens. We have k p = j m and {k 1 , . . . , k p-1 } = {i 1 , . . . , i n , j 1 , . . . , j m-1 }. Since i n ≤ j m-1 , we have ⊢ BB'IW ω k1 . . . ω kp-1 → (ω jm → ψ) by (v), (2) and the induction hypothesis.

Suppose m = 1 or (m > 1 and i n > j m-1 ). Then (vi)

⊢ BB'IW (ω jm → χ) → ((χ → ψ) → (ω jm → ψ)) (vii) ⊢ BB'IW (ω j1 . . . ω jm → χ) → (ω j1 . . . ω jm-1 → ((χ → ψ) → (ω jm → ψ))) (viii) ⊢ BB'IW ω j1 . . . ω jm-1 → ((χ → ψ) → (ω jm → ψ)) (ix)
⊢ BB'IW ω n1 . . . ω nq → (ω jm → ψ) where: (vi) is a type for B ′ ; (vii) follows from (vi) and Lemma 1.8; (viii) follows from (vii), (2) and modus ponens; {n 1 , . . . , n q } = {j 1 , . . . , j m-1 , i 1 , . . . , i n }; (ix) follows from (viii), (1) and the induction hypothesis. If j m > i n , then (n 1 , . . . , n q , j m ) = (k 1 , . . . , k p ). Otherwise j m = i n , n q = i n , (n 1 , . . . n q ) = (k 1 , . . . , k p ) and (x) Lemma 1.10. For every formula φ, we have ⊢ BB'IW φ if and only if φ is Λ NF -inhabited.

⊢ BB'IW ω k1 . . . ω kp-1 → (ω in → (ω in → ψ)) (xi) ⊢ BB'IW (ω in → (ω in → ψ)) → (ω in → ψ) (xii) ⊢ BB'IW (ω k1 . . . ω kp-1 → (ω in → (ω in → ψ))) → (ω k1 . . . ω kp-1 → (ω in → ψ)) (xiii) ⊢ BB'IW ω k1 . . . ω kp-1 → (ω in → ψ) where: (x) is (ix); (xi)
Proof. The left to right implication is Lemma 1.7. Using Lemma 1.9 when M is an application, an immediate induction on M shows that if M : ψ, Free(M ) = (x 1 , . . . , x n ) and x 1 : χ 1 , . . . , x n : χ n , then ⊢ BB'IW χ 1 . . . χ n → ψ

Stable parts and blueprints

The last lemma showed that the decidability of type inhabitation for BB ′ IW is equivalent to the decidability of Λ NF -inhabitation. The sequel is devoted to the elaboration of a decision algorithm for the latter problem.

The problem we shall examine throughout Sections 2 and 3 is the following: if an inhabitant is not of minimal size, is there any way to transform it (with the help of grafts and/or another compression of some sort) into a smaller inhabitant of the same type? This question is not easy because we are dealing with a lambda-calculus restricted with strong structural constraints (righ-maximality). There are however simple situations in which an inhabitant is obviously not of minimal size.

Consider a Λ NF -inhabitant M and two subterms N, P of M such that P is a strict subterm of N . Suppose:

-N, P are applications of the same type or abstractions of the same type.

-Free(N ) = X = (x 1 , . . . , x n ), -Free(P ) = Y = (y 1 0 , . . . , y 1 p1 , . . . , y n 0 , . . . , y n pn ) -Ω(X) = (χ 1 , . . . , χ n ), -Ω(Y ) = (χ 1 0 , . . . , χ 1 p1 , . . . , χ n 0 , . . . , χ n pn ), -χ i j = χ i for each i, j. Then M is not of minimal size. Indeed we can rename the free variables of P (letting ρ(y i j ) = x i ) so as to obtain a term P ′ of the same size as P , of the same type and the same free variables as N . The subterm N of M can be replaced with P ′ in M . The resulting term is a Λ NF -inhabitant of the same type but of strictly smaller size.

This simple property is far from being enough to characterise the minimal inhabitants of a formula: there are indeed formulas with inhabitants of abitrary size in which this situation never occurs. What we need is a more flexible way to reduce the size of non-minimal inhabitants. In particular, we need a better understanding of our available freedom of action if we are to rename the free variables of a term -possibly occurrence by occurrence -and if we want to ensure that right-maximality is preserved. This section is devoted to the proof of two key lemmas that delimit this freedom.

-In Sections 2.1, 2.2 and 2.2 we show how to build from any term M ∈ Λ NF a partial tree labelled with formulas. This partial tree is called the blueprint of M . This blueprint can be seen as a synthesized version of M that contains all and only the information required to determine whether a (non-uniform) renaming of the free variables of M will preserve hereditarily right-maximality. -In Sections 2.4 and 2.5 we introduce a rewriting relation on blueprints that allows one to "extract" sequences of formulas from a blueprint. -In section 2.6 we prove our two key lemmas. Lemma 2.15 clarifies the link between the blueprints of M and λx.M (provided both are in Λ NF ). This lemma proves in particular that the sequence of the types of the free variables of M (that is, Ω(Free(M ))) can always be extracted from its blueprint. Lemma 2.16 shows that for every sequence of formulas φ that can be extracted from the blueprint of M , there exists a (nonuniform) renaming of the free variables of M that will produce a term N of the same type and with the same blueprint as M , and such that Ω(Free(N )) = φ.

As a continuation of our first example, let us examine the consequences of this last result.

Consider again a Λ NF -inhabitant M and two subterms N, P of M such that P is a strict subterm of N and N, P are applications of the same type or abstractions of the same type. Suppose:

the sequence Ω(Free(N )) can be extracted from the blueprint of P .

This situation is a generalization of the preceding one (in our first example Ω(X) could also be extracted from the blueprint of P , see Definition 2.10). The term M is still not of minimal size. Indeed, we may use the second key lemma to prove the existence of (non-uniform) renaming of the free variables of P that will produce a term P ′ of the same type as P such that Free(P ′ ) = Free(N ). The term N can be replaced with P ′ in M .

Partial trees and trees

Definition 2.1. Let (A , ≤) be the set of all finite sequences over the set N + of natural numbers, ordered by prefix ordering. Elements of A are called addresses. We call partial tree every function π whose domain is a set of addresses. For each partial tree π and for each address a, we let π |a denote the partial tree

c → π(a•c) of domain {c | a•c ∈ dom(π)}.
Definition 2.2. For all partial trees π, π ′ and for every address a, we let π[a ← π ′ ] denote the partial tree π ′′ such that

π ′′ |a = π ′ and π ′′ (b) = π(b) for all b ∈ dom(π) such that a ≤ b. Definition 2.3. A tree domain is a set A ⊆ A such that for all a ∈ A: every prefix of a is in A; for every integer i > 0, if a • (i) ∈ A, then a • (j) ∈ A for each j ∈ {1, . . . , i -1}.
A tree domain A is finitely branching if and only if for each a ∈ A, there exists an i > 0 such that a • (i) is undefined. We call tree every function whose domain is a tree domain.

In the sequel terms will be freely identified with trees. We identify: x with the tree mapping ε to x; λx.M with the tree τ mapping ε to λx and such that τ |(1) is the tree of M ; (M 1 M 2 ) with the tree τ mapping ε to @ and such that τ |(i) is the tree of M i for each i ∈ {1, 2}.

Blueprints

Definition 2.4. Let S be the signature consisting of all formulas and all symbols of the form @ φ where φ is a formula. Each formula is considered as a symbol of null arity. Each @ φ is of arity 2.

We call blueprint every finite partial tree α : A → S satisfying the following condition: for each a ∈ A, if α(a) = @ φ , then α |a•(1) and α |a•(2) are of non-empty domains. A rooted blueprint is a blueprint α such that ε ∈ dom(α).

For each S ⊆ S, we call S-blueprint every blueprint whose image is a subset of S. We write B(S) for the set of all S-blueprints, and B ε (S) for the set of all rooted S-blueprints.

Definition 2.5. For every blueprint α and every address a, the relative depth of a in α is the number of b ∈ dom(α) such that b < a. The relative depth of α is defined as 0 if α is of empty domain, the maximal relative depth of an address in α otherwise.

In the sequel the following notations will be used to denote blueprints (see Figure 2):

-∅ B denotes the blueprint of empty domain.

we abbreviate ε → φ as φ.

-@ φ (α 1 , α 2 ) denotes the (rooted) blueprint α such that α(ε) = φ, α |(1) = α 1 , α |(2) = α 1 . -for every sequence a = (a 1 , . . . , a k ) of pairwise incomparable addresses, * a (α 1 , . . . , α k ) denotes the blueprint α of minimal domain such that α |ai = α i for each i ∈ [1, . . . , k]. -we let * (α 1 , . . . , α k ) denote the blueprint * a (α 1 , . . . , α k ) such that a = ((1), . . . , (k)).
For each blueprint α, the choice of a, α 1 , . . . , α k such that α = * a (α 1 , . . . , α k ) is obviously not unique. The sequence (α 1 , . . . , α k ) may contain an arbitrary number of empty blueprints, hence the sequence a may be of arbitrary length. Also, α can be roooted (if Fig. 2. Construction of blueprints, with the notations of Section 2.2. In the upper diagram, the blueprints α and β must be non-empty. Although α1, . . . , α k are displayed from left to right, the sequence (a1, . . . , a k ) needs not to be lexicographically ordered.

k = 1, a 1 = ε and α 1 is rooted) or empty (if k = 0 or α 1 = . . . = α k = ∅ B )
. Those ambiguities will not be difficult to deal with, but they will require a few precautions in our proofs and definitions by induction on blueprints.

Blueprint of a term

Definition 2.6. For all M ∈ Λ NF , the stable part of M is the set of all a ∈ dom(M ) such that Free(M |a ) ⊆ Free(M ) and M |a is a variable or an application.

It is easy to check that our conventions (no variable is simultaneously free and bound in a term) ensure that the stable part of a term does not depend on the choice of variable names. Since M is in normal form, M is of empty stable part if and only if it is closed. Definition 2.7. For all M ∈ Λ NF , we call blueprint of M the function α mapping each a in the stable part of M to:

-ψ if M |a is a variable of type ψ, -@ ψ if M |a is an application of type ψ.
We let M α denote the judgment "M is of blueprint α" (Figure 3).

If M = (M 1 M 2 ) ∈ Λ NF , M : φ, M 1 α 1 , M 2 α 2 , then each α i is of non-empty domain and (M 1 M 2 ) @ φ (α 1 , α 2 ) -
in other words the so-called blueprint of M is indeed a blueprint, provided so are the blueprints of M 1 , M 2 . When M = λx.M 1 the blueprint of M is of the form * (α) -the relation between α and the blueprint of M 1 in that case will be clarified by Lemma 2.15.

Lemma 2.8. For all M ∈ Λ NF and forall a • b ∈ dom(M ): Proof. The first proposition is a consequence of our bound variable convention (see Section

1 If Free(M |a•b ) ⊆ Free(M ) then Free(M |a•b ) ⊆ Free(M |a ). 2 If M |a α and M |a•b β, then α |b = β.
1.1): if Free(M ) = X, Free(M |a ) = X ′ ∪ Y where X ′ ⊆ X and X, Y are disjoint, then every element of Free(M |a•b ) in X is also an element of X ′ . Thus if a • b is in the stable part of M , then b is also in the stable part of M |a .
The second proposition is equivalent to the first.

Extraction of the formulas of a blueprint

Definition 2.9. The judgment "β is the blueprint obtained by extracting the formula φ at the address a in the blueprint α", written α ⊲ a φ β, is inductively defined by:

1 φ ⊲ ε φ ∅ B , 2 if α ⊲ a φ β, then @ ψ (γ, α) ⊲ (2)•a φ * (γ, β) 3 if α ⊲ a φ β, then * (b,c1,...,c k ) (α, γ 1 , . . . , γ k ) ⊲ b•a φ * (b,c1,...,c k ) (β, γ 1 , . . . , γ n ).
In (2) we assume of course that α and γ are non-empty. In (3) we assume b = ε in order to avoid circularity.

Fig. 5. Full reductions of @ ψ (χ → ψ, @χ(φ → χ, φ)) to ∅ B .
For instance (Figure 5):

-@ ψ (χ → ψ, @ χ (φ → χ, φ)) ⊲ (2,2) φ * (χ → ψ, * (φ → χ, ∅ B )) ⊲ (2,1) φ→χ * (χ → ψ, * (∅ B , ∅ B )) ⊲ (1) χ→ψ * (∅ B , * (∅ B , ∅ B )) = ∅ B -@ ψ (χ → ψ, @ χ (φ → χ, φ)) ⊲ (2,2) φ * (χ → ψ, * (φ → χ, ∅ B )) ⊲ (1) χ→ψ * (∅ B , * (φ → χ, ∅ B )) ⊲ (2,1) φ→χ * (∅ B , * (∅ B , ∅ B )) = ∅ B
When α ⊲ a φ β, the blueprint β can be seen as α in which the formula φ at a is erased together with all @'s in the path to a. At each @ this path must follow the right branch of @. The constraints on the construction of blueprints imply the existence of at least one such path in every non-empty blueprint, even if it is not the blueprint of a term.

Sets of extractible sequences

Definition 2.10. For each formula φ, let ⊲ φ be the relation defined by: α ⊲ φ β if and only if there exists a such that α ⊲ a φ β. We write ⊲ + φ for the transitive closure of ⊲ φ . For each α, we write F (α) for the set of all sequences (φ 1 , . . . , φ n ) such that α ⊲ + φn . . .

⊲ + φ1 ∅ B .
The set F (α) is what we called "set of extractible sequences of α" in the introduction of Section 2. Note that F (∅ B ) = {ε}. If α = ∅ B , then all elements of F (α) are nonempty sequences. Note also that each ⊲-reduction strictly decreases the cardinality of the domain of a blueprint, therefore F (α) is a finite set for all α. We now introduce the notion of shuffle which will allow us to characterise F (α) depending on the structure of α.

Fig. 6. Shuffling of two sequences. The chunks of F and G need not to be of the same size -some of them can be empty. Every contraction of the resulting sequence belongs to ⊛(F, G). Each contraction belongs also to ⊚(F, G) when F, G are non-empty and the last chunk G p of G is non-empty.

Definition 2.11. A contraction of a sequence F is either the sequence F or a sequence

G • (f ) • H where G • (f ) • (f ) • H is a contraction of F .
Definition 2.12. For all finite sequences F 1 , . . . , F n we call shuffle of (F 1 , . . . , F n ) every sequence

F 1 1 • . . . • F 1 n • . . . • F p 1 • . . . • F p n such that F 1 i • . . . • F p i = F i for each i.
For each tuple of sets of finite sequences (F 1 , . . . , F n ) we write ⊛(F 1 , . . . , F n ) for the closure under contraction of the set of shuffles of elements of

F 1 × . . . × F n . Definition 2.13. Given two non-empty finite sequences F 1 , F 2 , we call right-shuffle of (F 1 , F 2 ) every sequence F 1 1 • F 1 2 • . . . • F p 1 • F p 2 such that F 1 i • . . . F p i = F i for each i and F p 2 = ε.
For each pair of sets of non-empty finite sequences (F 1 , F 2 ) we write ⊚(F 1 , F 2 ) for the closure under contraction of the set of right-shuffles of elements

F 1 × F 2 .
The principle of (right-)shuffling is depicted on Figure 6. The following properties follow from our definitions and will be used without reference:

1 If α = ∅ B , then F (α) = {ε}. 2 If α = φ, then F (α) = {(φ)}. 3 If α = * a (α 1 , . . . , α k ), then F (α) = ⊛(F (α 1 ), . . . , F (α k )). 4 If α = @ φ (α 1 , α 2 ), then F (α) = ⊚(F (α 1 ), F (α 2 )).

Abstraction vs. extraction

Lemma 2.14. Suppose {a 1 , . . . , a p } = {b 1 , . . . , b p }, and:

-α ⊲ a1 χ . . . ⊲ ap χ β, -α ⊲ b1 χ . . . ⊲ bp χ β ′ . Then β = β ′ .
Proof. By an easy induction on α.

Recall that for every strictly increasing sequence of variables X = (x 1 , . . . , x n ), we write Ω(X) for the sequence of the types of x 1 , . . . , x n . We now clarify the link between the blueprint α of a term M and the one of λx.M .

The next lemma shows in particular that if M, λx.M ∈ Λ NF , then M and λx.M Lemma 2.15. Suppose M ∈ Λ NF is of blueprint α, with Free(M ) = (x 1 , . . . , x n ) and Ω(x 1 , . . . , x n ) = (χ 1 , . . . , χ n ). For each i ∈ [0, . . . , n]:

let α i be the restriction of α to dom(α) ∩ {a | Free(M |a ) ⊆ {x 1 , . . . , x i }}.

let β i be the blueprint of λx i+1 . . . x n .M , Then:

1 For each i ∈ [0, . . . , n] we have dom( We shall prove by induction on M that for all pairs (X, X ′ ) such that Free(M ) = X •X ′ , we have µ M (X, α) = ρ N (X ′ , α) -in particular for all i > 0 we have

β i ) = {1 n-1 • a | a ∈ dom(α i )} and β i|1n-i = α i . 2 For each i ∈ ]0, . . . , n]: (a) there exist a i 0 , . . . , a i pi such that {a i 0 , . . . , a i pi } = {a | M |a = x i } and α i ⊲ a i 0 χi . . . ⊲ a i p i χi α i-1 , (b) if {b 0 , . . . , b pi } = {a | M |a = x i } and α i ⊲ b0 χi . . . ⊲ bp i χi α ′ then α ′ = α i-1 . 3 We have (χ 1 , . . . , χ n ) ∈ F (α).
α i-1 = µ M ((x 1 , . . . , x i-1 ), α) = ρ M ((x i , . . . , x n ), α) = ρ M ((x i ), ρ M ((x i+1 . . . , x n ), α)) = ρ M ((x i ), µ M ((x 1 . . . , x i ), α)) = ρ M ((x i ), α i )
thus (2.a) holds. The case X ′ = ε is immediate, hence we may as well assume that X ′ is a non-empty suffix of Free(M ). The case of M equal to a variable follows immediately from our definitions.

Suppose M = (M 1 M 2 ), M 1 γ 1 and M 2 γ 2 . There exist X 1 , X 2 , X ′ 1 , X ′ 2 such that: X 1 ∪ X 2 = X; X ′ 1 ∪ X ′ 2 = X ′ ; Free(M j ) = X j • X ′ j for each j ∈ {1, 2}. We have α = @ ψ (γ 1 , γ 2 ) where ψ is the type of M , and µ M (X, α) = * (µ M1 (X 1 , γ 1 ), µ M2 (X 2 , γ 2 )). By induction hypothesis µ Mi (X i , γ i ) = ρ Mi (X ′ i , γ i ) for each i. The sequence X ′ is non-empty hence the last elements of X ′ , X ′ 2 are equal. Assume X ′ = X ′′ • (x) and X ′ 2 = X ′′ 2 • (x). If x is not the last element of X ′ 1 then: ρ M (X ′ , α) = ρ M (X ′′ • (x), @ ψ (γ 1 , γ 2 )) = ρ M (X ′ 1 ∪ X ′′ 2 , * (γ 1 , ρ M2 ((x), γ 2 ))) = * (ρ M1 (X ′ 1 , γ 1 ), ρ M2 (X ′′ 2 , ρ M2 ((x), γ 2 ))) = * (ρ M1 (X ′ 1 , γ 1 ), ρ M2 (X ′′ 2 • (x), γ 2 )) = * (ρ M1 (X ′ 1 , γ 1 ), ρ M2 (X ′ 2 , γ 2 )) Otherwise, X ′ 1 = X ′′ 1 • (x) and we have: ρ M (X ′ , α) = ρ M (X ′ , @ ψ (γ 1 , γ 2 )) = ρ M (X ′′ 1 ∪ X ′′ 2 , * (ρ M1 ((x), γ 1 ), ρ M2 ((x), γ 2 ))) = * (ρ M1 (X ′′ 1 , ρ M1 ((x), γ 1 )), ρ M2 (X ′′ 2 , ρ M2 ((x), γ 2 ))) = * (ρ M1 (X ′′ 1 • (x), γ 1 ), ρ M2 (X ′′ 2 • (x), γ 2 )) = * (ρ M1 (X ′ 1 , γ 1 ), ρ M2 (X ′ 2 , γ 2 )) In either case ρ M (X ′ , α) = * (ρ M1 (X ′ 1 , γ 1 ), ρ M2 (X ′ 2 , γ 2 )) = * (µ M1 (X 1 , γ 1 ), µ M2 (X 2 , γ 2 )) = µ M (X, α) Suppose M = λx.M 1 , M 1 γ 1 . By induction hypothesis µ M1 (X, γ 1 ) = ρ M1 (X ′ •(x), γ 1 ) = ρ M1 (X ′ , ρ M1 ((x), γ 1 )) = ρ M1 (X ′ , µ(X •X ′ , γ 1 )) = ρ M1 (X ′ , α |(1) ). Moreover µ M1 (X, γ 1 ) = µ M1 (X, µ M1 (X•X ′ , γ 1 )) = µ M1 (X, α |(1) ). Hence µ M1 (X, α |(1) ) = ρ M1 (X ′ , α |(1) ), therefore µ M1 (X, α) = ρ M1 (X ′ , α).
Thus the full sequence of the types of the free variables of M can be extracted from its blueprint. The next lemma shows that conversely for each sequence χ in F (α), there exists a term N with the same domain, blueprint and of the same type as M , and such that the sequence of types of the free variables of N is equal to χ, see Figure 8.

Vertical compressions and compact terms

The aim of this section is to provide a partial characterisation of minimal inhabitants. Section 3.1 is just a simple remark on the relative depths of their blueprints, and an easy Fig. 9. How the compression of terms is able to follow the compression of blueprints.

consequence of the subformula property (Lemma 1.5): if M is a minimal Λ NF -inhabitant of φ, then for all addresses a in M the blueprint of M |a is of relative depth at most k × p, where:

k is the number of λ in the path from the root to M to a, -p is the number of subformulas of φ.

We call locally compact every Λ NF -inhabitant satisfying this condition. In Section 3.2 we introduce the notion of vertical compression of a blueprint. A (strict) vertical compression of β is obtained by taking any address b in β, then by grafting β |b at any address a < b such that β(a) = β(b). The vertical compressions of β are all blueprints obtained by applying this transformation to β zero of more times. The key property of those compressions is the following (see Figure 9):

-If M is of blueprint β and α is a vertical compression of β, the compression of β into α can be mimicked by a compression of M into an HRM-term, in the following sense. Assuming α = β[a ← β |b ] (the base case), the term Q = M [a ← M |b ] is not in general an HRM-term. However, there exists an HRM-term M ′ with the same domain as Q and of the same type as M . Moreover M ′ and M are applications of the same type or abstractions of the same type.

Let us again consider a Λ NF -inhabitant M and two addresses a, b such that a < b, M |a and M |b are applications of the same type or abstractions of the same type. Suppose:

there exists a vertical compression α ′ of the blueprint of M |b such that the sequence Ω(Free(M |a )) can be extracted from α ′ .

This situation is a generalisation of the last example in the introduction of Section 2 (in which α ′ was equal to the blueprint of M |b , thereby a trivial compression of this blueprint). The term M is not minimal. Indeed, the key property above implies the existence of a term N of blueprint α ′ whose size is not greater than the size of M |b , and such that N, M |b , M |a are applications of the same type or abstractions of the same type. By Lemma 2.16, there exists a term P of the same type and with the same domain as N such that Free(P ) = Free(M |a ). The graft of P at a yields an inhabitant of strictly smaller size.

We will call compact all inhabitants in which the preceding situation does not occur. All inhabitants of minimal size are of course compact. As we shall see in Section 5, we will not need a sharper characterisation of minimal inhabitants. For every formula φ, the set of compact inhabitants of φ is actually a finite set, and our decision method will consist in the exhaustive computation of their domains.

Depths of the blueprints of minimal inhabitants

Definition 3.1. Two terms M, M ′ ∈ Λ NF are of the same kind if and only if they are both variables, or both applications, or both abstractions, and if they are of the same type.

Definition 3.2. For all formulas φ, we write Sub(φ) for the set of all subformulas of φ. Definition 3.3. Let M ∈ Λ NF . Let a be any address in M . Let (a 1 , . . . , a m ) be the strictly increasing sequence of all prefixes of a. Let (λx 1 , . . . , λx k ) be the subsequence of (M (a 1 ), . . . , M (a m )) consisting of all labels of the form λx. We write Λ(M, a) for (x 1 , . . . , x k ). Definition 3.4. Let M be a Λ NF -inhabitant of φ. We say that M is locally compact if for all addresses a in M , the blueprint of M |a is of relative depth at most |Λ(M, a)|×|Sub(φ)|. Hence there exist i, j such that i < j and (X a•bi , φ a•bi ) = (X a•bj , φ a•bj ), that is, M |a•bi and M |a•bj are applications of the same type and with the same free variables (Figure 10). Now, let (1) Suppose

M ′ = M [a • b i ← M |a•bj ]. The term M ′ is a Λ NF -inhabitant of φ of strictly smaller size.

Vertical compression of a blueprint

M = (M 1 M 2 ), M 1 β 1 , M 2 β 2 , a = (i) • a i and b = (i) • b i . By induction hypothesis there exists M ′ i of blueprint α i = β i [a i ← β i |bi ] = β i [a i ← β |b ],
of the same kind as M i and such that dom(M ′ i ) ≤ dom(M i ). Let j = 1 if i = 2, otherwise let j = 2. Let (M ′ j , α j ) = (M j , β j ). Let X = (x 1 , . . . , x n ) be the strictly increasing sequence of all variables free or bound in M ′ 2 . Let Y = (y 1 , . . . , y n ) be a strictly increasing sequence of variables such that Ω(X) = Ω(Y ) and y 1 is greater that or equal to the greatest variable of M ′ 1 . Let M ′′ 2 be the term obtained by replacing each x i by y i in M ′ 2 . We can take

M ′ = (M ′ 1 M ′′ 2 ). (2) Suppose M = λx.M 1 , M 1 β 1 , x : χ, a = (1) • a 1 and b = (1) • b 1 . As a, b ∈ dom(β),
we have also a 1 , b 1 ∈ dom(β 1 ). By induction hypothesis there exists M ′ 1 of the same kind as M 1 , of blueprint α 1 = β 1 [a 1 ← β 1|b 1 ] and such that dom(M ′ 1 ) ≤ dom(M 1 ). By Lemma 2.15.(2.a) there exist γ 1 , c 0 , . . . , c p such that {c 0 , . . . , c p } = {c | M |c = x}, β 1 ⊲ c0 χ . . . ⊲ cp χ γ 1 and β = * (γ 1 ). Since a, b ∈ dom(α), a 1 and c i are incomparable addresses for all i. Hence

α 1 = β 1 [a 1 ← β 1|b 1 ] ⊲ c0 χ . . . ⊲ cp χ γ 1 [a 1 ← β 1|b 1 ] = β[a ← β |b ] |(1) = α |1
. By Lemma 2.16 there exists a term M ′′ 1 of the same type and with the same domain as M ′ 1 such that the greatest variable y free in M ′′ Lemma 3.9. Every Λ NF -inhabitant of minimal size is compact. Every compact Λ NFinhabitant of φ is locally compact.

Proof. Let M by an arbitrary Λ NF -inhabitant of φ. (1) Assume M is not compact. Let a, b be such that a < b, M |a and M |b are of the same kind, M |b α b , α ′ ⇑ α b , Free(M |a ) = X a and Ω(X a ) ∈ F (α ′ ) (see Figure 11). By Lemma 3.7 there exists a term N ∈ Λ NF of blueprint α ′ , of the same kind as M |b and such that |dom(N )| ≤ |dom(M |b )|. By Lemma 2.16 there exists P ∈ Λ NF of blueprint α ′ , of the same kind as N , such that dom(P ) = dom(N ) and Free(P ) = X a . The term M [a ← P ] is then a Λ NF -inhabitant of φ of smaller size.

(2) Suppose M meets the conditions of Lemma 3.5. Let α b ′ be the blueprint of M |b ′ . By Lemma 2.15.(3) we have Ω(Free(M |b )) = Ω(Free(M |b ′ ) ∈ F (α b ′ ). Since the relation ⇑ is reflexive, M is not compact.

Shadows

So far we have isolated two properties shared by all minimal inhabitants (Lemma 3.9). We shall now exploit these properties so as to design a decision method for the inhabitation problem.

In Section 4.1 and 4.2 we show how to associate, with each locally compact inhabitant M of a formula φ, a tree with the same domain as M which we call the shadow of M . At each address a this tree is labelled with a triple of the form (χ a , γ a , φ a ) where φ a is the type of M |a , the sequence χ a is Ω(Free(M |a )), and γ a is a "transversal compression" of the blueprint α a of M |a (Definitions 4.1 and 4.2). Recall that χ a ∈ F (α a ) (by Lemma 2.15.( 3)). The blueprint γ a can be seen as a synthesized version of α a of the same relative depth but of smaller "width", and such that χ a ∈ F (γ a ) ⊆ F (α a ).

Each tree prefix of the shadow of M belongs to a finite set effectively computable from φ and the domain of this prefix. In particular, one can compute all possible values for its labels, regardless of the full knowledge of M -or even without the knowledge of the existence of M . The key property satisfied by this shadow at every address a is:

-for each γ ′ ⇑ γ a , there exists α ′ ⇑ α a such that F (γ ′ ) ⊆ F (α ′ ).
This property is sufficient to detect the non-compactness of M for a pair of addresses (a, b) only from the knowledge of χ a , φ a , γ b , φ b and the arity of the nodes at a and b. Indeed, suppose a < b, φ a = φ b and the nodes at a, b are of the same arity (1, or 2). Now, assume:

-there exists γ ′ ⇑ γ b such that χ a ∈ F (γ ′ ).
Then M |a and M |b are of the same kind and there exists

α ′ ⇑ α b such that χ a = Ω(Free(M |a )) ∈ F (γ ′ ) ⊆ F (α ′ ), therefore M is not compact.
In Section 4.2, what we call a shadow is merely a tree a → (χ a , γ a , φ a ) of a certain shape, no matter if this tree is the shadow of a term or not. This shadow is compact if there is no pair (a, b) as above. Of course, the shadow of a compact term is always compact in this sense.

In Section 5 we will prove that for every formula φ, the set of shadows of compact inhabitants of φ is a finite set effectively computable from φ (hence the same property holds for the set of compact inhabitants of φ), and we will deduce from this key property the decidability of type inhabitation for HRM-terms.

Blueprint equivalence and transversal compression

Definition 4.1. We let ≡ be the least binary relation on blueprints such that:

1 ∅ B ≡ ∅ B , 2 φ ≡ φ, 3 if α 1 ≡ β 1 , α 2 ≡ β 2 , then @ φ (α 1 , α 1 ) ≡ @ φ (β 1 , β 2 ), 4 if |a| = |b| = n and α i ≡ β i for each i ∈ [1, . . . , n], then * a (α 1 , . . . , α n ) ≡ * b (β 1 , . . . , β n ).
In (3), we assume α 1 , α 2 , β 1 , β 2 non-empty. In (4), we assume that the elements of each sequence a, b are pairwise incomparable addresses. As to avoid circularity we assume also a = ε or b = ε, and α i , β i = ∅ B for at least one i.

To some extent this equivalence allows us to consider blueprints regardless of the exact values of addresses. For instance * a (α 1 , . . . , α n ) ≡ * (α 1 , . . . , α n ) ≡ * (α n , . . . , α 1 ), also * ( * (α, β), γ) ≡ * (α, β, γ) ≡ * (α, * (β, γ)), etc. It is easy to check that α ≡ β implies F (α) = F (β) -this property will be used without reference. Definition 4.2. For each m ∈ N , we let m be the least binary relation such that:

1 if γ 1 ≡ . . . ≡ γ m ≡ γ m+1 ≡ ∅ B , then * a (γ 1 , . . . , γ m ) m * a•(b) (γ 1 , . . . , γ m , γ m+1 ), 2 if α = * a (α 1 , . . . , α n ), β = * b (β 1 , . . . , β p ) and α m β, then: (a) @ φ (α, γ) m @ φ (β, γ), (b) @ φ (γ, α) m @ φ (γ, β), (c) * a•(c) (α 1 , . . . , α n , γ) m * b•(c) (β 1 , . . . , β p , γ).
We call m-compression of β every α such that α m β. The width of β is defined as the least m ∈ N for which there is no α such that α m β. empty (hence B(S, d, 0) = {∅ B } for all d); if m ∈ N + , then B ε (S, 0, m) is the finite set of all formulas of S.

Shadow of a term

Definition 4.6. Let φ be a formula. Let S φ be the union of Sub(φ) (Definition 3.2) and the set of all @ ψ such that ψ ∈ Sub(φ). For each integer k, for each formula φ, we let

R(φ, k) = R (S φ , k × |Sub(φ)|, k),
where R is the function introduced in Lemma 4.5.(2).

Definition 4.7. A shadow is a finite tree in which each node is of arity at most 2 and is labelled with a triple of the form (χ, γ, ψ), where χ is a sequence of formulas, γ is a blueprint and ψ is a formula.

We call φ-shadow every shadow Ξ satisfying the following conditions. We have Ξ(ε) = (ε, ∅ B , φ). For each a ∈ dom(Ξ), let k a be the number of b < a such that the node of Ξ at b is unary, and let (χ a , γ a , ψ a ) = Ξ(a). Then: The tree Ξ mapping each a ∈ dom(M ) to (χ a .γ a , φ a ) will be called the shadow of M .

-χ a is a sequence of subformulas of φ of length at most k a , -γ a ∈ R(φ, k a ), -χ a ∈ F (γ a ) -ψ a is a subformula of φ.
Recall that if M is a locally compact Λ NF -inhabitant of φ, then for each address a in M , the blueprint α a of M |a is of relative depth at most |Λ(M, a)| × |Sub(φ)|. Every maximal |Λ(M, a)|-compression of α a produces a shadow α ′ a with the same relative depth and of width at most |Λ(M, a)|, to which some element of R(φ, |Λ(M, a)|) is equivalent, thus the shadow of M is well-defined. Note that the choice of γ a is possibly not unique (although it is, since R is a selector and one can actually prove that γ ⊑ max m α and γ ′ ⊑ max m α implies γ ≡ γ ′ , but this property is irrelevant to our discussion). We assume that some γ a is chosen for each address a in M .

Obviously the shadow of M satisfies the first, second and fourth conditions in the definition of φ-shadows given above -in the next section, we prove that it satisfies also the third.

Compact shadows and compact inhabitants

Definition 4.9. A shadow Ξ is compact if and only if there are no a, b such that: a < b, the nodes of Ξ at a, b are of the same arity, Ξ(a) = (χ a , γ a , ψ), Ξ(b) = (χ b , γ b , ψ) and there exists γ ′ ⇑ γ b such that χ a ∈ F (γ ′ ). Compare this definition with the definition of compactness for term (Definition 3.8). With the help of three auxiliary lemmas, we now prove the key lemma of Section 4: if M is a compact inhabitant -a fortiori locally compact by Lemma 3.9 -then the shadow of M is a compact φ-shadow.

Lemma 4.10. If α ⇑ β ⊑ 1 β ′ , then there exists α ′ such that α ⊑ 1 α ′ ⇑ β ′ . Proof. (1) An immediate induction on |dom(β ′ )| shows that if α = β[a ← β |b ] and β ≡ β ′ , then there exist a ′ , b ′ such that a ′ < b ′ and α ≡ α ′ = β ′ [a ′ ← β ′ |b ′ ].
As a consequence, an immediate induction on the length of the derivation of α ⇑ β shows that the lemma holds if β ≡ β ′ .

(2) Another induction on |dom(β

′ )| shows that if α ⇑ β 1 β ′ , then there exists α ′ such that α 1 α ′ ⇑ β ′ . The only non trivial case is α = * (a1) (α 1 ), β = * (a1) (β 1 ) with α 1 ⇑ β 1 and β ′ = * (a1,a2) (β 1 , β 2 ) with β 1 ≡ β 2 . Since α 1 ⇑ β 1 ≡ β 2 , by (1) there exists α 2 such that α 1 ≡ α 2 ⇑ β 2 . Hence α = * (a1) (α 1 ) 1 * (a1,a2) (α 1 , α 2 ) ⇑ * (a1,a2) (β 1 , β 2 ) = β ′ .
(3) Using ( 1) and ( 2), the lemma follows by induction on the length of an arbitrary sequence (β 0 , . . . , β n ) such that

β 0 = β, β n = β ′ and β i-1 ≡ β i or β i-1 1 β i for each i ∈ [1, . . . , n]. Lemma 4.11. If α ⊑ 1 β, then F (α) ⊆ F (β). Proof. By induction on |dom(β)|. Since γ ≡ γ ′ implies F (γ) = F (γ ′ ) and |dom(γ)| = |dom(γ ′ )|,
it suffices to consider the case where α is a 1-compression of β. The case α = * (a1) (α 1 ) and β = * (a1,a2) (α 1 , α 2 ) is clear. The remaining cases follow easily from the induction hypothesis.

Lemma 4.12. If α ⊑ m β, then the set of all elements of F (β) of length at most m is a subset of F (α).

Proof. By induction on |dom(β)|. Again, we examine only the case α m β. The proposition is trivially true if m = 0. Suppose m > 0. The only non-trivial case is α ≡ * a (γ 1 , . . . , γ m ) and β ≡ * a (γ 1 , . . . , γ m , γ m+1 ) with γ i ≡ γ for all i. Let Φ = F (γ).

For each integer k, let Φ (k) = ⊛(Φ 1 , . . . , Φ k ) where Φ i = F (γ) for each i. Let φ = (φ 1 , . . . , φ p ) ∈ F (β) be such that p ≤ m. We have to prove that φ ∈ F (α). For each J ⊆ {1, . . . , p}, let (j 1 , . . . , j q ) be the strictly increasing enumeration of all elements of J and let f (J) = (φ j1 , . . . , φ jq ). We have φ ∈ F (β) = Φ (m+1) , hence there exist J 1 , . . . , J m+1 such that J 1 ∪ . . . ∪ J m+1 = {1, . . . , p}, and f (J i ) ∈ F (γ) for each i ∈ {1, . . . , m + 1}.

For each j ∈ {1, . . . , p}, let k j be any element of {1, . . . , m + 1} such that j ∈ J kj . Then

J k1 ∪ . . . ∪ J kp = {1, . . . , p}, so φ ∈ ⊛({f (J k1 )}, . . . , {f (J kp )}) ⊆ Φ (p) ⊆ Φ (m) = F (α).
Lemma 4.13. Let M be a locally compact Λ NF -inhabitant of φ. The shadow of M is a φ-shadow. If M is compact, then this shadow is also compact.

Proof. For each address a in M , the sequence χ a = Ω(Free(M |a )) is a subsequence of Ω(Λ(M, a)), hence the first proposition follows from the definition of the shadow of M , Lemma 1.5, Lemma 2.15.(3) and Lemma 4.12. Let Ξ be shadow of M . Assume Ξ is not compact. There exist a, b ∈ dom(Ξ) = dom(M ) such that Ξ(a) = (χ a , γ a , ψ), Ξ(b) = (χ b , γ b , ψ), the nodes at a,b in Ξ are of the same arity, and there exists

γ ′ ⇑ γ b such that χ a ∈ F (γ ′ ). We have M |a , M |b of the same kind. Let α a , α b be the blueprints of M |a , M |b . Since γ b ⊑ max |Λ(M,a•b)| α b , we have γ ′ ⇑ γ b ⊑ 1 α b . By Lemma 4.10 there exists α ′ such that γ ′ ⊑ 1 α ′ ⇑ α b . By Lemma 4.11, we have χ a ∈ F (γ ′ ) ⊆ F (α ′ ), hence M is not compact.

Finiteness of the set of compact φ-shadows

Our last aim will be to prove that for each formula φ, the set of all compact φ-shadows is a finite set effectively computable from φ.

In definition 5.1, we introduce a last binary relation ⋐ on blueprints. The key lemma of this section (Lemma 5.14) shows that whenever S ⊂ S is a finite set (in particular when S is the set of all subformulas of φ and all @'s tagged with a subformula of φ), the relation ⋐ is an almost full relation [START_REF] Bezem | Term Rewriting Systems[END_REF] on the set of all S-blueprints: for every infinite sequence γ 1 , γ 2 , . . . over B(S), there exists i, j such that i < j and γ i ⋐ γ j . This result will be proven with the help of Melliès' Axiomatic Kruskal Theorem [START_REF] Melliès | On a duality between Kruskal and Dershowitz theorems[END_REF]. The finiteness of the set of compact φ-shadows follows from this key lemma with the help of König's Lemma (Lemma 5.15). The ability to compute these shadows follows directly from their definition.

By Lemma 4.13, a consequence of this result is also the finiteness for each φ of the set of all compact Λ NF -inhabitants of φ, although our decision method is based on the computation of shadows of compact terms rather than a direct computation of those terms. It is worth mentioning that the proof of Theorem 5.13 is non-constructive and that it gives no information about the complexity of our proof-search method -this question might be itself another open problem.

Almost full relations and Higman Theorem

Definition 5.1. We let ⋐ be the relation on blueprints defined by α ⋐ β if and only if for all χ ∈ F (α), there exists γ ⇑ β such that χ ∈ F (γ).

Definition 5.2. Let U be an arbitrary set. An almost full relation (AFR) on U is a binary relation ≪ such that for every infinite sequence (u i ) i∈N over U, there exist i, j such that i < j and u i ≪ u j .

The main aim of Section 5 will be to prove the last key lemma from which we will easily infer the decidability of Λ NF -inhabitation: for each finite S ⊆ S, the relation ⋐ is an AFR on B(S).

Proposition 5.3.

1 If ≪ and ≪ ′ are AFRs on U, then ≪ ∩ ≪ ′ is an AFR on U. 2 Suppose ≪ U is an AFR on U and ≪ V is an AFR on V. Let ≪ U ×V be the relation defined by (U, V ) ≪ U ×V (U ′ , V ′ ) if and only if U ≪ U U ′ and V ≪ V V ′ . Then ≪ U ×V is an AFR on U × V.
Proof. See [START_REF] Melliès | On a duality between Kruskal and Dershowitz theorems[END_REF]. Both results appear in the proof of Theorem 1, Step 4 (p.523) as a corollary of Lemma 4 (p.520) Definition 5.4. Let U be a set, let ≪ be a binary relation. We let S(U) denote the set of all finite sequences over U. The relation ≪ S induced by ≪ on S(U) is defined by (U 1 , . . . , U n ) ≪ S (V 1 , . . . , V m ) if and only if there exists a strictly monotone function η : {1, . . . , n} → {1, . . . , m} such that U i ≪ V η(i) for each i ∈ {1, . . . , n}.

Theorem 5.5. (Higman) If ≪ is an AFR on U, then ≪ S is an AFR on S(U).

Proof. See [START_REF] Higman | Ordering by divisibility in abstract algebra[END_REF][START_REF] Kruskal | The theory of well-quasi-ordering: A frequently discovered concept[END_REF][START_REF] Melliès | On a duality between Kruskal and Dershowitz theorems[END_REF].

From rooted to unrooted blueprints

Melliès' Axiomatic Kruskal Theorem allows one to conclude that a relation is an AFR (a "well binary relation" in [START_REF] Melliès | On a duality between Kruskal and Dershowitz theorems[END_REF]) as long as it satisfies a set of five properties or "axioms" (six in the original version of the theorem -see the remarks of Melliès at the end of its proof explaining why five axioms suffice). The details of those axioms will be given in Section 5.3.

Four of those five axioms are relatively easy to check. The remaining axiom is more problematical. This rather technical section is entirely devoted to the proof of Lemma 5.11, which will ensure that this last axiom is satisfied. We want to prove the following proposition:

Let S be a finite subset of S. Let Bε be a subset of Bε(S).

Let B = { * a(β1, . . . , βn)| ∀i ∈ [1, . . . , n], βi ∈ Bε}. If ⋐ is an AFR on Bε, then ⋐ is an AFR on B.
Recall that B ε (S) stands for the set of all rooted S-blueprints. We want to be able to extend the property that ⋐ is an AFR on a given set of rooted blueprints to the set all blueprints that have those rooted blueprints at their minimal addresses.

Higman Theorem suffices to show that ⋐ S (Definition 5.4) is an AFR on the set of finite sequences over B ε . However, if one considers an infinite sequence (β i ) i∈N over B and transforms each β i = * ai (β i 1 , . . . , β i ni ) where β i 1 , . . . , β i ni ∈ B ε into σ(β i ) = (β i 1 , . . . , β i ni ), the theorem will only provide two integers i, j and strictly monotone function η such that i < j and β i k ⋐ β j η(k) for each k ∈ {1, . . . , n i }. This is sufficient to ensure that

β i = * ai (β i 1 , . . . , β i ni ) ⋐ * b (β j η(1) , . . . , β j η(ni)
), but not in general β i ⋐ β j . To bypass this difficulty we show how for each blueprint β ∈ B(S), one can extract from the set of all vertical compressions of β a complete set of "followers" of β of minimal size (Lemma 5.7). This set {α 1 , . . . , α p } has the property that for each φ ∈ F (β), there exists at least one α i such that F (α i ) contains a subsequence of φ -but not necessarily φ itself. The relative depth of each α i does not depend on the relative depth on β, but only on S: it is at most Σ 1+|S @ | i=1 i, where S @ is the set of all binary symbols in S. The lemma in proven in four steps.

First, observe that the set of all α ⇑ β of relative depth at most Σ

1+|S @ | i=1
i is a complete set of followers. If we consider the set of all γ such that γ ⊑ max 1 α for at least one such α, we obtain a (possibly infinite) set closed under ≡ and finite up to ≡. We call it the set of S-residuals of β.

Second, we prove that the set of S-residuals of β is a complete set of followers of β in the same sense, that is, for each φ ∈ F (β) there exists an S-residual γ of β such that F (γ) contains a subsequence of φ (Lemma 5.9).

Third, we prove that if β = * a (β 1 , . . . , β n ), . . , n], and if furthermore β, β ′ have the same set of S-residuals, then β ⋐ β ′ (Lemma 5.10).

β ′ = * b (β ′ 1 , . . . , β ′ n , β ′ n+1 , . . . , β ′ n+k ) are such that β i ⋐ β ′ i for each i ∈ [1, .
The last step is the proof of the lemma itself. The set of S-residuals is finite up to ≡ (Lemma 4.5), so there are only a finite number of possible values for the set of residuals of each S-blueprint. As a consequence, it is always possible to extract from an infinite sequence over B an infinite sequence of blueprints with the same set of residuals. The conclusion follows from the third step and Higman Theorem.

Definition 5.6. For every S ⊆ S, we let S @ denote the set of all binary symbols in S.

Lemma 5.7. Let S be a finite subset of S. For all β ∈ B(S), for all ψ ∈ F (β), there exists α of relative depth at most Σ 1+|S @ | i=1 i such that α ⇑ β and such that F (α) contains a subsequence of ψ. i. Indeed, suppose d is of maximal relative depth and not a starting address for (α, φ). Then d must be incomparable with each starting address for (α, φ). Let e be the shortest prefix of d in dom(α) that is incomparable with each starting address for (α, φ). The address e is of relative depth at most |S @ | in αotherwise there would exist in dom(α) an address f < e of relative depth |S @ | and a starting adress for (α, φ) of the form f • f ′ , of relative depth strictly greater than |S α |, a contradiction. Moreover the relative depth of d is the sum of the relative depth of e in α and the relative depth of α |e .

The cases β = ∅ B is immediate. If β = * a (β 1 , . . . , β n ), i = j and β i , β j = ∅ B , then the conclusion follows easily from the induction hypothesis. Suppose β = @ ψ (β 1 , β 2 ).

(1) Let d be an address of maximal length in β -1 (@ ψ ). Let δ = @ ψ (δ 1 , δ 2 ) = β |d . By assumption ε is the only element of δ -1 (@ ψ ). As ψ ∈ F (β), there exist ψ 0 ∈ F (δ), ψ 1 ∈ F (δ 1 ), ψ 2 ∈ F (δ 2 ) such that ψ 0 is a subsequence ψ and ψ 0 ∈ ⊚({ψ 1 }, {ψ 2 }). By induction hypothesis there exists an (S -{@ ψ })-linearisation (γ 1 , χ 1 ) satisfying conditions (1.a), (1.b) w.r.t (δ 1 , ψ 1 ), and an (S -{@ ψ })-linearisation (γ 2 , χ 2 ) satisfying conditions (2.a), (2.b), (2.c) w.r.t (δ 2 , ψ 2 ). Let γ = @ ψ (γ 1 , γ 2 ). We have γ ⇑ δ and β

(ε) = δ(ε) = γ(ε), hence γ ⇑ β. The blueprint γ 1 is of relative depth at most 1 + Σ |S @ |-1 i=1 i ≤ Σ |S @ | i=1 i. The blueprint γ 2 is of relative depth at most |S @ |+Σ |S @ |-1 i=1 = Σ |S @ | i=1 i. Therefore γ is of relative depth at most 1 + Σ |S @ | i=1 i. Now χ 2 is
a subsequence of ψ 2 with the same last element, so there exists in ⊚({χ 1 }, {χ 2 }) ⊆ F (@ ψ (γ 1 , γ 2 )) a subsequence χ of ψ 0 . Thus (γ, χ) satisfies (1.a) and (1.b) w.r.t (β, ψ).

(2) As ψ ∈ F (β), there exist

ψ 1 ∈ F (β 1 ), ψ 2 ∈ F (β 2 ) such that ψ ∈ ⊚({ψ 1 }, {ψ 2 })
. By induction hypothesis there exists an S-linearisation (α 1 , φ 1 ) satisfying conditions (1.a), (1.b) w.r.t (β 1 , ψ 1 ), and an S-linearisation (α 2 , φ 2 ) satisfying conditions (2.a), (2.b), (2.c) w.r.t (β 2 , ψ 2 ).

Let α 0 = @ ψ (α 1 , α 2 ). We have α 0 ⇑ β. The last elements of φ 2 , ψ 2 are equal and ⊚({φ 1 }, {φ 2 }) ⊆ F (α 0 ). Hence there exists in F (α 0 ) a subsequence φ 0 of ψ with the same last element as ψ. Thus (α 0 , φ 0 ) satisfies (2.a).

For all c incomparable with each starting address for (α 0 , φ 0 ), either c = (1) • c ′ and c ′ ∈ dom(α 1 ), or c = (2)•c ′′ and c ′′ ∈ dom(α 2 ) is incomparable with each starting address in α 2 . As a consequence, the choice of α 1 , α 2 ensures that (α 0 , φ 0 ) satisfies (2.c).

If (α 0 , φ 0 ) satisfies (2.b), then we may take (α, φ) = (α 0 , φ 0 ). Otherwise some starting address b for (α 0 , φ 0 ) does not satisfy condition (2.b). Let (b 1 , . . . , b n , b n+1 ) be the path to b in α. We have b 1 = ε, and for each i > 0, there exists d i such that b i = (2) • d i . The sequence (d 2 , . . . , d n+1 ) is then a path to d = d n+1 in α 2 , and d is a starting address for (α 2 , φ 2 ). The values α 2 (d 2 ), . . . , α 2 (d n ) are pairwise distinct, so there must exist i > 1 such that α(b i ) = @ ψ . Since b i is in the path to b, there exists in F (α 2|d i ) a subsequence φ ′ 0 of φ 0 with the same last element as φ 0 . For α ). The pair (α, φ) satisfies also those conditions w.r.t (β, ψ).

′ 0 = α 0 [ε ← α 2|d i ], we have α ′ 0 ⇑ β, φ ′ 0 ∈ F (α ′ 0 )
Definition 5.8. Let S be a finite subset of S. For all β ∈ B(S), for all α ⇑ β of relative depth at most Σ 1+|S @ | i=1 i, we call S-residual of β every α 0 such that α 0 ⊑ max 1 α.

Note that the set of S-residuals of β is {∅ B } if β = ∅ B . Otherwise, it is an infinite set: even if β = φ, the set of residuals of β is the ≡-equivalence class of β and contains all blueprints of the form * a (φ) (recall that ≡ is a subset of ⊑ 1 , see Definition 4.3).

Lemma 5.9. Let S be a finite subset of S. For all β ∈ B(S) and for all ψ ∈ F (β), there exists an S-residual α 0 of β such that F (α 0 ) contains a subsequence of ψ.

Proof. (1) Let γ, δ be arbitrary blueprints. Suppose γ 1 δ. We prove by induction on δ that for all φ ∈ F (δ), there exists in F (γ) a subsequence of φ. In order to deal with the case δ = @ φ (δ 1 , δ 2 ), we need to prove a slightly more precise property: for all φ ∈ F (δ), there exists in F (γ) a subsequence ψ of φ such that the last elements of φ, ψ are equal. The base case is δ = * (a1,a2) (γ 1 , γ 2 ), γ 1 ≡ γ 2 and γ = * a1 (γ 1 ), and this case is clear. Other cases follow easily from the induction hypothesis.

(2) We prove the lemma. By Lemma 5.7 and by definition of an S-residual, there exist α 0 , α such that α 0 ⊑ 1 α ⇑ β, F (α) contains a subsequence of ψ and α 0 is an S-residual. It follows from (1) that F (α 0 ) contains a subsequence of ψ.

Lemma 5.10. Let S be a finite subset of S. Suppose:

-β = * a (β 1 , . . . , β n ) ∈ B(S), -β ′ = * b (β ′ 1 , . . . , β ′ n , β ′ n+1 , . . . , β ′ n+k ) ∈ B(S), -β i ⋐ β ′ i for each i ∈ {1, . . . , n}, -the sets of S-residuals of β and β ′ are equal. Then β ⋐ β ′ . Proof. Let ψ ∈ F (β). There exists for each i ∈ [1, . . . , n] a sequence ψ i ∈ F (β i ) such that ψ ∈ ⊛({ψ 1 }, . . . , {ψ n }). By assumption there exists for each i ∈ [1, . . . , n] an α i ⇑ β ′ i such that ψ i ∈ F (α i ). As a consequence ψ ∈ F ( * (α 1 , . . . , α n )).
By Lemma 5.9 there exists an S-residual α 0 of β such that F (α 0 ) contains a subsequence φ of ψ. By assumption α 0 is also an S-residual of β ′ , hence there exist α

′ 1 , . . . , α ′ n+k , b such that α 0 ⊑ 1 * b (α ′ 1 , . . . , α ′ n+k ) ⇑ β ′ . By Lemma 4.11, we have φ ∈ F ( * b (α ′ 1 , . . . , α ′ n+k )). Hence for each i ∈ [1, . . . , n + k], there exists in F (α ′ i ) a subsequence of φ, which is also a subsequence of ψ. Now, let α = * b (α 1 , . . . , α n , α ′ n+1 , . . . , α ′ n+k ). Then α ⇑ β ′ , ψ ∈ F ( * (α 1 , . . . α n ))
, and for each j ∈ [1, . . . , k] there exists in F (α ′ n+j ) a subsequence of ψ. As a consequence ψ ∈ F (α).

Lemma 5.11. Let S be a finite subset of S. Let B ε be a subset of

B ε (S). Let B = { * a (β 1 , . . . , β n )| ∀i ∈ [1, . . . , n], β i ∈ B ε }. If ⋐ is an AFR on B ε , then ⋐ is an AFR on B. Proof. Let R = B(S, Σ 1+|S @ | i=1
i, 1) (see Definition 4.4). For each β ∈ B, let ρ(β) be the set of S-residuals of β. We have ρ(β) ⊆ R. Moreover ρ(β) is closed under ≡ (as ≡ is a subset of ⊑ 1 , see Definition 4.3), that is, ρ(β) is a union of the elements of a subset of R/ ≡ . By Lemma 4.5.(1) the latter is a finite set, therefore {ρ(β) | β ∈ B} is a finite set.

For each β = * a (β 1 , . . . , β n ) ∈ B where a is increasing w.r.t the lexicographic ordering of addresses and β 1 , . . . , β n ∈ B ε , let σ(β) = (β 1 , . . . , β n ) -recall that we can take a = ε, n = 0 if β = ∅ B , and a = (ε), n = 1 if β is a rooted blueprint. Since {ρ(β) | β ∈ B} is a finite set, every infinite sequence over B contains an infinite subsequence of blueprints with the same set of S-residuals. By assumption ⋐ is an AFR on B ε . By Theorem 5.5, ⋐ S is an AFR on {σ(β) | β ∈ B}.

Thus for every infinite sequence (β i ) i∈N over B there exist i, j such that i < j, σ(β i ) ⋐ S σ(β j ) and β i , β j have the same set of residuals. For σ(β i ) = (β i 1 , . . . , β i n ) and σ(β j ) = (β j 1 , . . . , β j n+k ), there exists a subsequence (β i l1 , . . . , β i ln ) of σ(β j ) such that β i 1 ⋐ β i l1 , . . . , β i n ⋐ β i ln . There exist also l n+1 , . . . , l n+k and two sequences a and b such that β i = * a (β i 1 , . . . , β i n ) and β j = * b (β j l1 , . . . , β j ln , β j ln+1 , . . . , β j l n+k ). By Lemma 5.10 we have β i ⋐ β j .

Axiomatic Kruskal Theorem and main key lemma

The following definition is borrowed from [START_REF] Melliès | On a duality between Kruskal and Dershowitz theorems[END_REF]):

Definition 5.12. An abstract decomposition system is an 8-tuple (T , L, V, T , L , V ,

• -→, ⊢)

where:

-T is a set of terms noted t, u, . . . equipped with a binary relation T , -L is a set of labels noted f, g, . . . equipped with a binary relation L , -V is a set of vectors noted T, U, . . . equipped with a binary relation V , - For each such system, we let ⊲ T be the binary relation on T defined by

t ⊲ T u ⇐⇒ ∃(f, T ) ∈ L × V, t f -→ T ⊢ u
An elementary term t is a term minimal w.r.t ⊲ T , that is, a term for which there exists no u such that t ⊲ T u.

Theorem 5.13. (Melliès) Suppose (T , L, V, T , L , V ,

• -→, ⊢) satisfies the following properties:

-(Axiom I) There is no infinite chain t 1 ⊲ T t 2 ⊲ T . . .

-(Axiom II) The relation T is an AFR on the set of elementary terms.

-(Axiom III) For all t, u, u ′ , if t T u ′ and u ⊲ T u ′ , then t T u. -(Axiom IV-bis) For all t, u, f, g, T, U , if t f -→ T and u g -→ U and f L g and T V U , then t T u.

-(Axiom V) For all W ⊆ V, for W ⊢ = {t ∈ T | ∃T ∈ W, T ⊢ t}, if T is an AFR on W ⊢ , then V is an AFR on W.

If furthermore L is an AFR on L, then T is an AFR on T .

Proof. See [START_REF] Melliès | On a duality between Kruskal and Dershowitz theorems[END_REF]. Mellies' result is actually established for an alternate list of axioms (numbered from I to VI). The possibility to drop Axiom VI and to replace Axiom IV with Axiom IV-bis is a remark that follows the proof of the main theorem.

Lemma 5.14. For each finite S ⊆ S, the relation ⋐ is an AFR on B(S).

Proof. According to Lemma 5.11 it is sufficient to prove that ⋐ is an AFR on B ε (S). Let (T , L, V, T , L , V ,

• -→, ⊢) be the abstract decomposition system defined as follows.

-The set T is B ε (S); we let α T β if and only if there exists an address c such that α ⋐ (β |c ) and α(ε) = (β |c )(ε). -The set L is the set of all @'s in S, the relation L is the identity relation on this set.

-The set V is B(S) × B(S).

The relation V is defined by (α 1 , α 2 ) V (β 1 , β 2 ) if and only if α 1 ⋐ β 1 and α 2 ⋐ β 2 .

-The relation Note that the elements of V are pairs of blueprints that may be rootless. However if V ⊢ β, then the blueprint β is always a rooted blueprint, thus the relation ⊢ is indeed a subset of V × T . (A) For all T ′ ⊆ T , the relation ⋐ is an AFR on T ′ if and only if T is an AFR on T ′ . Indeed, consider an arbitrary infinite sequence α over T ′ . This sequence contains an infinite subsequence (α) i∈N such that all α i (ε) are equal. Clearly α i ⋐ α j implies α i T α j . Conversely, if α i T α j , then there exists c such that α i ⋐ α j |c and α i (ε) = α j (ε) = α j (c). So α i ⋐ α j |c ⇑ α j , hence α i ⋐ α j .

(B) We now check that all axioms of Theorem 5.13 are satisfied. Axiom I is clear. The set of elementary terms is the set of all blueprints consisting of single formulas of S. The relation T is of course an AFR on the set of elementary terms, that is, axiom II is satisfied. Axiom III is immediate. If (α 1 , α 2 ) V (β 1 , β 2 ) then α 1 ⋐ β 1 and α 2 ⋐ β 2 , hence @ ψ (α 1 , α 2 ) ⋐ @ ψ (β 1 , β 2 ), a fortiori @ ψ (α 1 , α 2 ) T @ ψ (β 1 , β 2 ), hence Axiom IVbis is satisfied. It remains to prove that Axiom V is satisfied. Let W ⊆ V. By definition W ⊢ = {β ∈ T | ∃(α 1 , α 2 ) ∈ W, (α 1 , α 2 ) ⊢ β}. Assuming T is an AFR on W ⊢ , we prove that V is an AFR on W. Lemma 5.15. For each formula φ, the set of all compact φ-shadows is a finite set effectively computable from φ.

Proof. For each compact φ-shadow Ξ and for each address a such that a is a leaf in Ξ, call step-continuation at a of Ξ every compact φ-shadow Ξ ′ such that dom(Ξ ′ ) dom(Ξ) ∪ {a • (1), a • (2)} and Ξ, Ξ ′ take the same values on dom(Ξ). Let be the relation defined by Ξ Ξ ′ if and only if Ξ ′ is a step continuation of Ξ. By Lemma 4.5 and the fact that the set of subformulas of φ is a finite set, for all Ξ, the set of all Ξ ′ such that Ξ Ξ ′ , is a finite set effectively computable from Ξ. Let C be the closure under of {(ε → (ε, ∅ B , φ))} The set of all compact φ-shadows is clearly equal to this set, hence it suffices to prove that C is a finite set. Assume by way of contradiction that C is infinite. By König's Lemma there exists an infinite sequence Ξ 0 Ξ 1 . . . over C. The union Ξ ∞ = ∪ i≥0 Ξ i is a tree of infinite domain. By König's Lemma again, there exists an infinite chain of addresses a 1 < a 2 < . . . such that all a i are nodes of Ξ ∞ with the same arity and labelled with the same subformula of φ. If i < j and a i , a j are labelled with (χ i , γ i , ψ), (χ i , γ j , ψ), then we cannot have γ i ⋐ γ j , otherwise there would exist a k such that Ξ k is not compact. A contradiction follows from Lemma 5.14.

6. From the shadows to the light Theorem 6.1. Ticket Entailment is decidable.

Proof. The following propositions are equivalent:

the formula φ is provable in the logic T → , -the formula φ is inhabited by a combinator within the basis BB ′ IW, -the formula φ is Λ NF -inhabited (Lemma 1.10), -there exists a compact Λ NF -inhabitant of φ (Lemma 3.9) -there exists a compact φ-shadow with the same tree domain as a Λ NF -inhabitant of φ (Lemmas 3.9 and 4.13).

By Lemma 5.15, the set of compact φ-shadows is effectively computable from φ. By the subformula property (Lemma 1.5), for each shadow Ξ in this set, up to the choice of bound variables, there are only a finite number of Λ NF -inhabitant of φ with the same domain as Ξ. Moreover this set of inhabitants is clearly computable from Ξ and φ. Hence the existence of a Λ NF -inhabitant of φ is decidable.

Fig. 1 .

 1 Fig. 1. Principle of the proof of decidability of type inhabitation for HRM-terms.

  is a type for W; (xii) follows from (xi) and Lemma 1.8; (xiii) follows from (x), (xii) and modus ponens; (xiii) is ⊢ BB'IW ω k1 . . . ω kp → ψ.

Fig. 3 .

 3 Fig. 3. An element of Λ NF with its blueprint (x0 < x1 < y1, x2 < x3 < y0 < y2, x1 < y0 < y2).

Fig. 4 .

 4 Fig. 4. Principle of blueprint reduction.

Fig. 7 .

 7 Fig. 7. How the blueprint of M evolves into the blueprint of λx.M

  Proof. Property (1) follows immediately from the definition of a blueprint. Since α n = α and α 0 = ∅ B , Property (3) follows from Property (2.a). Property (2.b) follows from Property (2.a) and Lemma 2.14. As to prove (2.a) we introduce the following notations.For each N ∈ Λ NF , we let ρ N be the least partial function satisfying the following conditions: for every blueprint γ, we have ρ N (ε, γ) = γ; for every finite sequence of variables Y and for every blueprintγ, if ρ N (Y, γ) = δ, {b | N |b = y} = {b 0 , . . . , b m } and δ ⊲ b0 χ . . .⊲ bm χ δ ′ , then ρ M ((y)•Y, γ) = δ ′ . By Lemma 2.14, if {b | N |b = y} = {b 0 , . . . , b m } = {c 0 , . . . , c m }, δ⊲ b0 χ .. .⊲ bm χ δ ′ and δ⊲ c0 χ . . .⊲ cm χ δ ′′ , then δ ′ = δ ′′ , thus ρ N is indeed a function. For each finite sequence of variables Y ′ and for each blueprint γ, we let µ N (Y ′ , γ) be the restriction of γ to dom(γ) ∩ {b | Free(N |b ) ⊆ Y ′ }.

Fig. 8 .

 8 Fig. 8. A non-uniform renaming of the variables of M , based on an alternate extraction of the formulas of its blueprint.

  Lemma 2.16. Let M ∈ Λ NF be a term of blueprint α. Then for every strictly increasing sequence of variables Y = (y 1 , . . . , y m ) such that Ω(Y ) = (ω 1 , . . . , ω m ), there exists N with the same domain, blueprint and of the same type as M such that Free(N ) = Y and {b | N |b = y i } = {b i 1 , . . . , b i pi } for each i. Proof. By induction on M . The proposition is clear if M is a variable. The case of M = (M 1 M 2 ) follows easily from the induction hypothesis. Suppose M = λx.M 1 : φ → ψ with M 1 γ. Let Y ′ = (y 1 , . . . , y m , x). By Lemma 2.15.(2.a) there exist a 1 , . . . , a p such that {a 1 , . . . , a p } = {a | M |a = x} and γ ⊲ a0 φ . . . ⊲ ap φ γ ′ = α |1 . Now By induction hypothesis there exists N 1 with the same domain, blueprint and of the same type as M 1 such that Free(N 1 ) = Y ′ , {a | N 1|a = x} = {a 0 , . . . , a p } and {c | N 1|c = y i } = {c i 0 , . . . , c i pi } for each i. By Lemma 2.15.(2.b) we have λx.N 1 α, hence we may take N = λx.N 1 .

  Lemma 3.5. Let M be a Λ NF -inhabitant of φ. If M is not locally compact, then there exist two addresses b, b ′ such that b < b ′ , M |b and M |b ′ are of the same kind and Free(M |b ) = Free(M |b ′ ). Moreover, M is not a Λ NF -inhabitant of φ of minimal size. Proof. For each address a in dom(M ), let α a be the blueprint of M |a and let X a = Free(M |a ). Assume the existence of an α a of relative depth n > |Λ(M, a)| × |Sub(φ)|. There exist b 1 , . . . , b n+1 ∈ dom(α a ) such that b 1 < . . . < b n < b n+1 . By Lemma 2.8.(1) we have X a•bn ⊆ . . . ⊆ X a•b1 ⊆ Λ(M, a). By Lemma 1.5, each φ a•bi is a subformula of φ.

Definition 3. 6 .

 6 We let ⇑ be the least reflexive and transitive binary relation on blueprints satisfying the following: if a, b ∈ dom(β), a < b and β(a) = β(b), then β[a ← β |b ] ⇑ β. Lemma 3.7. Suppose M ∈ Λ NF , M : φ, M β and α ⇑ β. There exists a term M ′ ∈ Λ NF of the same kind as M , of blueprint α and such that |dom(M ′ )| ≤ |dom(M )|. Proof. It suffices to consider the case of α = β[a ← β |b ] with a, b ∈ dom(β), a < b and β(a) = β(b). We prove the existence of M ′ by induction on the length of a. If a = ε then M is necessarily an application and β(ε) = β(b) = @ φ , hence M |b is an application of type φ, and we can take M ′ = M |b . Assume a = ε.

Fig. 10 .

 10 Fig. 10. Proof of Lemma 3.5.

  1 is of type χ and {c | M ′′ 1 |c = y} = {c 0 , . . . , c p }. By Lemma 2.15.(2.b) we have λy.M ′′ 1 α, hence we may take M ′ = λy.M ′′ 1 . Definition 3.8. A term M ∈ Λ NF is compact when there are no a, b, α ′ such that a < b, M |a and M |b are of the same kind, M |b α b , α ′ ⇑ α b and Ω(Free(M |a )) ∈ F (α ′ ).

Fig. 11 .

 11 Fig. 11. Proof of Lemma 3.9, part (1).

  Definition 4.8. Let M be a locally compact Λ NF -inhabitant of φ. For each a ∈ dom(M ):let χ a = Ω(Free(M |a )), -let α a be the blueprint of M |a , -let γ a ∈ R(φ, |Λ(M, a)|) be such that γ a ⊑ |Λ(M,a)| α a , -let φ a be the type of M |a .

Fig. 12 .

 12 Fig. 12. A compact inhabitant and its shadow.

  Proof. Call S-linearisation every pair (γ, χ) such that γ ∈ B(S) and χ ∈ F (γ). Call starting address for (γ, χ) every address b for which there exist φ, γ′ such that γ ⊲ b φ γ ′ and χ ∈ ⊚(F (γ ′ ), (φ)). Call path to b in γ the maximal sequence (b 1 , . . . , b n , b n+1 ) over dom(γ) such that b 1 < . . . < b n < b n+1 = b.Given an arbitrary S-linearisation (β, ψ), we prove simultaneously by induction on |dom(β)| the following properties:1 There exists an S-linearisation (γ, χ) such that: (a) γ ⇑ β and χ is a subsequence of ψ, (b) γ is of relative depth at most 1 + Σ |S @ | i=1 i. 2 There exists an S-linearisation (α, φ) such that: (a) α ⇑ β, φ is a subsequence of ψ, and if ψ = ε, then the last elements of φ, ψ are equal, (b) for each starting address b for (α, φ) and for (b 1 , . . . , b n , b n+1 ) equal to the path to b in α, the values α(b 1 ), . . . , α(b n ) are pairwise distinct, (c) for all c incomparable with each starting address for (α, φ), (α |c ) is of relative depth at most 1 + Σ |S @ | i=1 i. Note that the conjunction of (2.b) and (2.c) implies that every address d in α is of relative depth at most |S @ |+1+Σ |S @ | i=1 i = Σ 1+|S @ | i=1

  and the last elements of φ ′ 0 , φ 0 , ψ are equal. By induction hypothesis there exists an S-linearisation (α, φ) satisfying (2.a), (2.b), (2.c) w.r.t (α ′ 0 , φ ′ 0

•-→

  is a relation on T × L × V, e.g. t f -→ T -⊢ is a relation on V × T , e.g. T ⊢ t.

•-→

  is defined by α@ φ -→ (β 1 , β 2 ) if and only if α = @ φ (β 1 , β 2 ).-The relation ⊢ is the least relation satisfying the following condition. If V = (α 1 , α 2 ), i ∈ {1, 2}, β 1 , . . . , β n ∈ B ε (S) and α i = * a (β 1 , . . . , β n ), then V ⊢ β j for each j ∈ [1, . . . , n].

  By (A) the relation ⋐ is an AFR on W ⊢ ⊆ B ε (S). Let B = { * a (β 1 , . . . , β n )| ∀i ∈ [1, . . . , n], β i ∈ W ⊢ }.By Lemma 5.11 the relation ⋐ is an AFR on B. Moreover W ⊆ B × B. By Proposition 5.3.(2) the relation V is an AFR on B × B, therefore an AFR on W.

† In the course of the publication of this article, we heard of a work in progress by Katalin Bimbò and Michael Dunn towards a solution that is seemingly based on a different approach.

Acknowledgments

This work could not have been achieved without countless helpful comments and invaluable support from Pawe l Urzyczyn, Paul-André Melliès and Pierre-Louis Curien. I am also deeply indebted to the anonymous referees for their remarkably careful reading.

Again the elements of a • (b), a • (c) and b • (c) must be pairwise incomparable addresses, and α, β, γ must be non-empty. Note that for all non-empty β, we have ∅ B 0 β, hence the empty blueprint is the only blueprint of null width. If β is of width m > 0, then for all addresses a, for β |a = * a (γ 1 , . . . , γ k ) and for each γ i = ∅ B , the sequence (γ 1 , . . . , γ k ) contains no more than m blueprints ≡-equivalent to γ i . For instance, if φ, ψ, χ are distinct formulas, * (φ, φ, φ, ψ, ψ, χ) is of width 3, * (ω, @ ω ( * (φ, ψ), φ), @ ω ( * (ψ, φ), φ)) is of width 2, etc. For instance, if φ, ψ, χ are distinct formulas: Let (α 1 , . . . , α k ) be an enumeration of R ε (S, d, m). Let Σ d be the set of all functions from {1, . . . , k} to {0, . . . , m}. For each β ∈ B(S, d, m) there exist β 1 , . . . , β n ∈ B ε (S, d, m) and b such that β = * b (β 1 , . . . , β n ). We let σ β be the function mapping each i ∈ {1, . . . , k} to the number of occurrences of an element ≡-equivalent to α i in the sequence (β 1 , . . . , β n ). Clearly σ β ∈ Σ d and furthermore for all β ′ ∈ B(S, d, m) we have

The finiteness of B ε (S, d+1, m)/ ≡ follows immediately from the finiteness of B(S, d, m) and the fact that if β = @ φ (β 1 , β 2 ) and

The same property allows us to define R ε (S, d + 1, m) as the set of all blueprints of the form @ φ (γ 1 , γ 2 ) where @ φ ∈ S and each γ i is a non-empty element of R (S, d, m).

(2) The lemma follows by induction on d, using (1) and the facts that: B ε (S, 0, 0) is