LIPN, UMR 7030 CNRS, Université Paris 13, Sorbonne Paris Cité, France and
https://nguyentito.eu/nltd@nguyentito.euhttps://orcid.org/0000-0002-6900-5577John
Q. Public and Joan R. Public[500]Theory of computation Linear logic
[500]Theory of computation Denotational semantics [300]Theory of computation
Complexity theory and logic https://arxiv.org/abs/1902.00196 Partially
supported by the French ANR project Elica (ANR-14-CE25-0005).

###### Acknowledgements.

Thomas Seiller made several suggestions to significantly improve the
categorical presentation and conjectured Theorem 2.19. The proof in Section 5
incorporates major simplifications found by Kazushige Terui. Thanks also to
Seng Beng Goh, Thomas Ehrhard, Damiano Mazza, Paul-André Melliès, Paolo
Pistone, Pierre Pradic and Lorenzo Tortora de Falco for instructive
discussions; and to the anonymous reviewers of a previous submission for their
useful feedback.John Q. Open and Joan R. Access 2 42nd Conference on Very
Important Topics (CVIT 2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little
Whinging, United Kingdom 42 23

# Around finite second-order coherence spaces

Lê Thành Dũng Nguyễn

###### Abstract

Many applications of denotational semantics, such as higher-order model
checking or the complexity of normalization, rely on finite semantics for
monomorphic type systems. We exhibit such a finite semantics for a polymorphic
purely linear language: more precisely, we show that in Girard’s semantics of
second-order linear logic using coherence spaces and normal functors, the
denotations of multiplicative-additive formulas are finite.

This model is also effective, in the sense that the denotations of formulas
and proofs are computable, as we show. We also establish analogous results for
a second-order extension of Ehrhard’s hypercoherences; while finiteness holds
for the same reason as in coherence spaces, effectivity presents additional
difficulties.

Finally, we discuss the applications our our work to implicit computational
complexity in linear (or affine) logic. In view of these applications, we
study cardinality and complexity bounds in our finite semantics.

###### keywords:

coherence spaces, finite semantics, hypercoherences, impredicative
polymorphism, multiplicative-additive linear logic, normal functors

###### category:

##  1 Introduction

Polymorphism is a central topic in theoretical computer science since the
sixties. A breakthrough in its logical understanding was its analysis by means
of second order quantifiers, that is the introduction of System F (also known
as the polymorphic $\lambda$-calculus) at the beginning of the seventies. This
considerable success later led Jean-Yves Girard to develop a denotational
semantics for System F [12], to get a deeper understanding of its
computational features. Indeed, the general goal of denotational semantics is
to give a “mathematical” counterpart to syntactic devices such as proofs and
programs, thus bringing to the fore their essential properties. Sometimes this
eventually results in improvements of the syntax: Linear Logic itself [13]
arose precisely from the denotational model introduced in [12].

But denotational semantics is not just a matter of increasing our
understanding of programming languages, it also has direct algorithmic
applications. Let us mention:

  * •

in the simply-typed lambda calculus (${\mathrm{ST}\lambda}$), the _semantic
evaluation_ technique for complexity bounds, see Terui’s recent paper [24] and
references therein;

  * •

in ${\mathrm{ST}\lambda}$ extended with a fixed-point combinator, the semantic
approach to _higher-order model checking_ (HOMC) advocated by Salvati and
Walukiewicz [25, 26] (see also [1, 20]).

The following little-known theorem illustrates both kinds of applications.
Indeed, it is a result in _implicit computational complexity_ : it gives a
machine-free characterization of a complexity class. At the same time, it is
an instance of the correspondence between Church encodings and automata that
HOMC generalizes to infinite trees.

######  Theorem 1.1 (Hillebrand and Kanellakis [19]).

The languages decided by ${\mathrm{ST}\lambda}$ terms from Church-encoded
binary strings to Church booleans, i.e. of type
$\mathtt{Str}_{\mathrm{ST}\lambda}[A]\to\mathtt{Bool}_{\mathrm{ST}\lambda}$,
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$; $o$ is a base type,
while $A$ may be chosen depending on the language one wants to decide.)

To prove this, the main idea is to build a deterministic finite automaton
(DFA) computing the denotation of the input string. Crucially, this relies on
the existence of a _finite semantics_ for ${\mathrm{ST}\lambda}$ – such as the
category of finite sets – which will provide the states of the DFA. In
general, this finiteness property, or finer cardinality bounds, are key to
these applications.

This theorem also holds when replacing ${\mathrm{ST}\lambda}$ by propositional
linear logic, which also admits finite semantics. In fact, Terui’s solution to
the complexity of ${\mathrm{ST}\lambda}$ normalization at fixed order [24]
relies on such a semantics. As for HOMC, Grellois and Melliès have developed
an approach relying on models of linear logic [18, 17].

However, all of this concerns only _monomorphic_ type systems, for a simple
reason: as we shall soon see, _System F does not admit any non-trivial finite
semantics_. A central message of this paper is that second-order
quantification is not the only culprit here: one can also blame _non-
linearity_ , i.e. the possibility of duplicating data. What we show is that a
semantics for a purely linear language with impredicative polymorphism can be
finite:

######  Theorem 1.2.

Second-order Multiplicative-Additive Linear Logic ($\textsc{mall}_{2}$) admits
a non-trivial (i.e. distinguishing the two inhabitants of $1\oplus 1$) finite
semantics.

Recall that $\textsc{mall}_{2}$ is the fragment of second-order linear logic
without the _exponential modalities_ $\oc/\wn$ whose role is to allow111The
possibility of duplication is expressed through the contraction rule $\oc
A\multimap\oc A\otimes\oc A$. a controlled amount of non-linearity. We shall
also prove the analogous property for the second-order _affine_
$\lambda$-calculus.

###  1.1 Some immediate consequences of finite semantics

To illustrate the power of the above theorem, we find it instructive to
explain first the impossibility of finite semantics for System F. It is a
consequence of its ability to represent infinite data types, with definable
destructors.

######  Proposition 1.3.

Let $\mathtt{Nat}_{F}=\forall X.\,(X\to X)\to(X\to X)$ be the type of System F
natural numbers. Then any semantics distinguishing the two inhabitants of the
type of booleans $\mathtt{Bool}_{F}=\forall X.\,X\to X\to X$ is injective on
$\mathtt{Nat}$ – implying the latter has an infinite denotation.

######  Proof 1.4.

For any $n\in\mathbb{N}$, one can define the predicate
$\mathtt{eq}_{n}:\mathtt{Nat}_{F}\to\mathtt{Bool}_{F}$ which tests if its
argument is equal to222We identify natural numbers with their Church encoding.
$n$. Thus, if $m$ and $n$ share the same denotation, then
$\mathtt{eq}_{n}(n)=_{\beta}\mathtt{true}$ and $\mathtt{eq}_{n}(m)$ have the
same denotation. Since we have assumed that $\mathtt{true}$ and
$\mathtt{false}$ have different denotations, this means that
$\mathtt{eq}_{n}(m)=_{\beta}\mathtt{true}$, i.e. $m=n$.

The argument above is robust enough to apply to a wide variety of situations.
For instance, the existence of a finite semantics for ${\mathrm{ST}\lambda}$
immediately yields by contrapositive:

######  Theorem 1.5 (Statman).

Equality is not definable on the Church integers in ${\mathrm{ST}\lambda}$.

Another such situation is the system $\mu$mall: propositional mall with fixed
points [3]. Some functions analogous to $\mathtt{eq}_{n}$ can also be defined
in $\mu$mall, using $\mu X.\,1\oplus X$ as the type of natural numbers. This
leads to a first application of our Theorem 1.2:

######  Theorem 1.6.

There exists no faithful translation from $\mu$mall to $\textsc{mall}_{2}$.

######  Proof 1.7.

Else, $\mu$mall would admit a non-trivial finite semantics, by translating it
into $\textsc{mall}_{2}$ and using the semantics of $\textsc{mall}_{2}$. By
the argument above, this leads to a contradiction.

While $\mu$mall can be translated in full second-order linear logic, it was
argued that both polymorphism and exponentials were required for such a
translation [3, §2.3]. Our finite semantics provides a short rigourous proof
of the necessity of exponentials, and pinpoints the main reason:
_$\textsc{mall}_{2}$ cannot represent infinite data types_.

This divide between $\textsc{mall}_{2}$ and $\mu$mall is further explored in
this paper in the context of implicit complexity; this is discussed in Section
1.3.

######  Remark 1.8.

Although ${\mathrm{ST}\lambda}$ can represent functions on infinite data types
such as integers or strings, this generally involves a meta-level universal
quantification, see e.g. Hillebrand and Kanellakis’s theorem. In
$\textsc{mall}_{2}$, which already contains quantifiers, this way of
sidestepping the issue does not work.

###  1.2 Concrete models: coherence spaces and hypercoherences

It turns out that a finite semantics of $\textsc{mall}_{2}$ has been lying
around all along since the birth of linear logic, though we are not aware of
anyone noticing this fact beforehand. It is none other than Girard’s
_coherence spaces_ [13], which he obtained as a simplification of his previous
work on “qualitative domains” in System F [12], discovering linear logic along
the way.

In this model, open types (i.e. formulas with free variables) are represented
as _normal functors_ 333This categorical tool had been used previously to give
the first quantitative semantics of the $\lambda$-calculus [14] – a work which
is arguably one of the main inspirations for linear logic (linear
$\lambda$-terms are interpreted in this model as monomials of degree 1, hence
“linear”), and even differential linear logic [10].. To prove our finiteness
theorem, we introduce a notion of normal functor of _finite degree_ , which is
preserved by $\textsc{mall}_{2}$ connectives and ensures finiteness. It is
also equivalent to an asymptotic _polynomial growth_ property.

Furthermore, this semantics is more concrete than its formulation using
category-theoretic machinery could suggest. Thanks to a combinatorial
presentation, we prove that it is an _effective_ model: the denotations of
types and terms are computable. Note that historically, effectivity was a
major motivation for using coherence spaces instead of qualitative domains
(see [12, Appendix C], especially Remark C.3).

We also study the interpretation of $\textsc{mall}_{2}$ in Ehrhard’s
_hypercoherences_ [9]. Although it was defined as a model of propositional
linear logic, transposing the recipe of coherence spaces gives a model of
second-order linear logic, with finite denotations for $\textsc{mall}_{2}$
formulas and proofs. In this semantics, effectivity stumbles upon the same
issue as in qualitative domains: roughly speaking, the presence of “$n$-ary
coherences” for arbitrary $n\geq 2$ (while in coherence spaces, $n=2$). We
show that despite this, the hypercoherence model can be made effective for
$\textsc{mall}_{2}$, using a notion of “specification by projections”.

###  1.3 Relevance to implicit computational complexity

The semantic developments we present here have already been applied to obtain
some results on variants of Elementary Linear Logic (ELL) [8]. In this
subsystem of linear logic, purely “geometric” restrictions inspired by the
theory of proof nets enforce complexity constraints, following an approach
pioneered by the characterization of polynomial time in Light Linear Logic
(LLL) [16]. Thanks to our finite semantics, we can apply to second-order ELL
some ideas from another tradition in implicit complexity, exemplified by
Hillebrand and Kanellakis’s Theorem 1.1. (Although some previous works on
“light logics” such as LLL and ELL make use of semantic arguments – for
instance, Statman’s above-mentioned Theorem 1.5 has been applied to LLL in [7]
– to our knowledge these applications have mostly consisted in proving
inexpressivity results for monomorphic systems.)

  * •

In [22], we characterize _regular languages_ in the _elementary affine
$\lambda$-calculus_ [5]; as a side effect, this answers an open question on a
pre-existing characterization of polynomial time (we refer to [22] for further
discussion of the significance of this result). A crucial ingredient is the
existence of a finite semantics of the second-order affine $\lambda$-calculus,
which we shall prove in this paper using coherence spaces.

  * •

In a joint work with P. Pradic [23], we define a class of queries over finite
structures expressed in ELL, which lies between deterministic and non-
deterministic _logarithmic space_. (We also obtain a somewhat contrived exact
characterization of deterministic logarithmic space.) This relies on some
cardinality and complexity bounds on the coherence semantics of
$\textsc{mall}_{2}$, which we establish in the present paper.

