Iryna Andriyanova
email: iryna.andriyanova@ensea.fr

Emina Soljanin

IR-HARQ Schemes with Finite-Length Punctured LDPC Codes over the BEC

The incremental redundancy hybrid ARQ (IR-HARQ) schemes based on finite-length LDPC codes are considered in this paper. The transmission is assumed to take place over time varying binary erasure channels, such as mobile wireless channels at the applications layer for instance. Also, the iterative decoding is supposed. Two following issues are addressed: a) establishment of transmission rules for the m-th transmission after m -1 unsuccessful ones; b) approximation of the throughput and delay performance which would be accurate for finite codelengths, down to several hundreds of bits.

I. INTRODUCTION

Hybrid ARQ transmission schemes combine the conventional ARQ with forward error correction. In applications with fluctuating channel conditions, such as mobile and satellite packet data transmission, a scheme known as incremental redundancy hybrid ARQ (IR-HARQ) or Type II HARQ achieves higher throughput efficiency by adapting its error correcting code redundancy to varying channel conditions. Because of that, the scheme has been adopted by a number of standards for mobile phone networks. IR-HARQ is considered to be one of the most important features of the CDMA2000 1xEV-DO Release 0 and Revision A systems [START_REF] Wu | The cdma2000 high rate packet data system[END_REF], [START_REF] Bhushan | CDMA2000 1xEV-DO revision A: a physical layer and mac layer overview[END_REF]. A historic overview of HARQ schemes, up to 1998, can be found in [START_REF] Costello | Applications of errorcontrol coding[END_REF]. For a survey of more recent developments, we direct the reader to [START_REF] Lott | Hybrid ARQ: theory, state of the art and future directions[END_REF] and references therein.

In the third generation wireless standards, the IR-HARQ scheme resides in the physical layer and operates over time varying fading channels. The scheme is based on a turbo code dating back to the IS-95 standard. A possible replacement of this code by an LDPC or a fountain code was considered in [START_REF] Soljanin | Incremental redundancy hybrid ARQ with LDPC and Raptor codes[END_REF]. In this paper we are concerned with a performance approximation of IR-HARQ schemes based on LDPC codes of some finite codelength n, under iterative decoding. For simplicity, it is assumed that the schemes operate over time varying binary erasure channels (BECs). Inspite of simplicity of the channel model, it is already of interest as it can be used for the applications layer in environments with time varying or unknown channels.

IR-HARQ schemes operates as follows. At the transmitter, the user data bits are encoded by a a low rate code, referred to as the mother code. Initially, only a selected number of encoded bits are transmitted, and the decoding is attempted at the receiving end. If the decoding fails, the transmitter is notified, and it sends additional parity bits, possibly under different channel conditions and/or at different power. Decoding is again attempted at the receiving end, where the new bits are combined with those previously received. The procedure is repeated after each subsequent transmission request until all the parity bits of the mother code are transmitted.

The fundamental decision that the transmitter has to make in the course of this protocol is how many bits bits to send in transmission m after a failed transmission m -1 to achieve a particular tradeoff between the throughput and the number of transmissions. In this paper we address this question for IR-HARQ schemes are based on finite-length, iteratively decoded LDPC codes operating over time varying BECs. Another important question that we investigate is an accurate approximation of the average throughput and the average delay for the same type of scheme. The first issue received a limited attention in the literature, being only considered to some extent for IR-HARQ schemes operating at the physical layer over time varying fading channels in 3GPP and 3GPP2 standards' committees and in [START_REF] Soljanin | Hybrid ARQ with random transmission assignments[END_REF], [START_REF] Soljanin | Incremental redundancy hybrid ARQ with LDPC and Raptor codes[END_REF]. The second issue, on the contrary, was quite intensively investigated, see for instance [START_REF] Sesia | Incremental redundancy hybrid ARQ schemes based on Low-Density Parity-Check codes[END_REF], [START_REF] Soljanin | Incremental redundancy hybrid ARQ with LDPC and Raptor codes[END_REF], [START_REF] Levorato | Performance analysis of type ii hybrid ARQ with Low-Density Parity-Check codes[END_REF]. However, the obtained results only give bounds, obtained either under maximum-likelihood decoding assumption, either under (more practical) iterative decoding, but based on the bit error probability, which means that the bound is tight only for large codelengths. The approach taken in this paper is based on the block error performance under iterative decoding, which is the main novelty compared to existing results. This paper is organized as follows: In Sec. II, we describe the mother code model, our IR-HARQ protocol and multiple transmissions channel model. We also derive transmission rules for two approximations of the channel model, used to simplify the analysis. In Sec. III, we derive expressions for the average throughput and delay of the protocol. In Sec. IV, we evaluate numerically the protocol performance of a (3, 6) LDPC code based IR-HARQ scheme. We then discuss our observations and future work.

II. IR-HARQ SCHEMES

A. The Mother Code

The mother code is taken at random from an irregular LDPC code ensemble of length n, parametrized by degree distributions λ(x) and ρ(x) (see [START_REF] Richardson | Modern coding theory[END_REF] for more details about LDPC codes). Note that each code in the ensemble corresponds to a different Tanner graph with n variable and k check nodes, in which fraction iλ i /( i iλ i ) of the variable nodes have degree i, 1 ≤ i ≤ n, and fraction jρ j /( j jρ j ) of the check nodes have degree j, 1 ≤ j ≤ k. The performance of iterative decoding of such ensembles is well understood when n is sufficiently large and when they are used for a transmission over a channel with some fixed erasure rate ǫ. Namely, as long as ǫ < ǫ * where

ǫ * = min x∈(0,1) x λ(1 -ρ(1 -x))
, the iterative message passing algorithm leads to vanishing biterasure probability as the number of iterations grows.

B. The Multiple-Transmissions Model and Protocol

We consider an IR HARQ scheme with at most M transmissions. We assume that the channel erasure probability during a single transmission does not change, and is equal to ǫ j during transmission j, 1 ≤ j ≤ M . Prior to transmission j, the transmitter knows the channels of the previous transmissions, that is, ǫ 1 , . . . , ǫ j-1 , and may or may not know ǫ j .

If transmission m -1 fails, for 1 ≤ m < M , the transmitter needs to decide how many and which bits to send in transmission m, and at which power. For a given power, higher number of transmitted bits improves the probability of successful decoding, and therefore decreases the expected number of transmissions. On the other hand, higher number of transmitted bits reduces the expected throughput. Our first objective is to determine the transmission rules based on the knowledge of the used LDPC ensemble.

We first have to understand the performance of iterative decoding of our code ensembles after each transmission. To that end, we adopt a probabilistic model in which the transmitter assigns a bit corresponding to a variable node of degree i to transmission j with probability q ij1 . Clearly, the transmitter has also the constraint (known as rate compatible puncturing) to assign to transmission j only the bits which have not been assigned to any of the previous transmissions. The IR-HARQ protocol outlined below implements our model while conforming to rate compatible puncturing; it is based on the one proposed in [START_REF] Soljanin | Hybrid ARQ with random transmission assignments[END_REF]. The values of q ij are determined prior to transmission j, which can be done by using one of the approaches we propose in Sec. II-D.

IR-HARQ Protocol

Let V i be the set the variable nodes with degree i. Before the IR HARQ protocol starts 1) For each variable node v of degree i, generate a number θ v independently and uniformly at random over [0, 1).

2) Determine q ij (see Sec. II-D) 3) Compute p i1 as p i1 = 1 -q i1 . 4) For each node v s.t. θ v ≥ p i1 , assign bit corresponding to v to transmission 1. If transmission j -1 fails for 2 ≤ j < M -1 1) Determine q ij (see Sec. II-D). 2) Compute p ij as p ij = p i(j-1) -q ij . 3) For each node v s.t. p ij ≤ θ v < p i(j-1)
, assign the bit corresponding to v to transmission j.

If transmission M -1 fails transmit all remaining bits.

The values of q ij can be determined by one of two methods derived in Sec. II-D. These methods are based on two following approximations of our multiple transmissions channel model for each IR transmission, the so called equivalent erasure channel and the equivalent punctured code model:

1) Equivalent Erasure Channel Approximation: Under our model, after m transmissions, a bit corresponding to a variable node of degree i will not reach the destination if it is assigned to one of the first m transmissions and then erased by the channel (which happens with the probability m j=1 q ij ǫ j ) or if it is simply not assigned to one of the first m transmission (which happens with probability 1 -m j=1 q ij ). Equivalently, after m transmissions, a bit corresponding to a variable node of degree i is erased independently and uniformly at random with probability ν im given by

ν im = (1 - m j=1 q ij ) + m j=1 q ij ǫ j = 1 - m j=1 q ij (1 -ǫ j ).
Consequently, the expected number of erased bits after the first m transmissions is given by

ν m = i λ i ν im . (1)
Therefore, upon transmission m, we can approximate our model as that of the mother code being sent over a BEC with erasure rate ν m .

2) Equivalent Punctured Code Approximation: By using the above stated IR-HARQ protocol, the bits that the transmitter chooses to sent up to the m-th transmission, can be equivalently seen as obtained by implementing a puncturing device which punctures a bit corresponding to a variable node of degree i with probability p im , where p im = 1 -m j=1 q ij , or as shown within the protocol above

p i1 = 1 -q i1 , and p ij = p i(j-1) -q ij for 1 < j ≤ M. (2)
Given that a bit corresponding to a variable node of degree i is assigned to one of the first m transmissions, it gets erased with probability ( m j=1 q ij ǫ j )/( m k=1 q ij ). So, we can model our IR-HARQ protocol through transmission m as transmission of the punctured mother code over a BEC with erasure rate

ε m = i λ i m j=1 q ij ǫ j m k=1 q ij , (3)
where the considered bit is punctured with probability p im .

C. Performance at Transmission m Lemma 2.1: If an LDPC code based IR-HARQ scheme assigns a bit corresponding to a variable node of degree i to transmission j with probability q ij , then in the process of iterative decoding after transmission m is complete, the average probability x ℓ that the message from a variable node to a check node in the ℓth iteration is the erasure is given by

x m ℓ = i λ i ν im [1 -ρ(1 -x m ℓ-1 )] i-1
Proof: In the ℓth iteration, a check-to-variable node message sent by a degree i check node is the erasure message if any of the (i-1) incoming messages is an erasure, which on the average occurs with probability 1 -(1 -x m ℓ-1 ) i-1 . Thus the expected value of the erasure probability of a check-tovariable message in the ℓth iteration is equal to 1-ρ(1-x m ℓ-1 ). Now consider a variable-to-check message in the ℓth iteration sent by a variable node of degree i. It will be an erasure if the bit corresponding to the node was not received (which happens with probability ν im ) and each of the (i-1) incoming check-to-variable messages are erasures. Thus, it is an erasure with probability ν im [1 -ρ(1 -x m ℓ-1 )] i-1 , and on the average,

x m ℓ = i λ i ν im [1 -ρ(1 -x m ℓ-1 )] i-1 .

D. Transmission Rules

Suppose that m-1 transmissions have taken place and were unsuccessful. We now need to decide which fraction q im of bits corresponding to the variable nodes of degree i to assign to transmission m in order to have a successful decoding with high probability. We propose two following rules on which a decision can be made.

