Keywords: independent double-gate MOSFETs, short-channel effects, quantum confinement effects, numerical simulation

A two-dimensional (2D) numerical simulation code of drain current including selfconsistent solving of the Schrödinger and Poisson equations coupled with the drift-diffusion transport equation in double-gate (DG) metal-oxide-semiconductor field-effect transistor (MOSFET) devices has been developed. This code has been used to investigate the operation of independent DG (IDG) MOSFETs compared with classical DG MOSFETs in terms of short-channel effects (SCEs) and carrier quantum confinement. Simulations show that IDG MOSFET operation is different from that of DG MOSFETs due to the presence of a transverse electric field in the first structure that induces significant enhancement of quantum mechanical confinement. This leads to subthreshold performance degradation and to SCE enhancement in IDG MOSFETs compared with DG MOSFETs. We show that, in contrast to DG MOSFETs, quantum confinement effects must be taken into account in IDG MOSFET operation even for thick silicon films ( > 10 -15 nm).

Introduction

Because metal-oxide-semiconductor field-effect transistor (MOSFET) scaling is approaching its limits, double-gate (DG) MOSFETs are envisaged as a possible alternative to conventional bulk MOSFETs. Despite excellent electrical performance characteristics due to its multiple conduction surfaces, conventional DG MOSFETs allow only three-terminal operation because the two gates are tied together. DG structures with independent gates have been recently proposed [START_REF] Mathew | Proc. IEEE Int. SOI Conf[END_REF][START_REF] Masahara | [END_REF][3][4][5] , allowing a four-terminal operation. Independent DG (IDG) MOSFETs offer additional advantages, such as dynamic threshold voltage control by one of the two gates and transconductance modulation, in addition to the conventional switching operation [START_REF] Mathew | Proc. IEEE Int. SOI Conf[END_REF]3) .

In this study, we propose a two-dimensional (2D) numerical simulation code for the drain current including self-consistent solution of the Schrödinger and Poisson equations coupled with the drift-diffusion transport equation. This quantum drift-diffusion code is used to analyze the variation with the back gate bias of electrical parameters, such as threshold voltage (V T ), V T roll-off, drain-induced barrier lowering (DIBL) effect, and subthreshold swing (S). The difference between classical (i.e., without quantum confinement) and quantum threshold voltages (∆V Tq ), as a function of different silicon film thicknesses (3-10 nm) in IDG MOSFETs, is also thoroughly investigated. An extensive comparison between the IDG mode (the front and back gates are biased independently) and the DG mode (the front and back gates are tied together, i.e. conventional DG MOSFETs) is also performed to show the effects of the transverse electric field on carrier quantum confinement and subthreshold performance characteristics of IDG MOSFETs.

Simulation Details

Simulated devices

The IDG MOSFET considered in this study is schematically shown in Fig. 1(a). The structure is symmetric with an intrinsic thin silicon film and a highly doped source and drain regions (N SD = 3×10 20 cm -3 ). Identical midgap metal gates (Φ mf = Φ mb = 4.61 eV) and front and back gate-oxide layers of 1.0 nm thickness (T oxf = T oxb = T ox ) have been also considered.

The front and back gates are biased with V Gf and V Gb , respectively. In order to investigate the SCEs and quantum mechanical confinement in IDG MOSFETs, different gate lengths (L = 200, 50, and 20 nm) and silicon film thicknesses (T Si = 10, 5, and 3 nm) have been simulated.

Quantum drift-diffusion simulation code

In this study, we developed a 2D numerical simulation code that describes the operation of IDG MOSFETs. The code can take into account asymmetric devices (i.e., with independent gate bias, different gate work functions, or different gate-oxide thicknesses) and both nchannel and p-channel IDG MOSFETs.

The code is based on the numerical solution of the Poisson equation or Poisson-Schrödinger system coupled with the standard drift-diffusion transport equation (DDTE). The charge density (and consequently, the drain current) can be evaluated in both classical (Poisson + DDTE) and quantum-mechanical (Poisson-Schrödinger + DDTE) cases; the latter being commonly called "quantum drift-diffusion" in the literature [6][7][8] .

Poisson, Schrödinger, and DDTE equations are solved using a finite difference scheme with a uniform mesh on a 2D domain including the channel, source and drain regions, gateoxide layers, and gate electrodes. Electric field penetration in the source and drain regions and electron wave function penetration in the gate-oxide layers can thus be taken into account. A flowchart of the code is shown in Fig. 1(b).

In the following, we briefly describe the equations for an n-channel fully depleted IDG device. Similar equations can be derived for p-channel structures. For a given channel geometry and bias conditions, the 2D Poisson equation is solved [see the flowchart in Fig.

1(b)

] considering the charge density given as [START_REF] Taur | Fundamentals of Modern VLSI Devices[END_REF] [ ]

DOP (x, y) q N n(x, y) ρ = × - , (1)
where q is the absolute value of the electron charge, N DOP is the doping atom concentration in the Si film (N DOP = +N D in the source and drain regions and N DOP = -N A in the channel), and n(x,y) is the electron density.

In the classical case, n is evaluated using the well-known Fermi-Dirac or Boltzmann statistics ( )

C C F n(x, y) N exp E (x, y) (x)   = -β -Φ   , (2)
where β = q/kT, Φ Fn (x) is the 1D electron quasi-Fermi level (carrier transport is purely 1D in the channel device if the ratio of channel length to film thickness is typically greater than 3, which is the case in this study), E C (x,y) is the minimum of the conduction band, and N C is the effective three-dimensional (3D) density of states for the conduction band.

In the quantum case, Poisson and Schrödinger equations [Fig. 1(b)] are self-consistently solved [6][7][8] . Owing to the thin body, a strong vertical confinement (in the y-direction) causes the separation between carrier subbands to be large in energy. Every subband is then treated individually and the quasi-Fermi level populates only a few modes even at a high bias. The quantum charge density n Q is given as 10)

( ) { } lev N 2 t,l i i Q t,l t,l t,l F 2D 2 l,t i 1 qkT n (x, y) m g (x, y) ln 1 exp E (x) (x) =   = × Ψ × + -β -Φ   π ∑ ∑ h , (3)
where subscript t refers to transverse electrons (m t * = 0.19×m 0 , g t = 4, ), E i t,l (x) is the ith (t or l) carrier energy subband induced by the one-dimensional (1D) vertical confinement, Ψ i t,l (x,y) is the corresponding normalized wave function, and N lev is the maximum number of modes considered (we assume here N lev =20 to correctly treat both source/drain and channel regions).

The next solving step concerns the continuity equation [Fig. 1(b)], which is numerically solved to ensure a constant drain current along the channel (x-direction). The continuity equation gives the numerical solution of the quasi-Fermi level Φ F (x) used in eqs. ( 2) or (3).

After reaching convergence, the drain current density is finally evaluated from the driftdiffusion expression [START_REF] Munteanu | [END_REF]11) F d (x) J(x, y) q µ(x, y) n(x, y) dx

Φ = -× × × , ( 4
)
where µ is the electron mobility. To facilitate our understanding of quantum confinement effects in IDG MOSFETs, we considered here a constant mobility (the mobility dependences as function of transverse and longitudinal electric fields, lattice temperature, and doping level and the subband modulation on the channel mobility are not taken into account in our simulations 12) ). Note that the solution of the Poisson-Schrödinger system can also be coupled with the ballistic transport equation, as was presented in a previous work 11,13) .

The code provides considerable additional information and valuable physical insights (such as the 2D profile of electrostatic potential, classical and quantum carrier densities in the channel, energy levels, and total inversion charge) used to investigate the SCEs and quantummechanical effects in IDG MOSFETs. Simulated I DS (V Gf ) characteristics in DG and IDG MOSFETs have been compared in the classical case with data obtained from simulation with a commercial code 14,15) (Atlas Silvaco [START_REF]Atlas User's Manual[END_REF] ). An excellent fit has been obtained for large ranges of gate lengths, silicon film thicknesses, and V Gb values.

We end this section with a discussion of the domain validity of our simulation approach.

As device dimensions continue to decrease, the channel lengths (widths and/or thicknesses) are approaching the characteristic wavelength of particles (for example, the de Broglie wavelength at the Fermi energy) and quantum effects are expected to be increasingly significant. Quantum effects (related to both carrier confinement and quantum ballistic transport) may dominate the operation of nanoscale devices: for example, it is expected that direct source-to-drain tunnelling will be a serious limiting physical phenomenon for future device scaling (typically below 6-8 nm channel length 11,[START_REF] Autran | [END_REF] ). The drift-diffusion transport model considered in this study does not have predictive capability for simulating quantum transport in ultra small structures; quantum transport tools are thus required for accurate description of nanoscale device operation. Different approaches have been developed, one of the most precise being the solving of the Schrödinger equation with open boundary conditions, as performed using the non-equilibrium Green's function (NEGF) formalism 13,18- 20) . However, in this paper, the smallest channel length considered in simulation is L=20 nm.

For channel lengths larger than 20 nm, it can be considered that quantum transport is still limited and that carrier transport can be described by the drift-diffusion approach with a sufficient accuracy.

Results and Discussion

For all simulations, a constant carrier mobility [µ(x,y) = 200 cm 2 /(V.s)] in the silicon film (source-channel-drain) has been considered. I DS (V Gf ) characteristics of an n-channel IDG MOSFET in classical (dash lines) and quantum (solid lines) cases for different back gate biases are shown in Fig. 2(a). We can firstly note that V Gb modulates I DS (V Gf ) characteristics in both the classical and quantum cases. Then, the main electrical parameters in the subthreshold regime (threshold voltage V T , subthreshold swing S, and off-state current I off ) are also modulated by V Gb . These parameters depend on the transverse electric field E xC in the structure, given as 21) ( ) ( )

ox ox Si Si FBb FBf Gb Gf xC T 2 T V V V V E         ε ε + - - - = , (5)
where V FBf and V FBb are the flat-band voltages at the front and back gates (in our case V FBf = V FBb , because the two gates are considered identical), and ε Si and ε ox are the silicon film and oxide-gate permittivity, respectively. We can also observe in Fig. 2(a) the marked effect of quantum mechanical confinement on the electrical parameters of the IDG MOSFET even when the silicon film is relatively thick. To compare the effects of quantum confinement in IDG MOSFETs (V Gb ≠ V Gf ) and DG MOSFETs (V Gb = V Gf ), I DS (V Gf ) curves in the classical and quantum cases are presented in Fig. 2(b) for V Gb = 0 V. In DG MOSFETs, the I DS (V Gf ) characteristic in the quantum case simply shifts towards the right side and the subthreshold swing is the same as that obtained in the classical case. In IDG MOSFETs, the subthreshold swing is degraded in addition to the shift of the I DS (V Gf ) characteristics in the quantum case compared with the classical case. Thus, the quantum-induced shift in I DS (V Gf ) curves is larger in IDG MOSFETs than in DG MOSFETs.