As an illustration of the power of finite second-order coherence spaces, we
prove a slight variation of the first item above (regular languages) in the
setting of second-order ELL. By using some specific features of this model, we
get a shorter proof than in [22], which is very close to the proof of Theorem
1.1 by Hillebrand and Kanellakis.

One should note that if we were to enrich ELL with type fixpoints, then,
instead of regular languages, one would obtain a class containing at
least444We believe that this class would be exactly P. But to adapt the P
soundness theorem in [4] to ELL, one would need to work with some notion of
proof net for second-order (elementary) linear logic with additives; since
this is likely to involve technical complications, we have not attempted to do
so. the languages decidable in polynomial time (as can be shown by adapting
the proof of polynomial time completeness in [4]; see also the discussion in
[22]). This gives a quantitative manifestation of the expressivity gap between
$\mu$mall and $\textsc{mall}_{2}$ mentioned earlier in this introduction.

###  1.4 Plan of the paper

We first recall the second-order coherence space model and prove its
finiteness and effectivity for $\textsc{mall}_{2}$ in Section 2. This is
followed by a short discussion, in Section 3, on the adaptation of this finite
semantics to the second-order affine $\lambda$-calculus. We define the second-
order extension of the hypercoherence model in Section 4, and show how to make
it effective.

##  2 Finite and effective second-order coherence spaces

Before we tackle the question of finiteness, we must first recall Girard’s
model of second-order linear logic in coherence spaces. Since this model is
not very well-known, the first two subsections will be expository with no new
results. Finiteness is shown in Section 2.3, and effectivity in Section 2.4.
The omitted proofs of this section are in Appendix A.

#### Syntax

The formulas of _second-order linear logic_ are given by the grammar

$A,B:=X\mid X^{\perp}\mid 1\mid\bot\mid A\otimes B\mid A\parr B\mid
0\mid\top\mid A\oplus B\mid A\with B\mid\forall X.\,A\mid\exists X.\,B\mid\oc
A\mid\wn A$

where $X$ belongs to a fixed countable set of variables. _Propositional_
linear logic is the fragment made of formulas without quantifiers
$\exists/\forall$, while $\textsc{mall}_{2}$ is the fragment without the the
exponential modalities $\oc$/$\wn$.

The involutive _linear negation_ $(-)^{\perp}$ is defined inductively on
formulas by the rules in Figure 1. It is used to define linear implication as
$A\multimap B:=A^{\perp}\parr B$.

Since we work in pre-existing semantics, we do not need to formally define the
notion of denotational model of linear logic; we refer to [21] for an
extensive survey of this topic. We will not be need to work with some precise
proof system – e.g. sequent calculus – either, except in Section 5.

$\begin{array}[]{lcl!\qquad lcl !\qquad
lcl}1^{\bot}&:=&\bot&\bot^{\bot}&:=&1&(\exists X.\,A)^{\bot}&:=&\forall
X.\,A^{\bot}\\\ (A\otimes B)^{\bot}&:=&A^{\bot}\parr B^{\bot}&(A\parr
B)^{\bot}&:=&A^{\bot}\otimes B^{\bot}&(\forall X.\,A)^{\bot}&:=&\exists
X.\,A^{\bot}\\\ 0^{\bot}&:=&\top&\top^{\bot}&:=&0&(\oc A)^{\bot}&:=&\wn
A^{\bot}\\\ (A\oplus B)^{\bot}&:=&A^{\bot}\with B^{\bot}&(A\with
B)^{\bot}&:=&A^{\bot}\oplus B^{\bot}&(\wn A)^{\bot}&:=&\oc
A^{\bot}\end{array}$ Figure 1: Duality for formulas of linear logic.

#### Coherence spaces (propositional case)

Recall that a _coherence space_ is an undirected (reflexive) graph, i.e. a
pair $X=(\mathopen{|}X\mathclose{|},\coh_{X})$ of a set
$\mathopen{|}X\mathclose{|}$ – the _web_ of $X$ – and a symmetric and
reflexive relation
$\coh_{X}\;\subseteq\mathopen{|}X\mathclose{|}\times\mathopen{|}X\mathclose{|}$
– its _coherence relation_. A subset $c\subseteq\mathopen{|}A\mathclose{|}$ is
a _clique_ of $A$ if its points are pairwise coherent for $\coh_{A}$; in this
case we write $c\sqsubset A$.

The operations $(-)^{\perp},\otimes,\oplus,\oc$ are defined on coherence
spaces as follows (cf. [15]):

  * •

$\mathopen{|}X^{\perp}\mathclose{|}=\mathopen{|}X\mathclose{|}$ and
$x\coh_{X^{\perp}}x^{\prime}\iff x\not\coh_{X}x^{\prime}\lor x=x^{\prime}$
(complement graph)

  * •

$\mathopen{|}X\otimes
Y\mathclose{|}=\mathopen{|}X\mathclose{|}\times\mathopen{|}Y\mathclose{|}$ and
$(x,y)\coh_{X\otimes Y}(x^{\prime},y^{\prime})\iff x\coh_{X}x^{\prime}\land
y\coh_{Y}y^{\prime}$

  * •

$\mathopen{|}X\oplus
Y\mathclose{|}=\mathopen{|}X\mathclose{|}\uplus\mathopen{|}Y\mathclose{|}$ and
$z\coh_{A\oplus B}z^{\prime}\iff\exists Z\in\\{X,Y\\}:(z\in Z\land
z^{\prime}\in Z\land z\coh_{Z}z^{\prime})$

  * •

$\mathopen{|}\oc X\mathclose{|}=\\{\text{cliques of $X$}\\}$ and $c\coh_{\oc
X}c^{\prime}\iff c\cup c^{\prime}\sqsubset X$ (“set-based” exponential)

Furthermore, the multiplicative units $1,\bot$ are interpreted as the
singleton space, and the additive units $\top,0$ as the empty space. This is
enough to define inductively the denotation
$\mathopen{\llbracket}A\mathclose{\rrbracket}$ of a formula $A$ in
propositional linear logic, given an assignment of the free variables of $A$
to coherence spaces.

A proof $\pi:A$ is interpreted in the coherence space model as a clique
$\mathopen{\llbracket}\pi\mathclose{\rrbracket}\sqsubset\mathopen{\llbracket}A\mathclose{\rrbracket}$.
In terms of categorical semantics, the model is given as the category
$\mathsf{CohL}$:

  * •

whose objects are coherence spaces;

  * •

whose morphisms between $X$ and $Y$ are cliques in $X\multimap Y$, composition
being relational composition (this is meaningful since $\mathopen{|}X\multimap
Y\mathclose{|}=\mathopen{|}X\mathclose{|}\times\mathopen{|}Y\mathclose{|}$).

###  2.1 Functors on embeddings and uniform families

In order to interpret second-order quantification, we want to give a first-
class status to the map $\\{\text{assignments for variables in
$A$}\\}\to\\{\text{possible values for
$\mathopen{\llbracket}A\mathclose{\rrbracket}$}\\}$ when $A$ is an open type
(i.e. a formula with free variables). The first idea that comes to mind is to
consider it as a functor on $\mathsf{CohL}$. But it stumbles on the fact that
while the binary connectives are _covariant_ bifunctors on $\mathsf{CohL}$,
linear negation is a _contravariant_ endofunctor. Instead, Girard’s idea is to
work in a “category of embeddings” (see [6]) to make negation covariant.

######  Definition 2.1.

An _embedding_ of a coherence space $X$ into a coherence space $Y$ is an
injection $\iota:\mathopen{|}X\mathclose{|}\to\mathopen{|}Y\mathclose{|}$ such
that $x\coh_{X}x^{\prime}\Leftrightarrow\iota(x)\coh_{Y}\iota(x^{\prime})$. We
write $\iota:X\hookrightarrow Y$.

The category $\mathsf{CohI}$ has as objects coherence spaces, and as morphisms
the embeddings.

######  Proposition 2.2.

$(-)^{\perp}$ is a _covariant_ endofunctor of $\mathsf{CohI}$.

######  Proof 2.3.

If $X$ is an induced subgraph of $Y$, then $X^{\perp}$ is an induced subgraph
of $Y^{\perp}$.

######  Remark 2.4.

In the same vein, the graph $\\{(x,\iota(x))\mid
x\in\mathopen{|}X\mathclose{|}\\}$ of an embedding $\iota:X\hookrightarrow Y$
is a clique both in $X\multimap Y$ and in $X^{\perp}\multimap Y^{\perp}$.

Let us say, provisionally, that functors $F:\mathsf{CohI}^{n}\to\mathsf{CohI}$
are our semantical counterpart of open formulas with $n$ variables. A proof of
such a formula should be a family of cliques $c_{X_{1},\ldots,X_{n}}\sqsubset
F(X_{1},\ldots,X_{n})$, “uniform” in some way. The following notion of
uniformity has been called the “mutilation property” by Girard [12]:

######  Definition 2.5.

A family $c_{X_{1},\ldots,X_{n}}\sqsubset F(X_{1},\ldots,X_{n})$ is _uniform_
if for any embeddings $\iota_{i}:X_{i}\hookrightarrow Y_{i}$
($i\in\\{1,\ldots,n\\}$),
$c_{X_{1},\ldots,X_{n}}=F(\iota_{1},\ldots,\iota_{n})^{-1}(c_{Y_{1},\ldots,Y_{n}})$.

######  Remark 2.6.

At this point we have to point out a subtlety of the coherence space model: it
is not a priori obvious that uniformity is closed under composition, in other
words, that the pointwise composition of a uniform clique family for
$F\multimap G$ with a uniform clique family for $G\multimap H$ is uniform for
$F\multimap H$. Indeed, taking $n=1$ for simplicity, the uniformity condition
for a family $f_{X}\sqsubset F(X)\multimap G(X)$ seen as a family of morphisms
is expressed as a diagram

${F(Y)}$${G(Y)}$${F(X)}$${G(X)}$$\scriptstyle{f_{Y}}$$\scriptstyle{G(\iota)^{-}}$$\scriptstyle{F(\iota)^{+}}$$\scriptstyle{f_{X}}$

in $\mathsf{CohL}$, where $j^{+}=\\{(x,j(x))\mid x\in A\\}\sqsubset A\multimap
B$ and $j^{-}=\\{(j(x),x)\mid x\in A\\}\sqsubset B\multimap A$ for
$j:A\hookrightarrow B$. Such diagrams cannot be “formally” pasted
horizontally.

It turns out that uniform clique families _do_ compose, but this issue is non-
trivial and was overlooked in Girard’s papers. A proof is part of the folklore
and often credited to Eugenio Moggi.

######  Remark 2.7.

In the relational semantics of linear logic, in which objects are sets and
morphisms are relations, one could define an analogous notion of uniform
subset family for a functor on the category of injections. But then, for the
uniform families

$c_{S}=\\{*\\}\times S\subseteq\mathopen{\llbracket}1\multimap
X\mathclose{\rrbracket}_{X\mapsto S}\qquad
c^{\prime}_{S}=S\times\\{*\\}\subseteq\mathopen{\llbracket}X\multimap
1\mathclose{\rrbracket}_{X\mapsto S}$

the composition $c^{\prime}_{S}\circ c_{S}$ is _not uniform_ : it is equal to
$\\{(*,*)\\}$ if $S\neq\varnothing$, and $\varnothing$ if $S=\varnothing$.

This issue with the second-order relational model is known and has been
investigated by A. Bac-Bruasse (whose PhD thesis in French [2] is the main
reference on the subject to our knowledge), T. Ehrhard and C. Tasson. What
makes composition work in coherence spaces is the domain-theoretic _stability_
555Stability is indeed a recurring pattern here: the uniformity condition is
reminiscent of Berry’s stable order between functions on domains, and the
preservation of pullbacks in normal functors (next section) is a
categorification of stability. property of morphisms. This is our reason for
working with coherence spaces instead of the simpler relational model.

###  2.2 Normal functors

