Call-by-Value Solvability and Multi Types

This paper provides a characterization of call-by-value solvability using call-by-value multi types. Our work is based on Accattoli and Paolini's characterization of  call-by-value solvable terms as those terminating with respect to the solving strategy of the value substitution calculus, a refinement of Plotkin's call-by-value $\l$-calculus. Here we show that the solving strategy terminates on a term $\tm$ if and only if $\tm$ is typable in a certain way in the multi type system induced by Ehrhard's call-by-value relational semantics. Moreover, we show how to extract from the type system exact bounds on the length of the solving evaluation and on the size of its normal form, adapting de Carvalho's technique for call-by-name.

§ INTRODUCTION

Plotkin's call-by-value $\l$-calculus <cit.> is at
the heart  of
programming languages such as OCaml and proof assistants such as Coq. In the study of programming
languages, call-by-value () evaluation is usually weak, that is, it does not reduce under
abstractions, and terms are assumed to be closed, , without free variables.
These constraints give rise to an elegant framework—we call it Closed ,  following

It often happens, however, that one needs to go beyond Closed by
considering Strong , which is the extended setting where reduction under abstractions is allowed
and terms may be open, or the intermediate framework of Open , where evaluation is weak
but terms are not necessarily closed.
The need arises, most notably, when describing the implementation model of Coq, as done by and Leroy
<cit.>, to realize the essential conversion test for dependent types. Other
motivations lie in the study of bisimulations by Lassen
<cit.>, partial evaluation <cit.>, or various topics
of a semantical or logical nature, recalled below.

Naïve Extension of  In call-by-name () turning to open terms  or strong
evaluation is harmless because does not impose any special form to the arguments of
On the contrary, turning to Open  or Strong is delicate. While some fundamental properties such
as confluence and standardization hold also in such cases, as showed by Plotkin's himself <cit.>,
others—typically of a semantical nature—break as soon as one considers open terms.

The problems of can be traced back to Plotkin's seminal paper,
where he points out the
incompleteness of with respect to CPS translations, an issue later solved with categorical
tools by Moggi <cit.>. This
led to a number of studies, among others
<cit.>, that
introduced many proposals of
improved calculi for .

The relationship with denotational semantics is also problematic, as  first shown by Paolini and Ronchi della Rocca
<cit.>. There are two subtle

* Solvability: the adaptation of the notion of solvability—roughly,
a form of
meaningfulness for terms—to ;

* Adequacy: denotational semantics that are
adequate for Closed <cit.> are no longer adequate for the extended settings. Roughly,
there are terms that are semantically divergent, that is, with
trivial semantics (or unsolvable),
while they are normal forms with respect to Plotkin's rules, and
so are expected to have non-trivial
semantics (and be solvable).

Both semantical issues of Open/Strong have been addressed in the literature, relying of linear logic tools. Adequacy is studied at length by Accattoli and Guerrieri in <cit.>, thus we here focus on solvability.

*Call-by-Value Solvability About solvability, Accattoli and Paolini <cit.>
characterize operationally solvable terms using a calculus isomorphic to the proof-net representation of $\l$-calculus, the value substitution calculus (shortened to ).
Namely, they introduce a solving evaluation strategy (called stratified-weak in <cit.>) in the that terminates if and only if the term is solvable—notably their strategy requires strong evaluation.
This is akin to what happens in , where solvable term are
those for which head evaluation terminates. A key point is that
such a characterization of solvability is impossible in Plotkin's original formulation of .

We would like to mention that the literature contains also a detailed study of solvability due to Garcia-Perez and Nogueira <cit.> based on a different approach, as they stick to Plotkin's call-by-value $\l$-calculus.

Here we continue Accattoli and Paolini's study of solvability, providing two contributions:

* Types and solvability: we characterize solvability using multi types, a variant of intersection types surveyed below. Namely, we prove that a term is solvable if and only if it is typable in a certain way;

* Bounds from types: we show how to extract, from a certain class of typing derivations, the number of steps taken by the solving strategy on a solvable term, together with the size of the solving normal form.

Before giving more details about our results, we recall multi types and their use for extracting operational bounds.

*Multi Types Intersection types are one of the standard tools to study $\l$-calculi, mainly used to characterize termination properties—classical references are Coppo and Dezani <cit.>, Pottinger <cit.>, and Krivine <cit.>.  In contrast to other type systems, they do not provide a logical interpretation, at least not as smoothly as for simple or polymorphic types—see Ronchi Della Rocca and Roversi's <cit.> or Bono, Venneri, and Bettini's <cit.> for details. They are better understood, in fact, as syntactic presentations of denotational semantics: they are invariant under evaluation and type all and only the terminating terms, thus naturally providing an adequate denotational model.

Intersection types are a flexible tool that can
be formulated in various ways. A flavour that emerged
in the last 10 years is that of non-idempotent intersection
types, where the
intersection $A \cap A$ is not equivalent to $A$. They were first considered by Gardner <cit.>, and then Kfoury <cit.>, Neergaard and Mairson <cit.>, and de Carvalho <cit.> provided a first wave of works abut them—a survey can be
found in Bucciarelli, Kesner, and Ventura's <cit.>. Non-idempotent intersections can be seen as multisets, which is why, to ease the
language, we prefer to call them multi types rather than
non-idempotent intersection types.

Multi types retain the denotational character of intersection types, and they actually refine it along two correlated lines. First, taking types with multiplicities gives rise to a quantitative approach, that reflects
resource consumption in the evaluation of terms. Second, such a quantitative feature turns out to coincide exactly with the one at work in linear logic.
Some care is needed here: multi types do not correspond to linear logic formulas, rather to the relational denotational semantics of linear logic (two seminal references for such a semantic are Girard's <cit.> and Bucciarelli and Ehrhard's <cit.>; see also <cit.>)—similarly to intersection types, they provide a denotational rather than a logical interpretation.

*De Carvalho's Bounds from Multi Types An insightful use of multi types is de Carvalho's connection between the size of types and the size of normal forms, and between the size of type derivations and evaluation lengths for the
$\l$-calculus <cit.>. He shows how from a certain class of typing derivations one can extract exact bounds about the length of evaluations and the size of the normal form of a term, according to various notions of evaluation. In particular, he shows how to do it for head reduction, which in is the strategy characterizing solvability, that is, for which terminating terms coincide with solvable terms.

