Ugo Dal

Barbara Petit

Linear Dependent Types in a Call-by-Value Scenario

Keywords: Complexity Analysis, Implicit Computational Complexity, Type Systems, Linear Logic

Linear dependent types were introduced recently [1] as a formal system that allows to precisely capture both the extensional behavior and the time complexity of λ-terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to callby-value computation. A system of linear dependent types for Plotkin's PCF is introduced, called dℓPCF V , whose types reflect the complexity of evaluating terms in the CEK machine. dℓPCF V is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behaviour of terms can be derived, provided all true index term inequalities can be used as assumptions.

Introduction

Program verification is one of the most challenging activities in computer science, due to the fundamental limitations recursion theory and complexity theory pose on it. A variety of methodologies for formally verifying properties of programs have been introduced in the last fifty years. Among them, type systems have certain peculiarities. On the one hand, the way type systems are defined makes the task of proving a given program to have a type simple and modular: a type derivation for a compound program usually consists of some type derivations for the components, appropriately glued together in a syntax-directed way (i.e., attributing a type to a program can usually be done compositionally). On the other, the kind of specifications that can be expressed through types have traditionally been weak, although stronger properties have recently become of interest, including security properties [START_REF] Volpano | A sound type system for secure flow analysis[END_REF][START_REF] Sabelfeld | Language-based information-flow security[END_REF], termination [START_REF] Barthe | Type-based termination with sized products[END_REF], monadic temporal properties [START_REF] Kobayashi | A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes[END_REF] or resource bounds [START_REF] Karlbary | Resource bound certification[END_REF][START_REF] Jost | Static Determination of Quantitative Resource Usage for Higher-Order Programs[END_REF]. But contrarily to what happens with other formal methods (e.g. model checking or program logics), giving a type to a program t is a sound but incomplete way to prove t to satisfy a specification: there are correct programs which cannot be proved such by way of typing.

In other words, the tension between expressiveness and tractability is particularly evident in the field of type systems, where certain good properties the majority of type systems enjoy (e.g. syntax-directedness) are usually considered desirable (if not necessary), but also have their drawbacks: some specifications are intrinsically hard to verify locally and compositionally. One specific research field in which the just-described scenario manifests itself is complexity analysis, in which specifications are concrete or asymptotic bounds on the complexity of the underlying program. Many type systems have been introduced capturing, for instance, the class of polynomial time computable functions [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF][START_REF] Baillot | Light types for polynomial time computation in lambda calculus[END_REF][START_REF] Baillot | A polytime functional language from light linear logic[END_REF]. All of them, under mild assumptions, can be employed as tools to certify programs as asymptotically time efficient. However, a tiny slice of the polytime programs are generally typable, since the underlying complexity class FP is only characterized in a purely extensional sense -for every function in FP there is at least one typable program computing it.

Gaboardi and the first author have recently introduced [START_REF] Lago | Linear dependent types and relative completeness[END_REF] a type system for Plotkin's PCF, called dℓPCF N , in which linearity and a restricted form of dependency in the spirit of Xi's DML [START_REF] Xi | Dependent types for program termination verification[END_REF] are present:

• Linearity makes it possible to precisely control the number of times subterms are copied during the evaluation of a term t. This number is actually a parameter which accurately reflects the time complexity of evaluating t [START_REF] Lago | Context semantics, linear logic, and computational complexity[END_REF]. • Dependency allows to type distinct (virtual) copies of a term with dis-tinct types. This gives the type system an extra flexibility similar to that of intersection types [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF][START_REF] Carvalho | Execution time of lambda-terms via denotational semantics and intersection types[END_REF]. When mixed together, these two ingredients allow to precisely capture the extensional behavior of λ-terms and the time complexity of their evaluation by the Krivine's Abstract Machine [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF] (KAM). Both soundness and relative completeness hold for dℓPCF N . Noticeably, this not only holds for terms of base type, but also for first-order functions.

One may argue, however, that the practical relevance of these results is quite limited, given that call-by-name evaluation and KAM are very inefficient: why would one be interested in verifying the complexity of evaluating concrete programs in such a setting?

In this work, we show that linear dependent types can also be applied to the analysis of call-by-value evaluation of functional programs. This is done by introducing another system of linear dependent types for Plotkin's PCF. The system, called dℓPCF V , captures the complexity of evaluating terms by Felleisen and Friedman's CEK machine [START_REF] Felleisen | Control Operators, the SECD-Machine and the λ-Calculus[END_REF], a simple abstract machine for call-by-value evaluation. dℓPCF V is proved to have the same good properties enjoyed by its sibling dℓPCF N , namely soundness and relative completeness: every true statement about the intensional (and extensional) behavior of terms can be derived, provided all true index term inequalities can be used as assumptions.

Actually, dℓPCF V is not merely a variation on dℓPCF N : not only typing rules are different, but also the language of types itself must be modified. Roughly, dℓPCF V and dℓPCF N can be thought as being induced by two translations of intuitionistic logic into linear logic: the latter corresponds to Girard's translation A ñ B " !A ⊸ B, while the former corresponds to A ñ B " !pA ⊸ Bq. The strong link between translations of IL into ILL and notions of reduction for the λ-calculus is well-known (see e.g. [START_REF] Maraist | Call-by-name, call-byvalue, call-by-need and the linear lambda calculus[END_REF]) and has been a guide in the design of dℓPCF V (this is explained in Section. 2.2). Overall, dℓPCF V is arguably simpler than dℓPCF N : base types need not be annotated with the ! operator.

Linear Dependent Types, Intuitively

Consider the following program:

dbl " fix f.λx. ifz x then x else spspf pppxqqqq. In a type system like PCF [START_REF] Plotkin | LCF considerd as a programming language[END_REF], the term dbl receives type Nat ñ Nat. As a consequence, dbl computes a function on natural numbers without "going wrong": it takes in input a natural number, and (possibly) produces in output another natural number. The type Nat ñ Nat, however, does not give any information about which specific function on the natural numbers dbl computes.

Properties of programs which are completely ignored by ordinary type systems are termination and its most natural refinement, namely termination within appropriate time bounds (e.g., polynomial bounds). Typing a term t with Nat ñ Nat does not guarantee that t, when applied to a natural number, terminates. Consider, as another example, a slight modification of dbl, namely div " fix f.λx. ifz x then x else spspf pxqqq.

It behaves as dbl when fed with 0, but it diverges when it receives a strictly positive natural number as argument. But look: div is not so different from dbl. Indeed, the latter can be obtained from the former by feeding not x but ppxq to the "recursive call" f . And any type system in which dbl and div are somehow recognized as being fundamentally different must be able to detect the presence of p in dbl and deduce termination from it. Indeed, sized types [START_REF] Barthe | Type-based termination with sized products[END_REF] and dependent types [START_REF] Xi | Dependent types for program termination verification[END_REF] are able to do so. Going further, we could ask the type system to be able not only to guarantee termination, but also to somehow evaluate the time or space consumption of programs. For example we could be interested in knowing that, on any natural number, dbl takes a polynomial number of steps to be evaluated in a given machine, and actually some type systems able to control the complexity of higher-order programs exist. Good examples are type systems for amortized analysis [START_REF] Jost | Static Determination of Quantitative Resource Usage for Higher-Order Programs[END_REF][START_REF] Hoffmann | Multivariate Amortized Resource Analysis[END_REF] or those using ideas from linear logic [START_REF] Baillot | Light types for polynomial time computation in lambda calculus[END_REF][START_REF] Baillot | A polytime functional language from light linear logic[END_REF]: in all of them, linearity plays a key role.

dℓPCF N [START_REF] Lago | Linear dependent types and relative completeness[END_REF] combines some of the ideas presented above with the principles of bounded linear logic (BLL [START_REF] Girard | Bounded linear logic: A modular approach to polynomial-time computability[END_REF]): the cost of evaluating a term is measured by counting how many times function arguments need to be copied during evaluation, and different copies can be given distinct, although uniform, types. Making this information explicit in types permits to compute the cost step by step during the type derivation process. Roughly, typing judgments in dℓPCF N are statements like

$ J t : ! n Natras ⊸ NatrIs,
where I and J depend on a and n is a natural number capturing the number of times t uses its argument. But this is not sufficient: analogously to what happens in BLL, dℓPCF N makes types more parametric. A type like ! n σ ⊸ τ is replaced by the more accurate ! aăn σ ⊸ τ , which tells us that the argument will be used n times, and each instance has type σ where, however, the variable a is substituted by a value less than n. This allows to type each copy of the argument differently but uniformly, since all instances of σ have the same PCF skeleton. This form of uniform linear dependence is actually crucial in obtaining the result which makes dℓPCF N different from similar type systems, namely completeness. As an example, dbl can be typed as follows in dℓPCF N :

$ E a dbl :! băa`1 Natras ⊸ Natr2 ˆas.
This tells us that the argument will be used a `1 times by dbl, and that the cost of evaluation will be itself proportional to a.

Why Another Type System?

The theory of λ-calculus is full of interesting results, one of them being the so-called Church-Rösser property: both β and βη reduction are confluent, i.e., if you fire two distinct redexes in a λ-term, you can always "close the diagram" by performing one or more rewriting steps. This, however, is only a local confluence result, and as such does not imply that all reduction strategies are computationally equivalent. Indeed, some of them are normalizing (like normal-order evaluation) while some others are not (like innermost reduction). But how about efficiency?

On the one hand, it is well known that optimal reduction is indeed possible [START_REF] Lamping | An algorithm for optimal lambda calculus reduction[END_REF], even if it gives rise to high overheads [START_REF] Asperti | Parallel beta reduction is not elementary recursive[END_REF]. On the other, call-byname evaluation (cbn) may be highly inefficient. Consider, as an example, the composition of dbl with itself:

dbl2 " λx.dblpdbl xq.
The term dbl2 n takes quadratic time to be evaluated by the KAM, since the evaluation of dbl n is repeated a linear number of times, whenever it reaches the head position. This actually can be seen from within dℓPCF N , since

$ E J dbl2 :! băI Natras ⊸ Natr4 ˆas,
where both I and J are quadratic in a (more precisely, I " 2a 2 `3a `1 and J " 4a 2 `8a `2). Call-by-value (cbv) solves this problem, at the price of not being normalizing. Indeed, eager evaluation of dbl2 when fed with a natural number n takes linear time in n. Besides giving examples like the one above, little can be said about the relative efficiency of call-by-value and call-by-name evaluation: the two are clearly incomparable from an analytical point of view (consider, as an another example, the term pλx.λy.xqΩ). A nice informal discussion about the advantages and disadvantages of call-by-value and call-by-name evaluation can be found in [START_REF] Asperti | The Optimal Implementation of Functional Programming Languages[END_REF], together with a comparison with Levy's notion of optimal reduction. The reason why a step forward dℓPCF N is needed is not necessarily related to efficiency: simply, in many modern functional programming languages (like OCaml and Scheme) terms are call-by-value evaluated. And on the other hand, upper bounds on the time complexity of programs written in functional languages (which can be seen as the long term goal of this line of research) should reflect the underlying evaluation strategy, which is an essential part of their definition, and not merely an implementation detail.

For the reasons above, we strongly believe that designing a type system in the style of dℓPCF N , but able to deal with eager evaluation, is a step forward applying linear dependent types to ML-like programming languages.

Call-by-Value, Call-by-Name and Linear Logic

Various notions of evaluation for the λ-calculus can be seen as translations of intuitionistic logic (or simply-typed λ-calculi) into Girard's linear logic. This correspondence has been investigated in the specific cases of call-byname, call-by-value, and call-by-need reduction (e.g. see the work of Maraist et al. [START_REF] Maraist | Call-by-name, call-byvalue, call-by-need and the linear lambda calculus[END_REF]). In this section, we briefly introduce the main ideas behind the correspondence, explaining why linear logic has guided the design of dℓPCF V .