The next goal is to interpret quantifiers. Let us look at the example of the
formula $X\multimap X$, which admits a proof $\pi$ such that
$\mathopen{\llbracket}\pi\mathclose{\rrbracket}_{X\mapsto S}=\\{(s,s)\mid s\in
S\\}$ for any coherence space $S$. This uniform family should correspond to a
clique in some space $\mathopen{\llbracket}\forall X.\,X\multimap
X\mathclose{\rrbracket}$. The idea is to take some kind of “patterns with
bound variables” as the points of this coherence space. Typically,
$\\{(s,s)\mid s\in S\\}$ should correspond to the single pattern $\langle
x\vdash(x,x)\rangle$ with a bound variable $x$ – and thus to the clique
$\\{\langle x\vdash(x,x)\rangle\\}\sqsubset\mathopen{\llbracket}\forall
X.\,X\multimap X\mathclose{\rrbracket}$. Observe:

  * •

that the substitution of the variable $x$ by $s\in S$ in $(x,x)$ corresponds
to the functoriality of $\mathopen{\llbracket}X\multimap
X\mathclose{\rrbracket}:\mathsf{CohI}\to\mathsf{CohI}$ with respect to the
embedding $\iota:\\{x\\}\hookrightarrow S$ such that $\iota(x)=s$;

  * •

that $(x,x)\in F(\\{x\\})$, and $\\{x\\}$ is “minimal” or “initial” in the
sense that any other $(s,s)\in F(S)$ is an image of $(x,x)$ via an embedding
$\\{x\\}\hookrightarrow S$.

We thus arrive at the idea that “patterns with bound variables” should
correspond to “minimal” spaces. To guarantee their existence, we need to put
an additional condition on our functors $\mathsf{CohI}^{n}\to\mathsf{CohI}$.
This is why Girard interprets open types by _normal functors_.

######  Definition 2.8.

A functor is _normal_ if it preserves filtered colimits and finite pullbacks.

The name comes from Girard’s _normal form theorem_ :

######  Theorem 2.9.

Let $F:\mathsf{CohI}^{n}\to\mathsf{CohI}$ be a functor,
$\mathopen{|}F\mathclose{|}$ be the covariant presheaf obtained by taking the
web, and $\mathsf{El}(\mathopen{|}F\mathclose{|})$ be its category of
elements.

$F$ is normal if and only if, for any object $\vec{X}$ in $\mathsf{CohI}^{n}$
and point $x\in\mathopen{|}F(\vec{X})\mathclose{|}$, the slice category
$\mathsf{El}(\mathopen{|}F\mathclose{|})/(\vec{X},x)$ admits a _finite
initial_ object $(\vec{X^{\prime}},x^{\prime})$.

In this case, $(\vec{X^{\prime}},x^{\prime})$ is initial in its own slice
category. We call an object of $\mathsf{El}(\mathopen{|}F\mathclose{|})$
enjoying this property a _normal form_.

######  Remark 2.10.

It is worth noting that this characterisation is one of many similar results.
For instance, Joyal’s analytic functors have a _weak_ finite normal form
property (i.e. where the initial elements are only weakly initial), a
variation corresponding to preservation of weak pullbacks and filtered
colimits. Similarly, Kock’s characterisation of polynomial functors states
that preservation of wide pullbacks is equivalent to the existence of normal
forms (though not finite); in fact, Girard’s normal functors correspond to
Kock’s _finitary polynomial functors_. See the discussion in [11, §1.18–1.21].

######  Definition 2.11.

Let $F$ be a normal functor. We define $\mathrm{NF}(F)$ to be its set of
isomorphism classes of normal forms (for isomorphisms in
$\mathsf{El}(\mathopen{|}F\mathclose{|})$).

######  Notation 2.12.

We use the notation $\langle\vec{X}\vdash x\rangle$ for normal forms
$(\vec{X},x)\in\mathrm{NF}(F)$. Alternatively, if
$\vec{X}=(X_{1},\ldots,X_{n})$, we may write $\langle X_{1},\ldots,X_{n}\vdash
x\rangle$.

The set $\mathrm{NF}(F)$ summarizes in a way all the webs $|F(\vec{X}|)$ of
the instantiations of $F$, as the proposition below shows. As for the uniform
families of cliques of $F$, they are summarized by the _trace_ of $F$, a
coherence space built from $\mathrm{NF}(F)$.

######  Proposition 2.13.

Let $F:\mathsf{CohI}^{n}\to\mathsf{CohI}$ be a normal functor and
$\vec{X}=(X_{1},\ldots,X_{n})$. Then
$\mathopen{|}F(\vec{X})\mathclose{|}=\\{F(\iota_{1},\ldots,\iota_{n})(y)\mid\langle\vec{Y}\vdash
y\rangle\in\mathrm{NF}(F),\,\iota_{i}:Y_{i}\hookrightarrow
X_{i}\;\text{for}\;i\in\\{1\ldots n\\}\\}$.

######  Definition 2.14.

Let $F:\mathsf{CohI}^{n}\to\mathsf{CohI}$ be a normal functor. We endow
$\mathrm{NF}(F)$ with a non-reflexive coherence relation:
$\langle\vec{X}\vdash x\rangle\coh_{\mathrm{NF}(F)}\langle\vec{Y}\vdash
y\rangle$ when for all $n$-tuples $\vec{Z}$ and all embeddings
$\iota_{\vec{X},i}:X_{i}\hookrightarrow Z_{i}$ and
$\iota_{\vec{Y},i}:Y_{i}\hookrightarrow Z_{i}$,
$F(\iota_{\vec{X},1},\ldots,\iota_{\vec{X},n})(x)\coh_{F(\vec{Z})}F(\iota_{\vec{Y},1},\ldots,\iota_{\vec{Y},n})(y)$.

The _trace_ $\mathrm{Tr}(F)$ is defined as the coherence space made of the
self-coherent normal forms of $F$, equipped with the coherence relation above.

######  Proposition 2.15.

There is a bijection between the cliques $c\sqsubset\mathrm{Tr}(F)$ and the
uniform families of cliques $c_{\vec{X}}\sqsubset F(\vec{X})$ for a normal
functor $F:\mathsf{CohI}^{n}\to\mathsf{CohI}$, given by

$c_{X}=\\{F(\iota_{1},\ldots,\iota_{n})(y)\mid\langle\vec{Y}\vdash y\rangle\in
c,\iota_{i}:Y_{i}\hookrightarrow X_{i}\;\text{for}\;i\in\\{1\ldots n\\}\\}$

This leads to the interpretation of quantifiers. One interprets inductively
any formula of second-order linear logic $A$ with $n$ free variables into a
normal functor
$\mathopen{\llbracket}A\mathclose{\rrbracket}:\mathsf{CohI}^{n}\to\mathsf{CohI}$:
the connectives $\oplus,\otimes,(-)^{\perp}$ extend to “pointwise” operations
on normal functors, and the case $A=\forall X.\,B$ is handled by the operation
introduced below.

######  Proposition 2.16.

Let $F$ be a normal functor $F:\mathsf{CohI}^{n+1}\rightarrow\mathsf{CohI}$.
The map on objects
$\forall(F)(X_{1},\ldots,X_{n})=\mathrm{Tr}(F(X_{1},\dots,X_{n},-))$ extends
to a normal functor $\forall(F):\mathsf{CohI}^{n}\to\mathsf{CohI}$.

###  2.3 Ensuring finiteness: normal functors of finite degree

We now come to our technical contributions, having just finished the
exposition of Girard’s model. This section introduces a notion of _degree_ of
a normal functor, which will witness the finiteness of the interpretation of
$\textsc{mall}_{2}$.

######  Definition 2.17.

Let $F:\mathsf{CohI}^{n}\rightarrow\mathsf{CohI}$ be a normal functor. We
define the degree of $F$ as:

$\deg(F)=\sup\;\\{\mathrm{card}(\mathopen{|}X_{i}\mathclose{|})\mid\langle
X_{1},\ldots,X_{n}\vdash x\rangle\in\mathrm{NF}(F),i\in\\{1,\dots,n\\}\\}.$

We say $F$ is _finite_ if it preserves finiteness of cardinality and is of
finite degree.

Note that a normal functor may have finite but unbounded normal forms, so that
its degree is in fact infinite. Typically, this is the case for the
exponential modalities, which explains why the model is not finite for full
second-order linear logic. We now give two characterizations of finite normal
functors.

######  Proposition 2.18.

A normal functor $F$ is finite if and only if $\mathrm{NF}(F)$ is finite.

######  Theorem 2.19 (Finiteness = polynomial growth).

Let $F:\mathsf{CohI}\rightarrow\mathsf{CohI}$ be a normal functor. There
exists $d\in\mathbb{N}$ s.t.
$\mathrm{card}(\mathopen{|}F(X)\mathclose{|})=\mathcal{O}(\mathrm{card}(\mathopen{|}X\mathclose{|}^{d}))$
if and only if $F$ is a _finite_ normal functor. In that case, $\deg{F}$ is
the smallest such $d$.

For applications such as the one in Section 5, the relevant notion of “finite
semantics” is a model with finite sets of morphisms. Finite normal functors
achieve this requirement.

######  Proposition 2.20.

A finite normal functor has finitely many uniform families of cliques.

######  Proof 2.21.

By Proposition 2.18 together with Proposition 2.15, since
$\mathopen{|}\mathrm{Tr}(F)\mathclose{|}\subseteq\mathrm{NF}(F)$.

To obtain a finite semantics, our goal is therefore to show that inside the
model of coherence spaces and normal functors, the finite ones constitute a
submodel of $\textsc{mall}_{2}$.

######  Proposition 2.22.

If $F$ and $G$ normal functors in $\mathsf{CohI}^{n}\rightarrow\mathsf{CohI}$,
then $\deg{F^{\bot}}=\deg{F}$, $\deg{F\otimes G}=\deg{F}+\deg{G}$, and
$\deg{F\oplus G}=\max\\{\deg{F},\deg{G}\\}$.

######  Proposition 2.23.

For any normal functor $F:\mathsf{CohI}^{n+1}\rightarrow\mathsf{CohI}$,
$\deg{\forall(F)}\leqslant\deg{F}$.

######  Theorem 2.24.

Finite normal functors are closed under $\textsc{mall}_{2}$ connectives.

######  Proof 2.25.

We still need to show that if $F,G:\mathsf{CohI}^{n}\to\mathsf{CohI}$ are
finite normal functors, then $F\oplus G,F\otimes G$ and $\forall(F)$ preserve
finiteness of cardinality. This is immediate for the first two, and the latter
reduces to the case $n=1$: we must show that $\mathrm{Tr}(F)$ is finite. This
follows from Proposition 2.18 since
$\mathopen{|}\mathrm{Tr}(F)\mathclose{|}\subseteq\mathrm{NF}(F)$.

The above results, together with Proposition 2.20, entails the Theorem 1.2
claimed in the introduction. We can be a bit more precise:

######  Corollary 2.26.

Let $A$ be a formula of second-order linear logic. Suppose that in all
subformulas of $A$ of the form $\oc B$ or $\wn B$, any type variable in $B$ is
bound by a quantifier in $B$. Then
$\mathopen{\llbracket}A\mathclose{\rrbracket}$ is a finite normal functor. In
particular:

  * •

this applies when $A$ is a $\textsc{mall}_{2}$ formula;

  * •

when $A$ is closed, $\mathopen{\llbracket}A\mathclose{\rrbracket}$ is a finite
coherence space.

###  2.4 Effectivity properties via a combinatorial description

We are now ready to revisit the example outlined at the start of Section 2.2,
and discuss in more generality the “combinatorial” or “syntactic” presentation
of the $\textsc{mall}_{2}$-definable coherence spaces. Our exposition here is
inspired by the description of normal functors over the category of sets and
injections in [2, §IV.5].

The idea is to see the webs $\mathopen{|}X_{i}\mathclose{|}$ in a normal form
$\langle X_{1},\ldots,X_{n}\vdash x\rangle$ as sets of _bound variables_ in
$x$. Recall that these normal forms are considered up to isomorphism in a
category of elements $\mathsf{El}(\mathopen{|}F\mathclose{|})$; these
isomorphisms should be understood as $\alpha$-renamings. The initiality
condition on normal forms means that all the variables in the
$\mathopen{|}X_{i}\mathclose{|}$ appear free in $x$ – otherwise, one could
take a smaller $X^{\prime}_{i}$. Note that the coherence spaces $X_{i}$
specify not only which variables are bound, but also the coherence relation
between them.

