Pierre Clairambault
email: p.clairambault@bath.ac.uk

Estimation of the length of interactions in arena game semantics

We estimate the maximal length of interactions between strategies in HO/N game semantics, in the spirit of the work by Schwichtenberg and Beckmann for the length of reduction in simply typed λ-calculus. Because of the operational content of game semantics, the bounds presented here also apply to head linear reduction on λ-terms and to the execution of programs by abstract machines (PAM/KAM), including in presence of computational effects such as non-determinism or ground type references. The proof proceeds by extracting from the games model a combinatorial rewriting rule on trees of natural numbers, which can then be analysed independently of game semantics or λ-calculus.

Introduction

Among the numerous notions of execution that one can consider on higher-order programming languages (in particular on the λ-calculus) head linear reduction [START_REF] Danos | How abstract machines implement head linear reduction[END_REF] plays a particular role. Although it is not as widespread and specifically studied as, say, β-reduction, it is nonetheless implicit to various approaches of higher-order computation, such as geometry of interaction, game semantics, optimal reduction and ordinary operational semantics. It is also implicit to several abstract machines, including the Krivine Abstract Machine (KAM) [START_REF] Krivine | Un interpréteur du λ-calcul[END_REF] and the Pointer Abstract Machine (PAM) [START_REF] Danos | How abstract machines implement head linear reduction[END_REF], in the sense that it is the reduction they perform [START_REF] Danos | How abstract machines implement head linear reduction[END_REF][START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF] and as such is a valuable abstraction of how programs are executed in the implementation of higher order languages.

Despite being closer to the implementation of programming languages, head linear reduction never drew a lot of attention from the community. Part of the reason for that is that it is not a usual notion of reduction: defining it properly on λ-terms requires both to extend the notion of redex and to restrict to linear substitution, leading to rather subtle and tricky definitions which lack the canonicity of β-reduction 1 . Moreover, its associated observational equivalence is the same as for the usual head β-reduction, which makes it non relevant as long as one is interested in the equational theory of λ-calculus. However, head linear reduction should appear in the foreground as soon as one is interested in quantitative aspects of computation, such as complexity. On the contrary, although very precise bounds are known for the possible length of β-reduction chains in simply typed λ-calculus [START_REF] Schwichtenberg | Complexity of normalization in the pure typed lambdacalculus[END_REF][START_REF] Beckmann | Exact bounds for lengths of reductions in typed λ-calculus[END_REF], to the author's knowledge, the situation for head linear reduction remains essentially unexplored. Even if it is generally expected that the bounds remain hyper-exponential2 (and this indeed what we will prove), it does not seem to follow easily from the bounds known for β-reduction.

Rather than reasoning directly on head linear reduction, we will instead look at it through game semantics [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF]. Indeed, there is a close relationship between head linear reduction and interaction in games model of programming languages [START_REF] Vincent Danos | Game semantics and abstract machines[END_REF]. More precisely, given two β-normal and η-long λ-terms S and T , there is a step-by-step correspondence between head linear reduction chains of ST and game-theoretic interactions between the strategies S and T . Of course, game semantics are not central to our analysis: as is often the case, our methods and results could be adapted to a purely syntactical framework. However, games have this considerable advantage of accommodating in a single framework purely functional programming languages such as the λ-calculus or PCF and a number of computational features such as non-determinism [START_REF] Harmer | A fully abstract game semantics for finite nondeterminism[END_REF], control operators [START_REF] Laird | Full abstraction for functional languages with control[END_REF] and references [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF]. This will allow us to do our study with an increased generality: our complexity results will hold for a variety of settings, from simply typed λ-calculus to richer languages possibly featuring the computational effects mentioned above, as long as there is no fixed point operator.

Outline. In Section 2 we will recall some of the basic definitions of Hyland-Ong game semantics, define the central notion of size of a strategy, and introduce our main question as the problem of finding the maximal length of an interaction between two strategies of fixed size. Our approach will be then to progressively simplify this problem in order to reach its underlying combinatorial nature. In Section 3 we first introduce the notion of visible pointer structures, i.e. plays where the identity of moves has been forgotten. This allows a more elementary (strategy-free) equivalent statement of our problem. Then we show how each position in a visible pointer structure can be characterised by a tree of natural numbers called an agent. We then show that the problem can be once again reformulated as the maximal length of a reduction on these agents. In Section 4 we study the length of this reduction, giving in particular an upper bound. We also give a corresponding lower bound, and finally use our result to estimate the maximal length of head linear reduction sequences on simply typed λ-terms.

Related works. Our results and part of our methods are similar to the works of Schwichtenberg and Beckmann [START_REF] Schwichtenberg | Complexity of normalization in the pure typed lambdacalculus[END_REF][START_REF] Beckmann | Exact bounds for lengths of reductions in typed λ-calculus[END_REF], but the reduction we study is in some sense more challenging, because redexes are not destroyed as they are reduced. Moreover, the game semantics setting allows for an extra generality. The present work also has common points with work by Dal Lago and Laurent [START_REF] Dal | Quantitative game semantics for linear logic[END_REF], in the sense that it uses tools from game semantics to reason on the length of execution. However the approach is very different : their estimate is very precise but uses an information on terms difficult to compute (almost as hard as actually performing execution). Here, we need little information on terms (gathering this information is linear in the size of the term), but our bounds are, in most cases, very rough.

Arena game semantics

We recall briefly the now usual definitions of arena games, first introduced in [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF]. More detailed accounts can be found in [START_REF] Mccusker | Games and Full Abstraction for FPC[END_REF][START_REF] Harmer | Innocent game semantics[END_REF]. We are interested in games with two participants: Opponent (O, the environment ) and Player (P, the program).

Arenas and Plays

Valid plays are generated by directed graphs called arenas, which are semantic versions of types. Formally, an arena is a structure A = (M A , λ A , I A , ⊢ A ) where:

• M A is a set of moves,
• λ A : M A → {O, P } is a polarity function indicating whether a move is an Opponent or Player move (O-move or P -move).

•

I A ⊆ λ -1 A ({O}) is a set of initial moves. • ⊢ A ⊂ M A × M A is a relation called enabling, such that if m ⊢ A n, then λ A (m) = λ A (n).
In other words, an arena is just a directed bipartite graph. We now define plays as justified sequences over A: these are sequences s of moves of A, each non-initial move m in s being equipped with a pointer to an earlier move n in s, satisfying n ⊢ A m. In other words, a justified sequence s over A is such that each reversed pointer chain s i0 ← s i1 ← . . . ← s in is a path on A (viewed as a graph). The role of pointers is to allow reopenings or backtracking in plays. When writing justified sequences, we will often omit the justification information if this does not cause any ambiguity. The symbol ⊑ will denote the prefix ordering on justified sequences, and s 1 ⊑ P s 2 will mean that s 1 is a P -ending prefix of s 2 . If s is a justified sequence on A, |s| will denote its length.

Given a justified sequence s on A, it has two subsequences of particular interest: the P-view and O-view. The view for P (resp. O) may be understood as the subsequence of the play where P (resp. O) only sees his own duplications.

Practically, the P-view s of s is computed by forgetting everything under Opponent's pointers, in the following recursive way:

• sm = s m if λ A (m) = P ;
• sm = m if m ∈ I A and m has no justification pointer;

• s 1 ms 2 n = s mn if λ A (n) = O and n points to m.
The O-view s of s is defined dually, without the special treatment of initial moves 3 . The legal plays over A, denoted by L A , are the justified sequences s on A satisfying the alternation condition, i.e. that if tmn ⊑ s, then λ A (m) = λ A (n).

Classes of strategies

In this subsection, we will present several classes of strategies on arena games that are of interest to us in the present paper. A strategy σ on A is a set of even-length legal plays on A, closed under even-length prefix. A strategy from A to B is a strategy σ : A ⇒ B, where A ⇒ B is the usual arrow arena defined by Composition is associative and admits copycat strategies as identities.

