# Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus

Patrick Baillot, Erika de Benedetti, Simona Ronchi Della Rocca

► To cite this version:

Patrick Baillot, Erika de Benedetti, Simona Ronchi Della Rocca. Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.151-163, 10.1007/978-3-662-44602-7_13. hal-01015171v2

HAL Id: hal-01015171

https://inria.hal.science/hal-01015171v2

Submitted on 24 Nov 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus*

Patrick Baillot<fnref n="1" />, Erika De Benedetti<fnref n="1" />,<fnref n="2" />, and Simona Ronchi Della Rocca<fnref n="2" />

**Abstract.** In this paper an implicit characterization of the complexity classes k-EXP and k-FEXP, for $k \ge 0$, is given, by a type assignment system for a stratified $\lambda$-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k-EXP is characterized by a hierarchy of types.

**Keywords:** Implicit computational complexity · Linear logic · Lambda-calculus

## 1 Introduction

*Context.* Early work on the study of complexity classes by means of programming languages has been carried out by Neil Jones [10,11], in particular using functional programming. The interest of these investigations is twofold: from the computational complexity point of view, they provide new characterizations of complexity classes, which abstract away from machine models; from the programming language point of view, they are a way to analyze the impact on complexity of various programming features (higher-order types, recursive definitions, read/write operations). This fits more generally in the research line of *implicit computational complexity* (ICC), whose goal is to study complexity classes without relying on explicit bounds on resources but instead by considering restrictions on programming languages and calculi. Seminal research in this direction has been carried out in the fields of recursion theory [4,13], $\lambda$-calculus [15] and linear logic [9]. These contributions usually exhibit a new specific language

<footnote n="1">¹ CNRS, ENS de Lyon, INRIA, UCBL, Université de Lyon, LIP - Lyon, France</footnote>

<footnote n="2">² Università degli Studi di Torino, Dipartimento di Informatica - Torino, Italy</footnote>

<footnote>* This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).</footnote>
or logic for each complexity class, for instance PTIME, PSPACE, LOGSPACE: let us call *monovalent* the characterizations of this kind. We think however that the field would benefit from some more uniform presentations, which would consist in both a general language and a family of static criteria on programs of this language, each of which characterizing a particular complexity class. We call such a setting a *polyvalent* characterization; we believe that this approach is more promising for providing insights on the relationships between complexity classes. Polyvalent characterizations of this nature have been given in [11,14], but their criteria used for reaching point (2) referred to the construction steps of the programs. Here we are interested in defining a polyvalent characterization where (2) is expressed by means of the program's type in a dedicated system.

*Stratification and Linear Logic.* An ubiquitous notion in implicit complexity is that of *stratification*, by which we informally designate here the fact of organizing computation into distinct strata. This intuition underlies several systems: ramified and safe recursion [13,4], in which data is organized into strata; stratified comprehension [14], where strata are used for quantification; variants of linear logic [9] where programs are divided into strata thanks to a modality. More recently stratification of data has been related fruitfully to type systems for non-interference [18].

The linear logic approach to ICC is based on the proofs-as-programs correspondence. This logic indeed provides a powerful system to analyse the duplication and sharing of arguments in functional computation: this is made possible by a specific logical connective for the duplication of arguments, the ! modality. As in functional computation the reuse of an argument can cause a complexity explosion, the idea is to use weak versions of ! to characterize complexity classes. This intuition is illustrated by elementary linear logic (ELL) [9,8], a simple variant of linear logic which provides a monovalent characterisation of elementary complexity, that is to say computation in time bounded by a tower of exponentials of fixed height. Other variants of linear logic provide characterizations of PTIME, but they use either a more complicated language [9] or a more specific programming discipline [12].

*Contribution and Comparison.* In [2] a polyvalent characterization in ELL proof-nets of the complexity classes $k-EXP = \cup_{i \in \mathbb{N}} \text{DTIME}(2^{n_i})$ for all $k \ge 0$ has been obtained. However this approach has some shortcomings:

1. The complexity soundness proof uses a partly semantic argument ([2] Lemma 3 p. 10) and so it does not provide a syntactic way to evaluate the programs with the given complexity bound.
2. The characterization is given for classes of predicates, and not for classes of functions. Moreover it is not so clear how to extend this result to functions because of the semantic argument mentioned above.

3. The language of proof-nets is not as standard and widespread as say that of λ-calculus.

In the present work, we wish to establish an analogous polyvalent charac-
terization in the setting of λ-calculus, with a stronger complexity sound-
ness result based on a concrete evaluation procedure. We think this could
provide a more solid basis to explore other characterizations of this kind.
In particular we define the λ'-calculus, a variant of λ-calculus with ex-
plicit stratifications, which allows both to recover the results of [2] and
to characterize also the function complexity classes k-FEXP, by two dis-
tinct hierarchies of types. In fact, the characterization obtained through a
standard representation of data-types like in [2] does not account for some
closure properties of the function classes k-FEXP, in particular composi-
tion, so we propose a new, maybe less natural, representation in order
to grasp these properties. Our language makes it easier to define such
non-standard representation.

*Technical Approach.* One could expect that the results of [2] might be extended to λ'-calculus by considering a translation of terms into proof-nets. However it is not so straightforward: term reduction cannot be directly simulated by the evaluation procedure in [2], because (i) it follows a specific cut-elimination strategy and (ii) ultimately it uses a semantic argument. For this reason we give here a direct proof of the result in λ'-calculus, which requires defining new measures on terms and is not a mere adaptation of the proof-net argument.