*De Carvalho's Legacy De Carvalho developed his results in his PhD defended in 2007 <cit.>, known by the community thanks to a technical report that was eventually published much later <cit.>.

Soon after his PhD, he adapted his work to linear logic,
with Pagani and Tortora de Falco <cit.>.

A few years later, Bernadet and Graham-Lengrand adapted his work to measure the longest evaluation in the $\l$-calculus <cit.>.

At the time, it was not known whether it would make sense to count the number of $\beta$-steps (or linear logic cut-elimination steps) as a reasonable measure of complexity. After this was clarified (in the positive, for $\beta$ steps) by Accattoli and Dal Lago <cit.>, de Carvalho's work has been revisited by Accattoli, Graham-Lengrand, and Kesner in 2018 <cit.>. The revisitation started a new wave of works adapting de Carvalho's study to many evaluation strategies and extensions of the $\l$-calculus, including call-by-value <cit.>, call-by-need <cit.>, fully lazy call-by-need <cit.>, a linear logic presentation of call-by-push-value <cit.>, the $\lambda\mu$-calculus <cit.>, the $\l$-calculus with pattern matching <cit.>, the probabilistic $\l$-calculus <cit.>, and the abstract machine underlying the geometry of interaction <cit.>.

*and Multi Types Of all these studies, the relevant one for this paper is Accattoli and Guerrieri's study of <cit.>, which rests on Ehrhard's relational semantics <cit.> reformulated as multi types. They show that the evaluation of a term $\tm$ terminates in if and only if $\tm$ is typable with multi types, and that in that case $\tm$ is typable with the empty multi set, that they note $\zero$. Moreover, they show how to extract bounds to evaluation lengths and to the size of normal forms from type derivations, and characterize those type derivations that give exact bounds.

*Contribution 1: Qualitative Characterization of Solvability Here, we study the solving strategy which is an extension of evaluation in . Namely, it is a strong strategy that iterates under abstractions, but not all abstractions, only under head abstractions. We study it via Ehrhard's multi type system, as in  <cit.>. Since the strategy extends open evaluation, the terms that are terminating for the solving strategy—that is, the solvable terms—cannot be characterized simply as the typable ones.

The typical example is $\la\var\Omega$, which is normal for open evaluation but unsolvable (and thus diverging for the solving strategy). It is typable with $\zero$, and only with $\zero$. One is then tempted to characterize solvable terms as those ones typable with a type different from $\zero$. Unfortunately, things are slightly subtler, as $\la\vartwo\la\var\Omega$ is also normal for open evaluation but unsolvable, and it is typable with $\zero$ and, for instance, also with $\mset{\larrow\mtype\zero}$. We then define a notion of solvable multi type, which is a multi type that is not $\zero$ and that contains types that (recursively) do not have $\zero$ on the right of $\multimap$. Our result is that a term is solvable if and only if it is typable with a solvable multi type.

Our notion of solvable type is not new, as in fact the idea appears in the literature in other papers using intersection types to study solvability <cit.>. Those type systems, however, are defective, and the characterizations that they claim are not in fact proved because their systems do not verify subject reduction  (for <cit.> subject expansion also fails), as we detail in Appendix <ref>. Therefore, a first contribution of this work is to recast their idea in a setting where it fully works.

*Contribution 2: Quantitative Characterization of Solvability The second contribution of this work is that we exploit the quantitative character of multi types and extract bounds from type derivations, building over de Carvalho's technique. First, we show that every solvable derivations provides bounds to the length of the solving evaluation and to the size of the solving normal form. Second, we characterize the solvable derivations that provide exact bounds. This last part requires to introduce two refinements of solvable types, as solvable type derivations are in general too permissive with respect to quantitative bounds.

On the one hand, we need to ensure that sub-terms evaluated by the solving strategy are typed exactly once (with multi types a sub-term can naturally be typed many times). Such a constraint gives rise to unitary solvable types. On the other hand, we need to ensure that sub-terms not touched by the solving strategy are not typed. This is obtained by constraining types appearing in the typing context and on the left of $\multimap$, and gives rise to the notion of inertly solvable types. We then prove that when a solvable type derivation is both unitary and inert—which we shall refer to as being precisely solvable—then it captures exactly the evaluation length and the size of the normal form for the solving strategy.

Such a quantitative study of solvability is the first one in the literature, and the described refinements of solvable types are also new.

*Reasonable Cost Models In <cit.>, Accattoli et al. prove that the number of $\beta$ steps of a strategy of the VSC, namely the external one, is a reasonable time cost model for (where reasonable means polynomially related to the time cost model of Turing machines). The solving strategy studied here is a sub-strategy of the external one, and so the result transfers. Thus, we obtain that multi types provide quantitative bounds that are meaningful from a computational complexity point of view.

*Syntactic Variants We study via the VSC, to stress the linear logic background and foundation of our study. Everything could equivalently be  easily  reformulated inside (the intuitionistic and fragment of) Curien and Herbelin's
$\lambdamucalc$-calculus, following the isomorphism with the VSC developed in <cit.>
and preserving the number of steps/cost model. The solving strategy can also be reformulated using the shuffling calculus $\shufcalc$ by Guerrieri and Carraro
<cit.>, a calculus with commuting conversions used recently also by Manzonetto et al.
<cit.>.  Commuting conversion steps, however, cannot be counted via multi
types (but they should), and the cost model of $\shufcalc$ is unclear (see
<cit.>). Therefore, $\shufcalc$ can be used for a qualitative study of solvability, but not for a
quantitative one as we do here. Calculi with $\letexp$-commutation rules such as the one by Herbelin and Zimmerman <cit.> simply
can be seen as subcalculi of the VSC (up to structural equivalence, see <cit.>). Similar remarks apply to many other calculi
<cit.>. The key point of the VSC (valid also
in $\lambdamucalc$) is that it does not need any commuting rule.

*Proofs Proofs are in the Appendix.

*Historical Note This paper has been uploaded to Arxiv in February 2022 but the results were developed by the authors in 2020. They were part of a larger and rejected submission to LICS 2021 that included also the results of <cit.>.

§ VALUE SUBSTITUTION CALCULUS

Here we present the value substitution calculus (for short) introduced by Accattoli and Paolini <cit.>, and we recall some properties.
The is a $\lambda$-calculus with let-expressions whose reduction rules mimic cut-elimination on proof-nets, via Girard's translation $(A \Rightarrow B)^v = \oc (A^v \multimap B^v)$ of intuitionistic logic into linear logic, as explained in <cit.>.

