On the Elementary Affine Lambda-Calculus with and Without Fixed Points

TL;DR

This paper investigates the elementary affine lambda-calculus, demonstrating that removing type fixpoints limits its expressive power to regular languages, and proposes improvements for characterizing complexity classes with recursive types.

Contribution

It shows that without recursive types, the calculus characterizes regular languages, and introduces an aesthetic enhancement for representing FP and k-FEXPTIME with recursive types.

Findings

Without fixpoints, the calculus characterizes regular languages.

Semantic evaluation method proves the necessity of fixpoints for complexity classes.

Improved characterization of FP and k-FEXPTIME with recursive types.

Abstract

The elementary affine lambda-calculus was introduced as a polyvalent setting for implicit computational complexity, allowing for characterizations of polynomial time and hyperexponential time predicates. But these results rely on type fixpoints (a.k.a. recursive types), and it was unknown whether this feature of the type system was really necessary. We give a positive answer by showing that without type fixpoints, we get a characterization of regular languages instead of polynomial time. The proof uses the semantic evaluation method. We also propose an aesthetic improvement on the characterization of the function classes FP and k-FEXPTIME in the presence of recursive types.

Equations

$${\mathtt{Str}}_{\_}S:=\forall \alpha .({\mathtt{Str}}_{\_}S⊸\alpha )⊸({\mathtt{Str}}_{\_}S⊸\alpha )⊸\alpha ⊸\alpha$$

$${\mathtt{Str}}_{\_}S:=\mu \beta .\forall \alpha .(\beta ⊸\alpha )⊸(\beta ⊸\alpha )⊸\alpha ⊸\alpha$$

$$S(\epsilon )=\lambda f_{\_}0.\lambda f_{\_}1.\lambda x.xS(0\cdot w^{\prime })=\lambda f_{\_}0.\lambda f_{\_}1.\lambda x.f_{\_}0S(w^{\prime })S(1\cdot w^{\prime })=\lambda f_{\_}0.\lambda f_{\_}1.\lambda x.f_{\_}1S(w^{\prime })$$

$$t,u::=x\mid \lambda x.t\mid \lambda \text{oc}x.t\mid tu\mid \text{oc}t(\lambda x.t)u{⟶}_{\_}\beta t\{x:=u\}(\lambda \text{oc}x.t)(\text{oc}u){⟶}_{\_}\text{oc}t\{x:=u\}$$

$$\text{for w=w\_1…w\_n∈{0,1}∗},\overline{w}=\lambda \text{oc}{f}_{\_}0.\lambda \text{oc}{f}_{\_}1.\text{oc}(\lambda x.f_{\_}{w}_{\_}1(\dots (f_{\_}{w}_{\_}nx)\dots ))$$

$$A::=\alpha \mid SS::=\sigma ⊸\tau \mid \forall \alpha .S\sigma ,\tau ::=A\mid \text{oc}\sigma$$

$$\text{variable rules}\frac{}{\Gamma ,x:A\mid \Delta \mid \Theta ⊢x:A}\frac{}{\Gamma \mid \Delta \mid \Theta ,x:\sigma ⊢x:\sigma }$$

$$\text{abstraction rules}\frac{\Gamma ,x:A\mid \Delta \mid \Theta ⊢t:\tau }{\Gamma \mid \Delta \mid \Theta ⊢\lambda x.t:A⊸\tau }\frac{\Gamma \mid \Delta ,x:\text{oc}\sigma \mid \Theta ⊢t:\tau }{\Gamma \mid \Delta \mid \Theta ⊢\lambda \text{oc}x.t:\text{oc}\sigma ⊸\tau }$$

$$\text{application rule}\frac{\Gamma \mid \Delta \mid \Theta ⊢t:\sigma ⊸\tau {\Gamma }^{\prime }\mid \Delta \mid \Theta ⊢u:\sigma }{\Gamma \uplus {\Gamma }^{\prime }\mid \Delta \mid \Theta ⊢tu:\tau }$$

$$\text{quantifier rules}\frac{\Gamma \mid \Delta \mid \Theta ⊢t:S}{\Gamma \mid \Delta \mid \Theta ⊢t:\forall \alpha .S}\frac{\Gamma \mid \Delta \mid \Theta ⊢t:\forall \alpha .S}{\Gamma \mid \Delta \mid \Theta ⊢t:S\{\alpha :=A\}}$$

$$\text{functorial promotion rule}\frac{\varnothing \mid \varnothing \mid \Theta ⊢t:\sigma }{\Gamma \mid \text{oc}\Theta ,\Delta \mid {\Theta }^{\prime }⊢\text{oc}t:\text{oc}\sigma }$$

$$\text{for w=w\_1…w\_n∈{0,1}∗},x:\alpha \mid \varnothing \mid f_{\_}0:\alpha ⊸\alpha ,f_{\_}1:\alpha ⊸\alpha ⊢f_{\_}{w}_{\_}1(\dots (f_{\_}{w}_{\_}nx)\dots ):\alpha$$

$$\text{μ-fold}\frac{\Gamma \mid \Delta \mid \Theta ⊢t:S\{\alpha :=\mu \alpha .S\}}{\Gamma \mid \Delta \mid \Theta ⊢t:\mu \alpha .S}\text{μ-unfold}\frac{\Gamma \mid \Delta \mid \Theta ⊢t:\mu \alpha .S}{\Gamma \mid \Delta \mid \Theta ⊢t:S\{\alpha :=\mu \alpha .S\}}$$

$$\mathtt{Nat}=\forall \alpha .\text{oc}(\alpha ⊸\alpha )⊸\text{oc}(\alpha ⊸\alpha )\sigma \otimes \tau =\forall \alpha .(\sigma ⊸\tau ⊸\alpha )⊸\alpha$$

$$\mathtt{cast}=\lambda n.\lambda \text{oc}w.\lambda \text{oc}{f}_{\_}0.\lambda \text{oc}{f}_{\_}1.\mathtt{let}\text{oc}g\leftarrow n\text{oc}(\lambda (h\otimes u).t)\mathtt{in}\text{oc}({\pi }_{\_}1(g((\lambda x.x)\otimes w)))$$

$$\text{with}t=\mathtt{let}f\otimes v\leftarrow (\mathtt{case}u\mid 0v\mapsto f_{\_}0\otimes v\mid 1v\mapsto f_{\_}1\otimes v\mid \epsilon \mapsto (\lambda z.z)\otimes S(\epsilon ))\mathtt{in}(\lambda x.h(fx))\otimes v$$

$$\lambda \text{oc}w.{\mathtt{cast}}^{(k+1)}(t_{\_}\mathcal{M}\text{oc}w)(f\text{oc}w):\text{oc}\mathtt{Str}⊸{\text{oc}}^{k+1}\mathtt{Str}$$

$$\mathcal{L}_{\_}{\mathrm{ST}\lambda}(t)=\varphi_{\_}A^{-1}(\{\omega\in\left\llbracket\mathtt{Str}[A]\right\rrbracket\mid\left\llbracket t\right\rrbracket(\omega)=\left\llbracket\mathtt{true}\right\rrbracket\})$$

$$\left\llbracket\mathtt{Str}[A]\right\rrbracket=\left(\left\llbracket A\to A\right\rrbracket^{\left\llbracket A\to A\right\rrbracket}\right)^{\left\llbracket A\to A\right\rrbracket}\cong\mathrm{End}(\left\llbracket A\right\rrbracket)^{\mathrm{End}(\left\llbracket A\right\rrbracket)^{2}}$$

$$\forall(f_{\_}0,f_{\_}1)\in\mathrm{End}(\left\llbracket A\right\rrbracket)^{2},\;\left(w\mapsto\left\llbracket\overline{w}\right\rrbracket(f_{\_}0,f_{\_}1)\right)\text{ is a morphism }\{0,1\}^{*}\to\mathrm{End}(\left\llbracket A\right\rrbracket)$$

$$\forall(f_{\_}0,f_{\_}1)\in\mathrm{End}(\left\llbracket A\right\rrbracket)^{2},\;\left\llbracket\overline{w}\right\rrbracket(f_{\_}0,f_{\_}1)=f_{\_}{w_{\_}1}\circ\ldots\circ f_{\_}{w_{\_}n}$$

$$\Vert \text{oc}t{\Vert }_0=(\lambda x.x)\Vert (\lambda \text{oc}x.t){\Vert }_0=\lambda x.\Vert t{\Vert }_0\Vert \lambda x.t{\Vert }_0=\lambda x.\Vert t{\Vert }_0\Vert tu{\Vert }_0=\Vert t{\Vert }_0\Vert u{\Vert }_0\Vert x{\Vert }_0=x$$

$$\Vert \text{oc}\sigma {\Vert }_0=1\Vert \sigma ⊸\tau {\Vert }_0=\Vert \sigma {\Vert }_0⊸\Vert \tau {\Vert }_0\Vert \alpha {\Vert }_0=\alpha \Vert \forall \alpha .\sigma {\Vert }_0=\forall \alpha .\Vert \sigma {\Vert }_0$$

$$v=\mathtt{let}\text{oc}{y}_{\_}1\leftarrow (\dots (\mathtt{let}\text{oc}{y}_{\_}l\leftarrow x\text{oc}{f}_{\_}0\text{oc}{f}_{\_}1\mathtt{in}\text{oc}{p}_{\_}l)\dots )\mathtt{in}\text{oc}{p}_{\_}1$$