1) Rules Based on the Density Evolution for the Multiple Channel Transmissions and the Equivalent Erasure Channel

Approximation: Based on Lemma 2.1, the iterative algorithm leads to vanishing bit-erasure probability as the number of iterations grows if we can choose q im (1 -ǫ m ) so that

x - i λ i ν im [1 -ρ(1 -x)] i-1 < 0 for all x ∈ (0, 1).
To simplify the computations that would have to be done by the transmitter at each iteration, we will use the equivalent erasure channel approximation (described in Sec. II-B2), and analyze the decoding after the first m transmissions as decoding of the mother code after a single transmission over the erasure channel with fixed error rate ν m given by [START_REF] Wu | The cdma2000 high rate packet data system[END_REF]. For this model, we need to ensure that ν m < ǫ * , that is, choose q im s.t. the following condition holds:

q im (1 -ǫ m ) > 1 -ǫ * - m-1 j=1 q ij (1 -ǫ j ) (4)
Note that this condition specifies only the minimum value that the product q im (1 -ǫ m ) should take in order to guarantee vanishing bit-erasure probability as the number of iterations grows. The redundancy increment q im has direct influence on throughput, but we need to know the actual probability of successful decoding to be able to study the delay of our scheme. We will address this problem by using the equivalent punctured code approximation of Sec. II-B2.

2) Rules Based on the Equivalent Punctured Code Scaling Approximation:

We first derive the block erasure rate P (m) B at transmission m. Such estimation is particularly interesting for short-length codes, down to several hundreds-one thousand bits. For punctured LDPC codes of length n, we know from [START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF] how to estimate P B quite accurately.

Recall from Sec. II-B2 that we model our IR-HARQ protocol through transmission m as transmission of the punctured mother code over a BEC with erasure rate ε m given by ( 3), where the bit corresponding to a variable node of degree i is punctured with probability p im . Let us denote this block erasure rate at transmission m by P (m) B . We are going to show that the constraint of keeping P (m) B below a certain value provides us a requirement on p im , and by ( 2), on q im . We use the following scaling approximation of [START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF] for P (m) B :

P (m) B ≃ Q √ n(ε * m -ε m -β m n -2/3 ) α m , (5)
where ε * m is the asymptotic iterative threshold, i.e., the (unique) solution of the density evolution equation

x = i λ i ν im [1 -ρ(1 -x)] i-1 , (6)
and α m and β m are parameters that explicitly depend on the mother LDPC code ensemble (i.e., λ and ρ), puncturing rates p im , and the threshold ε * m . Expressions for α m (scaling parameter) and β m (shift parameter) are given in in Appendix A and come from the results derived in [START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF].

If we ask for P (m) B < γ, where γ is a small positive constant, we have to have

ε * m -ε m -β m n -2/3 α m < Q -1 (γ) √ n . (7)
For simplicity, let us consider a particular case of punctured regular codes of type (x c-1 , x d-1 , p m ). Then α m and β m can be simply expressed through the scaling and shift parameters of the mother ensemble and the punctured probability p m (see [START_REF] Amraoui | Finitelength scaling for iteratively decoded LDPC ensembles[END_REF]); moreover, ε * m = p m + (1 -p m )ǫ * . Hence ( 7) becomes

(1 -p m )[(1 -p m )ǫ * + p m ] - m j=1 q j ǫ j < αQ -1 (γ) √ n + βn -2/3 .
Given that 1 -p m = m j=1 q j , we finally obtain that

q m (1 -ǫ m -q m (1 -ǫ * )) < αQ -1 (γ) √ n + βn -2/3 -Q m-1 , (8) where
Q m-1 = m-1 j=1 q j [1 -ǫ j + ( m-1 j=1 q j )(1 -ǫ * )].
Note that here the concentration of the block erasure rate of a code from the punctured ensemble around the average is assumed, while the literature only provides the concentration theorem for the bit erasure rate. However, for ǫ close to ǫ * , the number of erased bits after a decoding failure is linear in the codelength, and such a concentration may be assumed.

III. AVERAGE THROUGHPUT AND DELAY

The standard measure of ARQ protocol efficiency is throughput, defined as the average number of user data bits accepted at the receiving end in the time required for transmission of a single bit. We next derive the expected throughput our IR-HARQ scheme for regular codes. The results for irregular codes is obtained by replacing q m below by i λ i q im .

Let R be the rate of the code, ω m be the probability that it takes m transmissions for the decoding to be successful. The probability that one of the m ≤ M transmissions is successful is M m=1 ω m . Because our protocol is limited to M transmissions, if none of these transmissions is successful, the throughput is equal to 0. When one of the m ≤ M transmissions is successful, the number of user data bits communicated to the receiver is Rn. The number of the encoded bits sent to the receiver through the mth transmission is n m j=1 q j . So, the average throughput η is given by

η = R M m=1 ω m M m=1 ω m m j=1 q j
where ω m = P is given by [START_REF] Soljanin | Incremental redundancy hybrid ARQ with LDPC and Raptor codes[END_REF]. Note that the above expression for throughput becomes equal to its counterpart in [START_REF] Sesia | Incremental redundancy hybrid ARQ schemes based on Low-Density Parity-Check codes[END_REF] when q m = 1/M and when P (m) B is replaced by the probability that the asymptotic bit erasure rate P b at the transmission m goes to 0. It was proposed in [START_REF] Sesia | Incremental redundancy hybrid ARQ schemes based on Low-Density Parity-Check codes[END_REF] to compute P b through density evolution, i.e., P (m) ≈ Prob[P (m) b → 0]. Clearly, this quantity is a lower bound on the failure probability at transmission m, and hence, gives an upper bound on the average throughput and a lower bound on the average delay. Unfortunately, the bounds were shown to be too optimistic for finite-length codes for small and medium codelengths. This issue can be overcome by using the approximation for P (m) B which is more accurate. The second important parameter is the delay, which is the average number of bits needed to transmit in order to receive the useful information (user data bits). Similarly, the average delay τ of the IR-HARQ scheme can be shown to be equal to

τ = n M m=1 ω m m j=1 q j M m=1 ω m .

IV. EXAMPLES AND DISCUSSION

A. A Scheme Based on the (3, 6) Mother Ensemble

Let us check how tight our predictions are. Fig. 1 compares values of η versus the average channel erasure probability, obtained numerically and using our approximation. We used a (3, 6)-regular ensemble of length 1024. Note that for [START_REF] Costello | Applications of errorcontrol coding[END_REF][START_REF] Soljanin | Hybrid ARQ with random transmission assignments[END_REF] LDPC codes, ǫ * = 0.4293, α = 0.5603 and β = 0.616 [START_REF] Amraoui | Finitelength scaling for iteratively decoded LDPC ensembles[END_REF]. M been fixed to 5 (all 512 information bits are allocated to the first transmission and each following transmission contains 128 redundancy bits). We can see that the predicted curve for η and the simulated one are very close to each other. Let us use our approximation to study the effect of the codelength n and of the number of retransmissions M on η and τ . In Fig. 2, the average throughput versus average channel erasure probability is represented for different M and n. The taken ensemble is the (3, 6)-regular one, chosen codelengths -1024 and 8192. At each retransmission we send the M -th part of the codeword, M = 5; 15; 100. The capacity limit for the BEC is 1 -ǫ. One can see that the curve obtained for larger n is sharper, owing to the faster decrease of the block erasure rate in the waterfall region. Next, for increasing M , the curves approach the maximum throughput performance η max that can be obtained with given code ensemble; it is given by

η max (ǫ) = R 1 -ǫ * (1 -ǫ)
for ǫ ∈ [0, ǫ * ] and 0 otherwise. It is worth to note that approaching to η max by increasing M comes at the price of increasing the average delay (see

B. Discussion

In this paper we have considered IR-HARQ schemes based on finite-length LDPC codes and have defined the transmission rules as well as a very accurate estimation of its average throughput and delay. The aforementioned estimation is based on the average block erasure performance of punctured codes obtained through the scaling approximation [START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF]. The transmission was considered to take place over the BEC, but our results can be extended to other symmetric memoryless channels. Moreover, they can also be combined with [START_REF] Duc | Packet error rate and efficiency closed-form expressions for cross-layer hybrid arq schemes[END_REF], giving an approximation of the failure probability of data packets at the application layer. A natural way of extending the obtained result is optimization of parameters of the mother code and of the IR-HARQ scheme by obtaining the best tradeoff between η and τ . Further, the IR-HARQ scheme based on the optimized ensemble may be compared with schemes based on other codes, such as Raptor codes for instance. This point will be presented in our future work.

APPENDIX

To give the expression for the scaling parameter α m and the shift parameter β m , some more definitions of parameters of punctured LDPC codes are needed.

Definition 1: Let the variable node degree distribution from the node perspective be Λ(x) = i∈V Λ i x i-1 , for which Λ i represent the fraction of variable nodes of degree i, i ∈ V .

Definition 2: For given polynomial p m (x), let λ p (x) = i∈V p i λ i x i-1 and λp (x) = i∈V (1 -p i )λ i x i-1 . Note that that λ(x) = λ p (x) + λp (x). Similarly, let Λp (x) = i∈V (1 -p i )Λ i x i-1 . Also, let us introduce the following notation: y(x) = 1 -ρ(x), π(y) = ǫ λp (y) + λ p (y), ξ(x) = (π ′ (y))2 (ȳ)(ρ ′ (1) -ρ ′ (x)), µ(x) = π ′ (y)ρ ′ (x), where x = 1 -x and ȳ = 1 -y. Assume x * satisfies the equation ( 6) and y * = y(x * ), then the expression for α m and β m derived in [START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF] are: • l lp ml (1 -p ml )λ l+1 (y * ) l-1 π(y * )

As we can see, α m and β m only depend on η * m , x * and y * and on polynomials λ, ρ and p m . Moreover, they give a very accurate approximation as it is shown in [START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF].

Interestingly, for regular LDPC codes with parameters (x c-1 , x d-1 , p m ) 2 , α m and β m can be expressed through the scaling α and shift β parameters of the unpunctured ensemble (i.e. p m (x) = 0):

α m = α 1 -p m , β m = β 1 -p m . (11)

Fig. 1 .

 1 Fig. 1. Average throughput η versus equivalent channel erasure probability for (3, 6) LDPC codes of length 1024. M = 5. Dashed line -numerical result, straight line -our estimation.

Fig. 2 .

 2 Fig. 2.Throughput versus channel erasure probability for 5, 15 and 100 retransmissions using[START_REF] Costello | Applications of errorcontrol coding[END_REF][START_REF] Soljanin | Hybrid ARQ with random transmission assignments[END_REF]-regular LDPC codes. The dotted line represents the capacity limit; straight lines correspond to n = 1024; dashed lines -to n = 8192.

Fig. 3 Fig. 3 .

 33 Fig.3for illustration). In fact, τ = RM/η, and τ max = RM/η max = M (1 -ǫ * )/(1 -ǫ).