In , $\beta$-redexes are decomposed via let-expressions, and the
by-value restriction on evaluation is on the let-substitution rule, not on $\beta$-redexes, because only values
can be substituted.
A let-expression is formulated as an explicit substitution or sharing (for short) $\tm\esub{\var}{\tmtwo}$ which binds $\var$ in $\tm$.
All along the
paper we use (many notions of) contexts, terms with a hole, noted $\ctxhole$. For now, we need substitution contexts $\sctx$, which are simply lists of . The grammars are:

\textsc{Values } & \val & \grameq \var \mid  \la\var\tm
\\
\textsc{Terms } & \tm,\tmtwo, \tmthree & \grameq \val \mid \tm\tmtwo
\mid \tm \esub\var\tmtwo
\\
\textsc{Substitution Ctxs } &\subctx & \grameq \ctxhole \mid \subctx \esub\var\tm
%\textsc{Contexts} & \ctx & \grameq \ctxhole \mid \ctx \tm \mid \tm \ctx \mid \la{\var}{\ctx} \mid %
%\ctx \esub\var\tm \mid \tm \esub \var \ctx
\end{array}$

The set of free variables of term $\tm$ is denoted by $\fv{\tm}$.
Plugging a term $\tm$ in a context $\ctx$ is noted $\ctxp{\tm}$, possibly capturing variables.
An answer is a term of the shape $\sctxp\val$, where $\val$ is a value (an abstraction) and $\sctx$ is a substitution context.
We use $\tm \isub{\var}{\tmtwo}$ for the capture-avoiding substitution of
$\tm$ for each free occurrence of $\var$ in $\tm$.
There are two kinds of rewrite rules, both work at a distance, that is, up to a substitution context.

$\begin{array}{rr@{\ }l@{\ }l}
\textsc{Multiplicative rule} & \subctxp{\la\var\tm}\tmtwo &  \rtom  & \subctxp{\tm\esub{\var}{\tmtwo}} \\
\textsc{Exponential rule}  & \tm\esub\var{\subctxp{\val}} &  \rtoe  & \subctxp{\tm\isub{\var}{\val}}
%    \textsc{Expon. Variables}  & \tm\esub\var{\subctxp{\vartwo}} &  \rtoevar  & \subctxp{\tm\isub{\var}{\vartwo}}
\end{array}$

We shall consider three fragments of the  .
They all contain the terms of , they differ only in the choice of evaluation contexts for the rewrite rules.

*The Open VSC We first focus on the open fragment of the , where rewriting is forbidden under abstraction and terms are possibly open (but not necessarily). This fragment has a nice inductive description of its normal forms, called fireballs, that is the starting point for many other definitions in the paper. Open contexts and rules are defined as follows.

\textsc{Open ctxs} && \weakctx & \grameq \ctxhole \mid \weakctx \tm \mid \tm \weakctx \mid \weakctx \esub\var\tm \mid
\tm\esub\var \weakctx
\end{aligned}$

Open rewrite rules:

a '
1 a '

($a \in \set{\msym,\esym}$)

\textsc{Open reduction}:& \tovsubo  \, \defeq \, \tomo \cup \toeo
\end{array}$

*  $\tovsubo$ is diamond; $\tomo$ and $\toeo$ strongly commute.

*  A term is $\osym$-normal if and only if it is a fireball, where fireballs (and proper inert terms) are defined by:

Proper inert terms       ||

Fireballs       ||

Diamond of $\tovsubo$ and strong commutation of $\tomo$ and $\toeo$ are technical facts (see  <Ref> for definitions) with relevant consequences:
$\tovsubo$ is confluent and its non-determinism is only apparent, because if an $\osym$-evaluation from $\tm$ reaches
a $\osym$-normal form $\tmtwo$, then every $\osym$-evaluation from $\tm$ eventually ends in $\tmtwo$;
and all these $\osym$-evaluations have same length and same number of $\msym$-steps and $\esym$-steps.
Same properties hold for other strategies we shall consider.

The Closed  is the restriction of the Open to closed terms. Its normal forms are the closed values, that is, closed abstractions (the only fireballs that are closed).

Proper inert terms have the form of applications iterated $n > 0$ times, possibly interleaved with ES, starting with a head free variable.
It is natural to see a variable as a “degenerate” case, and to define inert terms as variables or proper inert terms.

\begin{equation*}
\textsc{Inert terms } \ \itm \grameq \var \mid \pitm
\end{equation*}

In our study, inert terms (including variables) play a crucial role.
For instance, for inert terms  we shall prove stronger claims about typability to have the right inductive hypothesis.
In , variables have somehow a double nature as both inert terms (the stronger statements for inert terms also hold for variables) and values (the exponential step can fire $\tm\esub{\var}{\vartwo}$).

*The Strong/Full VSC To avoid notation clashes between the Solvable and the Strong (both would start with 's'), we refer to the Strong as the . The is obtained by allowing rewriting rules  to be applied everywhere in a term.

$\begin{array}{l r rclccc}
\textsc{Full ctxs} & \fctx  \grameq \ctxhole \mid \fctx \tm \mid \tm \fctx \mid \la{\var}{\fctx} \mid
\fctx \esub\var\tm \mid \tm \esub \var \fctx
\end{array}$

Full rewrite rules:

a '
1a '

($a \in \set{\msym,\esym}$)

$\begin{array}{r l@{\ } l@{\ } lllllll}
\textsc{\Full reduction:} & \tovsub  & \defeq  &\tom \cup \toe
\end{array}$

Reduction $\tovsub$ is not diamond:
see all the $\vsub$-evaluations of $(\var\var) \esub{\var}{\la{\vartwo} \Id \Id}$ with $\Id \defeq \la{\varthree}\varthree$.

The reduction $\tovsub$ is confluent.

*Plotkin vs VSC

Plotkin's original $\lambda$-calculus $\plotcalc$ <cit.> can be easily simulated in the .
The syntax of $\plotcalc$ is simply the same as in the but without .
The reduction $\tobvplot$ in $\plotcalc$ is the closure under contexts (without ) of the rule

\[(\la{\var}\tm)\val \rtobvplot \tm\isub{\var}{\val}\]