$$us=(\lambda x.v)s⟶v\{x:=s\}{⟶}^{\ast }\text{oc}(p_{\_}1\{y_{\_}1:=(\dots p_{\_}l\{y_{\_}l:=h\}\dots )\})$$

$$\lambda x.f_{\_}^{\prime }{w}_{\_}1(\dots (f_{\_}^{\prime }{w}_{\_}nx)\dots ){⟶}^{\ast }{h}^{\prime }\text{and by truncation}\lambda x.f_{\_}{w}_{\_}1(\dots (f_{\_}{w}_{\_}nx)\dots ){⟶}^{\ast }\Vert h^{\prime }{\Vert }_0$$

$$\{w\in \{0,1{\}}^{\ast }\mid u\overline{w}\dots \overline{w}{⟶}^{\ast }\text{oc}\mathtt{true}\}$$

$$\left\llbracket b\right\rrbracket=\left\llbracket g\right\rrbracket\left(\Phi_{\|\sigma\|_{0}}(w)(\left\llbracket f_{\_}0\right\rrbracket,\left\llbracket f_{\_}1\right\rrbracket),\ldots,\Phi_{\|\sigma\|_{0}}(w)(\left\llbracket f_{\_}0\right\rrbracket,\left\llbracket f_{\_}1\right\rrbracket)\right)$$

$$\{w\in \{0,1{\}}^{\ast }\mid t\text{oc}\overline{w}{⟶}^{\ast }\text{oc}\text{oc}\mathtt{true}\}=\{w\in \{0,1{\}}^{\ast }\mid u\overline{w}\dots \overline{w}{⟶}^{\ast }\text{oc}\mathtt{true}\}$$

$$\forall X.\text{oc}X⊸\text{oc}(X⊸X⊸X)⊸\text{oc}(X⊸X\otimes X)⊸\text{oc}X$$

Full text

1 Introduction

The elementary affine $\lambda$-calculus

Elementary Linear Logic (ELL), introduced by Girard [10], is a logic that can be seen as a typed functional programming language through the proof-as-programs correspondence. Its typing rules ensure that a function can be expressed if and only if it is elementary recursive (as is expounded in detail in [7]), hence the name. (This is an instance of the “type-theoretic” or “Curry–Howard” approach to implicit computational complexity.) This was refined by Baillot [2] into a characterization of each level of the $k$-EXPTIME hierarchy, in an affine variant of ELL.

A later improvement by Baillot, De Benedetti and Ronchi [3] consisted in turning this logic into an actual type system for a functional calculus with good properties (e.g. subject reduction), called the elementary affine $\lambda$-calculus. In this paper, we shall call their system ${\mu\mathrm{EA}\lambda}$ – the reason for the $\mu$ will soon become clear. The main result about it is:

Theorem 1.1** ([3]).**

The programs of type $\oc\mathtt{Str}\multimap\oc^{k+2}\mathtt{Bool}$ in ${\mu\mathrm{EA}\lambda}$ decide exactly the languages in the class $k$-EXPTIME. In particular $\oc\mathtt{Str}\multimap\ \oc\oc\mathtt{Bool}$ corresponds to polynomial time (P) predicates.

Here are some indications for the reader unfamiliar with linear or affine type systems:

• •

a program of type $A\multimap B$ uses its input of type $A$ at most once to produce its output of type $B$;

• •

$\oc A$ means roughly “as many $A$’s as you want”, so a function which uses its argument multiple times can be given a type of the form $\oc A\multimap B$;

• •

in usual linear or affine logic, one can convert a $\oc A$ into a $A$; however, in the elementary affine $\lambda$-calculus, there is a restriction which makes the exponential depth (number of ‘$\oc$’ modalities) meaningful, one cannot perform such a depth-changing operation – this is why the depth $k$ of the output $\oc^{k}\mathtt{Bool}$ (i.e. $\oc(\ldots(\oc\mathtt{Bool}))$ with $k$ ‘$\oc$’) controls the complexity;

• •

the type of booleans is defined as $\mathtt{Bool}=\forall\alpha.\,\alpha\multimap\alpha\multimap\alpha$, and it has two inhabitants;

• •

$\mathtt{Str}=\forall\alpha.\,\mathtt{Str}[\alpha]$, with $\mathtt{Str}[\alpha]=\oc(\alpha\multimap\alpha)\multimap\oc(\alpha\multimap\alpha)\multimap\oc(\alpha\multimap\alpha)$, is the type of Church encodings of binary strings: the string $w_{\_}1\ldots w_{\_}n\in\{0,1\}^{*}$ is represented as the function which, for any type $A$, takes as input $f_{\_}0:A\multimap A$ and $f_{\_}1:A\multimap A$, and returns $f_{\_}{w_{\_}1}\circ\ldots\circ f_{\_}{w_{\_}n}$.

Type fixpoints and Scott encodings

We wish to draw attention to a particular feature of this language: the presence of type fixpoints111A remark for the readers acquainted with typed $\lambda$-calculi: there is no “positivity” constraint imposed, yet those recursive types are harmless for the normalization property, as the untyped version of the elementary affine $\lambda$-calculus is already normalizing. The analogous property for ELL was already remarked in [10]., a.k.a. recursive types. An example is the type of Scott binary strings:

[TABLE]

In the elementary affine $\lambda$-calculus as defined in [3], this recursive equation can be turned into a valid type definition, by using a fixed point operator $\mu$ on types (this explains our name ${\mu\mathrm{EA}\lambda}$):

[TABLE]

The idea is that strings are represented by their “pattern-matching” function (destructor): if $u$ is a Scott binary string, then $u\;f_{\_}0\;f_{\_}1\;x$ morally means “if $u$ represents the empty word, return $x$; else, return $f_{\_}c$ applied to $v$ where $c\in\{0,1\}$ is the first letter and $v$ represents the suffix”. Formally, we associate to each string $w\in\{0,1\}^{*}$ a ${\mu\mathrm{EA}\lambda}$-term $S(w)$ of type $\mathtt{Str}_{\_}S$:

[TABLE]

This encoding of strings has been used to give a characterization of function classes in ${\mu\mathrm{EA}\lambda}$:

Theorem 1.2** ([3]).**

The programs of type $\oc\mathtt{Str}\multimap\oc^{k+2}\mathtt{Str}_{\_}S$ in ${\mu\mathrm{EA}\lambda}$ compute exactly the functions in the class $k$-FEXPTIME. In particular $\oc\mathtt{Str}\multimap\ \oc\oc\mathtt{Str}_{\_}S$ corresponds to FP.

Our contributions

There are two natural questions concerning the necessity of type fixpoints:

• •

In the interface: it is possible to characterize this hierarchy of function classes using a function type involving only Church encodings?

• •

In the implementation: the extensional completeness proof for the predicate classes (Theorem 1.1) makes use of the type $\mathtt{Str}_{\_}S$ (to represent configurations of Turing machines), even though this type does not appear in the statement; could one avoid recursive types in the proof? This question has been raised by Baillot in the conclusion of [2].

In this paper, we answer both questions. The first one has a positive answer:

Theorem 1.3**.**

The programs of type $\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Str}$ in ${\mu\mathrm{EA}\lambda}$ compute exactly the functions in the class $k$-FEXPTIME. In particular $\oc\mathtt{Str}\multimap\ \oc\mathtt{Str}$ corresponds to FP.

An advantage of this characterization is that it reflects the fact that composing a $k$-FEXPTIME function $f$ with a $l$-FEXPTIME function $g$ gives a $(k+l)$-FEXPTIME function: since any ${\mu\mathrm{EA}\lambda}$-term of type $A\multimap B$ lifts to a term of type $\oc^{k}A\multimap\oc^{k}B$ (this is called “functorial promotion”, cf. Proposition 2.2), we can compose the terms $f:\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Str}$ and $g^{(k)}:\oc^{k+1}\mathtt{Str}\multimap\oc^{(l+1)+k}\mathtt{Str}$ to obtain a term of type $\oc\mathtt{Str}\multimap\oc^{(k+l)+1}\mathtt{Str}$. In particular FP is closed under composition. A characterization of FP in ${\mu\mathrm{EA}\lambda}$ by a function type whose input and output types coincide was proposed in [3], but it is less natural: a string is represented as a pair of its length (Church-encoded) and its contents (Scott-encoded).

As for the second question, we should first mention that Girard’s original characterization of elementary recursive functions in ELL does not involve type fixpoints. This can be replayed in the elementary affine $\lambda$-calculus without type fixpoints, which we shall denote by ${\mathrm{EA}\lambda}$.

Theorem 1.4** ([2]).**

The class of elementary recursive functions is the union, over $k\in\mathbb{N}$, of the classes of functions computed by programs of type $\oc\mathtt{Str}\multimap\oc^{k}\mathtt{Str}$ in ${\mathrm{EA}\lambda}$.

(The detailed proof given in [2] is for Elementary Affine Logic; it can be directly transposed to ${\mathrm{EA}\lambda}$.)

However, the characterization of P by $\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ fails in ${\mathrm{EA}\lambda}$, as we show:

Theorem 1.5**.**