*Related Works.* The first results on ELL [9,8] as well as later works [19,6] have been carried out in the setting of proof-nets. Other syntaxes have then been explored. First, specific term calculi corresponding to the related system LLL and to ELL have been proposed [22,17,16]. Alternatively [5] used standard λ-calculus with a type system derived from ELL. The λ'-calculus we use here has a syntax similar to e.g. [21,7], and our type system is inspired by [5].

*Outline.* In the following we first introduce the λ'-calculus as an untyped calculus, delineate a notion of well-formed terms and study the complexity of the reduction of these terms (Sect. 2). We then define a type system inspired by ELL and exhibit two families of types corresponding respectively to the hierarchies k-EXP and k-FEXP for k ≥ 0 (Sect. 3). Finally
we introduce a second characterization of this hierarchy, based on a non-standard data-type (Sect. 4). A conclusion follows.

A version of this work with a technical appendix containing detailed proofs is available as [3].

# 2 The $\lambda^1$-Calculus

## 2.1 Terms and Reduction

We use a calculus, $\lambda^1$-calculus, which adds to ordinary $\lambda$-calculus a ! modality and distinguishes two notions of $\lambda$-abstraction:

$$M, N ::= x \mid \lambda x.M \mid \lambda^1 x.M \mid MN \mid !M$$

where $x$ ranges over a countable set of term variables $Var$. The usual notions of free variables is extended with $FV(\lambda^1 x.M) = FV(M) \setminus \{x\}$, $FV(!M) = FV(M)$. As usual, terms are considered modulo renaming of bound variables, and $=$ denotes the syntactic equality modulo this renaming.

*Contexts.* We consider the class of (one hole) contexts generated by the following grammar:

$$C ::= \Box | \lambda x.C | \lambda^1 x.C | CM | MC | !C$$

As usual, capture of variables may occur. The occurrence of a term $N$ in $M$ is a context $C$ such that $M = C[N]$; in practice we simply write $N$ for the occurrence if there is no ambiguity and call it a subterm of $M$.

*Depth.* The depth of the occurrence $C$ in $M$, denoted by $\delta(C, M)$, is the number of ! modalities surrounding the hole of $C$ in $M$.

Moreover, the depth $\delta(M)$ of a term $M$ is the maximal nesting of ! in $M$.

*Example 1.* $M =!((\lambda x.x) !y !y)$. Then $\delta(!((\lambda x.x) !\Box !y), M) = 3$ and $\delta(!((\lambda x.x) !y !\Box), M) = 2$; moreover, $\delta(M) = 3$.

*Dynamics.* The reduction $\rightarrow$ is the contextual closure of the following rules:

$$(\lambda x.M)N \rightarrow M[N/x] \quad (\beta\text{-rule}) \quad (\lambda^1 x.M)!N \rightarrow M[N/x] \quad (!\text{-rule})$$

where $[N/x]$ denotes the capture free substitution of $x$ by $N$, whose definition is the obvious extension of the corresponding one for $\lambda$-calculus.
Observe that a term such as $(\lambda^1 x.M)P$ is a redex only if $P=!N$ for some $N$; the intuition behind these two kinds of redexes is that the abstraction $\lambda$ expects an input at depth 0, while $\lambda^1$ expects an input at depth 1.

A subterm at depth $i$ in $M$ is an occurrence $C$ in $M$ such that $\delta(C, M) = i$; we denote by $\rightarrow_i$ the reduction of a redex occurring at depth $i$. As usual, $\stackrel{*}{\rightarrow} (\stackrel{*}{\rightarrow}_i)$ denotes the reflexive and transitive closure of $\rightarrow (\rightarrow_i)$. We say that a term is in *i-normal form* if it does not have any redex at depth less than or equal to $i$; then $M$ is in normal form iff it is in $\delta(M)$-normal form. We denote as $nf_i$ the set of terms in *i-normal form*.

We have a confluence property, whose proof is adapted from [20], taking into account the notion of depth:

**Proposition 1.**

(i) Let $M \in nf_i$ and $M \rightarrow_j M'$, with $j \ge i + 1$, then $M' \in nf_i$.

(ii) [Confluence at fixed depth] Let $M \rightarrow_i P$ and $M \rightarrow_i Q$, then there is a term $N$ such that $P \stackrel{*}{\rightarrow}_i N$ and $Q \stackrel{*}{\rightarrow}_i N$.

(iii) [Confluence] Let $M \rightarrow P$ and $M \rightarrow Q$, then there is a term $N$ such that $P \stackrel{*}{\rightarrow} N$ and $Q \stackrel{*}{\rightarrow} N$.

We consider a specific subclass of terms, inspired by elementary linear logic (ELL) [9,17]:

**Definition 1 (Well-formed Term).** A term $M$ is well-formed (w.f.) if and only if, for any subterm $N$ of $M$ which is an abstraction, we have:

1. if $N = \lambda x.P$, then $x$ occurs at most once and at depth 0 in $P$;

2. if $N = \lambda^1 x.P$, then $x$ can only occur at depth 1 in $P$.

*Example 2.* $\lambda f.\lambda x.f(fx)$, the standard representation of the Church integer 2, is not w.f.; its w.f. counterpart is $\lambda^1 f.!(\lambda x.f(fx))$.

The motivation behind such definition is that the depth of subterms in a w.f. term does not change during reduction: if an abstraction expects an input at depth 0 (resp. 1), which is the case of $\lambda$ (resp. $\lambda^1$), then the substitutions occur at depth 0 (resp. 1), as each occurrence of its bound variable is at depth 0 (resp. 1).