b 2 π

 2 * )ρ ′ (1 -x * )(1 -µ(x * )) λp (y * ) 2 • µ(x * ) * )x * ρ ′ (1 -x * ) • -λp (y * )µ ′ (x * ) = x * ρ ′ (1 -x * ) λ ′ (y * ) λ(y * ) y * -x * ρ ′ (1 -x * ) y * + (x * ρ ′ (1 -x * )) (y * ) π ′′ (y * ) + π ′ (y * ) y * -π(y * ) ′2 π(y * ) x * (1 -η * m )ρ ′ (x * ) y *2

Note that in this case the concentration of code performances around the average performance may be assumed, and it becomes sufficient to describe the performance of almost any code from the ensemble. If the code bits were punctured with probability q regardless of their degree, the concentration property would be lost[START_REF] Andriyanova | Waterfall region performance of punctured LDPC codes over the BEC[END_REF].

for this particular case, pm is a positive constant, 0 ≤ pm ≤ 1


G Bonfante
email: bonfante@loria.fr

J.-Y Marion

J.-Y Moyen
email: moyen@lipn.univ-paris13.fr

Quasi-interpretations a way to control resources

This paper presents in a reasoned way our works on resource analysis by quasiinterpretations. The controlled resources are typically the runtime, the runspace or the size of a result in a program execution.

Quasi-interpretations allow analyzing system complexity. A quasi-interpretation is a numerical assignment, which provides an upper bound on computed functions and which is compatible with the program operational semantics. Quasiinterpretation method offers several advantages: (i) It provides hints in order to optimize an execution, (ii) it gives resource certificates, and (iii) finding quasiinterpretations is decidable for a broad class which is relevant for feasible computations.

By combining the quasi-interpretation method with termination tools (here term orderings), we obtained several characterizations of complexity classes starting from Ptime and Pspace.

Introduction

This paper is part of a general investigation on program complexity analysis. We present the quasi-interpretation method which applies potentially to any formalism that can be reduced to transition systems. A quasi-interpretation gives a kind of measure by assigning to each symbol of a system a monotonic numerical function over R + . A quasi-interpretation possesses two main properties. First, the quasiinterpretation of a constructor term is a real which bounds its size. Second, a quasiinterpretation weakly decreases when a term is reduced.

From a practical point of view, the quasi-interpretation method is a tool to perform complexity analysis in a static way. Quasi-interpretations allow to establish an upper bound on the size of intermediate values which occur in a computation. This was used for a resource byte-code verifier in [START_REF] Amadio | A functional scenario for bytecode verification of resource bounds[END_REF]. Moreover in the context of mobile-code or of secured application, a resource certificate can be sent which consists in the (partial) proof of the fact that a program admits a quasi-interpretation.

We restrict our study to quasi-interpretations over R + which are bounded by some polynomials. A consequence of Tarski's Theorem [START_REF] Tarski | A Decision Method for Elementary Algebra and Geometry[END_REF] is that it is decidable whether or not a program admits a Max-Poly quasi-interpretation which are built by combining max operator of fixed arity and polynomials of bounded degrees. This leads to an automatic synthesis procedure of a meaningful class of quasi-interpretations.

From a theoretical point of view, we combine quasi-interpretations with termination tools. We focus on simplification orderings and we consider in particular Recursive Path Orderings introduced by Dershowitz [START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF]. It turns out that we characterize the class Ptime of functions computable in polynomial time [START_REF] Marion | Efficient first order functional program interpreter with time bound certifications[END_REF] and the class Pspace of functions computable in polynomial space [START_REF] Bonfante | On lexicographic termination ordering with space bound certifications[END_REF].

This work is related to Cobham [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF], Bellantoni and Cook [START_REF] Bellantoni | A new recursion-theoretic characterization of the poly-time functions[END_REF], Leivant [START_REF] Leivant | Predicative recurrence and computational complexity I: Word recurrence and poly-time[END_REF] and Leivant-Marion [START_REF] Leivant | Lambda calculus characterizations of poly-time[END_REF] ideas to delineate complexity classes. Note that most of the machine-independent characterizations of complexity classes have an extensional point of view. They study functions and do not pay too much attention to the algorithmic aspects. In this paper, we try an alternative way of looking at complexity classes by focusing on algorithms. In this long-term research program, the completeness problematic has moved and the nature of the problem has changed. Indeed, the class of algorithms (with respect to some encoding), say which run in polynomial time, is not recursively enumerable. So we cannot expect to characterize all Ptime algorithms. But we think that this question could shed light on the nature of computations and contribute to an intentional computability theory. Similar questions have been brought up by Caseiro [START_REF] Caseiro | Equations for defining Poly-Time[END_REF], Hofmann [START_REF] Hofmann | A type system for bounded space and functional in-place update[END_REF] and Jones [START_REF] Jones | LOGSPACE and PTIME characterized by programming languages[END_REF]. It is also worth mentioning the studies on intentionality of Colson, see for example [START_REF] Colson | Functions versus algorithms[END_REF], and of Moschovakis, as well as Gurevich.

Lastly, Marion and Péchoux suggest a new method, called sup-interpretation [START_REF] Marion | Resource analysis by sup-interpretation[END_REF], which is closely related to quasi-interpretations. Sup-interpretations allow to capture more algorithms, and to characterize small parallel complexity classes [START_REF] Bonfante | A characterization of alternating log time by first order functional programs[END_REF]. On the other hand, sup-interpretations do not have the nice properties of quasiinterpretations.

The paper organization is the following. The next Section introduces the first order functional programming language. The quasi-interpretations are defined next in Section 3. We suggest a classification of quasi-interpretations which induces a natural complexity hierarchy. Then, we study quasi-interpretation properties. Section 4 establishes that it is decidable if a program admits a quasi-interpretation with respect to a broad class of polynomially bounded assignments. Section 5 defines recursive path orderings used to prove termination of programs and some properties that we shall use later on. After these three sections, we state the main results at the beginning of Sections 6 and 7. Roughly speaking, the first result says that programs which terminate by product or lexicographic orderings are computable in polynomial-space. The second result means that programs that terminate by product ordering or that are tail recursive are computable in polynomial time. It is worth noticing that we have to compute the program by call by value semantics with a cache in order to have an exponential speed-up. The last Section 8 is devoted to simulations of both space and time bounded computations.

First order functional programming

Term rewriting systems underpin first order functional programming, that is why we refer to Dershowitz and Jouannaud survey [START_REF] Dershowitz | Handbook of Theoretical Computer Science[END_REF]. Throughout the following discussion, we consider three finite disjoint sets X , F , C of variables, function symbols and constructors.

Syntax of programs

Definition 1 The sets of terms and the rules are defined in the following way:

(Constructor terms) T (C) ∋ v ::= c | c(v 1 , • • • , v n ) (terms) T (C, F , X ) ∋ t ::= c | x | c(t 1 , • • • , t n ) | f(t 1 , • • • , t n ) (patterns) P ∋ p ::= c | x | c(p 1 , • • • , p n ) (rules) D ∋ d ::= f(p 1 , • • • , p n ) → t
where x ∈ X , f ∈ F , and c ∈ C. We shall use a type writer font for function symbols and a bold face font for constructors.

Definition 2 A program is a quadruplet f = X , C, F , E such that E is a finite set of D-rules.
Each variable in the right-hand side of a rule also appears in the left hand side of the same rule. We distinguish among F a main function symbol whose name is given by the program name f.

The set of rules induces a rewriting relation →. The relation * → is the reflexive and transitive closure of →. Throughout, we consider orthogonal programs which is a sufficient condition in order to be confluent. Following Huet [START_REF] Huet | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF], the program rules satisfy both conditions:

(i) Each rule f(p 1 , • • • , p n ) → t is left-linear, that is a variable appears only once in f(p 1 , • • • , p n ),
and (ii) there are no two left hand-sides which are overlapping. Lastly, a ground term is a term with no variables.

c ∈ C t i ↓ w i (Constructor) c(t 1 , • • • , t n ) ↓ c(w 1 , • • • , w n ) t i ↓ w i f(p 1 , • • • , p n ) → r ∈ E σ ∈ S p i σ = w i rσ ↓ w (Function) f(t 1 , • • • , t n ) ↓ w

Semantics

Orthogonal programs define a class of deterministic first order functional programs. The domain of the computed functions is the constructor term algebra T (C).

A substitution σ is a mapping from variables to terms. We say that it is a constructor substitution when the range of σ is T (C). We note S the set of these constructor substitutions.

We consider a call by value semantics which is displayed in Figure 1. The meaning of t ↓ w is that t evaluates to a constructor term w. The program f computes a partial function f :

T (C) n → T (C) defined as follows. For every v 1 , • • • , v n ∈ T (C), f (v 1 , • • • , v n ) = w iff f(v 1 , • • • , v n ) ↓ w. Otherwise, it is undefined and f (v 1 , • • • , v n ) = ⊥.
Notice that if t ↓ w then t * →w, because programs are confluent.

3 Quasi-interpretations

Quasi-interpretation definition

To approach the resource control problem, we suggest the concept of quasi-interpretation which plays the main role in this study. Quasi-interpretations have been introduced by Marion [START_REF] Marion | Complexité implicite des calculs, de la théorie à la pratique[END_REF][START_REF] Marion | Analysing the implicit complexity of programs[END_REF], Bonfante [START_REF] Bonfante | Constructions d'ordres, analyse de la complexité[END_REF], and Marion-Moyen [START_REF] Marion | Efficient first order functional program interpreter with time bound certifications[END_REF]. There are related to interpretation to prove termination, an in particular to [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF].

The fundamental property of a quasi-interpretation is that it is a numerical approximation from above of the size of each intermediate values (that is constructor terms), which appears in a reduction process. However, a quasi-interpretation does not give an upper bound on a term size which appears in a reduction process. A typical example is the lcs example in 6 whose reduction involved terms of exponential size, but the lcs program admits an additive quasi-interpretation, as we shall see later.

Let R + be the set of non-negative real numbers. An assignment -is a mapping from constructors and function symbols, that is C F , such that for each symbol f of arity n it yields (1) An non-negative real number c of R + , for every symbol c of arity 0.

(2) a n-ary function b : (R + ) n → R + for every symbol b of arity is n > 0.

Take a denumerable sequence X 1 , . . . , X n , . . . We extend an assignment -to terms canonically. Given a term t with n variables x 1 , . . . , x n , the assignment t denotes a function from (R + ) n to R + and is defined as follows:

x i = X i x i ∈ X b(t 1 , • • • , t n ) = b ( t 1 , • • • , t n )
An assignment satisfies the subterm property if for any i = 1, n and any

X 1 , • • • , X n in R + , we have b (X 1 , • • • , X n ) ≥ X i (1)
A direct consequence of the subterm property is that for any ground term s and any subterm t of s, s ≥ t .

An assignment is weakly monotone if for any symbol b, b is an increasing (not necessarily strictly) function with respect to each variable. That is, for every symbol b and for all

i = 1, n if X i ≥ Y i , we have b (X 1 , • • • , X n ) ≥ b (Y 1 , • • • , Y n ).
A substitution σ is defined over a term t, if the domain of σ contains all variables of t.

Given two terms t and u, we say that t ≥ u if for every constructor substitution σ defined over t and u, we have tσ ≥ uσ .