Let $\tm$ be a term without .
If $\tm \tobvplot \tm'$ then $\tm \tom \!\cdot \toe  \tm'$.

There is no sensible way to simulate into $\plotcalc$.
Indeed is a proper extension of $\plotcalc$: makes divergent terms such as $(\la{\var}\delta)(\vartwo\vartwo)\delta$ and $\delta ((\la{\var}\delta) (\vartwo\vartwo))$ that are $\betaplot$-normal. Despite being an extension of $\plotcalc$, VSC does not loose the essence, as $(\la\var\vartwo) \Omega$ is strongly divergent in both $\plotcalc$ and VSC, while in it normalizes in one step, erasing $\Omega$.

§ CALL-BY-VALUE SOLVABILITY AND THE SOLVING STRATEGY

In the $\lambda$-calculus, the notion of solvability identifies somehow “meaningful” terms.
This notion is well studied in the $\lambda$-calculus, with an elegant theory, see Barendregt <cit.>.
In , an elegant theory of solvability is still missing because of issues first observed by Ronchi Della Rocca and Paolini <cit.> (a survey is in <cit.>), amounting to intrinsic limitations of  Plotkin's original $\lambda$-calculus <cit.>. Accattoli and Paolini showed that instead the is a good framework for solvability <cit.>.

Since the definition of solvability depends on the calculus and its evaluation, we give a parametric definition.

Let $X$ be a calculus.
A term $\tm$ in $X$ is $X$-solvable if there are terms $\tmtwo_1, \dots , \tmtwo_k$ and variables $\var_1, \dots , \var_h$, with $h, k \geq 0$, such that
$(\lambda \var_1 \dots \la{\var_h}\tm) \tmtwo_1 \dots \tmtwo_k$ $X$-evaluates to $\Id \defeq \la{\var}\var$.

*The Solving VSC
Accattoli and Paolini <cit.>  characterize operationally -solvability: a term $\tm$ is -solvable if and only if $\tm$ $\solvredsym$-normalizes, for a suitable definition of solving reduction $\tosolv$ in between the full one $\tovsub$ and the open one $\tovsubo$, that is, restricting $\tovsub$ but extending $\tovsubo$, given below.
The Solving  is the endowed with the solving reduction $\tosolv$ that we now define.
It is obtained by extending the open rewriting rules under head
abstractions only, via the notion of solving context.

\textsc{Solving ctxs} && \solvctx &\grameq \openctx \mid \la{\var}\solvctx \mid \solvctx \tm \mid \solvctx\esub{\var}{\tm}
\end{aligned}$

Solving rewrite rules:

a '
1a '

($a \in \set{\msym,\esym}$)
\textsc{Solving reduction}:& \tovsubsolv  \, \defeq \, \tomsolv \cup \toesolv
\end{array}$

For instance, because of the extension under head abstractions,
$\la\var (\Id \Id) \tomsolv \la\var(\varthree\esub\varthree\Id) \toesolv \la\var\Id$.
But reduction under non-head abstractions is forbidden:
$\vartwo (\la\var(\Id \Id)) \not\tomsolv  \vartwo (\la\var(\varthree\esub\varthree\Id))$.

The solving strategy captures the fact that $\tm \defeq \la\var\Omega$ is unsolvable, as $\tovsubsolv$ diverges on $\tm$, while $\tmtwo \defeq \var (\la\var\Omega)$ is solvable, and indeed $\tovsubsolv$ terminates on $\tmtwo$. Note also the difference between and solvability: a term such as  $\tmthree \defeq \var\Omega$ is unsolvable (and $\tovsubsolv$ indeed diverges) while it is solvable (it is head normal). Every solvable term is also solvable, as the solving strategy is an extension of the head strategy, because it reduces arguments  both out of abstractions and under head abstractions.

*  $\tosolv$ is diamond; $\tosolvm$ and $\tosolve$ strongly commute.

*  A term is $\solvredsym$-normal if and only if it is a solvable fireball, where solvable fireballs are defined by:

$\textsc{Solvable fireballs} \qquad \solvnf \grameq  \itm \mid \la{\var}\solvnf \mid \solvnf \esub{\var}{\pitm}$

§ MULTI TYPES BY VALUE

We present a  multi type system for .
For Plotkin's $\l$-calculus, it has been introduced by Ehrhard <cit.>, as the version of de Carvalho's System $\mathsf{R}$ for <cit.>. Both systems can be seen as the restrictions to the /translations of the $\l$-calculus of the relational semantics of linear logic. The system in particular is studied with respect to by Accattoli and Guerrieri in <cit.>.

*Multi Types There are two layers of types, linear and multi types, mutually defined by:

\begin{align*}
\textsc{Linear types \ } \ltype, \ltypetwo &\grameq \ground \mid \larrow{\mtype}{\mtypetwo} \quad
\textsc{Multi types \ } \mtype, \mtypetwo &\grameq \mset{\ltype_1, \dots, \ltype_n} \quad n \geq 0
\end{align*}

where $\ground$ is an unspecified ground type and $\mset{\ltype_1, \dots, \ltype_n}$ is our notation for finite
The empty multi type $\mset{\,}$ (obtained taking $n = 0$) is also denoted by $\emptymset$.

A generic (multi or linear) type is denoted by $\type$.

A multi type $\mset{\ltype_1, \dots, \ltype_n}$ has to be intended as a conjunction $\ltype_1 \land \dots \land
\ltype_n$ of linear types $\ltype_1, \dots, \ltype_n$, for a commutative, associative, non-idempotent conjunction
$\land$ (morally a tensor $\otimes$), whose neutral element is $\emptymset$.

The intuition is that a linear type corresponds to a single use of a term $\tm$, and that $\tm$ is typed with a
$\mtype$ of $n$ linear types if it is going to be used (at most) $n$ times. The  meaning of using a term is not
easy to define precisely. Roughly, it means that if $\tm$ is part of a larger term $\tmtwo$, then (at most) $n$ copies
of $\tm$ shall end up in evaluation position during the evaluation of $\tmtwo$. More precisely, the $n$ copies shall
up in evaluation positions where

The derivation rules for the multi types system are in <Ref> (explanation follows).  The rules are the same as in Ehrhard <cit.>, up to the fact that they are extended to .