The class of w.f. terms is preserved by reduction and their depth does not increase during reduction:

**Lemma 1.** If $M$ is w.f. and $M \rightarrow M'$, then $M'$ is w.f., and $\delta(M') \le \delta(M)$.

From now on, we assume that all terms are well formed.
*Sizes.* In order to study the reduction, it is useful to examine the size of M at depth *i*, denoted by |M|<sub>*i*</sub>, defined as follows:

- If $M = \mathbf{x}$, then $|\mathbf{x}|_0 = 1$ and $|\mathbf{x}|_i = 0$ for $i \ge 1$;

- If $M = \lambda \mathbf{x}.N$ or $M = \lambda^1 \mathbf{x}.N$, then $|M|_0 = |N|_0 + 1$ and $|M|_i = |N|_i$ for $i \ge 1$;

- If $M = \mathbf{NP}$, then $|M|_0 = |N|_0 + |\mathbf{P}|_0 + 1$ and $|M|_i = |N|_i + |\mathbf{P}|_i$ for $i \ge 1$;

- If $M = \mathbf{!N}$, then $|M|_0 = 0$ and $|M|_{i+1} = |N|_i$ for $i \ge 0$;

Let $\delta(\mathbf{M}) = d$; then $|\mathbf{M}|_{i+} = \sum_{j=i}^{d} |\mathbf{M}|_j$ and the size of $\mathbf{M}$ is $|\mathbf{M}| = \sum_{i=0}^{d} |\mathbf{M}|_i$.
The definition is extended to contexts, where $|\Box|_i = 0$ for $i \ge 0$. We
consider how the size of a term changes during reduction:

**Lemma 2.** If $M \to_i M'$, then $|M'|_i \le |M|_i - 1$, and $|M'|_j = |M|_j$ for $j < i$.

*Strategy.* The fact that by Prop. 1.(i) reducing a redex does not cre-
ate any redex at strictly lower depth suggests considering the following,
non-deterministic, *level-by-level* reduction strategy: if the term is not in
normal form reduce (non deterministically) a redex at depth *i*, where
*i* ≥ 0 is the minimal depth such that *M* ∉ *nf*<sub>*i*</sub>. A *level-by-level reduction
sequence* is a reduction sequence following the level-by-level strategy. We
say that a reduction sequence is *maximal* if either it is infinite, or if it
finishes with a normal term.

**Proposition 2.** Any reduction of a term by the level-by-level strategy terminates.

It follows that a maximal level-by-level reduction sequence of a term
M has the shape shown in (1), where $\rightsquigarrow_i$ denotes one reduction step ac-
cording to the level-by-level strategy, performed at depth $i$. We call *round*
$i$ the subsequence of $\rightsquigarrow_i$ starting from $M_i^1$. Note that, for all $i$ and $j > i$,
$M_j^1 \in \mathbf{nf}_i$. We simply write $\rightsquigarrow$ when we do not refer to a particular depth.

$$
M_0^1 \rightsquigarrow_0 \dots \rightsquigarrow_0 M_0^{n_0} = M_1^1 \rightsquigarrow_1 \dots \rightsquigarrow_1 M_1^{n_1} = \dots = M_\delta^1 \rightsquigarrow_\delta \dots \rightsquigarrow_\delta M_\delta^{n_\delta} \quad (1)
$$

In a particular case, namely in Lemma 3, we use a deterministic ver-
sion of the level-by-level strategy, called *leftmost-by-level*, which proceeds
at every level from left to right, taking into account the shape of the dif-
ferent redexes in our calculus. That is to say, it chooses at every step the
leftmost subterm of the shape *MN*, where *M* is an abstraction, and, in case
it is already a redex it reduces it, in case it is of the shape $(\lambda'\mathbf{x}.\mathbf{P})\mathbf{N}$, where
$\mathbf{N} \neq \mathbf{!Q}$, for some $\mathbf{Q}$, then it looks for the next redex in $\mathbf{N}$. This corresponds
to using the call-by-name discipline for *β*-redexes and the call-by-value
for *!*-redexes [20].
$M \implies N$ denotes that $N$ is obtained from $M$ by performing one reduction step according to the leftmost-by-level strategy. All the notations for $\to$ are extended to $\rightsquigarrow$ and $\implies$ in a straightforward way.

## 2.2 Representation of Functions

In order to represent functions, we first need to encode data. For booleans we can use the familiar encoding true = $\lambda x.\lambda y.x$ and false = $\lambda x.\lambda y.y$. For tally integers, the usual encoding of Church integers does not give w.f. terms; instead, we use the following encodings for Church integers and Church binary words:

$$n \in \mathbb{N}, \qquad \underline{n} = \lambda^!f.!(\lambda x.f(f...(f x)...))$$

$$w \in \{0,1\}^*, \quad w = \langle i_1, ..., i_n \rangle, \qquad \underline{w} = \lambda^!f_0.\lambda^!f_1.!(\lambda x.f_{i_1}(f_{i_2}...(f_{i_n} x)...))$$

By abuse of notation we also denote by $\perp$ the term $\lambda^!f.!f$. Observe that the terms encoding booleans are of depth 0, while those representing Church integers and Church binary words are of depth 1. We denote the length of a word $w \in \{0,1\}^*$ by $\text{length}(w)$.

We represent computation on a binary word by considering applications of the form $P!w$, with a ! modality on the argument, because the program should be able to duplicate its input. Concerning the form of the result, since we want to allow computation at arbitrary depth, we require the output to be of the form $!^k D$, where $k \in \mathbb{N}$ and $D$ is one of the data representations above.

We thus say that a function $f: \{0,1\}^* \to \{\text{true}, \text{false}\}$ is represented by a term (program) P if P is a closed normal term and there exists $k \in \mathbb{N}$ such that, for any $w \in \{0,1\}^*$ and $D = f(w) \in \{\text{true}, \text{false}\}$ we have: $P!\underline{w} \stackrel{*}{\to} !^k D$. This definition can be adapted to functions with other domains and codomains.

## 2.3 Complexity of Reduction

We study the complexity of the reduction of terms of the form $P!\underline{w}$. Actually it is useful to analyze the complexity of the reduction of such terms to their $k$-normal form, i.e. by reducing until depth $k$, for $k \in \mathbb{N}$. We define the notation $2_i^n$ in the following way: $2_0^n = x$ and $2_{i+1}^n = 2^{2_i^n}$.

**Proposition 3.** Given a program P, for any $k \ge 2$, there exists a polynomial $q$ such that, for any $w \in \{0,1\}^*$, $P!\underline{w} \stackrel{*}{\to} M_k^1 \in \mathbf{nf}_{k-1}$ in at most $2^{q(n)}$ steps, and $|M_k^1| \le 2^{q(n)}$, where $n = \text{length}(w)$. In particular, in the case where $k = 2$ we have a polynomial bound $q(n)$.
In the rest of this section we prove Prop. 3.

Let $M = P!w$ and consider a level-by-level reduction sequence of $M$, using the notations of (1). By Lemma 2 we know that the number of steps at depth $i$ is bounded by $|M_i^1|$ and that there are $(d+1)$ rounds. In order to bound the total number of steps it is thus sufficient to bound $|M_i^1|$ by means of $|M|$:

**Lemma 3 (Size-Growth).** If $M \stackrel{*}{\Longrightarrow}_i M'$ by $c$ reduction steps, then $|M'| \le |M| \cdot (|M| + 1)^c$ $(0 \le i \le \delta(M))$.

*Proof (Prop. 3).* We proceed by induction on $k \ge 2$. We assume that $P$ is of the form $\lambda^1 y.Q$ (otherwise $P!w$ is already a normal form).

- Case $k=2$:

We consider a level-by-level reduction sequence of $P!w$. We need to examine reduction at depths 0 and 1. At depth 0 we have $(\lambda^1 y.Q)!w \to Q[w/y] = M_1^1$. Observe that $M_1^1 \in nf_0$ because the occurrences of $y$ in $Q$ are at depth 1; denote by $b$ the number of occurrences of $y$ in $Q$, which does not depend on $n$.

Since $|Q[w/y]|_1 \le |Q|_1 + b \cdot |w|_0$ and $|w|_0 = 2$ (by definition of the encoding), we have that $|M_1^1|_1 = |Q[w/y]|_1 \le |Q|_1 + 2b$. Let $c$ be $|Q|_1 + 2b$, which does not depend on $n$: then, by Lemma 2, the number of steps at depth 1 is bounded by $c$. This proves the first part of the statement. Let $M_2^1 \in nf_1$ be the term obtained after reduction at depth 1. By Prop. 1.(ii) we have that $M_1^1 \stackrel{*}{\Longrightarrow}_1 M_2^1$ and by Lemma 2 this reduction is done in $c'$ steps, where $c' \le |M_1^1|_1 \le c$, so by Lemma 3 we have that $|M_2^1| \le |M_1^1| \cdot (|M_1^1| + 1)^c$. Moreover $|M_1^1| \le |Q| + b|w|$, so it is polynomial in $n$, and the statement is proved for $k=2$.

- Assume the property holds for $k$ and let us prove it for $k+1$.

By assumption $M$ reduces to $M_k^1$ in at most $2^{q(n)}$ steps and $|M_k^1| \le 2^{q(n)}$. Let $M_k^1 \stackrel{*}{\Longrightarrow}_k M_{k+1}^1 \in nf_k$. By Lemma 2 this reduction sequence has at most $|M_k^1|_k$ steps, and $|M_k^1|_k \le |M_k^1| \le 2^{q(n)}$. So on the whole $M$ reduces to $M_{k+1}^1$ in at most $2 \cdot 2^{q(n)} \le 2^{2q(n)}$ steps. Moreover by Prop. 1.(ii) we have that $M_k^1 \stackrel{*}{\Longrightarrow} M_{k+1}^1$ and by Lemma 2 and Lemma 3 we get

$$|M_{k+1}^1| \le |M_k^1| \cdot (|M_k^1| + 1)^{2^{q(n)}} \le 2^{q(n)} \cdot (2^{2q(n)})^{2^{q(n)}} \le 2^{q(n)} \cdot 2^{2^{3q(n)}} \le 2^{q'(n)}$$

for some polynomial $q'(n)$.
*Approximations.* From Prop. 3 we can easily derive a $2_{k-2}^{q(n)}$ bound on the number of *steps* of the reduction of $P!w$ not only to its $(k-1)$-normal form, but also to its $k$-normal form $M_{k+1}^1$. Unfortunately this does not yield directly a *time* bound $O(2_{k-2}^{q(n)})$ for the simulation of this reduction on a Turing machine, because during round $k$ the size of the term at depth $k+1$ could grow exponentially. However if we are only interested in the result at depth $k$, the subterms at depth $k+1$ are actually irrelevant. For this reason we introduce a notion of *approximation*, inspired by the semantics of stratified coherence spaces [1], which allows us to compute up to a certain depth $k$, while ignoring what happens at depth $k+1$.

We extend the calculus with a constant $*$; its sizes $|*|_i$ are defined as for variables. If $M$ is a term and $i \in \mathbb{N}$, we define its $i$-th approximation $\bar{M}^i$ by: $\bar{M}^0 = *$, $\bar{M}^{i+1} = !\bar{M}^i$, $\bar{x}^i = x$, and for all other constructions $(\cdot)^i$ acts as identity, e.g. $\bar{MN}^i = \bar{M}^i\bar{N}^i$.

So $\bar{M}^i$ is obtained by replacing in $M$ all subterms at depth $i+1$ by $*$. For instance we have $\bar{w}^0 = \lambda^1 f_0.\lambda^1 f_1.*$ and $\bar{w}^{i+1} = \bar{w}$ for $i \ge 0$.

**Lemma 4.** (i) Let $M \to_j M'$: if $j \le i$ then $\bar{M}^i \to_j \bar{M}'^i$, otherwise $\bar{M}^i = \bar{M}'^i$. (ii) Let $\bar{M}^i \to_i \bar{M}'^i$: then $|\bar{M}'^i| < |\bar{M}^i|$.

**Proposition 4.** *Given a program P, for any $k \ge 2$, there exists a polynomial $q$ such that for any $w \in \{0,1\}^*$, the reduction of $\bar{P!w}^k$ to its $k$-normal form can be computed in time $O(2_{k-2}^{q(n)})$ on a Turing machine, where $n = \text{length}(w)$.*

*Proof.* Observe that $\bar{P!w}^k = \bar{P}^k!w$. By Prop. 3 and Lemma 4.(i), it reduces to its $(k-1)$-normal form $\bar{M}_k^1$ in $O(2_{k-2}^{q(n)})$ steps and with intermediary terms of size $O(2_{k-2}^{q(n)})$. Now by Lemma 4.(ii) the reduction of $\bar{M}_k^1$ at depth $k$ is done in $O(2_{k-2}^{q(n)})$ steps and with intermediary terms of size $O(2_{k-2}^{q(n)})$. We can then conclude by using the fact that one reduction step in a term $M$ can be simulated in time $p(|M|)$ on a Turing machine, for a suitably chosen polynomial $p$.

# 3 Type System

We introduce a type assignment system for $\lambda^1$-calculus, based on ELL, such that all typed terms are also w.f. and the previous results are preserved.
<table><caption>**Table 1.** Derivation rules.</caption>
  <tbody>
    <tr>
      <td>Γ, x : A | Δ | Θ ⊢ x : A (Ax<sup>L</sup>)</td>
      <td>Γ | Δ | x : σ, Θ ⊢ x : σ (Ax<sup>P</sup>)</td>
    </tr>
    <tr>
      <td>Γ, x : A | Δ | Θ ⊢ M : τ / Γ | Δ | Θ ⊢ λx.M : A → τ (¬ I<sup>L</sup>)</td>
      <td>Γ | Δ, x : !σ | Θ ⊢ M : τ / Γ | Δ | Θ ⊢ λ'<sub>x.M</sub> : !σ → τ (¬ I<sup>E</sup>)</td>
    </tr>
    <tr>
      <td>Γ<sub>1</sub> | Δ | Θ ⊢ M : σ → τ / Γ<sub>1</sub>, Γ<sub>2</sub> | Δ | Θ ⊢ MN : τ (¬ E)</td>
      <td>Γ<sub>1</sub>#Γ<sub>2</sub> / Γ | !Θ', Δ | Θ ⊢ !M : !σ (!)</td>
    </tr>
    <tr>
      <td>Γ | Δ | Θ ⊢ M : S a ∉ FTV(Γ) ∪ FTV(Δ) ∪ FTV(Θ) / Γ | Δ | Θ ⊢ M : ∀a.S (∀I)</td>
      <td>Γ | Δ | Θ ⊢ M : ∀a.S / Γ | Δ | Θ ⊢ M : S[σ/a] (∀E)</td>
    </tr>
    <tr>
      <td>Γ | Δ | Θ ⊢ M : S[μa.S/a] / Γ | Δ | Θ ⊢ M : μa.S (μI)</td>
      <td>Γ | Δ | Θ ⊢ M : μa.S / Γ | Δ | Θ ⊢ M : S[μa.S/a] (μE)</td>
    </tr>
  </tbody>
</table>

The set $\mathcal{T}$ of types are generated by the grammar

$A ::= a | S$ (linear types)

$S ::= \sigma \to \sigma | \forall a.S | \mu a.S$ (strict linear types)

$\sigma ::= A | !\sigma$ (types)

where *a* ranges over a countable set of type variables. Observe that we consider both polymorphic types (*∀a.S*) and type fixpoints (*μa.S*); the restriction of both abstractions to act on strict linear types is necessary for the subject reduction property.

A basis is a partial function from variables to types, with finite domain; given two bases $\Gamma_1$ and $\Gamma_2$, let $\Gamma_1\#\Gamma_2$ iff $\text{dom}(\Gamma_1) \cap \text{dom}(\Gamma_2) = \emptyset$. Following the work of [5], we consider three different bases $\Gamma | \Delta | \Theta$, called respectively the *linear*, *modal* and *parking* basis, such that $\Gamma\#\Delta$, $\Gamma\#\Theta$ and $\Delta\#\Theta$. The premises in $\Gamma$ assign to variables linear types, while the premises in $\Delta$ assign modal types.

The typing system proves statements of the shape Γ | Δ | Θ ⊢ M : σ,
and derivations are denoted by Π, Σ. The rules are given in Table 1.
Observe that, in rule (¬ E), M and N share variables in the modal and
parking basis, but their linear bases must be disjoint. Note also that there
is no axiom rule for variables in the modal basis, so the only way to in-
troduce a variable in this basis is the (!) rule, moving variables from the
parking to the modal basis. Finally, observe that there is no abstraction
rule for variables in the parking basis: indeed parking variables only have
a "temporary" status, awaiting to be moved to the modal basis.

We say that a term M is well-typed iff there is a derivation $Π \triangleright Γ | Δ | \emptyset \vdash M : σ$ for some $Γ, Δ, σ$: indeed parking variables are only considered as an intermediary status before becoming modal variables.

When all three bases are empty we denote the derivation by $Π \triangleright \vdash M : σ$. The main difference w.r.t. the type system of [5] is the (!) rule: here we allow only the parking context to be non-empty, in order to ensure that typable terms are well formed: it is the key to obtain a $2_k^{\text{poly}(n)}$ complexity bound for a specific $k$ depending on the type, instead of just an elementary bound.

Both the type and depth of a term are preserved during reduction:

**Theorem 1 (Subject Reduction).** $Γ | Δ | Θ \vdash M : σ$ and $M \to M'$ imply $Γ | Δ | Θ \vdash M' : σ$.

**Proposition 5.** If a term is well-typed, then it is also well-formed.

The proof comes easily from the following proposition:

**Proposition 6 (Variables Depth).** Let $Γ | Δ | Θ \vdash M : σ$. Then:

- if $x \in \text{dom}(Γ) \cup \text{dom}(Θ)$, then $x$ can only occur at depth 0 in M;

- if $x \in \text{dom}(Δ)$, then $x$ can only occur at depth 1 in M.

## 3.1 Datatypes

In section 2.2 we introduced w.f. terms encoding data, for which we now define the following types, adapted from system F, representing respectively booleans, Church tally integers and Church binary words:

$$B = \forall a.a \to a \to a \qquad N = \forall a.!(a \to a) \to!(a \to a)$$

$$W = \forall a.!(a \to a) \to!(a \to a) \to!(a \to a)$$

We also use Scott binary words, defined inductively as

$$\hat{\epsilon} \stackrel{\text{def}}{=} \lambda f_0. \lambda f_1. \lambda x. x \qquad \hat{0w} \stackrel{\text{def}}{=} \lambda f_0. \lambda f_1. \lambda x. f_0 \hat{w} \qquad \hat{1w} \stackrel{\text{def}}{=} \lambda f_0. \lambda f_1. \lambda x. f_1 \hat{w}$$

having type $W_S \stackrel{\text{def}}{=} \mu b. \forall a. (b \to a) \to (b \to a) \to (a \to a)$.

The following properties ensure that, given a datatype, every derivation having such type reduces to a term having the desired shape:

**Proposition 7.** (i) If $M \vdash M : !^k B$ for $k \ge 0$ and $M \in \mathbf{nf}_k$, then either $M = !^k \text{true}$ or $M = !^k \text{false}$.

(ii) If $M \vdash M : !^k W_S$ for $k \ge 0$ and $M \in \mathbf{nf}_k$, then $M = !^k \hat{w}$ for some $\hat{w}$.
## 3.2 Complexity Soundness and Completeness

We are interested in giving a precise account of the hierarchy of classes characterized by this typed $\lambda^1$-calculus. Denote by FDTIME($F(n)$) and by DTIME($F(n)$) respectively the class of functions and the class of predicates on binary words computable on a deterministic Turing machine in time $O(F(n))$; the complexity classes we are interested in, for $k \ge 0$, are:

$$k-\text{EXP} = \bigcup_{i \in \mathbb{N}} \text{DTIME}(2_k^{n_i}) \quad \text{and} \quad k-\text{FEXP} = \bigcup_{i \in \mathbb{N}} \text{FDTIME}(2_k^{n_i}).$$

In particular, observe that PTIME = $\bigcup_{i \in \mathbb{N}} \text{DTIME}(n^i) = \text{O-EXP}$ and FPTIME = $\bigcup_{i \in \mathbb{N}} \text{FDTIME}(n^i) = \text{O-FEXP}$.

**Soundness** Let $\mathcal{F}(\sigma)$ denote the set of closed terms representing functions, to which type $\sigma$ can be assigned: we prove that $\mathcal{F}(!W \to!^{k+2}B) \subseteq k-\text{EXP}$ and $\mathcal{F}(!W \to!^{k+2}W_S) \subseteq k-\text{FEXP}$.

**Theorem 2 (Soundness).** Let $\vdash P :!W \to!^{k+2}B$ where P is a program, and let $\vdash \underline{w} : W$ where $\text{length}(\underline{w}) = n$; then the reduction $P!\underline{w} \stackrel{*}{\to} !^{k+2}D$ can be computed in time $2_k^{p(n)}$, where D is either true or false and p is a polynomial.

**Proof.** Recall that a program P is a typed closed term in normal form: we denote by $M'$ the normal form of $P!\underline{w}$. By Prop. 4 we know that $\overline{P!\underline{w}}^{k+2}$ can be reduced to a term N in $\overline{nf_{k+2}}$ in time $O(2_k^{p(n)})$ on a Turing machine, where $n = \text{length}(\underline{w})$. Moreover by Lemma 4.(i) and Prop. 1.(iii) we have that $\overline{M'}^{k+2} = N$. Now, as $P!\underline{w}$ has type $!^{k+2}B$, by Theorem 1 the term $M'$ is a closed term of type $!^{k+2}B$ and, by Prop. 7.(i), it is equal to $!^{k+2}\text{true}$ or $!^{k+2}\text{false}$. Then $N = \overline{M'}^{k+2} = M'$, so $P!\underline{w}$ can be computed in time $O(2_k^{p(n)})$.

Complexity soundness can be proved for functions by a similar proof, in which Prop. 7.(ii) is used in order to read the output as a Scott word:

**Theorem 3.** Let $\vdash P :!W \to!^{k+2}W_S$ where P is a program, and let $\vdash \underline{w} : W$ where $\text{length}(\underline{w}) = n$; then the reduction $P!\underline{w} \stackrel{*}{\to} !^{k+2}\hat{w}'$ can be computed in time $2_k^{p(n)}$, where p is a polynomial.

**Completeness** We proved that $\mathcal{F}(!W \to!^{k+2}B) \subseteq k-\text{EXP}$ and $\mathcal{F}(!W \to!^{k+2}W_S) \subseteq k-\text{FEXP}$; now we want to strengthen this result by examining the converse inclusions. To do so we simulate k-EXP time bounded Turing machines, by an iteration, so as to prove the following results:
**Theorem 4 (Extensional Completeness).**

- Let $f$ be a binary predicate in $k$-EXP, for any $k \ge 0$; then there is a term $M$ representing $f$ such that $\vdash M :!W \neg!{k+2}B$.

- Let $g$ be a function on binary words in $k$-FEXP, for $k \ge 0$; then there is a term $M$ representing $g$ such that $\vdash M :!W \neg!{k+2}W_S$.

Note that this characterization, for $k = 0$, does not account for the fact that FPTIME is closed by composition: indeed, programs of type $!W \neg!{k+2}W_S$ cannot be composed, since we do not have any coercion from $W_S$ to $W$. For this reason, we explore an alternative characterization.

**4 Refining Types for an Alternative Characterization**

Our aim is to take a pair $\langle n, w \rangle$ to represent the word $w'$ such that:

$$w' = \begin{cases} w & \text{if } \text{length}(w) \le n, \\ \text{the prefix of } w \text{ of length } n & \text{otherwise.} \end{cases}$$

For this reason, we introduce a new data-type using the connective $\otimes$ defined by $\sigma \otimes \tau \stackrel{\text{def}}{=} \forall a.((\sigma \to \tau \to a) \to a)$ on types and the corresponding constructions on terms:

$$\begin{align*} M_1 \otimes M_2 &\stackrel{\text{def}}{=} \lambda x.xM_1M_2 \\ \lambda(x_1 \otimes x_2).M &\stackrel{\text{def}}{=} \lambda x.(x\lambda y_1y_2.\lambda z.zy_1y_2)\lambda x_1x_2.M \\ \lambda'(x_1 \otimes x_2).M &\stackrel{\text{def}}{=} \lambda x.(x\lambda'y_1y_2.\lambda z.z'y_1y_2)\lambda'x_1x_2.M \end{align*}$$

Note that we cannot define the abstraction in the usual way, i.e. $\lambda(x_1 \otimes x_2).M \stackrel{\text{def}}{=} \lambda x.x(\lambda x_1.\lambda x_2.M)$, otherwise we could not type pairs in a uniform way; moreover, when applied to a pair, this term reduces to the usual one.

The associated reduction rules $(\lambda(x_1 \otimes x_2).N)(M_1 \otimes M_2) \to N[M_1/x_1, M_2/x_2]$ and $(\lambda'(x_1 \otimes x_2).N)(!M_1 \otimes !M_2) \to N[M_1/x_1, M_2/x_2]$ are derivable.

We represent a pair $\langle n, w \rangle$ through a term $!\underline{n} \otimes !^2\hat{w}$ of type $!N \otimes !^2W_S$, i.e. a combined data-type containing a Church integer $!\underline{n}$ and a Scott word $!^2\hat{w}$: in practice, $\underline{n}$ is meant to represent the length of a list, whose content is described by $\hat{w}$. In order to maintain this invariant, when computing on elements $!\underline{n} \otimes !^2\hat{w}$ of this data-type, the property that the length of $w$ is inferior or equal to $n$ is preserved.

As before, we need to be able to extract the result, in this case a pair:
**Proposition 8.** If $\vdash \mathbf{M} : !^k \mathbf{N} \otimes !^{k+1} W_S$ for $k \ge 0$ and $\mathbf{M} \in \mathbf{n}f_{k+1}$, then there exists $m \in \mathbb{N}$ and $w \in \{0, 1\}^*$ such that $\mathbf{M} = !^k \underline{m} \otimes !^{k+1} \hat{w}$.

Then we are able to prove both soundness and completeness results:

**Theorem 5.** Let $\vdash \mathbf{P} : (!\mathbf{N} \otimes !^2 W_S) \dashv (!^{k+1}\mathbf{N} \otimes !^{k+2} W_S)$ where $\mathbf{P}$ is a program, then for any $\underline{m}$ and $\hat{w}$ the reduction of $\mathbf{P}(!\underline{m} \otimes !^2 \hat{w})$ to its normal form can be computed in time $2_k^{p(n)}$, where $p$ is a polynomial and $n = m + \text{length}(w)$.

**Theorem 6.** Let $f$ be a function on binary words in $\mathbf{k}\text{-FEXP}$, for $k \ge 0$; then there is a term $\mathbf{M}$ representing $f$ such that $\vdash \mathbf{M} : (!\mathbf{N} \otimes !^2 W_S) \dashv (!^{k+1}\mathbf{N} \otimes !^{k+2} W_S)$.

Observe that we are able to compose two terms having type $(!\mathbf{N} \otimes !^2 W_S) \dashv (!\mathbf{N} \otimes !^2 W_S)$, so to illustrate the fact that FPTIME is closed by composition; moreover, if $f \in \text{FPTIME}$ and $g \in \mathbf{k}\text{-FEXP}$, then we can compose terms representing them, which shows that $g \circ f \in \mathbf{k}\text{-FEXP}$.

While the previous characterization of $\mathbf{k}\text{-FEXP}$ in Section 3.2 offers the advantage of simplicity, because it uses classical data-types (Church and Scott binary words), this second characterization offers a better account of the closure properties of these complexity classes, at the price of a slightly more involved representation of words.

# 5 Conclusions

We have shown how the concept of !-stratification coming from linear logic can be fruitfully employed in $\lambda$-calculus and characterize the hierarchies $\mathbf{k}\text{-EXP}$ and $\mathbf{k}\text{-FEXP}$, including the classes PTIME and FPTIME. A nice aspect of our system with respect to former polyvalent characterizations [11,14] is that the complexity bound can be deduced by looking only at the interface of the program (its type) without refering to the constructions steps. In our proofs we have carefully distinguished the respective roles played by syntactic ingredients (well-formedness) and typing ingredients. This has allowed us to illustrate how types can provide two different characterizations of the class $\mathbf{k}\text{-FEXP}$, based on the use of different data-types. We believe that the separation between syntactic and typing arguments can facilitate the possible future usage of our calculus with other type systems. As future work it would be challenging to investigate if similar characterizations could be obtained for other hierarchies, like possibly space hierarchies.
References

1. Baillot, P.: Stratified coherence spaces: a denotational semantics for light linear logic. Theor. Comput. Sci. 318(1-2), 29–55 (2004)

2. Baillot, P.: Elementary linear logic revisited for polynomial time and an exponential time hierarchy. In: Yang, H. (ed.) APLAS. Lecture Notes in Computer Science, vol. 7078, pp. 337–352. Springer (2011)

3. Baillot, P., De Benedetti, E., Ronchi Della Rocca, S.: Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Tech. rep. (2014), http://hal.archives-ouvertes.fr/hal-01015171, 31 pages

4. Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the poly-time functions. Computational Complexity 2, 97–110 (1992)

5. Coppola, P., Dal Lago, U., Ronchi Della Rocca, S.: Light logics and the call-by-value lambda-calculus. Logical Methods in Computer Science 4(4) (2008)

6. Dal Lago, U.: Context semantics, linear logic, and computational complexity. ACM Trans. Comput. Log. 10(4) (2009)

7. Dal Lago, U., Masini, A., Zorzi, M.: Quantum implicit computational complexity. Theor. Comput. Sci. 411(2), 377–409 (2010)

8. Danos, V., Joinet, J.B.: Linear logic and elementary time. Inf. Comput. 183(1), 123–137 (2003)

9. Girard, J.Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)

10. Jones, N.D.: Computability and complexity - from a programming perspective. Foundations of computing series, MIT Press (1997)

11. Jones, N.D.: The expressive power of higher-order types or, life without cons. J. Funct. Program. 11(1), 5–94 (2001)

12. Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1-2), 163–180 (2004)