Definition 3 (Quasi-interpretation) A quasi-interpretation -of a program f is a weakly monotonic assignment satisfying the subterm property such that for each rule l → r l ≥ r

Throughout, when we shall write "quasi-interpretation", we always mean "quasiinterpretation of a program f = X , C, F , E ".

It is worth noticing that the inequalities that defines a quasi-interpretation are not strict which differs from the notion of interpretation used to prove termination.

= C[f(p 1 , • • • , p n )σ] and u 1 = C[tσ]. Since -is a quasi-interpretation, we have tσ ≤ f(p 1 , • • • , p n )σ .
The weak monotonicity property implies that

C[tσ] ≤ C[f(p 1 , • • • , p n )σ] .
We conclude by induction hypothesis. 2

Example 5 Given a list l of tally natural numbers, sort(l ) sorts the elements of l by insertion. The constructor set is C = {tt, ff, 0, suc, nil, cons}.

if tt then x else y → x if ff then x else y → y 0 < suc(y) → tt x < 0 → ff suc(x) < suc(y) → x < y insert(a, nil) → cons(a, nil) insert(a, cons(b, l)) → if a < b then cons(a, cons(b, l)) else cons(b, insert(a, l)) sort(nil) → nil sort(cons(a, l)) → insert(a, sort(l))
Constructors admit the following quasi-interpretation.

tt = ff = 0 = nil = 0 suc (X) = X + 1 cons (X, Y ) = X + Y + 1
And function symbols

if then else (X, Y, Z) = max(X, Y, Z) < (X, Y ) = max(X, Y ) insert (X, Y ) = X + Y + 1 sort (X) = X
This example illustrates two important facts. Quasi-interpretations can be maxfunctions like in the case of <. And, the quasi-interpretations of both sides of a rule can be the same. For example take the last rule. We see that sort(cons(a, l)) = A + L + 1 = insert(a, sort(l))

Example 6 Given two binary words u and v over the constructor set {a, b, ǫ}, lcs(u, v) returns the the length of the longest common subsequence of u and v.

The expression lcs(ababa, baaba) evaluates to suc 4 (0) because the length longest common subsequence is 4 (take baba).

max(n, 0) → n max(0, m) → m max(suc(n), suc(m)) → suc(max(n, m))
lcs(ǫ, y) → 0 lcs(x, ǫ) → 0 lcs(i(x), i(y)) → suc(lcs(x, y))

i ∈ {a, b} lcs(i(x), j(y)) → max(lcs(x, j(y)), lcs(i(x), y)) i = j, j ∈ {a, b}

It admits the following quasi-interpretation:

• ǫ = 0 = 0 • a (X) = b (X) = suc (X) = X + 1 • lcs (X, Y ) = max (X, Y ) = max(X, Y )

Taxonomy of Quasi-interpretations

Our aim is to study feasible computations. That is why we confine ourselves to programs admitting quasi-interpretations which are bounded by polynomials. We insist that assignments are bounded by polynomials, but are not necessarily polynomials.

Definition 7 An assignment -is polynomial if for each symbol b ∈ F C, b is a function bounded by a polynomial.

Next, we classify polynomial assignment according to the rate of growth of constructor assignments.

Definition 8 Let c be a constructor of arity n > 0.

• An assignment of c is additive (or of kind 0) if

c (X 1 , • • • , X n ) = n i=1 X i + α where α ≥ 1. • An assignment of c is affine (or of kind 1) if c (X 1 , • • • , X n ) = n i=1 β i X i + α α ≥ 1
where the β i 's are constants of R + and α > 1.

• An assignment c is multiplicative (or of kind 2) if c (X 1 , • • • , X n ) = Q(X 1 , • • • , X n ) + α α ≥ 1
where Q is a polynomial.

We classify polynomial assignments by the kind of assignments given to constructors, and not to function symbols. If each constructor assignment is additive (resp. affine, multiplicative) then the assignment is additive (resp. affine, multiplicative) assignment.

A program f admits an additive quasi-interpretation if it is an additive assignment. We shall also just say that f is additive, without explicitly mentioning the additive quasi-interpretation tied to it.

Similarly, A program f admits an affine (resp. a multiplicative) quasi-interpretation if it is an affine (resp. a multiplicative). We shall also just say that f is affine (resp. multiplicative).

In both previous examples, programs admit a polynomial quasi-interpretation because each quasi-interpretation is bounded by a polynomial. In example 5, the quasi interpretation of the function symbol < is not a polynomial. The insertion sort program admits an additive quasi-interpretation because each constructor (that is the symbol in {tt, ff, 0, suc, nil, cons}) admits an additive assignment. On the other hand, the assignment of the function symbol < is not additive but it is does not matter because it is not a constructor. For the same reason, the lcs example admits also an additive quasi-interpretation.

Example 9

We give three programs which illustrate the three kinds of program classes delineated by quasi-interpretations.

add(0, y) → y (2) add(suc(x), y) → suc(add(x, y)) (3) mult(0, y) → 0 (4) mult(suc(x), y) → add(y, mult(x, y)) (5)
These rules define the addition and the multiplication. They admit the following additive quasi-interpretation.

0 = 0 (6) suc (X) = X + 1 (7) add (X, Y ) = X + Y (8) mult (X, Y ) = X × Y (9)
So, addition and multiplication are additive programs (additivity only refers to the interpretation of constructors). Now, in order to define the exponential, we introduce another successor s which has an affine assignment.

exp(0) → suc(0) (10) exp(s(x)) → add(exp(x), exp(x)) (11)
The quasi-interpretations of the new symbols are:

s (X) = 2X + 1 (12) exp (X) = X + 1 ( 13
)
The above program which defines the exponential admits an affine quasi-interpretation.

We see that the domain of exp and its co-domain are not the same. Indeed, the domain is generated by {0, s} whose quasi-interpretation is affine and the co-domain is generated by {0, suc} whose quasi-interpretation is additive. We shall see later on that it is necessary to have two successors with different kinds of quasi-interpretations. Similar observations have be done in [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF] and on tiering system in which an argument of tier 1 produces an output of tier 0. We think that it is worth to investigate this analogy in order to interpret tiering concepts by quasi-interpretations.

We define the doubly-exponential function, i.e. n → 2 2 n , as follows (here we need yet another successor, s ′ ).

dexp(0) → suc(suc(0)) (14)
dexp(s ′ (x)) → mult(dexp(x), dexp(x)) (15)
and

s ′ (X) = (X + 2) 2 (16) dexp (X) = X + 2 (17)
Again we see that the domain and co-domain are not the same. The domain admits a multiplicative quasi-interpretation and the co-domain has an additive one.

Other classes of assignments could be introduced such as elementary or primitive recursive assignments, but we will not discuss about them in this paper. This type of extensions is related to Lescanne's paper [START_REF] Lescanne | Termination of rewrite systems by elementary interpretations[END_REF] about interpretation for termination proofs.

Elementary properties of assignments

We study now some quantitative properties of assignments when they are of the kind mentioned above. The size |t| of a term t is defined by

|t| =    0 if t is 0-ary symbol 1 + i=1,n |t i | if t = f(t 1 , . . . , t n )
Proposition 10 Assume that is an additive, an affine or a multiplicative assignment. For any constructor term t in T (C), we have |t| ≤ t .

PROOF. The proof goes by induction on the size of t. 2 Proposition 11 Assume that is an additive, an affine or a multiplicative quasiinterpretation of a program f. For any term u and any constructor term t ∈ T (C), if u * →t, we have |t| ≤ u .

PROOF. Proposition 4 implies that u ≥ t . Then from Proposition 10, we have

|t| ≤ t . So, |t| ≤ u . 2 Proposition 12
• If is an additive assignment, for any constructor term t in T (C),

we have t ≤ k × |t|. • If is an affine assignment, for any constructor term t in T (C), we have t ≤ 2 k×|t| . • If f is a multiplicative program, for any constructor term t in T (C), we have t ≤ 2 2 k×|t| .
where in each case k is a constant which depends on the assignment given to constructors.

PROOF. The proof goes by induction on the size of t. 2

It is worth noticing that the above Proposition illustrates a general phenomenon that we shall see all along this paper. Roughly speaking, the complexity increases by an exponential when we jump from additive to affine quasi-interpretations, or from affine to multiplicative ones.

Call-trees

We present now call-trees which are a tool that we shall use all along. A call-tree gives a static view of an execution which captures all function calls. Hence, we can study dependencies between function calls without taking care of the extra details provided by the underlying rewriting relation.

Take a program

f = X , C, F , E . A state of a program f is a tuple h, v 1 , • • • , v p
where h is a function symbol of F of arity p and v 1 , . . . , v p are constructor terms of T (C). Throughout, we may omit to mention the program f when the context is clear.

Assume that η

1 = h, v 1 , • • • , v p and η 2 = g, u 1 , • • • , u m are two states. A transition is a triplet η 1 e ; η 2 such that: (i) e is a rule h(q 1 , • • • , q p ) → t of E, (ii) there is a constructor substitution σ such that q i σ = v i for all 1 ≤ i ≤ p, (iii) there is a subterm g(s 1 , • • • , s m ) of t such that for any 1 ≤ i ≤ m, s i σ * →u i and u i ∈ T (C).
The reflexive transitive closure of ∪ e∈E e ; is * ;.

Proposition 13 Let -be a quasi-interpretation of a program f. Assume that h, v 1 , • • • , v p and g, u 1 , • • • , u m are two states such that h, v 1 , • • • , v p * ; g, u 1 , • • • , u m Then we have g(u 1 , • • • , u m ) ≤ h(v 1 , • • • , v p ) and also u i ≤ h(v 1 , • • • , v p ) for all 1 ≤ i ≤ m. PROOF. The hypothesis h, v 1 , • • • , v p * ; g, u 1 , • • • , u m means that there is a term t such that h(v 1 , • • • , v p ) * →t and that g(u 1 , • • • , u m ) is a subterm of t. Proposi- tion 4 states h(v 1 , • • • , v p ) ≥ t . Since a quasi-interpretation satisfies the subterm property, we have u i ≤ g(u 1 , • • • , u m ) ≤ h(v 1 , • • • , v p ) . 2
Next, we define the g, u 1 , • • • , u m -call tree as a tree where (i) g,

u 1 , • • • , u m is the root. (ii) the set of nodes is {η | h, v 1 , • • • , v p *
; η} and (iii) there is an edge between the state η 1 and the state η 2 if η 1 e ; η 2 . Some state may actually appear several time in the tree. This happen typically in two cases: when there is a loop in the computation or when there are two different sequences of call leading to the same one (such as with the Fibonacci function). We do not merge identical states in the call-tree, hence nodes are occurrences of a state rather that a state alone.

Keeping several occurrences of the same state is useful because here we need to mimic the call by value semantics of Figure 1. This semantics actually performs identical calls several times. In Section 7 identical nodes in a call tree will be merged and the tree will thus turn into a directed acyclic graph.

The size of a state g,

u 1 , • • • , u m is m i=1 |u i |.
Lemma 14 Let -be an additive (or affine, or multiplicative) quasi-interpretation of a program f. The size of each node of the f,