The programs of type $\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ in ${\mathrm{EA}\lambda}$ decide exactly the regular languages. This is also the case for the ${\mathrm{EA}\lambda}$-terms of type $\mathtt{Str}\multimap\oc\mathtt{Bool}$.

This result is surprising for a few reasons: the class of languages obtained is unexpectedly small, and it hints at connections between ${\mathrm{EA}\lambda}$ and formal language theory (the conclusion will discuss this further). The proof techniques for the above theorem are quite different from those used in [3]: instead of bounding the syntactic normalization process, we take inspiration from the tradition of implicit complexity in the simply typed $\lambda$-calculus (${\mathrm{ST}\lambda}$), in particular from:

Theorem 1.6** (Hillebrand & Kanellakis [15]).**

In the simply typed $\lambda$-calculus, the languages decided by terms of type $\mathtt{Str}_{\_}{{\mathrm{ST}\lambda}}[A]\to\mathtt{Bool}_{\_}{\mathrm{ST}\lambda}$ – $A$ is a simple type that may be chosen depending on the language – are exactly the regular languages.

Here $\mathtt{Str}_{\_}{\mathrm{ST}\lambda}[A]=(A\to A)\to(A\to A)\to(A\to A)$ and $\mathtt{Bool}_{\_}{\mathrm{ST}\lambda}=o\to o\to o$, where $o$ is a base type. This is proved using the semantic evaluation method (see [20] and references therein). To make this method work in our case, we need a new result in denotational semantics:

Lemma 1.7**.**

The second-order affine $\lambda$-calculus ${\mathrm{A}\lambda{}2}$ – i.e. the subsystem of ${\mathrm{EA}\lambda}$ without the exponential modality ‘$\oc$’ – admits a non-trivial finite semantics.

By “non-trivial” we mean distinguishing the two inhabitants of $\mathtt{Bool}=\forall\alpha.\,\alpha\multimap\alpha\multimap\alpha$. The term “second-order” refers to the (impredicative) polymorphism supported by both ${\mu\mathrm{EA}\lambda}$ and ${\mathrm{EA}\lambda}$ – indeed, the types $\mathtt{Bool}$, $\mathtt{Str}$ and $\mathtt{Str}_{\_}S$ all contain second-order quantifiers ($\forall$). The lemma means morally that one cannot represent infinite data types in ${\mu\mathrm{EA}\lambda}$ without using the exponential modality – whereas in ${\mu\mathrm{EA}\lambda}$, the exponential-free type $\mathtt{Str}_{\_}S$ encodes the infinite set $\{0,1\}^{*}$.

Thus, motivated by this question in implicit complexity, we set out to establish the above lemma, and came up with two approaches:

• •

a “category-theoretic” solution consists in showing the finiteness of a pre-existing model based on coherence spaces and normal functors; this is the subject of another paper [16];

• •

a “syntactic” solution, developed in a joint work with P. Pistone, T. Seiller and L. Tortora de Falco, relies on a careful combinatorial study of second-order proof nets; it will be written up in an upcoming paper.

The further development of these semantic tools has led to more results on ${\mathrm{EA}\lambda}$ and/or on Elementary Linear Logic without type fixpoints, which are beyond the scope of the present paper. This includes an already published joint work with P. Pradic [17] on logarithmic space.

Plan of the paper

We recall from [3] the definitions of ${\mathrm{EA}\lambda}$ and ${\mu\mathrm{EA}\lambda}$ in Section 2, and then quickly prove Theorem 1.3 in Section 3. The bulk of the paper is Section 4, dedicated to proving Theorem 1.5. The conclusion (Section 5) discusses the above-mentioned new perspectives on ${\mathrm{EA}\lambda}$ opened up by our results and by refinements of Lemma 1.7.

Acknowledgments

This work owes a great deal to Thomas Seiller’s supervision. Thanks also to Patrick Baillot, Alexis Ghyselen, Damiano Mazza (an extremely fruitful discussion with Thomas and him triggered this work) and Pierre Pradic.

2 The elementary affine $\lambda$-calculus

The syntax of elementary affine $\lambda$-terms and the reduction rules are given by

[TABLE]

where $x$ is taken in a countable set of variables, and $t\{x:=u\}$ refers to the substitution of all free occurrences of $x$ in $t$ by $u$. The reduction rules $\longrightarrow_{\_}\beta$ and $\longrightarrow_{\_}\oc$ are actually the contextual closure of the rules given above, for the obvious notion of context (see [3] for details).

We shall also write $\mathtt{let}\;\oc x\leftarrow u\;\mathtt{in}\;t$ for $(\lambda\oc x.\,t)\,u$ (this is just some “syntactic sugar”). The notion of depth of a subterm in a term, defined as the number of exponential modalities $\oc(-)$ (“exponentials” for short) surrounding the subterm, will play an important role.

As an example, let us formally define the Church-encoded binary strings:

[TABLE]

The above is essentially Simpson’s linear $\lambda$-calculus with thunks [19]. (Other examples of linear $\lambda$-calculi with explicit exponentials are given in [13].) We shall now turn this untyped calculus into ${\mathrm{EA}\lambda}$ by endowing it with its type system – an adaptation of Coppola et al.’s Elementary Type Assignment System [8]. The grammar of types for ${\mathrm{EA}\lambda}$ is

[TABLE]

The two first classes of types are called respectively linear and strictly linear. (We follow the terminology of [3]; “linear” does not mean exponential-free, it merely means that the head connective is not an exponential.) The reason for restricting quantification to strictly linear types is a technical subtlety related to subject reduction (see [8, §7.2]).

The typing judgements involve a context split into three parts: they are of the form $\Gamma\mid\Delta\mid\Theta\vdash t:\sigma$. The idea is that the partial assignements $\Gamma$, $\Delta$ and $\Theta$ of variables to types correspond respectively to linear, non-linear and “temporary” variables; accordingly, $\Gamma$ maps variables to linear types (denoted $A$ above), $\Delta$ maps variables to types of the form $\oc\sigma$, while $\Theta$ maps variables to arbitrary types. The domains of $\Gamma$, $\Delta$ and $\Theta$ are required to be pairwise disjoint. The derivation rules for ${\mathrm{EA}\lambda}$ are:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

In these rules, following the conventions established above, $A$ stands for a linear type, $S$ stands for a strictly linear type and $\sigma$ and $\tau$ stand for arbitrary types. In particular, in the quantifier elimination rule, $\alpha$ can only be instantiated by a linear type. So, for instance, one cannot give the type $\oc\beta\multimap\oc\beta$ to $\lambda x.\,x$ through a quantifier introduction followed by a quantifier elimination; indeed, as one would expect, the only normal term of this type is $\lambda\oc x.\,\oc{x}$. (Despite this, the polymorphism is still impredicative.)

Coming back to the example of Church binary strings, one can show by induction that

[TABLE]

and deduce from this that $\vdash\overline{w}:\mathtt{Str}$ (recall that $\mathtt{Str}=\forall\alpha.\,\oc(\alpha\multimap\alpha)\multimap\oc(\alpha\multimap\alpha)\multimap\oc(\alpha\multimap\alpha)$).

The system ${\mu\mathrm{EA}\lambda}$ is obtained by extending the grammar of types with $S::=\ldots\mid\mu\alpha.\,S$, and adding new derivation rules for the type fixpoint operator $\mu$:

[TABLE]

Let us recall two basic properties satisfied both by ${\mathrm{EA}\lambda}$ and ${\mu\mathrm{EA}\lambda}$, all proved in [3].

Proposition 2.1** (Stratification and linearity [3, Lemma 27]).**

Let $t$ be a typable term.

• •

for any subterm of the form $\lambda\oc x.\,u$ of $t$, all the occurrences of $x$ must be at depth 1 in $u$;

• •

for any subterm $\lambda x.\,u$ of $t$, there is at most one occurrence of $x$ in $u$, whose depth must be 0 in $u$.

As a consequence, the reduction rules are depth-preserving.

Proposition 2.2** **($k$-fold functorial promotion

[3, Proposition 28]).

Let $t:\sigma_{\_}1\multimap\ldots\multimap\sigma_{\_}n\multimap\tau$ is a closed elementary affine $\lambda$-term and $k\geq 1$. There is a term $t^{(k)}:\oc^{k}\sigma_{\_}1\multimap\ldots\oc^{k}\sigma_{\_}n\multimap\oc^{k}\tau$ such that $t^{(k)}\,(\oc^{k}u_{\_}1)\,\ldots\,(\oc^{k}u_{\_}n)$ and $\oc^{k}(t\,u_{\_}1\,\ldots\,u_{\_}n)$ have the same normal form for all closed terms $u_{\_}i:\sigma_{\_}i$ ($i\in\{1,\ldots,n\}$).

3 The $k$-FEXPTIME hierarchy in ${\mu\mathrm{EA}\lambda}$ (proof of

Theorem 1.3)

First, the soundness part of Theorem 1.3 follows immediately from Theorem 1.2.

Proposition 3.1**.**

All functions represented by ${\mu\mathrm{EA}\lambda}$-terms of type $\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Str}$ are in $k$-FEXPTIME.

Proof.