A multi (linear) judgment has the shape $\typctx \vdash \tm \hastype \type$ where $\tm$ is a term, $\type$ is a
multi (linear) type and $\typctx$ is a type context, that is, a total function from variables to multi types
such that  the set $\domain{\typctx} \defeq \{\var \mid \typctx(\var) \neq \emptymset\}$ is finite.

{\begin{prooftree}[label separation = .1em]
\infer0
{\var \hastype [\ltype] \vdash \var \hastype \ltype}
\end{prooftree}}
\quad
{\begin{prooftree}[separation=1em, label separation = .1em]
\hypo{\typctx \vdash \tm \hastype \mset{ \larrow{\mtype\!}{\!\mtypetwo} }}
\hypo{\typctxtwo \vdash \tmtwo \hastype \mtype}
\infer2[\scriptsize$\ruleAp$]
{\typctx \uplus \typctxtwo \vdash \tm\tmtwo \hastype \mtypetwo}
\end{prooftree}}
\quad
{\begin{prooftree}[label separation = .1em]
\hypo{\tyjp{}{\tm}{\typctx, \var \hastype \mtype}{\mtypetwo}}
\infer1[\scriptsize$\ruleFun$]
\end{prooftree}}
\quad
{\begin{prooftree}[separation=1em, label separation = .1em]
\hypo{\typctx, \var \hastype \mtype \vdash \tm \hastype \mtypetwo}
\hypo{\typctxtwo \vdash \tmtwo \hastype \mtype}
\infer2
{\typctx \uplus \typctxtwo \vdash \tm \esub\var\tmtwo \hastype \mtypetwo}
\end{prooftree}}
\quad
{\begin{prooftree}[separation=1em, label separation = .1em]
\hypo{\left[\tyjp{}{\val}{\typctx_{i}}{\ltype_{i}}\right]_{\iI}}
\infer1
{\tyjp{}{\val}{\biguplus_{\iI}\typctx_{i} }{\mult{\ltype_{i}}_{\iI}}}
\end{prooftree}}

Call-by-Value Multi Type System.

*Technicalities about Types The type context $\typctx$ is empty if $\dom{\typctx} = \emptyset$.
Multi-set sum $\mplus$ is extended to type contexts point-wise,
$(\typctx \mplus \typctxtwo)(\var) \defeq \typctx(\var) \mplus \typctxtwo(\var)$ for each variable $\var$.
This notion is extended to a finite family of type contexts as expected,
in particular $\bigmplus_{i \in J\!} \typctx_i$ is the empty context  when $J = \emptyset$.
A type context $\typctx$ is denoted by $\var_1 \hastype \mtype_1, \dots, \var_n \hastype \mtype_n$ (for some $n \in
\nat$) if $\dom{\typctx} \subseteq \{\var_1, \dots, \var_n\}$ and $\typctx(\var_i) = \mtype_{i}$ for all $1 \leq i \leq
Given two type contexts $\typctx$ and $\typctxtwo$ such that $\dom{\typctx} \cap \dom{\typctxtwo} = \emptyset$, the
context $\typctx, \typctxtwo$ is defined by $(\typctx, \typctxtwo)(\var) \defeq \typctx(\var)$ if $\var \in
\dom{\typctx}$, $(\typctx, \typctxtwo)(\var) \defeq \typctxtwo(\var)$ if $\var \in \dom{\typctxtwo}$, and $(\typctx,
\typctxtwo)(\var) \defeq \emptymset$ otherwise.
Note that $\typctx, \var \hastype \emptymset = \typctx$, where we implicitly assume $\var \notin \dom{\typctx}$.

We write $\concl{\tderiv}{\typctx}{\tm}{\mtype}$ if $\tderiv$ is a (type) derivation (a tree built up from the rules in <Ref>) with conclusion the multi judgment $\typctx \vdash \tm \hastype \mtype$.
In particular,  we write $\concl{\tderiv}{\,}{\tm}{\mtype}$ when $\typctx$ is empty.
We write $\derive{\tderiv}{\tm}$ if $\concl{\tderiv}{\typctx}{\tm}{\mtype}$ for some type context $\typctx$ and multi type $\mtype$.

*Explanations About the Rules of the Type System
All rules but $\ruleAx$ and $\ruleFun$ assign a multi type to the term on the
right-hand side of a judgment.
Variables and abstractions are the only terms that can be typed by a linear type, via $\ruleAx$ and $\ruleFun$.
Rule $\ruleMany$ can be applied to variables and abstractions only, turning linear types into multi types: they have as many premises as the elements in the (possibly
empty) set of indices $I$ (when $I = \emptyset$, the rule has no premises, and it gives an empty multi type $\emptymset$).
The $\ruleMany$ rules say how many “copies” of one occurrence of abstraction or variable in a term $\tm$ are needed to evaluate $\tm$.
Essentially, they correspond to the promotion rule of linear logic,
which, in the representation of the $\lambda$-calculus, is indeed used for typing
abstractions and variables.

*The Sizes of Type Derivations Our study being quantitative, we need a notion of size of type derivations. In fact, we shall use two notions of size.

Let $\tderiv$ be a derivation.
The (general) size $\size{\tderiv}$ of $\tderiv$ is the number of

rule occurrences in $\tderiv$ except for the rule $\ruleMany$.

The multiplicative size $\sizem{\tderiv}$ of $\tderiv$ is the number of occurrences of the rules $\lambda$ and
$\ruleAp$ in $\tderiv$.

The two sizes for a derivation play different qualitative and quantitative roles. Qualitative: to have a
combinatorial proof of the characterization of solvable terms, we need a measure that
decreases for some kinds of $\tovsub$ steps;
this role is played by the general size $\size{\!\cdot\!}$.
Quantitative: to count the number of $\tom$ steps in
solving evaluations, the cost model;
his role is played by the multiplicative size $\sizem{\!\cdot\!}$.

*Substitution and Removal Lemmas
The two next lemmas establish a key feature of this type system: in a typed term $\tm$,
substituting a value for
a variable as in the exponential step, or dually removing a value, preserves the type of $\tm$ and consumes (dually, adds) the multi type of the variable.
Besides, it also provides  quantitative information about the type derivation for $\tm$ before and after the substitution/removal.