t 1 , • • • , t n -call graph is bounded by d × f(t 1 , • • • , t n )
where d is the maximal arity of a function symbol in f.

PROOF. Suppose that g, u 1 , • • • , u m is a state of the f, t 1 , • • • , t n -call graph. It follows from Proposition 13 that u i ≤ f(t 1 , • • • , t n ) . As each u i is a constructor term, Proposition 10 entails that |u i | ≤ u i . Therefore | g, u 1 , • • • , u m | = i=1,n |u i | ≤ d × f(t 1 , • • • , t n )
where d is the maximal arity of a function symbol. 2

Upper bound on the complexity

It turns out that we can now state a quite important practical point. Indeed, consider an additive program f. Then, the quasi-interpretation of f(t From this result, we can see that the halting problem on a given input is decidable, thus leading to a potential runtime detection of non-termination. In [START_REF] Amadio | Max-plus quasi-interpretations[END_REF], Amadio wrote a first proof of the result above.

Theorem 16 There is an evaluation procedure which, given an additive program f and given n constructor terms

t 1 , • • • , t n , computes the value w if f(t 1 , • • • , t n ) ↓
′ × d × f(t 1 , • • • , t n ) for some constant k ′ .
(Notice that here, we do not take into consideration the size of the stack.) Cook's theorem [START_REF] Cook | Characterizations of pushdown machines in terms of time-bounded computers[END_REF] implies that the call by value evaluator can be then simulated in time 2 K× f(t 1 ,••• ,tn) for some constant K (which depends on k ′ and d).

Since the program admits a polynomial quasi-interpretation, the time is bounded by 2 ), where K ′ and K ′′ are two constants.

Uniform Termination is undecidable

Quasi-interpretations do not ensure termination. Indeed, the rule f(x) → f(x) admits the quasi-interpretation f (X) = X but does not terminate. Moreover, quasiinterpretations do not give enough information to decide uniform termination as stated in the following theorem.

Theorem 18 It is undecidable to know whether a program which admits a polynomial quasi-interpretation, terminates or not on all inputs.

PROOF. Senizergues proved in [START_REF] Senizergues | Some undecidable termination problems for semi-thue systems[END_REF] that the uniform termination of non-increasing semi-Thue systems is undecidable. These semi-Thue systems are a particular case of rewriting systems with a quasi-interpretation (simply take the identity polynomial for the unary symbols and 1 for the unique constant ǫ) . The conclusion follows immediately. 2

Synthesis of Quasi-interpretations

We consider now the problem of finding program quasi-interpretations, which is an important practical question. For this, we restrict assignments to the class Max-Poly. The class of Max-Poly functions contains constant functions ranging over non-negative rationals and is closed by projections, maximum, addition, multiplication and composition.

We establish as a direct consequence of Tarski's Theorem [START_REF] Tarski | A Decision Method for Elementary Algebra and Geometry[END_REF] that finding a program quasi-interpretation, which belongs to the class Max-Poly over non-negative real numbers, is decidable, when degrees are fixed. Indeed, Tarski demonstrated that the first-order theory for reals containing the addition +, the multiplication ×, the equality =, the order > with variables over reals and rational constants is decidable.

On the other hand, the same question over natural numbers is undecidable because it is a consequence of Matiyasevich's Theorem [START_REF] Matiyasevich | Hilbert's 10th Problem[END_REF].

We consider two related problems. The first one is the verification problem:

inputs: A program f and an assignment -. problem: Is -a quasi-interpretation for f?

The second one is the synthesis problem:

input: A program f. problem: Is there an assignment -which is a quasi-interpretation for f?

Before proceeding to the main discussion, it is convenient to have a normal representation of function in Max-Poly.

Proposition 19 (Normalization) A Max-Poly function Q can always be expressed as:

Q(X 1 , . . . , X n ) = max(P 1 (X 1 , . . . , X n ), . . . , P k (X 1 , . . . , X n ))
where each P i is a polynomial. We say that the max-degree of Q is k and the degree of Q is the maximum degree of the polynomials P 1 , . . . , P k .

PROOF. This is due to the fact that max is distributive with + and × over the non-negative reals. 2

Now consider a Max-Poly assignment -of a program f. Take a rule l → r and define

S l→r = ∀X 1 , . . . X p ≥ 0 : i=1..n j=1..m P i (X 1 , . . . , X p ) ≥ Q j (X 1 , . . . , X p )
where l = max(P 1 , . . . , P n ), r = max(Q 1 , . . . , Q m ) and X 1 , . . . , X p are all the variables of l . (Recall that the variables of r are also variables of l .)

We see that the first order formula S l→r is true iff l ≥ r .

Theorem 20

The verification problem for Max-Poly assignments is decidable in exponential time in the size of the program.

PROOF.

In order to solve the verification problem, we have to decide whether or not the following first order formula is true.

S E = l→r∈E
S l→r for a given assignment This is performed by Tarski's decision procedure. Basu, Pollack and Roy [START_REF] Basu | On the combinatorial and algebraic complexity of quantifier elimination[END_REF] established that such procedure is at most exponential in the number of quantifiers. In our case, it corresponds to the maximum arity of symbols. 2

Theorem 21

The synthesis problem for Max-Poly assignment of bounded degree and bounded max-degree is decidable in doubly exponential time in the size of the program.

PROOF. Without loss of generality, we restrict ourselves to unary functions. Functions with many variables are handled in the same way but with more coefficients and indexes. By Theorem hypothesis, we assume that the degree is d and the max-degree is k.

Suppose that there are n symbols, constructors or functions, b 1 , . . . , b n . The assignment of b i is of the form

b i (X) = max(P b i 1 (X), . . . , P b i k (X))
where where S E is defined in the previous proof. Lastly, we need to verify that the subterm and the weak monotonicity properties and the fact that the coefficient of degree 0 for constructors is ≥ 1.

P b i m = d j=0 a b i ,m,j X j
The total number of quantifiers is k × (d + 1) × n. So, the decision procedure is doubly exponential in the size of the program. 2

Remark 22

The quasi interpretations of all examples belong to the class Max-Poly.

Actually, it appears that the class of Max-Poly quasi-interpretations is sufficient for daily programs. In practice, each program appears to admit a Max-Poly quasiinterpretation with low degrees, usually no more than 2 for both the degree of polynomials and the arity of max.

Although a solution of the decision of Max-Poly synthesis problem is presented above, yet the procedure for carrying out the decision is complex. There is need of specific methods for finding quasi-interpretations which are in a smaller class but which are relevant. For this reason, Amadio [START_REF] Amadio | Max-plus quasi-interpretations[END_REF] considered the max-plus algebra over rational numbers. A program which admits a quasi-interpretation over the maxplus algebra are related to non-size increasing according to Hofmann [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF]. Amadio established that the synthesis of max-plus quasi-interpretation is in NPtime-hard and NPtime-complete in the case of multi-linear assignments.

Termination

We now focus on termination which plays the role of a mold capturing certain algorithm patterns. We obtain a finer control resource by the combination of termination tools and quasi-interpretations. Here, we consider Recursive Path Orderings which are simplification orderings and so well-founded. Among the pioneers of this subject, there are Plaisted [START_REF] Plaisted | A recursively defined ordering for proving termination of term rewriting systems[END_REF], Dershowitz [START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF], Kamin and Lévy [START_REF] Kamin | Attempts for generalising the recursive path orderings[END_REF]. Finally, Krishnamoorthy and Narendran in [START_REF] Krishnamoorthy | On recursive path ordering[END_REF] have proved that deciding whether a program terminates by Recursive Path Orderings is a NP-complete problem.

Extension of an ordering to sequences

Suppose that is a partial ordering and ≺ its strict part. We describe two extensions of ≺ to sequences of the same length.

Definition 23

The product extension1 of ≺ over sequences, noted ≺ p , is defined as follows.

We have

(m 1 , • • • , m k ) ≺ p (n 1 , • • • , n k ) if and only if (i) ∀i ≤ p, m i n i and (ii) ∃j ≤ k such that m j ≺ n j .

Definition 24

The lexicographic extension of ≺, noted ≺ l , is defined as follows.

We have

(m 1 , • • • , m k ) ≺ l (n 1 , • • • , n k ) if
and only if there exists an index j such that (i) ∀i < j, m i n i and (ii) m j ≺ n j .

The product ordering of sequences in a restriction of the more usual multi-set ordering of sequences. We do not need here the full power of the multi-set ordering mainly because we only compare sequences of the same length will the multi-set ordering works on sequences of any length.

Notice that the product ordering of sequences is also a restriction of the lexicographic ordering, that is two sequences ordered by the product extension are also ordered lexicographically.

Recursive path ordering with status

Let ≺ F be an ordering on F and ≈ F be a compatible equivalence relation such that if f ≈ F g then f and g have the same arity. The quasi-ordering

F =≺ F ∪ ≈ F is a precedence over F . u = t i or u ≺ rpo t i f ∈ F C u ≺ rpo f(. . . , t i , . . .) ∀i u i ≺ rpo f(t 1 , • • • , t n ) f ∈ F , c ∈ C c(u 1 , • • • , u m ) ≺ rpo f(t 1 , • • • , t n ) ∀i u i ≺ rpo f(t 1 , • • • , t n ) g ≺ F f f, g ∈ F g(u 1 , • • • , u m ) ≺ rpo f(t 1 , • • • , t n ) (u 1 , • • • , u n ) ≺ st(f) rpo (t 1 , • • • , t n ) f ≈ F g ∀i u i ≺ rpo f(t 1 , • • • , t n ) f, g ∈ F g(u 1 , • • • , u n ) ≺ rpo f(t 1 , • • • , t n ) Fig. 2

. Definition of ≺ rpo

Definition 25 A status st is a mapping which associates to each function symbol f of F a status st(f) in {p, l}. A status is compatible with a precedence F if it satisfies the fact that if f ≈ F g then st(f) = st(g).

Throughout, we assume that status are compatible with precedences.

Definition 26 Given a precedence F and a status st, the recursive path ordering ≺ rpo is defined in Figure 2.

When st(f) = p, the status of f is said to be product. In that case, the arguments are compared with the product extension of ≺ rpo . Otherwise, the status is said to be lexicographic.

A program is ordered by ≺ rpo if there is a precedence on F and a status st such that for each rule is decreasing, that is each rule l → r, we have r ≺ rpo l.

Theorem 27 (Dershowitz [START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF]) Each program which is ordered by ≺ rpo terminates on all inputs.

Example 28

(1) The shuffle program rearranges two words. It terminates with a product status. shuffle(ǫ, y) → y shuffle(x, ǫ) → x shuffle(i(x), j(y)) → i(j(shuffle(x, y)))

i, j ∈ {0, 1}

The following program reverses a word by tail-recursion. It terminates with a lexicographic status.

reverse(ǫ, y) → y reverse(i(x), y) → reverse(x, i(y))

i ∈ {0, 1}

(3) The program sort of Example 5 terminates if each function symbol has a product status and by setting the precedence if then else ≺ F insert ≺ F sort (4) The lcs program of Example 6 is ordered by taking max ≺ F lcs, and both symbols have a product status.

Extensional Characterization