In turn, this $x$ is a syntax tree with binders – indeed the interpretation of
quantifiers uses (unary) normal forms. The $\textsc{mall}_{2}$ connectives
induce a grammar of terms

$x::=a\in\mathrm{Var}\mid(x,x)\mid\mathrm{inl}(x)\mid\mathrm{inr}(x)\mid\langle
X\vdash x\rangle$

where $\mathopen{|}X\mathclose{|}\subset\mathrm{Var}$. The functorial action
of a $\textsc{mall}_{2}$-definable functor $F$ on embeddings then corresponds
to substitution – indeed an embedding $\iota_{i}:X_{i}\hookrightarrow Y_{i}$
is an assignment of variables.

The shape of the term is in fact heavily constrained by the
$\textsc{mall}_{2}$ formula which $F$ interprets. With this point of view, one
sees that $\deg(F)$ is the maximum number of leaves which a syntax tree in
$\mathrm{NF}(F)$ can have.

With such a concrete description it becomes easier to see how one can compute
operations on these variable types and cliques. For instance:

######  Proposition 2.27.

For any $\textsc{mall}_{2}$-definable functor $F$, the non-reflexive coherence
relation on $\mathrm{NF}(F)$ (Definition 2.14) is decidable.

This may be used to establish the _effectivity_ of our finite semantics of
$\textsc{mall}_{2}$:

######  Theorem 2.28.

The function sending a $\textsc{mall}_{2}$ formula $A$ to
$\mathrm{Tr}(\mathopen{\llbracket}A\mathclose{\rrbracket})$ is computable.
Futhermore, the function taking a formula $A$ and a proof $\pi:A$ as input and
returning the clique of
$\mathrm{Tr}(\mathopen{\llbracket}A\mathclose{\rrbracket})$ corresponding to
the uniform family
$\mathopen{\llbracket}\pi\mathclose{\rrbracket}(\vec{X})\sqsubset\mathopen{\llbracket}A\mathclose{\rrbracket}(\vec{X})$
is computable.

######  Theorem 2.29.

Let $F:\mathsf{CohI}^{n}\to\mathsf{CohI}$ be a fixed
$\textsc{mall}_{2}$-definable finite normal functor.

  * •

The function $\vec{X}\mapsto F(\vec{X})$ is computable in _logarithmic space_.

  * •

For any $c\sqsubset\mathrm{Tr}(F)$, the function $\vec{X}\mapsto
c_{\vec{X}}\sqsubset F(\vec{X})$ is computable in _logarithmic space_.

Since the output of a logarithmic space algorithm has polynomial size, this is
consistent with Theorem 2.19.

##  3 A finite semantics of the second-order affine $\lambda$-calculus

Let us discuss briefly how to adapt our finite coherence semantics from
$\textsc{mall}_{2}$ to its intuitionistic affine variant. Indeed, the
existence of a finite semantics for this variant is used in one of the
applications to implicit complexity mentioned in the introduction [22].

The starting point is to give a semantics of the propositional affine
$\lambda$-calculus. To do so, the natural idea is to use the well-known notion
of affine function space between coherence spaces: $X\rightarrowtriangle
Y=(X\multimap Y)\with Y$, so that every clique $c\sqsubset
X\rightarrowtriangle Y$ can be written uniquely as the disjoint union
$c=c_{1}\sqcup c_{2}$ of a linear function from $X$ to $Y$ ($c_{1}\sqsubset
X\multimap Y$) and a constant part ($c_{2}\sqsubset Y$). Composition is
defined as666Fore $r\subseteq S\times T$ and $s\subseteq S$, $r(s)$ denotes
$\\{y\mid\exists x\in s:(x,y)\in r\\}$; this generalizes function composition
and can be seen as a degenerate case of relational composition.
$c^{\prime}\circ_{\mathrm{aff}}c=(c^{\prime}_{1}\circ
c_{1})\sqcup(c^{\prime}_{2}\cup c^{\prime}_{1}(c_{2}))$ for $c\sqsubset
X\rightarrowtriangle Y$ and $c^{\prime}\sqsubset Y\rightarrowtriangle Z$.
Coherence spaces and affine functions form a category $\mathsf{CohA}$ which
can also be seen as the Kleisli category for the comonad $(-\with 1)$, via the
isomorphism $(X\multimap Y)\with Y\cong(X\with 1)\multimap Y$.

One issue is that this category does not quite fit into the definition of a
“symmetric monoidal closed category with terminal unit”, which is the usual
notion of denotational model for the affine $\lambda$-calculus. The reason is
that it does not admit a monoidal product $*$ such that, for any coherence
space $B$, $(-*B)$ is left adjoint to $(B\rightarrowtriangle-)$. Let us review
the two main candidates:

  * •

$*=\otimes$ fails: morally, an affine function from $A\otimes B$ can either
use both $A$ and $B$ or none of them, but not one out of the two;

  * •

$A*B=(A\with 1)\otimes(B\with 1)$ almost works, except for the fact that it is
not associative777A similar problem afflicts the treatment of intuitionistic
disjunction in domain-theoretic models..

To sidestep this issue, we do not attempt to interpret an affine tensor
product – it does not exist anyway in the syntax of the affine
$\lambda$-calculus (in practice, one uses the second-order encoding888Whose
interpretation in our coherence space semantics coincides with $(A\with
1)\otimes(B\with 1)$. $A\odot B=\forall X.\,(A\rightarrowtriangle
B\rightarrowtriangle X)\rightarrowtriangle X$). Instead, we give a semantics
in a “closed multicategory”. In the absence of a well-established theory of
multicategorical models of typed $\lambda$-calculi and their extension with
second-order quantification, we merely give a concrete interpretation of
second-order affine $\lambda$-terms.

An affine type in the grammar $A,B::=X\mid A\rightarrowtriangle B\mid\forall
X.\,A$ with $n$ type variables is interpreted as a normal functor
$\mathsf{CohI}^{n}\to\mathsf{CohI}$ by induction:

$\mathopen{\llbracket}A\rightarrowtriangle B\mathclose{\rrbracket}=(A\with
1)\multimap B\qquad\mathopen{\llbracket}\forall
X.\,A\mathclose{\rrbracket}=\forall(\mathopen{\llbracket}A\mathclose{\rrbracket})$

An affine $\lambda$-term $t:B$ with $m$ free variables
$x_{1}:A_{1},\ldots,x_{m}:A_{m}$ is mapped to a uniform family
$\mathopen{\llbracket}t\mathclose{\rrbracket}(\vec{X})\sqsubset(\mathopen{\llbracket}A_{1}\mathclose{\rrbracket}(\vec{X})\with
1)\otimes\ldots\otimes(\mathopen{\llbracket}A_{m}\mathclose{\rrbracket}(\vec{X})\with
1)\multimap\mathopen{\llbracket}B\mathclose{\rrbracket}(\vec{X})$. The details
are unsurpring and are given in Appendix B.

######  Remark 3.1.

One could try instead to use the Eilenberg–Moore category of coalgebras for
the comonad $(-\with 1)$ instead of its Kleisli category. But in that case,
even though the monoidal product can be defined, the function space cannot.

##  4 Hypercoherences

The remainder of the paper is dedicated to applying the ideas we developed in
coherence spaces to Ehrhard’s _hypercoherence_ [9] model of linear logic. To
our knowledge, the treatment of quantifiers in hypercoherences has not
appeared in the literature, but it is easily constructed by analogy with
coherence spaces, as we do in Section 4.1. As mentioned in the introduction,
obtaining an effective model will be harder than in the case of coherence
spaces, and this is where most of our energy will be spent (Section 4.2). Some
proofs are in Appendix C.

######  Notation 4.1.

Given a set $S$, we write $\mathcal{P}_{\mathrm{fin}}(S)$ (resp.
$\mathcal{P}_{\mathrm{fin}}^{*}(S)$) for the set of finite (resp. finite non-
empty) subsets of $S$. An alternative notation for
$S^{\prime}\in\mathcal{P}_{\mathrm{fin}}(S)$ (resp.
$S^{\prime}\in\mathcal{P}_{\mathrm{fin}}^{*}(S)$) is
$S^{\prime}\subseteq_{\mathrm{fin}}S$ (resp.
$S^{\prime}\subseteq_{\mathrm{fin}}^{*}S$).

Recall that a _hypercoherence_ $X$ is a pair $(|X|,\Gamma(X))$ where $|X|$ is
a set and $\Gamma(X)\subseteq\mathcal{P}_{\mathrm{fin}}^{*}(S)$ contains all
singletons ($\forall x\in|X|,\,\\{x\\}\in\Gamma(X)$). Equivalently, one could
specify a hypercoherence $X$ by the data of $|X|$ and
$\Gamma^{**}(X)=\Gamma(X)\setminus\\{\\{x\\}\mid x\in|X|\\}$. A subset $c$ of
$|X|$ is a _clique_ of $X$ (as in coherence spaces, this is denoted
$c\sqsubset X$) if $\mathcal{P}_{\mathrm{fin}}^{*}(c)\subseteq\Gamma(X)$.

Hypercoherences support the following operations:

  * •

$X^{\perp}=(|X|,\mathcal{P}_{\mathrm{fin}}^{*}(X)\setminus\Gamma^{**}(X))$

  * •

$X\otimes
Y=(|X|\times|Y|,\\{S\mid\pi_{1}(S)\in\Gamma(X)\land\pi_{2}(S)\in\Gamma(Y)\\})$

  * •