Figure 3 shows the threshold voltage [extracted by the constant current method at a current of 100 nA/L(nm) from I DS (V Gf ) curves at V D = 1.0 V] in the IDG MOSFET, as a function of V Gb for L = 50 nm and two different silicon film thicknesses in both the classical and quantum cases. The high threshold voltages are due to the midgap metal gates chosen for DG MOSFET structures. As expected, the threshold voltage varies linearly when V Gb increases from -1.0 to ~0.1 V in both the classical and quantum cases. This V T linear variation of the threshold voltage and other peculiarities of IDG MOSFETs, such as the gain in sensitivity to V Gb , can be practically used for circuit applications such as signal mixers and memory cells [START_REF] Mathew | Proc. IEEE Int. SOI Conf[END_REF][START_REF] Masahara | [END_REF][3][4][5] . Figure 3 shows that the quantum threshold voltage is always higher than the classical one owing to quantum confinement that causes electron density reduction in the silicon film. We also note that the classical and quantum threshold voltages are nearly equal when V Gb reaches V Gf = V T , i.e., when E xC tends to zero. Thus, the effect of carrier quantization in IDG MOSFETs is minimal when the transverse electric field is close to zero, i.e., when the electric-field-induced quantum confinement is weak.

The threshold voltage as a function of T Si in the IDG MOSFET (at V Gb = 0 V) and the DG MOSFET for L = 50 nm in the classical and quantum cases is presented in Fig. 4. In the DG MOSFET, the reduction in T Si only induces a slight increase in threshold voltage. The difference between the quantum and classical threshold voltages is small in the DG MOSFET for all silicon film thicknesses. A different behaviour is obtained for the IDG MOSFET: the increase in threshold voltage when T Si decreases is large, particularly in the quantum simulation. The difference between the classical and quantum V T is found to be markedly increased in the IDG MOSFET compared with the DG MOSFET, owing to the occurrence of electric-field-induced quantum confinement in the IDG MOSFET in addition to structural quantum confinement. These results illustrate the significant impact of quantum confinement on electrical parameters of IDG MOSFETs, particularly for thin silicon films.

In order to investigate SCEs in IDG MOSFETs, the V T roll-off variation versus T Si in both the classical and quantum cases at different V Gb is shown in Fig. 5. The V T roll-off for a specific channel length L is calculated at V D = 0.1 V as V T (L = 200 nm) -V T (L). The V T rolloff is higher in the quantum case, because the quantum confinement tends to move the charge centroid away from the front interface, and thus, the control by the front gate of SCEs is less effective. This effect is confirmed by the V T roll-off behaviour with V Gb : the quantum V T roll-off is higher for V Gb = -0.6 V than for V Gb = 0 V, because in the first case, the transverse electric field is larger, leading to a significant quantum confinement. The charge centroid is moved towards the back interface and the control of SCEs is more difficult 3,21) for V Gb = -0.6

V than for V Gb = 0 V. In this latter case, the quantum confinement is notably reduced and the charge centroid is near the front interface. When T Si is reduced (e.g., T Si = 3 nm), the V T rolloff strongly decreases for all V Gb and in both the classical and quantum cases, owing to better control by the front gate of the electrostatic potential in the channel. The comparison between the quantum and classical simulations in Fig. 5 shows that, although SCEs are reduced when silicon film is thinned, quantum confinement markedly degrades the SCE immunity of IDG MOSFETs.

For short-channel devices (e.g., L = 20 nm), it is important to study the impact of quantum mechanical effects on the DIBL effect [calculated as

[V T (V D = 0.1 V) -V T (V D = 1.0V)]/∆V D ].
In Fig. 6, DIBL is plotted as a function of V Gb in both the classical and quantum cases and compared with DIBL in DG MOSFETs. This figure confirms that quantum confinement is more important in IDG MOSFETs than in DG MOSFETs. Our results show that for a V Gb less than about 0.2 V, DIBL in an IDG MOSFET is weaker than that in a DG MOSFET for the classical simulation, whereas, for the quantum simulation, DIBL in a DG MOSFET is always weaker than that in an IDG MOSFET. Similarly to V T roll-off, this is due to the effect of quantum confinement on the charge centroid that is pushed towards the back interface and makes the SCE control more difficult 3,21) . This result illustrates the difference in electrical behaviour between DG and IDG MOSFETs, particularly for short-channel devices.

The effect of quantum confinement, i.e., carrier-energy quantization, can be particularly well illustrated by plotting the difference between the quantum threshold voltage and the classical threshold voltage (∆V Tq ) as a function of V Gb [Fig. 7(a)] and T Si [Fig. 7(b)]. To better understand the effect of V Gb variation on quantum confinement, the transverse electric field as a function of V Gb is shown in Fig. 8 for L = 50 nm and three silicon film thicknesses in the quantum case. The transverse electric field is calculated using eq. ( 5), where V Gf is used under the threshold voltage conditions (V Gf = V T with V D = 0.1 V). We can firstly note that when the transverse electric field is minimum in the structure (for V Gb approximately 0.4 V),

∆V Tq is minimum. When V Gb moves away from this value and decreases towards a negative value or increases above 0.4 V, the transverse electric field increases and quantum confinement is enhanced (then ∆V Tq increases). Furthermore, when T Si is reduced, the quantum confinement is negligible for T Si > 5 nm, in IDG MOSFETs quantum confinement cannot be neglected even for thick films (T Si > 10 nm, depending on V Gb ). For negative V Gb , quantum confinement is significant even for T Si > 15 nm. These results show that quantum effects must be considered in the modeling of IDG MOSFET operation not only for thin films, but also for relatively thick silicon films, for which quantum confinement can be neglected in DG MOSFET operation.

Finally, the last parameter extracted from the I DS (V Gf ) characteristics is the subthreshold swing. Figure 9(a) shows the subthreshold swing as a function of V Gb in both the classical and quantum simulations for IDG and DG MOSFETs with T Si = 10 nm and L = 50 nm. The variation in S for a V Gb higher than 0.2 V is not shown, because S is very large (for example, if V Gb = 0.4 V, S > 140 mV/dec) owing to SCEs and the device cannot be used under these bias conditions. The subthreshold slope is higher in the IDG MOSFET than in the DG MOSFET. The DG MOSFET has a nearly ideal subthreshold slope (S = 62mV/dec), while the best (minimum) subthreshold swing in the IDG MOSFET is 76mV/dec in the classical simulation. This value increases with V Gb owing to a strong electron accumulation near the back gate. The quantum mechanical effects also modify this parameter in IDG MOSFETs due to the shift of the charge centroid away from the front interface, which enhances the SCEs. Since the reduction in T Si does not significantly affect the subthreshold swing in DG MOSFETs, in IDG MOSFETs, the subthreshold swing is enhanced in both the classical and quantum cases for V Gb = 0 V. The difference between the classical and quantum simulations is quasi constant but not negligible (~15 -20 mV/dec).

Conclusions

In this study, short-channel effects and quantum confinement in IDG MOSFET devices have been investigated using a 2D numerical simulation code that calculates the drain current.

The main electrical parameters of IDG MOSFETs (threshold voltage, V T roll-off, ∆V Tq , and subthreshold swing) have been compared with those of DG MOSFETs for different gate lengths and silicon film thicknesses. The results show that the electrical operation of IDG MOSFETs differs from that of DG MOSFETs owing to the presence of an important transverse electric field in the first structure. This transverse electric field significantly modifies the quantum well shape and leads to the occurrence of electric-field-induced quantum confinement in IDG MOSFETs, in addition to T Si -induced structural quantum confinement. This phenomenon leads to subthreshold performance degradation and to the enhancement of SCEs in IDG MOSFETs compared with DG MOSFETs. This study shows that in IDG MOSFETs, quantum effects can be important even for T Si > 10 -15 nm (depending on V Gb ), while in DG MOSFETs quantum confinement is negligible for T Si > 5

Structure definition

Classical simulation

Poisson: [ ] ( )

V V ρ - = ∇ ε ∇ Quantum simulation Poisson: [ ] ( ) V V ρ - = ∇ ε ∇ Schrödinger: Ψ =       Ψ ∇ ∇ - E m 1 2

I DS

Yes

  Figure 2(b) shows that the effects of quantum mechanical confinement are more important in IDG MOSFETs than in DG MOSFETs. The explanation is that carriers are confined in a triangular quantum well in IDG MOSFETs and not in a rectangular quantum well, as is the case in DG MOSFETs. Therefore, in IDG MOSFETs, carriers are subjected to electric-field-induced quantum confinement, in addition to T Siinduced structural confinement. In DG MOSFETs, the transverse electric field is very weak (E xC ~ 0 V/m) and quantum effects are predominantly due to structural quantum confinement.

  transverse electric field further increases and ∆V Tq strongly increases with the reduction in T Si [as shown in Figs. 7(a) and 7(b)]. For comparison, Fig. 7(b) also shows ∆V Tq variation as a function of T Si in the DG MOSFET: in this case, ∆V Tq is almost negligible for T Si > 5 nm owing to the weak structural quantum confinement in thick films. This figure confirms that quantum confinement is less important in DG MOSFETs than in IDG MOSFETs, where both T Si -induced structural and electric-field-induced quantum confinements occur. The main conclusion drawn from Fig. 7(b) is that while in DG MOSFETs one can consider that