The orderings considered are special cases of more general ones and in particular of Multiset Path Ordering and Lexicographic Path Ordering. Nevertheless, they characterize the same set of functions. Say that a RPO Pro -program is a program in which each function symbol has a product status. Following the result of Hofbauer [START_REF] Hofbauer | Termination proofs with multiset path orderings imply primitive recursive derivation lengths[END_REF], we have2

Theorem 29 The set of functions computed by RPO Pro -programs is exactly the set of primitive recursive functions.

Now, say that a RPO Lex -program is a program in which each function symbol has a lexicographic status. Weiermann [START_REF] Weiermann | Termination proofs by lexicographic path orderings yield multiply recursive derivation lengths[END_REF] has established that3

Theorem 30 The set of functions computed by RPO Lex -programs is exactly the set of multiple-recursive functions.

Consequences of termination proofs

We write u t to say that u is a subterm of t.

Proposition 31

(1) For each constructor term t and u, u ≺ rpo t iff u ⊳ t.

(2) For each constructor term

u 1 , • • • , u n and t 1 , • • • , t n , (u 1 , • • • , u n ) ≺ x rpo (t 1 , • • • , t n ) implies (u 1 , • • • , u n ) ⊳ x (t 1 , • • • , t n ),
where x is a status p or l and ⊳ x is the corresponding extension based on the subterm relation.

(3) For each constructor term u

1 , • • • , u n and t 1 , • • • , t n , (u 1 , • • • , u n ) ≺ x rpo (t 1 , • • • , t n ) implies (|u 1 |, • • • , |u n |) < x (|t 1 |, • • • , |t n |)
, where x is a status p or l and < x is the corresponding extension of the ordering over natural numbers.

PROOF. The proofs go by induction on the size of terms. 2

Remark 32

The ordering ≺ rpo is not stable for constructor contexts. Indeed, we have 1(ǫ) ≺ rpo 0(1(ǫ)), but 1(1(ǫ)) ≺ rpo 1(0(1(ǫ))) does not hold. So, ≺ rpo is not a reduction ordering but there is no rewriting inside constructor terms.

Lemma 33 Let f be a program which is ordered by ≺ rpo , α be the number of function symbols and d be the maximal arity of function symbols. Assume that the size of each state of the f, t 1 , • • • , t n -call tree is strictly bounded by A. Then the following facts hold:

(1) If f, t 1 , • • • , t n * ; g, u 1 , • • • , u m then (a) g ≺ F f or (b) g ≈ F f and (u 1 , • • • , u m ) ≺ st(f) rpo (t 1 , • • • , t n ). (2) If f, t 1 , • • • , t n * ; g, u 1 , • • • , u m and g ≈ F f then the number of states be- tween the states f, t 1 , • • • , t n and g, u 1 , • • • , u m is bounded by A d .
(3) The length of each branch of the call-tree is bounded by α × A d .

PROOF.

(1) Because the rules of the program decrease by

≺ rpo . (2) Suppose that h, v 1 , • • • , v p is a state between f, t 1 , • • • , t n and g, u 1 , • • • , u m .
Due to the first point of this lemma, we have h

≈ F f and (v 1 , • • • , v p ) ≺ st(f) rpo (t 1 , • • • , t n ). So, by proposition 31(3), we have (|v 1 |, • • • , |v p |) < st(f) (|t 1 |, • • • , |t n |). Since the
not(tt) → ff not(ff) → tt or(tt, x) → tt or(ff, x) → x 0 = 0 → tt suc(x) = 0 → ff 0 = suc(y) → ff suc(x) = suc(y) → x = y in(x, nil) → ff in(x, cons(a, l)) → or(x = a, in(x, l))
verify(Var(x), t) → in(x, t) verify(Not(φ), t) → not(verify(φ, t)) verify(Or(φ 1 , φ 2 ), t) → or(verify(φ 1 , t), verify(φ 2 , t)) verify(Exists(n, φ), t) → or(verify(φ, cons(n, t)), verify(φ, t))

qbf(φ) → verify(φ, nil)
Booleans are encoded by {tt, ff}, variables are encoded by unary integers which are generated by {0, suc}. Formulae are built from {Var, Not, Or, Exists}. All these symbols are constructors. The main function symbol is qbf.

Rules are ordered by ≺ rpo by putting

{not, or, = } ≺ F in ≺ F verify ≺ F qbf
and each function symbol has a product status except verify which has a lexicographic status.

They admit the following additive quasi-interpretations :

c = 0 where c is a constructor of arity 0 c (X 1 , • • • , X n ) = 1 + n i=1 X i
where c is a constructor of arity > 0

verify (Φ, T ) = Φ + T qbf (Φ) = Φ + 1 g (X 1 , • • • , X n ) = n max i=1 X i
for other function symbols 6.2 RPO QI -programs are Pspace computable

We are now establishing that a RPO QI -program f is computable in polynomial space.

Lemma 37 Let f be a RPO QI -program. For each constructor term t 1 , • • • , t n , the space used by a call by value interpreter to compute

f(t 1 , • • • , t n ) is bounded by a polynomial in f(t 1 , • • • , t n ) .
PROOF. Take an innermost call by value interpreter, like the one of Figure 1. It builds recursively in a depth first manner the f, t 1 , • • • , t n -call tree, evaluates nodes and backtracks. Put

A = f(t 1 , • • • , t n ) .
The interpreter only needs to store states along a branch of the call-tree. Each state as well as the intermediate results are bounded by O(A). The maximal length of a branch is bounded by α × A d by Lemma 33 [START_REF] Andersen | Generalizing Cook's transformation to imperative stack programs[END_REF]. The number of states and results to memorize for the depth first search is bounded by α × A d+1 × β where β is the maximal size of a rule. In other words, β is an upper bound on the width of the call-tree. Therefore, the space used by the interpreter is bounded by O(A d+1 ). 2

Theorem 38 Let f be an additive RPO QI -program. For each constructor term t 1 , • • • , t n , the space used by a call by value interpreter to compute

f(t 1 , • • • , t n ) is bounded by a polynomial in max n i=1 |t i |.
PROOF. By Proposition 12, we have

t i ≤ O(|t i |). Because quasi-interpretations are polynomially bounded, we have f(t 1 , • • • , t n ) ≤ P (max n i=1 |t i |)
, for some polynomial P . So the space is bounded by O(P (max n i=1 |t i |) d+1 ) following Lemma 37. 2

Beyond polynomial space

The kind of constructor quasi-interpretations provides an upper bound on the space required to evaluate a program.

The upper-bound on time-usage is established by Theorem 47 below. The completeness of this characterization is established by Theorem 54.

Example 43

The lcs example 6 is quite interesting and is an illustration of an important observation. Indeed, if one applies the rules of the program following a call by value strategy, one gets an exponentially long derivation chain. But the theorem states that the lcs function is computable in polynomial time. Actually, one should be careful not to confuse the algorithm and the function it computes. This function (length of the longest common subsequence) is a classical textbook example of so called "dynamic programming" (see chapter 16 of [START_REF] Cormen | Introduction to Algorithms[END_REF]) and can in this way be computed in polynomial time.

So, the theorem does not characterize the complexity of the algorithm, which we should call its explicit complexity but the complexity of the function computed by this algorithm, which we should dub its implicit complexity.

7.2 RPO QI Pro+Lin -programs are Ptime computable

In order to avoid an exponential explosion like, for instance, in the lcs case, we switch from the call-by-value semantics previously defined to a call-by-value semantics with cache, see Figure 4. Hence, we simulate dynamic programming techniques, which consist in storing each result of a function call in a table and avoiding to recompute the same function call if it is already in the table. This technique is inspired from Andersen and Jones' rereading ( [START_REF] Andersen | Generalizing Cook's transformation to imperative stack programs[END_REF]) of Cook simulation technique over 2 way push-down automata ( [START_REF] Cook | Characterizations of pushdown machines in terms of time-bounded computers[END_REF]) and is called memoization.

The expression C, t ⇓ C ′ , w means that the computation of t is w given a program f and an initial cache C. The final cache C ′ contains C and each call which has been necessary to complete the computation.

More precisely, say that a configuration is a list such as (g, w Fig. 3. The lcs, ababa, baaba -call tree with memoization.

(Constructor) Figure 3 shows what happens to the lcs, ababa, baaba -call tree when memoization is applied. Notice that identical subtrees are merged and the call-tree becomes a directed acyclic graph.

c ∈ C C i-1 , t i ⇓ C i , w i C 0 , c(t 1 , • • • , t n ) ⇓ C n , c(w 1 , • • • , w n ) (Read) C i-1 , t i ⇓ C i , w i (f, w 1 , • • • , w n , w) ∈ C n C 0 , f(t 1 , • • • , t n ) ⇓ C n , w (Update) C i-1 , t i ⇓ C i , w i f(p 1 , • • • , p n ) → r ∈ E σ ∈ S p i σ = w i C n , rσ ⇓ C, w C 0 , f(t 1 , • • • , t n ) ⇓ C ∪ (f, w 1 , • • • , w n , w), w
The key point for additive programs, is to establish that the size of a cache C is polynomially bounded in the size of the input arguments.

Lemma 44 Suppose that C 0 , f(t 1 , • • • , t n ) ⇓ C, w . The size of the final cache C is bounded by a polynomial in f(t 1 , • • • , t n ) .
PROOF. Define C g as the set of m-uplets of T (C)-terms which are the arguments of states of g. That is, (u

1 , • • • , u m ) ∈ C g iff (g, u 1 , • • • , u m , v) ∈ C. We have #C = g∈F #C g (18)
where we write #S for the cardinal of a set S.

To give an upper-bound on the cardinality of C g , we define two sets C ∨ g and C ∧ g . The idea is to separate the calls which come from functions of strictly higher precedence and the ones which come from functions of the same precedence. Consider the f, v 1 , • • • , v n -call tree. Say that the covering graph of g is the subgraph of the f, v 1 , • • • , v n -call tree obtained by removing all states which are not labeled by functions h which has precedence equivalent to g, that h ≈ F g. Define two sets C ∨ g and C ∧ g as follows. C ∨ g contains all the roots of the covering graph of g labeled by g, and C ∧ g contains all the other nodes of the covering graph labeled by g.

• We consider the C ∨ g 's. Suppose that f ≈ F g, but f = g. For the special case where g ≈ F f, we have #C ∨ f = 1. By definition, we have #C ∨ g = 0. Suppose that g ≺ F f. Then, (u

1 , • • • , u m ) ∈ C ∨ g . It follows that the cardinality of C ∨ g is bounded by #C ∨ g ≤ g≺ F f #C f (19)
• We consider C ∧ g . ( 1) The status of g is product. Proposition 31 states that sub-calls of the same rank starting from

f(v 1 , • • • , v n ) have
(|v i | + 1) ≤ (d × f(t 1 , • • • , t n ) ) d ( 20
)
where d is the maximal arity of a function symbol. (2) The status of g is lexicographic. But by definition of RPO QI Lin -programs, there is at most one recursive call starting from g for each rule application. Lemma 33 [START_REF] Andersen | Generalizing Cook's transformation to imperative stack programs[END_REF] entails that the maximal length of a branch is f(t 1 , • • • , t n ) d which is also a bound on the number of successive calls initiated by f.