$X\oplus Y=(|X|+|Y|,\mathsf{inl}(\Gamma(X))\cup\mathsf{inr}(\Gamma(Y))$

As in coherence spaces, one builds a category $\mathsf{HCohL}$ whose objects
are hypercoherences and whose morphisms between $X$ and $Y$ are the cliques of
$X\multimap Y=(X\otimes Y^{\perp})^{\perp}$. These morphisms are composed by
relational composition.

###  4.1 Variable and second-order hypercoherences

We follow the recipe of coherence spaces to extend this model to
$\textsc{mall}_{2}$.

An _embedding_ $X\hookrightarrow Y$ of hypercoherences is an injection
$|X|\hookrightarrow|Y|$ which preserves both coherence and incoherence of
subsets (equivalently, the graph of the injection is both a morphism
$X\multimap Y$ and a morphism $X^{\perp}\multimap Y^{\perp}$). (Similarly, if
$S\subseteq|X|$, the sub-hypercoherence of $X$ _induced by $S$_ is
$(S,\mathcal{P}_{\mathrm{fin}}^{*}(S)\cap\Gamma(X))$.)

######  Definition 4.2.

The category $\mathsf{HCohI}$ has hypercoherences as objects, and embeddings
as morphisms. A $n$-parameter _variable hypercoherence_ is a normal functor
$\mathsf{HCohI}^{n}\to\mathsf{HCohI}$.

A variable hypercoherence $F$ is _(weakly) finite_ if $\mathrm{NF}(F)$ is
finite – as in coherence spaces, $\mathrm{NF}(F)$ is defined from the presheaf
$|F|$. Its _degree_ $\deg(F)$ is defined as in Definition 2.17.

######  Definition 4.3.

Let $F:\mathsf{HCohI}^{n}\to\mathsf{HCohI}$ be a variable hypercoherence. A
family $c_{X_{1},\ldots,X_{n}}\sqsubset F(X_{1},\ldots,X_{n})$ is _uniform_ if
for any embeddings $\iota_{i}:X_{i}\hookrightarrow Y_{i}$
($i\in\\{1,\ldots,n\\}$),
$c_{X_{1},\ldots,X_{n}}=F(\iota_{1},\ldots,\iota_{n})^{-1}(c_{Y_{1},\ldots,Y_{n}})$.

######  Proposition 4.4.

For all $n\in\mathbb{N}$, the $n$-parameter variable hypercoherences and
uniform families of cliques form a category $\mathsf{HCohL}(n)$ which is a
model of propositional mall.

The $n=0$ case is $\mathsf{HCohL}(0)=\mathsf{HCohL}$. As we saw in Remark 2.6,
it is not quite trivial to show that $\mathsf{HCohL}(n)$ is a category, but
since the morphisms in $\mathsf{HCohL}$ enjoy the domain-theoretic _stability_
property, the proof used in the case of coherence spaces applies _mutatis
mutandis_.

Now we wish to define a notion of trace $\mathrm{Tr}(F)$ of a normal functor
$F$ to interpret $\forall$. The fundamental thing to ensure is the adjunction
(usual in categorical semantics)

$\mathsf{HCohL}(n)(A,\forall(F))\cong\mathsf{HCohL}(n+1)(\mathrm{Const}(A),F)$

where $\mathrm{Const}$ is a “weakening” map sending a $n$-parameter
hypercoherence to a $(n+1)$-parameter one. This reduces to the case999If one
were to specialize this further to
$\mathsf{HCohL}(0)(1,\mathrm{Tr}(F))\cong\mathsf{HCohL}(1)(1,F)$ – i.e. the
cliques of $\mathrm{Tr}(F)$ are in bijection with the variable cliques of $F$
– then it would not determine $\mathrm{Tr}(F)$ uniquely, unlike the case of
coherence spaces: in general, the structure of a hypercoherence cannot be
fully recovered from its domain of cliques. That said, the adjunction defining
$\mathrm{Tr}(-)$ can be derived from this bijection between cliques together
with $\mathrm{Tr}(\mathrm{Const}(A)\multimap F)\cong A\multimap\mathrm{Tr}(F)$
(i.e. commutation between $\forall$ and $\parr$). $n=0$:
$\mathsf{HCohL}(A,\mathrm{Tr}(F))\cong\mathsf{HCohL}(1)(\mathrm{Const}(A),F)$.
So $\mathrm{Tr}$, being an adjoint functor, is unique up to natural
isomorphism101010An isomorphism $X\cong Y$ in $\mathsf{HCohL}$ is just a
bijection from $|X|$ to $|Y|$ sending $\Gamma(X)$ to $\Gamma(Y)$. (if it
exists); we can just state the definition – mimicking coherence spaces – and
check that the adjunction holds.

######  Definition 4.5.

For $x\in|F(X)|$, $\mathrm{NF}(x;F)$ denotes (the isomorphism class of) the
normal form of $x$. For $S\subseteq|F(X)|$, $\mathrm{NF}(S;F)$ is the direct
image of $S$ by the function $\mathrm{NF}(-;F)$.

######  Definition 4.6.

Let $F$ be a one-parameter variable hypercoherence.
$N\subseteq_{\mathrm{fin}}^{*}\mathrm{NF}(F)$ is said to be coherent when for
any $X$ and any $S\subseteq_{\mathrm{fin}}^{*}|F(X)|$, if $\mathrm{NF}(S;F)=N$
then $S\in\Gamma(F(X))$. The set of coherent sets of normal forms is denoted
by $\Gamma\mathrm{NF}(F)$.

The _trace_ of $F$ (notation: $\mathrm{Tr}(F)$) is the hypercoherence defined
by

$|\mathrm{Tr}(F)|=\\{x\in\mathrm{NF}(F)\mid\\{x\\}\in\Gamma\mathrm{NF}(F)\\}\quad\Gamma(\mathrm{Tr}(F))=\mathcal{P}_{\mathrm{fin}}^{*}(\mathrm{Tr}(F))\cap\Gamma\mathrm{NF}(F)$

and from this we define $\forall(G):\vec{X}\mapsto\mathrm{Tr}(G(\vec{X},-))$
for $G:\mathsf{HCohI}^{n+1}\to\mathsf{HCohI}$.

One can then routinely check that the adjunction holds. We therefore conclude:

######  Theorem 4.7.

Variable hypercoherences and uniform families of cliques form a semantics of
second-order linear logic. Furthermore, by restricting to weakly finite
variable hypercoherences, we obtain a finite semantics of $\textsc{mall}_{2}$.

###  4.2 Strong finiteness and effectivity

Unfortunately, the model of weakly finite variable hypercoherences is _not
effective_. Let us give an exemple: let $f:\mathbb{N}\to\\{0,1\\}$ be any
function, and

$F_{f}(X)=(|X|,\\{S\subseteq_{\mathrm{fin}}^{*}|X|\mid
f(\mathrm{Card}(S))=1\\})$

This map on objects can be extended to a functor
$F_{f}:\mathsf{HCohI}\to\mathsf{HCohI}$ which is in fact a weakly finite
variable hypercoherence. But if $f$ is uncomputable, then
$X\mapsto\Gamma(F_{f}(X))$ also is.

We are therefore seeking an additional condition on variable hypercoherences
which would both guarantee effectivity and be preserved by $\textsc{mall}_{2}$
connectives. More precisely, our goal is to exhibit a class of variable
hypercoherences $F$ such that $\Gamma(F)$ can be described canonically by some
finite data – just as $\mathrm{NF}(F)$ fulfills this role for $|F|$ when $F$
is weakly finite. This is the purpose of the following defintions.

######  Definition 4.8.

Let $F$ be a $n$-parameter variable hypercoherence and $1\leq k\leq n$.

For any $P\subseteq\mathrm{NF}(F)$, a _projection from $P$_ on the $k$-th
parameter is a dependent function

$f:(\langle X_{1},\ldots,X_{n}\vdash x\rangle\in P)\to|X_{k}|$

i.e. it is a function $f$ defined on $P$ such that $f(\langle
X_{1},\ldots,X_{n}\vdash x\rangle)\in|X_{k}|$. The set of projections from $P$
on the $k$-th parameter is written $\mathrm{Proj}_{k}(P)$.

Any $f\in\mathrm{Proj}_{k}(P)$ induces a family of functions indexed by
hypercoherences $Y_{1},\ldots,Y_{n}$

$f^{F}_{Y_{1},\ldots,Y_{n}}:\\{y\in|F(Y_{1},\ldots,Y_{n})|\mid\mathrm{NF}(y;F)\in
P\\}\to|Y_{k}|$

as follows: let $\mathrm{NF}(y;F)=\langle X_{1},\ldots,X_{n}\vdash x\rangle\in
P$, then $F(\iota_{1},\ldots,\iota_{n})(x)=y$ for some (unique) embeddings
$\iota_{i}:X_{i}\hookrightarrow Y_{i}$; one then takes
$f^{F}_{Y_{1},\ldots,Y_{n}}(y)$ to be $\iota_{k}(f(x))$.

By direct image, this induces a family of functions

$f^{F}_{Y_{1},\ldots,Y_{n}}:\\{S\subseteq_{\mathrm{fin}}^{*}|F(Y_{1},\ldots,Y_{n})|\mid\mathrm{NF}(S;F)=P\\}\to\mathcal{P}_{\mathrm{fin}}^{*}(|Y_{k}|)$

Note that this could be extended to “$\mathrm{NF}(S;F)\subseteq P$” but most
uses of this direct image will happen with $\mathrm{NF}(S;F)=P$.

We also write
$\mathrm{Proj}(P)=\mathrm{Proj}_{1}(P)\cup\ldots\cup\mathrm{Proj}_{n}(P)$.

######  Notation 4.9.

Given a hypercoherence $X$ and $S\subseteq_{\mathrm{fin}}^{*}|X|$, we define
$l_{X}(S)$ to be $\odot$ if $S$ is a singleton, $\ominus$ if
$S\in\Gamma^{**}(X)$, $\oplus$ if $S\in\Gamma^{**}(X^{\perp})$.

(Mnemonic: $l_{A\oplus B}(S\cup T)=\oplus$ for all non-empty $S\subseteq|A|$
and $T\subseteq|B|$.)

Our eventual goal is to specify variable hypercoherences using projections as
follows: given $S\subseteq_{\mathrm{fin}}^{*}|F(\vec{Y})|$,
$l_{F(\vec{Y})}(S)$ should be determined by the
$l_{Y_{k}}(f^{F}_{\vec{Y}}(S))$ for $f\in\mathrm{Proj}_{k}(\mathrm{NF}(S;F))$,
$k\in\\{1,\ldots,n\\}$, following a sort of “truth table”. However, to make
this specification canonical, one should ensure that all “rows” in the table
are meaningful, i.e. serve to determine the (in)coherence of at least one
$S\subseteq_{\mathrm{fin}}^{*}|F(\vec{Y})|$ for some $\vec{Y}$. This is the
purpose of the following.

######  Definition 4.10.

Let $F$ be a $n$-parameter variable hypercoherence, and
$P\subseteq\mathrm{NF}(F)$. We write $\mathrm{Val}(P)$ for the set of
_valuations_ on $P$, that is, of functions
$\mathrm{Proj}(P)\to\\{\odot,\ominus,\oplus\\}$.

A valuation $v$ on $P$ is _possible_ when there exist hypercoherences
$Y_{1},\ldots,Y_{n}$ and a subset $S\subseteq|F(Y_{1},\ldots,Y_{n})|$ such
that $\mathrm{NF}(S;F)=P$ and $v(f)=l_{Y_{k}}(f^{F}_{Y_{1},\ldots,Y_{n}}(S))$
for $f\in\mathrm{Proj}_{k}(P,F)$. The set of possible valuations on $P$ is
denoted $\mathrm{PVal}(P)$.

######  Definition 4.11.

A _specification by projections_ of $F$ is a dependent function

$\sigma_{F}:(P\in\mathcal{P}_{\mathrm{fin}}^{*}(\mathrm{NF}(F)))\to\mathrm{PVal}(P)\to\\{\odot,\ominus,\oplus\\}$

such that, for all $Y_{1},\ldots,Y_{n}\in\mathsf{HCohL}$ and
$S\subseteq_{\mathrm{fin}}^{*}|F(Y_{1},\ldots,Y_{n})|$,

$l_{F(Y_{1},\ldots,Y_{n})}(S)=\sigma_{F}(\mathrm{NF}(S;F),(f\in\mathrm{Proj}_{k}(\mathrm{NF}(S;F))\mapsto
l_{Y_{k}}(f^{F}_{Y_{1},\ldots,Y_{n}}(S))))$

A variable hypercoherence is _strongly finite_ if it is weakly finite and
admits a specification by projections. (Note that if a specification by
projections exists for $F$, it is unique.)

To justify the terminology, observe that for a weakly finite $F$, there are
finitely many $P\subseteq_{\mathrm{fin}}^{*}\mathrm{NF}(F)$ and the sets
$\mathrm{Proj}_{k}(P,F)$ are finite. Therefore, if $F$ admits a specification
by projections, then this specification is a finite object, and so $\Gamma(F)$
is finitely described. This notion successfully excludes pathological examples
such as our $F_{f}$ above:

######  Proposition 4.12.

If $F:\mathsf{HCohI}^{n}\to\mathsf{HCohI}$ is strongly finite, then
$\vec{X}\mapsto F(\vec{X})$ is computable.

######  Proof 4.13.

All projections are computable, so it suffices to precompute a table encoding
the specification, and to look up the relevant row.

######  Remark 4.14.

Our definition of specification by projections is very restrictive. For
instance, if $\langle\varnothing,\ldots,\varnothing\vdash x\rangle\in
P\subseteq_{\mathrm{fin}}^{*}\mathrm{NF}(F)$ and $\mathrm{Card}(P)\geq 2$,
then the $S\subseteq_{\mathrm{fin}}^{*}|F(\vec{Y})|$ such that
$\mathrm{NF}(S;F)=P$ are either all coherent or all incoherent, independently
of $\vec{Y}$.

We still need to show that strongly finite variable hypercoherences are closed
under all $\textsc{mall}_{2}$ connectives, and that the interpretations of
$\textsc{mall}_{2}$ formulas and proofs can be effectively computed. The main
lemma is:

######  Lemma 4.15.

There exists a criterion to determine, given
$P\subseteq_{\mathrm{fin}}^{*}\mathrm{NF}(F)$ and $v\in\mathrm{Val}(P)$,
whether the valuation $v$ is possible; this criterion is effective when $F$ is
weakly finite. Note that $F$ is not part of the input; that means that
$\mathrm{PVal}(P)$ depends only on $P$, not on any other information on $F$.

######  Proposition 4.16.

The normal functors $(X_{1},\ldots,X_{k})\mapsto A$ and
$(X_{1},\ldots,X_{n})\mapsto X_{k}$ admit specifications by projections (and
are therefore strongly finite).

######  Proposition 4.17.

If the $n$-parameter variable hypercoherences $F$ and $G$ can be specified by
projections, then it is also the case for $F^{\perp}$, $F\otimes G$ and
$F\oplus G$. Furthermore, if $F$ and $G$ are finite, then
$\sigma_{F^{\perp}}$, $\sigma_{F\otimes G}$ and $\sigma_{F\oplus G}$ are
computable from $\sigma_{F}$ and $\sigma_{G}$.

In the above proposition, finiteness may refer to either weak or strong
finiteness: since we assume specifiability by projections, those two notions
become equivalent by definition.

######  Proposition 4.18.

If $F\in\mathsf{HCohL}(n+1)$ admits a specification by projections, then so
can $\forall(F)\in\mathsf{HCohL}(n)$. Furthermore, the function
$(\mathrm{NF}(F),\sigma_{F})\mapsto(\mathrm{NF}(\forall(F)),\sigma_{\forall(F)})$
defined on finite $F$ is computable.

From these propositions, we see that
$A\mapsto\mathopen{\llbracket}A\mathclose{\rrbracket}$ is computable in the
second-order hypercoherence model. Since
$(\pi:A)\mapsto\mathopen{\llbracket}\pi\mathclose{\rrbracket}\sqsubset\mathopen{\llbracket}A\mathclose{\rrbracket}$
is computable for essentially the same reasons as in coherence spaces, we may
conclude:

######  Theorem 4.19.

Strongly finite variable hypercoherences form an effective model of
$\textsc{mall}_{2}$.

##  5 Application: characterizing regular languages

Next, we illustrate the usefulness of our finite semantics of
$\textsc{mall}_{2}$ on the following theorem.

######  Definition 5.1.

We consider the “stratified” Church encoding of strings: $\mathtt{Str}=\forall
X.\mathtt{Str}[X]$, where $\mathtt{Str}[X]=\oc(X\multimap
X)\multimap\oc(X\multimap X)\multimap\oc(X\multimap X)$.

Given a proof $\pi:\oc\mathtt{Str}\multimap\oc^{k}\mathtt{Bool}$ (with111111We
also take $\mathtt{true}$ (resp. $\mathtt{false}$) to be the proof of $1\oplus
1$ proving the left (resp. right) occurrence of $1$. $\mathtt{Bool}=1\oplus
1$), the language decided by $\pi$ is defined as121212$\pi(\overline{w})$
denotes the proof obtained by applying a cut to $\pi$ and $\overline{w}$, and
$\oc^{k}\mathtt{true}$ is the proof consisting of $k$ promotion rules with
empty context applied to $\mathtt{true}$; cf. the sequent calculus recalled in
Appendix D.
$\mathcal{L}(\pi)=\\{w\in\\{0,1\\}^{*}\mid\pi(\overline{w})\longrightarrow^{*}\oc^{k}\mathtt{true}\\}$,
where $\overline{w}$ is the Church encoding of $w$.

######  Theorem 5.2.

The type $\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ in _second-order
Elementary Linear Logic ( $\textsc{ell}_{2}$)_ captures the class of _regular
languages_. In other words, the languages that can be expressed as
$\mathcal{L}(\pi)$ for some proof
$\pi:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ in $\textsc{ell}_{2}$ are
exactly the regular languages.

Roughly speaking, $\textsc{ell}_{2}$ is a subsystem of full second-order
linear logic where the rules governing the exponential modalities are
restricted: promotion and dereliction are removed, and replaced with
_functorial promotion_ : from $\vdash A_{1},\ldots,A_{n},B$, infer $\vdash\wn
A_{1},\ldots,\wn A_{n},\oc B$. This induces a sort of “stratification” on
formulas and proofs, which is the reason why the number of $\oc$ modalities in
the output type of an $\textsc{ell}_{2}$ function is significant.

The formal definition of $\textsc{ell}_{2}$ is given in Appendix D. Some parts
of the proof of Theorem 5.2 are also relegated to this section of the
appendix. To summarize:

  * •

By encoding deterministic finite automata as proofs of
$\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$, we show that every regular
language can be decided by such a proof.

  * •

Using the aforementioned stratification property of $\textsc{ell}_{2}$, we
reduce the converse (only regular languages can be decided) to the lemma
below. This reduction involves a “truncation at depth $k$” operation, similar
to the one defined in [22] for the elementary affine $\lambda$-calculus, which
might be of independent interest.

The lemma whose proof features coherence spaces actually applies to full
second-order linear logic (with unrestricted exponentials). This is because
the “geometric” properties specific to $\textsc{ell}_{2}$ have already been
exploited in the previous step.

######  Lemma 5.3.

Let
$\pi:\mathtt{Str}[A_{1}]\otimes\ldots\otimes\mathtt{Str}[A_{n}]\multimap\mathtt{Bool}$
be a proof in second-order linear logic where $A_{1},\ldots,A_{n}$ are closed
$\textsc{mall}_{2}$ formulas. Then the following language is regular:

$\\{w\in\\{0,1\\}^{*}\mid\pi(\overline{w}[A_{i}]\otimes\ldots\otimes\overline{w}[A_{n}])\longrightarrow^{*}\mathtt{true}\\}$

where $\overline{w}[A_{i}]:\mathtt{Str}[A_{i}]$ is the instantiation of
$\overline{w}$ on $A_{i}$.

######  Proof 5.4.

Let $B=\mathtt{Str}[A_{1}]\otimes\ldots\otimes\mathtt{Str}[A_{n}]$. By
Corollary 2.26, we know that $\mathopen{\llbracket}B\mathclose{\rrbracket}$ is
a finite coherence space. Indeed, if a subformula of $B$ is the form $\oc C$,
then it cannot be a subformula of some $A_{i}$ since the $A_{i}$ are
$\textsc{mall}_{2}$ formulas, so $C=A_{i}\multimap A_{i}$ for some
$i\in\\{1,\ldots,n\\}$. Since $A_{i}$ is closed, the premise of Corollary 2.26
holds.

Let $x\in\\{0,1\\}$. The operation “add a $x$ at the end of the string” is
definable by a proof $\mathtt{snoc}^{x}_{X}$ of
$\mathtt{Str}[X]\multimap\mathtt{Str}[X]$. From this, we can derive
$\mathtt{snoc}^{x}_{A_{1},\ldots,A_{n}}:B\multimap B$. This allows us to
define a deterministic finite automaton (writing $\varepsilon$ for the empty
string):

  * •

whose states are the cliques of
$\mathopen{\llbracket}B\mathclose{\rrbracket}$, with initial state
$q_{I}=\mathopen{\llbracket}\overline{\varepsilon}[A_{1}]\otimes\ldots\otimes\overline{\varepsilon}[A_{n}]\mathclose{\rrbracket}$;

  * •

whose transition function is
$\delta(x,q)=\mathopen{\llbracket}\mathtt{snoc}^{x}_{A_{1},\ldots,A_{n}}\mathclose{\rrbracket}(q)$
for $x\in\\{0,1\\}$;

  * •

whose accepting states are $\\{q\sqsubset
B\mid\mathopen{\llbracket}\hat{\pi}\mathclose{\rrbracket}(q)=\mathopen{\llbracket}\mathtt{true}\mathclose{\rrbracket}\\}$.

Thanks to the compositionality of the coherence space model, when the DFA
reads a word $w\in\\{0,1\\}$, it ends in the state
$\mathopen{\llbracket}\overline{w}\mathclose{\rrbracket}$. This state is
accepting if and only if
$\mathopen{\llbracket}\hat{\pi}(\overline{w})\mathclose{\rrbracket}=\mathopen{\llbracket}\mathtt{true}\mathclose{\rrbracket}$;
since the semantics is injective on $\mathtt{Bool}$, the DFA recognizes the
language we want.

##  6 Conclusion

Motivated by applications to implicit complexity, we sought a finite semantics
for $\textsc{mall}_{2}$, and obtained it by proving the finiteness of the pre-
existing model of coherence spaces and normal functors. In retrospect, this is
not so surprising: one advantage of coherence spaces (e.g. over Scott
domains), that had already been stressed early in their history, is their
tendency to give small and legible interpretations to formulas.

Another early observation by Girard was that the existential introduction in
this model has a non-trivial computational contents, subsuming the cut rule –
this was mentioned as being “key to a semantic approach to computation” [13,
p. 57]. By going from $A[T]$ to $\exists X.\,A$, the information of the
witness $T$ is compressed into some bounded data, and this is why the
semantics can be finite. Let us reformulate this from the programming language
point of view on existential types as abstract data types: the cliques of
$\mathopen{\llbracket}\exists X.\,A\mathclose{\rrbracket}$ keep just enough
information about the cliques of
$\mathopen{\llbracket}A[T]\mathclose{\rrbracket}$ they originate from to
determine their interaction with the generic (universally typed) programs
which might use them.

Relatedly, observe that the syntactic model of propositional mall is finite,
and the existential witnesses are the only reason why this is not the case in
$\textsc{mall}_{2}$. One could also try to directly implement the above
intuitions starting from the syntax; this will be the subject of an upcoming
paper with P. Pistone, T. Seiller and L. Tortora de Falco.

Aside from finiteness, the present work also investigated in detail the
question of effectivity. Almost no effort is needed in the case of coherence
spaces, but to obtain an effective hypercoherence model of
$\textsc{mall}_{2}$, we had to introduce the idea of specifications by
projections.

## References

  * [1] Klaus Aehlig.  A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata.  Logical Methods in Computer Science, 3(3), July 2007.  doi:10.2168/LMCS-3(3:1)2007.
  * [2] Alexandra Bac-Bruasse.  Logique linéaire indexée du second ordre.  PhD thesis, Université Aix-Marseille II, December 2001.
  * [3] David Baelde.  Least and Greatest Fixed Points in Linear Logic.  ACM Transactions on Computational Logic, 13(1):1–44, January 2012\.  doi:10.1145/2071368.2071370.
  * [4] Patrick Baillot.  On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy.  Information and Computation, 241:3–31, April 2015.  doi:10.1016/j.ic.2014.10.005.
  * [5] Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca.  Characterizing polynomial and exponential complexity classes in elementary lambda-calculus.  Information and Computation, 261:55–77, August 2018.  doi:10.1016/j.ic.2018.05.005.
  * [6] Thierry Coquand.  Categories of embeddings.  Theoretical Computer Science, 68(3):221–237, November 1989.  doi:10.1016/0304-3975(89)90161-8.
  * [7] Ugo Dal Lago and Patrick Baillot.  On light logics, uniform encodings and polynomial time.  Mathematical Structures in Computer Science, 16(4):713–733, August 2006.  doi:10.1017/S0960129506005421.
  * [8] Vincent Danos and Jean-Baptiste Joinet.  Linear logic and elementary time.  Information and Computation, 183(1):123–137, May 2003.  doi:10.1016/S0890-5401(03)00010-5.
  * [9] Thomas Ehrhard.  Hypercoherences: a strongly stable model of linear logic.  Mathematical Structures in Computer Science, 3(04):365, December 1993.  doi:10.1017/S0960129500000281.
  * [10] Thomas Ehrhard.  An introduction to differential linear logic: proof-nets, models and antiderivatives.  Mathematical Structures in Computer Science, pages 1–66, February 2017.  doi:10.1017/S0960129516000372.
  * [11] Nicola Gambino and Joachim Kock.  Polynomial functors and polynomial monads.  Mathematical Proceedings of the Cambridge Philosophical Society, 154(01):153–192, January 2013.  arXiv: 0906.4931.  doi:10.1017/S0305004112000394.
  * [12] Jean-Yves Girard.  The system F of variable types, fifteen years later.  Theoretical Computer Science, 45:159–192, January 1986.  doi:10.1016/0304-3975(86)90044-7.
  * [13] Jean-Yves Girard.  Linear logic.  Theoretical Computer Science, 50(1):1–101, January 1987.  doi:10.1016/0304-3975(87)90045-4.
  * [14] Jean-Yves Girard.  Normal functors, power series and $\lambda$-calculus.  Annals of Pure and Applied Logic, 37(2):129–177, February 1988\.  doi:10.1016/0168-0072(88)90025-5.
  * [15] Jean-Yves Girard.  Linear logic: its syntax and semantics.  In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Notes. Cambridge University Press, 1995.
  * [16] Jean-Yves Girard.  Light Linear Logic.  Information and Computation, 143(2):175–204, June 1998.  doi:10.1006/inco.1998.2700.
  * [17] Charles Grellois.  Semantics of linear logic and higher-order model-checking.  PhD thesis, Univeristé Denis Diderot Paris 7, April 2016.  URL: https://tel.archives-ouvertes.fr/tel-01311150/.
  * [18] Charles Grellois and Paul-André Melliès.  Relational Semantics of Linear Logic and Higher-order Model Checking.  In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), pages 260–276, 2015.  doi:10.4230/LIPIcs.CSL.2015.260.
  * [19] Gerd G. Hillebrand and Paris C. Kanellakis.  On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi.  In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 253–263. IEEE Computer Society, 1996.  doi:10.1109/LICS.1996.561337.
  * [20] Martin Hofmann and Jérémy Ledent.  A cartesian-closed category for higher-order model checking.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, Reykjavik, Iceland, June 2017. IEEE.  doi:10.1109/LICS.2017.8005120.
  * [21] Paul-André Melliès.  Categorical semantics of linear logic.  In Interactive Models of Computation and Program Behaviour, number 27 in Panoramas et Synthèses, pages 1–196. Société Mathématique de France, 2009.
  * [22] Lê Thành Dũng Nguyễn.  On the elementary affine $\lambda$-calculus with and without type fixpoints.  Submitted, 2019.  URL: https://nguyentito.eu/ealreg.pdf.
  * [23] Lê Thành Dũng Nguyễn and Pierre Pradic.  From normal functors to logarithmic space queries.  In 46th International Colloquium on Automata, Languages and Programming (ICALP’19), pages 151:1–151:15, 2019.  doi:10.4230/LIPIcs.ICALP.2019.151.
  * [24] Kazushige Terui.  Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus.  In 23rd International Conference on Rewriting Techniques and Applications (RTA’12), pages 323–338, 2012.  doi:10.4230/LIPIcs.RTA.2012.323.
  * [25] Igor Walukiewicz and Sylvain Salvati.  Using models to model-check recursive schemes.  Logical Methods in Computer Science, Volume 11, Issue 2, June 2015\.
  * [26] Igor Walukiewicz and Sylvain Salvati.  Typing weak MSOL properties.  Logical Methods in Computer Science, Volume 13, Issue 1, March 2017\.