Figure 9 (

 9 Figure 9(b) shows the effect of T Si on the subthreshold swing in IDG and DG MOSFETs.

Figure 1 .

 1 Figure 1. (a) Schematic view of simulated IDG MOSFET. The main device electrical and

Figure 2 .

 2 Figure 2. Impact of quantum-mechanical effects on drain current of n-channel IDG MOSFET:

Figure 3 .

 3 Figure 3. Impact of SCEs and quantum confinement on threshold voltage as function of back

Figure 4 .

 4 Figure 4. Threshold voltage versus silicon film thickness in classical and quantum cases for

Figure 5 .

 5 Figure 5. Comparison between V T roll-off in quantum and classical cases versus silicon film

Figure 6 .

 6 Figure 6. Quantum and classical simulations of IDG MOSFET DIBL versus back gate bias for

Figure 7 .

 7 Figure 7. Difference between threshold voltages calculated in classical and quantum

Figure 8 .

 8 Figure 8. Transverse electric field in L = 50 nm n-channel IDG MOSFET in quantum

Figure 9 (

 9 Figure 9 (a) Subthreshold swing as function of back gate voltage in classical and quantum

Figure 1 .

 1 Figure 1. Moreau et al.

Figure 2 .Figure 3 .Figure 4 .Figure 5 .

 2345 Figure 2. Moreau et al.

Figure 6 .

 6 Figure 6. Moreau et al.

Figure 7 .Figure 8 .

 78 Figure 7. Moreau et al.

Figure 9 .

 9 Figure 9. Moreau et al.

nm. We demonstrate that quantum confinement must be taken into account in the modeling of IDG MOSFETs, not only for thin silicon films but also for relatively thick silicon films, for which quantum confinement can be neglected in DG MOSFET operation.

Acknowledgements

The authors would like to thank X. Loussier from IM2NP, Marseille, France, for providing Atlas numerical simulation data. This work was supported by the French Ministry of Research (ANR PNANO project "MULTIGRILLES").


Pierre Vial

Every λ-Term is Meaningful for the Infinitary Relational Model

Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto-autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every λ-term. However, these observations do not say much about what coinductive (i.e. infinitary) type grammars are able to provide: it is for instance very difficult to know what types (besides R) can be assigned to a given term in this setting. We begin with a discussion on the expressivity of different forms of infinite types. Then, using the resource-awareness of sequential intersection types (system S) and tracking, we prove that infinite types are able to characterize the arity of every λ-terms and that, in the infinitary extension of the relational model, every term has a "meaning" i.e. a non-empty denotation. From the technical point of view, we must deal with the total lack of guarantee of productivity for typable terms: we do so by importing methods inspired by first order model theory.

1 Introduction (Infinite types)

Some semantical aspects of infinite types

It is well-known that the mere fact of allowing infinite formulas gives birth to unsound/contradictory proof systems. For instance, let A be any formula. We then define the infinite formula F A by F A := (((. . .) → A) → A) → A i.e. F A = F A → A (the letter "F" stands for "fixpoint"). The formula F A gives rise both to a proof of A and-via the Curry-Howard correspondence-to the typing of a term with A, this term being no other than the auto-autoapplication Ω := ∆ ∆ (with ∆ = λx.x x). This is given by Fig. 1.

Thus, every type A is inhabited by Ω. But given a λ-term t, what types A does t inhabit? A first observation is that every λ-term can easily be typed: let ax x : F A x : F A ax x : F A x : F A app x : F A x x : A abs λx.x x : F A → A ax x : F A x : F A ax x : F A x : F A app x : F A x x : A abs λx.x x : F A app Ω : A Figure 1: Typing Ω,inferring A us just define R (standing for "reflexive") by R = R → R. Thus, R = (R → R) → (R → R) = . . . Then, it is very easy to type every term with R. In the inductive steps below, Γ denotes a context that assigns R to every variable of its domain: Γ; x:R x:R Γ; x:R t:R Γ λx.t:R→R (= R) Γ t:R (=R→R) Γ u:R Γ t u : R Therefore, every λ-term inhabits the type R. Yet, this does not answer the former question: what types does a term t inhabit? As we will see, this question has no simple answer and we will chiefly focus on one aspect of this problem, namely, the typing constraints caused by the arity of the λ-terms. Intuitively, the arity of a λ-term t (sometimes called its order e.g., in [START_REF] Bucciarelli | Graph easy sets of mute lambda terms[END_REF]) is the supremal n such that t → * β λx 1 . . . x n .u (for some term u) i.e. the number of abstractions that one can output from t. For instance, the arity Ω of 0 (it is a zero term), the arity of the head normal form (HNF) λx 1 x 2 .x u 1 u 2 u 3 (with u 1 , u 2 , u 3 terms) is 2 and the term Y λ := (λx.λy.xx)λx.λy.xx has an infinite arity, because Y λ → n β λy 1 . . . λy n .Y λ . The arity of a type is the number of its top-level arrows e.g., if o 1 , o 2 are type atoms (or type variables), o 1 → o 1 , o 1 , o 1 → o 2 → o 1 and (o 1 → o 2 ) → o 1 are of respective arities 1, 0, 2, 1. Via Curry-Howard, the constructor λx corresponds to the introduction of an implication, and so, in most type systems, a typed term of the form λx 1 . . . x n .u is typed with an arrow of arity n. For instance, if λx.λy.u is typed, then it is so with a type of the form A → B → C.

Moreover, if a type system satisfies subject reduction, meaning that typing is stable under reduction, the above observation entails that, if a typable term is of arity n, then it is typable only with types of arity n (the arity of a term is a lower bound for the arity of its possible types). Equivalently, if t is typed with B, then the arity of B statically gives an upper bound to the arity of t (static meaning without reduction). A finite type has a finite arity (whereas the finite term Y λ has an infinite arity). Yet, unsurprisingly, an infinite type may have an infinite arity e.g., R defined by R = R → R above. This confirms that the typing of any term t with R is trivial and does not bring any information, since the arity of a term is of course ∞. However, the facts that, by allowing infinite types, (1) one can type every term with R = R → R and (2) one can type Ω with any type A, do not mean that finding the types that can be assigned to a given term t is an easy problem in this setting.

Intersection Types and Arity

We have just seen that subject reduction naturally ensures that simple typing provides an upper bound to the arity of a typed term. Intersection type systems (i.t.s.), introduced by Coppo-Dezani [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF], generally satisfy subject expansion, meaning that typing is stable under anti-reduction. Those systems feature a type constructor ∧ (intersection) and are designed to ensure equivalences of the form "t is typable iff t is normalizing" and also provide semantical proofs of non-type-theoretic properties such as "t is weakly normalizing iff the leftmostoutermost reduction strategy terminates on t" [START_REF] Krivine | Lambda-calculus, types and models. Ellis Horwood series in computers and their applications[END_REF]. From subject expansion and the typing of normal forms (NF) i.e. terminal states, i.t.s. are actually able to capture the arity of some λ-terms. For instance, if an i.t.s. characterizes head normalization (HN), then, every HN term t of arity p is typable with a type whose arity is also equal to p (and not only bounded below by p).

Let us informally explain why and how the arity of the typable terms is usually captured by i.t.s. For instance, i.t.s. characterizing HN usually feature arrow types having an empty source 1 (that we generically denote by ∅), meaning that the underlying functions do not look at their argument. Namely, if t : ∅ → B, then t u is typable with B for any term u. This allows us to easily type any HNF while capturing its arity: in Fig. 2, one just assigns ∅ → . . . → ∅ → o (arity q) to the head variable x, so that x t 1 . . . t q is typed with the type atom o and the HNF λx 1 . . . x p .x t 1 . . . t q , whose arity is p, is typed with an arrow type of arity p. Then, by subject expansion, one concludes that every HN term of arity p is typable with a type of arity p. The same argument can be adapted to i.t.s. characterizing weak (including infinitary weak) or strong normalization, which also usually capture the arity of their typable terms.

In Search for Infinite Denotations

Independently from normalization properties, another important facet of i.t.s. is that they also provide denotational models for the λ-calculus i.e. they associate to each λ-term a denotation

[[t]] (usually, [[t]] is a morphism in a category), meaning that [[t]] is invariant under β-conversion (i.e. t 1 = β t 2 implies [[t 1 ]] = [[t 2 ]]
). For instance, the typing judgments of Gardner-de Carvalho's system R 0 (that we will shortly discuss in § 2.1) correspond to the points of the relational model [START_REF] Bucciarelli | Not enough points is enough[END_REF]: indeed, {£ R0 Γ t : τ | Γ, τ } = [[t]] rel for any term t, where the left-hand side corresponds to the set of derivable judgments of system R 0 typing t and the right-hand side, the denotation of t in the relational model. Thus, infinite types are a mean to study the infinitary extension of the relational model.

The (finitary) relational model only gives a (non-empty) denotation to HN terms. This reflects the fact that non-HN (equivalently, unsolvable) terms have an infinitary behavior w.r.t. head reduction. In this regard, it is natural to seek whether such terms have an infinitary semantics, since infinitary models bring information on asymptotic aspects of terms e.g., in the recent work of Grellois-Melliès [START_REF] Grellois | An infinitary model of linear logic[END_REF][START_REF] Grellois | Relational semantics of linear logic and higherorder model checking[END_REF]. The first main contribution of this article is to prove that every term has a non-empty interpretation in the infinitary relational model M rel . This furthers the approach of Curry, aiming at finding more and more "meanings" to λ-terms (see e.g., [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF] or § 5.4. on "illative systems" in [START_REF] Cardone | Lambda-Calculus and Combinators in the 20th Century[END_REF]). One may thus consider that, in M rel , every λ-term is meaningful (although we do not have yet a deep understanding of this model, beyond arity-related aspects).

An interesting aspect of models is that they allow us to statically discriminate terms from one another, meaning that if

[[t 1 ]] = [[t 2 ]] then t 1 = β t 2 i.
e. two terms that do not have the same denotation do not represent two different states of a same program. For instance, the i.t.s. that are able to assign a type of arity n to any (e.g., HN) term of arity n (but not to one of arity n + 1) can be regarded as arity-discriminating for HN terms. This holds for system R 0 . We prove that the infinitary extension of system R 0 , that we denote R, is arity-discriminating for all λ-terms (not just the HN ones). This second main contribution of the paper (Theorem. 2) extends a feature of system R 0 concerning HN terms to the whole λ-calculus.

Stability and the Difficulty of Infinitary Typing

We saw above how i.t.s. capture the arity of the typed terms in finite/productive case (productive cases include infinitary normalizing terms). Let us now understand why the method of § 1.2 fails while studying full infinitary typing. Fig. 2 shows well that typing in a given i.t.s. (and in particular, capturing the arity) reduces to typing the "partial" normal forms (e.g., HNF or β-NF). Intuitively, the nodes corresponding to the normalized parts of a term cannot be affected by reduction e.g., the nodes labelled with λx i , @ and x in Fig. 2 (the "spine" of the HNF). Such nodes are stable. In contrast, some terms (the so-called mute terms [START_REF] Berarducci | Some new results on easy lambda-terms[END_REF]) do not ever give rise to stable positions and are thus totally unproductive e.g., the term Ω.

Thus, there is no clear way to capture the arity of any typable term: the example of Ω shows that the case of totally unstabilizable term must be handled when considering infinite types. Note that Ω is just an example of a mute term, that happens to satisfy the nice fixpoint equation Ω → β Ω and has a simple parsing tree. This partially explains why Ω was easily typable. In general, there is no method to type generic mute terms that do not satisfy an equation.

Infinitary Typing and Klop's Problem

Let us say a few words about the questions raised by infinitary typing in the non-idempotent intersection type framework i.e. by the interpretation of terms in the infinitary relational model.

• One of the fundamental interests of non-idempotent intersection (A∧A = A) is that, in this setting, a type is a resource that cannot be duplicated or merged/contracted and that is possibly consumed under reduction.

• Moreover, non-idempotent i.t.s. are often relevant, meaning that weakening is not allowed.

An i.t.s. that forbids duplication and weakening can be qualified as linear, which is the case of system R 0 that we hinted at in § 1.3, and its infinitary version R.

As we will see in § 2.1, relevance disables the argument proving that every term is typable with ρ, the non-idempotent counterpart of the type R considered above. However, while trying to characterize a form of infinitary weak normalization, we noticed in [START_REF] Vial | Infinitary intersection types as sequences: A new answer to Klop's problem[END_REF] that Ω is also typable in R. We recovered soundness by defining a validity criterion, discarding degenerate typing derivations, which was possible by introducing a rigid variant of system R, namely system S. System S has many nice features e.g., tracking (motivated in § 2.2). Still, these observations raise the problem of characterizing the set of typable terms (without validity criterion) in the coinductive relevant and non-idempotent framework. In particular, is every term R-typable? Or is there a term t that is not R-typable? Observe that such a term t would not be linearizable, even in an infinite way (since a R/S-derivation typing t induces a linear representation of t). The existence of non-linearizable terms would be very surprising. Therefore, it must be investigated. Since our main theorem (Theorem 1) states that system R actually types every term, we actually prove that every term is linearizable, as expected.

Note again that the method described at the end of § 1.2 does not work for non-normal terms: naively, when x u occurs in t, we would like to assign to x a type of the form A → B, where A is the type of u, and proceed by induction. However, x may be substituted in the course of a reduction sequence, and so, typing constraints on x are not easily readable. Thus, in the productive case, in the purpose of proving that the terms of a given set (e.g., the set of HN terms above) are typable, we escape this problem by typing normal forms (e.g., HNF) and then proceeding by expansion. But, by § 1.4, this cannot work when we want to type every term.

To sum up, due to full resource-awareness (including relevance), typing in the coinductive systems R and S is intrinsically non-trivial. But the same reason (full resource-awareness) make linear intersection type systems the good framework to study the expressive power of infinite types and to capture the arity of every λ-term. Thus, besides our first goal. . . Goal 1. Capturing the arity of every λ-term with infinite types.

. . . we have now a second one, narrowly related to the first: Goal 2. Proving that every term is R-typable.

A Technical Contribution

We have not addressed yet the way we can study unproductive/mute terms, despite the fact that all the known techniques of intersection type theory fail: we propose a solution to overcome this difficulty, inspired by (a simplified form of) first order model theory, that we mix with techniques specific to the λ-calculus. This is our main technical innovation, since it enables the study of unproductive reduction. Thus, beyond the relational model, this work proposes the first use of first order model theory to study an infinitary extension of a finitary model of the λ-calculus and to generalize properties coming from the finite model to every λ-term (e.g., capturing their arity). The proof that every term is R-typable has three main stages: [START_REF] Barendregt | The Lambda-Calculus: Its Syntax and Sematics. Ellis Horwood series in computers and their applications[END_REF] reducing the problem to a set of stability relations ( § 3) (2) describing the possible interactions between these relations ( § 4.2) (3) describing a procedure of partial (but more importantly finite) normalization ( § 5). The same ingredients allow us to capture the arity. The italicized words, as well as the tools of the proof and how they arise, are gradually explained in the paper but we refer to § 3.1, 3.2 and the introduction of § 4 for some high-level input.

Outline

To sum up, our main contributions in this article consist of (1) proving that every term has a non-empty denotation in the infinitary relational model (2) the arity of terms can be captured by infinitary type systems (3) introducing a method giving rise to semantic descriptions of λ-terms, whether they normalize or not.

In § 2, we present two non-idempotent i.t.s. and the notions of relevance and tracking. In § 3, we explain why describing the "form" of the derivations in system S (presented in § 2.2) may help us to prove that every term is S-typable and we characterize these forms. The key notion of thread is defined. In § 4, we define, for a given term t, a nihilating chain as a proof that t is not S-typable. Proving that every term is typable reduces to proving that nihilating chains do not exist (Prop. 2). We prove that, under a positivity condition involving threads, nihilating chains indeed do not exist (Prop. 3). In § 5, we prove that the positivity condition can be assumed without loss of generality, by means of a finite normalization procedure. Thus, no proof of untypability exists and every term is typable. We conclude in § 6 by notably sketching the adaptation of the previous steps giving the expected type-theoretic arity-capture.

Infinitary Relevant and Non-Idempotent Intersection 2.1 System R

We now define more formally system R, the coinductive version of the finite system R 0 , independently introduced by Gardner and de Carvalho [START_REF] Gardner | Discovering needed reductions using type theory[END_REF][START_REF] Carvalho | Sémantique de la logique linéaire et temps de calcul[END_REF]. See [START_REF] Bucciarelli | Non-idempotent intersection types for the lambda-calculus[END_REF] for a general presentation of R 0 . System R is of good help to understand relevant intersectionbut, as we shall see in § 2.2 and 3.1, it is unfit to express the techniques yielding Theorems 1 and 2, and we refer to it only for heuristic purposes.

The set of R-types is coinductively defined by.

σ, τ ::= o ∈ O | [σ i ] i∈I → τ
We call I := [σ i ] i∈I a multiset type. The multiset types represent intersection in system R 0 and the intersection operator ∧ is the multiset-theoretic sum:

∧ i∈I I i = + i∈I I i (i.e. ∧ i∈I [σ i j ] j∈J(i) := + i∈I [σ i j ] j∈J(i)
). We assume I to be countable, the empty multiset type is denoted by [ ] and [σ]

ω := [σ i ] i∈ω with ∀i ∈ ω, σ i = σ.
An R-context (metavariables Γ, ∆) is a total function from V (the set of term variables) to the set of multiset types. The domain of Γ is given by {x | Γ(x) = [ ]}. The intersection of contexts + i∈I Γ i is defined point-wise. We may write Γ; ∆ instead of Γ+∆ when dom(Γ)∩dom(∆) = ∅. Given a multiset type [σ i ] i∈I , we write x : [σ i ] i∈I for the context Γ s.t. Γ(x) = [σ i ] i∈I and Γ(y) = [ ] for all y = x. An R-judgment is a triple Γ t : σ where Γ is an R-context, t a term and σ an R-type.

The set of R-derivations is defined inductively by:

ax x : [τ ] x : τ Γ; x : [σ i ] i∈I t : τ abs Γ λx.t : [σ i ] i∈I → τ Γ t : [σ i ] i∈I → τ (∆ i u : σ i ) i∈I app Γ + (+ i∈I ∆ i ) t u : τ
As announced in § 1.5, system R is not only non-idempotent, but also relevant. For instance, the K-term λx.y can only be assigned types of the form [ ] → τ . Indeed, λx.y can only by typed by:

ax x : [τ ] x : τ abs x : [τ ] λy.x : [ ] → τ
This comes from the fact that y does not occur in x, and thus, by relevance, the constructor λy cannot invoke a (non-empty) type on the left-hand side of the arrow type.

Fig. 1 can adapted and we can type Ω with τ for all R-types τ , by just defining φ τ by φ τ = [φ τ ] ω → τ . However, defining ρ by ρ = [ρ] ω → ρ does not allow us to type every term with ρ in system R.

To understand why, note first that relevance can be disabled, by replacing ax par ax w :

i 0 ∈ I ax w Γ; x : [σ i ] i∈I x : σ i0
We call R w the type system thus obtained. Then, the proof on p. 2 can be adapted to R w , by considering only contexts Γ, Γ t , Γ u assigning [ρ] ω to all the variables in their domains:

ax x:[ρ] ω x:ρ Γ; x : [ρ] ω t:ρ abs Γ λx.t : ρ Γ t t:ρ (Γ u u:ρ) ω app Γ t + Γ u t u : ρ
Thus, every term is R w -typable. But note that, by relevance, this proof by induction on the structure of t fails for R. For instance, if x is not in t, Γ t : ρ yields Γ λx.t : [ ] → ρ ( = ρ!) and since the empty multiset type may occur in unpredictable places in a term, finding an R-typing of any term t is non-trivial.

In some sense, R-typability is about capturing the way relevance constrains emptiness to occur! But since a variable x can be substituted under reduction as observed in § 1.5, [ ] may occur in unpredictable places.

Towards Tracking and Sequential Intersection

Unfortunately, resource-awareness of system R is not enough to process the proof techniques to be developed here: we also need tracking. Let us just give an example to show what the impossibility of tracking means:

ax x : [[σ, σ]→τ ] x : [σ, σ]→τ ax x : [σ] x : σ ax x : [σ] x : σ app x : [[σ, σ] → τ, σ, σ] x x : τ
In this derivation, in the context x : [[σ] → τ, σ, σ] of the conclusion, one cannot know which particular axiom rule, each red occurrence of σ comes from: there is no possible notion of pointer with multiset intersections, which is one thing that we absolutely need to capture the key notion of support candidate in § 3.1.

Tracking can be retrieved while keeping most of system R 0 's nice features (e.g., syntax-direction) by considering system S, that we introduced in [START_REF] Vial | Infinitary intersection types as sequences: A new answer to Klop's problem[END_REF]. System S uses sequence types instead of multiset types to represent intersection. For instance, instead of having a cardinal Formally, the set of S-types is defined coinductively by:

3 intersection [o, o , o], system S considers a cardinal 3 sequence (2 • o, 5 • o , 8 • o). Sequences come along with a disjoint union operator e.g., (2 • o, 5 • o , 8 • o) = (2 • o, 5 • o ) (8 • o): in this
T, S k ::= o F → T F ::= (k • S k ) k∈K (K ⊆ N \ {0, 1})
The empty sequence type is denoted ( ) and we often write (S k ) k∈K instead of (k •S k ) k∈K . The set of top-level tracks of a sequence type is called its set of roots and we write e.g., Rt(F ) = {2, 5, 8} when F = (2 • S, 5 • S , 8 • S). Note that the disjoint union operator can lead to track conflict e.g., , if

F 1 = (2 • o, 3 • o ) and F 2 = (3•o , 8•o), the union F 1 F 2 is not defined, since Rt(F 1 )∩Rt(F 2 ) = {3} = ∅.
An S-context C (or D) is a total function from V to the set of S-types. The operator is extended point-wise. An S-judgment is a triple C t : T , where C, t and T are respectively an S-context, a term and T an S-type. A sequence judgment is a family of judgments (k

• (D k u : S k )) k∈K (with K ⊆ N \ {0, 1}
) that all type the same term u, often just written (D k u : S k ) k∈K . For instance, if 5 ∈ K, then the judgment on track 5 is C 5 u : S 5 .

The set of S-derivations is defined inductively by:

x : (k • T ) x : T ax C; x : (S k ) k∈K t : T C λx.t : (S k ) k∈K → T abs C t : (S k ) k∈K → T (D k u : S k ) k∈K C ( k∈K D k ) t u : T app
The app-rule can be applied only if there is no track conflict in the context C ( k∈K D k ). In an ax-rule concluding with x : (k • T ) x : T , the track k is called the axiom track of this axiom rule. We refer to § III and IV of [START_REF] Vial | Infinitary intersection types as sequences: A new answer to Klop's problem[END_REF] for additional examples and figures for all what concerns the basics of system S sketched here and thereafter.

Let

S ex = (2 • o, 7 • o ) → o .
To gain space, we write k x : T (with k 2, x ∈ V , T S-type) instead of x : (k • T ) x : T in ax-rules. We also indicate the track of argument derivations between square brackets e.g., x : (3 • o) [START_REF] Bucciarelli | Not enough points is enough[END_REF] means that the argument judgment x : (3 • o) x : o is on track 5):

ax 3 y : S ex ax 3 x : o [5] ax 9 x : o [6] app x : (3 • o, 9 • o ), y : (3•S ex ) y x : o ax y : (3 • (2 • o, 7 • o ) → o ) λx.y x : (3 • o, 9 • o ) → o
As expected: Property 1. Systems S and R enjoy subject reduction and expansion If tracks are erased, a sequence becomes a multiset and S-derivations collapse on R-derivations (e.g., P ex on P ex ), so that an S-typable term is also R-typable. We may thus replace Goal 2 by Goal 3.

Goal 3. Proving that every term is S-typable.

We reduce the problem (i.e. proving that a term t is typable in system S) into a first order theory, that we call T t . We actually prove that T t indeed captures the problem, by means of a proposition that can be interpreted as a (simplified) completeness theorem (see Corollary 1): we show that if T t is coherent, then t is S-typable. Then we prove that T t is coherent for all terms t. Go to the introduction of § 3.2 and 4 to have a closer descriptions of the proof of the coherence of T t and of its main stages.

Parsing, Pointing

In this technical section, we explain how we may point inside an S-type or an S-derivation, thanks to tracking. We define the support of an S-type and an S-derivation, and also the key notions of biposition and bisupports. Let N * denote the set of the finite words on N, the operator • denotes concatenation, ε the empty word and the prefix order e.g., 2

• 1 • 3 • 7 ∈ N * , 2 • 1 2 • 1 • 3 • 7.
Moreover, the collapse k of a track k is defined by k = min(k, 2). This notation is extended letter-wise on N * e.g., 0

•5•1•3•2 = 0•2•1•2•2. The support of term is defined by induction as expected: supp(x) = {ε}, supp(λx.t) = {ε} ∪ 0 • supp(t) and supp(t u) = {ε} ∪ 1 • supp(t) ∪ 2 • supp(u). If a ∈ N *
and a ∈ supp(t), we denote by t| a the subterm of t rooted at position a whereas t(a) is the constructor (@, x or λx) of t at position a e.g., t| 0 = y x and t(0 • 1) = y with t = λx.y x.

The support of a type (resp. a sequence type), which is a tree of N * (resp. a forest), is defined by mutual coinduction:

supp(o) = {ε}, supp(F → T ) = {ε} ∪ supp(F ) ∪ 1 • supp(T ) and supp((T k ) k∈K ) = ∪ k∈K k • supp(T k ) e.g.
, supp(S ex ) = {ε, 1, 2, 7}. We can define the support of a derivation P £C t : T : supp(P ) = ε if P is an axiom rule, supp(P ) = {ε} ∪ 0 • supp(P 0 ) if t = λx.t 0 and P 0 is the subderivation typing t 0 , supp(P ) = {ε} ∪ 1 • supp(P 1 ) ∪ k∈K k • supp(P k ) if t = t 1 t 2 , P 1 is the left subderivation typing t 1 and P k the subderivation typing t 2 on track k. The P k (k ∈ K) are called argument derivations. For instance, supp(P ex ) = {ε, 0, 0•1, 0•5, 0•6}, P (0 • 1) = y : (3•S ex ) y : S ex and

P (0•6) = x : (9•o ) x : o .
Choice function for axiom tracks: Note that, to define an S-derivation typing a term t (thus fulfilling Goal 3), one must one choose an axiom track in every axiom rule so that no conflict arise. In this short article, let us just say that we can escape this problem by resorting to an arbitrary injection from N * to N \ {0, 1}, that chooses axiom tracks for us: we say that an S-derivation P is a • -derivation if P (a) = (x : (k • T ) x : T ) (i.e. a is the position of an ax-rule typing x in P ), then k = a . If t is • -typable, then t is in particular S-typable, so that we now replace Goal 3 with Goal 4: Goal 4. Given an injection • : N * → N \ {0, 1}, proving that every term is

• -typable.

The injectivity hypothesis allows us to stop bothering about track conflict any further while achieving Goal 4. It is also w.r.t. the function • that we will capture where emptiness occurs (see § 3.2).

We explain now how to point inside types nested in S-derivations, or to axioms typing a given variable, and formalize the associated pointers. If P is an S-derivation and a ∈ supp(P ), then the judgment at position a is denoted C P (a) t| a : T P (a) e.g., C Pex (0 • 6) = x : (9 • o ) and T Pex (0 • 6) = o . Let P be an S-derivation. A right biposition is a pair of the form (a, c), where a ∈ supp(P ) and c ∈ supp(T P (a)), we write bisupp(P ) for the (right) bisupport of P i.e. its set of (right) bipositions. If (a, c) ∈ bisupp(P ), then P (a, c) denotes T P (a, c) e.g., P ex (0•6, ε) = o and P ex (0

• 1, ε) = o, P ex (0 • 1, 1) = o and P ex (ε, 9) = o .
Note that, contrary to [START_REF] Vial | Infinitary intersection types as sequences: A new answer to Klop's problem[END_REF], we only consider right bipositions. For this article, we think a biposition as type symbol (o ∈ O or →) nested in a given S-derivation P and we often use this heuristic identification implicitly, most notably when describing Fig. 4.

Assume that P types t. We set A = supp(P ) and B = bisupp(P ). If x ∈ V , a ∈ A, we set Ax P a (x) = {a 0 ∈ A | a a 0 , t(a) = x, a 0 , a a 0 a 0 , t(a 0 ) = λx} (occurrences of x in P above a, that are not bound w.r.t. a) e.g., Ax Pex ε (x) = ∅ (x is bound at the root), but Ax Pex 0 (x) = {0 • 5, 0 • 6} (x is not bound at position 0). Technically, this notation is crucial to harness relevance (see polar inversion, § 3.3) but the important thing to remember is that, thanks to tracking, in system S, one can unambiguously designate the axiom rules typing the variable of a λx.

Typing some Notable Terms in System R

We now use system R to type a few terms satisfying fixpoint equations. Some of them are not head normalizing.

Let ∆ f = λx.f (x x), Y = λf.∆ f ∆ f (Y is Curry fixpoint combinator ). Moreover, if I = λx.x and K = λxy.x, then Y I → Ω (satisfying Ω → β Ω), Y f → Y f := ∆ f ∆ f (satisfying Y f → β f (Y f )) and Y K → β Y λ := (λx.λy.xx)λx.λy.xx (satisfying Y λ → β λy.Y λ ).
Iterating reduction on Y f and Y λ infinitely many times, we see that Y f (resp. Y λ ) strongly converges to the infinitary term f ω := f (f (...)) (resp. λy.λy....) in the sense of [START_REF] Kennaway | Infinitary lambda calculus[END_REF][START_REF] Czajka | A coinductive confluence proof for infinitary lambda-calculus[END_REF]. Thus, Ω and Y f are both zero terms ( § 1.1) and Y λ a term of infinite arity. The term Ω is actually a mute term (see § 1.4) and Y f is a term whose Böhm tree (see [START_REF] Barendregt | The Lambda-Calculus: Its Syntax and Sematics. Ellis Horwood series in computers and their applications[END_REF], chapter 10) f ω does not contain ⊥.

Because of rule abs and subject reduction, a term of arity n may only be typed with a type of arity n, as explained in § 1.1. However, some R-derivations can capture more precisely the arity of terms. For each R-type τ , we define coinductively φ τ by φ τ = [φ τ ] ω → τ . For instance, we consider the following typing of Y (omitting left-hand sides of ax-rules):

Π ∆ f = ax f : [τ ] → τ ax x : φ τ ax x : φ τ ω app x : [φ τ ] ω x x : τ app f : [[τ ] → τ ]; x : [φ τ ] ω f (x x) : τ abs f : [[τ ] → τ ] ∆ f : φ τ (= [φ τ ] ω → τ ) Π Y = Π ∆ f (Π ∆ f ) ω app f : [[τ ] → τ ] ω ∆ f ∆ f : τ abs Y : [[τ ] → τ ] ω → τ Thus, Y is R-typable with [[τ ] → τ ] ω → τ for any type τ .
Using suitable instances or variants of Π Y , we can build Π Ω £ Ω : τ (for any τ ) and Π λ £ Y λ : [ ] → [ ] → . . . By instantiating τ with a type variable o, we get Ω : o and Y f : o. Thus, the zero terms Ω and Y f are typed2 with types of arity 0 whereas Y λ (whose arity is infinite) is typed with a type of infinite arity, as it was constrained to be.

We will generalize this result (not only for terms built from a fixpoint combinator like Ω or λx.Ω) and show that, for all pure terms t of arity n, there is an R-derivation typing t with a type of arity n (Theorem 2).

Bisupport Candidates

In this section, we characterize, for a given term t, its bisupport candidates i.e. the (potential) forms of the derivations typing t. By "form", we intuitively mean a set of unlabelled positions (that must be stable under some suitable relations). We make explicit that idea by studying first the possible forms of an S-type in § 3.1. The notion of unlabelled position has a meaning only because tracks of S allow us to define suitable pointers. It would be impossible in system R.

A Toy Example: Support Candidates for Types

In this section, we explain how the notion of "form" of a support can be formalized by giving a characterization of the supports of S-types in terms of stability conditions. The definition of a particular S-type T can be understood as a two-step process: first, we choose the support C := supp(T ), next, we choose the type labels T (c) (in the signature O ∪ {→}) given to the positions c ∈ C. However, not all the subsets C ⊆ N * are fit to be the support of a type, and not all the possible decorations of a suitable set C yield a correct type.

For instance, let us consider the two sets of positions C 1 and C 2 below. Do they define the supports of some types T 1 and T 2 ?

1 4 1 3 8 C 1 = {ε, 1, 4, 4•1, 4•3, 4•8} 1 4 3 C2 = {ε, 1, 4, 4•3}
As it turns out, C 1 is the support of a type e.g., (4

• (8 • o 3 , 3 • o 1 ) → o 2 ) → o 1 (figure below)
. By contrast, no type T may satisfy supp(T ) = C 2 , because a non-terminal node of a type (necessarily an arrow) should have a child on track 1 (by convention, its right-hand side), but 4 ∈ C 2 and 4

• 1 / ∈ C 2 . → 1 o 1 4 → 1 o 2 3 o 1 o 3 8 Type (4•(8•o3, 3•o1) → o2) → o1 o 1 o 1 4 → 1 → o 3 3 o 3 8 Wrong decoration
This motivates the following notion: a support candidate of type is a subset C ⊆ N * such that there exists a type T satisfying C = supp(T ). Given a support candidate C, it is easy to define a correct type whose support is C:

• The label of non-terminal nodes of C should be arrows.

• the leaves of C should be decorated with type atoms o ∈ O.

So was done for the decoration on the left-hand side, representing the type (4

• (8 • o 3 , 3 • o 1 ) → o 2 ) → o 1 .
In contrast, the decoration on the right-hand side is incorrect: ε (non-terminal) is labelled with ∈ O and 4 • 1 (leaf) with →.

The observations about C 1 and C 2 above suggest considering two relations → t1 and → t2 defined by:

• For all c ∈ N * , k ∈ N, c • k → t1 c. • For all c ∈ N * , k 2, c • k → t2 c • 1. A set of positions C is closed under → t1 (i.e. c 1 ∈ C and c 1 → t1 c 2 entails c 2 ∈ C)
iff it is a tree. Stability under condition → t2 means that if a node c is not terminal, then it has a child on track 1.

Lemma 1. Let C ⊆ N * . Then C is a type support candidate (i.e. there exists a type T s.t. C = supp(T )) iff C is non-empty and is closed under → t1 and → t2 .

Thus, relations → t1 and → t2 are enough to characterize support candidates. We call them stability relations e.g., the good candidate support C 1 is stable under → t1 and → t2 , whereas 4

• 3 ∈ C 2 , 4 • 3 → t2 4 • 1 but 4 • 1 / ∈ C 2 , so that the bad candidate support C 2 is not stable under → t2 .
When c 1 → t1 c 2 or c 1 → t2 c 2 , we say that c 1 subjugates c 2 , because c 1 demands c 2 to ensure a correct formation of the support.

Toward the Characterization of Bisupport Candidates

For the remainder of this paper, we fix an injection • : N * → N \ {0, 1}. By Goal 4, we want to prove that every term t is • -typable. By analogy with the notion of candidate supports for types (previous section), the idea is to characterize the bisupport candidates for the • -derivations typing a given term t i.e. sets B ⊆ N * ×N * s.t. there exists a • -derivation P typing t satisfying B = bisupp(P ) (Prop. 1 to come). We proceed by defining in § 3:

• B t , the set of the potential bipositions of a derivation typing a term t (in this Section 3.2).

• On B t , we define a relation → • (which is actually the union of 7 stability relations). More precisely:

-There is a special constant symbol p ⊥ in B t , that roughly indicates "untypability" or "emptiness".

-The term t is typable iff there is a non-empty subset B of B t , such that B is stable under → • and does not contain p ⊥ (compare this statement with Lemma 1). Such a B is the support of a derivation typing t. This equivalence is given by the "completeness-like" statement of Corollary 1.

Let us now define B t by first noticing that not every position a ∈ N * (or (a, c) ∈ N * × N * ) may be in a derivation typing a given term t. For instance, we have supp(λx.y x) = {ε, 0, 0 • 1, 0 • 2}, so, if P types λx.x x, then a ∈ supp(P ) implies a = ε, 0, 0 • 1 or 0 • 2 i.e. supp(P ) ⊆ {ε, 0, 0

• 1, 0 • 2}. For instance, supp(P ex ) = {ε, 0, 0 • 1, 0 • 2, 0 • 5, 0 • 6}. More generally, if t is a term, we set A t = {a ∈ N * | a ∈ supp(t)} and B t = (A t × N * ) ∪ {p ⊥ } (
where p ⊥ is an "empty biposition" constant), so that, if P is a • -derivation typing t, then a position (resp. a biposition) of P must be in A t (resp. in B t \ {p ⊥ }) i.e. supp(t) ⊆ A t and bisupp(P ) ⊂ B t \ {p ⊥ }. The constant p ⊥ roughly materializes emptiness and will be used to describe how "relevance-related emptiness" is constrained to occur in • -derivations (see polar inversion in § 3.3).

We omit P and t from some notations. We set A a (x) = {a 0 ∈ A | a a 0 , t(a 0 ) = x, a 0 , a a 0 < a 0 , t(a 0 ) = λx}. Thus, with the notation Ax P a of § 2.3, if P is a • -derivation, then Ax P a (x) ⊂ A a (x) for all a ∈ supp(P ), x ∈ V and A a (x) may be considered as the set of position candidates for ax-rules typing x above a. Now, remember that the function • has been fixed to choose axiom tracks for us ( § 2.3): if x a variable and a 0 an axiom position candidate for x (i.e. t(a 0 ) = x), then a potential • -derivation P containing a 0 has an axiom of the form P (a 0 ) = x : (k • T ) x : T with k = a 0 . Thus, if t(a) = λx and we set Tr λ (a) = { a 0 | a 0 ∈ A a•0 (x)}, then Tr λ (a) is the set of axiom tracks dedicated to x above the abs-rule at position a by the function • . It is interesting in that, e.g., if t(a) = λx and 8 / ∈ Tr λ (a), then we can assert that, if there exists a • -derivation P and a ∈ supp(P ), then P (a) = (S k ) k∈K → T with 8 / ∈ K. Indeed, by definition of Tr λ (a), there is no axiom position candidate a 0 for x above a whose axiom track is 8.

Thus, when a variable x is not at some places in t, • constrains emptiness to "occur" at some particular tracks if we perform an abstraction λx, and then, we informally say e.g., that emptiness occurs on track 8 w.r.t. position a under the above assumption. This give us more fine-grained information about occurrences of emptiness in a derivation typing t: system S (enriched with • ) will provide us information about emptiness track by track. This is precisely what we need to understand typability in the relevant and non-idempotent framework (remember § 1.5) in that, we have to ensure that emptiness does not compromise typability: intuitively, emptiness must not propagate everywhere in the derivations typing a given term t. If it did, a derivation typing t would be empty (i.e. t would not be typable) and we want to show that this does not happen, in the purpose of proving that every term is typable in S

Tracking a Type in a Derivation

Let us now express the stability conditions (as in § 3.1) that a • -bisupport candidate for a derivation typing t should satisfy. We will need to ensure the points below:

• Identification of the components (i.e. the bipositions) of a same type T in a derivation from bottom to top (see Fig. 3): relation of ascendance → asc .

• Identification of the components of type given in an ax-rule to a variable x (S 5 in Fig. 3) and its occurrence called by the abstraction λx: relation of polar inversion → pi .

• Identification of the matching components of the types of u and v in the app-rule typing u v (types S k in the app-rule of Fig. 3): relation of consumption →.

• Correct type formation, as in Sec. 3.1: extensions of relations → t1 and → t2 .

• The type of a subterm of the form λx.u is an arrow type (and not a type variable): relation → abs .

Abstraction rule ax

x : (5•S 5 ) x : S 5 pos(5)

C; x : (S k ) k∈K u : T a•0 By lack of space, most of the proofs are omitted for the remainder of the paper and we can only give a few details on the concepts that we use. We refer to the webpage of the author, or Chapters 11 and 12 of [START_REF] Vial | Non-Idempotent Typing Operator, beyond the Lambda-Calculus[END_REF] for all the details and more examples and heuristics.

(with 5 ∈ K, 8 / ∈ K) abs C λx.u : (S k ) k∈K → T a Application rule C u : (S k ) k∈K → T a•1 (D k v : S k a•k ) k∈K app C ( k∈K D k ) u v : T a
In Fig. 3, we indicate the position of a judgment between angle ( =square) brackets e.g., C; x : (S k ) k∈K t : T a • 0 means that judgment C; x : (S k ) k∈K t : T is at position a • 0. We denote by pos the (partial) converse of • e.g., if a 0 := pos(7) exists, then a 0 is the axiom position candidate whose axiom track is 7: concretely, this just means that, if there exists a • -derivation P typing t s.t. a 0 ∈ supp(P ), then P (A) = x : (7•S) x : S for some type S and x.

Assume that, in a • -derivation P , we find an abs-rule at position a as in The occurrence of T in the conclusion of the rule is intuitively the same as that in its premise: we say the former is the ascendant of the latter, since it occurs above in the typing derivation. Likewise, in the apprule, the occurrence of T in C k∈K D k u v : T stems from that of premise C u : (S k ) k∈K → T : the first occurrence of T is also the ascendant of T in the conclusion of the rule. Ascendance induces a stability relation → asc on the set of type elements i.e. on B t , the set of candidate bipositions of t, that can be formally defined by:

• (a, c) → asc (a • 1, 1 • c) if t(a) = @. • (a, 1 • c) → asc (a • 0, c) if t(a) = λx.
For instance, in Fig 4, the red (resp. the blue) occurrences of o are ascendants of one another. They correspond to bipositions (ε, 1 2 ) → asc (0, 1)

→ asc (0 2 , ε) → asc (0 2 • 1, 1) (resp. (ε, 1 • 4 • 1) → asc (0, 4 • 1)) from bottom to top.
Assume that 5 ∈ K in the abs-rule at position a in Fig. 3.

Then the occurrence of S 5 in (S k ) k∈K → T at pos. a stems from an axiom rule concluding with x : (5 • S 5 ) x : S 5 at pos. pos(5): we say that the occurrence S 5 (in (S k ) k∈K → T ) is the polar inverse of the occurrence of S 5 in the axiom rule. Assume on the contrary that 8 / ∈ K. So S 8 does not exist and there is no ax-rule typing x and using axiom track 8 above a. Morally, S 8 is empty.

More generally, if t(a) = λx and k 0 2, the function • . . .

• . . . either gives a unique axiom position candidate for the type on track k in (S k ) k∈K : this happens when ∃a 0 a • 0 s.t. a 0 = k 0 (i.e. , when k 0 ∈ Tr λ (a) by construction of Tr λ (a)). In that case, a 0 = pos(k 0 ).

• . . . or tells us that k 0 / ∈ K i.e. there cannot be a (top-level) type on track k 0 in (S k ) k∈K → T . In other words, this indicates that emptiness on track k 0 w.r.t. position a, which formally happens whenever no a 0 a • 0 satisfies a 0 (i.e. k 0 / ∈ Tr λ (a)). In that case, pos(k 0 ) is undefined. We consider the type S k0 (that intuitively does not exist) be the polar inverse of an empty type.

Polar inversion also induces a stability relation → pi on B t , that can be formally defined by:

• (a, k • c) → pi (pos(k), c) if k ∈ Tr λ (a) (first case) • (a, k • c) → pi p ⊥ if k / ∈ Tr λ (a) (second case)
For instance, in Fig. 4, the top blue occurrence of o is the polar inverse of the top red one: formally, (0, 4 • 1) → pi (0 2 • 1, 1). Now, we may understand the use of constant p ⊥ : it indicates biposition that cannot be in any potential • -derivation typing t. More precisely, p ⊥ is here to play the role of the polar inverse of all the bipositions that cannot exist, because of the choices made by the function • .

Type Formation, Type Consumption

In this subsection, we conclude the definitions of the stability relations that characterize the form of S-derivations, yielding the notion of subjugation (as in § 3.1), between candidate bipositions.

The notion of consumption is related to rule app. Assume t(a) = @, t| a = u v with u : (S k ) k∈K → T and v : S k for all k ∈ K as in Fig. 3 so that u v can be typed with T . Each type S k occurs in (S k ) k∈K → T and v : S k . However, it is absent in the type of u v: we say it has been consumed. Formally, we set, for all (a, c) ∈ B t , k 2 s.t. t(a) = @:

• (a • 1, k • c) → a (a • k, c)
In Fig. 4, the orange and the purple occurrences of o are consumed in the app-rule: formally, (0

2 • 1, 8) → 0 2 (0 2 • 8, ε).
We set → = ∪{→ a | a ∈ A, t(a) = @} and write ← for the symmetric relation.

Let P be a • -derivation typing a term t. If p 1 → asc p 2 or p 1 → pi p 2 or p 1 → p 2 , then p 1 ∈ bisupp(P ) iff p 2 ∈ bisupp(P ) (by construction of those relations).

Relations → t1 and → t2 ensure that the types are correctly defined and are natural extensions of those of Sec 3.1:

• For all (a, c) ∈ B t and k ∈ N, (a, c • k) → t1 (a, c).
• For all (a, c) ∈ B t and k 2, (a, c • k) → t2 (a, c • 1).

The relation below → abs ensures that, if λx.u is a typed subterm of t, then its type T is an arrow type.

• if t| a = λx.u, then(a, ε) → abs (a, 1)
The "big-step" stability relation → down below roughly states that the support of a potential derivation is a tree: We set

• (a , c) → down (a, ε) • p ⊥ → down (a, ε) ax 4 x : (8•o, 3•o , 2•o)→o ax 9 x : o [2] ax 2 x : o [3] ax 5 x : o [8] app . . . x x : o abs λx.x x : (2 • o , 4 • (8 • o, 3 • o , 2 • o) → o , 5 • o, 9 • o) → o abs λyx.xx : ( ) → (2 • o , 4 • (8 • o, 3 • o , 2 • o) → o , 5 • o, 9 • o) → o
→ • = → ∪ ← ∪ → t1 ∪ → t2 ∪ → abs ∪ → down . If p 1 → • p 2 ,
notice that, by construction, p 1 ∈ bisupp(P ) implies p 2 ∈ bisupp(P ). We say then that p 1 subjugates p 2 , generalizing § 3.1.

Characterizing Bisupport Candidates with Threads

We prove now that the relations above are indeed enough to express a sufficient condition of typability (Corollary 1).

As we have seen, if P is a • -derivation, then bisupp(P ) is closed under → asc , asc ←, → pi , pi ←, →, ←, → t1 , → t2 , → abs and → down . Of course, p ⊥ , the empty biposition, cannot be in P . It turns out that it is enough to characterize candidate bisupports (Prop. 1). Let ≡ be the reflexive, transitive, symmetric closure of → asc ∪ → pi . We have:

Proposition 1. Let B ⊆ B t .
Then B is a • -candidate bisupport for a derivation typing t (i.e. there exists a • -derivation s.t. B = bisupp(P )) iff (1) B is non-empty, (2) B is closed under ≡ and → • , and (3) B does not contain p ⊥ .

In other words, a set of real bipositions (i.e. excluding p ⊥ ) is the bisupport of an actual • -derivation typing t when it is closed under the relations ≡ and → • . If such a set exists, then t is typable.

Proof sketch. The necessity of these conditions has been discussed in § 3.3 and 3.4. Conversely, assume that ∅ = B ⊂ B t \ {p ⊥ } is closed under ≡ and → • . We want a derivation P s.t. bisupp(P ) = B. For that, we need to suitably decorate the p ∈ B. Mainly, a non-terminal biposition must be labelled with → and a terminal one with a fixed type atom o, in order to get correct types (as in § 3.1). On can check that P is a correct S-derivation using the definition of ≡ and → • .

From now on, it will be better to reason modulo ≡ (it may already be guessed that ≡ should commute with →, → t1 , . . ., which is made explicit in § 4.2) and to focus on subjugation. Definition 1. Let t be a term and • : N * → N \ {0, 1} an injection, and → asc , → pi the relations of ascendance and polar inversion in B t defined w.r.t. • .

• An ascendant thread is an equivalence class of relation ≡ asc , the reflexive, transitive, symmetric closure of → asc .

• A thread (metavariable θ) is an equivalence class of relation ≡ (see Fig. 4 ).

• The quotient set B t / ≡ is denoted Thr.

In Fig. 4, the red occurrences of o correspond to an ascendant thread and the blue one to another. Their union constitutes a (full) thread, that we denote θ a . Likewise, the green and the orange occurrences of o respectively correspond to the negative and the positive part of a thread θ b . The unique purple occurrence of o corresponds to a singleton thread θ c .

The notation Thr implicitly depends on t and • . The thread of (a, c) ∈ B is written thr(a, c) and we set:

θ ε = thr(ε, ε) θ ⊥ = thr(p ⊥ ) "root thread"
"thread of emptiness"

If thr(p) = θ, we say that θ occurs at biposition p, also written θ : p or p : θ e.g., θ a : (ε, 1 2 ) or θ a : (0, 4•1).

We consider now the extension of every other relation modulo ≡. Namely, we write θ 1 →a θ 2 if ∃p 1 , p 2 , θ 1 = thr(p 1 ), θ 2 = thr(p 2 ), p 1 → a p 2 . Thus, θ 1 →a θ 2 iff θ 1 : p 1 → a p 2 : θ 2 for some p 1 , p 2 . In that case, we say that θ 1 (resp. θ 2 ) has been left-consumed (resp. right-consumed) at biposition p 1 (resp. p 2 ) e.g., in Fig. 4, θ b : (0 Analogies with first order model theory: given t ∈ Λ and • and keeping in mind the intuition of bisupport candidates, let T t, • be the first order theory whose set of constants is Thr(P ), that features one unary predicate symbol inBis (standing for "is in bisupport") and whose set of axioms is {inBis(θ 1 ) ≡ inBis(θ 2 ) | θ 1 , θ 2 ∈ Thr(P ), θ 1 →• θ 1 } ∪ {¬inBis(θ ⊥ )}. Then Corollary 1 states that there exists a • -derivation P typing t iff T t, • is not contradictory: this is a sort of completeness result. Of course, it remains to be proved that T t, • is not contradictory (given any t). And this will be done using a technique closely associated to the λ-calculus: a finite reduction strategy (presented in § 5).

Nihilating Chains

We begin § 4 with a global description of the key steps leading to the fulfillment of Goal 4 (every term is • -typable) giving the final result (every term is R-typable) and a presentation of the central notion of nihilating chain.

For the purpose of proving that every term is typable, we want to prove that, for each term t and injection • : N * → N \ {0, 1}, there is a • -derivation typing t. According to Corollary 1, we must show that θ ⊥ is not in the reflexive transitive closure of θ ε by →• . A proof of θ ε → *

• θ ⊥ would involve a nihilating chain:

Definition 2. • A chain is a finite sequence of the form θ 0 →• θ 1 →• . . . →• θ m .
• When θ 0 = θ ε , θ m = θ ⊥ , the chain is said to be nihilating.

In order to apply Corollary 1, we must then prove that there are no nihilating chains. In other words, this corollary implies: Proposition 2. If the nihilating chains do not exist, then every term is •typable, and thus, also R-typable.

We proceed ad absurdum and consider θ 0 →• θ 1 →• . . . →• θ m with θ 0 = θ ε and θ m = θ ⊥ . However, →• can be →, ←, →t1 , →t2 , →abs or →down . The structure of the proof is the following:

• We define (Definition 3) the notion of polarity for bipositions: a biposition is negative when it is created by an abs-rule (modulo → asc ) and positive otherwise.

• The termination of a finite collapsing strategy (Sec. 5.2) guarantees that positivity can be assumed to only occur at suitable places in the chain without loss of generality. In that case, we say that the chain is normal (Definition 4).

• In normal chains, the different cases of subjugation interact well ( § 4.2), so that, from any normal chain, we may build another that begins with θ ε →• θ 1 . This is easily shown to be impossible, which entails that nihilating chains do not exist and that every term is S-typable.

Polarity and Threads

In this section, we define the key notion of syntactic polarity. If p → asc p i (i = 1, 2) then p 1 = p 2 (→ asc is functional) and we write p 1 = p 2 = asc(p). We set, for all p ∈ B, Asc(p) = asc i (p), where i is maximal (i.e. asc i (p) is defined, but not asc i+1 (p)). Thus, Asc(p) is the top ascendant of p e.g., in Fig. 4, the top red (resp. blue) occurrence of o is the top ascendant of the other ones (resp. one). A top ascendant is either located in an ax-node (e.g., the top red ascendant in Fig. 4) or in an abs-node (e.g., the blue ones), motivating: [START_REF] Vial | Non-Idempotent Typing Operator, beyond the Lambda-Calculus[END_REF] for details. Then, one proves that there is no θ such that θ ε ⊕ →θ. This implies that there is no chain of the form θ ε = θ 0 ⊕ →θ 1 ⊕ →... ⊕ →θ = θ ⊥ , and then, that there is no normal nihilating chain: Proposition 3. There is no normal nihilating chain.

u λx (S k ) k∈K → T λ3 ( * )→(S k ) k∈K →T @ (S k ) k∈K → T λ2 ( * )→(S k ) k∈K →T λ1 ( * )→( * )→(S k ) k∈K →T @ ( * ) → (S k ) k∈K → T @ (S k ) k∈K → T @ T The S k are consumed there v (S k ) k∈K step 1 u1 λx λ3 @ λ2 @ @ v u2 λx λ3 @ @ v step 2 step 3 step 4 u3 (S k ) k∈K → T λx @ T v (S k ) k∈K u3[v/x]
= θ 0 ⊕ →θ 1 ⊕ →... ⊕ →θ = θ ⊥ . See § 12.3.3 in
Proposition 3 almost proves that every term is • -typable (by Proposition 2). Almost, because only the non-existence of normal nihilating chains is ensured for now (and not that of nihilating chains in general). The only point that will remain to be verified is that normal nihilating chains can be considered without loss of generality (which is the object of § 5).

Normalizing Nihilating Chains

Residuation and Subjugation

In this section, we explain why negative left-consumption in a nihilating chain can be avoided (without loss of generality). By Prop. 2 and 3, this will allow us to prove that every term is typable. The fact that system S is relevant, non-idempotent, rigid and syntax-directed entails that if P £ C t : T and t b → β t , then, there is a unique derivation P £ C t : T obtained from P by subject reduction (thus, subject reduction is deterministic in system S).

Moreover, intuitively, every part of P comes from a part of P and so, every position and right biposition of P can be thought as the (quasi-)residual of position or (right) biposition of P . We do not give details (that can be found in § IV and Fig. 1 in [START_REF] Vial | Infinitary intersection types as sequences: A new answer to Klop's problem[END_REF]), but this induces a function QRes b from the right bisupport of P to that of P . The function QRes b turns out to be compatible with thread-membership:

Lemma 6. If p 1 ≡ p 2 in P , then QRes b (p 1 ) ≡ QRes b (p 2 ) in P .
This Lemma allows us to define (quasi-)residuals for threads. We set Res b (θ) = thr (QRes b (p)) for any p : θ (where thr (•) denotes threads in B t ). By case analysis, we have:

Lemma 7. Let θ 1 , θ 2 ∈ Thr. We set θ i = Res b (θ i ) (i = 1, 2). • If θ 1 →θ 2 , then θ 1 →θ 2 or θ 1 = θ 2 . • If θ 1 →t1 θ 2 , then θ 1 →t1 θ 2 or θ 1 = θ 2 . • If θ 1 →t2 θ 2 , then θ 1 →t2 θ 2 , θ 1 →down θ 2 or θ 1 = θ 2 . • If θ 1 →abs θ 2 , then θ 1 →abs θ 2 or θ 1 = θ 2 . • If θ 1 →down θ 2 , then θ 1 →down θ 2 or θ 1 = θ 2 .
See § 12.4.1 in [START_REF] Vial | Non-Idempotent Typing Operator, beyond the Lambda-Calculus[END_REF] for the proofs of Lemmas 6 and 7.

Finally, Res b (θ ε ) = θ ε and Res b (θ ⊥ ) = θ ⊥ as expected, so Lemma 7 implies that, if there is a nihilating chain for t of length m, then there is one for t of length m (whenever t → * t ).

The Collapsing Strategy

We explain now how to normalize a chain i.e. discard negative left-consumption. This will allow us to use Proposition 3 to finally conclude that nihilating chains do not exist.

The idea is that if θ L →a θ R , then either t| a is a redex and we have Res b (θ L ) = Res b (θ R ) (i.e. θ 1 and θ 2 are collapsed by the reduction step) or θ L passes through a redex. When we reduce this redex, the "height" of θ L will decrease. More precisely, the 2nd case is associated with the notion of redex tower, which is more or less a finite nesting of redexes, that can -more importantly -be collapsed in a finite number of steps. A case of negative left-consumption of a sequence type (S k ) k∈K (which is the domain of the abstraction λx.u), coming along with a redex tower, is represented in Fig. 5 (we write λi instead of λx i and ( * ) for matterless sequence types). The sequence type (S k ) k∈K of negative polarity is "called" by the node λx at the top of the figure and consumed at the bottom app-rule. The initial redex tower is reduced in 4 steps, so that its height decreases and finally, the types S k , that were left-consumed negatively, are destroyed in the final term u 3 [v/x]. . Lemma 8. If θ 1 →θ 2 , then there is a reduction path rs such that Res rs (θ 1 ) = Res rs (θ 2 ) (residuation naturally extends along with rs). This Lemma, along with the conclusion of § 5.1, yields: Proposition 4. There is a reduction strategy (the "collapsing strategy") producing a normal nihilating chain from any nihilating chain.

Applications

We can now prove that every term is • -typable (and thus, also R-typable, by Goal 4), using Prop. 2, the residuation of threads (S 5.1), the collapsing strategy (Prop. 4) and the non-existence of normal threads (Prop. 3), which is ensured by the Interaction Lemmas.

Theorem 1. Every λ-term is typable in the relevant and non-idempotent intersection type system R.

By the same techniques (the complete proofs are in § 12.4.5 of [START_REF] Vial | Non-Idempotent Typing Operator, beyond the Lambda-Calculus[END_REF]), system R discriminates terms w.r.t. their arities, as claimed: Lemma 9. Let t be a zero term and o a type atom, then there is context C such that C t : o is S-derivable.

Proof sketch. Let t be a term s.t. θ ε → *

• thr(ε, 1) i.e. s.t. (ε, 1) ∈ B min (see Corollary 1), which implies that the type of t cannot be a type atom by the proof of this same corollary. We prove that t is of arity 1, which is enough to conclude.

For that, we consider a λ-chain i.e. a chain of the form θ ε = θ 0 →• . . . →• θ m = thr(ε, 1), of minimal length. The notion of normal chains extends to λ-chains and by the collapsing strategy, we can replace t by a reduct t s.t. the considered chain is normal.

Using ad hoc interaction lemmas, we prove that the normality of the chain entails θ ε →abs thr(ε, ε). Collapsing then redex towers, we may reduce t to an abstraction λx.t . Q.E.D. Theorem 2. Let t be a term of arity n. Then there is a context Γ and a type τ of arity n (see Sec. 2.4) such that Γ t : τ is R-derivable.

Proof sketch. When n = ∞, this comes from Theorem 1, subject reduction and the abs-rule. When n ∈ N, we use Lemma 9 and (finite) subject expansion (Proposition 1).

Conclusion:

We proved that every term is typable in a reasonable relevant intersection type system (Theorem 1). If we take the typing rules of S coinductively (and not only the type grammar), we can also type every infinitary λ-term [START_REF] Kennaway | Infinitary lambda calculus[END_REF].

The techniques that we have developed here build, to the best of our knowledge, the first bridge between first-order model theory and the study of models of the pure λ-calculus. They are actually modular: we also use them, in a companion paper, to prove that every multiset-based derivation is the collapse of a sequential derivation [START_REF] Vial | Representing permutations without permutations, or the expressive power of sequence types[END_REF]. This suggests that these techniques could be used to study the coinductive version of finitary models of the λ-calculus and extend some of their semantical properties to all λ-terms.

By setting, for each term t, [[t]] rel∞ = {£ R Γ t : τ | Γ, τ } (cf. § 1.3), one defines the infinitary version of the relation model, in which, by Theorem 1, no term has a trivial denotation, including the mute terms. This model is thus non-sensible [START_REF] Berarducci | Infinite lambda-calculus and non-sensible models[END_REF] since it does not equate all the non-head normalizing terms (e.g., Ω and λx.Ω of respective arities 0 and 1) by Theorem 2.

We presented a first semantical result about this model (Theorem 2), but its equational theory has yet to be studied. According to the same theorem, this model equates all the closed zero terms. It then differs both from the non-sensible model of Berarducci trees and that of Lévy-Longo trees, respectively related to Λ 111 and Λ 001 in [START_REF] Kennaway | Infinitary lambda calculus[END_REF]. This work may suggest a new notion of tree, that could shed some light on Open Problem # 18 of TLCA (the problem of finding trees related to various contextual equivalences).

The study of infinitary models (beyond infinite tree models) is at its early stages, but it already provides descriptions of the infinitary behaviors of λterms (cf. Grellois-Melliès' infinitary model of Linear Logic in [START_REF] Grellois | An infinitary model of linear logic[END_REF][START_REF] Grellois | Relational semantics of linear logic and higherorder model checking[END_REF]). The semantical implications of the main theorem (every term is R-typable) remain to be understood and the proof techniques presented here can certainly be used to study infinitary models or coinductive/recursive type systems before they are endowed with some validity or guard condition, or maybe to build other models of pure λ-calculus, for instance, to get some semantical proof of the easiness [START_REF] Jacopini | A condition for identifying two elements of whatever model of combinatory logic[END_REF] of sets of mute terms, as in [START_REF] Bucciarelli | Graph easy sets of mute lambda terms[END_REF].

Figure 2 :

 2 Figure 2: Typing a Head Normal Form in an i.t.s.

  equality, the occurrence of o in the left-hand side annotated with 2 unambiguously comes from that which is also annotated with 2 in the right-hand side. We call these annotations tracks. In contrast, [o, o , o] = [o, o ] + [o], but there is no way to unambiguously associate to an occurrence of o in the left-hand side the one of [o, o ] or the one of [o] in the right-hand side.

Figure 3 :

 3 Figure 3: Ascendance, Polar Inversion and Consumption

  Fig 3: the judgment C; x : (S k ) k∈K u : T (pos. a • 0) yields C λx.u : (S k ) k∈K → T below (pos. a).

Figure 4 :

 4 Figure 4: Threads, Ascendance and Consumption Note that Lemma 7 would not hold without considering → down .

  2 •1, 8) →0 2 (0 2 •8, ε) : θ c . We do likewise for → t1 , → t2 , → abs , → down , → • , thus defining →t1 , →t2 , →abs , →down , →• , whose reflexive transitive closure of relation →• is denoted → * • . If θ ⊥ is not in the transitive closure of {θ ε } by →• , then t is typable in S (by means of a • -derivation). Proof. Let B min = {p ∈ B | θ ε → * • thr(p)} i.e. B min is the union of the reflexive transitive closure of θ ε under →• . If θ ε → • * θ ⊥ does not hold, then B min satisfies the hypotheses of Prop. 1. So there is a derivation P s.t. bisupp(P ) = B min and thus, t is typable.

	Corollary 1.

In this article, we put aside non-strict types systems (e.g., system DΩ[START_REF] Krivine | Lambda-calculus, types and models. Ellis Horwood series in computers and their applications[END_REF][START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF]), in which types are less constrained by the arity of terms.

Note that Y f → f (Y f ) (Y f is HN) and Y f is typable with o in the finite system R 0 .

Definition 3.

• Let p ∈ B t \ {p ⊥ } and (a 0 , c 0 ) = Asc(p). We define the polarity of p as follows: if t(a 0 ) = x for some x ∈ V , then we set Pol(p) = ⊕ and if t(a 0 ) = λx, then we set Pol(p) = . We also set Pol(p ⊥ ) = .

• If thr(p) = θ and Pol(p) = ⊕/ , we say that θ occurs positively/negatively at biposition p.

• If θ is left/right-consumed at p and Pol(p) = ⊕ (resp. Pol(p) = ), we say that θ is left/right-consumed positively (resp. negatively) at biposition p.

Then, we write for instance θ 1 ⊕ →a θ 2 to mean that θ 1 is left-consumed positively and θ 2 is right-consumed negatively in the app-rule at position a. In Fig. 4, the blue occurrences of o are negative, the red ones are positive and

Interactions in Normal Chains

In § 4.2, we present the notion of normal chain and explicit some interaction properties that allow us to simplify/rewrite them.

As it has been discussed in § 1.5 and 2.1, the possibility for a variable x (of a redex or of a redex to be created later) to be substituted in a reduction sequence is problematic. Intuitively, a biposition is negative when it was "created" in an abstraction λx and that left-consumption is associated to left-hand sides of application. Thus, a negative left-consumption hints at the presence of redex (this intuition will be made more explicit in Sec. 5.2). More precisely, it indicates the presence of what we will call a redex tower. This suggests the following notion: Definition 4. A chain is normal if no thread is left-consumed negatively in it (there is no link of the form θ i →θ i+1 or θ i ← θ i+1 ).

Normal chains can be handled! The interaction lemmas below describe some commutations between stability relations. Lemma 5.

• If thr(p) = θ ⊥ , then Pol(p) = .

• If θ →t1 θ ⊥ or θ → t2 θ ⊥ , then θ = θ ⊥ .

• We cannot have θ →abs θ ⊥ or θ →down θ ⊥ .