Let $\tm$ be a term, $\val$ be a value and $\namedtyjp{\tderiv}{}{\tm}{\typctx, \var \hastype
\mtypetwo}{\mtype}$ and $\namedtyjp{\tderivtwo}{}{\val}{\typctxtwo}{\mtypetwo}$ be derivations.
Then there is a derivation $\namedtyjp{\tderivthree}{}{\tm \isub{\var}{\val}}{\typctx \mplus \typctxtwo}{\mtype}$
with $\sizem{\tderivthree} = \sizem{\tderiv} + \sizem{\tderivtwo}$ and $\size{\tderivthree} \leq \size{\tderiv} +
\size{\tderivtwo}$.

Let $\tm$ be a term, $\val$ be a value, and
be a derivation.
Then there are two  derivations $\namedtyjp{\tderivtwo}{}{\tm}{\typctxtwo, \var \hastype
\mtypetwo}{\mtype}$
and $\namedtyjp{\tderivthree}{}{\val}{\typctxthree}{\mtypetwo}$ such that $\typctx = \typctxtwo \mplus \typctxthree$
with $\sizem{\tderiv} = \sizem{\tderivtwo} + \sizem{\tderivthree}$ and $\size{\tderiv} \leq \size{\tderivtwo} +
\size{\tderivthree}$.

*The Special Role of Inert Terms In the characterizations via multi types of the following two sections, inert terms play a crucial role. In statements about solvable normal forms, they usually satisfy stronger properties, essential for the induction to go through. Predicates shall also spread on inert terms: if assumed on the type context, they transfer to the right-hand type, which is in turn the key step to propagate the predicate on sub-derivations.

§ MULTI TYPES FOR OPEN

Here we recall the relationship between multi types and developed by Accattoli and Guerrieri in
<cit.>. The reason is threefold:

* Building block: the solvable case relies on the open one, because the solving strategy is an iteration of open evaluation under head abstractions.

* Blueprint: the open case provides the blueprint for the solvable case.

* Adapting a few details: the development in <cit.> needs to be slightly adapted to our present framework.
Namely, here we use the Open VSC
instead of the split fireball calculus used in <cit.> (another formalism for ),
and we include a ground type $\ground$, necessary to later deal with the solving strategy.

*The Open Size of Terms For our quantitative study, we need a notion of term size, introduced here. Now, we actually need a notion of size for each evaluation strategy that we aim at measuring via multi types. Essentially, the size counts the constructors of a term that can be traversed by the strategy. The open size $\sizeo{\tm}$ of a term $\tm$, then, is its number of applications out of abstractions,
\begin{align*}
\sizeo{\var} &\defeq 0
\sizeo{\la{\var}{\tm}} & \defeq  0
\sizeo{\tm\tmtwo} & \defeq  \sizeo{\tm} + \sizeo{\tmtwo} + 1
\sizeo{\tm \esub{\var}{\tmtwo}} & \defeq  \sizeo{\tm} + \sizeo{\tmtwo}.
\end{align*}

*Overview of the Characterization
Qualitatively, the open evaluation of $\tm$ terminates if and only if $\tm$ is typable.
Since $\tovsubo$ does not reduce under abstractions, every abstraction is $\osym$-normal and hence must be typable: for this reason, $\la{\var}\delta\delta$ is typable with $\emptytype$ (take the derivation only made of one rule $\ruleManyVal$ with $0$ premises), though $\delta\delta$ is not.

Quantitatively, the multiplicative size
$\sizem{\tderiv}$ of every type derivation $\tderiv$ for $\tm$ provides bounds the sum of the length of the open evaluation of $\tm$ plus
the open size of its open normal form. To obtain exact bounds, then, one has to consider only type derivations satisfying a further tight predicate, defined below over the auxiliary inert predicate for type derivations.

*Inert and Tight Derivations
A multi type is ground if it is of the form $n\mset{\ground} \defeq \mset{ \ground, \dots, \ground}$  ($n$  times $\ground$) for any $n \geq 0$ (so, $0\mset{\ground} = \emptytype$).
Inert types are defined below, with $n \geq 0$.

\begin{align*}
\textsc{Inert multi type }& \imtype \grameq 	\mset{ \inltype_1, \dots, \inltype_n}
\textsc{Inert linear type }& \inltype \grameq \ground \mid \larrow{n\mset{\ground}}{\imtype}
\end{align*}

A type context $\var_1 \hastype \mtype_1, \dots, \var_n \hastype \mtype_n$ is inert if $\mtype_1, \dots,
\mtype_n$ are inert multi types.

Note that
every ground multi type is inert.

A derivation $\namedtyjp{\tderiv}{}{\tm}{\typctx}{\mtype}$ is inert if $\typctx$ is an inert type context and $\mtype$ is an inert multi type. If, moreover, $\mtype$ is a ground multi type, then $\tderiv$ is tight.

Note that the definitions of inert and tight derivation depend only on its final judgment.

derivations are those we are actually interested in, but often, for the induction to go through, we have to consider the wider class of inert derivations.
For instance, tight derivations may have a complex
structure, having sub-derivations for inert terms that might
not be tight, but only inert.
Additionally, inert types spread on inert terms—the first key property of inert terms.

Let $\concl{\tderiv}{\typctx}{\itm}{\mtype}$ be a derivation and $\itm$ be an inert term.
If $\typctx$ is a inert type context, then $\mtype$ is a inert multi type (and so $\tderiv$ is inert).

Open correctness establishes that all typable terms $\osym$-normalize and the multiplicative size of the derivation bounds the number of $\tomo$ steps plus the open size of the $\osym$-normal form; this bound is exact if the derivation is tight.
Open correctness is proved following a standard scheme in two stages: $(a)$ quantitative subject reduction states that every $\tovsubo$ step preserves types and decreases the general size of a derivation, and that any $\tomo$ step decreases by an exact quantity the multiplicative size of a derivation;
$(b)$ a lemma states that the multiplicative size of any derivation typing a $\osym$-normal form $\tm$ provides an upper bound to the open size of $\tm$, and if moreover the derivation is tight then the bound is exact. The lemma follows—its unusual statement puts forward the special role of inert terms.

Let $\fire$ be a fireball.
If $\namedtyjp{\tderiv}{}{\fire}{\typctx}{\mtype}$
then $\sizem{\tderiv} \geq \sizeo{\fire}$.
If, moreover, $\typctx$ is inert and ($\mtype$ is ground inert or $\fire$ is inert), then
$\sizem{\tderiv} = \sizeo{\fire}$.