There exists a coercion $\oc\mathtt{Str}\multimap\oc^{2}\mathtt{Str}_{\_}S$ (by completeness part of Theorem 1.2 applied to the identity function in FP) which lifts by functorial promotion (Proposition 2.2) to $\oc^{k+1}\mathtt{Str}\multimap\oc^{k+2}\mathtt{Str}_{\_}S$. So any function represented by a term of type $\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Str}$ is also represented by a term of type $\oc\mathtt{Str}\multimap\oc^{k+2}\mathtt{Str}_{\_}S$. Thus the soundness part of Theorem 1.2 applies. ∎

For the extensional completeness, we also take Theorem 1.2 as our starting point. The idea is to convert $\oc\mathtt{Str}_{\_}S$ into $\mathtt{Str}$ with the help of an auxiliary integer which provides an upper bound on the length of the string. (Similar ideas appear in [4].)

We shall use the type of Church natural numbers and the usual second-order encoding of pairs:

[TABLE]

The aforementioned upper bound will be an inhabitant of the type $\mathtt{Nat}$. An integer $n\in\mathbb{N}$ is represented in $\mathtt{Nat}$ by the iterator $f\mapsto f^{n}$ (formally, $\overline{n}=\lambda\oc f.\,\oc(\lambda x.\,f\,(\ldots(f\,x)\ldots))$ with $n$ times $f$).

To help readability we extend the syntax with the abbreviation

• •

$u\otimes v:=\lambda f.\,f\,u\,v$ so that $u\otimes v:\sigma\otimes\tau$ if $u:\sigma$ and $v:\tau$

given in [3], and introduce some additional syntactic sugar:

• •

$\mathtt{let}\;x\otimes y\leftarrow u\;\mathtt{in}\;t:=u\,(\lambda x.\,\lambda y.\,t)$ for $u:\sigma\otimes\tau$, and $\lambda(x\otimes y).\,t:=\lambda z.\,\mathtt{let}\;x\otimes y\leftarrow z\;\mathtt{in}\;t$

• •

$\mathtt{case}\;u\mid\mathtt{0}x\mapsto a\mid\mathtt{1}y\mapsto b\mid\varepsilon\mapsto c:=u\,(\lambda x.\,a)\,(\lambda y.\,b)\,c$ for $u:\mathtt{Str}_{\_}S$

The affine projections $\pi_{\_}i=\lambda(x_{\_}1\otimes x_{\_}2).\,x_{\_}i$ ($i\in\{1,2\}$) are also defined in [3].

Remark 3.2**.**

Our definition of $\lambda(x\otimes y).\,t$ is much simpler that the one given in [3], but the drawback is that it only works when the type of $t$ is linear, i.e. its head connective is not an exponential. Indeed, $u:\sigma\otimes\tau$ can be instantiated to $u:(\sigma\multimap\tau\multimap A)\multimap A$ by the quantifier elimination rule only when $A$ is linear. This condition will hold in our use cases below.

Now that we are equipped with all these data types, we can make progress on our proof.

Lemma 3.3**.**

There exists a ${\mu\mathrm{EA}\lambda}$-term $\mathtt{cast}:\mathtt{Nat}\multimap\oc\mathtt{Str}_{\_}S\multimap\mathtt{Str}$ which converts a Scott encoding into a Church encoding, provided that the integer argument is greater or equal to the length of the string.

Proof.

Our implementation of $\mathtt{cast}$ instantiates the input $\mathtt{Nat}$ on $(\alpha\multimap\alpha)\otimes\mathtt{Str}_{\_}S$ where $\alpha$ is the eigenvariable of the $\forall$ in the output $\mathtt{Str}$ (recall that $S(\varepsilon)$ refers to the Scott encoding of the empty word):

[TABLE]

[TABLE]

To explain this functional program, let us reformulate it as an imperative algorithm: $t$ can be considered as the body of a for loop which alters two mutable variables $h:(\alpha\multimap\alpha)$ and $u:\mathtt{Str}_{\_}S$. At each iteration, if $u$ is non-empty, its first letter is popped (viewing $u$ as a mutable stack) and $h$ is post-composed with either $f_{\_}0$ or $f_{\_}1$ depending on this letter.

After $n$ iterations starting from $h=(\lambda x.\,x)$ and $u=w$, if $w$ is the Scott encoding of $w_{\_}1\ldots w_{\_}m$, the result obtained is $(f_{\_}{w_{\_}1}\circ\ldots\circ f_{\_}{w_{\_}N})\otimes(S(w_{\_}{N+1}\ldots w_{\_}m))$ where $N=\min(n,m)$. In particular, if $n\geq m$, the first component will be $f_{\_}{w_{\_}1}\circ\ldots\circ f_{\_}{w_{\_}m}$ – which corresponds to the definition of the Church encoding. ∎

To obtain the desired upper bound, we recall a lemma from [3]. It is used in the proof of Theorem 1.2 in order to simulate Turing machines.

Lemma 3.4** ([3]).**

Let $\mathcal{M}$ be a $k$-FEXPTIME Turing machine. There is a ${\mathrm{EA}\lambda}$-term $t_{\_}{\mathcal{M}}:\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Nat}$ computing an upper bound on the running time of $\mathcal{M}$ on the given input string.

We now have all the ingredients for the extensional completeness proof.

Theorem 3.5**.**

All $k$-FEXPTIME functions can be represented by ${\mu\mathrm{EA}\lambda}$-terms of type $\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Str}$.

Proof.

Consider any function computed by a $k$-FEXPTIME Turing machine $\mathcal{M}$. By the completeness part of Theorem 1.2, we can choose a ${\mu\mathrm{EA}\lambda}$-term $f:\oc\mathtt{Str}\multimap\oc^{k+2}\mathtt{Str}_{\_}S$ computing this function. We also choose a term $t_{\_}{\mathcal{M}}$ satisfying the conditions of the above lemma. Then the term

[TABLE]

– where $\mathtt{cast}^{(k+1)}$ is the $(k+1)$-fold functorial promotion of $\mathtt{cast}$ – computes the same function as $\mathcal{M}$. Indeed, the assumption of Lemma 3.3 is satisfied, since for a Turing machine, the length of the output is bounded by the running time. ∎

4 Regular languages in ${\mathrm{EA}\lambda}$ (proof of Theorem 1.5)

In this section, we wish to show that, in ${\mathrm{EA}\lambda}$ (without fixpoints):

• •

all terms $t:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ decide regular languages;

• •

moreover, all regular languages can be decided by terms $t:\mathtt{Str}\multimap\oc\mathtt{Bool}$.

By functorial promotion, the class of languages characterized by $\mathtt{Str}\multimap\oc\mathtt{Bool}$ is included in the class corresponding to $\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$, so this will entail that both are exactly the class of regular languages. The situation is the opposite of the previous section: the second item (extensional completeness) is easy, while the first (soundness) is hard.

Regular languages admit many well-known equivalent definitions, e.g. regular expressions and finite automata (with many variants: non-determinism, bidirectionality, etc.). The classic characterization which will prove useful for us is:

Theorem 4.1**.**

A language is regular if and only if it can be expressed as $\varphi^{-1}(S)$, where $\varphi:\{0,1\}^{*}\to M$ is a monoid morphism, $M$ is a finite monoid and $S\subseteq M$.

4.1 Extensional completeness

Proposition 4.2**.**

All regular languages can be decided by ${\mathrm{EA}\lambda}$-terms of type $\mathtt{Str}\multimap\oc\mathtt{Bool}$.

Proof.

Let $\varphi:\{0,1\}^{*}\to M$ be a morphism to a finite monoid $M$. Without loss of generality, we may assume that the underlying set of $M$ is $\{1,\ldots,k\}$, and the identity element of the monoid is $1$. We represent the monoid elements in ${\mathrm{EA}\lambda}$ as inhabitants of the type $\mathtt{M}=\forall\alpha.\,\alpha\multimap\ldots\alpha\multimap\alpha$; the element $i$ is mapped to the term $m_{\_}i=\lambda x_{\_}1.\,\ldots\,\lambda x_{\_}k.\,x_{\_}i$. We define:

• •

$\delta_{\_}c=\lambda m.\,m\,m_{\_}{\varphi(c)\cdot 1}\,\ldots\,m_{\_}{\varphi(c)\cdot k}:\mathtt{M}\multimap\mathtt{M}$ for $c\in\{0,1\}$

• •

for $S\subseteq M$, $\chi_{\_}S=\lambda m.\,m\,b_{\_}1\,\ldots\,b_{\_}k:\mathtt{M}\multimap\mathtt{Bool}$ where $b_{\_}i=\mathtt{true}$ (resp. $\mathtt{false}$) if $i\in S$ (resp. $i\notin S$).

Then the language $\varphi^{-1}(S)$ is decided by the term $\lambda w.\,\mathtt{let}\;\oc d\leftarrow w\,\oc\delta_{\_}0\,\oc\delta_{\_}1\;\mathtt{in}\;\oc(\chi_{\_}S\,(d\,m_{\_}1))$. ∎

Next, to prepare the ground for our proof of soundness in ${\mathrm{EA}\lambda}$, we review our direct inspiration in the simply typed $\lambda$-calculus: the proof of one direction of Theorem 1.6. The goal is to show that any simply typed $\lambda$-term $t:\mathtt{Str}_{\_}{{\mathrm{ST}\lambda}}[A]\to\mathtt{Bool}_{\_}{\mathrm{ST}\lambda}$, where $A$ is an arbitrary simple type, decides a language $\mathcal{L}_{\_}{\mathrm{ST}\lambda}(t)$ which is regular. This was done using automata in [15], but we find it simpler to work with monoid morphisms (though this is, in the end, merely a different presentation of the same proof).