From both previous points, we obtain that

#C ∧ g ≤ (#C ∨ g + 1) × d d × f(t 1 , • • • , t n ) d (21)
Finally, we have

#C g ≤ #C ∨ g + #C ∧ g (22)
By combining ( 18), ( 19), [START_REF] Huet | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF], and ( 22), we see that the cardinality of C is polynomially bounded in

f(t 1 , • • • , t n ) . 2
Example 45 Figures 5 and6 show the covering graphs of lcs and max in the lcs, ababa, baaba -call tree. Nodes in C ∨ g have been squared while nodes of C ∧ g have been circled (g ∈ {lcs, max}).

Lemma 46 Let f be a RPO QI Pro+Lin -program. For each constructor term t 1 , • • • , t n , the runtime of the call by value interpreter with cache to compute

f(t 1 , • • • , t n ) is bounded by a polynomial in f(t 1 , • • • , t n ) .
PROOF. Since an evaluation procedure memorizes all necessary configurations, the runtime is at most quadratic in the size of the cache. Note that the exact runtime depends on the implementation strategy and in particular on the cache management. In the general case, memoization is not used because one cannot decide which results will be reused and the cache may become too big to be really useful. In our particular case, the termination ordering gives enough information on the structure of the program to minimize the cache [START_REF] Marion | Complexité implicite des calculs, de la théorie à la pratique[END_REF].

We Fig. 6. The max-covering graph of the call-tree.

of the states below N-states are useless in order to determine f, t 1 , • • • , t n . And, we can forget them. Therefore, it is sufficient to store in a cache a separation set N for each function symbol. Now say that a separation set N is minimal if for each state s ∈ N, N \ {s} is not a separation set. We can require an implementation to keep a minimal separation set. To perform dynamically, we have to compare configurations in the cache. Take two configurations (f,

t 1 , • • • , t n , t) and (g, u 1 , • • • , u m , u). If f(t 1 , • • • , t n ) ≺ rpo g(u 1 , • • • , u m ) then
= i(π), s ′ )], [Pred(π = p(π), s ′ )], [Branch(π, s ′ , s ′′ )], [Fork min (s ′ , s ′′ )], [Fork max (s ′ , s ′′ )], [End].
A configuration of a PRM M is given by a pair (s, F ) where s ∈ S and F is a function Π → W which stores register values. We note {π ← π ′ }F to mean that the value of the register π is the content of π ′ , the other registers stay unchanged.

In order to have a choice mechanism to simulate alternation by the fork operation, we define an ordering ◭ on W : ǫ ◭ y, 0(x) ◭ 1(y), i(x) ◭ i(y) if and only if x ◭ y. We define the operations min ◭ and max ◭ wrt ◭.

Next, we define a semantic partial-function eval : N × S × W m → W, that maps the result of the machine in a time bound given by the first argument.

• eval(0, s, F ) is undefined.

• If com(s) is Succ(π = i(π), s ′ ) eval(t + 1, s, F ) = eval(t, s ′ , {π ← i(π)}F ). • If com(s) is Pred(π = p(π), s ′ )], then eval(t+1, s, F ) = eval(t, s ′ , {π ← p(π)}F )
where p is the predecessor function on W; where F 0 (π i ) = w i for i = 1..k and otherwise F 0 (π j ) = ǫ.

• If com(s) is Branch(π, s ′ , s ′′ ) then eval(t + 1, s, F ) = eval(t, r, F ), where r = s ′ if π = 0(w) and r = s ′′ if π = 1(w); • If com(s) is Fork min (s ′ , s ′′ ) then eval(t + 1, s, F ) = min ◭ (eval(t, s ′ , F ), eval(t, s ′′ , F )); • If com(s) is Fork max (s ′ , s ′′ ) then eval(t + 1, s, F ) = max ◭ (eval(t, s ′ , F ), eval(t, s ′′ , F )); • If com(s) is End then eval(t + 1, s, F ) = F (output).

Space and Time bounded computation

A Register machines (RM) is a PRM without fork commands. A Turing machine can be simulated linearly in time by a RM.

Proposition 49 A function φ is computable in polynomial (respectively exponential, doubly exponential) time iff φ is RM-computable in polynomial time (resp. exponential, doubly exponential).

There are pleasingly well-known tight connections between space used by a Turing machine and time used by PRM. The essence of the translation comes from the work of Savitch [START_REF] Savitch | Relationship between nondeterministic and deterministic tape classes[END_REF] and Chandra, Kozen, Stockmeyer [START_REF] Chandra | [END_REF].

Theorem 50 A function φ is computable in polynomial (resp. exponential, doubly exponential) space iff φ is PRM-computable in polynomial time (resp. exponential, doubly exponential). Now, it remains to compute the clock, that is the length of the iteration of the main loop of the simulation in order to complete the simulation.

Simulation of Polynomial computations

Proposition 53 Any polynomial is computed by an additive RPO QI Lin -programs (resp. RPO QI Pro -programs).

PROOF. We define any polynomial by composition from the additive programs for the addition add and the multiplication mult.

add(⋄, y) → y add(s(x), y) → s(add(x, y)) mult(⋄, y) → ⋄ mult(s(x), y) → add(y, mult(x, y))

The programs add and mult admits the following quasi-interpretations add (X, Y ) = X + Y mult (X, Y ) = X × Y where constructors have the quasi-interpretation ⋄ = 0 s (X) = X + 1

The programs add and mult terminates by ≺ rpo by putting add ≺ F mult with a product status. So, any polynomial is a RPO QI Pro -program. On the other hand, add and mult are linear and thus any polynomial is a also RPO QI Lin -program. 2 PROOF. Let φ be a function which is computed by a RM in time bounded by a polynomial P .

For the first case, the time bound P is computed by an additive RPO QI Lin -program following Proposition 53. We compose with Lemma 51, we conclude that φ is computed by an additive RPO QI Lin -program.

For the second case, the time bound P is also an additive RPO QI Pro -program following Proposition 53. We compose with Lemma 52, we conclude that φ is computed by an additive RPO QI Pro -program.

The last case is an immediate consequence of the previous constructions. We have exp γ (n) = m where n = (s ′ ) n (⋄) and m = (s) 2 γn (⋄).

Constructors have the following quasi-interpretation ⋄ = 0 s (X) = X + 1 s ′ (X) = 2 γ X + 2 γ -1 s (X) = 2X + 1 And this program admits the following quasi-interpretations PROOF. The function λn.2 2 γn is computed by dmk γ (⋄) → ⋄ dmk γ (s ′′ (x)) → s′′ (. . . (s ′′ (dmk γ (x))) . . .) γ times square(x) → mult(x, x) mult is defined in Prop 53 dexp(⋄) → s(s(⋄)) dexp(s ′′ (x)) → square(dexp(x)) dexp γ (x) → dexp(dmk γ (x))

mk k (X) = X d (X) = 2X exp (X) = X + 1 exp γ (X) = X +
We have dexp γ (n) = m where n = (s ′′ ) n (⋄) and m = (s) 2 2 γn (⋄).

Constructors have the following quasi-interpretation ⋄ = 0 s (X) = X + 1 s ′′ (X) = θ γ (X) s′′ (X) = (X + 2) 2 where θ 0 (X) = X θ k+1 (X) = (θ k (X) + 2) 2 0 ≤ k < γ

Fig. 1 .

 1 Fig. 1. Call by value semantics with respect to a program X , C, F, E .

Now, we have

  to guess polynomial coefficients by proving the validity of the formula: ∃a b 1 ,1,0 . . . a b 1 ,k,d , . . . , a bn,1,0 , . . . , a bn,k,d : S E