M A⇒B = M A + M B , λ A⇒B = [λ A , λ B ] (
P -visible strategies. A strategy σ is P -visible if each of its moves points to the current P -view. Formally, for all sab ∈ σ, b points inside sa . P -visible strategies are stable under composition, as is proved for instance in [START_REF] Harmer | Innocent game semantics[END_REF]. They correspond loosely to functional programs with ground type references [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF].

Innocent strategies. The class of innocent strategies is central in game semantics, because of their correspondence with purely functional programs (or λ-terms) and of their useful definability properties. A strategy σ is innocent if

sab ∈ σ ∧ t ∈ σ ∧ ta ∈ L A ∧ sa = ta ⇒ tab ∈ σ
Intuitively, an innocent strategy only takes its P -view into account to determine its next move. Indeed, any innocent strategy is characterized by a set of Pviews. This observation is very important since P -views can be seen as abstract representations of branches of η-expanded Böhm trees (a.k.a. Nakajima trees [START_REF] Nakajima | Infinite normal forms for the λ-calculus[END_REF]) : this is the key to the definability process on innocent strategies [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF]. It is quite technical to prove that innocent strategies are stable under composition, proofs can be found for instance in [START_REF] Harmer | Innocent game semantics[END_REF][START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF]. Arenas and innocent strategies form a cartesian closed category and are therefore a model of simply typed λ-calculus.

Bounded strategies. A strategy σ is bounded if it is P -visible and if the length of its P -views is bounded: formally, there exists N ∈ N such that for all s ∈ σ, | s | ≤ N . Bounded strategies are stable under composition, as is proved in [START_REF] Clairambault | Totality in arena games[END_REF] for the innocent case and in [START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF] for the general case. This result corresponds loosely to the strong normalisation result on simply-typed λ-calculus. Syntactically, bounded strategies include the interpretation of all terms of a functional programming language without a fixed point operator but with Algol-like ground type references (for details about how reference cells get interpreted as strategies see for instance [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF], it is obvious that this interpretation yields a bounded strategy) and arbitrary non determinism. This remark is important since it implies that our results will hold for any program written with these constructs, as long as they do not use recursion or a fixed point operator.

Size of strategies and interactions

Since in this paper we will be interested in the length of interactions, it is sensible to make it precise first what we mean by the size of strategies. Let σ be a bounded strategy, its size is defined as

|σ| = max s∈σ | s | 2
All our analysis on the size of interactions will be based on this notion of size of strategies. Our starting point is the following finiteness result, proved in [START_REF] Clairambault | Totality in arena games[END_REF].

We say that an interaction u ∈ I(A, B, C) is passive if the only move by the external Opponent on A, C is the initial move on C, so that the interaction stops as soon as we need additional input from the external Opponent.

Proposition 1. Let σ : A ⇒ B and τ : B ⇒ C be bounded strategies and let u ∈ σ||τ be a passive interaction, then u is finite.

Using this, we can actually deduce the existence of an uniform bound on the length of such u ∈ σ||τ , which only depends on the respective size of σ and τ : Lemma 1. For all n, p ∈ N there is a lesser N (n, p) ∈ N such that for all arenas A, B and C, for all σ : A ⇒ B and τ : B ⇒ C such that |σ| ≤ p and |τ | ≤ n, for all passive u ∈ σ||τ we have |u| ≤ N (n, p).

Proof. For arenas A, B and C consider the set T

A,B,C of all passive interactions u ∈ I(A, B, C) such that for all s ⊑ u ↾B,C , | s | ≤ 2n and for all s ⊑ u A,B , | s | ≤ 2p.
Then, consider the union T of all the T A,B,C , our goal here is to find a bound on the length of all elements of T . Consider now the tree structure on T given by the prefix ordering. To make this tree finitely branching, consider the relation m ∼ = n ⇔ depth(m) = depth(n) on moves, where depth(m) is the number of pointers required to go from m to an initial move. The tree T / ∼ = is now finitely branching, but is also well-founded by Proposition 1, therefore it is finite by König's lemma 4 . Let N (n, p) be its maximal depth, it is now obvious that it satisfies the required properties.

We have proved the existence of the uniform bound N (n, p), but in a way that provides no feasible means of estimating N (n, p). The goal of the rest of this paper is to estimate this bound as precisely as possible. As a matter of fact, we will be mainly interested in the "typed" variant N d (n, p), defined as the maximum length of all possible passive interactions between strategies σ : A ⇒ B and τ : B ⇒ C of respective size p and n, where B has a finite depth d -1.

Pointer structures and rewriting

We have seen that to prove Lemma 1, we must consider plays up to an equivalence relation ∼ = which assimilates all moves at the same depth. Indeed, general arenas and plays contain information which is useless for us. Following [START_REF] Clairambault | Totality in arena games[END_REF], we will here reason on pointer structures, which result of considering moves in plays up to ∼ =. Pointer structures are also similar to the parity pointer functions of Harmer, Hyland and Melliès [START_REF] Harmer | Categorical combinatorics for innocent strategies[END_REF] and to the interaction sequences of Coquand [START_REF] Coquand | A semantics of evidence for classical arithmetic[END_REF]. We will delve here into their combinatorics and extract from them a small rewriting system, whose study is sufficient to characterize their length.

N d (n, p) as a bound for pointer structures

Visible pointer structures. In [START_REF] Clairambault | Totality in arena games[END_REF], we introduced pointer structures by elementary axioms, independent of the general notions of game semantics. Instead here, we define pointer structures as usual alternating plays, but on the particular "pure" arena I ω = n∈N I n , where I 0 = ⊥ (⊥ is the singleton arena with just one Opponent move) and I n+1 = I n ⇒ ⊥. As we are interested in the interaction between P -visible strategies, we will only consider visible pointer structures, where both players point in their corresponding view. Formally, s is visible if for all s ′ p ⊑ P s, a points inside s ′ and if for all s ′ o ⊑ O s, o points inside s ′ . The depth of a visible pointer structure s is the smallest d such that s is a play on I d . Let us denote by V the set of all visible pointer structures.

Atomic agents. After forgetting information on plays, let us forget information on strategies. Instead of considering bounded strategies with all their intentional behaviour, we will just keep the data of their size. Pointer structures will then be considered as interactions between the corresponding numbers which will be called atomic agents. If n is such a natural number, we define its trace as follows, along with the dual notion of co-trace:

T r(n) = {s ∈ V | ∀s ′ ⊑ s, | s ′ | ≤ 2n} coT r(p) = {s ∈ V | ∀s ′ ⊑ s, | s ′ | ≤ 2p + 1}
An interaction at depth d between n and p is a visible pointer structure s of depth at most d such that s ∈ T r(n) ∩ coT r(p). We write s ∈ n ⋆ d p. These definitions allow to give the following strategy-free equivalent formulation of N d (n, p).

Agents

To bound the length of a pointer structure s, our idea is to label each of its moves s i by an object t, expressing the size that the strategies have left. Let us consider here an analogy between pointer structures and the execution of λ-terms by the KAM 5 . Consider the following three KAM computation steps:

(λx.xS) ⋆ T • π 0 3 T ⋆ S x →T • π 0
The interaction between two closed terms (with empty environment) leads, after three steps of computation, to the interaction between two open terms T and S (where x is free in S), with an environment. By analogy, if s 0 is labelled by the pair (n, p) of interacting "strategies", each move s i should correspond to an interaction between objects (a, b), where a and b have a tree-like structure which is reminiscent of those of closures 6 . We will call a pointed visible pointer structure (pvps) a pair (s, i) where s is a visible pointer structure and i ≤ |s| -1 is an arbitrary "starting" move. We adapt the notions of size and depth for pvps, and introduce a notion of context. Definition 1. Let (s, i) be a pointed visible pointer structure. The residual size of s at i, written rsize(s, i), is defined as follows:

• If s i is an Opponent move, it is max si∈ s ≤j | s ≤j | -| s ≤i | + 1 • If s i is a Player move, it is max si∈ s ≤j | s ≤j | -| s ≤i | + 1
where s i ∈ s ≤j means that the computation of s ≤j reaches7 s i . Dually, we have the notion of residual co-size of s at i, written rcosize(s, i), defined as follows:

• If s i is an Opponent move, it is max si∈ s ≤j | s ≤j | -| s ≤i | + 1 • Otherwise, max si∈ s ≤j | s ≤j | -| s ≤i | + 1
The residual depth of s at i is the maximal length of a pointer chain in s starting from s i . Definition 2. Let s be a visible pointer structure. We define the context of (s, i) as:

• If s i is an O-move, the set {s n1 , . . . , s np } of O-moves appearing in s <i ,
• If s i is a P-move, the set {s n1 , . . . , s np } of P-moves appearing in s <i .

In other words it is the set of moves to which s i+1 can point whilst abiding to the visibility condition, except s i . We also need the dual notion of co-context, which contains the moves the other player can point to. The co-context of (s, i) is:

• If s i is an O-move,
• rsize(s, i) ≤ 2n (resp. rcosize(s, i) ≤ 2n + 1),
• If {s n1 , . . . , s np } is the context of (s, i) (resp. co-context), then for each k ∈ {1, . . . , p} we have (s, n k ) ∈ coT r(a k ).

• If {s n1 , . . . , s np } is the context of (s, i) (resp. co-context), then for each k ∈ {1, . . . , p} the residual depth of s at n k is less than d k .

Then, we define an interaction of two agents a and b at depth d as a pair (s, i) ∈ T r(a) ∩ coT r(b) where the residual depth of s at i is less than d, which we write (s, i) ∈ a ⋆ d b.

Notice that we use the same notations T r, coT r and ⋆ both for natural numbers and general agents. This should not generate any confusion, since the definitions just above coincide with the previous ones in the special case of "atomic", or closed, agents: if n and p are natural numbers, then obviously

s ∈ n ⋆ d p if and only if (s, 0) ∈ n[] ⋆ d p[].
Note also that definitions are adapted here to this particular setting where strategies are replaced by natural numbers, however they could be generalized to the usual notion of strategies. An agent would be then a tree of strategies, and a trace of this agent would be a possible interaction between all these strategies. This would be a new approach to the problem of revealed or uncovered game semantics [START_REF] Greenland | Game semantics for region analysis[END_REF][START_REF] Blum | Thesis fascicle: Local computation of β-reduction[END_REF], where strategies are not necessarily cut-free.

Simulation of visible pointer structures

We introduce now the main tool of this paper, a reduction on agents which "simulates" visible pointer structures: if n[{d 1 }a 1 , . . . , {d p }a p ] and b are agents where i ∈ {1, . . . , p}, d i > 0 in the first case and d > 0 in the second case. We can now state the following central proposition.

Proposition 2 (Simulation). Let (s, i) ∈ a ⋆ d b, then if s i+1 is defined, there exists (a, d, b) (a ′ , d ′ , b ′ ) such that (s, i + 1) ∈ a ′ ⋆ d ′ b ′ .
Proof. The proof proceeds by a close analysis of where in its P -view (resp. O-view) s i+1 can point. If it points to s i , then the active strategy asks for its argument which corresponds to the second reduction case. If it points to some element s ni of its context, the active strategy calls the i-th element of its context: this is the first reduction case, putting the subtree a i in head position.

The rest of the proof consists in technical verifications, to check that the new triple (a

′ , d ′ , b ′ ) is such that (s, i + 1) ∈ a ′ ⋆ d ′ b ′ .
The result above will be sufficient for our purpose. Let us mention in passing that the connection between visible pointer structures and agents is in fact tighter: a reduction chain starting from a triple (n[], d, p[]) can also be canonically mapped to a pointed visible pointer structure in n ⋆ d p, and the two translations are inverse of one another. The interested reader is directed to [START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF]. We let the obvious verification to the reader. This is helpful, as all that remains to study is this reduction on agents illustrated in Figure 1. To summarize, if N (a) denotes the length of the longest reduction sequence starting from an agent a, we have the following property. Proof. Obvious from the simulation lemma, adding 1 for the initial move which is not accounted for by the reduction on agents. In fact this is an equality, as one can prove using the reverse simulation lemma mentioned above. See [START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF].

n dp G G G G G G G G G G G G G G d1 a i Ñ Ñ Ñ Ñ Ñ Ñ Ñ Ñ e e

Length of interactions

The goal of this section is to study the reduction on agents introduced above, and to estimate its maximal length. We will first provide an upper bound for this length, adapting a method used by Beckmann [START_REF] Beckmann | Exact bounds for lengths of reductions in typed λ-calculus[END_REF] to estimate the maximal length of reductions on simply typed λ-calculus. We will then discuss the question of lower bounds, and finally describe an application to head linear reduction.

Upper bound

We define on agents a predicate ρ α , which introduction rules are compatible both with syntax and reduction. then ρ α+1 a.

• Cut. If ρ α a, ρ β b and d ≤ ρ, then ρ α+β a • d b.
By this inductive definition, each proposition ρ α a is witnessed by a tree using Base, Red and Cut. Red-free trees look like syntax trees, are easy to build but give few information on the reduction, whereas Cut-free trees look like reduction trees, are difficult to build but give very accurate information on the length of reduction. The idea of the proof is then to design an automatic way to turn a Red-free tree to a Cut-free tree, via a cut elimination lemma. Let us now give the statement and sketch the proof of the four important lemmas that underlie our reasoning.

A context-agent a() is a finite tree whose edges are labelled by natural numbers, and whose nodes are labelled either by natural numbers, or by the variable x, with the constraint that all edges leading to x must be labelled by the same number d; d is called the type of x in a(). If We denote by a(b) the result of substituting of all occurrences of x in a() by b. We denote by a(∅) the agent obtained by deleting in a all occurrences of x, along with the edges leading to them. Proof. We prove by induction on the tree witness for ρ α a(∅) that the above property is true for all context-arena a ′ () such that a(∅) = a ′ (∅). The way to handle each case is essentially forced by the induction hypothesis.

Lemma 4 (Cut elimination lemma). Suppose ρ+1 α a. Then if α = 0, ρ 0 a.

Otherwise, ρ 2 α-1 a.

Proof. By induction on the witness for ρ+1 α a, using the substitution lemma when the last rule is Cut with a type of ρ + 1.

Lemma 5 (Recomposition lemma). Let a be an agent. Then depth(a) max(a)|a| a, where depth(a) is the maximal label of an edge in a, max(a) is the maximal label of a node and |a| is the number of nodes.

Proof. By induction on a.

Lemma 6 (Bound lemma). Let a be an agent, then if 0 α a, N (a) ≤ α.

Proof. The only used rules are Base, Red and Cut with ρ = 0. These Cut rules do not add any possible reduction and are easy to eliminate, then the lemma is easily proved by induction on a.

These lemmas are sufficient to give a first upper bound, by iterating the cut elimination lemma starting from the witness tree for ρ α a generated by the recomposition lemma. However when the type is small, some of the lemmas above can be improved. For instance if 0 α a(∅), 0 β b and the type of x in a() is 1, then 0 α+β a(b), since once the reduction reaches b it will never enter a() again. Using this we get a "base" cut-elimination lemma, stating that for all a, whenever 1 α a then we have actually 0 α a instead of 0

2 α-1
a. Using this, we prove the following. Note that whereas the bounds in [START_REF] Beckmann | Exact bounds for lengths of reductions in typed λ-calculus[END_REF] are asymptotic and give poor quantitative information if instantiated on small types, our bound does provide valuable information on interactions with small depth. For instance, if σ : A ⇒ B and τ : B ⇒ C such that rsize(σ) = p, rsize(τ ) = n and the depth of B is at most 2, then no interaction between σ and τ can be longer than N 3 (n, p) ≤ 2 n(p+1) . As we will see below, this can not be significantly improved. In fact, we conjecture that for all n ≥ 1 and p ≥ 2, we have N 3 (n, p) = 2 p n -1 p-1 + 1 : this was found and machine-checked for all n + p ≤ 17 thanks to an implementation of agents and their reduction, unfortunately we could not prove its correctness, nor generalize it to higher depths.

Lower bound

As argued in the introduction, the upper bound above applies to several programming languages executed by head linear reduction, possibly featuring non determinism and/or ground type references, therefore the fact that we used game semantics to prove it increases its generality. On the other hand, if we try to give the closest possible lower bound for N d (n, p) using the full power of visible pointer structures, we would get a lower bound without meaning for most languages concerned by the upper bound, since pointer structures have no innocence or determinism requirements 8 . Therefore what makes more sense is to describe a lower bound in the more restricted possible framework, i.e. simply typed λ-calculus.

We won't detail the construction much, as the method is standard and does not bring a lot to our analysis. The idea is to define higher types for church integers by A 0 = ⊥ and A n+1 = A n → A n . Then, denoting by n p the church integer for n of type A p+2 , we define S n = 2 n 2 n-1 . . . 2 0 : A 2 . We apply then S n to id ⊥ to get a term whose head linear reduction chain has at least 2 1 n+1 steps. In game semantics, 2 n has size n + 3 and all other components have size smaller than n + 2, the depth of the ambient arena being n + 2. The function N d (n, p) being monotonically increasing in all its parameters we have the following inequalities for 3 ≤ d ≤ min(n -1, p), both bounds making sense for all programming languages containing the simply-typed λ-calculus and whose terms can be interpreted as bounded strategies.

2 2 d-2 ≤ N d (n, p) ≤ 2 n(p+1) d-2
Note that from this we can deduce bounds for N (n, p), when we have no information on the depth of the ambient arena. Indeed, we always have d ≤ 2n and d ≤ 2p + 1 because a pointer chain in a play is visible by both players. Thus, N (n, p) = N min(2n,2p+1) (n, p).

Application to head linear reduction

Earlier works on game semantics [START_REF] Vincent Danos | Game semantics and abstract machines[END_REF] suggest that in every games model of a programming language lies a hidden notion of linear reduction, head linear reduction when modelling call-by-name evaluation: this is the foundation for our claim that our game-theoretic result is really about the length of execution in programming languages whose terms can be described as bounded strategies.

Of course it requires some work to interface execution in these programming languages to our game-theoretic results, and part of this work has to be redone in each case. To illustrate this, we now describe how to extract from our results a theorem about the length of head linear reduction sequences in simply-typed λ-calculus. For the formal definition of head linear reduction, the reader is directed to [START_REF] Danos | How abstract machines implement head linear reduction[END_REF]. If S is a λ-term then the spinal height of S is the quantity sh(S) defined by induction as sh(x) = 1, sh(λx.S) = sh(S) and sh(ST ) = max(sh(S), sh(T ) + 1); when S is a βη-normal form, sh(S) is nothing but the height of its Böhm tree. The height of S is the subtly dif- 8 Our experiments with pointer structures and agents confirmed indeed that the possibility to use non-innocent behaviour does allow significantly longer plays. ferent quantity9 h(S) defined by h(x) = 1, h(λx.M ) = h(M ) and h(M N ) = max(h(M ), h(N )) + 1. Finally, the level of a type lv(A) is defined by lv(⊥) = 0 and lv(A → B) = max(lv(A) + 1, lv(B)) and the degree g(S) of a term is the maximal level of the type of all subterms of S.

A game situation [START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF] is the data of λ-terms S : A 1 → . . . → A p → B and T 1 : A 1 , . . . T p : A p in η-long β-normal form, and we are interested in the term ST 1 . . . T p . Our game-theoretic results apply immediately to game situations, because of the connection between game-theoretic interaction and head linear reduction [START_REF] Vincent Danos | Game semantics and abstract machines[END_REF]: if N (ST 1 . . . T p ) denotes the length of the head linear reduction chain of ST 1 . . . T p , then we have N (ST 1 . . . T p ) ≤ N d (n, p) where d is the depth of the arena corresponding to A → B, n is the size of S and p is the maximal size of all of the T i . But since S and T i are already in η-long β-normal form, we have | S | = sh(S) and | T i | = sh(T i ). Thus, we conclude that in the case of a game situation we have:

N (ST 1 . . . T p ) ≤ 2 sh(S)(maxi(sh(Ti))+1) maxilv(Ai)-1
Outside of game situations, it is less obvious to see how our results apply. The more elegant approach would be probably to extend the connection between head linear reduction and game semantics to revealed semantics, which would give the adequate theoretical foundations to associate an agent to any η-long λ-term. Without these tools, we can nonetheless apply the following hack. Suppose we have a λ-term S. The idea is to "delay" all redexes, replacing each redex (λx.S)T of type A → B in S with y A,B (λx.S)T , where we add a new symbol y A,B : (A → B) → A → B for each pair (A, B). We iterate this operation until we reach a β-normal λ-term S t , which satisfies sh(S t ) ≤ h(S). We then expand S t to its η-long form η(S t ), which satisfies sh(η(S t )) ≤ sh(S t )+ g(S t ) ≤ h(S) + g(S) + 1. We consider now the term (λy 1 . . . y p .η(S t ))ev 1 . . . ev p , where each y i binds one of the new symbols y A,B , and ev i : (A → B) → A → B is the (η-long form of) the corresponding evaluation λ-term. We recognise here a game situation, whose head linear reduction chain is necessarily longer than for S (we have only added steps due to the delaying of redexes and η-expansion). Using the inequality above for game situations, we conclude:

N (S) ≤ 2 (h(S)+g(S)+1)(g(S)+1) g(S)

Conclusion & future work

Applied to head linear reduction on simply typed λ-calculus, our results show that the price of linearity is not as high as one might expect. Not only the bounds remain in E 4 , but they are only slightly higher than those for usual β-reduction: in particular, the height of the tower of exponentials is the same.

A strength of our method is that it is not restricted to λ-calculus; the results should indeed immediately apply as well to similar notions of reduction on other total programming languages. Beyond ground type references and non determinism, there are also games model of call-by-value languages [START_REF] Abramsky | Call-by-value games[END_REF] generating pointer structures as well, thus this work should also provide bounds for the corresponding call-by-value linear reduction (tail linear reduction?). All the tools used here also can be extended to non-alternating plays [START_REF] Laird | A game semantics of the asynchronous π-calculus[END_REF], which suggests that this work could be used to give bounds to the length of reductions in some restricted concurrent languages.

We also agents are worth studying further. Their combinatorial nature and their connection to execution of programs may prove interesting for the study of higher order systems with restricted complexity, such as light linear logics [START_REF] Girard | Light linear logic[END_REF]. For instance, proofs typable in light systems may correspond to agents with some restricted behaviours, which would make them a valuable tool for the study of programming languages with implicit complexity. by definition of P -view it is {s n1 , . . . , s np , s i } where {s n1 , . . . , s np } is the context of (s, i). Since (s, i) ∈ T r(n[a 1 , . . . , a p ]) we have as required (s, n k ) ∈ coT r(a k ) for each k ∈ {1, . . . , p} and (s, i) ∈ coT r(b) because (s, i) ∈ a ⋆ d b. For the third part, we have to prove that the depth of s relative to i + 1 is at most d -1, but it is obvious since the depth relative to i is at most d and s i+1 → s i .

• Otherwise, we have s i+1 → s nj for j ∈ {1, . . . , p}. Then, we claim that (s, i+1) ∈ a j ⋆ di-1 (n- a for all α ≤ α ′ and ρ ≤ ρ ′ .

Proof. By induction on a.

Lemma 9 (Null substitution lemma). If ρ α a(∅) and the type of x in a is 0, then for all agent b we still have ρ α a(b). Moreover, the witness includes as many Cut rules as for ρ α a(∅).

Proof. We prove by induction on the tree witness for ρ α a(∅) that the above property is true for all context-arena a ′ such that a(∅) = a ′ (∅).

• Base. The root of a is 0, hence the result is trivial.

• Red. Suppose a ′ has the form n[{d 1 }a 1 , . . . , {d p }a p , {d}x], where a 1 , . . . , a p possibly include occurrences of x (the case where x appears as a son of the root encompasses the other). The premises of Red are then that for

1 ≤ i ≤ p such that d i ≥ 1, ρ α-1 a i (∅)• di-1 (n-1)[{d 1 }a 1 (∅), . . . {d p }a p (∅)]
and ρ α-1 (n -1)[{d 1 }a 1 (∅), . . . {d p }a p (∅)]. The induction hypothesis on these premises give witnesses for the two following properties: Proof. We prove by induction on the tree witness for ρ α a(∅) that the above property is true for all context-arena a ′ such that a(∅) = a ′ (∅).

ρ α-1 (a i • di-1 (n -1)[{d 1 }a 1 , . . . , {d p }a p , {d}x])(b) (1)
• Base. The root of a is 0, hence the result is trivial.

• Red. Suppose a ′ has the form n[{d 1 }a 1 , . . . , {d p }a p , {d}x], where a 1 , . . . , a p possibly include occurrences of x (the case where x appears as a son of the root encompasses the other). The premises of Red are then that for

1 ≤ i ≤ p such that d i ≥ 1, ρ α-1 a i (∅)• di-1 (n-1)[{d 1 }a 1 (∅), . . . {d p }a p (∅)]
and ρ α-1 (n -1)[{d 1 }a 1 (∅), . . . {d p }a p (∅)]. The induction hypothesis on these premises give witnesses for the two following properties:

ρ (α-1)(β+1) (a i • di-1 (n -1)[{d 1 }a 1 , . . . , {d p }a p , {d}x])(b) (3) ρ
(α-1)(β+1) ((n -1)[{d 1 }a 1 , . . . {d p }a p , {d}x])(b) (4)
By hypothesis we have ρ β b, hence by Cut (since d -1 ≤ ρ), we have: Proof. By induction on the tree witness for ρ+1 α a.

ρ (α-1)(β+1)+β b • d-1 (n -1)[{d 1 }a 1 (b), . . . {d p }a p (b), {d}b] (5)
• Base. Trivial.

• Red. Suppose a = n[{d 1 }a 1 , . . . , {d p }a p ], the premises of Red are ρ+1 α-1 If n = 0 this is exactly Base. Otherwise we apply Red. There is no possible reduction, so the only thing we have to prove is ρ α+n-1 (n -1)[], which is provided by the induction hypothesis. Then we prove the lemma by immediate induction on a, using only Base', Cut and Lemma 8.

a i • di-1 (n -1)[{d 1 }a 1 , . . . ,
From now on, let N (a) denote the longest reduction sequence of a. We also use the notations 2 n 0 = n and 2 n d+1 = 2 2 n d for iterated exponentials.

Lemma 13 (Bound lemma). Let a be an agent, then if 0 α a, N (a) ≤ α.

Proof. First of all we prove that if there is a witness for 0 α a, then it can be supposed Cut-free: this is proved by induction on 0 α a, eliminating each use of Cut by Lemma 9. Then, by induction on the Cut-free witness tree for 0 α a:

• Base. Then, the root of a is 0, thus N (a) = 0; there is nothing to prove.

• Red. The premises of 0 α a include in particular that for all a ′ such that a a ′ , we have 0 α-1 a ′ . By induction hypothesis, this means that for all such a ′ we have N (a ′ ) ≤ α -1, hence N (a) ≤ α.

From all this, it is possible to give a first upper bound by using the recomposition lemma, then iterating the cut elimination lemma. However, we will first prove here a refined version of the cut elimination lemma when ρ = 1, which will allow to decrease by one the height of the tower of exponentials. First, we need the following adaptation of the substitution lemma: Proof. We prove by induction on the tree witness for 0 α a(∅) that the above property is true for all context-arena a ′ such that a(∅) = a ′ (∅).

• Base. The root of a is 0, hence the result is trivial. .

  where λ A means λ A with polarity O/P reversed), I A⇒B = I B and ⊢ A⇒B =⊢ A + ⊢ B +I B × I A . Composition. We define composition of strategies by the usual parallel interaction plus hiding mechanism. If A, B and C are arenas, we define the set of interactions I(A, B, C) as the set of justified sequences u over A, B and C such that u ↾A,B ∈ L A⇒B , u ↾B,C ∈ L B⇒C and u ↾A,C ∈ L A⇒C . Then, if σ : A ⇒ B and τ : B ⇒ C, we define parallel interaction as σ || τ = {u ∈ I(A, B, C) | u ↾A,B ∈ σ ∧ u ↾B,C ∈ τ }, composition is then defined as σ; τ = {u ↾A,C | u ∈ σ||τ }.

Lemma 2 .

 2 Let n and p be natural numbers and d ≥ 2, then N d (n, p) = max{|s| | s ∈ n ⋆ d p} Proof. Consider the maximal bounded strategies of respective size n and p, defined as n = {s ∈ I d | ∀s ′ ⊑ s, | s ′ | ≤ 2n and p = {s ∈ I d-1 | ∀s ′ ⊑ s, | s ′ | ≤ 2p. Then pointer structures in n ⋆ d p are the same as (passive) interactions in p||n, thus max{|s| | s ∈ n ⋆ d p} ≤ N d (n, p). Reciprocally, if σ : A ⇒ B has size p and τ : B ⇒ C has size n and if u ∈ σ||τ is passive, then if u ′ denotes u where moves are considered up to ∼ = we have u ′ ∈ p||n thus u ′ ∈ n ⋆ d p and N d (n, p) = max{|s| | s ∈ n ⋆ d p}.

  (n > 0), we define the non-deterministic reduction relation on triples (a, d, b), where d is a depth (a natural number) and a and b are agents, by the following two cases: (n[{d 1 }a 1 , . . . , {d p }a p ], d, b) (a i , d i -1, (n -1)[{d 1 }a 1 , . . . , {d p }a p , {d}b]) (n[{d 1 }a 1 , . . . , {d p }a p ], d, b) (b, d -1, (n -1)[{d 1 }a 1 , . . . , {d p }a p , {d}b])

Figure 1 :

 1 Figure 1: Rewriting rule on agents

Proposition 3 .

 3 Let n, p ≥ 0, d ≥ 2, then N d (n, p) ≤ N (n[{d}p[]]) + 1.

Lemma 3 (

 3 Substitution lemma). If ρ α a(∅), ρ β b and d ≤ ρ + 1 (where d is the type of x in a), then ρ α(β+1) a(b)

Theorem 1 ( 2 Proof. 2 n 2 .

 1222 Upper bound). Let depth(a) denote the highest edge label in a, max(a) means the highest node label and |a| means the number of nodes of a. Then if depth(a) ≥ 1 and max(a) ≥ 1 we have: N (a) ≤ 2 max(a)|a|-1 depth(a)-1 For the particular case when a = n[{d}p[]] and if d ≥ 2 we have: N d (n, p) ≤ 2 n(p+1) d-Both proofs are rather direct. For the first part, by the recomposition lemma we have depth(a) max(a)|a| a. It suffices then to apply depth(a) -1 times the cut elimination lemma, then use the "base" cut-elimination lemma to eliminate the remaining cuts. For the second part we reason likewise, but rely on the substitution lemma instead of the recomposition lemma to get d-1 n(p+1) n[{d}p[]], which gives N (n[{d}p[]]) ≤ But we have N d (n, p) ≤ N (n[{d}p[]]) + 1 by Proposition 3, which concludes the proof.

ρ α- 1 ( 2 )

 12 (n -1)[{d 1 }a 1 , . . . {d p }a p , {d}x])(b) (All the possible reductions are already covered since d = 0, thus by Red we have ρ (α-1)+1 a(b) as required. • Cut. Let us suppose ρ α+γ a(∅) is obtained by Cut, hence a(∅) has the form a 1 (∅) • d1 a 2 (∅). Let us suppose that a ′ has the form (a 1 • d ′ a 2 ) • d x, since once again the case where x is a child of the root of a ′ encompasses the other. The premises of Cut are then ρ α a 1 (∅) and ρ γ a 2 (∅), and d ′ ≤ ρ. Note now that we also have (a 1 • d x)(∅) = a 1 (∅), therefore the induction hypothesis on ρ α a 1 (∅) along with ρ β b and d ≤ ρ + 1 implies that ρ α a 1 (b)• d b. But by induction hypothesis we also have ρ γ a 2 (b), hence by Cut: ρ α+γ (a 1 (b) • d b) • d ′ a 2 (b) Which was what was required for (a 1 (b) • d ′ a 2 (b)) • d b, thus it suffices since trees are considered up to permutation. Lemma 10 (Main substitution lemma). If ρ α a(∅), ρ β b and d ≤ ρ + 1 (where d is the type of x in a), then ρ α(β+1) a(b)

Using ( 3 )

 3 for all i ∈ {1, . . . , p}, (4) (adjusted to ρ (α-1)(β+1)+β by Lemma 8) and[START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF] we deduce by Red thatρ (α-1)(β+1)+β+1 n[{d 1 }a 1 (b), . . . , {d p }a p (b), {d}b]Which is what was required. • Cut. Let us suppose ρ α+γ a(∅) is obtained by Cut, hence a(∅) has the form a 1 (∅) • d1 a 2 (∅). Let us suppose that a ′ has the form (a 1 • d ′ a 2 ) • d x, since once again the case where x is a child of the root of a ′ encompasses the other. The premises of Cut are then ρ α a 1 (∅) and ρ γ a 2 (∅), and d ′ ≤ ρ. Note now that we also have (a 1 • d x)(∅) = a 1 (∅), therefore the induction hypothesis on ρ α a 1 (∅) along with ρ β b and d ≤ ρ+1 implies that ρ α(β+1) a 1 (b) • d b. But by induction hypothesis we also have ρ γ(β+1) a 2 (b), hence by Cut: ρ α(β+1)+γ(β+1) (a 1 (b) • d b) • d ′ a 2 (b) Which was what was required for (a 1 (b) • d ′ a 2 (b)) • d b, thus it suffices since trees are considered up to permutation. Lemma 11 (Cut elimination lemma). Suppose ρ+1 α a. Then if α = 0, ρ 0 a.

2 α- 1 a.2 α- 1 a 1 and ρ 2 β- 1 a 2 , 1 (a 2 ) = a 1 • d a 2 = a, thus ρ 2 α+β- 1 aa 1 and ρ β ′ a 2 .a 1 and ρ 0 a 1 ,

 11121212121 If α = 1, then the premises of Red are ρ+1 0 a i • di-1 (n -1)[{d 1 }a 1 , . . . , {d p }a p ] for all i ∈ {1, . . . , p} and ρ+1 0 (n -1)[{d 1 }a 1 , . . . , {d p }a p ]. By induction hypothesis this is still true with ρ instead of ρ + 1, thus by Red we have ρ 1 [{d 1 }a 1 , . . . , {d p }a p ] which is what we needed to prove. • Cut. Suppose a = a 1 • d a 2 , the premises of Cut are ρ+1 α a 1 , ρ+1 β a 2 and d ≤ ρ + 1. If α, β ≥ 1 then by induction hypothesis it follows thatρ in particular if we define a context-agent a ′ 1 = a 1 • d x we have ρ 2 α-1 a ′ 1 (∅), hence by the substitution lemma (since d ≤ ρ + 1) we haveρ 2 α-1 (2 β-1 +1) a ′ thanks to Lemma 8 (since it is always true than 2 α+β-1 ≥ 2 α-1 (2 β-1 + 1)). If α = 0then by induction hypothesis we have ρ 0 We use then the substitution lemma (since d ≤ ρ + 1) to get ρ 0 (a 1 • d a 2 ), which is stronger that what was required whatever was the value of β. The last remaining case is when α = 1 and β = 0, then by induction hypothesis ρ 1 thus by the substitution lemma we have as required ρ 1 (a 1 • d a 2 ).Lemma 12 (Recomposition lemma). Let a be an agent. Then:depth(a) max(a)|a| aWhere depth(a) is the maximal label of an edge in a, max(a) is the maximal label of a node and |a| is the number of nodes.Proof. First, let us show that the following rule Base' is admissible, for any α and ρ. ρ α+n n[]

Lemma 14 (

 14 Base substitution lemma). If 0 α a(∅), 0 β b and the type of x in a is 1, then 0 α+β a(b).

•α a 1 and 1 β a 2 .Theorem 2 ( 1 2

 221 Cut. Suppose a = a 1 • d a 2 with d ≤ 1, the premises of Cut are that 1 If d = 0, then the result is trivial by the induction hypothesis and Cut. If d = 1, we just apply Lemma 14 instead of Cut. Upper bound). Let depth(a) denote the highest edge label in a, max(a) means the highest node label and |a| means the number of nodes of a. Then if depth(a) ≥ 1 and max(a) ≥ 1 we have: N (a) ≤ 2 max(a)|a|-1 depth(a)-1For the particular case when a = n[{d}p[]] and if d ≥ 2 we have:N d (n, p) ≤ 2 n(p+1) d-2Proof. Let us first prove the first part. By the recomposition lemma, we have depth(a) max(a)|a| a. By depth(a) -1 iterations of the cut elimination lemma, we have max(a)|a|-1 depth(a)-1 a. But then by Lemma 15 also have 0 2 max(a)|a|-1 depth(a)-1 a. By Lemma 13, this implies as required that N (a) ≤ 2 max(a)|a|-1 depth(a)-1 . We turn now to the second part. Obviously, we have d-1 n n[] and d-1 p p[]. By the substitution lemma, this implies that d-1 n(p+1) n[{d}p[]]. By d -2 applications of the cut elimination lemma, and one application of Lemma 15, this means that

  the set {s n1 , . . . , s np } of P-moves appearing in s <i , • If s i is a P-move, the set {s n1 , . . . , s np } of O-moves appearing in s <i . Definition 3. A general agent (just called agent for short) is a finite tree, whose nodes and edges are both labelled by natural numbers. If a 1 , . . . , a p are agents and d 1 , . . . , d p are natural numbers, we write: n[{d 1 }a 1 , . . . , {d p }a p ] =

	a 1	n . . . { { { { { { { { d1	dp g g g g g g g g	a

p Definition 4 (Trace, co-trace, interaction). Let us generalize the notion of trace to general agents. The two notions T r and coT r are defined by mutual recursion, as follows: let a = n[{d 1 }a 1 , . . . , {d p }a p ] be an agent. We say that (s, i) is a trace (resp. a co-trace) of a, denoted (s, i) ∈ T r(a) (resp. (s, i) ∈ coT r(a)) if the following conditions are satisfied:

  Definition 5. The predicate ρ α (where ρ, α range over natural numbers) is defined on agents in the following inductive way. • Base. ρ α 0[{d 1 }a 1 , . . . , {d p }a p ] • Red. Suppose a = n[{d 1 }a 1 , . . . , {d p }a p ]. Then if for all a ′ such that a a ′ we have ρ α a ′ and if we also have ρ α (n -1)[{d 1 }a 1 , . . . , {d p }a p ],

  [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF][{d 1 }a 1 , . . . , {d p }a p , {d}b]. We do have (s, i+1) ∈ T r(a j ) because (s, i) ∈ T r(n[{d 1 }a 1 , . . . , {d p }a p ]), thus (s, n j ) ∈ coT r(a j ) and (s, i + 1) ∈ T r(a j ) by Lemma 7. It remains to show that (s, i + 1) ∈ coT r((n -1)[{d 1 }a 1 , . . . , {d p }a p , {d}b]) and that the depth of s relative to i + 1 is at most d 1 -1, but the proofs are exactly the same as in the previous case.

	B Upper bound
	Lemma 8 (Monotonicity). If ρ α a, then ρ ′ α ′

However, there are syntaxes on which head linear reductions appear more canonical that β-reduction, for instance proof nets[START_REF] Mascari | Head linear reduction and pure proof net extraction[END_REF].

Note however that in[START_REF] De Bruijn | Generalizing Automath by means of a lambda-typed lambda calculus[END_REF], De Bruijn gives an upper bound for his local β-reduction, akin to head linear reduction. The bound is an iterate of the diagonal of an Ackermann-like function!

In the terminology of[START_REF] Harmer | Innocent game semantics[END_REF], it is the long O-view.

Or, more adequately, the fan theorem.

The syntax used here seems natural enough, but is for instance described in[START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF].

As in the example above, closures are pairs M σ where M is an open term and σ is an environment, i.e. a mapping which to each free variable of M associates a closure.

So starting from s j and following Opponent's pointers eventually reaches s i .

One can easily prove that on closed terms, it is always less than the more common notion of height defined as h(x) = 0, h(λx.S) = 1 + h(S) and h(ST ) = max(h(S), h(T )) + 1, for which our upper bound consequently also holds.

Acknowledgements. This work was partially supported by the French ANR project CHOCO. The author also would like to thank Fabien Renaud for interesting discussions on related subjects.

A pointer structures and rewriting Lemma 7. Let s be a pointed visible pointer structure and a = n[{d 1 }a 1 , . . . , {d p }a p ] an agent such that (s, i) ∈ coT r(a). Then if s j → s i , (s, j) ∈ T r(a).

Proof. Let us suppose without loss of generality that s i is an Opponent move; the other case can be obtained just by switching Player/Opponent and Pviews/O-views everywhere. Then s j being a Player move, we have to check first that rsize(s, j) ≤ 2n, i.e.

and the inequality is obvious. We need now to examine the context of (s, j). Since s j is a Player move, it is defined as the set {s n1 , . . . , s np } of Player moves appearing in s <j , which is also the set of Player moves appearing in s <i and therefore the co-context of (s, i). But (s, i) ∈ coT r(a), hence for all k ∈ {1, . . . , p} we have (s, n k ) ∈ coT r(a k ) which is exactly what we needed.

Proof. Suppose a = n[{d 1 }a 1 , . . . , {d p }a p ]. Let {s n1 , . . . , s np } be the context of (s, i). By visibility, s i+1 must either point to s i or to an element of the context. Let us distinguish cases.

• If s i+1 → s i , then we claim that (s, i+1) ∈ b⋆ d-1 (n-1)[{d 1 }a 1 , . . . , {d p }a p , {d}b],

i.e (s, i + 1) ∈ T r(b), (s, i + 1) ∈ coT r((n -1)[{d 1 }a 1 , . . . , {d p }a p , {d}b]) and the depth of s relative to i+1 is at most d-1. For the first part, we use that (s, i) ∈ a ⋆ d b : in particular, (s, i) ∈ coT r(b) and since s i+1 → s i this implies by Lemma 7 that (s, i + 1) ∈ T r(b). For the second part, we must first check that rcosize(s, i + 1) ≤ 2(n -1) + 1. Let us suppose without loss of generality that s i is an Opponent move, all the reasoning below can be adapted by switching Player/Opponent and P -views/O-views everywhere. We want to prove:

Thus we only need to remark that | s ≤i+1 | = | s ≤i | + 1 since s i+1 is a Player move. Now, we must examine the co-context of (s, i + 1), but

• Red. Suppose a ′ has the form n[{d 1 }a 1 , . . . , {d p }a p , {d}x], where a 1 , . . . , a p possibly include occurrences of x (the case where x appears as a son of the root encompasses the other). The premises of Red are then that for

and 0 α-1 (n -1)[{d 1 }a 1 (∅), . . . {d p }a p (∅)]. The induction hypothesis on these premises give witnesses for the two following properties:

By hypothesis we have 0 β b, hence by Lemma 9 (since d = 1) we have

Hence, using ( 6) for all i ∈ {1, . . . , p}, (7) and (B) (adjusted to Proof. By induction on the witness tree for 1 α a.

• Base. Trivial.

• Red. Suppose a has the form n[{d 1 }a 1 , . . . , {d p }a p ]. The premises of Red are that for all i ∈ {1, . . . , p} we have 1 α-1 a 1 • di-1 (n-1){d 1 }a 1 , . . . , {d p }a p ] and 1 α-1 (n-1){d 1 }a 1 , . . . , {d p }a p ]. The result is then trivial by induction hypothesis and Red.


C Lopez
email: lopez@lirmm.fr

V Prince
email: prince@lirmm.fr

M Roche
email: mroche@lirmm.fr

Automatic Generation Approach of Short Titles

Keywords: information retrieval, automatic titling, text-mining

Automatic titling of text documents is an essential task for several applications (automatic heading of e-mails, summarization, and so forth). In this article, we present a technique that suggests titles showing coherence with both the text and the Web, as well as with their dynamic context. The approach evaluation indicates that automatically generated titles are informative and/or catchy.

Introduction

A title is an important element of a textual document. It can be seen as a semantic object with three functions: Interest/captivate the reader, inform the reader, introduce the subject of the article. Numerous applications bound to automatic titling are possible. One of the immediate applications is to provide a title for those documents such as "no object" e-mails, or comments on fora, and blogs. Another is the automatic titling of stream texts, beforehand structured by a thematic segmentation task. On-line newspapers develop and publish numerous articles every day. Most known European newspapers publish one article every few minutes. An automatic titling tool would help time saving for journalists, by providing informative and catchy headlines. Finally, an application of Web pages titling would allow to respect one of the standard W3C criteria.

In this paper, we describe a system that automatically generates short titles (ST) using Web Mining. The target language is French, but the method can be easily transposed to most Western languages (an experiment is currently conducted for English). From syntactical patterns stemming from statistical analyses on human written titles (section 3.1), ST candidates are shaped (section 3.2). The main problem is that several ST can be relevant for the same text (or text section). They can vary, according to their size (in number of words), their shape, and their highlighted topic. The ST candidate will thus be subject to a validation in two phases: (1) Candidates coherence as acceptable (meaningful, well-formed) phrases present in the text (section 3.3.1), (2) Or present / popular in Web pages (section 3.3.2). ST candidates are then contextualized (section 3.4 and 3.5), a technique that filters the most relevant candidate for the handled text section. Evaluation (section 4) indicates that the selected ST are relevant.

Previous Works

Among several works in the domain, some of the oldest have noticed that items appearing in a title were often present in the body of the text [START_REF] Baxendale | Man-made index for technical literature -an experiment[END_REF]. More recent works (e.g., [START_REF] Lopez | Automatic titling of electronic documents by noun phrase extraction[END_REF]) have consolidated this idea and shown that the frequency of titles words is very important within the document body. So, a big part of the information allowing title determination, is already in the document. Some of the cited authors have already proposed a method extracting noun phrases (NP) from texts data, and ranking them as possible candidates for the role of document head phrase [START_REF] Lopez | Automatic titling of electronic documents by noun phrase extraction[END_REF]. In their approach, one of the benefits is that long titles can be proposed. The main inconvenience is that the produced titles are not original, and can neither be idiomatic nor metaphorical. Besides, the approach efficiency is limited by the absence (or weak presence) of relevant NPs in the text. Furthermore, this approach has limits about short noun phrases. Approach evaluation indicates that only 60% of "noun adjective" or "adjective noun" titles are informative and 5% are catchy.

In [START_REF] Jin | A new probabilistic model for title generation[END_REF], a probabilistic model for title generation is proposed, based on the use of TF-IDF. This model is considered as effective in creating human readable titles, but it does not take into account syntactic coherence.

To remedy to these problems, this study proposes an approach using the Web. It tries to generate short titles, by combining elements already present in the text (at first).

Automatic Generation of Short Titles

In this paper, we are interested in short titles generation. Our approach determines a global process consisting in three main steps: Shaping candidate titles (section 3.2), discussing the candidates coherence (section 3.3), and dynamic contextualization of candidate titles (section 3.4).

3.1Statistical Analysis

We consider the subtitles of journalistic articles as short titles. So, our statistical study is performed on journalistic articles subtitles, in order to determine these patterns. Our corpus was established from Factiva, selecting 200 French journalistic articles stemming from the French daily paper 'Le Monde' (in November, 2010) and containing at least a subtitle. With the aim that results were not biased by the possible errors inferred by the choice of a morphosyntactic tagger, subtitles were manually analyzed, according to 4 morphosyntactic patterns containing Common Nouns (CN), ADJectives (ADJ), and Grammatical Words (GW: articles, determiners, prepositions, etc.). 12% of subtitles have a "CN" form, 43% of subtitles have a "CN ADJ" or "ADJ CN" form, 14% of subtitles have a "CN GW CN" form, and 26% of subtitles contain four words or more. Considering these results, we focused on the automatic generation of titles of the "CN ADJ " and "ADJ CN" forms, which cover 43% of journalistic subtitles stemming from 'Le Monde' articles. The following section consists in building candidate titles with a "CN ADJ" and "ADJ CN" form.

Generation of Candidates Titles

The generation of candidate titles relies on the TF-IDF score [START_REF] Salton | Term-weighting approaches in automatic text retrieval[END_REF]. The purpose is to extract common nouns and relevant adjectives from the text. The text is tagged (without lemmatization) with TreeTagger [START_REF] Schmid | Probabilistic part-of-speech tagging using decision trees[END_REF]. For every extracted common noun, a score corresponding to the TF-IDF (noted TF-IDF CN ) is attributed, allowing to classify the common noun by order of relevance to the text. On the other hand, for every extracted adjective, a score corresponding to the simple TF (noted TF ADJ ) is attributed. This method favors the most frequent adjectives of the text, discarding specific ones (by not using IDF). Specificity must be an attribute of the common noun, since it governs the phrase.

In the text to be titled, three common nouns with the highest TF-IDF values and ten adjectives with highest TF values are extracted. This limit is due to the limited queries on search engines. The following section describes the candidate titles coherence determination.

Coherence of Candidate Titles

While potentially relevant couples were built in the previous section, in this section we determine which ones are coherent, grammatically and semantically, for their use as headings. This coherence is estimated according to the document itself (section 3.3.1), then, by browsing the Web (section 3.3.2).

According to the text

The coherence of the terms composing every title candidate with regard to the text is assured by the use of the TF-IDF, during their generation (see section 3.2). In this way, common nouns and most relevant adjectives for titling are extracted. We use the distance (in number of words) between the CN and ADJ, as a new criterion of coherence in candidate titles. This distance, noted Dist(CN,ADJ) , is computed for every candidate and used in the computation of the distance coefficient (formula (1)). This distance is applied as a coefficient in the score defined for every candidate.

(1)

According to the Web

Candidate titles (CT) might not be present as phrases in the text, but might be nevertheless coherent candidates. Another method is to query the Web to assert their plausibility.

As [START_REF] Turney | Mining the web for synonyms: Pmi-ir versus LSA on TOEFL[END_REF], we use the frequency of appearance of bigrams on the Web. This method measures the dependence between the common noun and the adjective composing a candidate title. This is an argument against applying lemmatization. The methods thus automatically favors a well-formed "CN ADJ" couple (eg, "chapeau bas") over a badly built couple (eg, "chapeau basse"). To do so, the best dependence measure has to be chosen. Let nb(X) a function that returns the number of pages sent by the search engine (here, Google) in answer to the query X. For example, nb(CN) returns the number of pages found for X = CN, reecting the popularity of the term CN on the Web. Also, nb(CN,ADJ) returns the number of pages found for X = "CN ADJ".

Mutual Information (MI) [START_REF] Church | Word association norms, mutual information, and lexicography[END_REF], Cubic Mutual Information (MI 3 ), and Dice coefficient are measures based on nb(X) used in Data Mining in order to rank elements. These various statistical measures, adapted to the titling task, help obtaining a classification that tackles the coherence of candidate titles, according to their presence/popularity in Web pages. DICE and MI 3 favor frequent co-occurrences (i.e. the numerator), compared to MI [START_REF] Roche | Text and Web Mining Approaches in Order to Build Specialized Ontologies[END_REF]. Applied to the context of the "CN ADJ" bigrams validation, we obtain the formula (2).

(2)

We chose DICE for the continuation of our study, that gives the best results according to [START_REF] Roche | Text and Web Mining Approaches in Order to Build Specialized Ontologies[END_REF]. To take into account the "ADJ CN" candidate titles (see section 3.1), we retain the maximum value obtained between DICE(ADJ,CN) and DICE(CN,ADJ). Finally, several coherent candidates, according to the text and the Web, might reach the top of the classification. Among these candidate titles, we have to determine which is the most relevant one, by taking into account the context of each candidate.

Dynamic Contextualisation

To determine the most relevant candidate title, we compare the context of the text with the context in which these candidates are met on the Web. Further to the submission of a query (via a Google API), the Google search engine presents the results (list of Web sites). For each of these sites, an outline of the Web page contents is presented (between 10 and 30 words), justifying the returned result, by putting in bold font the terms initially present in the query. The document used for the determination of the Web context of every candidate title is the concatenation of the first 10 outlines (limit imposed by Google) of a given query. As regards the text context, it is determined from the document to be titled body text.

To determine the Web context and the text context, we use Salton's vector model [START_REF] Salton | A vector space model for automatic indexing[END_REF]. For every common noun and adjective of documents (text and Web documents), a TF value is assigned. These figures constitute the coordinates of the contextual vector (TCV for the text and WCV for Web). Finally, to each candidate title, a WCV is associated. If the vocabulary present in a candidate title context (WCV) is close to the vocabulary of the text (TCV), then this candidate is favored. For every candidate title, the cosine similarity (or cosine measure) is used between two vectors covering all the possible (TCV Text , WCV Cand ) couples. So, the retained couples are the ones whose textual context is the "closest" to the Web context.

JDM Contextualisation

JeuxDeMots (JDM) is a Web-based serious game with the purpose of building a popular lexical network [START_REF] Lafourcade | Making people play for lexical acsquisition with the jeuxdemots prototype[END_REF], in several languages (French, English, Spanish, and so forth). If Wordnet is the 'expert' lexical network, JeuxDeMots claims to translate the dynamics of popular usage of a language. In this study, the use of such a lexical network is interesting for the construction of a context that will be associated to every candidate title. The benefit is to generate a context containing terms which do not appear in the text. In the JDM lexical network, a weight is associated with every pair of words, which enables establishing a closeness relation between terms. The process of JDM contextualization is formed by three steps. For each candidate title: (1) Determine the set of nearest terms to CN, (2) Determine the set of nearest terms to ADJ, and (3) Compute the union of terms stemming from both sets (1 and 2) by taking into account weights (the sum of the weights is computed if the term belongs to both sets).

In the previous section, we defined the contextual vector of the text (TCV Text ). A new contextual vector, named JDM, is built for every candidate title, respecting the data structure of TCV Text (i.e. the same terms contribute to vectors). So, it is possible to compute the cosine between every couple of vectors (TCV Text , JDM Cand ). Couples obtaining a cosine close to 1 are considered as the most relevant. So, they indicate the candidate titles (represented by JDM Cand ) which can be used as a possible heading. In the following section, we describe a global measure combining the notion of coherence of the candidate titles and of contextualization.

Global Measure

By relying on the previously defined methods, a global measure, named AutoGT (Automatic Generation of Titles) has been set up, allowing to differentiate the relevant titles from those which are not. It accounts for the coherence of the candidate titles according to the Web and to the text.

It illustrates their ability to be contextually adequate. This global measure supplies a global rank function, taking into account all the concepts of this study. TI Cand is the function applied to a title candidate, which is the product of the TF-IDF of the common noun and the TF-IDF of the adjective (formula (3)).

(3) Considering TI Cand in AutoGT accounts for the relevance of the information contents in the terms composing the candidate titles. In this formula, WCV Cand could be replaced by JDM Cand if we prefer take into account the JDM context rather than the text context (TCV Text ).

(4)

With

, .

is always included between 0 and 1. So, with the use of the logarithm function, incoherent titles (lower than the K threshold compared with the DICE measure) will always be negative. Besides, the candidates classification (via DICE) of negative titles will also be maintained, since log 2 is a strictly increasing function (i.e., Coef Dist and TI Cand are always positive).On the contrary, coherent titles (above the K threshold) will be always positive, since the formula includes "1"which corresponds to the maximum DICE possible value.

Finally, the classification with contextual distance (cos(TCV Text , WCV Cand )) respects the order established by the cosine. We use the Coef Dist distance in order to privilege, among the coherent candidates and contextually relevant, those which are constituted by near terms in the text (see section 3.3.1). Finally, candidate titles that obtain a positive result are considered relevant by our measure. The candidate obtaining the highest score is retained for its use as title. The choice of the K threshold is crucial. In the following section, we propose a value of K, and estimate our AutoGT measure.

Evaluations

This section is dedicated to the evaluation of the titles generated by our approach according to several criteria. Once threshold K fixed, the AutoGT measure can be estimated.

K Threshold Determination

The results brought by the AutoGT measure strongly depend on the K relevance threshold. The behavior of this threshold is analyzed from the first 10 articles appeared on January 1st, 1994 in 'Le Monde' newspaper, that is 900 titles estimated manually (10 articles x 3 thresholds x 30 candidates). We shall not try to judge the acceptability of the thirty candidates (see section 3.2) but only their grammaticality. Various thresholds K(n) are tested (with n ∊{1, 10, 100}), based on the average of the values returned by the Dice measure (formula ( 7)).

This determination of K relies on precision (P), recall (R), and F-measure (F), which are classic methods of evaluation in text mining. Within the framework of these measures, an appropriate title is a grammatically correct title. The results indicate that the best compromise between precision and recall is obtained with K(10). In this study, we shall thus use the K(10) threshold, to be applied in AutoGT evaluation (formula (5)).

(5)

Evaluation of AutoGT

The automatically generated headings have to present the same characteristics as real titles, defined in the section 2. The first criterion concerns the information conveyed by the title, which has to be in connection with the handled text. If this requirement is met, we may conclude that the title is informative (noted I). Besides, a title will be considered catchy (noted C) if it contains a funny/humorous form (e.g. a pun), an expression or another construction that can surprise the reader, grammatically correct and informative (in connection with the text). This is the second requirement. Indeed, it will not be suitable to judge a catchy title if it is not in connection with the text. For example, the title "Chapeau bas" can be considered as informative (in this example, the text tribute to a fashion dressmaker who proposes hats) and catchy (use of expression, meaning 'congratulations'). If the text did not speak about hats and if it is not connected with the expression "Chapeau bas", we could not consider the title "Chapeau bas" as catchy, although it is an expression. This evaluation aims at detecting if those titles are "relevantly catchy".

We use the classical methods of evaluation (precision and recall). The evaluation is run on journalistic articles stemming from the daily newspaper Le Monde. We retained the first 20 articles published on January 1st, 1994. So, 600 titles (20 articles x 1 threshold x 30 candidates) stemming from the AutoGT method, while using the K(10) threshold (see section 4.1) which were manually estimated according to I and C (that is 1,200 expertises all in all). 1,460 queries on the search engine were necessary. Firstly we present the evaluation of the AutoGT method, using dynamic contextualization.

T1

Recall Precision F-measure I C I C

Besides, for every article, the highest score title returned by AutoGT, noted T1, is estimated. We note "yes" when the requirement is respected and "not" otherwise. The presence of "x" indicates that no title among 30 candidate titles corresponds to the expected requirements. For example, among 30 candidates built from the article 1, no one is informative or relevant. Focusing on informative titles, they obtain a precision of 40% compensated with a recall of 82%.

Since a T1 title is informative in 75 % of the cases, we can deduce that the K threshold must be refined to retain fewer candidate titles. The evaluation indicates that 75% of the T1 titles are informative and 30% are catchy (see Table 1). So, among the proposed informative titles, 40% are catchy, what constitutes a positive point for our approach.

In the evaluation using JDM context, we were only interested in the generated titles which were different depending on the used context. This evaluation is based on the first 10 articles of Le Monde (1994) where the titles automatically determined depend on the choice of the context. Results indicate that using JDM as a context is beneficial for the AutoGT method, independently from the aimed requirements (I and C): 60% of titles are informative with JDM (30% without JDM) and 30% of titles are catchy with JDM (10% without JDM). When titles generated with Web and JDM are different, JDM obtains better results (twice as relevant). Finally, we compare AutoGT based on T1 titles with a method of phrase extraction (PhrEx) as [START_REF] Lopez | Automatic titling of electronic documents by noun phrase extraction[END_REF]. PhrEx evaluation indicates that only 60% of "noun adjective" or "adjective noun" titles are informative and 5% are catchy.

Conclusions and Future Work

The automatic generation of titles is a complex task because titles has to be coherent, grammatically correct, informative, and catchy. In this article, we proposed an approach allowing the automatic generation of short titles. Having selected the coherent candidates by Web Mining methods, the informative and catchy titles are filtered by the AutoGT measure scores. Evaluation shows that this approach provides relevant headings to 75 % of the journalistic articles composing the corpus.

Contextualization is an important step of the method. Dynamically performed, it builds a title in terms of closeness to the text and to its plausibility according to the Web. A future work will consist in taking into account a context defined by the user. For example, the generated titles could depend on a political context if the user chooses to select a given thread. Furthermore, an "extended" context, automatically determined from the user's choice, could enhance or refine user's desiderata.


Fabio Lucchini
email: fabio.lucchini.83@gmail.com

An irrationality criterion involving recurring sequences

published or not. The documents may come

An irrationality criterion involving recurring sequences

Introduction

Let f ∈ C[X] be a polynomial of degree d > 1 and leading coefficient c = 0. Given x 0 , y 0 ∈ C, consider the recurring sequences x n , y n (n ∈ N) defined by

x n+1 = f (x n ), y n+1 = cy d n . Note that if x n → ∞ then x n+1 ∼ cx d n .
This lead to the following question: given x 0 ∈ C such that x n → ∞ there exists y 0 ∈ C such that x n ∼ y n ?

If f is a polynomial of the form c(X -a) d + a for some a ∈ C the answer is affirmative for if we take y 0 = x 0 -a then y n = x n -a for each n ∈ N hence x n ∼ y n whenever x n → ∞.

The next theorem states that, under certain arithmetical hypothesis, the polynomials c(X -a) d + a are the only ones with this property.

Theorem 1.1. Let f ∈ Z[X] be a polynomial of degree d > 1 and leading coefficient c = 0. Suppose that there exists two unbounded sequences x n , y n (n ∈ N) such that

x n+1 = f (x n ), y n+1 = cy d n and
x n ∼ y n as n → +∞. If x 0 is integer and y 0 is rational then there exists

a ∈ Q such that f (X) = c(X -a) d + a.
Note that the sequences x n , y n are actually divergent: this follows from the explicit formula

y n = c d n -1 d-1 y d n 0
which implies that y n is unbounded if and only if

cy d-1 0 > 1 (1)
and in this case y → ∞.

The proof of 1.1 follows several steps. The first (section 2) consist to show that the sequence x n admits a power series expansion in y n of the form

x n = y n + a 0 + a 1 y -1 n + a 2 y -2 n + • • • with a i ∈ Q. This guarantees (section 3) that given k ∈ N there exists two polynomials a, b ∈ Q[X] with a = 0 such that a(x n )y n = b(x n ) + o(y -k n )
as n → +∞. If x 0 is integer and y 0 rational, then the error term o(y -k n ) can be eliminated, so that y n can be written as a rational function of x n that's

y n = γ(x n ) eventually, where γ = b/a ∈ Q(X). Then γ satisfy the functional equation γ(f (X)) = cγ(X) d in Q(X). Doing arithmetic in Q[X]
(section 4) we conclude that this is possible if and only if f (X) is of the form c(X + a) d -a with c ∈ Z and a ∈ Q.

Power series expansion

It this section we show that the sequence x n admit a power series expansion in y n of the form

x n = y n + a 0 + a 1 y -1 n + a 2 y -2 n + • • • with a i ∈ Q.
In the sequel we consider complex sequences as functions N → C. Given a complex sequence ξ : N → C and n ∈ N we indicate with ξ n the value of ξ at n, as customary. If ξ, η are complex sequences then ξ + η and ξη are complex sequences defined as

(ξ + η) n = ξ n + η n (ξη) n = ξ n η n .
Finally, ξ τ denote the translate sequence, that's (ξ τ ) n = ξ n+1 . We start by formalizing the notion of power series of a sequences.

Definition 2.1. Let θ be a complex sequences such that θ → 0 and θ = 0 eventually. We say that a complex sequence ξ has a θ-expansion if for each k ∈ N there exists a polynomial p ∈ Q[X] such that

ξ = p(θ) + o(θ k ).
The purpose of this section is to prove the following:

Theorem 2.1. Let f be a complex polynomial with degree d > 1 and leading coefficient c, x, y : N → C be two complex sequences such that

x τ = f (x), y τ = cy d , (2)
x, y → ∞ and x ∼ y. If θ := 1/y and r := x -y, then r has θ-expansion.

Note that r = o(y) and from ( 2) we obtain a recurrence relation for r, namely

r τ = ducy d-1 r + v (3)
where

u := x d-1 + • • • + y d-1 dy d-1 ∼ 1, v := f (x) -cx d = O(y d-1 ).
The first step consist to show that r is bounded. Then an induction argument applied to the recurrence (3) will show that r has θ-expansion.

Lemma 2.2. If r is unbounded then r → ∞.

Proof. From (3) we obtain

|r| τ -|r| ≥ (du |c| |y| d-1 -1) |r| -|v| .
Since u ∼ 1 and y → ∞, there exists ū ∼ 1 such that

du |c| |y| d-1 -1 = dū |c| |y| d-1 ; in particular there exists N ∈ N such that ūn > 1 2 for n > N. Let C > 0 such that |v| ≤ C |y| d-1 and S be the set of n ∈ N with n > N such that |r n | > 2C d|c| .
Then

|v n | < (du n |c| |y n | d-1 -1) |r n | for n ∈ S, consequently |r n+1 | > |r n | > 2C cd for n ∈ S. Thus if n ∈ S then n + 1 ∈ S, hence |r n | > 2C
d|c| eventually. Since C can be choose great as we would, we obtain r → ∞.

Proposition 2.3. The sequence r is bounded.

Proof. Suppose r unbounded and let ̺ := |r/y|. From (3) we obtain

|̺ τ -du̺| ≤ |v| |y| -d (4)
where u ∼ 1 and vy -d = O(y -1 ), from which

̺ τ du̺ = 1 + O 1 r → 1 that's ̺ τ ∼ d̺.
In particular r = 0 eventually, that's ̺ > 0 eventually. Since d > 1 we have

̺ τ -̺ ∼ (d -1)̺ =⇒ ̺ τ -̺ ̺ → d -1
hence from d -1 > 0 and ̺ > 0 follows that ̺ is eventually non-decreasing. Since ̺ → 0 this implies ̺ = 0 eventually that's r = 0 eventually -a contradiction.

Now a proof of 2.1:

Proof. Since r is bounded and θ d-1 v is convergent, from r = 1 cdu (θ d-1 r τ -θ d-1 v)
follows that r is convergent, that's r has a θ-expansion of order 0. Suppose that r admit a θ-expansion of order k ∈ N, that's there exists

p ∈ Q[X] such that r = p(θ) + o(θ k ). Then r τ = p(θ d /c) + o(θ dk ) and since xθ = 1 + θr vθ d-1 = c 1 (1 + θr) d-1 + • • • + c d , with c i ∈ Z hence vθ d-1 = g(θ) + o(θ k+1 ) for some g ∈ Q[X]. Similarly u = (1 + θr) d-1 + • • • + 1 d = h(θ) + o(θ k+1 ).
Since u → 1 we have h(0) = 1 and

r = 1 cd θ d-1 p(θ d /c) -g(θ) + o(θ k+1 ) h(θ) + o(θ k+1 ) = q(θ) + o(θ k+1 ) for some q ∈ Q[X].

Approximation by rational functions

In this section we use the power series expansion obtained in the previous section to show that y can be approximated as a rational function of x, that's given k ∈ N there exists two polynomials a, b ∈ Q[X] with a = 0 such that

a(x)y = b(x) + o(θ k ).
Let E (θ) be denote the set of infinitesimal complex sequences which has a θ-expansion.

Lemma 3.1. Let ξ be a complex sequence which as a θ-expansion. For all k ∈ N there exists p ∈ Q[X] and η ∈ E (θ) such that ξ = p(θ) + θ k η.

Proof. Given k, by definition there exists a polynomial p ∈ Q

[X] such that ξ = p(θ) + o(θ k ). Define η := ξ -p(θ) θ k .
We prove that η ∈ E (θ). Certainly η is infinitesimal. Given h ∈ N, we claim that there exists a polynomial q ∈ Q[X] such that η = q(θ)

+ o(θ h ). Let p ∈ Q[X] such that ξ = p(θ) + o(θ h+k ). Then p(θ) -p(θ) = o(θ k ) hence there exists a polynomial q ∈ Q[X] such that p -p = X k q. Consequently, η = p(θ) -p(θ) + o(θ h+k ) θ k = q(θ) + o(θ h )
which conclude the proof. Now we shall investigate the structure of the set of sequences that admit θ-expansion. From the relation xθ = 1 + rθ, follows that the vector space S := Q[x] + E (θ) is closed by multiplication by x. More explicit:

Proposition 3.2. For every ξ ∈ S and a ∈ Q[X] there exists b ∈ Q[X] such that a(x)ξ -b(x) ∈ E (θ).
Proof. It's enough to prove the statement for ξ ∈ E (θ) and a = 0. By previous Lemma there exists a 0 ∈ Q and η ∈ E (θ) such that ξ = a 0 θ + ηθ. Proof. By Proposition 3.2 for every j = 0, . . . , k there exists b

j ∈ Q[X] such that x j ξ -b j (x) ∈ E (θ), that's x j ξ -b j (x) = p j (θ) + o(θ k ),
where p j ∈ Q[X]. We can assume p j = 0 or deg p j ≤ k, for all j. Since p j (0) = 0 for every j, the polynomials p 0 , . . . , p k are linearly dependent over Q. Thus there exists a 0 , . . . , a k ∈ Q not all 0 such that a 0 p 0 +

• • • + a k p k = 0 in Q[X]. Put a := a 0 + • • • + a k X k = 0 and b := a 0 b 0 + • • • + a k b k , then a(x)ξ = b(x) + o(θ k ).
Theorem 3.4. Under the assumption of 1.1, there exists

γ ∈ Q(X) \ Q such that γ(f (X)) = cγ(X) d .
Proof. If x 0 ∈ Z then x is an integer valued sequence. If y 0 is rational, there exists u 0 , v 0 integer with v 0 > 0 (without common factors) such that y 0 = u 0 v 0 . The sequences u τ = cu d and v τ = v d are integral valued and y = u v . Moreover, by (1), there exists k ∈ N such that vθ k → 0.

Since

y = x -r ∈ S , there exists a, b ∈ Q[X], with a = 0, such that a(x)y = b(x) + o(θ k ). We can assume a, b ∈ Z[X]. Consequently, a(x)u -b(x)v is a integer valued infinitesimal sequence, hence a(x)u -b(x)v = 0 eventually. Then we have b(x) a(x) = u v eventually, from which b(f (x)) a(f (x)) = c b(x) d a(x) d , that's ca(f (x))b(x) d -b(f (x))a(x) d = 0. Since x is unbounded, it follows that ca(f (X))b(X) d -b(f (X))a(X) d = 0 identically in Z[X]. The rational function γ = b a ∈ Q(X) satisfy γ(f (X)) = cγ(X) d .

Rational functional equation

In this section we prove the following:

Theorem 4.1. Let f ∈ C[X]
be a non-constant polynomial with degree d > 1 and leading coefficient c = 0. If there exists a non-constant rational function γ ∈ C(X) such that γ(f (X)) = cγ(X) d then there exists a ∈ C such that f (X) = c(X -a) d + a.

Recall that C[X] is a unique factorization domain with field of fractions C(X). In C[X] irreducible elements are the polynomials of degree 1. If p ∈ C[X] is an irreducible polynomial and γ ∈ C(X) then we can define the order ord p γ of γ at p and it's an integer.

Lemma 4.2. Let f be a non-constant polynomial in C[X]. For any monic irreducible polynomial q ∈ C[X] there exists a unique monic irreducible polynomial

p ∈ C[X] such that q(X) | p(f (X)) in C[X]
. If e q denote the order of p(f ) at q then 1 ≤ e q ≤ deg f . Moreover for any rational function γ ∈ C(X) we have ord q γ(f ) = e q ord p γ.

Proof. If q(X) = X -a for some a ∈ C then take p(X) = X -f (a). Since deg p(f (X)) = deg p deg f it follows that e q ≤ deg f . For the last statement, let n ∈ Z be the order of γ at p and let γ ∈ C(X) such that γ = p n γ; then p is not an irreducible factor of γ. Then γ(f ) = p(f ) n γ(f ) and p(f ), γ(f ) has no common irreducible factors. Consequently the order of γ(f ) at q is ne q .

Proposition 4.3. Let f (X) ∈ C[X] be a polynomial with degree d > 1 and leading coefficient c. If there exists a non-constant rational function γ ∈ C(X) such that γ(f (X)) = cγ(X) d then for any monic irreducible factor p of γ there exists an unique monic irreducible factor q of γ such that p(f (X)) = cq(X) d .

Proof. For any monic irreducible polynomial q ∈ C[X] let q * denote the monic irreducible polynomial in C[X] such that q(X) | q * (f (X)) and let e q be the order of q * (f (X)) at q. Let S be the set of monic irreducible factors of γ; since γ is not constant, S is non-empty. By previous lemma, d ord q γ = e q ord q * γ;

in particular q ∈ S if and only if q * ∈ S. Consequently we have a map * : q → q * from S into S.

Note that this map is onto for if p(X) = X -b ∈ S and q(X) = X -a where a ∈ C is a root of the polynomial f (X) -b, then q * = p hence q ∈ S. Since S is finite, the map * : q → q * is a permutation of S.

We obtain q∈S d ord q γ = q∈S e q ord q * γ but since q ord q γ = q ord q * γ = 0 it implies

d ♯S = q∈S e q
where ♯S denote the number of elements in S. Since 1 ≤ e q ≤ d, must be e q = d for each q thus q * (f ) = q d . Now we are able to prove 4.1:

Proof. Let p be a monic irreducible factor of γ. By 4.3 there exists a monic irreducible factor q of γ such that p(f (X)) = cq(X) d . If q(X) = X -a and p(X) = X -b then f (X) = c(X -a) d +b. Since q is a monic irreducible factor of γ, q(f (X)) is also a d-power of an irreducible factor of f . In particular, q(f ) has a multiple root r hence 0 = q(f (r)) ′ = f ′ (r) but since a is the only root of f ′ , it follows that r = f (a) = b, that's q(X) = p(X). Thus a = b, that's f (X) = c(X -a) d + a.

  Since xθ -1 = rθ ∈ E (θ), we have xξ -a 0 = η + a 0 rθ + rηθ ∈ E (θ), because r, θ, η ∈ E (θ). Conclude by induction on the degree of a. Theorem 3.3. Given ξ ∈ S , for every positive integer k there exists a, b ∈ Q[X], with a = 0 and deg a ≤ k, such that a(x)ξ = b(x) + o(θ k ).