##  Appendix A Omitted proofs of Section 2

######  Proof A.1 (Proof of Proposition 2.18).

($\Longrightarrow$) There are finitely many coherence spaces of cardinality
$\leq\deg(F)$, and their images by $F$ are all finite since $F$ preserves
finiteness.

($\Longleftarrow$) $\deg(F)$ is the supremum of a finite subset of
$\mathbb{N}$ and is therefore finite.

######  Proof A.2 (Proof of Theorem 2.19).

Note that $\mathrm{Card}(|F(X)|)=O(\mathrm{Card}(|X|)^{d})$ implies that $F$
sends finite spaces to finite spaes. Thus, in the remainder of this proof, we
assume that $F$ preserves finiteness of cardinality (otherwise, an equivalence
between two false propositions is true). With this assumption, it suffices to
prove that

$\deg(F)=\inf\\{d\in\mathbb{N}\mid\mathrm{Card}(|F(X)|)=O(\mathrm{Card}(|X|)^{d})\\}$

We decompose this equality into two inequalities.

($\leq$) Let $\langle X^{0}\vdash x\rangle\in\mathrm{NF}(F)$ and
$d=\mathrm{Card}(|X^{0}|)$. Let $[n]=1\&\ldots\&1$ ($n$ times). For all $n$,
there are $n^{d}$ embeddings $X^{0}\hookrightarrow X^{0}\otimes[n]$ which are
the identity on the first component. If for two such embeddings $\iota$ and
$\iota^{\prime}$, $F(\iota)(x)=F(\iota^{\prime})(x)$, then by uniqueness of
the normal form $\iota$ and $\iota^{\prime}$ are isomorphic in the slice
category $\mathsf{CohI}/(X^{0}\otimes[n])$; in the commuting triangle
$\iota=\rho\circ\iota^{\prime}$, $\rho$ can only be the identity, since our
considered family of embeddings differ only on the component $[n]$, and so
$\iota=\iota^{\prime}$. Thus, $\iota\mapsto F(\iota)(x)$ is injective over the
$n^{d}$ embeddings we consider, and therefore
$\mathrm{Card}(|F(X^{0}\otimes[n])|)\geq n^{d}$ while
$\mathrm{Card}(|X^{0}\otimes[n]|)=dn$.