4.2 A short soundness proof for Hillebrand and Kanellakis’s theorem

(sketch)

We shall omit the subscripts in the types $\mathtt{Str}_{\_}{\mathrm{ST}\lambda}[A]$ and $\mathtt{Bool}_{\_}{\mathrm{ST}\lambda}$ in this subsection.

Let us fix a simple type $A$. The fundamental idea is that, given any denotational semantics \left\llbracket-\right\rrbracket:

• •

the denotation \left\llbracket\overline{w}\right\rrbracket\in\left\llbracket\mathtt{Str}[A]\right\rrbracket of the encoding of $w\in\{0,1\}^{*}$ is enough to determine \left\llbracket t\,\overline{w}\right\rrbracket\in\left\llbracket\mathtt{Bool}\right\rrbracket – this is simply the compositionality of the semantics;

• •

provided the semantics is non-trivial, i.e. \left\llbracket\mathtt{true}\right\rrbracket\neq\left\llbracket\mathtt{false}\right\rrbracket, this subsequently determines $t\,\overline{w}$.

Formally, let us define \varphi_{\_}A:\{0,1\}^{*}\to\left\llbracket\mathtt{Str}[A]\right\rrbracket by \varphi_{\_}A(w)=\left\llbracket\overline{w}\right\rrbracket; then if \left\llbracket-\right\rrbracket is non-trivial,

[TABLE]

To show that $\mathcal{L}_{\_}{\mathrm{ST}\lambda}(t)$ is regular, we shall apply Theorem 4.1 to this equation. We must make sure that:

• •

\left\llbracket\mathtt{Str}[A]\right\rrbracket can be endowed with a monoid structure, in such a way that $\varphi$ is a monoid morphism – this is caused by the use of Church encodings;

• •

\left\llbracket\mathtt{Str}[A]\right\rrbracket is finite – thanks to the existence of a finite semantics for the simply typed $\lambda$-calculus.

Our choice of semantics, to satisfy both conditions, is the usual interpretation of types by mere sets (called the “full type frame” in [15]): \left\llbracket A\to B\right\rrbracket=\left\llbracket B\right\rrbracket^{\left\llbracket A\right\rrbracket}, with \left\llbracket o\right\rrbracket=\{0,1\} for the base type. Any choice for \left\llbracket o\right\rrbracket with at least two elements makes the semantics non-trivial. Furthermore, since \left\llbracket o\right\rrbracket is finite, the denotations of all types are also finite.

Finally, in order to define a monoid structure on \left\llbracket\mathtt{Str}[A]\right\rrbracket, observe that

[TABLE]

where \mathrm{End}(\left\llbracket A\right\rrbracket) is the monoid of maps from \left\llbracket A\right\rrbracket to itself, endowed with function composition. Thus, the right-hand side can be seen as a product of monoids. Proving that $\varphi$ is a morphism can then be done componentwise; the condition to be checked can be expressed as:

[TABLE]

By definition, $\overline{w}=\lambda f_{\_}0.\,\lambda f_{\_}1.\,\lambda x.\,f_{\_}{w_{\_}1}\,(\ldots(f_{\_}{w_{\_}n}\,x)\ldots)$ (where $w=w_{\_}1\ldots w_{\_}n$) so

[TABLE]

therefore $\varphi$ is none other than the product, over all (f_{\_}0,f_{\_}1)\in\mathrm{End}(\left\llbracket A\right\rrbracket)^{2}, of the monoid morphisms \{0,1\}^{*}\to\mathrm{End}(\left\llbracket A\right\rrbracket) defined by $c\mapsto f_{\_}c$ for $c\in\{0,1\}$.

Remark 4.3**.**

This reasoning can be made to work with any finite semantics of ${\mathrm{ST}\lambda}$, not just sets. An interesting choice is the “linearized Scott model”444This model is obtained from a semantics of linear logic as its exponential co-Kleisli category, i.e. via the translation $A\to B:=\oc{A}\multimap B$. The resulting category embeds fully and faithfully into the usual category of Scott domains and continuous functions, hence the name. See [20] for a short self-contained definition.: as remarked by Terui [20], in that semantics, the points in the denotation of a Church-encoded word correspond to nondeterministic finite automata accepting that word. This idea is also at the heart of Grellois and Melliès’s semantic approach to higher-order model checking [12, 11].

4.3 Soundness for regular languages in ${\mathrm{EA}\lambda}$

Our goal is now to emulate the above proof to show that the ${\mathrm{EA}\lambda}$-terms of type $\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ decide regular languages. (The result for $\mathtt{Str}\multimap\oc\mathtt{Bool}$ then follows by functorial promotion.) While the core of the semantic evaluation argument is similar, we need to do some syntactic analysis first before coming to this point.

4.3.1 Some lemmas and a truncation operation

Our proof relies on some general properties of ${\mathrm{EA}\lambda}$. The two following ones were established in [3].

Proposition 4.4** **(Reading property for booleans

[3, Lemma 31(i)]).

The only closed inhabitants of the type $\oc\oc\mathtt{Bool}$ are $\oc\oc\mathtt{true}$ and $\oc\oc\mathtt{false}$. ($\mathtt{true}=\lambda x.\,\lambda y.\,x$ and $\mathtt{false}=\lambda x.\,\lambda y.\,y$)

Proposition 4.5** ($\oc$-inversion [3, Lemma 29(i)]).**

If $\varnothing\mid\Delta\mid\varnothing\vdash t:\oc\sigma$, then $t=\oc{t^{\prime}}$ for some term $t^{\prime}$.

We will also make use of a truncation operation on ${\mathrm{EA}\lambda}$-terms. (To our knowledge, it has not appeared previously in the literature.) Its purpose is to erase all exponentials. This will be how the stratification property of ${\mathrm{EA}\lambda}$ (cf. Proposition 2.1) comes into play.

Definition 4.6**.**

The truncation at depth 0 $\|-\|_{0}$ is defined inductively on terms as:

[TABLE]

and on types as (using the abbreviation555This is justified as $\forall\alpha.\,\alpha\multimap\alpha$ is the unit to the tensor product used in Section 3. $1=\forall\alpha.\,\alpha\multimap\alpha$):

[TABLE]

Proposition 4.7**.**

If a typing judgment $\Gamma\mid\Delta\mid\varnothing\vdash t:\sigma$ is derivable in ${\mathrm{EA}\lambda}$, then, writing $\|\Gamma\|_{0}$ for $x_{\_}1:\|\tau_{\_}1\|_{0},\ldots,x_{\_}n:\|\tau_{\_}n\|_{0}$ if $\Gamma=x_{\_}1:\tau_{\_}1,\ldots,x_{\_}n:\tau_{\_}n$, the judgment $\|\Gamma\|_{0}\mid\varnothing\mid\varnothing\vdash\|t\|_{0}:\|\sigma\|_{0}$ is derivable. In particular, if $t:\sigma$ is a closed term, then $\|t\|_{0}:\|\sigma\|_{0}$.

Proof.

By a mostly straightforward induction on the type derivation. Even so, let us treat a case involving a small subtlety: when the derivation ends with a quantifier elimination. In that case, the induction hypothesis gives us the typing judgment $\|\Gamma\|_{0}\mid\varnothing\mid\varnothing\vdash\|t\|_{0}:\forall\alpha.\,\|S\|_{0}$, and from this we must derive $\|\Gamma\|_{0}\mid\varnothing\mid\varnothing\vdash t:\|S\{\alpha:=\sigma\}\|_{0}$. What the same instantiation rule can give us from our premise is $\|\Gamma\|_{0}\mid\varnothing\mid\varnothing\vdash t:\|S\|_{0}\{\alpha:=\|\sigma\|_{0}\}$. One is therefore led to hope that $\|S\|_{0}\{\alpha:=\|\sigma\|_{0}\}=\|S\{\alpha:=\sigma\}\|_{0}$. Indeed, this can be checked by distinguishing, for each occurrence of $\alpha$ in $\sigma$, two possible cases: either it is at depth 0 and remains in $\|S\|_{0}$, or at depth $\geq 1$ and is erased in $\|S\|_{0}$. ∎

Remark 4.8**.**

The above proof is the reason why we do not generalize here our truncation operation to a “truncation at depth $k$” for $k\geq 1$, which would erase all exponentials of depth $>k$. Indeed, a typical example for which the above reasoning would fail is the truncation at depth 1 of $\forall\alpha.\,\oc\alpha\multimap\alpha$ instantiated with $\alpha:=\oc\tau$. So these higher depths truncations would need additional conditions to be well-behaved.

Proposition 4.9**.**

For all $k\in\mathbb{N}$ and all ${\mathrm{EA}\lambda}$-terms $t,t^{\prime}$, if $t\longrightarrow t^{\prime}$, then $\|t\|_{0}\longrightarrow^{*}\|t^{\prime}\|_{0}$ (this also applies to untyped terms which satisfy the stratification property, i.e. the conclusions of Proposition 2.1).

Proof.

If the redex contracted in $t$ to obtain $t^{\prime}$ is at depth $\geq 1$, then one can prove that $\|t\|_{0}=\|t^{\prime}\|_{0}$.