The general principle in such translations, is to guarantee that whenever a term can possibly be duplicated, it must be mapped to a box in the underlying linear logic proof. In the cbn translation (also called Girard's translation), any argument to functions can possibly be substituted for a variable and copied, so arguments are banged during the translation:

pA ñ Bq ˚" p!A ˚q ⊸ B ˚.
Adding the quantitative bound on banged types (as explained in the previous section) gives rise to the type p! aăI σq ⊸ τ for functions (written ra ă Is¨σ ⊸ τ in [START_REF] Lago | Linear dependent types and relative completeness[END_REF]). In the same way, contexts are banged in the cbn translation: a typing judgment in dℓPCF N has the following form:

x 1 : ! a 1 ăI 1 σ 1 , . . . , x n : ! anăIn σ n $ J t : τ.
In the cbv translation, β-reduction should be performed only if the argument is a value. Thus, arguments are not automatically banged during the translation but values are, so that β-reduction remains blocked until the argument reduces to a value. In the λ-calculus functions are values, hence the translation of the intuitionistic arrow becomes

pA ñ Bq ˝" !pA ˝⊸ B ˝q.
Accordingly, function types have the form ! aăI pσ ⊸ τ q in dℓPCF V , and a judgment has the form x 1 : σ 1 , . . . , x n : σ n $ J t : τ. The syntax of types varies fairly much between dℓPCF N and dℓPCF V , and consequently the two type systems are different, although both of them are greatly inspired by linear logic.

In both dℓPCF N and dℓPCF V , however, the "target" of the translation is not the whole of ILL, but rather a restricted version of it, namely BLL, in which the complexity of normalization is kept under control by shifting from unbounded, infinitary, exponentials to finitary ones. For example, the BLL contraction rule allows to merge the first I copies of A, and the following J ones into the first I `J copies of A:

Γ, ! aăI A, ! aăJ AtI `a{au $ B Γ, ! aăI`J A $ B
We write σ Z τ "! aăI`J A if σ "! aăI A and τ "! aăJ AtI `a{au. Whenever a contraction rule is involved in the cbv translation of a type derivation, a sum Z appears at the same place in the corresponding dℓPCF V derivation.

Similarly, the dereliction rule allows to see any banged type as the first copy of itself: Γ, At0{au $ B Γ, ! aă1 A $ B hence any dereliction rule appearing in the translation of a typing judgment tells us that the corresponding type is copied once. Both contraction and dereliction appear while typing an application in dℓPCF V : the PCF typing rule Γ $ t :

A ñ B Γ $ u : A Γ $ tu : B corresponds to the ILL proof z: A ˝⊸B ˝$z: A ˝⊸B !z: !pA ˝⊸B ˝q$z: A ˝⊸B ˝Γ˝$ t ˝: !pA ˝⊸B ˝q Γ ˝$t ˝: A ˝⊸B ˝Γ˝$ u ˝: A Γ˝, Γ ˝$t ˝u˝: B Γ˝$
t ˝u˝: B which becomes the following, when appropriately decorated according to the principles of BLL (writing A 0 and B 0 for At0{au and Bt0{au, respectively):

z: A 0⊸B 0 $z: A 0⊸B 0 !z: !aă1pA ˝⊸B ˝q$z: A 0⊸B 0 Γ ˝$t ˝: !aă1pA ˝⊸B ˝q Γ ˝$t ˝: A 0⊸B 0 Γ ˝$u ˝: A 0 Γ ˝, Γ ˝$t ˝u˝: B 0 Γ ˝ZΓ ˝$t ˝u˝: B 0
The cbv translation of the application rule hence leads to the typing rule for applications in dℓPCF V :

Γ $ K t :! aă1 pσ ⊸ τ q ∆ $ H u : σt0{au Γ Z ∆ $ K`H tu : τ t0{au
The same kind of analysis allows to derive the typing rule for abstractions (whose call-by-value translation requires the use of a promotion rule) in dℓPCF V : Γ, x : σ $ K t : τ ř aăI Γ $ I`ř aăI K λx.t :! aăI pσ ⊸ τ q One may wonder what the term I represents in this typing rule, and more generally in a judgment such as Γ $ K t : ! aăI A. This is actually the main new idea of dℓPCF V : such a judgment intuitively means that the value to which t reduces will be used I times by the environment. If t is applied to an argument u, then t must reduce to an abstraction λx.s, that is used by the argument without being duplicated. In that case, I " 1, as indicated by the application typing rule. On the opposite, if t is applied to a function λx.u, then the type of this function must be of the form (up to a substitution of b) ! bă1 pp! aăI Aq ⊸ τ q. This means that λx.u uses I times its arguments, or, that x can appear at most I times in the reducts of u.

This suggests that the type derivation of a term is not unique in general: whether a term t has type ! aăI A or ! aăJ A depends on the use we want to make of t. This intuition will direct us in establishing the typing rules for the other PCF constructs (namely conditional branching and fixpoints).

dℓPCF V , Formally

In this section, the language of programs and a type system dℓPCF V for it will be introduced formally. While terms are just those of a fairly standard λ-calculus (namely Plotkin's PCF), types may include so-called index terms, which are first-order terms denoting natural numbers by which one can express properties about the extensional and intentional behavior of programs.

PCF

Plotkin introduced PCF [18] as a simply typed lambda calculus with full recursion. Terms of the language also include primitive natural numbers, predecessor and successor operators as well as a branching construct. PCF as in [START_REF] Plotkin | LCF considerd as a programming language[END_REF] also includes booleans, which we elide here for the sake of simplicity. We here adopt a call-by-value version of PCF. Values and terms are generated by the following grammar:

Values v, w ::" n | λx.t | fix x.t; Terms s, t, u ::" x | v | tu | sptq | pptq | ifz t then u else s.
The cbv operational semantics of PCF is generated by the rules in Figure 1, subject to the closure rules in Figure 2. The language is provided with a simple type system. Types (denoted by T , U ) are those generated by the basic type Nat and the binary type constructor ñ, and typing rules are standard (Figure 3). A term t is said to be a program if it can be given the PCF type Nat in the empty context. Notice that a typable PCF term is not guaranteed to terminate. For instance the term t ω def " fix y.λx.yx is typable with Nat ñ Nat. However, for any natural number n, the term t ω n call-by-value reduces to itself in two steps. In dℓPCF (Section 3.4), we decorate PCF types with some cost annotations (that are indexes, see Section 3.3), so that the evaluation complexity of a term can be deduced from its type. In particular, only terminating terms are typable.

The complexity bound that we will give for a given PCF term t will be related to its syntactic size |t|:

pλx.tq v Ñ v trx :" vs spnq Ñ v n `1 ppn `1q Ñ v n pp0q Ñ v 0 ifz 0 then t else u Ñ v t ifz n `1 then t else u Ñ v u p fix x.tq v Ñ v ptrx :" fix x.tsq v
t Ñ v s tu Ñ v su t Ñ v s ut Ñ v us t Ñ v s sptq Ñ v spsq t Ñ v s pptq Ñ v ppsq t Ñ v s ifz t then u else p Ñ v ifz s then u else p

Π, x

: T $ x : T Π, x : U $ t : T Π $ λx.t : U ñ T Π $ t : U ñ T Π $ u : U Π $ tu : T Π $ n : Nat Π $ t : Nat Π $ sptq : Nat Π $ t : Nat Π $ pptq : Nat Π $ t : Nat Π $ u : T Π $ s : T Π $ ifz t then u else s : T Π, x : T $ t : T Π $ fix x.t : T
|n| " |x| " 2; |λx.t| " | fix x.t| " |t| `2;

|tu| " |t| `|u| `2; |sptq| " |pptq| " |t| `2; | ifz t then u else s| " |t| `|u| `|s| `2.

In other words, every symbol counts for 2 in the syntactic size of a term. In the following, we might also consider the multiplicative size of PCF terms. It is defined as their syntactic size, except on values which have null multiplicative size (see Figure 11 for a formal definition). The reason why values are not taken into account by the multiplicative size, is that evaluation by the CEK abstract machine (that will be used to define the complexity of a term, see Section 3.2) proceeds by first scanning terms until a value is reached, and the cost of these initial steps is taken into account by the multiplicative size. Then this value is either erased (e.g. when a lambda abstraction is given an argument), or duplicated (e.g. when it is itself the argument to a lambda abstraction). The cost of this second phase is measured by the type system dℓPCF V .

An Abstract Machine for PCF

The call-by-value evaluation of PCF terms can be faithfully captured by an abstract machine in the style of CEK [START_REF] Felleisen | Control Operators, the SECD-Machine and the λ-Calculus[END_REF], which is the subject of this section.

The internal state of the CEK PCF machine consists of a closure and a stack, interacting following a set of rules (figures 4 and 5). The machine mimics weak call-by-value evaluation of programs: it starts with a closed term (or, formally, a closure) and an empty stack, and scans the term until it reaches its head subterm. Doing this, it records all the other subterms (that constitute its evaluation context) in the stacks. Once the head subterm has been reached, one of the reduction rules of Figure 1 is simulated.

Formally, a value closure is a pair v " x v ; ξ y where v is a value and ξ is an environment, itself a list of assignments of value closures to variables:

ξ ::" H | px Þ Ñ vq ¨ξ.
A closure is a pair c " x t ; ξ y where t is a term (and not necessarily a value). Given a closure c, one naturally define the unfolding Unfpcq, namely the x (closed) term obtained by iteratively substituting variables for terms, i.e.,

v ‹ argpc , πq ą c ‹ funpv , πq v ‹ funpx λx.t ; ξ y , πq ą x t ; px Þ Ñ vq ¨ξ y ‹ π v ‹ funpx fix x.t ; ξ y , πq ą x t ; px Þ Ñ x fix x.t ; ξ yq ¨ξ y ‹ argpv , πq x 0 ; ξ 1 y ‹ forkpt , u , ξ , πq ą x t ; ξ y ‹ π x n`1 ; ξ 1 y ‹ forkpt , u , ξ , πq ą x u ; ξ y ‹ π x n ; ξ y ‹ spπq ą x n`1 ; H y ‹ π x n ; ξ y ‹ ppπq ą x n´1 ; H y ‹ π
x ; ξ y ‹ π ą ξpxq ‹ π x tu ; ξ y ‹ π ą x t ; ξ y ‹ argpx u ; ξ y , πq x sptq ; ξ y ‹ π ą x t ; ξ y ‹ spπq x pptq ; ξ y ‹ π ą x t ; ξ y ‹ ppπq x ifz t then u else s ; ξ y ‹ π ą x t ; ξ y ‹ forkpu , s , ξ , πq
Unfpx t ; px 1 Þ Ñ v 1 q ¨. . . ¨px n Þ Ñ v n q yq " trx 1 :" Unfpv 1 qs ¨¨¨rx n :" Unfpv n qs.
Stacks are terms from the following grammar:

π ::" ˛| argpc , πq | funpv , πq | forkpt , u , ξ , πq | spπq | ppπq.
A process P is then a pair c ‹ π of a closure and a stack. The stack π describes the evaluation context (or the continuation) of the closure c. If it is in the form argpc o , π o q, it means that c o is the first argument of c, and π o is its continuation. Conversely, if π is funpv o , π o q, it means that after evaluating c, its value will be given as argument to the function represented by v. These constructions are used to simulate call-by-value β-reduction. Indeed, to evaluate the application of a function t to an argument u, the CEK PCF first computes the value λx.t o of t, then the value v of u, and last maps the variable x to v in t o :

x tu ; ξ y ‹ π ą x t ; ξ y ‹ argpx u ; ξ y , πq ą ˚x λx.t o ; ξ y ‹ argpx u ; ξ y , πq ą x u ; ξ y ‹ funpx λx.t o ; ξ y , πq ą ˚v ‹ funpx λx.t o ; ξ y , πq ą x t o ; px Þ Ñ vq ¨ξ y ‹ π
The last three constructions defining a stack are used to describe the evaluation context of a program whose value is a number. forkpt , u , ξ , π o q means that t will then be evaluated if this value is zero, and if it is strictly positive then u will be evaluated (in both cases, ξ will be the environment and π o the next continuation). spπ o q and ppπ o q mean that the successor and the predecessor of this value will be evaluated, respectively.

Figure 5 gives the formal rules that the CEK PCF follows to scan a term until the head subterm (which is a value) is reached, while Figure 4 gives the ones that simulate a reduction rule of PCF (Figure 1).

Evaluating a term t in the CEK PCF consists in iteratively applying any of these rules, starting from the process x t ; H y ‹ ˛. Please observe that the behavior of the machine is deterministic, since any process can be the left hand side of at most one evaluation rule. If the evaluation of a correct (i.e. typable) closed PCF term terminates, then it leads to a process on the form x v ; ξ y ‹ ˛. In this case, we may use the following notations: Definition 3.1 We say that a term t evaluates to a value v and we write t ó v when px t ; H y ‹ ˛q ą ˚px w ; ξ y ‹ ˛q and Unfpx w ; ξ yq " v. We also write t ó n v to specify that n steps are required for this evaluation to end.

The following ensures that the CEK PCF is an adequate methodology to evaluate PCF terms:

Proposition 3.1 (Adequacy) If t is a PCF term of type Nat, then t Ñ v n iff t ó n.
Proof. The proof is standard and proceeds as follows:

• On the one hand, one generalizes Unfp¨q to processes in the obvious way.

Moreover, the PCF type system is itself lifted to environments, closures, stacks, and ultimately processes. • On the other hand, it is shown that whenever P ą R, then UnfpPq Ñ v UnfpRq.

• Finally, it is shown that a typable process P is irreducible precisely when Unfp¨q is a value. l

Index Terms and Equational Programs

Syntactically, index terms are built either from function symbols from a given untyped signature Θ or by applying any of two special term constructs:

I, J, K ::" a | fpI 1 , . . . , I n q | ÿ aăI J | I,J ï a K.
Here, f is a symbol of arity n from Θ and a is a variable drawn from a set V of index variables. We assume the symbols 0, 1 (of arity 0) and `, ´(of arity 2) are always part of Θ (they will be used in the typing rules). An index term in the form ř aăI J is a bounded sum, while one in the form

Ï I,J a K is a forest cardinality. For every natural number n, the index term n is just 1 `1 `. . . `1 looooooomooooooon n times .
Index terms are meant to denote natural numbers, possibly depending on the (unknown) values of variables. Variables can be instantiated with other index terms, e.g. ItJ{au. So, index terms can also act as first order functions. What is the meaning of the function symbols from the signature Θ? It is the one induced by an equational program E. Formally, an equational program E over a signature Θ is a set of equations in the form I " J where both I and J are index terms. We are interested in equational programs guaranteeing that, whenever symbols in Θ are interpreted as partial functions over N and 0, 1, ànd ´are interpreted in the usual way, the semantics of any function symbol f can be uniquely determined from E. This can be guaranteed by, for example, taking E as an Herbrand-Gödel scheme [START_REF] Odifreddi | Classical Recursion Theory: the Theory of Functions and Sets of Natural Numbers, number 125[END_REF] or as an orthogonal constructor term rewriting system [START_REF] Baader | Term Rewriting and All That[END_REF]. The definition of index terms is parametric on Θ and E: this way one can tune our type system from a highly undecidable but truly powerful machinery down to a tractable but less expressive formal system.

What about the meaning of bounded sums and forest cardinalities? The first is very intuitive: the value of ř aăI J is simply the sum of all possible values of J with a taking the values from 0 up to I, excluded. Forest cardinalities, on the other hand, require some effort to be described. Informally, Ï I,J a K is an index term denoting the number of nodes in a forest composed of J trees described using K. All the nodes in the forest are (uniquely) identified by natural numbers. These are obtained by consecutively visiting each tree in preorder, starting from I. The term K has the role of describing the number of children of each forest node, e.g., the number of children of the node 0 is Kt0{au. More formally, the meaning of a forest cardinality is defined by the following two equations:

I,0 ï a K " 0; I,J`1 ï a K " ˜I,J ï a K ¸`1 `¨I `1`Ï I,J a K,KtI`Ï I,J a K{au ï a K '.
The first equation says that a forest of 0 trees contains no nodes. The second one tells us that a forest of J `1 trees contains:

• The nodes in the first J trees;

• plus the nodes in the last tree, which are just one plus the nodes in the immediate subtrees of the root, considered themselves as a forest. To better understand forest cardinalities, consider the following forest com-prising two trees: It is well described by an index term K with a free index variable a such that Kt1{au " 3; Ktn{au " 2 for n P t2, 8u; Ktn{au " 1 when n P t0, 6, 9, 11u; and Ktn{au " 0 when n P t3, 4, 5, 7, 10, 12u. That is, K describes the number of children of each node. Then Ï 0,2 a K " 13 since it takes into account the entire forest; Ï 0,1 a K " 8 since it takes into account only the leftmost tree; Ï 8,1 a K " 5 since it takes into account only the second tree of the forest; finally, Ï 2,3 a K " 6 since it takes into account only the three trees (as a forest) within the dashed rectangle.

One may wonder what is the role of forest cardinalities in the type system. Actually, they play a crucial role in the treatment of recursion, where the unfolding of recursion produces a tree-like structure whose size is just the number of times the (recursively defined) function will be used globally. Note that the value of a forest cardinality could also be undefined. For instance, this happens when infinite trees, corresponding to diverging recursive computations, are considered.

The expression I E ρ denotes the meaning of I, defined by induction along the lines of the previous discussion, where ρ : V Ñ N is an assignment and E is an equational program giving meaning to the function symbols in I. Since E does not necessarily interpret such symbols as total functions, and moreover, the value of a forest cardinality can be undefined, I E ρ can be undefined itself. A constraint is an inequality in the form I ď J. Such a constraint is true (or satisfied ) in an assignment ρ if I E ρ and J E ρ are both defined and the first is smaller or equal to the latter. Now, for a subset φ of V, and for a set Φ of constraints involving variables in φ, the expression φ; Φ ( E I ď J denotes the fact that the truth of I ď J semantically follows from the truth of the constraints in Φ. To denote that I is well defined for E and any valuation ρ satisfying Φ, we may write φ; Φ ( E I ó instead of φ; Φ ( E I ď I.

φ; Φ ( E K ď I φ; Φ ( E J ď H φ; Φ $ E NatrI, Js Ď NatrK, Hs φ; Φ $ E ̺ Ď σ φ; Φ $ E τ Ď ϕ φ; Φ $ E σ ⊸ τ Ď ̺ ⊸ ϕ pa, φq; pa ă J, Φq $ E A Ď B φ; Φ ( E J ď I φ; Φ $ E ra ă Is ¨A Ď ra ă Js ¨B

The dℓPCF V Type System

The Language of Types. The type system dℓPCF V can be seen as a refinement of PCF obtained by a linear decoration of its type derivations. Linear and modal types are defined as follows:

Linear Types A, B ::" σ ⊸ τ ;

Modal Types σ, τ ::" ra ă Is ¨A | NatrI, Js.

where I, J range over index terms and a ranges over index variables. Modal types need some comments. Natural numbers are freely duplicable, so NatrI, Js is modal by definition. As a first approximation, ra ă Is ¨A can be thought of as a universal quantification of A, and so a is bound in the linear type A.

Moreover, the condition a ă I says that σ consists of all the instances of the linear type A where the variable a is successively instantiated with the values from 0 to I ´1, i.e., At0{au, . . . , AtI ´1{au. For those readers who are familiar with linear logic, and in particular with BLL, the modal type ra ă Is ¨A is a generalization of the BLL formula ! aăp A to arbitrary index terms. As such it can be thought of as representing the type At0{au b ¨¨¨b AtI ´1{au. NatrIs is syntactic sugar for NatrI, Is. As usual, the variable a is said to be bound in the modal type ra ă Is ¨A, and when a does not appear free in σ nor in τ we may write σ I ⊸ τ instead of ra ă Is ¨σ ⊸ τ . In the typing rules we are going to define, modal types are manipulated in an algebraic way. For this reason, two operations on modal types need to be introduced. The first one is a binary operation Z on modal types. Suppose that σ " ra ă Is ¨Ata{cu and that τ " rb ă Js ¨AtI `b{cu. In other words, σ consists of the first I instances of A, i.e. At0{cu, . . . , AtI ´1{cu while τ consists of the next J instances of A, i.e. AtI `0{cu, . . . , AtI `J ´1{cu. Their sum σ Z τ is naturally defined as a modal type consisting of the first I `J instances of A, i.e. rc ă I `Js ¨A. Furthermore, NatrI, Js Z NatrI, Js is just NatrI, Js. An operation of bounded sum on modal types can be defined by generalizing the idea above: suppose that σ " rb ă Js ¨Atb `ÿ dăa Jtd{au{cu.

φ; Φ; Γ, x : σ $ E 0 x : σ pAxq φ; Φ; Γ $ E 0 n : Natrn, ns pnq pa, φq; pa ă I, Φq; Γ, x : σ $ E K t : τ φ; Φ; ř aăI Γ $ E I`ř aăI K λx.t : ra ă Is ¨σ ⊸ τ p⊸q φ; Φ; Γ $ E K t : ra ă 1s ¨σ ⊸ τ φ; Φ; ∆ $ E H u : σt0{au φ; Φ; Γ Z ∆ $ E K`H tu : τ t0{au pAppq φ; Φ; Γ $ E M t : NatrI, Js φ; Φ; Γ $ E M sptq : NatrI `1, J `1s psq φ; Φ; Γ $ E M t : NatrI, Js φ; Φ; Γ $ E M pptq : NatrI ´1, J ´1s ppq φ; Φ; Γ $ E M t : NatrJ, Ks φ; pJ ď 0, Φq; ∆ $ E N u : τ φ; pK ě 1, Φq; ∆ $ E N s : τ φ; Φ; Γ Z ∆ $ E M`N ifz t then u else s : τ pIfq pb, φq; pb ă H, Φq; Γ, x : ra ă Is ¨A $ E J t : ra ă 1s ¨B pa, b, φq; pa ă I, b ă H, Φq $ E Bt0{aut Ï b`1,a b I `b `1{bu Ď A φ; Φ; ř băH Γ $ E H`ř băH J fix x.t : ra ă Ks ¨Bt0{aut Ï 0,a b I{bu pFixq (where H " Ï 0,K b I) φ; Φ; Γ $ E I t : σ φ; Φ $ E ∆ Ď Γ φ; Φ $ E σ Ď τ φ; Φ ( E I ď J φ; Φ; ∆ $ E J t : τ pSubsq
Then its bounded sum ř aăI σ is just rc ă ř aăI Js¨A. Finally, ř aăI NatrJ, Ks " NatrJ, Ks, provided a is not free in J nor in K.

Subtyping. Central to dℓPCF V is the notion of subtyping. An inequality relation Ď between (linear or modal) types can be defined using the formal system in Figure 6. This relation corresponds to lifting index inequalities at the type level. Please observe that Ď is a preorder, i.e., a reflexive and transitive relation.

Typing. A typing judgment is of the form φ; Φ; Γ $ E K t : τ,
where K is the weight of t, that is (informally) the maximal number of substitutions involved in the cbv evaluation of t. Φ is a set of constraints (see Section 3.3) that we call the index context, and Γ is a context assigning a modal type to (at least) each free variable of t. Both sums and bounded sums are naturally extended from modal types to contexts (with, for instance, tx : σ; y : τ u Z tx : ζ, z : ηu " tx : σ Z ζ; y : τ ; z : ηu). There might be free index variables in Φ, Γ, τ and K, all of them from φ. Typing judgments can be derived from the rules of Figure 7. We are implicitly assuming that all index terms appearing in (derivable) typing judgments are defined in the appropriate index contexts. Derivation rules for abstractions and applications have been informally presented in Section 2.2. The other ones are then intuitive, except the derivation rule for typing fix x.t, that is worth an explanation: to simplify, assume we want to type only one copy of its type (that is, K " 1). To compute the weight of fix x.t, we need to know the number of times t will be copied during the evaluation, that is the number of nodes in the tree of its recursive calls. This tree is described by I (as explained in Section 3.3), since each occurrence of x in t stands for a recursive call. It has, say, H " Ï 0,1 b I nodes. At each node b of this tree, the a th occurrence of x will be replaced by the a th child of b, i.e. by b `1 `Ïb`1,a b I. The types have to match, and that is what the second premise expresses. Finally, the type of fix x.t is the type of the "main" copy of t, at the root of the tree (i.e., at b " 0). The weight counts all the recursive calls (i.e., H) plus the weight of each copy of t (i.e., the weight of t for each b ă H).

Last, the subsumption rule pSubsq allows to relax the precision standard of a typing judgment. One can also restrict the inequalities on indexes to equalities in this rule, this way constructing precise typing judgments. Observe that the set of all rules but this one is syntax directed. Moreover, the subsumption rule preserves the PCF skeleton of the types, and so the type system is itself syntax directed up to index inequalities.

Weights and the CEK PCF Machine. As it will be formalized in Section 5.3, an upper bound for the evaluation of a given term in the CEK PCF machine can be obtained by multiplying its weight and its syntactic size. This result can be explained as follows: the weight of a program represents the maximal number of substitutions in its cbv evaluation, and thereby the maximal number of steps of the form v ‹ funpx λx.t ; ξ y , πq ą x t ; px Þ Ñ vq ¨ξ y ‹ π;

(1)

v ‹ funpx fix x.t ; ξ y , πq ą x t ; px Þ Ñ x fix x.t ; ξ yq ¨ξ y ‹ argpv , πq (2)
in its evaluation with the CEK PCF . Between two such steps, the use of the other rules is not taken into account by the weight; however the other rules make the size of the process smaller.

Examples

In this section we will see how to type some common terms in dℓPCF V . As a byproduct, we will derive a weight for them.

Addition

In PCF, addition can be computed as follows:

add " fix x.λyz. ifz y then z else spx ppyq zq, and has type Nat ñ Nat ñ Nat. A brief analysis of its evaluation, if we apply it to two values v and w in Nat, indicates that a correct annotation for this type in dℓPCF V would be ra ă 1s ¨pNatrds ⊸ rc ă 1s ¨pNatres ⊸ Natrd `esqq , where d and e are variable symbols representing the values of v and w respectively. Since we directly apply add, without copying this function, the index variables a and c are bounded by 1. The type above is indeed derivable for add in dℓPCF V , assuming that the equational program E is powerful enough to express the following index terms (they all depend on the index variables b and d):

I " if b ă d then 1 else 0; J " d ´b ´1; H " d ´b; K " d ´b `1.
The derivation is given in Figure 8. We omit all the subsumption steps, but the index equalities they use are easy to check given that the number of nodes in the tree of recursive calls is Ï 0,1 b I " d `1. The final weight is equal to 3 ˆpd `1q.

Fibonacci

The Fibonacci function can easily be defined using addition:

fibo " fix f.λx. ifz x then 1 else ifz ppxq then 1 else add pf ppxqq pf ppppxqqq.

In order to derive a type for this function, we assume that the equational program allows to derive the following index (in)equalities (we later show a concrete example of such a model):

fpbq ě 2 ñ fpb `1q " fpbq ´1;

fpbq ě 2 ñ fpb `1 `b`1,1 ï b ipbqq " fpbq ´2; fpbq ě 2 ñ hpbq " hpb `1q `hpb `1 `b`1,1 ï b ipbqq ;
fpbq ď 1 ñ hpbq " 1; fpbq ě 2 ñ ipbq " 2; fpbq ď 1 ñ ipbq " 0; fpbq ě 2 ñ jpbq " 3 ¨phpb `1q `1q; fpbq ď 1 ñ jpbq " 0;

k " 0,1 ï b ipbq;
mp0, bq " fpbq ´1; mp1, bq " fpbq ´2; np0, bq " hpb `1q; np1, bq " hpbq ´hpb `1q.

We also use the previous type derivation for add with an instantiation of the variables d and e:

b; H; H $ E 3pnp0,bq`1q add : Natrnp0, bqs 1 ⊸ pNatrnp1, bqs 1 ⊸ Natrnp0, bq`np1, bqsq. The type derivation of fibo is given in Figure 9. For the sake of readability the semantic hypothesis of the subsumption derivation steps are not written, but they easily follow from the listed index equations. Subsumption steps are denoted with a dashed horizontal line between the premise and the conclusion. To apply the fixpoint derivation rule (double horizontal line, at the root of the derivation tree), the following semantic judgments have to hold:

a, b; b ă k, a ă ipbq ( E Natrmpa, bqs Ď Natrfp1 `b `b`1,a ï b ipbqqs; a, b; b ă k, a ă ipbq ( E Natrhp1 `b `b`1,a ï b ipbqqs Ď Natrnpa, bqs.
The validity of both judgments follows from the index equations we have assumed (the types are in fact pairwise equivalent). We will now delineate a model that validates those equations.

Fibonacci trees. The Fibonacci tree of size n, written T n , is defined inductively by

T 0 " Leaf 0 ; T 1 " Leaf 1 ; T n`2 " Node n`2 pT n`1 , T n q.
The usual notions on trees (leaves, descendants, right or left child, etc.) are defined in the standard way, and each node is naturally labeled by a natural number. As an example, the only node in T 1 is labeled with 1. Observe that for every n, the root of T n is labeled by n.

Consider now the Fibonacci tree of size n o P N. Its nodes are totally ordered by the usual tree preorder. We define fpbq as the label of the b th node of T no (in particular, fp0q " n o , because the preorder starts at the root), and hpbq as the number of leaves among the descendants of the b th node. We then define k as the total number of nodes in T no , and ipbq as 0 if fpbq P t0, 1u, and 2 otherwise. Please observe that ipbq is the symbol describing the tree T no as explained in Section 3.3 (in particular,

Ï b`1,1 b
ipbq is the number of descendants of the node b if it is not a leaf, and b `1 `Ïb`1,1 b ipbq is the number of its right children). We also define mpa, bq and npa, bq for a P t0, 1u by: mp0, bq " fpbq ´1; np0, bq " hpb `1q; mp1, bq " fpbq ´2; np1, bq " hpbq ´hpb `1q.

Finally, jpbq is zero if fpbq ď 1, and 3 ¨phpb `1q `1q otherwise. This model ensures the validity of all the index equations required to derive the type Natrfp0qs 1 ⊸ Natrhp0qs and the weight k `řbăk p1 `jpbqq for fibo. Notice that if fibo is applied to a natural number n o " fp0q, then the result is the number of leaves in T no , which is actually the value of the Fibonacci function in n o . In fact, the typing of the Fibonacci function has reduced the analysis of its code and its complexity to a set of first order equations that we can check semantically.

Φ o " tb ă k; fpbq ´1 ě 1u fibo " µf.λx. ifz x then 1 else `ifz ppxq then 1 else add pf ppxqq pf ppppxqqq Γ1 " t f : ra ă 1s ¨Natrmpa, bqs ⊸ Natrnpa, bqs , x : Natrfpbqs u Γ 2 " t f : ra ă 1s ¨Natrmpa `1, bqs ⊸ Natrnpa `1, bqs , x : Natrfpbqs u Γ 1 Z Γ 2 " t f : ra ă 2s ¨Natrmpa, bqs ⊸ Natrnpa, bqs , x :

The Metatheory of dℓPCF V

In this section, some metatheoretical results about dℓPCF V are presented. More specifically, type derivations are shown to be modifiable in many different ways, all of them leaving the underlying term unaltered. These manipulations, described in Section 5.1, form a basic toolkit which is essential to achieve the main results of this paper, namely intentional soundness and completeness (which are presented in Section 5.3 and Section 5.4, respectively). Types are preserved by call-by-value reduction, as proved in Section 5.2.

Manipulating Type Derivations

First of all, the constraints Φ in index, subtyping and typing judgments can be made stronger without altering the rest:

Lemma 5.1 (Strengthening) If φ; Ψ ( E Φ, then the following implica- tions hold: 1. If φ; Φ ( E I ď J, then φ; Ψ ( E I ď J; 2. If φ; Φ $ E σ Ď τ , then φ; Ψ $ E σ Ď τ ; 3. If φ; Φ; Γ $ E I t : σ, then φ; Ψ; Γ $ E I t : σ.
Proof. Point 1. is a trivial consequence of transitivity of implication in the metalogic. Point 2. can be proved by induction on the structure of the proof of φ; Φ $ E σ Ď τ , using 1. Point 3. can be proved by induction on a proof of φ; Φ; Γ $ E I t : σ, using 1 and 2. l Whatever appears on the right of $ E should hold for all values of the variables in φ satisfying Φ, so strengthening corresponds to making the judgment weaker, which is always possible. Fresh term variables can be added to the context Γ, leaving the rest of the judgment unchanged: Observe that the only hypothesis is that φ; Φ ( E I ó (see Section 3.3 for a definition): we do not require I to be a value of a that satisfies Ψ. If it is not the constraints in Φ, ΨtI{au become inconsistent, and the obtained judgments are vacuous.

Lemma

Subject Reduction

Subject Reduction is a property any reasonable type system satisfies: types should be preserved along reduction. Actually, dℓPCF V is no exception: Proposition 5.4 (Subject Reduction) If t Ñ v u and φ; Φ; H $ E M t : τ , then φ; Φ; H $ E M u : τ . Subject Reduction can be proved in a standard way, by going through a Substitution Lemma, which only needs to be proved when the term being substituted is a value. Preliminary to the Substitution Lemma are two auxiliary results stating that derivations giving types to values can, if certain conditions hold, be split into two (Lemma 5.5), or put in parametric form (Lemma 5.6):

Lemma 5.5 (Splitting) If φ; Φ; Γ $ E M v : τ 1 Z τ 2 , then there exist two indexes N 1 , N 2 , and two contexts Γ 1 , Γ 2 , such that φ; Φ; Γ i $ E N i v : τ i , and φ; Φ ( E N 1 `N2 ď M and φ; Φ $ E Γ Ď Γ 1 Z Γ 2 .
Proof. If v is a primitive integer n, the result is trivial as the only possible decomposition of a type for integers is NatrI, Js " NatrI, Js Z NatrI, Js. If v " λx.t, then its typing judgment derives from: pa, φq; pa ă I, Φq; ∆, x : σ $ E K t : τ ;

(3)

φ; Φ $ E Γ Ď ÿ aăI ∆; (4)
with τ 1 Z τ 2 " ra ă Is ¨σ ⊸ τ and M " I `řaăI K. Hence I " I 1 `I2 , and τ 1 " ra ă I 1 s ¨σ ⊸ τ , and τ 2 " ra ă I 2 s ¨σtI

φ; Φ ( E H ě Ï 0,K b I (6) pa, b, φq; pa ă I, b ă H, Φq $ E Bt0{aut Ï b`1,a b I `b `1{bu Ď A (7) pa, φq; pa ă K, Φq $ E Bt0{aut Ï 0,a b I{bu Ď C (8) φ; Φ $ E Γ Ď ř băH ∆ (9)
with τ 1 Z τ 2 " ra ă Ks ¨C, and M " H `řbăH J. Hence K " K 1 `K2 , with τ 1 " ra ă K 1 s ¨C, and τ 2 " ra ă

K 2 s ¨Cta `K1 {au. Let H 1 " Ï 0,K 1 b I and H 2 " Ï H 1 ,K 2 b I. Then H 1 `H2 " Ï 0,K b I, and H 2 is also equal to Ï 0,K 2 b
ItH 1 `b{bu. Just like the previous case, we can strengthen the hypothesis in ( 5), ( 7) and ( 8) and derive pb, φq; pb ă H 1 , Φq; ∆, x : ra ă Is ¨A $ E J t : ra ă 1s ¨B pa, b, φq;

pa ă I, b ă H 1 , Φq $ E Bt0{aut Ï b`1,a b I `b `1{bu Ď A pa, φq; pa ă K 1 , Φq $ E Bt0{aut Ï 0,a b I{bu Ď C φ; Φ; ř băH 1 ∆ $ E H 1 `řbăH 1 J fix x.t : ra ă K 1 s ¨C
Moreover, if we substitute b with b `H1 in ( 7) and we strengthen the constraints (since [START_REF] Karlbary | Resource bound certification[END_REF]

implies φ; Φ, b ă H 2 ( E Φ, b `H1 ă H), we get pa, b, φq; pa ă I, b ă H 2 , Φq $ E Bt0{aut Ï b`1,a b I`b`1{butH 1 `b{bu Ď AtH 1 `b{bu. But `Ïb`1,a b I`b`1 ˘tH 1 `b{bu " Ï H 1 `b`1,a b I`H 1 `b`1 and Ï H 1 `b`1,a b I " Ï b`1,a b pItH 1 `b{buq. Hence Bt0{aut Ï b`1,a b I `b `1{butH 1 `b{bu " BtH 1 b{but0{aut Ï b`1,a b pItH 1 `b{buq`b`1{bu.
In the same way we can substitute a with a `K1 in (8):

pa, φq; pa ă K 2 , Φq $ E Bt0{aut Ï 0,a`K 1 b I{bu Ď Cta `K1 {au. But Ï 0,a`K 1 b I " H 1 `ÏH 1 ,a b I " H 1 `Ï0,a b ItH 1 `b{bu, and then Bt0{aut Ï 0,a`K 1 b I{bu is equivalent to BtH 1 `b{but0{aut Ï 0,a b ItH 1 `b{bu{bu.
Finally, by substituting also b with b `H1 in (5) we can derive pb, φq ; pb ă H 2 , Φq ; ∆tH 1 `b{bu , x : pra ă Is ¨AqtH 1 `b{bu $ E JtH 1 `b{bu t : ra ă 1s ¨BtH 1 `b{bu pa, b, φq

; pa ă I, b ă H 2 , Φq $ E BtH 1 `b{but0{aut Ï b`1,a b pItH 1 `b{buq `b `1{bu Ď AtH 1 `b{bu pa, φq ; pa ă K 2 , Φq $ E BtH 1 `b{but0{aut Ï 0,a b ItH 1 `b{bu{bu Ď Cta `K1 {au φ ; Φ ; ř băH 2 ∆tH 1 `b{bu $ E H 2 `řbăH 2 JtH 1 `b{bu fix x.t : ra ă K 2 s ¨Cta `K1 {au
Thus we can conclude with Γ 1 "

ř aăH 1 ∆, Γ 2 " ř aăH 2 ∆ta `H1 {au, N 1 " H 1 `řaăH 1 J and N 2 " H 2 `řaăH 2 Jta `H1 {au. l
If splitting tells us that that the sum of two types can be split, parametric splitting allows to handle bounded sums:

Lemma 5.6 (Parametric Splitting) If φ; Φ; Γ $ E M v :
ř căJ σ is derivable, then there exist an index N and a context ∆ such that one can derive c, φ; c ă J, Φ; ∆ $ E N v : σ, and φ;

Φ ( E ř căJ N ď M and φ; Φ $ E Γ Ď ř căJ ∆.
Proof. The proof uses the same technique as for Lemma 5.5. If v is a lambda abstraction or a fixpoint, then ř căJ σ is on the form ra ă ř căJ Ls¨C, where ra ă Ls ¨Cta `řdăc Ltd{cu{au " σ. Then the result also follows from Strengthening (Lemma 5.1) and Index Substitution (Lemma 5.3): for the lambda abstraction, substitute a with a `řdăc Ltd{cu in [START_REF] Sabelfeld | Language-based information-flow security[END_REF] 5) and ( 7), and substitute a with a `řdăc Ltd{cu in [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF] to derive the result. l

One can already realize why these results are crucial for subject reduction: whenever the substituted value flows through a type derivation, there are various places where its type changes, namely when it reaches instances of the typing rules pAppq, p⊸q, pIfq and pRecq: in all these cases the type derivation for the value must be modified, and the splitting lemmas certify that this is possible, indeed. We can this way reach the key intermediate result:

Lemma 5.7 (Substitution) If φ; Φ; Γ, x : σ $ E M t : τ and φ; Φ; H $ E N v : σ are both derivable, then there is an index K such that φ; Φ; Γ $ E K trx :" vs : τ and φ; Φ ( E K ď M `N.

Proof. The proof goes by induction on the derivation of the typing judgment φ; Φ; Γ, x : σ $ E M t : τ , making intense use of Lemma 5.5 and Lemma 5.6. l Given Lemma 5.7, proving Proposition 5.4 is routine: the only two nontrivial cases are those where the fired redex is a β-redex or the unfolding of a recursively-defined function, and both consist in a substitution. Observe how Subject Reduction already embeds a form of extensional soundness for dℓPCF V : simply, types are preserved by reduction. As an example, if one builds a type derivation for $ E I t : Natr2, 7s, then the normal form of t (if it exists) is guaranteed to be a constant between 2 and 7. Observe, on the other hand, that nothing is known about the complexity of the underlying computational process yet, since the weight I does not necessarily decrease along reduction, although it cannot increase. In which sense, then, I is a measure of the complexity of evaluating the underlying term t? This is the topic of the following section.

Intentional Soundness

In this section, we prove the following result: Roughly speaking, this means that dℓPCF V also gives us some sensible information about the time complexity of evaluating typable PCF programs. The path towards Theorem 5.8 is not straightforward: it is necessary to lift dℓPCF V to a type system for closures, environments and processes, as defined in Section 3.2. Actually, the type system can be easily generalized to closures by the rule below:

φ; Φ $ E σ Ď τ φ; Φ ( E I ó φ; Φ $ E I ˛: pσ, τ q φ; Φ $ E J c : σt0{au φ; Φ $ E K ρ : pτ t0{au, ϕq φ; Φ ( E I " J `K φ; Φ $ E I argpc , ρq : pra ă 1s ¨pσ ⊸ τ q, ϕq φ; Φ $ E J v : ra ă 1s ¨pσ ⊸ τ q φ; Φ $ E K ρ : pτ t0{au, ϕq φ; Φ ( E I " J`K φ; Φ $ E I funpv , ρq : pσt0{au, ϕq φ; N " 0, Φ $ E J x t ; ξ y : σ φ; M ě 1, Φ $ E J x u ; ξ y : σ φ; Φ $ E K ρ : pσ, τ q φ; Φ ( E I " J `K φ; Φ $ E I forkpt , u , ξ , ρq : pNatrM, Ns, τ q φ; Φ $ E I π : pNatrM `1, N `1s, τ q φ; Φ $ E I spπq : pNatrM, Ns, τ q φ; Φ $ E I π : pNatrM ´1, N ´1s, τ q φ; Φ $ E I ppπq : pNatrM, Ns, τ q
φ; Φ; x 1 : σ 1 , . . . , x n : σ n $ E K t : τ φ; Φ $ E J i v i : σ i (for all iq φ; Φ ( E I " K `řiďn J i φ; Φ $ E I x t ; tx 1 Þ Ñ v 1 ; ¨¨¨; x n Þ Ñ v n u y : τ
We might write φ; Φ $ E J ξ : Γ when Γ " x 1 : σ 1 , . . . , x n : σ n and ξ " tx 1 Þ Ñ v 1 ; ¨¨¨; x n Þ Ñ v n u and J " pJ 1 , . . . , J n q and, for every i ď n, φ; Φ $ E J i v i : σ i . Hence the typing rule for a closure can also be written:

φ; Φ; Γ $ E K t : τ φ; Φ $ E J ξ : Γ φ; Φ ( E I " K `ř J φ; Φ $ E I x t ; ξ y : τ
Lifting everything to stacks, on the other hand, requires more work (see Figure 10). We say that a stack π is pφ; Φq-acceptable for σ with type τ and cost I (notation: φ; Φ $ E I π : pσ, τ q) when it interacts well with closures of type σ to produce a process of type τ . Finally, a process can be typed as follows:

φ; Φ $ E K c : σ φ; Φ $ E J π : pσ, τ q φ; Φ ( E I " K `J φ; Φ $ E I c
‹ π : τ This lifted type system is sound w.r.t. subtyping: Lemma 5.9 (Subtyping is Derivable) 1. The following typing rule for closures is derivable:

φ; Φ $ E I c : σ φ; Φ ( E I ď J φ; Φ $ E σ Ď τ φ; Φ $ E J c : τ 2.
The following typing rule for stacks is derivable:

φ; Φ $ E I π : pσ, τ q φ; Φ $ E ̺ Ď σ φ; Φ $ E τ Ď ϕ φ; Φ ( E I ď J φ; Φ $ E J π : p̺, ϕq 3.
The following typing rule for processes is derivable:

φ; Φ $ E I P : σ φ; Φ ( E I ď J φ; Φ $ E σ Ď τ φ; Φ $ E J P : τ
Proof. The first point directly follows from the typing rule Subs for terms.

The second one is proved by induction on the stack typing derivation, using 1.

The last point follows from the first two. l

In the meantime, the notion of weight has been lifted to processes too, with the hope that it strictly decreases at every evaluation step. Unfortunately, this does not hold: sometimes, evaluation leaves the weight of a process unchanged. However, in that case another parameter is guaranteed to decrease, namely the process size. The size |P| of a process P " c ‹ π is defined as |c| `|π|, where:

• The size |c| of a closure x t ; ξ y is the multiplicative size of t (see Section 3.1). • The size of |π| is the sum of the sizes of all closures appearing in π plus the number of occurrences of symbols (different from ˛and fun) in π.

Term Multiplicative Size }x} " 2; }n} " }λx.t} " } fix x.t} " 0; }tu} " }t} `}u} `2;

}sptq} " }pptq} " }t} `2; } ifz t then u else s} " }t} `}u} `}s} `2; The formal definition of |c ‹ π| is in Figure 11. The size of a process decreases by any evaluation steps, except the ones performing a substitution (1) and (2). However, these two reduction rules make the weight of a process to decrease, as formalized by the following proposition. By the way, these are the cases in which a box is opened up in the underlying linear logic proof. Proof. First, if P ą R with a non substitution rule (any rule of Figure 4 or Figure 5 except (1) and ( 2)), then it is easy to check that |P| ą |R|. Moreover, in all these cases P and R have the same type and the same weight. We detail some cases:

Closure

• If P " v ‹ argpc , πq ą c ‹ funpv , πq " R, then the typing of P derives from φ; Φ ( E I " J `K φ; Φ $ E K v : ra ă 1s ¨pσ 0 ⊸ τ 0 q φ; Φ $ E H c : σ 0 t0{au φ; Φ $ E L π : pτ 0 t0{au, τ q φ; Φ ( E J " H `L φ; Φ $ E J argpc , πq : pra ă 1s ¨pσ 0 ⊸ τ 0 q, τ q φ; Φ $ E I v ‹ argpc , πq : τ Hence we can derive for R: φ; Φ ( E I " H `L `K φ; Φ $ E H c : σ 0 t0{au φ; Φ $ E K v : ra ă 1s ¨pσ 0 ⊸ τ 0 q φ; Φ $ E L π : pτ 0 t0{au, τ q φ; Φ $ E L`K funpv , πq : pσ 0 t0{au, τ q φ; Φ $ E I c ‹ funpv , πq : τ • If P " x tu ; ξ y ‹ π ą x t ; ξ y ‹ argpx u ; ξ y , πq " R, then the typing of P derives from φ; Φ; Γ 1 $ E K 1 t:raă1s¨σ0⊸τ0 φ; Φ; Γ 2 $ E K 2 u:σ0t0{au φ;Φ;Γ1ZΓ2$ E K 1 `K2 tu:τ0t0{au φ; Φ $ E ∆ĎΓ1ZΓ2 φ; Φ $ E σĎτ0t0{au φ; Φ ( E K1`K2ďH φ;Φ;∆$ E H tu:σ φ;Φ $ E J ξ:∆ φ;Φ ( E H`ř J"H1 φ;Φ$ E H 1 x tu ; ξ y:σ φ;Φ $ E L π:pσ,τ q φ;Φ ( E I"L`H1 φ;Φ$ E I x tu ; ξ y ‹ π:τ
In particular, since subtyping is derivable for closures (Lemma 5.9), φ; Φ $ E J ξ : Γ 1 Z Γ 2 . By Lemma 5.5 (that can be trivially extended to closures), it means that there are some vectors of indexes M, N such that

φ; Φ $ E M ξ : Γ 1 φ; Φ $ E N ξ : Γ 2 φ; Φ ( E M `N " J
(where, as usual, the sum of vectors has to be understood componentwise). In the same way, since subtyping is derivable for stacks (Lemma 5.9), then φ; Φ $ E L π : pσ, τ q and φ;

Φ $ E σ Ď τ 0 t0{au entail φ; Φ $ E L π : pτ 0 t0{au, τ q
Hence we can derive:

φ;Φ;Γ 1 $ E K 1 t:raă1s¨σ 0 ⊸τ 0 φ;Φ $ E M ξ:Γ 1 φ;Φ$ E K 1 `ř M x t ; ξ y:raă1s¨σ 0 ⊸τ 0 φ;Φ;Γ 2 $ E K 2 u:σ 0 t0{au φ;Φ $ E N ξ:Γ 2 φ;Φ$ E K 2 `ř N x u ; ξ y:σ 0 t0{au φ;Φ$ E L π:pτ 0 t0{au,τ q φ;Φ$ E L`K 2 `ř N argpx u ; ξ y , πq:praă1s¨σ 0 ⊸τ 0 ,τ q φ;Φ$ E K 1 `ř M`L`K 2 `ř N x t ; ξ y ‹ argpx u ; ξ y , πq:τ
Finally we can conclude that φ; Φ $ E I R : τ with Lemma 5.9 since φ; Φ ( E I ě L `K1 `K2 `ř M `ř N. Now, if P ą R with a substitution rule (1) or ( 2), then the weight of P is strictly higher than the one of R:

• If P " v ‹ funpx λx.t ; ξ y , πq and R " x t ; px Þ Ñ vq ¨ξ y ‹ π, then the typing of P comes from a derivation of the form: Lemma 5.3). Hence we can derive:

φ; Φ $ E K v : σt0{au a, φ; a ă 1, Φ; Γ, x : σ $ E M t : σ 1 φ; Φ; Γ $ E 1`Mt0{au λx.t : ra ă 1s ¨pσ ⊸ σ 1 q φ; Φ $ E J ξ : Γ φ; Φ $ E 1`Mt0{au`ř J x λx.t ; ξ y : ra ă 1s ¨pσ ⊸ σ 1 q φ; Φ $ E H π : pσ 1 t0{au, τ q φ; Φ $ E 1`Mt0{au`ř J`H funpx λx.t ; ξ y , πq : pσt0{au, τ q φ; Φ $ E I v ‹ funpx λx.t ; ξ y , πq : τ (with φ; Φ ( E K `1 `Mt0{au `ř J `H " I). If a, φ; a ă 1, Φ; Γ, x : σ $ E M t : σ 1 is derivable, then φ; Φ; Γ, x : σt0{au $ E Mt0{au t : σ 1 t0{au is derivable too (see
φ; Φ; Γ, x : σt0{au $ E Mt0{au t : σ 1 t0{au φ; Φ $ E J ξ : Γ φ; Φ $ E K v : σt0{au φ; Φ $ E Mt0{au`ř J`K x t ; px Þ Ñ vq ¨ξ y : σ 1 t0{au φ; Φ $ E H π : pσ 1 t0{au, τ q φ; Φ $ E J x t ; px Þ Ñ vq ¨ξ y ‹ π : τ (with φ; Φ ( E J " K `Mt0{au `ř J `H,
x t ; H y ‹ ˛ą˚x v ; H y ‹ ˛.
By Proposition 5.10, it means that x v ; H y ‹ ˛has type NatrI, Js, and so has v. So we can conclude that v is a natural number in the interval r I E ; J E s.

(Relative) Completeness

In this section, we will prove some results about the expressive power of dℓPCF V , seen as a tool to prove intentional (but also extensional) properties of PCF terms. Actually, dℓPCF V is extremely powerful: every first-order PCF program computing the function f : N Ñ N in a number of steps bounded by g : N Ñ N can be proved to enjoy these properties by way of dℓPCF V , provided two conditions are satisfied: • On the one hand, the equational program E needs to be universal, meaning that every partial recursive function is expressible by some index terms. This can be guaranteed, as an example, by the presence of a universal program in E. • On the other hand, all true statements in the form φ; Φ ( E I ď J must be "available" in the type system for completeness to hold. In other words, one cannot assume that those judgments are derived in a given (recursively enumerable) formal system, because this would violate Gödel's Incompleteness Theorem. In fact, our completeness theorems are relative to an oracle for the truth of those assumptions, which is precisely what happens in similar results for Floyd-Hoare logics [START_REF] Cook | Soundness and completeness of an axiom system for program verification[END_REF].

PCF Typing. The first step towards completeness is quite easy: propositional type systems in the style of PCF for terms, closures, stacks and processes need to be introduced. All of them can be easily obtained by erasing the index information from dℓPCF V . As an example, the typing rule for the application looks like Γ $ PCF t : α ñ β Γ $ PCF u : α Γ $ PCF tu : β while processes can be typed by the following rule

$ PCF π : pα, βq $ PCF c : α $ PCF c ‹ π : β
Given any type σ (respectively, any type derivation δ) of dℓPCF V , the PCF type (respectively, the PCF type derivation) obtained by erasing all the index information will be denoted by p|σ|q (respectively, by p|δ|q). Of course both terms and processes enjoy subject reduction theorems with respect to PCF typing, and their proofs are much simpler than those for dℓPCF V . As an example, given a type derivation δ for $ PCF P : Nat (we might write δ ⊲ $ PCF P : Nat) and P ą R, a type derivation γ for $ PCF R : Nat can be easily built by manipulating in a standard way δ; we write δ ą γ.

Weighted Subject Expansion. The key ingredient for completeness is a dualisation of Weighted Subject Reduction: Proposition 5.12 (Weighted Subject Expansion) Suppose that δ ⊲ $ PCF P : α, that δ ą γ, and that ǫ ⊲ φ; Φ $ E I R : τ where p|ǫ|q " γ. Then there is θ ⊲ φ; Φ $ E J P : τ with p|θ|q " δ and φ; Φ ( E J ď I `1. Moreover, θ can be effectively computed from δ, ǫ and γ.

Proving Proposition 5.12 requires a careful analysis of the evolution of the CEK PCF machine, similarly to what happened for Weighted Subject Reduction. But while in the latter it is crucial to be able to (parametrically) split type derivations for terms (and thus closures), here we need to be able to join them:

Lemma 5.13 (Joining) Suppose E is universal. If δ i ⊲ φ; Φ; Γ i $ E N i v : τ i , p|δ 1 |q " p|δ 2 |q, φ; Φ $ E Γ Ď Γ 1 Z Γ 2 , φ; Φ $ E τ 1 Z τ 2 Ď τ and φ; Φ ( E N 1 `N2 ď M, then φ; Φ; Γ $ E M v : τ . Lemma 5.14 (Parametric Joining) Suppose that E is universal. If a, φ; a ă I, Φ; ∆ $ E N v : σ, φ; Φ $ E Γ Ď ř aăI ∆, φ; Φ $ E ř aăI σ Ď τ and φ; Φ ( E ř aăI N ď M, then φ; Φ; Γ $ E M v : τ .
Observe that the Joining Lemma requires the two type derivations to be joined to have the same PCF "skeleton". This is essential, because otherwise it would not be possible to unify them into one single type derivation.

Completeness for Programs. We now have all the necessary ingredients to obtain a first completeness result, namely one about programs (which are terms of type Nat). Suppose that t is a PCF program and that t Ñ v m, where m is a natural number. By Proposition 3.1, there is a sequence of processes P 1 ą P 2 ą . . . ą P n ,

where P 1 " px t ; H y ‹ ˛q and P n " px m ; H y ‹ ˛q. Of course, $ PCF P i : Nat for every i. For obvious reasons, $ E 0 P n : Natrms. Moreover, by Weighted Subject Expansion, we can derive each of $ E I i P i : Natrms, until we reach $ E I 1 P 1 : Natrms, where I 1 ď n. See Figure 12 for a graphical representation of the above argument. It should be now clear that one can reach the following: Theorem 5.15 (Completeness for Programs) Suppose that $ PCF t : Nat, that t ó n m and that E is universal. Then, $ E k t : Natrms, where k ď n. Uniformization and Completeness for Functions. Completeness for programs, however, is not satisfactory: the fact (normalizing) PCF terms of type Nat can all be analyzed by dℓPCF V is not so surprising, and other type systems (like non-idempotent intersection types [START_REF] Carvalho | Execution time of lambda-terms via denotational semantics and intersection types[END_REF]) have comparable expressive power. Suppose we want to generalize relative completeness to first-order functions: we would like to prove that every term t having a PCF type Nat ñ Nat (which terminates when fed with any natural number) can be typed in dℓPCF V . How could we proceed? First of all, observe that the argument in Figure 12 could be applied to all instances of t, namely to all terms in tt n | n P Nu. This way one can obtain, for every n P N, a type derivation δ n for

$ E

In t : ra ă J n s ¨NatrK n s ⊸ NatrH n s, where J n can be assumed to be 1, while K n can be assumed to be n. Moreover, the problem of obtaining δ n from n is recursive, i.e., can be solved by an algorithm. Surprisingly, the infinitely many type derivations in tδ n | n P Nu can be turned into one:

δ 1 ⊲ $ PCF P 1 : Nat θ 1 ⊲ $ E I 1 P 1 : Natrms δ 2 ⊲ $ PCF P 2 : Nat θ 2 ⊲ $ E I 2 P 2 : Natrms O O δ n´1 ⊲ $ PCF P n´1 : Nat θ n´1 ⊲ $ E I n´1 R n´1 : Natrms O O δ n ⊲ $ PCF P n : Nat θ n ⊲ $ E In P n : Natrms O O
Proposition 5.16 (Uniformization of Type Derivations) Suppose that E is universal and that tδ n u nPN is a recursively enumerable collection of type derivations satisfying the following constraints: 1. For every n P N, δ n ⊲ $ E In t : σ n ; 2. all derivations in tδ n u nPN have the same skeleton, i.e., for every n, m P N, p|δ n |q " p|δ m |q. Then there is a type derivation θ ⊲ a; H; H $ E I t : σ such that ( E Itn{au " I n and ( E σtn{au " σ n for all n.

Proof. The proof proceeds by first proving three lemmas:

• First of all, one can prove that any family of semantic judgment in the form t( E Itn{au " Jtn{auu nPN can be turned into one semantic judgment ( E I " J. • Then, it is possible to uniformize index terms themselves: if tI n u nPN is a family of index terms, then there is one index term I such that ( E Itn{au -I n .

• Subtyping judgments can be made uniform themselves. The three lemmas are exactly the necessary ingredients to carry out an induction on the structure of any δ n (they all have the same structure, anyway).

For more details, one can consult [START_REF] Lago | Linear dependent types and relative completeness[END_REF]. l

Uniformization of type derivations should be seen as an extreme form of joining: not only a finite number of type derivations for the same term can be unified into one, but any recursively enumerable class of them can. Again, the universality of E is crucial here. We are now ready to give the following: Theorem 5.17 (Completeness for Functions) Suppose that $ PCF t : Nat ñ Nat, that t n ó kn m n for all n P N and that E is universal. Then, there are index terms I and H such that a; H; H $ E I t : rb ă 1s ¨Natras ⊸ NatrHs, where ( E Itn{au ď k n and ( E Htn{au " m n .

Weight and Time Complexity

The intensional soundness and relative completeness results show a tight relation between the weight of a program and its evaluation time in the CEK PCF machine. Notice that, because of the subsumption typing rule, the weight of a term can be arbitrarily increased. However, the following corollary emphasizes that the lowest weight that can be associated to a program provides a rather tight bound of its complexity. Actually, the minimum weight of a program t represents the number of substitutions in its cbv evaluation or, formally, the number of steps of kind (1) or (2) in its evaluation by the CEK PCF machine (Remark 5.1). It is thus a lower bound on its time complexity in CEK PCF . Between two such substitution steps, the machine only scans the term to reach the head subterm (or to select one branch of the test for zero, when a fork rule is applied). At most |t| scanning steps can be done consecutively (during the evaluation, the machine only contains subterms2 of the initial term t), and so the total number of steps is bounded by the weight multiplied by |t|.

Perspectives and Developments

6.1. dℓPCF V , dℓPCF N and their Peculiarities In this section, we briefly describe in which senses dℓPCF V , the type system we introduce here, differs from dℓPCF N [START_REF] Lago | Linear dependent types and relative completeness[END_REF].

As already pointed out in Section 2.2, in dℓPCF N all arguments to functions are marked as duplicable, while in dℓPCF V the same role is played by functions themselves. This, coupled with linear dependency, implies that:

• When typing a term t in dℓPCF N any subterm u of t which can potentially be used as an argument to a function is typed parametrically on an index variable a, each value of a corresponding to a possible "use" of u; • If t is typed in dℓPCF V , the same holds for any λ-abstraction λx.u in t:

all possible uses of λx.u need to be taken into account in the underlying type if we want the latter to be precise and, ultimately, if we care about relative completeness. Saying it another way, both dℓPCF N and dℓPCF V are non-modular, in that the way one attributes a type (and ultimately a weight) to certain subterms can possibly depend on how they are used by the environment. This is indeed true if one builds a type derivation by way of a fixed (maybe weak) equational program. Typing a term and defining the underlying equational program at the same time, leaving some of the index terms unspecified, is a way to alleviate this problem, and is actually the main idea behind a linear dependent type inference algorithm [START_REF] Lago | The geometry of types[END_REF].

Technically, the metatheory of dℓPCF V can be explored with tools similar to those employed in dℓPCF N . However, the authors claim that most results about the former system, soundness and completeness in primis, are not easy consequences of the one enjoyed by the latter. An example are splitting lemmas, which are much easier to be proved in dℓPCF N (see [START_REF] Lago | Linear dependent types and relative completeness[END_REF] for more details).

Further Developments

Relative completeness of dℓPCF V , especially in its stronger form (Theorem 5.17) can be read as follows. Suppose that a sound, finitary formal system C deriving judgments in the form φ; Φ $ E I ď J is fixed and "plugged" into dℓPCF V . What you obtain is a sound, but necessarily incomplete formal system, due to Gödel's incompleteness. However, this incompleteness is only due to C and not to the rules of dℓPCF V , which are designed so as to reduce the problem of proving properties of programs to checking inequalities over E without any loss of information.

In this scenario, it is of paramount importance to devise techniques to automatically reduce the problem of checking whether a program satisfies a given intentional or extensional specification to the problem of checking whether a given set of inequalities over an equational program E holds. Indeed, many techniques and concrete tools are available for the latter problem (take, as an example, the immense literature on SMT solving), while the same cannot be said about the former problem. The situation, in a sense, is similar to the one in the realm of program logics for imperative programs, where logics are indeed very powerful [START_REF] Cook | Soundness and completeness of an axiom system for program verification[END_REF], and great effort have been directed to devise efficient algorithms generating weakest preconditions [START_REF] De Bakker | Mathematical theory of program correctness[END_REF].

Actually, at the time of writing, the authors are actively involved in the implementation of relative type inference algorithms for both dℓPCF N and dℓPCF V , which can be seen as having the same role as algorithms computing weakest preconditions. Efficient type inference algorithms can indeed be defined [START_REF] Lago | The geometry of types[END_REF]: the idea is to start with a PCF type derivation and decorate it with index terms, defining an appropriate equational program along the way. A detailed description of the type inference process is however outside the scope of this paper.

Related Work

Complexity analysis of higher-order programs has been (and continues to be) an object of study in the programming language research community.

Among the many works in this direction, we can mention the proposals for type systems for the λ-calculus characterizing in an extensional sense, e.g. polynomial time computable functions. Many of these techniques can be seen as static analysis methodologies: once a program is assigned a type, an upper bound to its time complexity is relatively easy to be synthesized. The problem with these systems, however, is that they are usually very weak from an intentional point of view: the class of typable programs is quite restricted.

More powerful static analysis methodologies can actually be devised. All of them, however, are either limited to very specific forms of resource bounds or to a peculiar form of higher-order functions or else they do not get rid of higher-order as the underlying logic. Consider, as an example, one of the earliest work in this direction, namely Sands's system of cost closures [START_REF] Sands | Complexity analysis for a lazy higher-order language[END_REF]: the class of programs that can be handled includes the full lazy λ-calculus, but the way complexity is reasoned about remains genuinely higher-order, being based on closures and contexts. In Benzinger's framework [START_REF] Benzinger | Automated higher-order complexity analysis[END_REF] higherorder programs are translated into higher-order equations, and the latter are turned into first-order ones; both steps, and in particular the second one, are not completeness-preserving. More generally, there is an inherent risk in doing program analysis by way of program transformation (see [START_REF] Rosendahl | Automatic complexity analysis[END_REF][START_REF] Danner | A static cost analysis for a higherorder language[END_REF]): if the automatic analysis of the transformed program fails, one is left with an unintelligible piece of code, which can hardly be analyzed manually or semi-automatically. In this respect, type systems constitute a very good compromise.

Recent works on amortized resource analysis are either limited to firstorder programs [START_REF] Hoffmann | Multivariate Amortized Resource Analysis[END_REF] or to linear bounds [START_REF] Jost | Static Determination of Quantitative Resource Usage for Higher-Order Programs[END_REF]. A recent proposal by Amadio and Régis-Gianas [START_REF] Ayache | Certifying and reasoning on cost annotations in c programs[END_REF] allows to reason on the the cost of higher-order functional programs by way of so-called cost-annotations, being sure that the actual behavior of compiled code somehow reflects the annotation. The logic in which cost annotations are written, however, is a higher-order Hoare logic. None of the proposed systems, on the other hand, are known to be (relatively) complete in the sense we use here.

Complexity analysis of first-order functional programs, or of programs written in other programming paradigms is a much more developed research area. Examples are the work by Crary And Weirich [START_REF] Crary | Resource bound certification[END_REF] or the SPEED project [START_REF] Gulwani | Speed: Symbolic complexity bound analysis[END_REF] Linear dependency can be seen as a way to turn games and strategies into types, this way facilitating verification. A recent work going in the same direction is Geometry of Synthesis, in particular when the latter is supported by type systems [START_REF] Ghica | Geometry of synthesis III: resource management through type inference[END_REF].

dℓPCF V and Implicit Complexity

There is a price to pay for the kind of relative completeness dℓPCF V (and dℓPCF N ) enjoys: checking a type derivation for correctness is undecidable in general, simply because it relies on semantic assumptions in the form of inequalities between index terms, or on subtyping judgments, which themselves rely on the properties of the underlying equational program E. Indeed, dℓPCF V should not be thought of as a type system, but rather as a framework in which various distinct type systems can be defined. Concrete type systems can be crafted by either instantiating E, or by choosing specific and sound formal systems for the verification of semantic assumptions. By the way, the just described problem is not peculiar to dℓPCF V : Floyd-Hoare program logics are themselves undecidable.

The main motivation behind the introduction of linear dependent types comes from implicit computational complexity. Traditionally, what prevents (most) ICC techniques to find concrete applications along this line is their poor expressive power: the class of programs which can be recognized as being efficient by (tools derived from) ICC systems is often very small and does not include programs corresponding to natural, well-known algorithms. In this respect, dℓPCF N and dℓPCF V are fundamentally different: all PCF programs with a certain complexity can be proved to be so by deriving a typing judgment for them.

Conclusions

Linear dependent types are shown to be applicable to the analysis of intentional and extensional properties of functional programs when the latter are call-by-value evaluated. More specifically, soundness and relative completeness results are proved for both programs and functions. This generalizes previous work by Gaboardi and the first author [START_REF] Lago | Linear dependent types and relative completeness[END_REF], who proved similar results in the call-by-name setting. This paper shows that linear dependency not only provides an expressive formalism, but is also robust enough to be adaptable to calculi whose notions of reduction are significantly different (and in many cases more efficient) than normal order evaluation.

Topics for future work include some further analysis about the applicability of linear dependent types to languages with more features, including some form of inductive data types, or ground type references. Another interesting problem is tuning linear dependent types in such a way as to capture the complexity of call-by-need evaluation.

Figure 1 :

 1 Figure 1: Call-by-value Reduction Rules for PCF terms.

Figure 2 :

 2 Figure 2: Closure Reduction Rules of PCF terms.

Figure 3 :

 3 Figure 3: PCF Typing Rules.

Figure 4 :

 4 Figure 4: CEK PCF Evaluation Rules for Value Closures.

Figure 5 :

 5 Figure 5: CEK PCF Contextual Evaluation Rules.

Figure 6 :

 6 Figure 6: Subtyping Derivation Rules of dℓPCF V .

Figure 7 :

 7 Figure 7: Typing Rules of dℓPCF V .

1 ⊸ pNatrnp1, bqs 1 ⊸ 1 ⊸ 1 ⊸Figure 9 :

 11119 Figure 9: A type derivation for fibo.

  For the fixpoint consider the index H 1 satisfying the equations H 1 t0{cu " Ï 0,Lt0{cu b I and H 1 ti `1{cu " Ï Hti{cu,Lti`1{cu b I. Then substitute b with b `řdăc H 1 td{cu (and add the constraint c ă J in the context) in (

Figure 10 :

 10 Figure 10: dℓPCF V : Lifting Typing to Stacks

Figure 11 :

 11 Figure 11: Size of Processes.

Proposition 5 . 10 (

 510 Weighted Subject Reduction) Assume P ą R and φ; Φ $ E I P : τ . Then φ; Φ $ E J R : τ and: • either φ; Φ ( E I " J and |P| ą |R|, • or φ; Φ ( E I ą J and |P| `|s| ą |R|, where s is a term appearing in P.

Figure 12 :

 12 Figure 12: Completeness for programs, sketch of the Proof.

Corollary 5 . 18

 518 Assume t is a PCF program that evaluates to m with n steps in the CEK PCF , and E is a universal equational program. Then one can derive $ E k t : Natrms in dℓPCF V , with k ď n ď k ¨|t|. Proof. The typing judgment with the lower bound k ď n are given by Theorem 5.15. The upper bound n ď k ¨|t| follows from Theorem 5.8. l

  Proof. 1. Assume that φ; Φ ( E I ó and pa, φq; Φ, Ψ ( E J ď K, and let ρ be an assignment satisfying Φ, ΨtI{au. In particular, ρ satisfies Φ, thus I E ρ is defined, say equal to n. For any index H, HtI{au E ρ " H E ρ,aÞ Ñn . Hence pρ, a Þ Ñ nq satisfies Φ, Ψ, and then it also satisfies J ď K. So JtI{au E ρ " J E ρ,aÞ Ñn ď K E ρ,aÞ Ñn " KtI{au E ρ , and ρ satisfies JtI{au ď KtI{au. Thus φ; Φ, ΨtI{au ( E JtI{au ď KtI{au. 2. By induction on the subtyping derivation, using 1. 3. By induction on the typing derivation, using 1. and 2. l

	Lemma 5.3 (Index Substitution) If φ; Φ ( E I ó, then the following im-
	plications hold:
	1. If pa, φq; Φ, Ψ (
	Proof. Again, this is an induction on the structure of a derivation for
	φ; Φ; Γ $ E I t : τ .	l
	Please note that ∆ is completely arbitrary. Another useful transformation on
	type derivations consists in substituting index variables for (defined) index
	terms.

5.2 (Context Weakening) φ; Φ; Γ $ E I t : τ implies φ; Φ; Γ, ∆ $ E I t : τ . E J ď K, then φ; Φ, ΨtI{au ( E JtI{au ď KtI{au; 2. If pa, φq; Φ, Ψ $ E σ Ď τ , then φ; Φ, ΨtI{au $ E σtI{au Ď τ tI{au; 3. If pa, φq; Φ, Ψ; Γ $ E J t : σ, then φ; Φ, ΨtI{au; ΓtI{au $ E JtI{au t : σtI{au.

  Size |x t ; ξ y| " }t};

	Stack Size
	| ˛| " 0;	|funpv , πq| " |v| `|π|;
	|spπq| " |ppπq| " |π| `1;	|argpc , πq| " |c| `|π| `1;
	|forkpt , u , ξ , πq| " }t} `}u} `|π| `1;
	Process Size
	|c ‹ π| " |c| `|π|.

  and thus φ; Φ ( E J " I ´1). Moreover, |P| " |v| `}λx.t} `|π| " |v| `|π|, while |R| " }t} `|π|. Hence, |P| `|t| ě |R| (as |u| ě }u} for any term u). The proof of this theorem formalizes the intuition that the weight of a program is the number of substitutions performed during its cbv evaluation. More precisely, if a typed process P has weight I and P ą R, then R can be typed with weight J such that• J " I ´1 if P ą R is a substitution step (1) or (2), • J " I otherwise.The weight of a process is thus an upper bound on the number of substitution steps in its evaluation. Corollary 5.11 Let P " x t ; H y ‹ ˛and |t| " m. If φ; Φ $ E I P : τ and P ą n R, then φ; Φ $ E J R : τ , and φ; Φ ( E pI ´J `1q ˆm ě n. Proof. First observe that if P ą ˚S then any term s appearing in S is either a subterm of t or a natural number n, and thus |s| ď m. Hence by induction on n we can prove using Proposition 5.10 that P ą n R implies n ď |P| ´|R| `p I E ρ ´ J E ρ q ¨|t| for any valuation ρ defined on φ and satisfying Φ. Then we can conclude since |P| " m and |R| ě 0. l Given Corollary 5.11, Theorem 5.8 is within reach: if $ E H t : NatrI, Js then x t ; H y ‹ ˛terminates in at most p H E ρ `1q ¨|t| steps in the CEK PCF , since weights cannot be negative. It reaches an irreducible process, that is a value closure together with an empty stack:

	l
	Splitting and parametric splitting play a crucial role here, once appropriately
	generalized to value closures.
	Remark 5.1

Email addresses: dallago@cs.unibo.it (Ugo Dal Lago), barbara.petit@inria.fr (Barbara Petit) This is a revised and extended version of a paper which appeared in the proceedings of PPDP 2012 Preprint submitted to ElsevierDecember 5, 2014

To claim this, we formally need to consider an extension of the subterm relation where all natural numbers n are equivalent.

A " Natr Js ⊸ rc ă 1s ¨pNatres ⊸ NatrJ `esq C " NatrHs ⊸ rc ă 1s ¨pNatres ⊸ NatrH `esq Γ " tx : ra ă Is ¨A, y :


Mohamad Hamieh
email: mohamad.hamieh@ensea.fr

Myriam Ariaudo
email: myriam.ariaudo@ensea.fr

Sizing of the Physical Layer of a RF Intra-Chip Communications

Keywords: RF-NoC, OFDMA modulation, Transmission optimization

In this paper we size a RF intra-chip communications based on Orthogonal Frequency Division Multiple Access (OFDMA) modulation which allows data rate and message recipient reconfiguration. Firstly, we present the advantages of this modulation such as providing flexible and high-speed data transmission. Then, we study the impact of the RF-interconnect channel shape on the transmission in terms of required transmission power. Finally, we present the effect of the channel composed of the line and its multiple access on the transfer of information and we perform a channel equalization to overcome this undesired effect.

I. INTRODUCTION

The technological progress in the design of system on Chip (SoC) is to integrate a very large number of processing elements and memories on a single chip leading to the rise of MultiProcessor System on Chip (MPSoC). Such an advanced integration allows to envisage powerful electronic systems that may offer a large number of services such as high bit rate, high speed transmission, etc. However these architectures put up new challenges for the interconnections between the processing units. The scaling up will impact heavily on the performance of global interconnections in terms of latency, flow rate and consumption. In this context, many integration technologies have been involved, like 3D [1], optical [START_REF] Brière | Design and behavioral modeling tools for optical network-on-chip[END_REF] and/or RF (Radio Frequency) [START_REF] Chang | Advanced RF/Baseband Interconnect Schemes for inter-and intra-ULSICommunications[END_REF][4] [START_REF] Socher | Can RF Help CMOS Processors?[END_REF] interconnect architectures. The interconnect between the Processing Elements (PE) in the same Network on Chip (NoC) through the RF approach, could benefit from high compatibility with the Silicium technology [START_REF] Ito | Bidirectional-and Multi-Drop-Transmission -Line Interconnect for Multipoint-to-Multipoint On-Chip Communications[END_REF]. In an integrated circuit, RF communications can either be wireless (antennas communications [START_REF] Floyd | Intra-chip wireless interconnect for clock distribution implemented with integrated antennas, receivers and transmitters[END_REF]) or through a transmission line [START_REF] Chang | CMP network-on-chip overlaid with multi-band RFinterconnect[END_REF]. In our paper, we consider the case where the transmission is provided through a transmission line.

In this context, as described in [START_REF] Unlu | An OFDMA Based RF Interconnect for Massive Multi-core Processors[END_REF] we propose to develop a hierarchical communication scheme for which a flexible RF interconnect is used to communicate between distant clusters of a single chip. Each of these clusters contains a wired NoC, whose processors communicate between each others by conventional buses, and a transmitter/receiver (Tx/Rx) system for the transmission with other distant clusters via a waveguide (RF transmission line)(fig. 1).

To allow the flexibility of transmissions, we have proposed an allocation of spectrum resources based on an Orthogonal Frequency Division Multiple Access (OFDMA) modulation which introduces essential advantages such as reducing the number of RF components and digital reconfigurability and allocation of subcarriers.

In this paper, we analyse the physical layer of this new RF-NoC interconnection. In part II, we present the method of resources allocation and its reconfigurability. In part III, we study the impact of the channel shape on the transmission, and we present the power levels required to ensure performant communications.

II. ALLOCATION OF SPECTRUM RESOURCES

Using the principle of spectrum sharing, the maximum number of simultaneous communications in full duplex between N clusters is reachable if the number of channels is set to N*(N-1). Frequency multiplexing is used for this application where a portion of total spectrum is allocated for each cluster communication. However, in case of FDMA (Frequency Division Multiple Access) modulation [START_REF] Rouvi`ere | Vhdl-ams model of rf-interconnect system for global on-chip communication[END_REF][10], the number of carriers should be limited to avoid subcarrier interferences that degrade the signal to noise ratio. Moreover to allow data rate and message recipient reconfiguration, this solution needs to reconfigure the RF part, including the frequency of the local oscillator and the bandwidth of the system, that is quite complex and power consuming. The OFDMA modulation scheme has been proposed in [START_REF] Unlu | An OFDMA Based RF Interconnect for Massive Multi-core Processors[END_REF] instead of the FDMA modulation, to divide the available bandwidth into as non-interferent subcarriers as necessary. Using this modulation, we achieve the maximum simultaneous transmissions over the whole band without interference between carriers. This mechanism allows for optimal occupancy of the band and doesn't need the reconfiguration of the RF part; every RF part of Tx/Rx will need to be wideband but not reconfigurable to perform flexible communications.

Since the OFDMA signal is based on FFT and IFFT, the total number of subcarriers that ensure communications between all Tx/Rx, at the same time, should be equal to 2 n . n is determined from the total number of possible transmission by 2 n > N*(N-1). With B the available frequency band, each subcarrier is wide.

In this configuration, two transmission scenarios are allowed:  A high data rate transmission: When only one cluster transmits information, it can benefit from high-speed transmission. Indeed, in this case, all the subcarriers can be allocated for this transmission.  A low data rate transmission: It occurs when many clusters transmit data at the same time. In this case, the subcarriers are shared between all transmissions according to the requirements.

.

In the event of a RF architecture which is composed of 32 RF-NoC [START_REF] Unlu | An OFDMA Based RF Interconnect for Massive Multi-core Processors[END_REF] interfaces with their own Tx/Rx that provide communications between 32 clusters through a transmission line, and to allow all clusters to communicate with each other simultaneously and in both directions, 992 simultaneous transmissions possible can occur. The system needs 1024 subcarriers. Assuming 20 GHz of bandwidth (limited in this study by the technology), the width of a subcarrier is 19.531MHz.

In this configuration, we can increase the rate for each transmission by increasing the number of subcarriers and/or by using higher order modulation. The minimum and maximum reachable rates are shown in the table-I.

We note that, any intermediate solution is made possible because a digital reconfigurability allocation of subcarriers and modulation is feasible thanks to the OFDMA modulation.

III. CHANNEL OPTIMIZATION.

We evaluate the levels of required powers in the worst cases to size the Tx/Rx circuits and optimize their characteristics.

A. Receiver sensitivity.

We evaluate the receiver sensitivity for a bit error rate set to 10 -8 and for a noise factor of the LNA (Low Noise Amplifier) supposed to be equal to 3 dB over the whole frequency band.

The sensitivity is computed for the two extreme transmission cases:

 Full band transmission.  Transmission over one subcarrier.

Two types of digital modulations are considered:  BPSK (Binary Phase shift keying).  64QAM (Quadrature Amplitude Modulation).

Table-II shows the sensitivity values for these configurations. Considering fig. 1, and a distance between two T x /R x of 8mm, the total length of the line is 120 mm.

In the case of direct coupling (fig. 4a) through the line, the presence of multiple T x /R x affects the characteristics of the transmission line, where multiple reflections appear along the line at the interconnect points. To overcome these problems, we used the capacitive coupling to access the line [START_REF] Wong | An empirical three-dimensional crossover capacitance model for multilevel interconnect VLSI circuits[END_REF][12][13][14] (fig. 4b).This method consists in transmitting a signal between two conductors, without any physical link: a gap between the Tx/Rx and the transmission line represents a coupling capacitance that provides the injection of the signal in the propagation channel. By using this method the characteristics of the transmission line are expected to be rather invariant over the whole frequency band, therefore less reflections phenomena appears.

In our study, we use a microstrip transmission line (MTL) as propagation channel. Concerning the substrate properties, they can be summarized as follows:(using a technology delivered by NxP Semiconductors company) height H=8,783 μm; permittivity ɛ r =4,2, loss tangent tgδ=2.10 -4 . In order to minimize the metal loss, we use a transmission line having a characteristic impedance equal to 30 Ω. We evaluate the transmission coefficient (S ji ) between the transmitter i and the receiver j. The Fig. 6 shows the variation of S ji for the farthest Tx and Rx (Tx 1 and Rx 32 in the case of U shape of the fig. 1).

To measure the linear attenuation, we place two ports at both ends of a line and we set their impedance equal to the characteristic impedance Zc (30 Ω in our case) of the line to ensure maximum transmission. The linear attenuation ranges from 0.2 to 0.3 dB/mm in the {20-40} GHz frequency band. The coupling capacitance between the Tx/Rx and the transmission line, that optimize transmission has a value equal to 30fF.

The fig. 6 shows that the lowest value of transmission coefficient S(32,1) is -69 dB.

Then, we calculate the minimum required transmission power corresponding to this value of Sji and to the values of sensitivities presented in Table I. The values of the required transmission power are relatively high.

To improve the level of communication between the different clusters of the circuit, we opt to change the shape of the transmission line, especially the maximum distance between the farthest clusters without degrading the transmission path (in term of desadaptation). To achieve this goal, we use a cross transmission line (fig. 5). This line shape has a length of 80 mm (distance between the cluster 1 and the cluster 32). The cross provides an additional division of the transmitted power at the crossing point, but the gain provided by the reduction of the maximum distance stay more important. The evaluation of the transmission coefficient S(32,1) is shown in fig. 6 (in blue dotted line). As shown in fig. 6 the transmission level increases from -69 dB to -49 dB in the worst case (the longest distance traveled by the signal) which greatly reduces the required transmission power (Table-III).

C. Channel equalization

In order to study the effect of the channel composed of the line and its multiple access on the transfer of information in the system, we perform a co-simulation (circuit-system) using the ADS software, for a transmission based on OFDMA modulation where all circuits are considered ideal except the transmission line.

As shown in fig. 6, the level of transmission is not constant over the whole frequency band leading to an erroneous reception of transmitted data if not equalized.

To overcome this channel effect, we require an estimation of the channel by generating a training sequence that is known by the transmitter and the receiver simultaneously. Thanks to this sequence the receivers can calculate the transfer function of the transmission channel and perform equalization of the signal before demodulation. We note that this training sequence will be generated only once during the system boot as the channel is static (invariant in time). As shown in fig. 7, after Zero-Forcing equalization, the constellation is perfectly corrected (in the case of ideal transceivers/receivers).

IV. CONCLUSION

In this paper we have sized a RF intra-chip communication based on OFDMA modulation. This solution presents many advantages such as providing flexible and highspeed data transmission and variable allocation of frequency band. We have shown the effect of the transmission line on the received data and their level. We also study in this paper the effects of the RF channel shape on the transmission level and the minimum transmission power needed. Finally, we have shown that this configuration needs a channel equalization; its implementation allows to escape the undesired effects of the signal propagation. Our future work is dedicated to study a new interconnect access method to the transmission line in order to obtain a much weaker attenuation through the propagation channel.

Figure 1 :

 1 Figure 1: General MPSOC architecture, based on the RF interconnect approach.

Figure 2 :

 2 Figure 2: Allocation scheme based on OFDMA.

Figure 6 :

 6 Figure 6: Linear attenuation and transmission coefficients Sji between Tx1 and Rx32 in case of U shape and Cross shape of the line

Figure 5 :Figure 4 :

 54 Figure 5: Cross transmission line

Figure57:

  Figure57: Constellations before and after channel equalization.

ACKNOWLEDGMENT This work is supported by the 2012 INS program of the French National Research Agency: ANR-GUI-AAP-05. We would like to thank NXP Semiconductors for providing us their technology.