13. Leivant, D.: Predicative recurrence and computational complexity I: word recurrence and poly-time. In: Feasible Mathematics II, pp. 320–343. Birkhauser (1994)

14. Leivant, D.: Calibrating computational feasibility by abstraction rank. In: LICS. pp. 345–. IEEE Computer Society (2002)

15. Leivant, D., Marion, J.Y.: Lambda-calculus characterizations of poly-time. Fundam. Inform. 19(1/2), 167–184 (1993)

16. Madet, A.: Implicit Complexity in Concurrent Lambda-Calculi. Ph.D. thesis, Université Paris 7 (December 2012), http://tel.archives-ouvertes.fr/tel-00794977

17. Madet, A., Amadio, R.M.: An elementary affine lambda-calculus with multithreading and side effects. In: Ong, C.H.L. (ed.) TLCA. Lecture Notes in Computer Science, vol. 6690, pp. 138–152. Springer (2011)

18. Marion, J.Y.: A type system for complexity flow analysis. In: LICS. pp. 123–132. IEEE Computer Society (2011)

19. Mazza, D.: Linear logic and polynomial time. Mathematical Structures in Computer Science 16(6), 947–988 (2006)

20. Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science, Springer, Berlin (2004), http://www.springer.com/sgw/cda/frontpage/0,5-40356-72-14202886-0,00.html

21. Ronchi Della Rocca, S., Roversi, L.: Lambda-calculus and intuitionistic linear logic. Studia Logica 59(3), 417–448 (1997)

22. Terui, K.: Light affine lambda-calculus and polynomial time strong normalization. Arch. Math. Log. 46(3-4), 253–280 (2007)