($\geq$) We assume $d=\deg(F)<\infty$ (when $\deg(F)=\infty$, the inequality
is true for trivial reasons). This entails that $\mathrm{NF}(F)$ is finite, by
Proposition 2.18. Now let $X$ be a finite coherence space of cardinality $n$;
each point $x\in|F(X)|$ has a normal form, so $\mathrm{Card}(|F(X)|)$ can be
bounded by summing over $\langle X^{0}\vdash x\rangle\in\mathrm{NF}(F)$ the
number of possible embeddings of $X^{0}$ in $X$. This number is at most
$O(n^{\mathrm{Card}(X^{0})})$ and by definition $\mathrm{Card}(X^{0})\leq d$.
In the end, using $\mathrm{Card}(\mathrm{NF}(F))=O(1)$, we get
$\mathrm{Card}(|F(X)|)=O(n^{d})$.

######  Proof A.3 (Proof of Proposition 2.22).

The case of negation is straightforward as
$\mathopen{|}F(X_{1},\dots,X_{n})\mathclose{|}=\mathopen{|}F^{\bot}(X_{1},\dots,X_{n})\mathclose{|}$.
For the $\oplus$ case, one easily checks that $\mathrm{NF}(F\oplus
G)\cong\mathrm{NF}(F)\uplus\mathrm{NF}(G)$.

Only the $\otimes$ case needs to be carefully checked. Consider
$\langle\vec{Z}\vdash(x,y)\rangle\in\mathrm{NF}(F\otimes G)$, and the
corresponding normal forms $\langle\vec{X}\vdash x\rangle\in\mathrm{NF}(F)$
and $\langle\vec{Y}\vdash y\rangle\in\mathrm{NF}(G)$. Then one can show, from
minimality of $\vec{Z}$, that131313For legibility purposes, we assume that $F$
preserves inclusions, and work with inclusions instead of embeddings; also,
all operations are applied componentwise on the $n$-tuples $\vec{X}$,
$\vec{Y}$, $\vec{Z}$. $\vec{X}\cup\vec{Y}\subseteq\vec{Z}$. Moreover, since
$x\in F(\vec{Z})$ and $y\in G(\vec{Z})$, we have
$\vec{X}\cup\vec{Y}\supseteq\vec{Z}$. Thus $\vec{X}\cup\vec{Y}=\vec{Z}$ and
$\deg{(F\otimes G)}\leqslant\deg{F}+\deg{G}$. The converse inequality is
obtained by noticing that if $\langle\vec{X}\vdash x\rangle\in\mathrm{NF}(F)$
and $\langle\vec{Y}\vdash y\rangle\in\mathrm{NF}(G)$, then
$\langle\vec{X}\oplus\vec{Y}\vdash(x,y)\rangle\in\mathrm{NF}(F\otimes G)$.

######  Proof A.4 (Proof of Proposition 2.23).

Suppose that $\langle Y_{1},\dots,Y_{n}\vdash\langle X_{1}\vdash
x\rangle\rangle\in\mathrm{NF}(\forall(F))$. It suffices to check that $\langle
Y_{1},\dots,Y_{n},X_{1}\vdash x\rangle\in\mathrm{NF}(F)$.

######  Proof A.5 (Proof of Theorem 2.29).

For each point $x\in\theta_{X}$, there is a unique $(\iota,y)$ such that
$F(\iota)(y)=x$; indeed, it is the initial object of the slice category
$\mathsf{El}(\mathopen{|}F\mathclose{|})/(X,x)$. So we have a bijection

$\theta_{X}\cong\\{(\iota,y)\mid\langle Y\vdash y\rangle\in\theta,\iota:Y\to
X\text{ embedding}\\}$

This bijection is computable in logarithmic space: it is just a matter of
performing substitutions on terms of size $O(1)$ (since $F$ is fixed),
although the $\iota$’s are not of constant size (because of the representation
of elements of $\mathopen{|}X\mathclose{|}$). Therefore the problem is reduced
to enumerating the right-hand side without repetitions.

There are finitely many $\langle Y\vdash y\rangle$ in $\theta$. For each of
them, each injection $Y\to X$ can be represented by
$\mathrm{card}(\mathopen{|}Y\mathclose{|})\leq\deg(F)=O(1)$ elements of
$\mathopen{|}X\mathclose{|}$: this takes
$O(\log\mathrm{card}(\mathopen{|}X\mathclose{|}))$ space. Thus, all the
injections can be enumerated in logarithmic space, and for each injection,
whether it is an embedding can be determined in logarithmic space (using the
coherence relation on $\mathrm{Tr}(F)$ which may be precomputed independently
of the input.)

##  Appendix B Details for Section 3

##  Appendix C Omitted proofs of Section 4

##  Appendix D Details and proofs for Section 5