Example. The non-inert fireball $\delta \defeq \la{\var}{\var\var}$ is typable and the last rule of any derivation $\concl{\tderiv}{\typctx}{\delta}{\mtype}$ is
If $\mtype$ is not ground then $\ruleManyVal$ has at least one premise that types the subterm $\var\var$, so $\sizem{\tderiv} > \sizeo{\delta}$.
If $\mtype$ is ground, then $\mtype = \emptytype$ and $\ruleManyVal$ has no premises, with $\sizem{\tderiv} = 0 = \sizeo{\delta}$.

For inert terms, <Ref> says that their open size is the multiplicative size of their inert derivations;
by spreading of inertness (<Ref>), it amounts to say that the type context is inert.

Let $\namedtyjp{\tderiv}{}{\tm}{\typctx}{\mtype}$ be a derivation.

* Multiplicative step: if $\tm \towm \tm'$ then there is a derivation
$\namedtyjp{\tderiv'}{}{\tm'}{\typctx}{\mtype}$ with
$\sizem{\tderiv'} = \sizem{\tderiv} - 2$ and $\size{\tderiv'} = \size{\tderiv} - 1$;

* Exponential step: if $\tm \towe \tm'$ then there is a derivation
$\namedtyjp{\tderiv'}{}{\tm'}{\typctx}{\mtype}$ such that
$\sizem{\tderiv'} = \sizem{\tderiv}$ and $\size{\tderiv'} < \size{\tderiv}$.

As the general size of derivations decreases after any $\tovsubo$ step,
we have a combinatorial proof of open correctness.

$\derive{\tderiv}{\tm}$ be a derivation.
Then there is a $\osym$-normalizing evaluation $\deriv \colon \tm \tovsubo^* \tmtwo$ with $2\sizem{\deriv} +
\sizeo{\tmtwo} \leq \sizem{\tderiv}$.

And if $\tderiv$ is tight, then $2\sizem{\deriv} + \sizeo{\tmtwo} = \sizem{\tderiv}$.

Open completeness establishes that every $\osym$-normalizing term is typable, and with a tight derivation $\tderiv$ such that $\sizem\tderiv$ is exactly the number of $\tomo$ steps plus the open size of the $\osym$-normal form.
The proof technique is standard: $(a)$ quantitative subject expansion states that typability can be pulled back along $\tovsubo$ steps, increasing $\size\tderiv$;
$(b)$ a lemma states that every $\osym$-normal form is typable with a tight derivation—inert terms verify a stronger statement.

* Inert: if $\tm$ is an inert term then, for any inert multi
type $\mtype$, there is an inert derivation $\concl{\tderiv}{\typctx}{\tm}{\mtype}$.

* Fireball: if $\tm$ is a fireball then there is a tight derivation $\concl{\tderiv}{\typctx}{\tm}{\emptytype}$.

Let $\namedtyjp{\tderiv'}{}{\tm'}{\typctx}{\mtype}$ be a derivation.

* Multiplicative step: if $\tm \towm \tm'$ then there is a derivation
$\namedtyjp{\tderiv}{}{\tm}{\typctx}{\mtype}$ with
$\sizem{\tderiv'} = \sizem{\tderiv} - 2$ and $\size{\tderiv'} = \size{\tderiv} - 1$;

* Exponential step: if $\tm \towe \tm'$ then there is a derivation
$\namedtyjp{\tderiv}{}{\tm}{\typctx}{\mtype}$ such that
$\sizem{\tderiv'} = \sizem{\tderiv}$ and $\size{\tderiv'} < \size{\tderiv}$.

As the general size of derivations increases
after a backward $\osym$-step,
a combinatorial proof of open completeness follows.

Let $\deriv \colon \tm \tovsubo^* \tmtwo$ be an $\osym$-normalizing evaluation.
Then there is a tight derivation $\concl{\tderiv}{\typctx}{\tm}{\emptytype}$ such that $2\sizem{\deriv} + \sizes{\fire} = \sizem{\tderiv}$.

§ MULTI TYPES FOR SOLVABILITY

Here we provide the main results of the paper.

*Solvable size First of all, we need a notion of size for normal forms of the solving strategy. The solvable size $\sizes{\tm}$ of a term $\tm$ is its number of applications plus its number of abstractions
not in argument position:

\begin{align*}
\sizes{\var} &\defeq 0
\sizes{\la{\var}{\tm}} & \defeq  \sizes{\tm} + 1
\sizes{\tm\tmtwo} & \defeq  \sizes{\tm} + \sizeo{\tmtwo} + 1
\sizes{\tm \esub{\var}{\tmtwo}} & \defeq  \sizes{\tm} + \sizeo{\tmtwo}.
\end{align*}

$\begin{array}{rr@{\ }c@{\ }l@{\qquad} rr@{\ }c@{\ }l}
\text{Solvable multi type } & \smtype &\grameq &	\mset{\sltype_1, \dots, \sltype_n} \ \ n > 0
\text{Solvable linear type} & \sltype &\grameq & \ground \mid  \larrow{\mtype}{\smtype}
\\
\text{Unitary s. multi type} & \usmtype &\grameq &	\mset{ \usltype}
\text{Unitary s. linear type} &\usltype &\grameq & \ground \mid \larrow{\mtype}{\usmtype}
\\
\text{Inertly s. multi type} & \ismtype &\grameq & \mset{\isltype_1, \dots, \isltype_n} \ \ n > 0
\text{Inertly s. linear type} & \isltype &\grameq & \ground \mid \larrow{\imtype}{\ismtype}
\end{array}$

Kinds of solvable types. A
type is precisely solvable if it is unitary and inertly solvable.

*Solvable Multi Types
The qualitative characterization of solvable terms with multi types is fairly simple: they are those terms typable with a solvable multi type, defined in <Ref>.
There are two ingredients: descending under abstraction, and selecting only head abstractions. They corresponds on types to, respectively, being typable with something that is not $\emptytype$, and having non-$\emptytype$ type on the right of the linear arrow—recursively.

Being typable with something that is not $\emptytype$, ultimately requires
a ground multi type $n\mset{\ground}$ different from $\emptytype$ in the type system (in contrast to the open case, where there is no need for $\ground$).

The point is exemplified by the term $\la{\vartwo}{\delta\delta}$ (with $\delta = \la{\var}{\var\var}$): it is $\osym$-normal and it can only be typed by $\emptytype$, but it is not $\solvredsym$-normalizing and it cannot be typed by solvable types.

