Patrick Baillot

Alexis Ghyselen

Combining Linear Logic and Size Types for Implicit Complexity (Long Version)

Keywords:

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and defines type systems based on restricted versions of the "!" modality controlling duplication. An instance of this is light linear logic for polynomial time computation [Girard98]. A second perspective relies on the idea of tracking the size increase between input and output, and together with a restricted use of recursion, to deduce from that time complexity bounds. This second approach is illustrated for instance by non-size-increasing types [Hofmann99]. However both approaches suffer from limitations. The first one, that of linear logic, has a limited intensional expressivity, that is to say some natural polynomial time programs are not typable. As to the second approach it is essentially linear, more precisely it does not allow for a non-linear use of functional arguments. In the present work we adress the problem of incorporating both approaches into a common type system. The source language we consider is a lambda-calculus with data-types and iteration, that is to say a variant of Godel's system T. Our goal is to design a system for this language allowing both to handle non-linear functional arguments and to keep a good intensional expressivity. We illustrate our methodology by choosing the system of elementary linear logic (ELL) and combining it with a system of linear size types. We discuss the expressivity of this new type system and prove that it gives a characterization of the complexity classes FPTIME and 2k-FEXPTIME, for k ě 0.

Presentation of s T and Control of the Reduction Procedure

. The calculus that we define in this paper, called s T for sized linear system T, is d T without references and with some simplifications and modifications in indexes and types. Informally, s T is a linear λ-calculus enriched with constructors for base types such as booleans, integers and words, and it comes with a constructor for high-order primitive recursion. Types are enriched with a polynomial index describing the size of the value represented by a term, and this index imposes a restriction on recursions. With this, we are able to derive a weight on terms in order to control the number of reduction steps of a term.

Syntax of s T and Type System