Otherwise, by induction on the context of the redex, one can restrict to the case where $t=u\,v$ and the application of $u$ to $v$ is the contracted redex. We proceed by case analysis:

• •

If $u=\lambda x.\,u^{\prime}$, then $t^{\prime}=u^{\prime}\{x:=v\}$. We use the fact that $x$ appears only at depth zero in $u^{\prime}$ (Proposition 2.1) to show that $\|u^{\prime}\{x:=v\}\|_{0}=\|u^{\prime}\|_{0}\{x:=\|v\|_{0}\}$. The latter is a reduct of $\|u\|_{0}\,\|v\|_{0}=\|t\|_{0}$.

• •

If $u=\lambda\oc x.\,u^{\prime}$, then $v=\oc{v^{\prime}}$ and $t^{\prime}=u^{\prime}\{x:=v^{\prime}\}$. Moreover, $x$ appears only at depth 1 in $u^{\prime}$ (again by Proposition 2.1). Therefore, $\|u^{\prime}\|_{0}$ does not contain $x$ as a free variable; thus, $\|t^{\prime}\|_{0}=\|u^{\prime}\|_{0}$ is a reduct of $\|t\|_{0}=(\lambda x.\,\|u^{\prime}\|_{0})\,\|v\|_{0}$.∎

A final general observation (unrelated to truncation) before delving into the soundness proof itself:

Proposition 4.10**.**

Let $t$ be a term a free variable $x$. Suppose that $t=t^{\prime}\{x_{\_}1:=x\}\ldots\{x_{\_}n:=x\}$, where each $x_{\_}i$ appears only once in $t^{\prime}$ (so $n$ is the number of occurrences of $x$ in $t$), and $\Gamma\mid\Delta\mid\Theta,x:A\vdash t:\tau$, where $A$ is linear (i.e. not of the form $\oc\sigma$). Then $\Gamma,x_{\_}1:A,\ldots,x_{\_}n:A\mid\Delta\mid\Theta\vdash t:\tau$. We write $t^{\prime}=t\{x:=x_{\_}1,\ldots,x_{\_}n\}$ for this situation. (Such a $t^{\prime}$ always exists given $t$.)

Proof.

By induction on typing derivations, replacing each rule of the form $\ldots\mid\ldots\mid\ldots,x:A\vdash x:\sigma$ by a rule of the form $\ldots,x_{\_}i:A,\ldots\mid\ldots\mid\ldots\vdash x_{\_}i:A$ for some $i\in\{1,\ldots,n\}$. ∎

4.3.2 Syntactic analysis

We can now start looking at the languages decided by ${\mathrm{EA}\lambda}$-terms.

Lemma 4.11**.**

For any ${\mathrm{EA}\lambda}$-term $t:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$, there exists $u:\mathtt{Str}[\sigma_{\_}1]\multimap\ldots\multimap\mathtt{Str}[\sigma_{\_}n]\multimap\oc\mathtt{Bool}$ (for some $n\in\mathbb{N}$) such that, for all $s:\mathtt{Str}$, $t\,\oc s$ and $\oc(u\,s\ldots\,s)$ have the same normal form.

Proof.

First, one may take $t$ to be in normal form. In that case, the only possible redex in $t\,\oc{s}$ is the application at the root. Moreover, $t\,\oc{s}$ must be reducible since it is neither $\oc\oc\mathtt{true}$ nor $\oc\oc\mathtt{false}$, cf. Proposition 4.4. Therefore, $t=(\lambda\oc x.\,t^{\prime})$ (the case $t=(\lambda x.\,t^{\prime})$ can be excluded because then $t$ would be of type $A\multimap\tau$ where $A$ is linear, in particular $A\neq\oc\mathtt{Str}$).

The next step is to prove that $t=\lambda\oc x.\,\oc{t^{\prime\prime}}$ for some ${\mathrm{EA}\lambda}$-term $t^{\prime\prime}$. According to the typing rules, the judgment $\varnothing\mid\varnothing\mid\varnothing\vdash t:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ can only be proven by first establishing $\varnothing\mid x:\oc\mathtt{Str}\mid\varnothing\vdash t^{\prime}:\oc\oc\mathtt{Bool}$. According to the $\oc$-inversion property (Proposition 4.5), since the first and third part of the typing context are empty and the head connective of the type is ‘$\oc$’, $t^{\prime}$ must be of the form $\oc{t^{\prime\prime}}$.

Finally, since $\varnothing\mid\varnothing\mid x:\mathtt{Str}\vdash t^{\prime}:\oc\oc\mathtt{Bool}$ must hold (it is the only premise which can lead to the above judgement on $t^{\prime}$), we can apply Proposition 4.10 to $t^{\prime\prime}$ (indeed, the type $\mathtt{Str}$ is linear). Then, the term $u=\lambda x_{\_}1.\,\ldots\,\lambda x_{\_}m.\,t^{\prime\prime}\{x:=x_{\_}1,\ldots,x_{\_}m\}$ (where $x$ occurs $m$ times in $t^{\prime\prime}$) enjoys the property claimed in the lemma statement. ∎

Let us focus on the case $n=1$ for a moment, and do the same kind of analysis again.

Lemma 4.12**.**

Let $u:\mathtt{Str}[\sigma]\multimap\oc\mathtt{Bool}$ be an ${\mathrm{EA}\lambda}$-term, and let $\tau=\sigma\multimap\sigma$.

There exist ${\mathrm{EA}\lambda}$-terms $f_{\_}0:\tau$, $f_{\_}1:\tau$ and $g:\tau\multimap\ldots\multimap\tau\multimap\oc\mathtt{Bool}$ (with $m$ times $\tau$, for some $m\in\mathbb{N}$) such that for all $s:\mathtt{Str}$, if $s\,\oc{f_{\_}0}\,\oc{f_{\_}1}\longrightarrow^{*}\oc{h}$, then $u\,s$ and $\oc(g\,h\,\ldots\,h)$ have the same normal form.

Proof.

We assume that $u$ is in normal form. Since the head connective of $\mathtt{Str}[\sigma]$ is not ‘$\oc$’, $u=\lambda x.\,v$ and $x:\mathtt{Str}[\sigma]\mid\varnothing\mid\varnothing\vdash v:\oc\mathtt{Bool}$. We may assume that $v$ contains $x$ as a free variable; otherwise, $u$ is a constant function and the conclusion we want holds trivially (take $m=0$).

Let us examine in general the shape of $v:\oc\theta$ in normal form (where $\theta$ is not necessarily $\mathtt{Bool}$) such that $x$ appears free in $v$ and $x:\mathtt{Str}[\sigma]\mid\varnothing\mid\varnothing\vdash v:\oc\theta$. By [3, Lemma 29(ii)], $v$ must be an application: $v=p\,q_{\_}1\,\ldots\,q_{\_}k$ where $p$ is not an application and $k\geq 1$. Observe that $p$ cannot be of the form $\lambda y.\,p^{\prime}$, since $p\,q_{\_}1$ would then be a redex. There are two possible cases:

• •

$p=x$, and then $\theta=\sigma\multimap\sigma=\tau$, $k=2$ and the closed ${\mathrm{EA}\lambda}$-terms $q_{\_}1,q_{\_}2:\oc\tau$ must be of the form $q_{\_}i=\oc{q^{\prime}_{\_}i}$ by $\oc$-inversion (Proposition 4.5)

• •

$p=(\lambda\oc y.\,p^{\prime})$, in which case $x$ must appear free in $q_{\_}1$. Indeed, suppose for the sake of contradiction that $q_{\_}1$ is closed; then $\varnothing\mid\varnothing\mid\varnothing\vdash q_{\_}1:\theta_{\_}1=\oc\rho$ for some $\rho$, therefore $\oc$-inversion gives us $q_{\_}1=\oc{r}$ for some $r$, so $p\,q_{\_}1$ would be a redex.

In the second case, we may furthermore take $k=1$ w.l.o.g.: if $k\geq 2$, then for all $s:\mathtt{Str}[\sigma]$, the term $((\lambda\oc y.\,p^{\prime}\,q_{\_}2\,\ldots\,q_{\_}k)\,q_{\_}1)\{x:=s\}$ has the same normal form as $v\{x:=s\}$ (this is analogous to Regnier’s $\sigma$-equivalence by redex permutations [18]). And since $\varnothing\mid y:\oc\rho\mid\varnothing\vdash p^{\prime}\,q_{\_}2\,\ldots\,q_{\_}k:\oc\theta$, the normal form of $p^{\prime}\,q_{\_}2\,\ldots\,q_{\_}k$ is of the form $\oc{p^{\prime\prime}}$ (this is again an application of $\oc$-inversion).

To recapitulate, either $v=x\,\oc{f_{\_}0}\,\oc{f_{\_}1}$ or $v=(\lambda\oc y.\,\oc{p})\,v^{\prime}=\mathtt{let}\;\oc y\leftarrow v^{\prime}\;\mathtt{in}\;\oc{p}$ where $x$ appears free in $v^{\prime}$, but not in $p$. In the latter case, we have $x:\mathtt{Str}[\sigma]\mid\varnothing\mid\varnothing\vdash v^{\prime}:\oc\theta^{\prime}$. So, by induction on the size of terms,

[TABLE]