*Precisely Solvable Multi Types The quantitative properties of solvable terms rest on two orthogonal predicates (see <Ref>).

The unitary one ensures that each solving multiplicative step is counted exactly once. Solvable types guarantee that each such step is counted, but it might be counted more than once. The constraint amounts to
asking that the topmost and right-hand multisets are singletons. This is the key requirement for obtaining that in the statement of subject reduction the general size of the derivation decreases by exactly one at each multiplicative step.

The inert predicate instead ensures that the type derivation does not type sub-terms that are not accessible to the solving strategy. Typing such sub-terms is harmless for a qualitative study, but it is problematic for a quantitative one, as it does introduces a mismatch between the size of solving normal forms and the size of their type derivations. The constraint amounts to asking that the left-hand multisets are inert.

Solvable types that are both unitary and inert are called precise, and provide exact bounds.

Solvable correctness claims that all terms typable with a solvable type $\mtype$ are $\solvredsym$-normalizing, and the multiplicative size of the derivation bounds the number of $\tosolvm$ steps plus the solvable size of the $\solvredsym$-normal form; this bound is exact if the type context is inert is $\mtype$ is precisely solvable.

Let $\solvnf$ be a solvable fireball.
If $\namedtyjp{\tderiv}{}{\solvnf}{\typctx}{\mtype}$ with $\mtype$ solvable ($\typctx$  inert and $\mtype$ precisely solvable),
then $\sizem{\tderiv} \geq \sizes{\solvnf}$ ($\sizem{\tderiv} = \sizes{\solvnf}$).

Let us see with an example why in <Ref> we need the restrictions on the type and type contexts to have (exact) bounds.
Consider the solvable fireball (but non-inert) $\delta = \la{\var}{\var\var}$, which is typable and the last rule of any derivation $\concl{\tderiv}{\typctx}{\delta}{\mtype}$ is $\ruleManyVal$.
The solvable size of $\delta$ is $\sizes{\delta} = \sizes{\var\var} + 1$, so in order that $\sizem{\tderiv} \geq \sizes{\delta}$, $\ruleManyVal$ needs to have at least one premise (otherwise $\sizem{\tderiv} = 0 < \sizes{\delta}$),
which is exactly what the solvability of multi type $\mtype$ guarantees.
If moreover we want $\sizem{\tderiv} = \sizes{\delta}$,
any premise of $\ruleMany$ typing $\var\var$ must be an inert derivation $\concl{\tderivtwo}{\var \hastype \mtypetwo}{\var\var}{\mtypethree}$, thus $\sizem{\tderivtwo} =  \sizes{\var\var}$, and $\ruleManyVal$ must have only one premise.
Summing up, $\mtype= \mset{\larrow{\mtypetwo}{\mtypethree}}$, which is both unitary and inertly (as $\mtypetwo$ is inert) solvable, precisely solvable.

Assume $\concl{\tderiv}{\typctx}{\tm}{\mtype}$, with $\mtype$ solvable (unitary solvable).

* Multiplicative step: if $\tm \tosolvm \tm'$ then there is a derivation
$\concl{\tderiv'}{\typctx}{\tm'}{\mtype}$ such that $\sizem{\tderiv'} \leq \sizem{\tderiv}-2$ and $\size{\tderiv'} <
\size{\tderiv}$
($\sizem{\tderiv'} = \sizem{\tderiv}-2$ and $\size{\tderiv'} = \size{\tderiv}-1$);

* Exponential step: if $\tm \tosolve \tm'$ then there is a derivation
$\concl{\tderiv'}{\typctx}{\tm'}{\mtype}$ such that
$\sizem{\tderiv'} = \sizem{\tderiv}$ and $\size{\tderiv'} < \size{\tderiv}$.

Quantitative solving subject reduction (<Ref>)—as well as expansion (<Ref> below)—holds only for a restricted set of multi types, the solvable ones.
The reason is evident if we consider the term $\la{\vartwo}{\delta\delta}$: it is
and typable only through a derivation $\concl{\tderiv}{\,}{\la{\vartwo}\delta\delta}{\emptytype}$ with $\sizem{\tderiv} = 0 = \size{\tderiv}$, but $\la{\vartwo}{\delta\delta} \tosolvm \la{\vartwo}\var\esub{\var}{\delta}$ and $\emptytype$ is not a solvable multi type.

Let $\concl{\tderiv}{\typctx}{\tm}{\mtype}$ be a derivation with $\mtype$ solvable ($\typctx$ inert and $\mtype$ precisely solvable).
there is an $\solvredsym$-normalizing evaluation $\deriv \colon \tm \tosolv^* \tmtwo$
with $2\sizem{\deriv} + \sizes{\tmtwo} \leq \sizem{\tderiv}$ ($2\sizem{\deriv} + \sizes{\tmtwo} = \sizem{\tderiv}$).

For the typability of solvable normal forms, the ground type $\ground$ plays a crucial role, since $\mset{\ground}$ is both a precisely solvable and an inert multi type, and hence we can apply <Ref> when $\solvnf$ is an inert term.

If $\tm$ is a solvable fireball, then there is a derivation
$\concl{\tderiv}{\typctx}{\tm}{\mtype}$ with $\typctx$ inert and $\mtype$ precisely solvable.

Assume $\concl{\tderiv'\!}{\typctx}{\tm'\!}{\mtypetwo}$ with $\mtypetwo$ solvable (unitary solvable).

* Multiplicative step: if $\tm \tosolvm \tm'$ then there is a derivation
$\concl{\tderiv}{\typctx}{\tm}{\mtypetwo}$ with
$\sizem{\tderiv'} \leq \sizem{\tderiv}-2$ and
($\sizem{\tderiv'} = \sizem{\tderiv}-2$ and $\size{\tderiv'} = \size{\tderiv}-1$);

* Exponential step: if $\tm \tosolve \tm'$ then there is a derivation
$\concl{\tderiv}{\typctx}{\tm}{\mtypetwo}$ such that
$\sizem{\tderiv'} = \sizem{\tderiv}$ and $\size{\tderiv'} < \size{\tderiv}$.

Let $\deriv \colon \tm \tosolv^* \tmtwo$ be an $\solvsym$-normalizing evaluation.
Then there is a derivation $\concl{\tderiv}{\typctx}{\tm}{\mtypetwo}$ with $\typctx$ inert, $\mtypetwo$ precisely solvable 	and .