Fig. 4 .

 4 Fig. 4. Call-by-value interpreter with Cache of X , C, F, E .g, w 1 , • • • , w m is a state, and g (w 1 , • • • , w m ) = w. When a term g(w 1 , • • • , w m ) is considered, we search for a configuration (g, w 1 , • • • , w m , w) in the current cache C.If such configuration exists, we use it to short-cut the computation and so we return w. Otherwise, we a program equation, say l → r, by matching g(w 1 , • • • , w m ) with l. Then, we update C by adding the configuration (g, w 1 , • • • , w m , w) to the current cache C.

  Proofs are very similar to the one of Theorem 47. The kind of quasi-interpretation gives the different upper-bounds on the time-usage as established in Proposition 12. The converse is again a consequence of Theorems 57 and 60. 8 Simulation of Parallel Register Machines 8.1 Parallel Register Machines Following [27], we introduce Parallel Register Machines (PRM) which are able to model the essential features of both traditional sequential computing like Turing Machines and alternating computations like Alternating Turing Machines. A PRM M works over the word algebra W generated by the constructors {0, 1, ǫ} and consists in (1) a finite set S = {s 0 , s 1 , . . . , s k } of states, including a distinct state begin. (2) a finite list Π = {π 1 , . . . , π m } of registers; we write output for π m ; Registers will only store values in W; (3) a function com mapping states to commands which are [Succ(π

  Let T : N → N be a function. A function φ :W k → W is PRM-computable in time T if there is a PRM M such that for each (w 1 , • • • , w k ) ∈ W k , we have eval(T ( k max i=1 |w i |), begin, F 0 ) = φ(w 1 , • • • , w k )

Theorem 54 •

 54 A polynomial time function is computed by an additive RPO QI Lin -program. • A polynomial time function is computed by an additive RPO QI Pro -program. • A polynomial time function is computed by an additive RPO QI Pro+Lin -program.

  The proof goes by induction on the derivation length n. For this, suppose that u = u 0 → . . . → u n = v. If n = 0 then the result is immediate. Otherwise n > 0 and in this case, there is a rule f(p 1 , • • • , p n ) → t and a constructor substitution σ such that u 0

	Proposition 4 Assume that -is a quasi-interpretation of a program f. For any ground terms u and v such that u

* →v, we have u ≥ v PROOF. A context is a particular term that we write C[⋄] where ⋄ is a new variable. The substitution of ⋄ in C[⋄] by a term t is noted C[t].

  1 , • • • , t n ) is bounded by a polynomial in the input size, that is in i=1,n (|t i |). Next, by combining Lemma 14, we deduce that the size of each state of the f, t 1 , • • • , t n -call tree is bounded by a polynomial in the input size. Because, the size of each state is bounded by the quasi-interpretation of the root. If f is an affine program, the size of each state of the f, t 1 , • • • , t n -call tree is bounded by 2 k×m where k is some constant. • If f is a multiplicative program, the size of each state of the f, t 1 , • • • , t n -call tree is bounded by 2 2 k×m where k is some constant.

Theorem 15 Assume that f is a program. For any constructor terms t 1 , . . . , t n , • If f is an additive program, the size of each state of the f, t 1 , • • • , t n -call tree is bounded by P (m) where P is some polynomial. • where m = max i=1,n |t i |. PROOF. It is a consequence of Lemma 14 and Proposition 12. 2

  w and otherwise returns ⊥, that is if the evaluation does not terminate. This evaluation procedure runs in exponential time, i.e. in 2 P (max n i=1 |t i |) , where P is a polynomial. And the width is bounded by te maximal arity d of a function symbol. So, the space use on the space is bounded by k

PROOF. We build a call by value evaluator with a deterministic Turing machine with an extra tape which behaves as a stack in order to evaluate f(t 1 , • • • , t n ). The stack is used for the recursive calls and the normal tapes contain the current context. Actually, a call by value procedure computes the value of each state of f, t 1 , • • • , t ncall graph and for this we perform breadth-first exploration. A context corresponds to a state and the number of states that we have to memorize is bounded by the width of the call-graph.

  P (max n i=1 |t i |) , where P (X) = K × f (kX, . . . , kX) by Proposition 12. 2 Corollary 17 There is an evaluation procedure which given an affine (resp. multiplicative) program f and n constructor terms t 1 , • • • , t n , computes the value w if t ↓ w and otherwise returns ⊥ in double exponential time, i.e. in 2 2 K ′ ×max n

	triple exponential time, i.e. in 2 2 2 K ′′ ×max n i=1	|t i |	i=1	|t i | (resp. in

  size of each component is bounded by A and n ≤ d, the length of the decreasing chain is bounded by A d . (3) In each branch, the previous point of the Lemma claims that there are at most A d states whose function symbols have the same precedence. Next, there are A d states whose function symbols have the precedence immediately below, and so on. As there are only α function symbols, the length of the branch is bounded by α × A d . Theorem 35 The set of functions computed by additive RPO QI -programs is exactly the set of functions computable in polynomial space. The upper-bound on space-usage is established by Theorem 38. The completeness of this characterization is established by Theorem 55. Example 36 The Quantified Boolean Formula (QBF) problem is Pspace complete. It consists in determining the validity of a boolean formula with quantifiers over propositional variables. Without loss of generality, we restrict formulae to ¬, ∨, ∃. QBF problem is solved by the following program.

	6 Characterizing space bounded computation
	6.1 Polynomial space computation
	Definition 34 A RPO QI -program is a program that (i) admits a quasi-interpre-
	tation and (ii) which terminates by ≺ rpo .
	2

  arguments which are subterms of the v i 's. Therefore there are at most i≤n (|v i | + 1) such sub-calls. It follows from Lemma 14 that the number of sub-calls is bounded

	i≤n

  2Fig. 5. The lcs-covering graph of the call-tree.Theorem 47 Let f be an additive RPO QI Pro+Lin -program (resp. RPO QI Pro -program and RPO QI Lin -program). For each constructor term t 1 , • • • , t n , the runtime to compute f(t 1 , • • • , t n ) is bounded by a polynomial in max n i=1 |t i |. Lemma 46 implies that the time is bounded by a polynomial in max n i=1 |t i |. 2

		lcs, ababa, baaba
	lcs, baba, baaba	lcs, ababa, aaba
	lcs, aba, aaba	lcs, baba, aba
	lcs, ba, aba	lcs, aba, aba	lcs, baba, ba
	lcs, a, aba	lcs, ba, ba	lcs, ba, ba	lcs, aba, a
	lcs, ǫ, ba	lcs, a, a	lcs, a, a	lcs, ba, ǫ
		lcs, ǫ, ǫ	lcs, ǫ, ǫ

PROOF. By Proposition 12, we have

t i ≤ O(|t i |). For some polynomial P we have f(t 1 , • • • , t n ) ≤ P (max n i=1 |t i |)

, because quasi-interpretations are polynomially bounded.

  see that if a function symbol is linear, see Definition 40, then no result needs to be recorded. More generally, consider the f, t 1 , • • • , t n -call tree. When evaluating f, t 1 , • • • , t n , the call by value semantics with cache stores all values. Say that a separation set N is a set of states such that each chain starting from the root state f, t 1 , • • • , t n meets a state of N. If we know the value of each state of N, then values

			max, 4, 4
			max, 3, 3
		max, 3, 2	max, 2, 2
	max, 1, 2	max, 2, 1	max, 1, 1
	max, 0, 1	max, 1, 0	max, 0, 0

  we do not need anymore the configuration (f, t 1 , • • • , t n , t) and we can erase it from the cache. The set of functions computed by affine RPO QI Pro+Lin -programs (resp. RPO QI Proprograms and RPO QI Lin -programs) is exactly the set of functions computable in linear exponential time, that is in time bounded by 2 O(n) . • The set of functions computed by multiplicative RPO QI Pro+Lin -programs (resp. RPO QI Proprograms and RPO QI Lin -programs) is exactly the set of functions computable in linear double exponential time, that is in time bounded by 2 2 O(n) .

	7.3 Beyond polynomial time
	Theorem 48
	•

2

  Theorem 55 A polynomial space function is computed by an additive RPO QIprogram.PROOF. Let φ be a function which is computed by a PRM in time bounded by a polynomial P . Since P is also computed by a RPO QI -program following Proposition 53 and by composing with Lemma 51, we conclude that φ is computed by an additive RPO QI -program. 28.6 Simulation of exponential computationsProposition 56 Let γ > 0 be a constant. The function λn.2 γn is computed by an affine RPO QI Lin -program (resp. RPO QI Pro -program).PROOF. The function λn.2 γn is computed bymk γ (⋄) → ⋄ mk γ (s ′ (x)) → s′ (. . . (s ′ (mk γ (x))) . . .) γ times d(x) → add(x, x)add is defined in Prop 53 exp(⋄) → s(⋄) exp(s ′ (x)) → d(exp(x)) exp γ (x) → exp(mk γ (x))

1

  This program terminates by ≺ rpo with a product status. So, λn.2 γn is a RPO QI Proprogram and also a RPO QI Lin -program. 2 Theorem 57 A exponential time function is computed by an affine RPO QI Lin -program (resp. RPO QI Pro -program or RPO QI Pro+Lin -program). Theorem 58 An exponential space function is computed by an affine RPO QI -program. 8.7 Simulation of doubly exponential computations Proposition 59 Let γ > 0 be a constant. The function λn.2 2 γn is computed by an multiplicative RPO QI Lin -program (resp. RPO QI Pro -program).

Unlike[START_REF] Marion | Efficient first order functional program interpreter with time bound certifications[END_REF], we have decided to present the product extension instead of the permutation extension. This simplifies the presentation without loss of generality. Actually, there is a tedious procedure to transform the rules in order to prove termination by product ordering.

Since the product ordering is a restriction of the multiset ordering, any RPO Pro -program is also terminating by the more usual MPO termination ordering. Conversely, as stated above, there is a (somewhat tedious) procedure to turn MPO programs into RPO Proprograms

.[START_REF] Andersen | Generalizing Cook's transformation to imperative stack programs[END_REF] here, the RPO Lex -programs are exactly the programs terminating by the usual LPO termination ordering.

Theorem 39

• The set of functions computed by affine RPO QI -programs is exactly the set of functions computable in linear exponential space, that is in space bounded by 2 O(n) where n is the size of the inputs. • The set of functions computed by multiplicative RPO QI -programs is exactly the set of functions computable in linear double exponential space, that is in space bounded by 2 2 O(n) where n is the size of the inputs..

then there is at most one occurrence in r of a function symbol g with the same precedence than f, that is f ≈ F g.

Definition 41

(1) A RPO QI Pro -program is a program that (i) admits a quasi-interpretation, (ii) which terminates by ≺ rpo and (iii) each function symbol has a product status.

(2) A RPO QI Lin -program is a program that (i) admits a quasi-interpretation, (ii) which terminates by ≺ rpo , and (iii) each function symbol is linear and has a lexicographic status.

(3) A RPO QI Pro+Lin -program is a program that (i) admits a quasi-interpretation, (ii) which terminates by ≺ rpo and (iii) each function symbol which has a lexicographic status is linear, and others have a product status.

Tail recursive programs are RPO QI Lin -programs as it is illustrated by the reverse program in Example 28. On the other hand, the program that solves QBF in Example 36, is not a RPO QI Lin -program, because of the definition of verify (in the case of Exists(n, φ)) which leads to two recursive calls with substitution of parameters. Note that lexicographic ordering captures the template of recursion with parameter substitutions which was the key ingredient of the characterization of polynomial space functions [START_REF] Leivant | Ramified recurrence and computational complexity II: substitution and poly-space[END_REF] by tiering discipline.

Theorem 42 The set of functions computed by additive RPO QI Lin -programs (resp. RPO QI Pro -programs and RPO QI Pro+Lin -programs) is exactly the set of functions computable in polynomial time.

Time bounded simulation with lexicographic termination

Without loss of generality, we consider only unary functions in the following. It would be laborious to specify this simulation in full details otherwise.

Lemma 51 (Lexicographic Plug and play lemma) Assume that φ : W → W is a PRM-computable function in time bounded by T . Define f by

Then,

(1) the function f is computed by an additive RPO QI -program, (2) and, if f is computed by a RM, then f is computable by an additive RPO QI Linprogram.

PROOF. Suppose that f is computed by a PRM M. The simulation of the PRM M is done by following the rules of the semantic partial function eval. For this, the set of constructors is C = {0, 1, s, ⋄, ǫ} ∪ S where S is the set of states.

We show first that min ◭ and max ◭ are additive RPO QI -program.

with i ∈ {0, 1}.

We associate the following quasi-interpretations:

Next, we write a program to compute the semantic partial function eval.

Finally, put f(t, w) → Eval(t, begin, w, ǫ, . . . , ǫ). It is routine to check that f = f . These programs admit the following quasi-interpretations:

The status of each function symbol is lexicographic. The precedence satisfies {min, max} ≺ F Eval ≺ F f. We see that each rule is decreasing by ≺ rpo . Therefore, f is a RPO QIprogram. Now, observe that Eval has always one occurrence in the right hand side of the rules except in the fork cases. So, f is a RPO QI Lin -program if f is computed by a RM. 2

Time bounded simulation with product termination

In [START_REF] Marion | Efficient first order functional program interpreter with time bound certifications[END_REF], the simulation of RM is performed by a RPO QI Pro -program in a different manner because the status of function symbols is product and not lexicographic as in the above result. For this reason, we give details of the simulation of a time bounded function in the case where symbols have a product status.

Lemma 52 (Product Plug and play lemma) Assume that φ : W → W is a RM-computable function in time bounded by T . Define f by

Then, f is computable by an additive RPO QI Pro -program.

PROOF. Compared with the previous proof, the simulation is performed in bottomup way. For this, we use an extra constructor c to encode tuples. And we define Step which gives the next configuration.

(a)

Step(c(s,

The simulation is made by Eval(ǫ, x) → x Eval(s(t), x) → Step(Eval(t, x)) f(t, w) = Eval(t, c(begin, w, ǫ, . . . , ǫ))

The rules are ordered by putting Step ≺ F Eval where each symbol has now a product status. A quasi-interpretation of the rules is

The others constructor assignments are identical to the ones in the previous simulation described in the proof of Lemma 51

Unlike the previous proof, this simulation can not be extended in order to capture parallel computation.

And the program admits the following quasi-interpretations dmk γ (X) = X square (X) = X 2 dexp (X) = X + 2 dexp γ (X) = X + 2

This program terminates by ≺ rpo with a product status. So, λn.