As a consequence, for all $s:\mathtt{Str}$, if $s\,\oc{f_{\_}0}\,\oc{f_{\_}1}\longrightarrow^{*}\oc{h}$ (recall that $f_{\_}0,f_{\_}1:\tau$ are closed) then

[TABLE]

(Morally, we are still trying to permute redexes; the reader may check that there is an analogy between the above operation and Carraro and Guerrieri’s $V\,((\lambda x.\,L)\,N)\rightsquigarrow(\lambda x.\,V\,L)\,N$ rule [5] for the call-by-value $\lambda$-calculus.)

Let $r=p_{\_}1\{y_{\_}1:=(\ldots p_{\_}l\{y_{\_}l:=z\}\ldots)\}$, where $z$ is a fresh variable, so that the right-hand side can be written as $\oc(r\{z:=h\})$. Since $h:\tau$ is a closed subterm of $\oc(r\{z:=h\}):\oc\mathtt{Bool}$ (we are using subject reduction here), then it must be true that $\varnothing\mid\varnothing\mid z:\tau\vdash r:\mathtt{Bool}$. Let us now apply Proposition 4.10, using the fact that $\tau=\sigma\multimap\sigma$ is linear: for some $m\in\mathbb{N}$, $z_{\_}1:\tau,\ldots,z_{\_}m:\tau\mid\varnothing\mid\varnothing\vdash r\{z:=z_{\_}1,\ldots,z_{\_}m\}:\mathtt{Bool}$.

Finally, we take $g=\lambda z_{\_}1.\,\ldots\,\lambda z_{\_}m.\,r\{z:=z_{\_}1,\ldots,z_{\_}m\}$. The lemma statement holds with the $f_{\_}0$, $f_{\_}1$, $m$ and $g$ that we have constructed. ∎

The last purely syntactic step is to use the truncation operation to formulate a variation of the above lemma. The point is to be able to decide the membership in the language defined by an ${\mathrm{EA}\lambda}$-term by computing purely in ${\mathrm{A}\lambda{}2}$. This sets the stage for the use of a semantics of ${\mathrm{A}\lambda{}2}$.

Lemma 4.13**.**

Let $u:\mathtt{Str}[\sigma]\multimap\oc\mathtt{Bool}$ be an ${\mathrm{EA}\lambda}$-term, and let $\tau=\|\sigma\multimap\sigma\|_{0}$.

There exist ${\mathrm{A}\lambda{}2}$-terms $f_{\_}0:\tau$, $f_{\_}1:\tau$ and $g:\tau\multimap\ldots\multimap\tau\multimap\oc\mathtt{Bool}$ (with $m$ times $\tau$, for some $m\in\mathbb{N}$) such that for all $w\in\{0,1\}^{*}$, if $\overline{w}\,\oc{f_{\_}0}\,\oc{f_{\_}1}\longrightarrow^{*}\oc{h}$, then $u\,\overline{w}$ and $\oc(g\,h\,\ldots\,h)$ have the same normal form.

(Recall that $\overline{w}:\mathtt{Str}$ is the Church encoding of $w$ in ${\mathrm{EA}\lambda}$.)

Proof.

Thanks to the previous lemma, there exist $f^{\prime}_{\_}0:\sigma\multimap\sigma$, $f^{\prime}_{\_}1:\sigma\multimap\sigma$ and $g^{\prime}:(\sigma\multimap\sigma)\multimap\ldots\multimap(\sigma\multimap\sigma)\multimap\oc\mathtt{Bool}$ with $m$ times $\tau$, for some $m\in\mathbb{N}$, such that the conclusion holds by replacing $\tau$ by $\sigma\multimap\sigma$ and $f_{\_}0,f_{\_}1,g$ by $f^{\prime}_{\_}0,f^{\prime}_{\_}1,g^{\prime}$. The only issue is that $f^{\prime}_{\_}0,f^{\prime}_{\_}1,g^{\prime}$ might not be in ${\mathrm{A}\lambda{}2}$. The idea is therefore to take $f_{\_}0=\|f^{\prime}_{\_}0\|_{0}$, $f_{\_}1=\|f^{\prime}_{\_}1\|_{0}$ and $g=\|g^{\prime}\|_{0}$, and to check that this works.

Let $h^{\prime}:\sigma\multimap\sigma$ be such that $\overline{w}\,\oc{f^{\prime}_{\_}0}\,\oc{f^{\prime}_{\_}1}\longrightarrow^{*}\oc{h^{\prime}}$. Since $\overline{w}=\lambda\oc a_{\_}0.\,\lambda\oc a_{\_}1.\,\oc(\lambda x.\,a_{\_}{w_{\_}1}\,(\ldots(a_{\_}{w_{\_}n}\,x)\ldots))$,

[TABLE]

So if $h$ is such that $\overline{w}\,\oc{f_{\_}0}\,\oc{f_{\_}1}\longrightarrow^{*}\oc{h}$, then by confluence [3, Lemma 8], $h$ and $\|h^{\prime}\|_{0}$ have the same normal form. Therefore, $g\,h\,\ldots\,h$ and $g\,\|h^{\prime}\|_{0}\,\ldots\,\|h^{\prime}\|_{0}$ have the same normal form. But the latter is none other than $\|g^{\prime}\,h^{\prime}\,\ldots\,h^{\prime}\|_{0}$.

To conclude, observe that:

• •

the normal form of $\oc(g^{\prime}\,h^{\prime}\,\ldots\,h^{\prime})$ is the same as that of $u\,\overline{w}$ by the previous lemma;

• •

by Proposition 4.4, the normal form of $g^{\prime}\,h^{\prime}\,\ldots\,h^{\prime}$ is some $b\in\{\mathtt{true},\mathtt{false}\}$;

• •

since $\|b\|_{0}=b$, $\oc\|g^{\prime}\,h^{\prime}\,\ldots\,h^{\prime}\|_{0}$ has the same normal form as $u\,\overline{w}$.

By the discussion above, this means that $\oc(g\,h\,\ldots\,h)$ and $u\,\overline{w}$ have the same normal form, as desired. ∎

4.3.3 Semantic evaluation

We are now ready to conclude our proof of soundness by adapting Hillebrand and Kanellakis’s argument. Let \left\llbracket-\right\rrbracket be any non-trivial finite semantics of ${\mathrm{A}\lambda{}2}$ – the notion of finiteness we need is that \left\llbracket A\right\rrbracket has finitely semantic inhabitants for all ${\mathrm{A}\lambda{}2}$ types $A$. (Equivalently, if our semantics is a category with a terminal object $1$, we require \mathrm{Hom}(1,\left\llbracket A\right\rrbracket) to be finite for all $A$.) Recall that although such a semantics is a central ingredient in our proof, we have simply assumed its existence, which is proved elsewhere (see Lemma 1.7 and the subsequent discussion).

Definition 4.14**.**

Let $A$ be a ${\mathrm{A}\lambda{}2}$ type. We define $\Phi_{A}(w)(\gamma_{\_}0,\gamma_{\_}1)=\gamma_{\_}{w_{\_}1}\circ\ldots\circ\gamma_{\_}{w_{\_}n}$ for $w\in\{0,1\}^{*}$ and (\gamma_{\_}0,\gamma_{\_}1)\in\mathrm{End}(\left\llbracket A\right\rrbracket)^{2}. In other words, \Phi_{\_}{A}:\{0,1\}^{*}\to\mathrm{End}(\left\llbracket A\right\rrbracket)^{\mathrm{End}(\left\llbracket A\right\rrbracket)^{2}} is the monoid morphism sending $c\in\{0,1\}$ to $(\gamma_{\_}0,\gamma_{\_}1)\mapsto\gamma_{\_}c$.

Here \mathrm{End}(\left\llbracket A\right\rrbracket) refers to the monoid of endomorphisms of \left\llbracket A\right\rrbracket in the semantics.

Proposition 4.15**.**

Let $w\in\{0,1\}^{*}$ and $\bar{w}:\mathtt{Str}$ be its encoding. For any ${\mathrm{A}\lambda{}2}$ type $\sigma$ and ${\mathrm{A}\lambda{}2}$-terms $f_{\_}0,f_{\_}1:\sigma\multimap\sigma$, $\bar{w}\,!f_{\_}0\,!f_{\_}1$ normalizes into some $\oc{h}$ with $h:\sigma\multimap\sigma$, and \Phi_{A}(w)(\left\llbracket f_{\_}0\right\rrbracket,\left\llbracket f_{\_}1\right\rrbracket)=\left\llbracket g\right\rrbracket.

Proof.

As in the case of the simply typed $\lambda$-calculus, this is by definition of the Church encoding. ∎

Lemma 4.16**.**

Let $u:\mathtt{Str}[\sigma_{\_}1]\multimap\ldots\multimap\mathtt{Str}[\sigma_{\_}n]\multimap\oc\mathtt{Bool}$.

For all $w_{\_}1,\ldots,w_{\_}n\in\{0,1\}^{*}$, the normal form of $u\,\overline{w_{\_}1}\,\ldots\,\overline{w_{\_}n}$ is completely determined by the functions $\Phi_{\|\sigma_{\_}1\|_{0}}(w_{\_}1),\ldots,\Phi_{\|\sigma_{\_}n\|_{0}}(w_{\_}n)$. As a consequence, the following language is regular:

[TABLE]

Proof.