$\text{(functorial promotion)}\frac{\vdash\Gamma,A}{\vdash\wn\Gamma,\oc
A}\qquad\text{(weakening)}\frac{\vdash\Gamma}{\vdash\Gamma,\wn
A}\qquad\text{(contraction)}\frac{\vdash\Gamma,\wn A,\wn A}{\vdash\Gamma,\wn
A}$ Figure 2: Exponential rules for the $\textsc{ell}_{2}$ sequent calculus.
In the functorial promotion rule, when $\Gamma=B_{1},\ldots,B_{k}$,
$\wn\Gamma$ stands for $\wn B_{1},\ldots,\wn B_{k}$.
$\displaystyle\text{({ax}-rule)}\frac{}{\vdash A,A^{\bot}}\qquad\text{(cut
rule)}\frac{\vdash\Gamma,A\quad\vdash
A^{\bot},\Delta}{\vdash\Gamma,\Delta}\qquad\text{(exchange
rule)}\frac{\vdash\Gamma,A,B,\Delta}{\vdash\Gamma,B,A,\Delta}$
$\displaystyle\text{($\otimes$-rule)}\frac{\vdash\Gamma,A\quad\vdash
B,\Delta}{\vdash\Gamma,A\otimes
B,\Delta}\qquad\text{($\parr$-rule)}\frac{\vdash\Gamma,A,B}{\vdash\Gamma,A\parr
B}\qquad\text{($\bot$-rule)}\frac{\vdash\Gamma}{\vdash\Gamma,\bot}\qquad\text{($1$-rule)}\frac{}{\vdash
1}$
$\displaystyle\text{($\oplus$-rule)}\frac{\vdash\Gamma,A_{i}}{\vdash\Gamma,A_{1}\oplus
A_{2}}\text{\footnotesize for
$i\in\\{1,2\\}$}\qquad\text{($\with$-rule)}\frac{\vdash\Gamma,A\quad\vdash\Gamma,B}{\vdash\Gamma,A\with
B}\qquad\text{($\top$-rule)}\frac{}{\vdash\Gamma,\top}$
$\displaystyle\text{($\exists$-rule)}\frac{\vdash\Gamma,A[B/X]}{\vdash\Gamma,\exists
X.\,A}\qquad\text{($\forall$-rule)}\frac{\vdash\Gamma,A}{\vdash\Gamma,\forall
X.\,A}\text{\footnotesize for $X$ not free in $\Gamma$}$ Figure 3: Rules for
the $\textsc{mall}_{2}$ sequent calculus (there is no rule for $0$).
$\begin{array}[]{r !\qquad!\leadsto!\qquad l}\text{ \ignorespaces
\ignorespaces \ignorespaces \ignorespaces\ignorespaces\leavevmode\lower
49.25775pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 10.15556pt\hbox{\hskip
4.0pt\hbox{ }\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to31.64444pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$A,A^{\perp}$}\hskip
4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 7.28876pt\hbox{\hskip
4.0pt\hbox{$\pi$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to28.27779pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$A,\Delta$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to74.37599pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 23.0491pt\hbox{\hbox{\hskip
4.0pt\hbox{$A,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}&\text{ \ignorespaces
\ignorespaces\leavevmode\lower 25.38887pt\hbox{\vbox{\hbox{\hskip
7.28876pt\hbox{\hskip 4.0pt\hbox{$\pi$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to28.27779pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$A,\Delta$}\hskip 4.0pt}}}}
\ignorespaces}\\\ \text{ \ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\leavevmode\lower
73.9044pt\hbox{\vbox{\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
8.73593pt\hbox{\hskip 4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 10.35489pt\hbox{\hskip
4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to37.21005pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma^{\prime},B$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to85.63597pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 9.56023pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Gamma^{\prime},A\otimes B$}\hskip
4.0pt}}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
2.31252pt\vbox{\hbox{\hskip 20.79877pt\hbox{\hskip 4.0pt\hbox{$\pi_{3}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to58.09782pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp},B^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to62.72284pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash A^{\perp}\parr
B^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
9.56023pt\lower-0.2pt\hbox{}\hbox
to153.25235pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 62.66644pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Gamma^{\prime},\Delta$}\hskip 4.0pt}}}}}
\ignorespaces}&\text{ \ignorespaces \ignorespaces \ignorespaces \ignorespaces
\ignorespaces \ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
73.9044pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 8.73593pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\vbox{\hbox{\hskip
10.35489pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to37.21005pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma^{\prime},B$}\hskip 4.0pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 20.79877pt\hbox{\hskip
4.0pt\hbox{$\pi_{3}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to58.09782pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
B^{\perp},A^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to109.76164pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 28.0803pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash A^{\perp},\Gamma^{\prime},\Delta$}\hskip 4.0pt}}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to130.10725pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 41.53366pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Gamma^{\prime},\Delta$}\hskip 4.0pt}}}}}
\ignorespaces}\\\ \text{ \ignorespaces \ignorespaces \ignorespaces
\ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
73.18219pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 10.15448pt\vbox{\hbox{\hskip
8.73593pt\hbox{\hskip 4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to54.2811pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A\oplus
B$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\vbox{\hbox{\hskip
12.43317pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to41.36661pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp},\Delta$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
12.72656pt\hbox{\hskip 4.0pt\hbox{$\pi_{3}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to41.9534pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
B^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to97.77377pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 17.52547pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash A^{\perp}\with B^{\perp},\Delta$}\hskip 4.0pt}}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to148.98317pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 57.08884pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}&\text{
\ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\leavevmode\lower
49.31331pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 8.73593pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 12.43317pt\hbox{\hskip
4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to41.36661pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to89.79253pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 27.49352pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}\\\ \text{
\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\leavevmode\lower
73.18219pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 6.84726pt\vbox{\hbox{\hskip
8.73593pt\hbox{\hskip 4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to47.66667pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn\Gamma,\oc
A$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
10.54866pt\vbox{\hbox{\hskip 18.69878pt\hbox{\hskip
4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to53.89783pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp},\Delta,B$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to74.99515pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn
A^{\perp},\wn\Delta,\oc B$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to137.11559pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 34.34077pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\wn\Delta,\oc B$}\hskip 4.0pt}}}}}
\ignorespaces}&\text{ \ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces \ignorespaces\leavevmode\lower
72.25775pt\hbox{\vbox{\vbox{\hbox{\vbox{\hbox{\hskip 8.73593pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 18.69878pt\hbox{\hskip
4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to53.89783pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp},\Delta,B$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to102.32375pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 27.49352pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Delta,B$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 16.94485pt\lower-0.2pt\hbox{}\hbox
to68.43404pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 16.94485pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\wn\Delta,\oc B$}\hskip 4.0pt}}}}}
\ignorespaces}\\\ \text{ \ignorespaces \ignorespaces \ignorespaces
\ignorespaces \ignorespaces\ignorespaces\leavevmode\lower
71.28554pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 15.58319pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to47.66667pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn\Gamma,\oc
A$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
11.21808pt\vbox{\hbox{\hskip 4.36095pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to25.22218pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Delta$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to47.65833pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn
A^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to109.77876pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 34.34077pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}&\text{
\ignorespaces \ignorespaces \ignorespaces\leavevmode\lower
47.41666pt\hbox{\vbox{\hbox{\hskip 7.93752pt\vbox{\hbox{\hskip
4.36095pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to25.22218pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Delta$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to41.09721pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\Delta$}\hskip 4.0pt}}}} \ignorespaces}\\\ \text{
\ignorespaces \ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\leavevmode\lower
73.18219pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 15.58319pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to47.66667pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn\Gamma,\oc
A$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\vbox{\hbox{\hskip
27.35263pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to71.20555pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn A^{\perp},\wn
A^{\perp},\Delta$}\hskip 4.0pt}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to71.20555pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 11.7736pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn A^{\perp},\Delta$}\hskip 4.0pt}}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to121.55237pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 40.22758pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}&\text{
\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\ignorespaces \ignorespaces\leavevmode\lower
96.12663pt\hbox{\vbox{\vbox{\hbox{\vbox{\hbox{\hskip 15.58319pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to47.66667pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn\Gamma,\oc
A$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\vbox{\hbox{\hskip
15.58319pt\hbox{\hskip 4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to47.66667pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn\Gamma,\oc
A$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
27.35263pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to71.20555pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\wn A^{\perp},\wn
A^{\perp},\Delta$}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to133.32599pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 34.34077pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn A^{\perp},\wn\Gamma,\Delta$}\hskip 4.0pt}}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to161.10565pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 51.51117pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\wn\Gamma,\Delta$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 51.51117pt\lower-0.2pt\hbox{}\hbox
to58.08333pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 60.00423pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\wn\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}\\\ \text{
\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\leavevmode\lower
73.45996pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 10.92355pt\vbox{\hbox{\hskip
8.73593pt\hbox{\hskip 4.0pt\hbox{$\pi_{1}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to33.97215pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,A$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to55.81926pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash\Gamma,\forall
X.\,A$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\vbox{\hbox{\hskip
28.51125pt\hbox{\hskip 4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to73.52277pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp}[B/X],\Delta$}\hskip 4.0pt}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to73.52277pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 5.15453pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\exists X.\,A^{\perp},\Delta$}\hskip 4.0pt}}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to138.64127pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 51.9179pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}&\text{
\ignorespaces \ignorespaces \ignorespaces
\ignorespaces\ignorespaces\leavevmode\lower
49.5911pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 8.73593pt\hbox{\hskip
4.0pt\hbox{$\pi_{1}[B/X]$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to66.12831pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,A[B/X]$}\hskip 4.0pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 28.51125pt\hbox{\hskip
4.0pt\hbox{$\pi_{2}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox
to73.52277pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\vdash
A^{\perp}[B/X],\Delta$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to154.10484pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 59.64967pt\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash\Gamma,\Delta$}\hskip 4.0pt}}}}} \ignorespaces}\\\
\end{array}$ Figure 4: Key reductions of $\textsc{ell}_{2}$ cut-elimination.

###  D.1 Proof of extensional completeness

######  Proposition D.1.

Any regular language can be expressed as $\mathcal{L}(\pi)$ for some
$\textsc{ell}_{2}$ proof $\pi:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$.

######  Proof D.2 (Proof sketch).

To encode a deterministic finite automaton with set of states $Q$ and
transition function, simply instantiate the input string at the type
$1\oplus\ldots\oplus 1$ ($\mathrm{Card}(Q)$ times), and give it as arguments
the linear functions representing $\delta(0,-)$ and $\delta(1,-)$.

###  D.2 Proof of soundness by reduction to Lemma 5.3

In this section, we fix $\pi:\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$ in
$\textsc{ell}_{2}$, and prove the converse of the above. The first step is to
understand the shape of $\pi$.

######  Lemma D.3.

Up to commutations, $\pi$ is of the form

$\hat{\pi}$
$\vdash\mathtt{Str}[A_{1}]^{\bot},\dots,\mathtt{Str}[A_{n}]^{\bot},\oc\mathtt{Bool}$
$\vdash\mathtt{Str}^{\bot},\dots,\mathtt{Str}^{\bot},\oc\mathtt{Bool}$ $\oc$
$\vdash\wn\mathtt{Str}^{\bot},\dots,\wn\mathtt{Str}^{\bot},\oc\oc\mathtt{Bool}$
$\vdash\wn\mathtt{Str}^{\bot},\oc\oc\mathtt{Bool}$ $\parr$
$\vdash\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$

######  Proof D.4.

A proof of
$\vdash\wn\mathtt{Str}^{\bot},\dots,\wn\mathtt{Str}^{\bot},\oc\oc\mathtt{Bool}$
necessarily ends either with a structural rule or a promotion. From this and
the invertibility of $\parr$, one obtains that the proof, up to commutation,
ends with the following sequence of rules:

$\vdash\mathtt{Str}^{\bot},\dots,\mathtt{Str}^{\bot},\oc\mathtt{Bool}$ $\oc$
$\vdash\wn\mathtt{Str}^{\bot},\dots,\wn\mathtt{Str}^{\bot},\oc\oc\mathtt{Bool}$
$\vdash\wn\mathtt{Str}^{\bot},\oc\oc\mathtt{Bool}$ $\parr$
$\vdash\oc\mathtt{Str}\multimap\oc\oc\mathtt{Bool}$

Now, recall that $\mathtt{Str}^{\bot}=\exists X.\mathtt{Str}[X]^{\bot}$.
Moreover, notice the introduction rule for $\exists$ commutes with all other
rules except promotion and the introduction of $\forall$. We only need to show
that the introduction rule for all $\exists$ connectives of the occurrences of
$\mathtt{Str}^{\bot}$ are not followed by a promotion or a $\forall$
introduction. Ruling out promotion is easy, as all formulas in the conclusion
sequent of a promotion rule have exponential as principal connectives.
Moreover, it is possible to rule out $\forall$ introductions as folllws. If a
$\forall$ introduction rule appears in the proof, the $\forall$ connective it
introduces is part of an existential witness. But all variables existentially
quantified appear under the scope of an exponential connective, and therefore
can only precede a promotion rule.

Now, a crucial observation is that _the $A_{i}$ in the previous lemma can be
taken in $\textsc{mall}_{2}$ w.l.o.g._ This is where the _stratification_
property of $\textsc{ell}_{2}$ plays a key role.

######  Lemma D.5.

There is a proof $\pi^{\prime}$ whose witnesses $A_{1},\ldots,A_{n}$ are
closed $\textsc{mall}_{2}$ formulas, and which decides the same language as
$\pi$.

######  Proof D.6.

We define the _truncation at depth 2_ of a formula as follows: all subformulas
of the form $!A$ (resp. $?A$) at depth 2, i.e. in the scope of two other
nested $!/?$ modalities, are replaced by $1$ (resp. $\bot$). Note that the
truncation at depth 2 of $!\mathtt{Str}$ and $!!\mathtt{Bool}$ are themselves.

This operation extends to proofs: any functorial promotion of conclusion
$\vdash\wn B_{1},\ldots,\wn B_{m},\oc C$ is replaced by the only proof of
$\vdash\bot,\ldots,\bot,1$, while contractions and weakenings are replaced by
cuts with $1\vdash 1\otimes 1$ and $\vdash 1$. Note that this truncation is
the identity on cut-free proofs of $!!\mathtt{Bool}$ and $!\mathtt{Str}$.

One may then check that truncation at depth 2 is compatible with cut-
elimination, which means that one can replace $\pi$ by its truncation at depth
2 and still recognize the same language. Then the $A_{i}$ are replaced by
their “truncation at depth 0” which are $\textsc{mall}_{2}$ formulas.

######  Proposition D.7.

$\mathcal{L}(\pi)$ is regular.

######  Proof D.8.

By Lemma 5.3, the language

$\\{w\in\\{0,1\\}^{*}\mid\hat{\pi}(\overline{w}[A_{i}]\otimes\ldots\otimes\overline{w}[A_{n}])\longrightarrow^{*}\mathtt{true}\\}$

is regular. A examination of the cut-elimination process reveals that this
language is none other than $\mathcal{L}(\pi)$.