Substitution. For an object t with a notion of free variable and substitution we write trt 1 {xs the term t in which free occurrences of x have been replaced by t 1 .

Introduction

Controlling the time complexity of programs is a crucial aspect of program development. Complexity analysis can be performed on the overwhole final program and some automatic techniques have been devised for this purpose. However if the program does not meet our expected complexity bound it might not be easy to track which subprograms are responsible for the poor performance and how they should be rewritten in order to improve the global time bound. Can one instead investigate some methodologies to program while staying in a given complexity class? Can one carry such program construction without having to deal with explicit annotations for time bounds? These are some of the questions that have been explored by implicit computational complexity, a line of research which defines calculi and logical systems corresponding to various complexity classes, such as FP, FEXPTIME, FLOGSPACE . . .

State of the Art.

A first success in implicit complexity was the recursion-theoretic characterization of FP [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]. This work on safe recursion leads to languages for polynomial time [START_REF] Hofmann | A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion[END_REF], for oracle functionals or for probabilistic computation [START_REF] Dal | A higher-order characterization of probabilistic polynomial time[END_REF][START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF]. Among the other different approaches of implicit complexity one can mention two important threads of work. The first one is issued from linear logic, which provides a decomposition of intuitionistic logic with a modality, !, accounting for duplication. By designing variants of linear logic with weak versions of the ! modality one obtains systems corresponding to different complexity classes, like light linear logic (LLL) for the class FP [START_REF] Girard | Light linear logic[END_REF] and elementary linear logic (ELL) for the classes k-FEXPTIME, for k ě 0. [START_REF] Girard | Light linear logic[END_REF][START_REF] Baillot | On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy[END_REF][START_REF] Danos | Linear logic and elementary time[END_REF]. These logical systems can be seen as type systems for some variants of lambda-calculi. A key feature of these systems, and the main ingredient for proving their complexity properties, is that they induce a stratification of the typed program into levels. We will thus refer to them as level-based systems. Their advantage is that they deal with a higher-order language, and that they are also compatible with polymorphism. Unfortunately they have a critical drawback: only few and very specific programs are actually typable, because the restrictions imposed to recursion by typing are in fact very strong... A second thread of work relies on the idea of tracking the size increase between the input and the output of a program. This approach is well illustrated by Hofmann's Non-size-increasing (NSI) type system [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF] : here the types carry information about the input/output size difference, and the recursion is restricted in such a way that typed programs admit polynomial time complexity. An important advantage with respect to LLL is that the system is algorithmically more expressive, that is to say that far more programs are typable. Of course such a simple system cannot be expected to recognize programs which are polynomial time for subtle reasons, but it enlightens interesting situations where the complexity can be deduced from this simple size analysis. A similar idea is also explored by the line of work on quasi-interpretations [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF][START_REF] Baillot | Higher-order interpretations and program complexity[END_REF], with a slightly different angle : here the kind of dependence between input and output size can be more general but the analysis is more of a semantic nature and in particular no type system is provided to derive quasi-interpretations. The type system d T of [START_REF] Baillot | Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs[END_REF] can be thought of as playing this role of describing the dependence between input and output size, and it allows to derive sharp time complexity bounds, even though these are not limited to polynomial bounds. Altogether we will refer to these approaches as sizebased systems. Unfortunately they also have a limitation: they do not deal with a full-fledge higher-order language, in the sense that functional arguments have to be used linearly, that is to say at most once.

Problematic. So on the one hand level-based systems manage higher-order but have a poor expressivity, and on the other hand sized-based systems have a good expressivity but do not deal with general higherorder. . . This is not a mere historical incident, in the sense that on both sides some attempts have been made to repair these defects but only with modest success: in [START_REF] Baillot | A polytime functional language from light linear logic[END_REF] for instance LLL is extended to a language with recursive definitions, but the main expressivity problem remains; in [START_REF] Baillot | Higher-order interpretations and program complexity[END_REF] quasi-interpretations are defined for a higher-order language, but a linearity condition still has to be imposed on functional arguments. The goal of the present work is precisely to try to remedy to this problem by reconciliating the level-based and the size-based approaches. From a practical point of view we want to design a system which would bring together the advantages of the two approaches. From a fundamental point of view we want to understand how the levels and the input/output size dependencies are correlated, and for instance if one of these two characteristics subsumes the other one.

Methodology. One way to bridge these two approaches could be to start with a level-based system such as LLL, and try to extend it with more typing rules so as to integrate in it some size-based features. However a technical difficulty for that is that the complexity bounds for LLL and variants of this system are usually obtained by following specific term reduction strategies such as the level-by-level strategy. Enriching the system while keeping the validity of such reduction strategies turns out to be very intricate. For instance this has been done in [START_REF] Baillot | A polytime functional language from light linear logic[END_REF] for dealing with recursive definitions with pattern-matching, but at the price of technical and cumbersome reasonings on the reduction sequences. Our methodology to overcome this difficulty in the present work will be to choose a variant of linear logic for which we can prove the complexity bound by using a measure which decreases for any reduction step. So in this case there is no need for specific reduction strategy, and the system is more robust to extensions. For that purpose we use elementary linear logic (ELL), and more precisely the elementary lambda-calculus studied in [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF].

Our language. Let us recall that ELL is essentially obtained from linear logic by dropping the two axioms !A

A and !A !!A for the ! functor (the co-unit and co-multiplication of the comonad). Basically, if we consider the family of types W ! i W (where W is a type for binary words), the larger the integer i, the more computational power we get... This results in a system that can characterize the classes k-FEXPTIME, for k ě 0 [START_REF] Baillot | On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy[END_REF]. The paper [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF] gives a reformulation of the principles of ELL in an extended lambda-calculus with constructions for !. It also incorporates other features (references and multithreading) which we will not be interested in here. Our idea will be to enrich the elementary lambda-calculus by a kind of bootstrapping, consisting in adding more terms to the "basic" type W W . For instance we can think of giving to this type enough terms for representing all polynomial time functions. The way we implement this idea is by using a second language. We believe that several equivalent choices could be made for this second language, and here we adopt for simplicity a variant of the language d T from [START_REF] Baillot | Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs[END_REF], a descendant of previous work on linear dependent types [START_REF] Dal | Linear dependent types and relative completeness[END_REF]. This language is a linear version of system T, that is to say a lambda-calculus with recursion, with types annotated with size expressions. Actually the type system of our second language can be thought of as a linear cousin of sized types [START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF][START_REF] Avanzini | Automating sized-type inference for complexity analysis[END_REF] and we call it s T . So on the whole our global language can be viewed as a kind of two-layer system, the lower one used for tuning first-order intensional expressivity, and the upper one for dealing with higher-order computation and non-linear use of functional arguments.

Roadmap of the paper. We will first define s T and investigate its properties (Sect. 2). Then we will recall the elementary lambda-calculus, define our enriched calculus, describe some examples of programs and study the reduction properties of this calculus (Sect. 3). After that we will establish the complexity results of our enriched calculus (Sect. 4).

pλx.tq V Ñ trV {xs let x b y " V b V 1 in t Ñ trV {xsrV 1 {ys if npV, V 1 q zero Ñ V 1 if npV, V 1 q succpW q Ñ V W iternpV, V 1 q zero Ñ V 1 iternpV, V 1 q succpW q Ñ iternpV, V V 1 q W if wpV0, V1, V 1 q Ñ V 1 if wpV0, V1, V 1 q sipW q Ñ Vi W iterwpV0, V1, V 1 q Ñ V 1 iterwpV0, V1, V 1 q sipW q Ñ iterwpV0, V1, Vi V 1 q W if pV, V 1 q tt Ñ V if pV, V 1 q ff Ñ V 1
Fig. 1. Base rules for s T problem since we can compute the mirror of a word and the subject reduction is easier to prove with this definition.

Those base reductions can be applied in contexts C defined by the following grammar :

C :" rs | C t | V C | C b t | t b C | let x b y " C in t | succpCq | if npC, tq | if npt, Cq | iternpV, Cq | s i pCq | if wpC, t, t 1 q | if wpt, C, t 1 q | if wpt, t 1 , Cq | iterwpV 0 , V 1 , Cq | if pC, tq | if pt, Cq
Linear Types with Sizes. Base types are given by the following grammar :

U :" W I | N I | B I, J, . . . :" a | n P N ˚| I `J | I ¨J I represents an index and a represents an index variable. We define for indexes the notions of free variables and free occurrences in the obvious way and we work up to renaming of variables. We also define the substitution of a free variable in an index in the obvious way.

For two indexes I and J, we say that I ď J if for any valuation φ mapping free variables of I and J to non-zero integers, we have I φ ď J φ . I φ is I where free variables have been replaced by their value in φ, thus I φ is a non-zero integer. We now consider that if I ď J and J ď I then I " J (ie we take the quotient set for the equivalence relation). Remark that by definition of indexes, we always have 1 ď I.

For two indexes I and J, we say that I ă J if for any valuation φ mapping free variables of I and J to non-zero integers, we have I φ ă J φ . This is not equivalent to I ď J and I ‰ J, as you can see with a ď a ¨b.

In this work, we only consider polynomial indexes, this is a huge restriction from usual linear dependent types, used for example in [START_REF] Baillot | Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs[END_REF] or [START_REF] Dal | Linear dependent types in a call-by-value scenario[END_REF], in which they consider any set of functions described by some rewrite rules, but in this work we only want to use s T to characterize polynomial time computation. Now, the types are given by the following grammar :

D :" U | D D 1 | D b D 1
We define a subtyping order Ă on types given by the following rules :

-B Ă B and if I ď J then N I Ă N J and W I Ă W J . -D 1 D 1 1 Ă D 2 D 1 2 iff D 2 Ă D 1 and D 1 1 Ă D 1 2 -D 1 b D 1 1 Ă D 2 b D 1 2 iff D 1 Ă D 2 and D 1 1 Ă D 1 2
Typing Rules and Weight. Variables contexts are denoted Γ , with the shape Γ "

x 1 : D 1 , . . . , x n : D n .
We say that Γ is included in Γ 1 when for all variable that appears in Γ , then it also appears in Γ 1 with the same type. We say that Γ Ă Γ 1 when Γ and Γ 1 have exactly the same variables, and for x : D in Γ and x :

D 1 in Γ 1 we have D Ă D 1 .
Ground variables contexts, denoted dΓ , are variables contexts in which all types are base types. We write Γ " Γ 1 , dΓ to denote the decomposition of Γ into a ground variable context dΓ and a variable context Γ 1 in which types are non-base types.

For a variable context without base types, we note Γ " Γ 1 , Γ 2 when Γ is the concatenation of Γ 1 and Γ 2 , and Γ 1 and Γ 2 do not have any common variables.

We denote proofs as π Γ $ t : D and we define an index ωpπq called the weight for such a proof. The idea is that the weight will be an upper-bound for the number of reduction steps of t. Note that since ωpπq is an index, this bound can depend of some index variables. The rules for those proofs are described by Figure 2 and Figure 3.

The typing rules for if n differs from the one defined in [START_REF] Baillot | Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs[END_REF], but since we do not consider type inference in this work, it allows us to simplify the rule to take something more intuitive. Remark that the if -rule is multiplicative, that means that the contexts are separated in the two premises. This gives us easier proofs for the following, but there is a way to keep the same contexts in the premises, see the appendix 6 for more details.

Note that in the rule for itern described in Figure 3, the index variable a must be a fresh variable.

The weight also differs from the one defined in [START_REF] Baillot | Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs[END_REF], since here we focus on a measure for reductions of terms, whereas in this paper, the authors work on a measure for reductions in a CEK abstract machine.

D Ă D 1 π Γ, x : D $ x : D 1 ωpπq " 1 σ Γ, x : D $ t : D 1 π Γ $ λx.t : D D 1 ωpπq " 1 `ωpσq σ1 Γ1, dΓ $ t : D 1 D σ2 Γ2, dΓ $ t 1 : D 1 π Γ1, Γ2, dΓ $ t t 1 : D ωpπq " ωpσ1q `ωpσ2q σ1 Γ1, dΓ $ t : D σ2 Γ2, dΓ $ t 1 : D 1 π Γ1, Γ2, dΓ $ t b t 1 : D b D 1 ωpπq " ωpσ1q `ωpσ2q `1 σ1 Γ1, dΓ $ t : D b D 1 σ2 Γ2, dΓ, x : D, y : D 1 $ t 1 : D 2 π Γ1, Γ2, dΓ $ let x b y " t in t 1 : D 2 ωpπq " ωpσ1q `ωpσ2q Fig. 2. Part 1 of the type system for s T π Γ $ zero : N I ωpπq " 0 σ Γ $ t : N J J `1 ď I π Γ $ succptq : N I ωpπq " ωpσq σ1 Γ1, dΓ $ t : N I D σ2 Γ2, dΓ $ t 1 : D π Γ1, Γ2, dΓ $ if npt, t 1 q : N I D ωpπq " ωpσ1q `ωpσ2q `1 D Ă E E Ă Era `1{as σ1 dΓ $ V : D Dra `1{as ErI{as Ă F σ2 Γ, dΓ $ t : Dr1{as π Γ, dΓ $ iternpV, tq : N I F ωpπq " I `ωpσ2q `I ¨ωpσ1qrI{as π Γ $ ttpor ffq : B ωpπq " 0 σ1 Γ1, dΓ $ t : D σ2 Γ2, dΓ $ t 1 : D π Γ1, Γ2, dΓ $ if pt, t 1 q : B D ωpπq " ωpσ1q `ωpσ2q ` 1
Fig. 3. Part 2 of the type system for s T

Some Examples of Programs in s T

We give some examples of programs in s T to compute polynomials. We detail more precisely one possible term for addition and one for multiplication for unary integers with their weight. We also give some examples on how to work with binary integers with type W.

Length of a word. We can give a term length with ¨$ length : W I N I that computes the length of a word : length " iterwpλn.succpnq, λn.succpnq, zeroq.

Reverse of a word, and mirror iterator. We can compute the reverse of a word pa 0 a 1 . . . a n Þ Ñ a n . . . a 1 a 0 q with the term rev " iterwpλw.s 0 pwq, λw.s 1 pwq, q : W I W I . Recall that the iterator on words in s T works in the reverse order, that is why this term is not identity but is indeed the term computing the reverse of a word. Now we define IT ERW pV 0 , V 1 , tq " λw.piterwpV 0 , V 1 , tqprev wq that is the iterator on words with the right order pIT ERW pV 0 , V 1 , tq s i1 ps i2 p. . . s in p q . . .qq Ñ ˚Vi1 pV i2 p. . . V in ptq . . .qq. The typing rule we can make for this constructor is exactly the same as the one for iterw.

Iterator with base type argument. We show that for integers we can construct a term RECpV, tq such that RECpV, tq n Ñ ˚V n ´1 pV n ´2 p. . . pV zero tq . . .qq.

RECpV, tq " λn.let x b y " piternpλr b n 1 .pV n 1 rq b succpn 1 q, t b zeroq nq in x

We can give this constructor a typing rule close to the one for the iteration, with an additional argument in the step term of type N a .

D Ă E E Ă Era `1{as dΓ $ V : N a D Dra `1{as
ErI{as Ă F Γ, dΓ $ t : Dr1{as Γ, dΓ $ RECpV, tq : N I F

In the same way, we could define a similar constructor for words.

Addition for unary words. The addition can be written in s T :

N I`a Ă N I`a x : N I , y : N I`a $ y : N I`a I `a `1 ď I `a `1 x : N I , y : N I`a $ succpyq : N I`a`1

x : N I $ λy.succpyq : N I`a N I`a ra `1{as

N I Ă N I`1 x : N I $ x : N I`a r1{as N I`a Ă N I`a N I`a Ă N I`a ra `1{as N I`a rJ{as Ă N I`J
x : N I $ iternpλy.succpyq, xq : N J N I`J π add pI, Jq ¨$ λx.iternpλy.succpyq, xq : N I N J N I`J add " λx.iternpλy.succpyq, xq, π add pI, Jq ¨$ add : N I N J N I`J . And the rules give us, for two integers n and m, add n m Ñ iternpλy.succpyq, nq m Ñ ˚pλy.succpyqq m n Ñ n `m The weight of this term is ω add pI, Jq " 1 `J `1 `J ¨p1 `1qrJ{as " 3J `2

Multiplication for unary words. The multiplication can be written in s T :

N I Ă N I x : N I $ x : N I π add pI, a ¨Iq x : N I $ add : N I N a¨I N pa`1q¨I x : N I $ add x : N a¨I N pa`1q¨I x : N I $ zero : N I N a¨I Ă N a¨I N a¨I Ă N a¨I ra `1{as N a¨I rJ{as Ă N I¨J x : N I $ iternpadd x, zeroq : N J N I¨J π mult pI, Jq ¨$ λx.iternpadd x, zeroq : N I N J N I¨J
With mult " λx.iternpadd x, zeroq : N I N J N I¨J . And this term is indeed the multiplication : mult n m Ñ ˚nm. The weight of this term is ω mult pI, Jq " 1 `J `1 `J ¨p1 `3I ¨a `2qrJ{as " 2 `4J `3IJ 2 To be rigorous, the sub-term add x is not a value, so we cannot write iternpadd x, zeroq, but we can use the usual η-rule and write the term iternpλy.add x y, zeroq.

With the multiplication, the addition and the fact that variables of base types can be duplicated, we can now compute the polynomials in s T .

Addition on binary integers. Now, we define some terms working on integers written in binary, with type W I . First, we define an addition on binary integers in s T with a control on the number of bits. More precisely, we give a term Cadd : N I W J1 W J2 W I such that Cadd n w 1 w 2 outputs the least significant n bits of the sum w 1 `w2 . For example, Cadd 3 101 110 = 011, and Cadd 5 101 110 " 01011. This will usually be used with a n greater than the expected number of bits, the idea being that those extra 0 can be useful for some other programs. If we want an exact addition, we can for example use this function with n being lengthpw 1 q `lengthpw 2 q, and then use a function to erase the extra zeros (we obtain then a type W I W J W I`J q. The term follows the usual idea for addition, we use a supplementary boolean to keep track of the carry. For simplification, we do not give an explicit term but we show that we have to use conditionals and work on each cases one by one.

Cadd " λn, w 1 , w 2 . let c

1 b r 1 b w 1 1 b w 1 2 " iternpλc b r b w b w 1 . match c, w, w 1 with pff, , q Þ Ñ ff b s 0 prq b b | . . . | ptt, s 1 pvq, s 1 pv 1 qq Þ Ñ tt b s 1 prq b v b v 1 , ff b b prev w 1 q b prev w 2 qq n in r.
For the typing of this term, we use in the iteration the type B b W a b W J1 b W J2 , with c representing the carry, r the current result, and w, w 1 the binary integers that we read from right to left.

Unary integers to binary integers. We define a term Cunarytobinary : N I N J W I such that on the input n, n 1 , this term computes the least n significant bit of the representation of n 1 in binary. As previously, we could define a term giving exactly the binary representation by taking an upper-bound of the size for the first argument and then erasing the extra zeros.

Cunarytobinary " λn.iternpλw.Cadd n w ps 1 p qq, Cadd n q Binary integers to unary integers. We would like a way to compute the unary integer for a given binary integer. However, this function is exponential in the size of its input, so it is impossible to write such a function in s T . Nevertheless, given an additional information bounding the size of this unary word, we can give a term Cbinarytounary : N I W J N I such that on an input n, w this term computes the minimum between n and the unary representation of w. First we describe a term min : N I N J N I . min " λn, n 1 .let r 0 b n 0 " piternpλr 1 b n 1 .if npλp.succpr 1 q b p, r 1 b zeroq n 1 , zero b n 1 q nq in r 0 In order to type this term, we use in the iteration the type N a b N J . Remark that this term allows us to erase the index J. Now that we have this term, we can define the following term :

Cbinarytounary " λn.iterwpλn 1 .min n pmult n 1 2q, λn 1 .min n succpmult n 1 2q, zeroq

Properties of the Type System and Terms

In order to prove the subject reduction for s T and that the weight is a bound on the number of reduction steps of a term, we successively prove lemmas leading to usual substitution lemmas.

Values and Closed Normal Forms. First, we show that values are indeed linked to normal forms. In particular, this theorem shows that a value of type integer is indeed of the form succpsuccp. . . psuccpzeroqq . . .qq. This imposes that in this call-by-value calculus, when an argument is of type N , it is the encoding of an integer.

Theorem 1. Let t be a term in s T, if t is closed and has a typing derivation $ t : D then : t is normal if and only if t is a value V.

The proof of this theorem can be found in the appendix, section 6.1. This is an usual proof by induction for the two implications relying on the definition of contexts.

Index Variable Substitution, Weakening and Subtyping. We will give some intermediate lemmas in order to prove the main theorem and some intuitions for the proofs. More details can be found in the appendix.

Lemma 1 (Weakening). Let ∆, Γ be disjoint typing contexts, and π Γ $ t : D then we have a proof π 1 Γ, ∆ $ t : D with ωpπq " ωpπ 1 q. Lemma 2. Let I, J, K be indexes, a, b index variables with a not free in K.

Then IrJ{asrK{bs " IrK{bsrJrK{bs{as Lemma 3 (Index substitution). Let I be an index. 1) Let J 1 , J 2 be indexes such that J 1 ď J 2 then J 1 rI{as ď J 2 rI{as 1') Let J 1 , J 2 be indexes such that J 1 ă J 2 then J 1 rI{as ă J 2 rI{as 2) Let D, D 1 be types such that D Ă D 1 then DrI{as Ă D 1 rI{as 3) If π Γ $ t : D then πrI{as Γ rI{as $ t : DrI{as 4) ωpπrI{asq " ωpπqrI{as Point 1 and 1' are by definition of ď and ă, then point 2 is a direct induction on types using point 1 for base types. Points 3 and 4 are proved by induction on π. Point 1 is used in the successors rules, and point 2 is used in the axiom rule. The only interesting cases are iterations, and one can find the proof for the itern case in the appendix, section 6.1 Lemma 4 (Monotonic index substitution). Take J 1 , J 2 such that J 1 ď J 2 1) Let I be an index, then IrJ 1 {as ď IrJ 2 {as 2) ωpπrJ 1 {asq ď ωpπrJ 2 {asq 3) Let E be a type. If E Ă Era `1{as then ErJ 1 {as Ă ErJ 2 {as and if Era `1{as Ă E then ErJ 2 {as Ă ErJ 1 {as Point 1 can be proved by induction on indexes, and then point 2 is just a particular case of point 1, by lemma 3.4. Point 3 is proved by induction on E. Lemma 5. If π Γ, dΓ $ V : U then we have a proof π 1 dΓ $ V : U with ωpπq " ωpπ 1 q. Moreover, ωpπ 1 q ď 1. This is easily proved by looking which values can be typed with a base type, and observing that the axiom rule is only used with a base typed variable. The other rules that can be used are zero-like and succ-like rules, for which the weight does not increase. That is why the total weight is smaller than the weight for the axiom rule, ie 1.

Lemma 6 (Monotonic dΓ ). If π Γ, dΓ $ t : D then for all subproof σ Γ 1 $ t 1 : D 1 of π, dΓ is included in the context Γ 1 .
This can be proved directly by induction on π.

Lemma 7 (Subtyping

). If π Γ $ t : D then for all Γ 1 , D 1 such that D Ă D 1 and Γ 1 Ă Γ , we have a proof π 1 Γ 1 $ t : D 1 with ωpπ 1 q ď ωpπq
This can be proved by induction on π. The only interesting cases are for iterations, in which case the property directly follows from point 2 and 3 of lemma 4. This lemma shows that we do not need an explicit subtyping rule.

Term Substitution Lemmas. In order to prove the subject reduction of the calculus, we explicit what happens during a substitution of a value in a term. We need to work on two cases, first a substitution of variables with base types, that is to say duplicable variables, and then variables with a non-base type for which the type system imposes linearity.

Lemma 8 (Base value substitution). If π Γ, dΓ, x : U $ t : D and σ dΓ $ V : U then we have a proof π 1 Γ, dΓ $ trV {xs : D. The proof π 1 is π in which we replace the occurrences of axiom rules Γ 1 , x : U $ x : U 1 by the proof σ 1 Γ 1 $ V : U 1 given by the weakening lemma (dΓ is in Γ 1 by lemma 6) and the subtyping lemma. Moreover, ωpπ 1 q ď ωpπq. This is proved by induction on π. Remark that x can appear several times in t since x is typed by a base type. The most interesting case is the axiom case for the variable x, that we develop here. The other cases are direct.

U Ă U 1 π Γ, dΓ, x : U $ x : U 1 ωpπq " 1
We have σ dΓ $ V : U , by the lemma 5, we have ωpσq ď 1 " ωpπq. By the weakening and subtyping lemmas, we have π 1 " σ 1 Γ, dΓ $ V : U 1 and ωpπ 1 q ď ωpσq ď ωpπq.

Lemma 9 (Non-base value substitution). If π Γ 1 , dΓ, x : D 1 $ t : D with D 1 not a base type, and σ Γ 2 , dΓ $ V : D 1 then we have a proof π 1 Γ 1 , Γ 2 , dΓ $ trV {xs : D. The proof π 1 is π in which we add Γ 2 in all contexts in the branch where x appears and we replace the occurrences of axiom rules Γ 1 , x : D 1 $ x : D 2 by the proof σ 1 Γ 1 , Γ 2 $ V : D 2 given by the weakening lemma and the subtyping lemma. Moreover, ωpπ 1 q ď ωpπq `ωpσq. This is proved by induction on π. The bound on the weight holds for the axiom rule by the subtyping lemma. In multiplicative rules such as application and if , the property holds by the fact that x only appears in one of the premises, and so ωpσq appears only once in the total weight. Finally, for the iteration rules, the property holds since x cannot appear in the step terms.

Main Theorem : The Weight Controls Reductions

In this section we express the subject-reduction of the calculus and the fact that the weight of a proof strictly decreases during a reduction. Theorem 2. Let τ Γ $ t 0 : D, and t 0 Ñ t 1 , then there is a proof τ 1 Γ $ t 1 : D such that ωpτ 1 q ă ωpτ q.

The proof of this theorem can be found in the appendix, in section 6.2. The main difficulty is to prove this result for base reductions. Base reductions that induces a substitution, like the usual β reduction, are proved by using the substitution lemmas given previously. The others interesting cases are the rules for iterators. For such a rule, the subject reduction is given by a good use of the fresh variable given in the typing rule. This is a rather direct proof by using the previous lemmas on indexes and typing derivations.

As the indexes can only define polynomials, the weight of a sequent can only be a polynomial on the index variables. And so, in s T , we can only define terms that works in polynomial time on their inputs.

Polynomial Indexes and Degree

For the following section on the elementary affine logic, we need to define a notion of degree of indexes and explicit some properties of this notion. The indexes can be seen as multi-variables polynomials, and we can define the degree of an index I by induction on I : ' @n P N ˚, dpnq " 0 ' For an index variable a, dpaq " 1 ' dpI `Jq " maxpdpIq, dpJqq ' dpI ¨Jq " dpIq `dpJq.

We have the following properties between indexes and degree :

Theorem 3 (Degree). 1) Let I be an index and k P N ˚, Irk{as ď k dpIq ¨Ir1{as.

2) If I ď J then dpIq ď dpJq.

The first point is proved by induction on I. For the second point, the proof can be found in the appendix, section 6.1. If one thinks of indexes as polynomials, this second point is really intuitive.

By the point 2, we also obtain that if I ď J and J ď I then dpIq " dpJq, and so the degree can be defined up to equivalence. This justifies that this definition is correct in our set of indexes with a quotient by the equivalence relation. This definition of degree is primordial for the control of reductions in the enriched EAL calculus, that we present in the following section.

Enriched EAL-Calculus

We work on an elementary affine lambda calculus based on [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF] without multithreading and side-effects, that we present here. In order to solve the problem of intensional expressivity of this calculus, we enrich it with constructors for integers, words and booleans, and some iterators on those types following the usual constraint on iteration in elementary affine logic (EAL). Then, using the fact that the proof of correctness in [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF] is robust enough to support functions computable in polynomial time with type N N (see Section 6.3 in the appendix), we enrich EAL with the polynomial time calculus defined previously. More precisely, we add the possibility to use first-order s T terms in this calculus in order to work on those base types, particularly we can then do controlled iterations for those types. We then adapt the measure used in [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF] to our calculus to find an upper-bound on the number of reductions for a term.

A Classical EAL-Calculus

First, let us present a λ-calculus for the classical elementary affine logic. In this calculus, any sequence of reduction terminates in elementary time. The keystone of this proof is the use of the modality "!", called bang, inspired by linear logic. In order to have this bound, there are some restrictions in the calculus like linearity (or affinity if we allow weakening) and an important notion linked with the "!" is used, the depth. We follow the presentation from [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF] and we encode the usual restrictions in a type system.

Terms and semantics. Terms are given by the following grammar :

M :" x | λx.M | M M 1 | !M | let !x " M in M 1
The constructor let !x " M in M 1 binds the variable x in M 1 . We define as usual the notion of free variables, free occurrences and substitution.

The semantic of this calculus is given by the two following rules :

pλx.M q M 1 Ñ M rM 1 {xs let !x "!M in M 1 Ñ M 1 rM {xs.
Those rules can be applied in any contexts.

Type system. We add to this calculus a polymorphic type system that also restraints the possible term we can write.

Types are given by the following grammar :

T :" α | T T 1 | !T | @α.
T Linear variables contexts are denoted Γ , with the shape Γ " x 1 : T 1 , . . . , x n : T n . We write Γ 1 , Γ 2 the disjoint union between Γ 1 and Γ 2 .

Global variables contexts are denoted ∆, with the shape ∆ " x 1 : T 1 , . . . , x n : T n , y 1 : rT 1 1 s, . . . y n : rT 1 m s. We say that [T] is a discharged type, as we could see in light linear logic, see for example [START_REF] Girard | Light linear logic[END_REF] and [START_REF] Terui | Light affine lambda calculus and polytime strong normalization[END_REF]. When we need to separate the discharged types from the others, we will write ∆ " ∆ 2 , r∆ 1 s". In this case, if r∆ 1 s " y 1 : rT 1 1 s, . . . , y m : rT 1 m s, then we note ∆ " y 1 : T 1 1 , . . . , y m : T 1 m . Typing judgments have the shape Γ | ∆ $ M : T . The rules are given in Figure 4. Observe that all the rules are multiplicative for Γ , and the "! Intro" rule erases linear contexts, non-discharged types and transforms discharged types into usual types. With this, we can see that some restrictions appears in a typed term. First, in λx.M , x occurs at most once in M , and moreover, there is no "! Intro" rule behind the axiom rule for x. Then, in let !x " M in M 1 , x can be duplicated, but there is exactly one "! Intro" rule behind each axiom rule for x. For example, with this type system, we can not type terms like λx.!x, λf, x.f pf xq or let !x " M in x.

With this type system, we obtain as a consequence of the results exposed in [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF] that any sequence of reductions of a typed term terminates in elementary time. This proof relies on the notion of depth linked with the modality "!" and a measure on terms bounding the number of reduction for this term. We will adapt and work with those two notions in the following part on the enriched EAL calculus, but for now, let us present some terms and encoding in this calculus.

Examples of terms in EAL and Church integers.

A useful term is the term proving the functoriality of the modality ! :

f onct " λf, x.let !g " f in let !y " x in !pg yq : @α, α 1 .!pα α 1 q !α !α 1 . f :!pα α 1 q | ¨$ f :!pα α 1 q x :!α | g : rα α 1 s $ x :!α ¨| g : α α 1 , y : α $ g : α α' ¨| g : α α 1 , y : α $ y : α ¨| g : α α 1 , y : α $ g y : α 1 ¨| g : rα α 1 s, y : rαs $!pg yq :!α 1 x :!α | g : rα α 1 s $ let !y " x in !pg yq f :!pα α 1 q, x :!α | ¨$ let !g " f in let !y " x in !pg yq :!α 1 ¨| ¨$ λf, x.let !g " f in let !y " x in !pg yq : !pα α 1 q !α !α 1 ¨| ¨$ λf, x.let !g " f in let !y " x in !pg yq : @α, α 1 .!pα α 1 q !α !α 1
Integers can be encoded in this calculus, using the type N " @α.!pα αq !pα αq. For example, 3 is described by the term 3 " λf.let !g " f in !pλx.g pg pg xqqq : N . With this encoding, addition and multiplication can be defined, with type N N N . add " λn, m, f.let

!f 1 " f in let !g " n !f 1 in let !h " m !f 1 in !pλx.h pg xqq mult " λn, m, f.let !g " f in npm !f q
And finally, one can also define an iterator using integers iter " λf, x, n.f onct pn f q x : @α.!pα

αq !α N !α such that iter !M !M 1 n Ñ ˚!pM n M 1 q.
Intensional expressivity. Those examples show that this calculus suffers from limitation. First, we need to work with Church integers, because of a lack of data structure. Furthermore, we need to be careful with the modality, and this can be sometime a bit tricky, as one can remark with the addition. And finally if we want to do an iteration, we are forced to work with type with bangs. This implies that each time we need to use an iteration, we are forced to add a bang in the final type. However, it has been proved [START_REF] Baillot | Characterizing polynomial and exponential complexity classes in elementary lambda-calculus[END_REF] that polynomial and exponential complexity classes can be characterized in this calculus, by fixing types. For example, with a type for words W and booleans B we have that !W !!B characterizes polynomial time computation. But with this type, the restriction explained above imposes that one can only use once a term like iter, and so, some natural polynomial time programs cannot be typed with the type !W !!B. We say that this calculus has a limited intensional expressivity.

One goal of this paper is to try to solve this problem, and for that, we now present an enriched version of this EAL-calculus, using the language s T defined previously.

Notations

Applications. For an object with a notion of application M and an integer n, we write

M n M 1 to denote n applications of M to M 1 . In particular, M 0 M 1 " M 1
We also define for a word w, given objects M a for all letter a, M w M 1 . This is defined by induction on words with M M 1 " M 1 and M aw 1 M 1 " M a pM w 1 M 1 q Notations for vectors. In the following we will work with vectors of N n`1 , for n P N. We introduce here some notations on those vectors.

We usually denote vectors by µ " pµp0q, . . . , µpnqq When there is no ambiguity with the value of n, for 0 ď k ď n, we note 1 k the vector µ with µpkq " 1 and @i, 0 ď i ď n, i ‰ k, µpiq " 0. We extend this notation for k ą n. In this case, 1 k is the zero-vector.

Let µ 0 P N n`1 and µ 1 P N m`1 . We denote µ " pµ 0 , µ 1 q P N m`n`2 the vector with @i, 0 ď i ď n, µpiq " µ 0 piq and @i, 0 ď i ď m, µpi `n `1q " µ 1 piq.

Let µ 0 , µ 1 P N n`1 . We write µ 0 ď µ 1 when @i, 0 ď i ď n, µ 0 piq ď µ 1 piq. And we write µ 0 ă µ 1 when µ 0 ď µ 1 and µ 0 ‰ µ 1 .

Let µ 0 , µ 1 P N n`1 . We write µ 0 ď lex µ 1 for the lexicographic order on vectors. For k P N, when there is no ambiguity with the value of n, we write k the vector µ such that @i, 0 ď i ď n, µpiq " k.

Syntax and Type System

Terms. Terms are defined by the following grammar :

M :" x | λx.M | M M 1 | !M | let !x " M in M 1 | M b M 1 | let x b y " M in M 1 | zero | succpM q | if npM, M 1 q | iter ! N pM, M 1 q | tt | ff | if pM, M 1 q | | s 0 pM q | s 1 pM q | if wpM 0 , M 1 , M q | iter ! W pM 0 , M 1 , M q | rλx n . . . x 1 .tspM 1 , . . . , M n q
Note that the t used in rλx n . . . x 1 .tspM 1 , . . . , M n q refers to terms defined in s T . This notation means that we call the function t defined in s T with arguments M 1 , . . . , M n . Moreover, n can be any integer, even 0.

Constructors for iterations directly follow from the ones we can define usually in EAL for Church integers or Church words, as we could see in the previous section on classical EAL.

Once again, we often write s i to denote s 0 or s 1 , and the choice of the alphabet t0, 1u is arbitrary, we could have used any finite alphabet.

In the following, we note v for base type values, defined by the following grammar

v :" zero | succpvq | | s i pvq | tt | ff
In particular, if n is an integer and w is a binary word, we note n for the base value succ n pzeroq, and w " w 1 ¨¨¨w n for the base value s w1 p. . . s wn p q . . .q.

We define the size |v| of v by |zero| " | | " |tt| " |ff| " 1 and |succpvq| " |s i pvq| " 1 `|v|.

As usual, we work up to α-isomorphism and we do not explicit the renaming of variables.

Reductions. Base reductions are defined by the rules given in Figure 5. Note that for some of these rules, for example the last one, v can denote either the s T term or the enriched EAL term. Those reductions can be extended to any contexts, and so we write M Ñ M 1 if there is a context C and a base reduction M 0 Ñ M 1 0 such that M " CpM 0 q and M 1 " CpM 1 0 q.

pλx.M q M 1 Ñ M rM 1 {xs let !x "!M in M 1 Ñ M 1 rM {xs let x b y " M b M 1 in N Ñ N rM {xsrM 1 {ys if npM, M 1 q zero Ñ M 1 if npM, M 1 q succpN q Ñ M N iter ! N p!M, !M 1 q n Ñ!pM n M 1 q, n integer if wpM0, M1, M q Ñ M if wpM0, M1, M q sipN q Ñ Mi N iter ! W p!M0, !M1, !M 1 q w Ñ!pM w M 1 q, w binary word if pM, M 1 q tt Ñ M if pM, M 1 q ff Ñ M 1 if t Ñ t 1 in s T , rtspq Ñ rt 1 spq rλxn . . . x1.tspM1, . . . , Mn´1, vq Ñ rλxn´1 . . . x1.trv{xnsspM1, . . . , Mn´1q rvspq Ñ v
Types. Types are usual types for intuitionistic linear logic enriched with some base types for booleans, integers and words. Base types are given by the following grammar : A :" B | N | W Types are given by the following grammar :

T :" A | T T 1 | !T | T b T 1
Type System and Measure. Linear variables contexts are denoted Γ and global variables contexts are denoted ∆. They are defined in the same way as in the previous part on the classical EAL-calculus.

Typing judgments have the usual shape of dual contexts judgments π Γ | ∆ $ M : T . For such a proof π, and i P N, we define a weight ω i pπq P N.

For all k, n P N, we note µ k n pπq " pω k pπq, . . . , ω n pπqq, with the convention that if k ą n, then µ k n pπq is the null-vector. We write µ n pπq to denote the vector µ 0 n pπq. In the definitions given in the type system, instead of defining ω i pπq for all i, we define µ n pπq for all n, from which one can recover the weights. We will often call µ n pπq the measure of the proof π.

The depth of a proof (or a typed term) is the greatest integer i such that ω i pπq ‰ 0. It is always defined for any proof.

The idea behind the definition of measure is to show that with a reduction step, this measure strictly decreases for the lexicographic order and we can control the growing of the weights.

Γ, x : T | ∆ $ x : T µnpπq " 10 π Γ | ∆, x : T $ x : T µnpπq " 10 σ Γ, x : T | ∆ $ M : T 1 π Γ | ∆ $ λx.M : T T 1 µnpπq " µnpσq `10 σ Γ | ∆ $ M : T 1 T τ Γ 1 | ∆ $ M 1 : T 1 π Γ, Γ 1 | ∆ $ M M 1 : T µnpπq " µnpσq `µnpτ q `10 σ H | ∆ $ M : T π Γ | ∆ 1 , r∆s $!M : !T µnpπq " p1, µn´1pσqq σ Γ 1 | ∆ $ M : !T τ Γ | ∆, x : rT s $ M 1 : T 1 π Γ, Γ 1 | ∆ $ let !x " M in M 1 : T 1 µnpπq " µnpσq `µnpτ q `10 σ Γ | ∆ $ M : T τ Γ 1 | ∆ $ M 1 : T 1 π Γ, Γ 1 | ∆ $ M b M 1 : T b T 1 µnpπq " µnpσq `µnpτ q `10 σ Γ 1 | ∆ $ M : T b T 1 τ Γ, x : T, y : T 1 | ∆ $ M 1 : T 2 π Γ, Γ 1 | ∆ $ let x b y " M in M 1 : T 2
µnpπq " µnpσq `µnpτ q `10 Fig. 6. Type system and measure for the classical EAL

π Γ | ∆ $ zero : N µnpπq " 11 σ Γ | ∆ $ M : N π Γ | ∆ $ succpM q : N µnpπq " µnpσq `11 σ Γ | ∆ $ M : N T τ Γ 1 | ∆ $ M 1 : T π Γ, Γ 1 | ∆ $ if npM, M 1 q : N T µnpπq " µnpσq `µnpτ q `10 σ Γ | ∆ $ M : !pT T q τ Γ 1 | ∆ $ M 1 : !T π Γ, Γ 1 | ∆ $ iter ! N pM, M 1 q : N !T
µnpπq " µnpσq `µnpτ q `10 Fig. 7. Type system and measure for constructors on integers

@i, p1 ď i ď kq, σi Γi | ∆ $ Mi : Ai τ x1 : A a 1 1 , . . . , x k : A a k k $ s T t : A I π Γ, Γ1, . . . , Γ k | ∆ $ rλx k . . . x1.tspM1, . . . , M k q : A µnpπq " k ř i"1
µnpσiq `kpdpωpτ q `Iq `1q ¨10 `ppωpτ q `Iqr1{b1s ¨¨¨r1{b l s `1q ¨11

where tb1, . . . , b l u " F V pωpτ qq Y F V pIq. The rules are given by the Figure 6, Figure 7 and Figure 8. The rules given in figure 6 represent the classic rules for EAL. Note that as we could see in the classical EAL calculus, those rules impose some restrictions in the use of variables. Indeed, for the terms λx.M and let x b y " M 1 in M , the newly defined variables are used at most once in M , and if they appear, then we did not cross a !. For the term let !x " M in M 1 , the variable x can be used as many times as we want in M 1 , but we need to cross exactly one time a ! to use the variable.

Remark that the constructors for base types values such as zero and succ given in Figure 7 influence the weight only in position 1 and not 0 like the others constructors.

For the rule given by Figure 8, some explanations are necessary. The premise for t is a proof in s T . In this proof, we add on each base types A i an index, more precisely an index variable a i . There is here an abuse of notation, since in s T there is no indexes on the boolean type B. So when A i " B, we just do not put any index on the type B. The same goes for the type A, if A is the boolean type B, then there is no index I, and we just replace in the measure I by 1. The typing in s T give us a weight ωpτ q and a size for the output I. The degree of those indexes influences the weight at position 0, and their values when all free variables are replaced by 1 influence the weight at position 1. Having the degree at position 0 will allow us the replacement of the arguments x i by their values given by M i , and the measure at position 1 will allow us to bound the number of reductions in s T and the size of the output.

Remark that when k " 0, the term rtspq influences only the weight at position 1, as constructors for base types.

We include a weakening in this rule, in order to conserve the weakening property of the calculus for the case k " 0.

The terms from s T that can be called are only first-order functions, so they take base type inputs and output a base type value.

Examples

We give some examples of terms in our enriched EAL calculus, first some terms we can usually see for the elementary affine logic, and then we give the term for computing tower of exponentials.

Some General Results and Notations on EAL. To begin with, we prove some formulas on the elementary affine logic that we will often use in examples without explicitly reminding them.

-We have a proof of the formula !T !T b!T given by the term λx.let !x 1 " x in !x 1 b!x 1 . -The types !pT b T 1 q and !T b!T 1 are equivalent, using the terms λc.let !c 1 " c in !plet x b y " c 1 in xqb!plet x b y " c 1 in yq and λc.let x b y " c in let !x 1 " x in let !y 1 " y in !px 1 b y 1 q. This proof is specific to affine logic since it relies on weakening. -For base types A we have the coercion A !A. For example, for words, this is given by the term coerc w " iter ! W p!pλw 1 .s 0 pw 1 qq, !pλw 1 .s 1 pw 1 qq, ! q, with coerc w w Ñ ˚!w. -We write λx b y.M for the term λc.let x b y " c in M .

Polynomials and Tower of Exponentials in EAL.

Recall that we defined polynomials in s T . With this we can define polynomials in EAL with type N N using the s T call. Moreover, using the iteration in EAL, we can define a tower of exponential.

We can compute the function k Þ Ñ 2 2 k in EAL with type N !N :

n : N | ¨$ n : N x 1 : N a1 $ s T mult x 1 x 1 : N a1¨a1 n : N | ¨$ rλx 1 .mult x 1 x 1 spnq : N N ¨| ¨$ λn.rλx 1 .mult x 1 x 1 spnq : N N ¨| ¨$!pλn.rλx 1 .mult x 1 x 1 spnqq :!pN N q ¨| ¨$!2 :!N ¨| ¨$ exp " iter ! N p!λn.rλx 1 .mult x 1 x 1 spnq, !2q : N !N
And the reduction rules give us :

iter ! N p!λn.rλx 1 .mult x 1 x 1 spnq, !2q k Ñ !ppλn.rλx 1 .mult x 1 x 1 spnqq k 2q Ñ ˚!p2 2 k q.
For an example of measure, for the subproof π ¨| ¨$ λn.rλx 1 .mult x 1 x 1 spnq : N N , we have depthpπq " 1 and as the weight for σ x 1 : N a1 $ s T mult x 1 x 1 : N a1¨a1 is ωpσq " 4 `a1 `3a 3 1 , we can deduce µpπq " p1 `1 `1 ¨pdpωpσq `a1 ¨a1 q `1q, 1 `pωpσq `a1 ¨a1 qr1{a 1 sq " p2 `3 `1, 1 `4 `1 `3 `1q " p6, 10q

If we define, 2 x 0 " x and 2 x k`1 " 2 2 x k , with the use of polynomials, we can represent the function n Þ Ñ 2

P pnq 2k

for all k ě 0 and polynomial P with a term of type N ! k N .

Satisfiability of a Propositional Formula. We can give a term of type N b W !B such that, given a formula on conjunctive normal form encoded in the type N b W , we can check the satisfiability of this formula. The modality in front of the output !B shows that we used a non-polynomial computation, or more precisely an iteration in EAL, in order to define the term, as expected of a term for satisfiability.

We encode formula in conjunctive normal form in the type N b W , representing the number of distinct variables in the formula and the encoding of the formula by a word on the alphabet Σ " t0, 1, #, |u. A literal is represented by the number of the corresponding variable written in binary and the first bit determines if the literal is positive or negative (0 meaning negative). The # indicates the beginning of the representation of a variable, and the | indicates the beginning of the representation of a clause.

For example, the formula px 1 _ x 0 _ x 2 q ^px 3 _ x 0 _ x 1 q ^px 2 _ x 0 _ x 3 q is represented by 4 b |#11#10#110|#111#00#01|#010#10#011 Intermediate terms in s T . We recall that we have already defined previously a term Cbinarytounary : N I W J N I that can be extended for the alphabet Σ. In the following, we may not always consider that the alphabet now contains # and | when we do not use them in the term. In this case, it means that the terms for those letters are not useful and so we could for example put the identity. We can also define a term occ a : W I N I that gives the number of occurrences of a P Σ in a word. We define a term that gives the n th bit (from right) of a binary word as a boolean :

n th " λw, n.if wpλw 1 .ff, λw 1 .tt, ffq ppiternppred, rev wqq nq : W I N I B with pred : W I W I " if wpλw.w, λw.w, q. We can define a term of type W I W I b W I that separates a word w " w 0 aw 1 in w 0 b w 1 such that w 1 does not contain any a. This function will allow us to extract the last clause/literal of a word representing a formula.

Extract a " λw.let b

1 b w 1 0 b w 1 1 " IT ERW pV 0 , V 1 , V # , V | , V q w in w 1 0 b w 1 1 with V a " λb b w 0 b w 1 .if ptt b s a pw 0 q b w 1 , tt b w 0 b w 1 q b @c ‰ a, V c " λb b w 0 b w 1 .if ptt b s c pw 0 q b w 1 , ff b w 0 b s c pw 1 qq b V " f f b b
For the intuition on this term, the boolean b 1 used in the iteration is a boolean that indicates if we have already read the letter "a" previously.

A valuation is represented by a binary word with a length equal to the number of variable, such that the n th bit of the word represents the boolean associated to the n th variable.

We define a term ClausetoBool : N I W J W K B such that, given the number of variable, a valuation and a word representing a clause, this term outputs the truth value of this clause using the valuation.

ClausetoBool " λn, w v , w c . let wbb " iternpλw 1 bb 1 .let w 0 bw 1 " Extract # w 1 in w 0 bpor b 1 pLittoBool n w v w 1 qq, w c b ffq pocc # w c q in b With LittoBool : N I W J W K B converting a literal into the boolean given by the valuation. LittoBool " λn, w v , w l .if w pλw 1 .n th w v pCbinarytounary n w 1 q, λw 1 .not pn th w v pCbinarytounary n w 1 qq, ffq w l .

With this we can check if a clause is true given a certain valuation. We can define in the same way a term F ormulatoBool :

N I W J W K B.
Testing all different valuations. Now all we have to do is to test this term on all possible valuations. If n is the number of variables, all possible valuations are described by all the binary integer from 0 to 2 n ´1.

Then we only need to use the iterator in s T with base type-inputs in order to check if one valuation satisfy the formula. Formally, this is given by the term :

SAT " λn b w.let !r " iter ! N p!pλn 0 b n 1 .succpn 0 q b rdoublespn 1 qq, !p0 b 1qq n in let !w f " coerc w in !plet n b exp " r in rλn, exp, w f .RECpλval, b.or b pF ormulatoBool n pCunarytobinary n valq w f q, ffq expspn, exp, w f qq.

The first line computes 2 n and also do the coercion of n. This technique is important as it shows that the linearity of EAL for base variables is not too constraining for the iteration. If you have to use it multiple time, you can just do a simultaneous iteration using the tensor type. In the last line the term is a big "or" on the term F ormulatoBool applied to different valuations. We recall that the constructor REC is the iterator with base type arguments that has been defined in the previous section on s T .

And with that we have SAT :

N b W !B.
Solving QBF k . Now we consider the following problem, with k being a fixed non-negative integer : Suppose given a formula with the form

Q k x n , x n´1 , . . . , x i k´1 `1. Q k´1 x i k´1 , x i k´1 ´1, . . . , x i k´2 `1.Q k´2 . . . , Q 1 x i1 , x i1´1 , . . . x 0 .φ
The formula φ is a propositional formula in conjunctive normal form on the variables from x 0 to x n , and Q i P t@, Du are alternating quantifiers. That means that if Q 1 is @ then Q 2 must be D and then Q 3 must be @ and so on. Here the variables are ordered for simplification. It can always be done by renaming. And now we have to answer if this formula is true. This can be solved in our enriched EAL calculus.

First, let us talk about the encoding of such a formula. With those ordered variable, a representation of such a formula can be a term of type

N k b N k´1 b . . . b N 1 b B b W .
For all i with 1 ď i ď k, N i represents the number of variables between the quantifiers Q i and Q i´1 . The boolean represents the quantifier Q k , with the convention @ " tt. And finally, the formula φ is encoded in a word as previously. This is not a canonic representation of a formula, but for any good encoding of a QBF k formula we should be able to extract those informations with a s T term, so for simplification, we directly take this encoding.

For example, with k " 2, the formula @x 3 , x 2 .Dx 1 , x 0 .px 1 _ x 0 _ x 2 q ^px 3 _ x 0 _ x 1 q ^px 2 _ x 0 _ x 3 q is represented by 2 b 2 b tt b |#11#10#110|#111#00#01|#010#10#011.

Defining a s T term for QBF k . Now we define by induction on k a s T term called qbf k for k a non-negative integer. We give to this term a type :

qbf k : W K1 b N I k b N J k b . . . b N I1 b N J1 b B b W K2 B.
One can see a similitude with the representation of a QBF k formula. But we add some arguments. First, the argument w v of type W K1 is a valuation on free variables of the QBF k formula. Then we are given for each quantifiers two integers n i and exp i of type N Ii and N Ji , with n i being the number of variables between the quantifiers Q i and Q i´1 , and exp i " 2 ni . Finally, the boolean represents the quantifier Q k and W K2 is a formula on variables from x 0 to x n1`...`n k `lengthpwvq´1 . qbf 0 has already been defined. Indeed, we have qbf 0 "

λw v b q b w f .F ormulatoBool plength w v q w v w f : W K1 b B b W K2
B. Now, let us give the term for qbf 1 . One can observe that it is close to the s T term used for SAT . To begin with, we define a term andor : B pB Bq " if pand, orq. We also write conc : W I W J W I`J the term for concatenation of words. With that we define :

qbf 1 " λw v b n 1 b exp 1 b q b w f . RECpλval, b.pandor qq b pqbf 0 pconc w v pCunarytobinary n 1 valqq b pnot qq b w f q, qq exp 1
So, contrary to SAT, we do not always do a big "or" on the results of qbf 0 but we do either a big "and" if the quantifier Q k is @, either a big "or" if the quantifier is D. And when we call qbf 0 , we have to update the current valuation w v and we have to alternate the quantifier. Now with this intuition, we give the general term for qbf k`1 :

qbf k`1 " λw v b exp k`1 b n k`1 b exp k b n k . . . b exp 1 b n 1 b q b w f . RECpλval, b.pandor qq b pqbf k pconc w v pCunarytobinary n k`1 valqq b exp k b n k . . . b exp 1 b n 1 b pnot qq b w f , qq exp k`1 .
And with this term, given a QBF k formula in the enriched EAL calculus of type

N k b N k´1 b . . . b N 1 b B b W , we can define the following term : ealqbf k " λn k b . . . b n 1 b q b w.let !r " p! q b exp n k b coerc n k b . . . b exp n 1 b coerc n 1 b coerc q b coerc w f in !prqbf k sprqq
With some abuse of notations since we consider the equivalence between !pT b T 1 q and p!T q b p!T 1 q and also between T b T 1 T 2 and T T 1 T 2 . Moreover, we duplicate here the variables n i but as explained previously for SAT, one can compute the coercion and the exponential simultaneously without duplication. It is just better for the intuition written that way.

And so, we obtain a term solving QBF k with type

N k b N k´1 b . . . b N 1 b B b W !B.
Solving the SUBSET SUM Problem. We give here another example of a NP-Complete problem. Given a goal integer k P N and a set S of integers, is there a subset S 1 Ă S such that ř nPS 1

n " k ?

We explain how we could solve this problem in our calculus. We represents the SUBSET SUM problem by two words, k written as a binary integer and a word of the form |n 1 |n 2 | . . . |n m , with the integers written in binary, representing the set S. In order to solve this problem, we can first define a s T term equal : W I W J B that verifies if two binary integers are equal. Note that this is not exactly the equality on words because of the possible extra zeros at the beginning. Then, we can define a term subsetsum : W I W J W I¨J such that, given the word w S representing the set S and a binary word w sub with a length equal to the cardinality of S, this term computes the sum of all the elements of the subset represented by w sub , since this word can be seen as a function from S to t0, 1u. With again some abuse of notation and non-linearity only to clarify things. And so, we obtain a term of type W b W !B. We could also construct a term that gives us the subset corresponding to the goal, by changing the type in the iteration REC from N a B B to N a pB b W I q pB b W I q, W I being the type of the argument w.

Properties of the Type System and the Measure

We give some properties of the type system and the measure, and we give the intuition or the way to prove those properties. The final goal is to prove the main theorem that will follow this section and bound the number of reduction steps of a typed term.

Weakening and Monotonic Contexts. To begin with, we define a !-free path. In a derivation tree π, a !-free path is a path starting from the root that does not cross a !-rule (the rule introducing a !M term). Those kind of paths are important for the substitution lemmas since the !-rule can erase contexts and remove discharged types. In the same way, we define a !-free branch as a !-free path that leads to a leaf.

Lemma 10 (Monotonic ∆). Suppose π Γ | ∆ $ M : T , then for any sequent

Γ 1 | ∆ 1 $ M 1 : T 1 that appears in a !-free path of π, we have ∆ included in ∆ 1 .
This is a direct proof by looking at the typing rules of the system. We can use this lemma when we know that the linear context has not been erased, or when the non-discharged types have not been erased.

Lemma 11 (Weakening). If Γ and Γ 1 are disjoint linear variables contexts, ∆ and ∆ 1 are disjoint general variables contexts and π Γ | ∆ $ M : T then we have a proof π 1 Γ, Γ 1 | ∆, ∆ 1 $ M : T with µ n pπ 1 q " µ n pπq for all n. Substitution Lemmas.

Lemma 12 (Linear Substitution).

If π Γ 1 , x : T 1 | ∆ $ M : T and σ Γ 2 | ∆ $ M 1 : T 1 then we have a proof π 1 Γ 1 , Γ 2 | ∆ $ M rM 1 {xs : T .
The proof π 1 is π in which we add Γ 2 in all branches where x appears, and we replace the occurrences of axiom rules Γ 1 , x :

T 1 | ∆ 1 $ x : T 1 by the proof σ 1 Γ 1 , Γ 2 | ∆ 1 $ M 1 : T 1
given by the weakening lemma, since ∆ is in ∆ 1 by lemma 10. Moreover, for all n, µ n pπ 1 q ď µ n pπq `µn pσq. This is proved by induction on π. The proof is rather direct since it comes from the fact that rules are multiplicative for Γ , and so x only appears in one of the premises for each rule. Moreover, in the !-rule, since x : T 1 is erased, it means that x does not appear in the term M, thus the proof follows from the fact that M rM 1 {xs " M .

Lemma 13 (General substitution). If π Γ | ∆, x : T 1 $ M : T and σ H | ∆ $ M 1 : T 1 and the number of occurrences of x in M is less than K, then we have a proof π 1 Γ | ∆ $ M rM 1 {xs : T . The proof π 1 is π in which we replace the occurrences of axiom rules

Γ 1 | ∆ 1 , x : T 1 $ x : T 1 by the proof σ 1 Γ 1 | ∆ 1 $ M 1 : T 1
given by the weakening lemma, since ∆ is in ∆ 1 by lemma 10. Moreover, for all n, µ n pπ 1 q ď µ n pπq `K ¨µn pσq. This lemma is proved by induction on π. For rules with more than one premise, for example the app rule with 2 premises, we use the fact that if we can bound the number of occurrences of x in M " M 0 M 1 by K, then we can find K 0 , K 1 such that K 0 `K1 " K and K i bounds the number of occurrences of x in M i . Lemma 14 (Discharged substitution lemma). If π Γ | ∆ 1 , r∆s, x : rT 1 s $ M : T and σ H | ∆ $ M 1 : T 1 then we have a proof π 1 Γ | ∆ 1 , r∆s $ M rM 1 {xs : T . The proof π 1 is π in which we replace the occurrences of axiom rules Γ 1 | ∆ 2 , x : T 1 $ x : T 1 by the proof σ 1 Γ 1 | ∆ 2 $ M 1 : T 1 given by the weakening lemma. Moreover, for all n, µ n pπ 1 q ď pω 0 pπq, pµ 1 n pπq `ω1 pπq ¨µn´1 pσqqq.

First we precise why we can use the weakening lemma to replace the axiom rules. By the lemma 10, in a branch that leads to an axiom rule for x, before crossing a !, we have a !-free path and so ∆ grows. Then in order to apply the axiom rule, we need to cross a ! since x has a discharged type at the root of π. After crossing this !, we cannot cross again a ! in a branch that lead to an axiom rule for x since crossing a ! would erase x. So we can again apply the lemma 10 and so ∆ is indeed included in ∆ 2 . Lemma 14 is proved by induction on π. All cases are direct except the ! rule, that can be found in the appendix.

Main Theorem : Defining a Measure to Bound the Number of Reductions

In this section, we show that we can bound the number of reduction steps of a typed term using the measure. This is done by showing that a reduction preserves some properties on the measure, and then give an explicit integer bound that will strictly decrease after a reduction. This proof uses the same logic as the one from [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF]. The relation R defined in the following is a generalization of the usual requirements exposed in elementary linear logic in order to control reductions.

Definition of t α and the Relation R.

Definition of t α . We define a family of tower functions t α px 1 , . . . , x n q on vectors of integers by induction on n, where we assume α ě 1 and x i ě 2 for all i. t α pq " 0 t α px 1 , . . . , x n´1 , x n q " pα ¨xn q 2 tα px 1 ,...,x n´1 q for n ě 1 Definition of R. We define a relation on vectors that we note R. Intuitively, we want Rpµ, µ 1 q to express the fact that a proof of measure µ has been reduced to a proof of measure µ 1 . Let µ, µ 1 P N n`1 . We have Rpµ, µ 1 q if and only if :

1. µ ě 2 and µ 1 ě 2.

2. µ 1 ă lex µ. And so we write µ " pω 0 , . . . , ω n q and µ 1 " pω 0 , . . . , ω i0´1 , ω 1 i0 , . . . , ω 1 n q. With ω i0 ą ω 1 i0 . 3. There exists d P N, 1 ď d ď pω i0 ´ω1 i0 q such that @j ą i 0 , ω 1 j ď ω j ¨pω i0`1 q d´1

The first condition with 2, that can also be seen in the definition of t α , makes calculation easier, since with this condition, exponentials and multiplications conserve the strict order between integers. This does not harm the proof, since we can simply add 2 to each vector we will consider. Some Properties on t α and R. We give some properties on t α and R. The proofs are usually calculation.

Lemma 15. If µ ď µ 1 then t α pµq ď t α pµ 1 q
This is just a consequence of the fact that the exponentiation is monotonic.

Lemma 16 (Shift). Let k P N ˚. Let µ " pω 0 , . . . , k ¨ωi´1 , ω i , . . . ω n q and µ 1 " pω 0 , . . . , ω i´1 , k ¨ωi , . . . ω n q. Then t α pµ 1 q ď t α pµq.

The proof of this lemma can be found in 6.6. This is just a calculation.

Lemma 17. If 2 ď µ 1 ă µ then Rpµ, µ 1 q.
Take d " 1 and the proof is direct.

Lemma 18. If Rpµ, µ 1 q then for all µ 0 , we have Rpµ `µ0 , µ 1 `µ0 q.

Point 1 and 2 in the definition of Rpµ `µ0 , µ 1 `µ0 q are given by the hypothesis Rpµ, µ 1 q. We keep the notations ω j , ω 1 j , i 0 , d. 1 ď d ď ω i0 ´ω1 i0 so 1 ď d ď pω i0 `µ0 pi 0 qq ´pω 1 i0 `µ0 pi 0 qq. Let j ą i 0 , we have : ω 1 j `µ0 pjq ď ω j ¨pω i0`1 q d´1 `µ0 pjq ď pω j `µ0 pjqq ¨pω i0`1 `µ0 pi 0 `1qq d´1 since ω i0`1 ě 1. This concludes the proof of lemma 18.

Finally, the theorem that connects those two definitions :

Theorem 4. Let µ, µ 1 P N n`1 and α ě n, α ě 1. If Rpµ, µ 1 q then t α pµ 1 q ă t α pµq
The proof of this theorem can be found in the appendix, section 6.6. Again, this is just a calculation using the previous lemmas. This theorem shows that if we want to ensure that a certain integer defined with t α strictly decreases for a reduction, it is sufficient to work with the relation R.

Reductions and Relations. We state the subject reduction of the calculus and we show that the measure allows us to construct a bound on the number of reductions.

Theorem 5. Let τ Γ | ∆ $ M 0 : T and M 0 Ñ M 1 . Let α be an integer equal or greater than the depth of τ . Then there is a proof τ 1 Γ | ∆ $ M 1 : T such that Rpµ α pτ q `2, µ α pτ 1 q `2q. Moreover, the depth of τ 1 is smaller than the depth of τ .

The proof of this theorem can be found in the appendix, in section 6.2. This proof uses the substitution lemma for reduction in which substitution appears, and for the others constructors, one can see that the measure given in the type system for this calculus is following this idea of the relation R. For example, in the reduction rλx n . . . x 1 .tspM 1 , . . . , M n´1 , vq Ñ rλx n´1 . . . x 1 .trv{x n sspM 1 , . . . , M n´1 q, the degree that appears at position 0 is here to compensate the growing of the measure at position 1. Indeed, at position 1, in the type system, we consider that all variables are sent to the integer 0. However, in this reduction rule, the variable x n is sent to an actual integer generally greater than 0. Thus, the weight in s T of the term t increases, and so the total measure µ increases at position 1. But as expressed by the relation R, we only need to control this growing. This is in fact what we show in the proof. Now using the previous results, we can easily conclude our bound on the number of reductions.

Theorem 6. Let π Γ | ∆ $ M : T . Denote α " maxpdepthpπq, 1q, then t α pµ α pπq `2q is a bound on the number of reductions from M .

For a proof π 1 , we define an integer t α pµ α pπ 1 q `2q. If we prove that this integer strictly decreases for a reduction, we obtain theorem 6.

By the theorem 5, for M Ñ ˚M 1 Ñ M 2 , α is an upper bound on the depth of the typing derivation of M 1 . We note τ the typing of M 1 and τ 1 the typing of M 2 . We have Rpµ α pτ q `2, µ α pτ 1 q `2q again by theorem 5. And finally, by the theorem 4, we have t α pµ α pτ 1 q `2q ă t α pµ α pτ q `2q. This concludes the proof.

Complexity Results : Characterization of 2k ´EXP

Now that we have proved the precedent theorem, we have obtained a bound on the number of reduction steps from a term. More precisely, this bound shows that between two consecutive weights ω i`1 and ω i , there is a difference of 2 in the height of the tower of exponentials. This will allow us to give a characterization of the classes 2k ´EXP for k ě 0, and each modality "!" in the type of a term will induce a difference of 2 in the height of the tower of exponential.

Restricted Reductions and Values

First, we show that the precedent bound on the number of reductions in Theorem 6 is imprecise. Indeed, if we restrict the possible reductions, we obtain a more precise bound.

Restricted Reductions : Reductions up to a Certain Depth. For i P N, we define the i-reductions, that we note Ñ i :

-@i ě 1, rtspq Ñ i rt 1 spq if t Ñ t 1 in s T . -@i ě 1, rvspq Ñ i v -For the other base reductions M Ñ M 1 , we have @i P N, M Ñ i M 1 -For all i P N, if M Ñ i M 1 then !M Ñ i`1 !M 1
-For all others constructors, the index i stays the same. For example for the application, we have for all

i P N, if M Ñ i M 1 then M N Ñ i M 1 N .
Now, we can find a more precise measure to bound the number of i-reductions. The proof is very similar to the proof of theorem 5 and 6, and one can find in section 6.7 some remarks explicitly describing the important points for lemma 19.

Lemma 19. Let i P N, τ Γ | ∆ $ M 0 : T and M 0 Ñ i M 1 . Then there is a proof τ 1 Γ | ∆ $ M 1 : T such that Rpµ i pτ q `2, µ i pτ 1 q `2q
From that, we can conclude the following theorem : Theorem 7. Let π Γ | ∆ $ M : T and α " maxpi, 1q. Then t α pµ i pπq `2q is a bound on the number of i-reductions from M . This theorem can be expanded for the classes 2k-FEXP, that is the class of function from words to words that can be computed by a one-tape Turing machine running with a time at most 2 P p|w|q 2k on a word w. For a more precise definitions of such classes, see [START_REF] Baillot | Characterizing polynomial and exponential complexity classes in elementary lambda-calculus[END_REF]. This characterization uses the same proof by replacing !W ! k`1 B by !W ! k`1 W . We could also characterize the class 2k-EXP, in the type W ! k B. Indeed, we used here the type !W ! k`1 B because it is easier to work with a duplicable variable in input, but in fact, for the case k " 0 as we can do everything in s T, the input is already duplicable. And then, for k ‰ 0, we showed previously in the examples for SAT or SUBSET SUM that even if the input is not duplicable, you can do simultaneous iteration in ELL and it works as if the variable was duplicable. We think that in our calculus, the base type variables could always be duplicable, not only in s T , and this should not harm our complexity bound. However, in order to simplify the proof, we did not consider this in this paper.

In elementary linear logic, we can characterize k-EXP with the type !W ! k`1 B. The difference between the two calculus can be explained by the fact that in classical ELL, in the type N N we only have polynomials of degree 1 (polynomials in general have the type !N !N ), whereas in our case, polynomials have the type N N .

Conclusion

We showed a way to enrich a calculus from ELL with data structures and iterations controlled by s T , and we showed that this new calculus still has the elementary time reduction procedure. Moreover, with precise types we can characterize more precise complexity classes. This proof relies on the definition of a measure and restricted reductions. It differs from the standard proofs one can find for precise correction proofs in calculus inspired by linear logic. Some classical methods for this kind of proof rely on proof-nets with particular reduction strategies, or if the model is a calculus, one can show how the variables are duplicated, and again explicit a specific reduction strategy. For example, some work had already been done in order to enrich light linear logic with a more natural way of programming [START_REF] Baillot | A polytime functional language from light linear logic[END_REF]. The proof of correction relies on a very specific strategy reduction, and as a consequence, it is hard to add a new enrichment in the calculus, since this proof is hard to adapt. This proof is pretty robust, it does not rely on a particular reduction strategy and thus an improvement of the calculus could be done without too much difficulty. Indeed, if we want to add more possibilities in the enriched calculus we defined, by verifying that the measure is still defined in such a way that reductions satisfy the relation R, and by adapting i-reductions and i-values, then we can show that this additional possibility does not break the proof of correction. An example of enrichment would be a way to duplicate base variable for the EAL-calculus by allowing the use of first-order functions in s T that output a tensor of base values. Another possibility would be to add list in our base values.

For further works, we could be interested in working with smaller complexity classes, and for example try to characterize the polynomial class with a type !W !!B. For that, we could wonder what happens when the computational power of the calculus used to enrich EAL decreases. For example, we could replace indexes in s T describing polynomials by an other class of indexes, such as indexes describing affine functions. Another approach would be to replace s T by the calculus for non-size increasing function [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF]. With the polynomial bound on this calculus [START_REF] Aehlig | A syntactical analysis of non-size-increasing polynomial time computation[END_REF] we could adapt our correction proof to this calculus, and we can then wonder what is the expressiveness of this calculus.

There are also some questions left open for the enriched EAL-calculus, we could for example work on type inference, using previous works on linear dependent types [START_REF] Dal | The geometry of types[END_REF], [START_REF] Baillot | Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs[END_REF], and on ELL [START_REF] Baillot | A feasible algorithm for typing in elementary affine logic[END_REF]. Maybe it is also possible to increase the power of s T in our calculus and not limit its use to first order-function. Furthermore, we could also try to add multithreading and side-effects in this calculus following the proof given in [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF].

Appendix

Type system for words in s T π Γ $ : W I ωpπq " 0

σ Γ $ t : W J J `1 ď I π Γ $ s i ptq : W I ωpπq " ωpσq σ 1 Γ 1 , dΓ $ t 1 : W I D σ 0 Γ 0 , dΓ $ t 0 : W I D σ Γ, dΓ $ t 1 : D π Γ 0 , Γ 1 , Γ, dΓ $ if wpt 0 , t 1 , t 1 q : W I D
ωpπq " ωpσ 1 q `ωpσ 0 q `ωpσq `1

D Ă E E Ă Era `1{as σ 1 dΓ $ V 1 : D Dra `1{as σ 0 dΓ $ V 0 : D Dra `1{as ErI{as Ă F σ Γ, dΓ $ t : Dr1{as π Γ, dΓ $ iterwpV 0 , V 1 , tq : N I F
ωpπq " I`ωpσq`I¨pωpσ 1 q`ωpσ 0 qqrI{as A non multiplicative rule for if In s T , the rule for if is multiplicative, this is not intuitive since in a computation, only one of the two term in the if is important, the other one will be erased. And so, for example, the term if px, xq should be considered linear in x. There is a way to avoid this problem, we give the method with an example. Take D a non base type and f a variable of type D. Take t and t 1 terms such that t contains at most one occurrence of the variable f and t 1 contains at most one occurrence of the variable f , suppose given two proofs σ f : D $ t : E and σ 1 f : D $ t 1 : E. We cannot have the proof f : D $ if pt, t 1 q : B D, however, we have the following proof

σ f 1 : D $ trf 1 {f s : E ¨$ λf 1 .trf 1 {f s : D E σ 1 f 1 : D $ t 1 rf 1 {f s : E ¨$ λf 1 .t 1 rf 1 {f s : D E ¨$ if pλf 1 .trf 1 {f s, λf 1 .t 1 rf 1 {f sq : B D E b : B $ b : B b : B $ pif pλf 1 .trf 1 {f s, λf 1 .t 1 rf 1 {f sqq b : D E f : D $ f : D f : D, b : B $ pif pλf 1 .trf 1 {f s, λf 1 .t 1 rf 1 {f sqq b f : E f : D $ λb.pif pλf 1 .trf 1 {f s, λf 1 .t 1 rf 1 {f sqq b f : B E
So if we forget about the renaming of variable, we could define IF pt, t 1 q " λb.if pλf.t, λf.t 1 q b f .

States A state is a tensor of boolean for which we can have a match case. More precisely, for n P N ˚, we define by induction the type B n " B b B n´1 with B 1 " B. B n describes states of size n. In the following, we will ignore the term for the associativity of the tensor. In order to precise the decomposition, we will note let x D b y D 1 " t in t 1 to explicit the decomposition when it is ambiguous. There are 2 n base states of size n, given by the 2 n possibilities of associating n times tt or ff. Moreover, there is a constructor to do a match-case on those states, case n pt 0 n , . . . , t 1 n q. We will consider in order to simplify the notations that those indexes are the integers from 0 to 2 n ´1 written in binary, with 1 referring to tt. We define it by induction, and give the typing.

For n " 1, case 1 pt 0 , t 1 q " if pt 1 , t 0 q and for n ě 0 :

case n`1 pt 0 n`1 , . . . , t 1 n`1 q " λs.let s 1 B n b x B " s in case n pt 1 0 n , . . . , t 1 1 n q s 1 with, for all boolean word i, t 1 i " if pt i1 , t i0 q x. With this definition, by noting i " b 1 ¨¨¨b n the state and the boolean word, we have case n pt 0 n , . . . , t 1 n q pb 1 ¨¨¨b n q Ñ ˚case n´1 pt 0 n´1 bn , . . . t 1 n´1 bn q pb 1 ¨¨¨b n´1 q Ñ ˚ti Moreover, we can deduce this rule : @i, 0 ď i ď 2 n ´1, Γ i , dΓ $ t i : D Γ 0 , . . . , Γ 2 n ´1, dΓ $ case n pt 0 , . . . , t 2 n ´1q : B n D

Intermediate lemmas in s T

Proof of theorem 1 We prove theorem 1 saying that a closed and typed term is normal if and only if it is a value. First, we prove by induction on values V that if V is closed and has a typing derivation then V is normal. We treat only some cases and the others are easily deducible from those cases.

-If V " λx.t then V is normal since in the definition of contexts for reductions, we cannot reduce under a λ-abstraction.

-If V " V 0 b V 1 .
V is closed so are V 0 and V 1 . Moreover V has a typing derivation, so it must finish with the introduction of tensor rule, and we deduce that V 0 and V 1 have also a typing derivation. So by induction hypothesis, V 0 and V 1 are normal. Then V has no base reduction possible, and no contexts reductions since V 0 and V 1 are normals, so V is normal.

-If V " zero then V is normal
Now for the other implication,, we prove that if a closed typed term is normal then it is a value. We prove that by induction on terms, again we only detail some interesting cases.

-If t " t 0 t 1 . Suppose, by absurd, that t is a closed typed normal term. Since t has a typing derivation, we know that t 0 and t 1 are also closed typed terms. By definition of contexts in which we can apply reductions, t 0 is normal, and so by induction hypothesis, t 0 is a value. Again, by definition of contexts, t 1 is normal, and so by induction hypothesis, t 1 is a value. So t 0 is a value with an arrow type D D 1 . By looking at the definition of values, either t 0 is a λ-abstraction, either it is one of the functional constructor like if n. If t 0 is a λ-abstraction, as t 1 is a value, we could apply the usual β-rule, so this is not possible because t is normal. If t 0 is if npV, V 1 q, as t 1 is a value of type N , it is the encoding of an integer, and so t is not normal since we could apply one of the if n rule. All the other cases works in the same way, and we deduce that t cannot be normal.

-If t " let x b y " t 0 in t 1 . Suppose that t is a closed typed normal term. Since t has a typing derivation, we know that t 0 has also a typing derivation, and t 0 is closed. By definition of contexts, t 0 is normal and so by induction hypothesis, t 0 is a value. t 0 has a tensor type D b D 1 , and t 0 is a value, by definition of values, t 0 is of the form V b V 1 , this is absurd since in this case t would not be normal. And so, we deduce that t cannot be a normal term.

Proof of lemma 3 We recall point 3 and point 4 of this lemma, and we show how to do the itern case for those points. Let I be an index.

3) If π Γ $ t : D then πrI{as Γ rI{as $ t : DrI{as 4) ωpπrI{asq " ωpπqrI{as Suppose that we have the following proof :

D Ă E E Ă Erb `1{bs σ1 dΓ $ V : D Drb `1{bs ErJ{bs Ă F σ2 Γ, dΓ $ t : Dr1{bs π Γ, dΓ $ iternpV, tq : N J F ωpπq " J `ωpσ2q `J ¨ωpσ1qrJ{bs
We want to prove that πrI{as Γ rI{as $ iternpV, tq : N JrI{as F rI{as By induction hypothesis and point 2 of lemma 3 we have

DrI{as Ă ErI{as

ErI{as Ă Erb `1{bsrI{as σ1rI{as dΓ rI{as $ V : DrI{as Drb `1{bsrI{as

ErJ{bsrI{as Ă F rI{as σ2rI{as Γ rI{as, dΓ rI{as $ t : Dr1{bsrI{as

By using the fact that b must be a fresh variable in Γ , dΓ , J and F , we can suppose, by renaming, that b is not free in I. Then, by lemma 2, we obtain a proof : With weight ωpπrI{asq " JrI{as `ωpσ 2 qrI{as `JrI{as ¨ωpσ 1 qrI{asrJrI{as{bs And so again by lemma 2, ωpπrI{asq " ωpπqrI{as.

Proof of theorem 3 We want to prove that for two indexes I and J, I ď J implies dpIq ď dpJq. First, we prove the following lemma :

Lemma 22. Let I be an index with at most one free variable x, then x dpIq ď I ď Ir1{xs ¨xdpIq . This is proved directly by induction on indexes, and it uses the fact that the constant integers in indexes are non-zero, the image of a variable in a valuation is non-zero and an index is always positive. Now, we prove our theorem by contraposition. Given I, J such that dpIq ą dpJq, we construct two new indexes called I 1 and J 1 that are I and J in which we replaced all variables by a new fresh variable x. The degree stays the same, and we have, by the lemma 22 :

x dpJq`1 ď x dpIq ď I 1 and J 1 ď x dpJq ¨J1 r1{xs.

If we replace x by k " pJ 1 r1{xs `1q (which is a non-zero integer), we obtain I 1 rk{xs ě k dpJq`1 and J 1 rk{xs ď k dpJq ¨pk ´1q.

And so we have I 1 rk{xs ą J 1 rk{xs. We deduce that we have a valuation φ that send all free variables of I and J to k such that I φ ą J φ , so we do not have I ď J. By contraposition, we obtain the point 2 of the theorem 3.

Main theorem in s T

We want to prove theorem 2, first let us recall the statement of this theorem : Let τ Γ $ t 0 : D, and t 0 Ñ t 1 , then there is a proof τ 1 Γ $ t 1 : D such that ωpτ 1 q ă ωpτ q.

We first consider the base-reduction case. Some cases are trivial and we will not develop them, indeed the if-rules can be proved only by using the weakening lemma.

-If t 0 " pλx.tqV , and t 1 " trV {xs such that V is a base-typed term. We have a proof :

π Γ1, dΓ, x : U $ t : D Γ1, dΓ $ λx.t : U D σ Γ2, dΓ $ V : U τ Γ1, Γ2, dΓ $ pλx.tqV : D
with ωpτ q " ωpσq `1 `ωpπq.

Then by lemma 5, we have a proof σ 1 dΓ $ V : U with ωpσq " ωpσ 1 q. Then by using the base value substitution lemma with π and σ 1 , we obtain a proof π 1 Γ 1 , dΓ $ trV {xs : D with ωpπ 1 q ď ωpπq. Finally, by using the weakening lemma, we obtain a proof τ 1 Γ 1 , Γ 2 , dΓ $ trV {xs : D with ωpτ 1 q " ωpπ 1 q ď ωpπq ă ωpτ q.

-If t 0 " pλx.tqV , and t 1 " trV {xs such that V is a non-base-typed term. We have a proof :

π Γ1, dΓ, x : D 1 $ t : D Γ1, dΓ $ λx.t : D 1 D σ Γ2, dΓ $ V : D 1 τ Γ1, Γ2, dΓ $ pλx.tqV : D
With ωpτ q " ωpσq `1 `ωpπq.

Then by using the non-base value substitution lemma with π and σ, we obtain a proof π 1 Γ 1 , Γ 2 , dΓ, $ trV {xs : D with ωpπ 1 q ď ωpπq `ωpσq. And so we have a proof τ 1 " π 1 Γ 1 , Γ 2 , dΓ $ trV {xs : D with ωpτ 1 q " ωpπ 1 q ď ωpπq `ωpσq ă ωpτ q. -If t 0 " let x b y " V 0 b V 1 in t and t 1 " trV 0 {xsrV 1 {ys. We have a proof : With ωpτ q " ωpπq `1 `ωpσ 0 q `ωpσ 1 q. By considering two times the substitution lemmas, either in the base type case or the non-base type case, we obtain a proof τ 1 Γ, Γ 1 , Γ 2 , dΓ $ trV 0 {xsrV 1 {ys such that ωpτ 1 q ď ωpπq `ωpσ 0 q `ωpσ 1 q ă ωpτ q. We do not detail explicitly how to use the substitution lemmas since it is the same as the previous cases.

-If t " iternpV, V 1 qzero and t 1 " V 1 .
We have a proof :

D Ă E E Ă Era `1{as σ1 dΓ $ V : D Dra `1{as ErI{as Ă F σ2 Γ, dΓ $ V 1 : Dr1{as Γ, dΓ $ iternpV, V 1 q : N I F Γ 1 , dΓ $ zero : N I τ Γ, Γ 1 , dΓ $ iternpV, V 1 qzero : F With ωpτ q " I `ωpσ 2 q `I ¨ωpσ 1 qrI{as ě 1 `ωpσ 2 q
We have Dr1{as Ă Er1{as Ă ErI{as Ă F by the index substitution lemma, and the monotonic index substitution lemma since 1 ď I. And so, by the subtyping and weakening lemmas, we have a proof

τ 1 " σ 1 2 Γ, Γ 1 , dΓ $ V 1 :
F with ωpτ 1 q ď ωpσ 2 q ă ωpτ q The proof for the rule iterw with follows the same logic.

-If t " iternpV, V 1 q succpW q and t 1 " iternpV, V V 1 qW . We have a proof :

D Ă E E Ă Era `1{as σ1 dΓ $ V : D Dra `1{as ErI{as Ă F σ2 Γ, dΓ $ V 1 : Dr1{as Γ, dΓ $ iternpV, V 1 q : N I F π Γ 1 , dΓ $ W : N J J `1 ď I Γ 1 , dΓ $ succpW q : N I τ Γ, Γ 1 , dΓ $ iternpV, V 1 q succpW q : F
With ωpτ q " ωpπq `I `ωpσ 2 q `I ¨ωpσ 1 qrI{as We can construct a proof for t 1 :

σ1r1{as dΓ $ V : Dr1{as Dra `1{asr1{as σ2 Γ, dΓ $ V 1 : Dr1{as Γ, dΓ $ V V 1 : Dra `1{asr1{as Dra `1{as Ă Era `1{as Era `1{as Ă Era `1{asra `1{as Era `1{asrJ{as " ErJ `1{as Ă ErI{as Ă F σ1ra `1{as dΓ $ V : Dra `1{as Dra `1{asra `1{as Γ, dΓ $ iternpV, V V 1 q : N J F π Γ 1 , dΓ $ W : N J τ 1 Γ, Γ 1 , dΓ $ iternpV, V V 1 qW : F
With ωpτ 1 q " ωpπq `J `ωpσ 2 q `ωpσ 1 qr1{as `J ¨ωpσ 1 qra `1{asrJ{as And we have ωpτ 1 q ď ωpπq `J `ωpσ 2 q `pJ `1q ¨ωpσ 1 qrJ `1{as so, since J `1 ď I, we have ωpτ 1 q ă ωpπq `I `ωpσ 2 q `I ¨ωpσ 1 qrI{as " ωpτ q The rules for iterw in the cases s 0 and s 1 are follow the same logic. Now we need to verify that a reduction under context strictly decreases the weight. This can be proved directly by structural induction on contexts.

Adding polynomial time functions in EAL

Here we explain very informally how we can add polynomial time functions in the calculus defined in [START_REF] Madet | An elementary affine λ-calculus with multithreading and side effects[END_REF], keeping the same kind of proof relying on the measure.

Suppose given a function f from integers to integers. We define a new constructor f in the classical EAL-calculus, and a new reduction rule f n Ñ f pnq, saying that f applied to the encoding of the integer n is reduced to the encoding of the integer f pnq. We add a cost to this reduction, depending on the integer n, that we call C f pnq. We give a typing rule for this constructor, f has type N N . If this function f is a polynomial time computable function, we can bound the cost function C f pnq by a polynomial function pn `2q d for a certain d, and we can also bound the size of f pnq by the cost, and so f pnq ď pn `2q d . Now if we look at the reduction rule, if we call µpf q the measure for f , we go from µpf q `p1, n `1q to p0, pn `2q d q, if we want to take in consideration the cost, we can add it in the measure, and suppose that in the right part of the reduction we have the measure p0, 2pn `2q d q. Now, see that if µpf q " pd, 1q, this reduction follows the relation R defined in section 3, and with that we can deduce that this construction works with the measure. We have τ H | ∆, x : T 1 $ M : T , and σ H | ∆ $ M 1 : T 1 . Moreover, the number of occurrences of the axiom rule for x in τ is bounded by ω 0 pτ q. Indeed the axiom rule has a weight 1 at position 0, and the only constructor that can shift this weight is the !, but as x is not erased, we know that in a branch of τ that leads to an axiom rule, we do not cross a !.

So by using the general substitution lemma, we obtain a proof τ 1 H | ∆ $ M rM 1 {xs : T with µ n´1 pτ 1 q ď µ n´1 pτ q `ω0 pτ q ¨µn´1 pσq. We can now build the proof τ 1 H | ∆ $ M rM 1 {xs : T π 1 Γ | ∆ 1 , r∆s $!M rM 1 {xs : !T µ n pπ 1 q " p1, µ n´1 pτ 1 qq With µ n pπ 1 q ď p1, pµ n´1 pτ q `ω0 pτ q ¨µn´1 pσqqq ď p1, pµ 1 n pπq `ω1 pπq ¨µn´1 pσqqq And so lemma 14 is verified.

σ 1 Γ 1 | ∆ $ M 1 : W T σ 0 Γ 0 | ∆ $ M 0 : W T σ Γ | ∆ $ M 1 : T π Γ 0 , Γ 1 , Γ | ∆ $ if wpM 0 , M 1 , M 1 q : W T
µ n pπq " µ n pσ 0 q `µn pσ 1 q `µn pσq `10

σ 1 Γ 1 | ∆ $ M 1 : !pT T q σ 0 Γ 0 | ∆ $ M 0 : !pT T q σ Γ | ∆ $ M : !T π Γ 0 , Γ 1 , Γ | ∆ $ iter ! W pM 0 , M 1 , M q : W !T
µ n pπq " µ n pσ 0 q `µn pσ 1 q `µn pσq `10 π Γ | ∆ $ tt : B µ n pπq " 1 1

And @n P N, µ n pτ q " µ n pσq `p4, µ n´1 pσ 1 q `µn´1 pσ 2 qq Note that @n P N, µ n pσq " pk `1q ¨11 . We can construct the proof τ1 :

σ1 H | ∆ $ M : T T σ1 H | ∆ $ M : T T σ2 H | ∆ $ M 1 : T ¨Ḧ | ∆ $ M k´1 M 1 : T H | ∆ $ M k M 1 : T τ 1
Γ1, Γ2, Γ3 | ∆ 1 , r∆s $!pM k M 1 q :!T And @n P N, µ n pτ 1 q " k ¨11 `p1, k ¨µn´1 pσ 1 q `µn´1 pσ 2 qq. We can see that depthpτ 1 q ď depthpτ q. Furthermore, we have ω 0 pτ q ´ω0 pτ 1 q ě 2, so for α ě depthpτ q ě 0, we have µ α pτ 1 q ă lex µ α pτ q. Moreover, k ¨p1 `ω0 pσ 1 qq `ω0 pσ 2 q `2 ď pk `1 `ω0 pσ 1 q `ω0 pσ 2 q `2q 2 this means ω 1 pτ 1 q `2 ď pω 1 pτ q `2q 2 And for 1 ă j ď α, ω j pτ 1 q `2 " k ¨ωj´1 pσ 1 q `ωj´1 pσ 2 q `2 ď pω j´1 pσ 1 q `ωj´1 pσ 2 q `2qpk `1 `ω0 pσ 1 q `ω0 pσ 2 q `2q " pω j pτ q `2qpω 1 pτ q `2q.

We can conclude Rpµ α pτ q `2, µ α pτ 1 q `2q The proof for the rule iter ! W follows the same logic. -If M 0 " rλx k . . . x 1 .tspM 1 1 , . . . , M 1 k´1 , vq and M 1 " rλx k´1 . . . x 1 .trv{x k sspM 1 1 , . . . , M 1 k´1 q, then we have a proof Note that the proof σ induces that v is either an actual integer m, an actual word w or an actual boolean tt or ff. Moreover, @n P N, µ n pσq " |v| ¨11 .

@n P N, µ n pτ q " k´1 ř i"1

µ n pσ i q `|v| ¨11 `kpdpωpπq `Iq `1q ¨10 `ppωpπq `Iqr1{b 1 s ¨¨¨r1{b l s `1q ¨11

With tb 1 , . . . , b l u " F V pIq Y F V pωpτ qq.

From the proof π, we can construct by lemma 3 a proof πr|v|{a k s x k : A |v| k , x k´1 : A a k´1 k´1 , . . . , x 1 : A a1 1 $ t : A Ir|v|{a k s . Note that if A k is the boolean type B, we do not need this substitution. But the following proof is still correct for this case, it would be as if a k is not a free variable, and so the substitution does nothing. For the other imprecise case when A is the boolean type B, just consider that I " 1 and so there is no substitution in I. Furthermore, we can construct a proof σ 1 ¨$s T v : A |v| k . By the base-value substitution lemma in s T , we have a proof π 1 x k´1 : A a k´1 k´1 , . . . , x 1 : A a1 1 $ trv{x k s : A Ir|v|{a k s and we have ωpπ 1 q ď ωpπqr|v|{a k s. We can now construct the proof τ 1 : @n P N, µ n pτ 1 q " k´1 ř i"1

µ n pσ i q `pk ´1qpdpωpπ 1 q `Ir|v|{a k sq `1q ¨10 ppωpπ configuration on a Turing machine after b steps, with B q coding the state, and then w 0 b b b w 1 represents the tape, with b being the head, w 0 represents the reverse of the word before b, and w 1 represents the word after b. We give her some terms used in the simulation of a Turing-machine :

-Given an initial state s of size q, we can code this state in a term s : B q . Then we can construct the term init with type w : W aw , n : N an $ init : Conf 1 . For this, pose init " b pif wpλw 1 .ff b w 1 , λw 1 .tt b w 1 , ff b q wq b s. -Given for each state s of size q and boolean b a transition function δpb, sq Ă tlef t, right, stayu ˆt0, 1u ˆt0, 1u q , we can construct a term step with type ¨$ step : Conf b Conf b`1 . For this, pose step " λc.let x b b b y b s " c in pcase q`1 pt 0 q`1 , . . . , t 1 q`1 qq pb b sq. b b s can be seen as a binary word of size q `1, and we define t bbs according to δpb, sq. For example, if δpb, sq " plef t, b 1 , s 1 q, we define t bbs " pif wpλw.w b ff, λw.w b tt, b ffq xq b s b 1 pyq b s 1 . Remark that the duplicated variables are x and y, which are base type variables. -Given for states of size q a function accept : B q Ñ B, we can construct a term f inal with ¨$ f inal :

Conf b B, defined by f inal " λc.let x b b b y b s " c in case q pt 0 q , t 1 q q s, with t s " acceptpsq. Now, suppose given a one-tape deterministic Turing machine T M on binary words such that for words w, T M works in time 2

P p|w|q 2k

. TM has an infinite tape, this means that on an input w, the Turing-machine can read outside the bound of w and in this case, it reads a 0. We can compute a term in EAL t T M such that ¨| ¨$ t T M :!W ! k`1 B and on an input !w, the term reduces to the term ! k`1 b with b " tt if w is accepted by T M , and b " ff otherwise.

For this, we show how to decompose the work in order to construct this term.

1. We duplicate the word given in input.

2. With one of those words, we compute the length of the word, using the term ¨| ¨$ λw.rλx 1 .length x 1 spwq : W N 3. Now that we have the size, we can compute 2

P p|w|q 2k

following the results from section 3.4. So we obtain !wb! k`1 n with n representing 2 P p|w|q 2k

. By using the coercion, we obtain ! k`1 wb! k`1 n 4. Now in s T, given a word w : W aw and an integer n : N an , we can code the input w in the type Conf 1 using the term init, by using for states a size q such that all states of T M can be coded in binary words of size q. Moreover, given the term ¨$ step : Conf b Conf b`1 that represents one step of the Turing machine T M , we can use the constructor itern to create a term of type N an Conf an 5. Given this term, we can apply it to n to simulate n steps of the Turing-machine T M . And by using the term f inal we can extract the result of the computation 6. This simulation in s T allows us to construct a term in EAL that simulates the Turing-machine T M with type p! k`1 W b! k`1 N q ! k`1 B.

So in conclusion, we can effectively simulate T M in a term of type !W ! k`1 B.

Fig. 4 .

 4 Fig. 4. Type system for the classical EAL

Fig. 5 .

 5 Fig. 5. Base rules for enriched EAL-calculus

  π

Fig. 8 .

 8 Fig. 8. Typing rule and measure for the s T call

  subsetsum " λw S .IT ERW pλw b w r .let w 0 b w 1 " Extract | w in w 0 b w r , λw b w r .let w 0 b w 1 " Extract | w in w 0 b pBinaryadd w r w 1 q, w S b s 0 p qq We obtain a type W I¨J for the output because we iterate at most J times a function for binary addition which can be given a type W a¨I W I W pa`1q¨I . Note that to define this function, we use extract | defined previously. Then, we can solve the SUBSET SUM problem in the same way as SAT with the term : SolvSubsetSum " λk b w S .let !r " pexp rocc | spw S qq b pcoerc w S q b pcoerc kq in !rλn, w, k.RECpλval, b.or b pequal k psubsetsum w pCunarytobinary pocc | wq valqqq, ffq nsprq

Theorem 8 .

 8 Terms of type !W ! k`1 B characterize the class 2k-EXP.

  σ0 Γ0, dΓ $ V0 : D0 σ1 Γ1, dΓ $ V1 : D1 Γ0, Γ1, dΓ $ V0 b V1 : D0 b D1 π Γ, x : D0, y : D1, dΓ $ t : D τ Γ, Γ0, Γ1, dΓ $ let x b y " V0 b V1 in t : D

6. 4

 4 Substitution lemmas in enriched EALτ H | ∆, x : T 1 $ M : T π Γ | ∆ 1 , r∆s, x : rT 1 s $!M : !T µ n pπq " p1, µ n´1 pτ qq

6. 5

 5 Type system for words and boolean in EALπ Γ | ∆ $ : W µ n pπq " 1 1 σ Γ | ∆ $ M : W π Γ | ∆ $ s i pM q : W µ n pπq " µ n pσq `11

@ 1 ď

 1 i ď pk ´1q σi Γi | ∆ $ M 1 i : Ai σ Γ k | ∆ $ v : A k π x k : A a k k , . . . , x1 : A a 1 1 $ s T t : A I τ Γ, Γ1, . . . Γ k | ∆ $ rλx k . . . x1.tspM 1 1 , . . . , M1k´1 , vq : A

@ 1 ď

 1 i ď pk ´1q σi Γi | ∆ $ M 1 i : Ai π 1 x k´1 : A a k´1 k´1 , . . . , x1 : A a 1 1 $ s T trv{x k s : A Ir|v|{a k s τ 1 Γ, Γ k , Γ1, . . . Γ k´1 | ∆ $ rλx k´1 . . . x1.trv{x k sspM 1 1 , . . . , M 1 k´1 q : A Let us denote tb 1 1 , . . . , b 1 l 1 u = F V pIq Y F V pωpτ qq Y F V pωpτ 1 qq.

(Lin Ax) Γ, x : T | ∆ $ x : T (Glob Ax) Γ | ∆, x : T $ x : T Γ, x : T | ∆ $ M : T 1 (λ-Abs) Γ | ∆ $ λx.M : T T 1 Γ | ∆ $ M : T 1 T Γ 1 | ∆ $ M 1 : T 1 (App) Γ, Γ 1 | ∆ $ M M 1 : T H | ∆ $ M : T (! Intro) Γ | ∆ 1 , r∆s $!M : !T Γ 1 | ∆ $ M : !T Γ | ∆, x : rT s $ M 1 : T 1 (! Elim) Γ, Γ 1 | ∆ $ let !x " M in M 1 : T 1 Γ | ∆ $ M : T α fresh in Γ ,∆ (@ Intro) Γ | ∆ $ M : @α.T Γ | ∆ $ M : @α.T (@ Elim) Γ | ∆ $ M : T rT 1 {αs

q `Ir|v|{a k sqr1{b 1 1 s ¨¨¨r1{b 1 l 1 s `1q ¨11 . With this, we can first see that depthpτ 1 q ď depthpτ q.

Values Associated to Restricted Reductions. We can now give the form of closed normal terms for i-reductions. For that, we define for all i P N, closed i-values V i by the following grammar :

And now we can prove the following lemma Lemma 20. Let M be a term. If M is closed and has a typing derivation then, for all i P N, if M is normal for i-reductions then M is a i-value V i .

We prove this by induction on the term M . Some cases can be found in the appendix, section 6.8.

From the previous results, we now have that, from a typed term M , we can reach the normal form for i-reductions for M in less than t i pµ i pπq `2q reductions, and this form is a i-value.

A Characterization of 2k-EXP

Now, we show that the type !W ! k`1 B characterizes the class 2k ´EXP for k ě 0. We recall that 2 x k is defined by 2 x 0 " x and 2 x k`1 " 2 2 x k . The class k ´EXP is the class of problem solvable by a Turing machine that works in time 2 ppnq k on an entry of size n. First we show that the number of reductions for such a term is bounded by a tower of exponentials of height 2k.

Let w be a word of size |w|. We can compute the result of t !w in less than a 2k-exponential tower in the size of w.

Observe that the result of this computation is of type ! k`1 B, and a pk `2q-value of type ! k`1 B is exactly of the form ! k`1 tt or ! k`1 ff. So it is enough to only consider pk `2q-reductions to compute the result, by lemma 20.

The measure µ n of t !w is µ n " µ n pπq `2 ¨10 `|w| ¨12 . By theorem 7, we can bound the number of reductions from t !w by t k`2 pµ k`2 `2q.

By definition, in t k`2 pµ k`2 `2q, we can see that the weight at position 2, where the size of w appears, is at height 2k. This concludes the proof of lemma 21. Now we have to prove that we can simulate a Turing-machine in our calculus. This proof is usual in implicit complexity [START_REF] Baillot | Characterizing polynomial and exponential complexity classes in elementary lambda-calculus[END_REF][START_REF] Baillot | On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy[END_REF]. The first thing we prove is the existence of a term in s T to simulate n steps of a deterministic Turing-machine on a word w. We give here the intuition of the encoding, and a more detailed explanation on how to work with this encoding can be found in the appendix, section 6.9.

Suppose given two variables w : W aw and n : N an , we note Conf b the type W aw`b b B b W aw`b b B q , with q an integer and B q being q tensors of booleans. This type represents a configuration on a Turing machine after b steps, with B q coding the state, and then w 0 b b b w 1 represents the tape, with b being the position of the head, w 0 represents the reverse of the word before b, and w 1 represents the word after b. We can then define multiple term in s T with this encoding. First we have a term init such that w : W aw , n : N an $ init : Conf 1 and init computes the initial configuration of the Turing machine. Then, we have a term step with ¨$ step : Conf b Conf b `1 that computes the result of the transition function from a configuration to the next one, and finally we have a term f inal with ¨$ f inal : Conf b B verifying if the final configuration is accepted or not. Now that we have that, if we can compute an integer n bounding the number of steps of a Turingmachine on an entry w, then we can effectively simulate the Turing-machine in our calculus using a s T call. As explained in the example in the previous section on enriched EAL, we can compute tower of exponentials if we have enough modalities !. This shows that, by using a ! modality, we can increase the integer n we can compute and thus increase the working time of the Turing-machine we want to simulate. A more detailed explanation on how to simulate a Turing machine is given in the appendix, section 6.9. With this, using the lemma 21, we have the following theorem

µ n pσq `µn pτ q `10 6.6 Lemmas for t α and R

Shift Lemma

We want to prove the shift lemma, lemma 16. First we recall the statement of this lemma : Let k P N ˚. Let µ " pω 0 , . . . , k ¨ωi´1 , ω i , . . . ω n q and µ 1 " pω 0 , . . . , ω i´1 , k ¨ωi , . . . ω n q. Then t α pµ 1 q ď t α pµq.

Let us define µ 0 " pω 0 , . . . , ω i´2 q.

α ¨k ¨ωi ď pα ¨ωi q 2 pα¨pk´1q¨ω i´1 q 2 tα pµ 0 q pα ¨k ¨ωi q 2 pα¨ω i´1 q 2 tα pµ 0 q ď pα ¨ωi q 2 pα¨pk´1q¨ω i´1 q 2 tα pµ 0 q ¨2pα¨ω i´1 q 2 tαpµ 0 q and so, t α pµ 0 , pω i´1 , k ¨ωi qq ď pα ¨ωi q 2 pα¨k¨ω i´1 q 2 tαpµ 0 q " t α pµ 0 , pk ¨ωi´1 , ω i qq We can now obtain t α pµ 1 q ď t α pµq by monotonicity of exponential. This concludes the proof of lemma 16.

Link between t α and R We want to prove Theorem 4. First let us recall the statement of this theorem : Let µ, µ 1 P N n`1 and α ě n, α ě 1. If Rpµ, µ 1 q then t α pµ 1 q ă t α pµq Suppose Rpµ, µ 1 q. Using the notations from the definition of R, we have µ ě pω 0 , . . . , ω 1 i0 `d, ω i0`1 , . . . , ω n q and we have µ 1 ď pω 0 , . . . , ω i0´1 , ω 1 i0 , ω i0`1 ¨pω i0`1 q d´1 , . . . , ω n ¨pω i0`1 q d´1 q. Let us call µ 0 " pω 0 , . . . , ω i0´1 q. α ¨d ě 1 so α ¨d ă 2 α¨d so, as ω i0`1 ě 2, we have pω i0`1 q α¨d ă pω i0`1 q 2 α¨d so α ¨pω i0`1 q α¨d ă pα ¨ωi0`1 q 2 pα¨dq 2 tα pµ 0 q and so pα ¨pω i0`1 q α¨d q 2 pα¨ω 1 i 0 q 2 tαpµ 0 q ă pα ¨ωi0`1 q 2 pα¨pd`ω 1 i 0 qq 2 tαpµ 0 q

So we obtain t α pω 0 , . . . , ω i0´1 , ω 1 i0 , pω i0`1 q α¨d q ă t α pω 0 , . . . , ω i0´1 , ω 1 i0 `d, ω i0`1 q. By lemma 15, since ω i0`1 ¨pω i0`1 q pn´i0qpd´1q ď pω i0`1 q α¨d , and by monotonicity of the exponential, we obtain t α pω 0 , . . . , ω i0´1 , ω 1 i0 , ω i0`1 ¨pω i0`1 q pn´i0qpd´1q , . . . , ω n q ă t α pω 0 , . . . , ω 1 i0 `d, ω i0`1 , . . . , ω n q. Using several times the shift lemma, we obtain t α pω 0 , . . . , ω i0´1 , ω 1 i0 , ω i0`1 ¨pω i0`1 q d´1 , . . . , ω n ¨pω i0`1 q d´1 q ă t α pω 0 , . . . , ω 1 i0 `d, ω i0`1 , . . . , ω n q. Again by lemma 15, we obtain t α pµ 1 q ă t α pµq This finishes the proof of theorem 4.

Main theorem for the enriched EAL calculus

In this section, we prove the main theorem for the enriched EAL calculus : Let τ Γ | ∆ $ M 0 : T and M 0 Ñ M 1 . Let α be an integer equal or greater than the depth of τ . Then there is a proof τ 1 Γ | ∆ $ M 1 : T such that Rpµ α pτ q `2, µ α pτ 1 q `2q. Moreover, the depth of τ 1 is smaller than the depth of τ .

We prove this by first considering the base reductions. The case for the if -constructors are direct, it is a simple consequence of lemma 17. We detail the other cases :

-If M 0 " pλx.M qM 1 and M 1 " M rM 1 {xs, we have a proof :

T is given by the linear substitution lemma. As a consequence, we have @n P N, µ n pτ 1 q ď µ n pπq `µn pσq. So we have @n P N, µ n pτ 1 q ă µ n pτ q. As a consequence, it is still true for n " α ě depthpτ q and the depth of τ 1 is smaller than the depth of τ , moreover, by the lemma 17, we have Rpµ α pτ q `2, µ α pτ 1 q `2q -If M 0 " let !x "!M 1 in M and M 1 " M rM 1 {xs then we have a proof :

By the discharged substitution lemma, we obtain a proof π 1 Γ 2 | ∆ 1 , r∆s $ M rM 1 {xs : T , with @n P N, µ n pπ 1 q ď pω 0 pπq, pµ 1 n pπq `ω1 pπq ¨µn´1 pσqqq. We can now use the weakening lemma to obtain τ 1 Γ 1 , Γ 2 | ∆ 1 , r∆s $ M rM 1 {xs : T . By the precedent upper-bound, we obtain depthpτ 1 q ď depthpτ q. Moreover, ω 0 pτ q ´ω0 pτ 1 q ě 2, and so for α ě depthpτ q ě 0, we have µ α pτ 1 q ă lex µ α pτ q. Finally, for α ě j ą 0, we have ω j pτ 1 q `2 ď ω j pπq `ω1 pπq ¨ωj´1 pσq `2 ω j pτ 1 q `2 ď pω j pπq `ωj´1 pσq `2q ¨pω 1 pπq `ω0 pσq `2q ω j pτ 1 q `2 ď pω j pτ q `2q ¨pω 1 pτ q `2q And so we obtain Rpµ α pτ q `2, µ α pτ 1 q `2q. -If M 0 " let x b y " M b M 1 in N and M 1 " N rM {xsrM 1 {ys, we have a proof :

And @n P N, µ n pτ q " µ n pπq `µn pσq `µn pσ 1 q `2 ¨10 Using two times the linear substitution lemma, we obtain a proof τ 1 Γ, Γ 1 , Γ 2 | ∆ $ N rM {xsrM 1 {ys : T 2 with @n P N, µ n pτ 1 q ď µ n pπq `µn pσq `µn pσ 1 q ă µ n pτ q. And so depthpτ 1 q ď depthpτ q and for α ě depthpτ q, µ α pτ 1 q ă µ α pτ q. By lemma 17, we have Rpµ α pτ q`2, µ α pτ 1 q2 q -If M 0 " iter ! N p!M, !M 1 q k and M 1 "!pM k M 1 q, then we have a proof :

Moreover, by theorem 3, since ωpπ 1 q `Ir|v|{a k s ď pI `ωpπqqr|v|{a k s, we have dpωpπ 1 q `Ir|v|{a k sq ď dppI `ωpπqqr|v|{a k sq ď dpI `ωpπqq. By the theorem 3, pI `ωpπqqr|v|{a k s ď |v| dpI`ωpπqq ¨pI `ωpπqqr1{a k s By the lemma 3, pI `ωpπqqr|v|{a k sr1{b 1 1 , . . . , b 1 l 1 s ď |v| dpI`ωpπqq ¨pI `ωpπqqr1{b 1 1 , . . . , b 1 l 1 s (the substitution for a k is either one of the b 1 by definition, either irrelevant if a k does not appear in the indexes). Now from those results, we have @n P N,

µ n pσ i q `pk ´1qpdpωpπq `Iq `1q ¨10 `p|v| dpI`ωpπqq ¨pI `ωpπqqr1{b 1 1 , . . . , b 1 l 1 s `1q1 1 .

Now we can prove Rpµ α pτ q `2, µ α pτ 1 q `2q : By the precedent bound we have ω 0 pτ q ´ω0 pτ 1 q ě dpωpπq `Iq `1.

ω 1 pτ 1 q `2 ď pω 1 pτ q `2q ¨pω 1 pτ q `2q dpωpπq`Iq

And for 1 ă j ď α,

ω j pσ i q `2 " ω j pτ q `2 ď pω j pτ q `2qpω 1 pτ q `2q dpωpπq`Iq

This proves Rpµ α pτ q `2, µ α pτ 1 q `2q. -If M 0 " rt 0 spq and M 1 " rt 1 spq with t 0 Ñ t 1 in s T . We have a proof :

@n P N, µ n pτ q " p1 `pωpπq `Iqr1{b 1 , . . . , b l sq ¨11 with tb 1 , . . . , b l u " F V pIq Y F V pωpπqq By the theorem 2, the main theorem of s T , we have a proof π 1 ¨$s T t 1 : A I with ωpπ 1 q ă ωpπq. So we can construct

Let us denote tb 1 1 , . . . , b 1 l 1 u all the free variables in I, ωpπq and ωpπ 1 q. @n P N, µ n pτ 1 q " p1 `pωpπ 1 q `Iqr1{b 1 1 , . . . , b 1 l 1 sq ¨11 . We directly see that the depth does not increase. Remark that the depth of τ is greater than 1 in this case We have by lemma 3, pωpπ 1 q `Iqr1{b 1 1 , . . . , b 1 l 1 s ă pωpπq `Iqr1{b 1 1 , . . . , b 1 l 1 s. And so, for α ě depthpτ q ě 1, µ α pτ 1 q ă µ α pτ q, and so we have Rpµ α pτ q `2, µ α pτ 1 q `2q. Remark that as opposed to all the precedent cases, µ 0 pτ q and µ 0 pτ 1 q are equal, and so we need to look at position 1 to see that the measure strictly decreases. This remark is primordial in the proof of another lemma, lemma 19.

-If M 0 " rvspq and M 1 " v. The fact that M 0 can be typed by τ indicates that v is either an actual integer, a word or a boolean. With this remark, the typing τ 1 of M 1 is just the usual typing for those values. Moreover, we know the weight in s T and the measure in EAL for the typing proof of a value, in s T the weight is 0 and in EAL the measure is |v| ¨11 . Furthermore, if π ¨$s T v : A I , then we know that |v| ď I. With this, we have µ n pτ q " p1 `Ir1{F V pIqsq ¨11 and µ n pτ 1 q " |v| ¨11 . By the lemma 3, we have |v| ď Ir1{F V pIqs and so for n ě 1, µ n pτ 1 q ă µ n pτ q. This gives us Rpµ α pτ q `2, µ α pτ 1 q `2q. And the fact that the depth does not increase is direct.

Remark that as the precedent case, we need to look at position 1 to see that the measure strictly decreases.

Now we need to work on the reductions under a context. For this we work by induction on contexts, and what we have done previously is the base case. For any inductive case of context except the ! case, the subject reduction and the fact the the depth does not increase are direct. Then, the relation between the measures is a consequence of lemma 18

When the context has the form C "!C 1 , the notion of depth is crucial for this case. Indeed suppose M Ñ M 1 , M 0 "!M and M 1 "!M 1 . With the proof τ for M 0 , we obtain a proof π for M , this gives us by induction hypothesis a proof π 1 for M 1 , and this gives us a proof τ 1 for M 1 .

Moreover, @n P N, µ n pτ q " p1, µ n´1 pπqq and µ n pτ 1 q " p1, µ n´1 pπ 1 qq.

As depthpπ 1 q ď depthpπq we have depthpτ 1 q " depthpπ 1 q `1 ď depthpπq `1 " depthpτ q. And for α ě depthpτ q, then pα ´1q ě depthpπq. And with Rpµ α´1 pπq `2, µ α´1 pπ 1 q `2q given by the induction hypothesis, we can easily deduce Rpµ α pτ q `2, µ α pτ 1 q `2q.

Remark that this proof shows that if we had Rpµ n pπq `2, µ n pπ 1 q `2q we obtain Rpµ n`1 pτ q `2, µ n`1 pτ 1 q `2q. This remark is important for the proof of lemma 19.

This concludes the proof of theorem 5.

i-values and i-normal forms

We want to prove lemma 20, saying that Let M be a term. If M is closed and has a typing derivation then, for all i P N, if M is normal for i-reductions then M is a i-value V i .

We prove that by induction on terms. Note that the case i " 0 is always direct since i-values are all terms, so we only need to work for i P N ˚. We detail here some cases :

and typed. Suppose, by contradiction, that M is normal for i-reductions. Then, M 0 and M 1 are also normals for i-reductions. And they are also closed and typed. So by induction hypothesis, M 0 and M 1 are i-values. By typing, we have a proof ¨| ¨$ M 0 : T T 1 . And so we have different possible case for M 0 : ' M 0 " λx.M 1 , in this case we have M Ñ i M 1 rM 1 {xs, and this contradicts the fact that M is normal for i-reductions. ' M 0 " if npV i 0 , V i 1 q. In this case, M 1 has type N . But the only i-values of type N are actual integers n since i ě 1, and so we can reduce M by the if n-rule. This contradicts our hypothesis. ' For iter ! N , if , if w and iter ! W , we have a similar proof as the one for the if n case. Finally, we have indeed a contradiction. So M is not normal for i-reductions.

-If M "!M 1 , M closed and typed. Then M 1 is also closed and typed. Let i P N ˚. Suppose that M is normal for i-reductions, then by definition, M 1 is normal for pi ´1q-reductions. So, by induction hypothesis, M 1 is a pi ´1q-value, and so M is indeed a i-value. -If M " let !x " M 0 in M 1 , M closed and typed, then M 0 is also closed and typed. Let i P N ˚, and suppose that M is normal for i-reductions. Then by definition M 0 is also normal for i-reductions, and so by induction hypothesis, M 0 is a i-value. Furthermore, by typing, M 0 had a type of the form !T , and since i ě 1 and M 0 is a i-value, we obtain that M 0 has the form M 0 "!M 1 , and so M can be reduced. -If M " rλx k . . . x 1 .tspM 1 , . . . , M k q. M closed and typed. If k ą 0, then as previously, if we suppose M normal, we obtain that M k must be of the form v, and this is absurd since for i ě 1, M would be reducible. If k " 0, then if we suppose M normal, it means that t is normal, closed, and typed, and so by theorem 1, t is of a form v, and so M is not normal.

This concludes the proof.

Complexity Results

We recall the notations. We are given two variables w : W aw and n : N an . n is the number of steps of the Turing machine and w is the input. Conf b is the type W aw`b b B b W aw`b b B q . This type represents a