We start with the case $n=1$, in which $u:\mathtt{Str}[\sigma]\multimap\oc\mathtt{Bool}$. Let $f_{\_}0:\tau$, $f_{\_}1:\tau$ and $g:\tau$ be given by Lemma 4.13, where $\tau=\|\sigma\multimap\sigma\|_{0}=\|\sigma\|_{0}\multimap\|\sigma\|_{0}$. For all $w\in\{0,1\}^{*}$, if $\overline{w}\,f_{\_}0\,f_{\_}1\longrightarrow^{*}\oc{h}$, then $u\,\overline{w}\longrightarrow^{*}b$ for some $b\in\{\mathtt{true},\mathtt{false}\}$ such that $g\,h\,\ldots\,h\longrightarrow^{*}b$. Since $f_{\_}0$, $f_{\_}1$ and $g$ are in ${\mathrm{A}\lambda{}2}$, so is $h$ (provided it is normal), and \left\llbracket g\,h\,\ldots\,h\right\rrbracket=\left\llbracket g\right\rrbracket(\left\llbracket h\right\rrbracket,\ldots,\left\llbracket h\right\rrbracket) by compositionality. Therefore

[TABLE]

thanks to the previous proposition. Since our semantics is non-trivial, i.e. \left\llbracket b\right\rrbracket=\left\llbracket\mathtt{true}\right\rrbracket\iff b=\mathtt{true}, $\Phi_{\|\sigma\|_{0}}(w)$ thus determines the normal form of $u\,\overline{w}$.

The result for arbitrary $n\geq 1$ is obtained by induction on $n$ by repeatedly applying the case $n=1$.

The consequence is that the language $\{w\in\{0,1\}^{*}\mid u\,\overline{w}\,\ldots\,\overline{w}\longrightarrow^{*}\oc\mathtt{true}\}$ can be written using only conditions on $\Phi_{\|\sigma_{\_}i\|_{0}}(w)$ ($i\in\{1,\ldots,n\}$), so it is the preimage of some subset of \prod_{\_}{i=1}^{n}\mathrm{End}(\left\llbracket\sigma_{\_}i\right\rrbracket)^{\mathrm{End}(\left\llbracket\sigma_{\_}i\right\rrbracket)^{2}} by the monoid morphism $w\mapsto(\Phi_{\|\sigma_{\_}1\|_{0}}(w),\ldots,\Phi_{\|\sigma_{\_}n\|_{0}}(w))$. ∎

This suffices to conclude the soundness proof. Let $t:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$. Then, by Lemma 4.11,

[TABLE]

for some $u:\mathtt{Str}[\sigma_{\_}1]\multimap\ldots\multimap\mathtt{Str}[\sigma_{\_}n]\multimap\oc\mathtt{Bool}$. The regularity of this language then follows from the above lemma.

4.4 Overcoming the expressivity barrier

Analyzing the our soundness proof for regular languages in ${\mathrm{EA}\lambda}$ reveals that fundamentally, what restricts the computational power is a conjunction of two facts:

the input $\mathtt{Str}$ is instantiated on some types $\sigma_{\_}1,\ldots,\sigma_{\_}n$ known in advance; 2. 2.

these $\sigma_{\_}i$ are morally finite data types, since they admit finite semantics.

This makes it impossible to iterate over, say, the configurations of a Turing machine, since their size depends on the input and the type $\sigma_{\_}i$ cannot “grow” to accomodate data of variable size.

If we stay at depth 2 in ${\mathrm{EA}\lambda}$, there is no way of avoiding the second fact (one can always truncate the $\sigma_{\_}i$ to exponential-free types), so if we want to retrieve a larger complexity class than regular languages without resorting to type fixpoints, we should try to circumvent the first obstacle. That means that the $\sigma_{\_}i$ should vary with the input. Thus, we are led to consider that inputs should provide types:

• •

the encoding of an input $x$ would be a term $t_{\_}x:\mathtt{Inp}[A_{\_}x]$, for some type $\mathtt{Inp}$ with one parameter;

• •

this $t_{\_}x$ would then be given as argument to a program of type $\forall\alpha.\,\mathtt{Inp}[\alpha]\multimap\mathtt{Bool}$.

In other words, we are considering existential input types. Indeed, if we were to extend ${\mathrm{EA}\lambda}$ with existential quantifiers666The reason this extension is not incorporated is that existentials can be encoded: $\exists\alpha.\,\tau:=\forall\beta.\,(\forall\alpha.\,\tau\multimap\beta)\multimap\beta$., there would be an isomorphism $(\exists\alpha.\,\mathtt{Inp}[\alpha])\multimap\mathtt{Bool}\cong\forall\alpha.\,(\mathtt{Inp}[\alpha]\multimap\mathtt{Bool})$.

Remark 4.17**.**

In fact there is a third fact which plays a role in bridling the complexity: the shape of the type $\mathtt{Str}$ which codes sequential iterations (but the same could be said of Church encodings of free algebras – with such inputs one characterizes regular tree languages).

For instance, let us consider as inputs circuits represented by the type

[TABLE]

where $\oc X$ corresponds to $\mathtt{true}$ constants, $\oc(X\multimap X\multimap X)$ corresponds to $\mathtt{nand}$ gates, and $\oc(X\multimap X\otimes X)$ corresponds to duplication gates used to represent fan-out. Then instantiating this with $X=\mathtt{Bool}$ and the obvious evaluation maps gives us an encoding of the circuit value problem, which is P-complete.

Although this input type seems morally less legitimate than Church encodings, it is hard to pinpoint precisely why it should be rejected.

5 Conclusion

This paper started with a positive result: there exists a characterization of FP and $k$-FEXPTIME in ${\mu\mathrm{EA}\lambda}$ whose statement is very simple. However, the characterization of regular languages in ${\mathrm{EA}\lambda}$, which takes up the rest of the paper, could be seen as a negative result: it demonstrates the lack of expressivity of ${\mathrm{EA}\lambda}$ without type fixpoints. (This is the spirit of Section 4.4.) Indeed, the small class of regular languages not quite a well-behaved complexity class, e.g. it is not closed under $\mathrm{AC}^{0}$ reductions.

That said, one can also read Theorem 1.5 as positive evidence of a connection between affine typing and automata. This connection clearly depends on the use of Church encodings – in other words, on the representation of strings by their iterators. This opens up two avenues for investigation:

• •

One can search for other automata-theoretic classes of interest that can be characterized in ${\mathrm{EA}\lambda}$.

• •

On the other hand, one can hope to obtain a well-behaved sub-polynomial complexity class by changing the representation of inputs, following the suggestions of Section 4.4.

We are currently working on the first research direction, by attempting to capture classes of transductions, i.e. of functions computed by automata with output. As of the time of writing, it seems likely that in ${\mathrm{EA}\lambda}$, $\mathtt{Str}\multimap\mathtt{Str}$ captures the well-known class of regular functions (see [9] for an overview of classical transduction classes, including regular functions), and that the class defined by $\oc\mathtt{Str}\multimap\oc\mathtt{Str}$ also admits an automata-theoretic characterization.

As for the second one, it is the topic of a sequel777This sequel has been published first, although the results in the present paper were mostly obtained before. paper [17] (joint work with P. Pradic) which studies an input type inspired by finite model theory, following Hillebrand’s thesis [14]. We obtain what we believe to be a characterization of deterministic logarithmic space (L), and manage to prove that the class we capture is between L and NL888Actually, a more precise upper bound is L with an oracle for unambiguous non-deterministic logarithmic space..

The importance of semantics

A novelty in our approach is that we betray the original spirit of “light logics” such as Light Linear Logic and Elementary Linear Logic [10], which consisted in bounding the complexity of normalization “geometrically”, independently of types. Here:

• •

geometry still plays an important structuring role, reflected by our use of a “truncation at depth zero” operation, which may be of independent interest;

• •

but our fine-grained analysis also requires to take into account the influence of types through semantics.

Though we are not the first to apply semantics to obtain inexpressivity results in light logics (cf. e.g. [6]), our recent discovery of a finite semantics of linear polymorphism (cf. the discussion below the statement of Lemma 1.7) opens up new possibilities. The above-mentioned sequel on logarithmic space is an illustration of this new way of working in ${\mathrm{EA}\lambda}$ and its variants: the best upper bound that we have is obtained using the effectiveness of the second-order coherence space model studied in [16].

Open questions

Aside from the perspectives already mentioned, there is an obvious question that remains after Theorem 1.5: what about $\oc\mathtt{Str}\multimap\oc^{k+2}\mathtt{Bool}$ (resp. $\oc\mathtt{Str}\multimap\oc^{k+1}\mathtt{Str}$) for $k\geq 1$? For now, what we know about the corresponding complexity class is that:

• •

it is contained in $k$-EXPTIME (resp. $k$-FEXPTIME), since the soundness results for ${\mu\mathrm{EA}\lambda}$ apply a fortiori to ${\mathrm{EA}\lambda}$;

• •

it contains $(k-1)$-EXPTIME (resp. $(k-1)$-FEXPTIME), by adapting the proofs given in [2].

We must confess that we have no idea about what class $\oc\mathtt{Str}\multimap\oc^{k+2}\mathtt{Bool}$ corresponds to, let alone about a proof strategy. Our only guesses is that the first containment is strict, and that semantics can prove useful for this problem.