Université de Paris, CNRS, IRIF and Institut Universitaire de France,
Francekesner@irif.frhttps://orcid.org/0000-0003-4254-3129 Inria, Franceandres-
ezequiel.viso@inria.frhttps://orcid.org/0000-0002-6822-8453 Delia Kesner and
Andrés Viso [500]Theory of computation

###### Acknowledgements.

We are specially grateful to G. Guerrieri for fruitful discussions. We also
thank B. Accattoli, A. Bucciarelli, and A. Ríos for constructive remarks. This
work has been partially supported by IRP SINFIN. Florin Manea and Alex Simpson
30 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) CSL 2022
CSL 2022 February 14–19, 2022 Göttingen, Germany 216 19

# Encoding Tight Typing in a Unified Framework

Delia Kesner  Andrés Viso

###### Abstract

This paper explores how the intersection type theories of call-by-name (CBN)
and call-by-value (CBV) can be _unified_ in a more general framework provided
by call-by-push-value (CBPV). Indeed, we propose _tight_ type systems for CBN
and CBV that can be both encoded in a unique _tight_ type system for CBPV. All
such systems are quantitative, i.e. they provide _exact_ information about the
length of normalization sequences to normal form as well as the size of these
normal forms. Moreover, the length of reduction sequences are discriminated
according to their multiplicative and exponential nature, a concept inherited
from linear logic. Last but not least, it is possible to extract quantitative
measures for CBN and CBV from their corresponding encodings in CBPV.

###### keywords:

Call-by-Push-Value, Call-by-Name, Call-by-Value, Intersection Types

##  1 Introduction

Every programming language implements a particular evaluation strategy which
specifies when and how parameters are evaluated during function calls. For
example, in call-by-value (CBV), the argument is evaluated before being passed
to the function, while in call-by-name (CBN) the argument is substituted
directly into the function body, so that the argument may never be evaluated,
or may be re-evaluated several times. CBN and CBV have always been studied
independently, by developing different techniques for one and the other, until
the remarkable observation that they are two different instances of a more
general framework introduced by Girard’s Linear Logic (LL). Their (logical)
duality (“CBN is _dual_ to CBV”) was understood later [18, 17]. And their
rewriting semantics were finally _unified_ by the call-by-push-value (CBPV)
paradigm —introduced by P.B. Levy [40, 41]—, a formalism being able to capture
different functional languages/evaluation strategies.

A typical aspect that one wants to compare between two different evaluation
strategies is the _number of steps_ that are necessary to get a result. Such
numbers are extracted from different models of computation and should be then
measured by _compatible_ instruments, either by means of common quantitative
tools, or by a precise transformation between them111Think for example about
cm and inches.. Thus, we provide a _uniform_ tool to measure quantitative
information extracted from the evaluation of programs in different programming
languages (namely CBN and CBV).

More concretely, we introduce typing systems capturing qualitative and
quantitative information of programs. From a qualitative point of view, the
typing systems characterize termination of programs, i.e. a program $p$ is
typable if and only if $p$ terminates. From a quantitative point of view, the
typing systems provide exact/tight information about the number of steps
needed to get a result, as well as the size of this result. All these
questions are addressed in the general framework of CBPV, being able to encode
CBN and CBV, both from a static and a dynamic point of view. Dynamically, CBN
and CBV evaluation strategies are known to be encodable by the rewriting
semantics of CBPV. Statically, we define tight typing systems providing
quantitative information for CBN and CBV, that can be seen as particular cases
of the tight quantitative typing system behind the unified framework of CBPV.
We now explain all these concepts in more detail.

Quantitative Types. Quantitative typing systems are often specified by non-
idempotent intersection types inspired by the relational semantics of LL [30,
11], as pioneered by [28]. This connection makes non-idempotent types not only
a qualitative typing tool to reason about programming languages, but mainly a
quantitative one, being able to specify properties related to the consumption
of resources, a remarkable investigation pioneered by the seminal de
Carvalho’s PhD thesis [19] (see also [21]). Thus, qualitatively, a non-
idempotent typing system is able to fully characterise normalisation, in the
sense that a term $t$ is typable if and only if $t$ is normalising. More
interestingly, quantitative typing systems also provide upper bounds, in the
sense that the length of any reduction sequence from $t$ to normal form _plus_
the size of this normal form is _bounded_ by the size of the type derivation
of $t$. Therefore, typability characterises normalisation in a qualitative as
well as in a quantitative way, but only provides upper bounds. Several papers
explore bounded measures of non-idempotent types for different higher order
languages. Some references are [24, 31, 4, 3, 35, 14, 20, 33, 23, 22, 13, 43].

In this satisfactory enough? A major observation concerning $\beta$-reduction
in $\lambda$-calculus is that the size of normal forms can be _exponentially_
bigger than the number of steps needed to reach these normal forms. This means
that bounding the sum of these two integers _at the same_ time is too rough,
and not very relevant from a quantitative point of view. Fortunately, it is
possible to extract better (i.e. independent and exact) measures from a non-
idempotent intersection type system. A crucial point to obtain exact measures,
instead of upper bounds, is to consider _minimal_ type derivations [19, 9,
23]. Therefore, _upper bounds_ for time _plus_ size can be refined into
_independent exact measures_ for time _and_ size [1]. More precisely, the
quantitative typing systems are now equipped with constants and _counters_ ,
together with an appropriate notion of tightness, which encodes minimality of
type derivations. For any _tight_ type derivation $\Phi$ of a term $t$ ending
with (independent) counters $(\mathit{b},\mathit{s})$, it is now possible to
show that $t$ is normalisable in $\mathit{b}$ steps and its normal form has
size $\mathit{s}$, so that the type system is able to _guess_ the number of
steps to normal form as well as the size of this normal form. The opposite
direction also holds: if $t$ normalises in $\mathit{b}$ steps to a normal form
size $\mathit{s}$, then it is possible to tightly type $t$ by using
(independent) counters $(\mathit{b},\mathit{s})$.

In this paper we design tight quantitative type systems that are also capable
to discriminate between multiplicative and exponential evaluation steps to
normal form, two conceptual notions coming from LL: _multiplicative_ steps are
essentially those that (linearly) reconfigure proofs/terms/programs, while
_exponential_ steps are the only ones that are potentially able to
erase/duplicate other objects. As a consequence, for any _tight_ type
derivation $\Phi$ of $t$ ending with (independent) counters
$(\mathit{m},\mathit{e},\mathit{s})$, the term $t$ is normalisable in
$\mathit{m}$ multiplicative and $\mathit{e}$ exponential steps to a normal
form having size $\mathit{s}$. The opposite direction also holds.

Call-by-push-value. CBPV extends the $\lambda$-calculus with two primitives
$\mathtt{thunk}$ and $\mathtt{force}$ distinguishing between _values_ and
_computations_ : the former freezes the execution of a term (i.e. turns a
computation into a value) while the latter fires again a frozen term (i.e.
turns a value into a computation). These primitives allow to capture the
duality between CBN and CBV by conveniently labelling a $\lambda$-term with
$\mathtt{thunk}/\mathtt{force}$ to pause/resume the evaluation of a subterm.
Thus, CBPV provides a _unique_ and _general_ formalism capturing different
functional strategies, and allowing to _uniformly_ study operational and
denotational semantics of different programming languages through a single
tool.

In this paper we model the CBPV paradigm by using the $\lambda!$-calculus
[12], based on the _bang calculus_ introduced in [26], which in turn extends
ideas by T. Ehrhard [25]. The granularity of the $\lambda!$-calculus,
expressed with both explicit substitutions and reduction at a distance
(details in Sec. 5), clearly allows to differentiate between _multiplicative_
and _exponential_ steps, as in LL. The corresponding CBN and CBV strategies
also follow this pattern: it is possible to distinguish the multiplicative
steps that only reconfigure pieces of syntax, from the exponential steps used
to implement erasure and duplication of terms.

Contributions. We first define deterministic strategies for CBN and CBV that
are able to discriminate between multiplicative and exponential steps (Sec.
2).

We then formulate tight typing systems for both CBN (Sec. 3) and CBV (Sec. 4),
called respectively $\mathcal{N}$ and $\mathcal{V}$. System $\mathcal{N}$ is a
direct extension of Gardner’s system [28], while system $\mathcal{V}$ is
completely new, and constitutes one of the major contributions of this paper.
A key feature of system $\mathcal{V}$ is its ability to distinguish between
the two different roles that variables may play in CBV depending on the
context where they are placed, i.e. to be a placeholder for a _value_ or the
head of a _neutral_ term. We show that both systems implement independent
measures for time and size, and that they are quantitatively sound and
complete. More precisely, we show that tight (i.e. minimal) typing derivations
in such systems (exactly) quantitatively characterise normalisation, i.e. if
$\Phi$ is a _tight_ type derivation of $t$ in system $\mathcal{N}$ (resp.
$\mathcal{V}$), ending with counters $(\mathit{m},\mathit{e},\mathit{s})$,
then there exists a CBN (resp. CBV) normal form $p$ of size $\mathit{s}$ such
that $t$ reduces to $p$ by using exactly $\mathit{m}$ multiplicative steps and
$\mathit{e}$ exponential steps. The converse, giving quantitative completeness
of the approach, also holds.

Sec. 5 recalls the bang calculus at a distance $\lambda!$ and Sec. 6 presents
its associated tight type system $\mathcal{B}$, together with their respective
quantitative sound and complete properties. The untyped CBN/CBV translations
into $\lambda!$ are recalled in Sec. 7, while the typed translations are
defined and discussed in Sec. 8, the other major contribution of this work.
Through these typed encodings, the counters of the source and target
derivations are related. This makes it possible to give the precise cost of
our typed translations, as well as to extract quantitative measures for CBN
and CBV from their corresponding encodings in CBPV.

Related Work. For CBN, non-idempotent types were introduced by [28], their
quantitative power was extensively studied in [19, 20], and their tight
extensions in [9, 1]. For CBV, non-idempotent types were introduced in [24],
and extensively studied, e.g. [31, 3]. A tight extension being able to count
reduction steps was recently defined in [4, 39] for a special version of
(closed) CBV, but it is not clear how this could be encoded in a linear logic
based CBPV framework. Another non-idempotent type system was also recently
introduced for CBV [42, 34], it is not tight and does not translate to CBPV.

A (non-tight) quantitative type system for the bang calculus, based on a
relational model, can be found in [32]. Another relational model that can be
seen as a non-tight system for CBPV was introduced by [16]. Following ideas in
[19, 9, 1], a type system $\mathcal{E}$ was proposed in [12] to fully exploit
tight quantitative aspects of the $\lambda!$-calculus: _independent exact
measures_ for time and size are guessed by the types system. However, no
relation between tightness for CBN/CBV and tightness for the
$\lambda!$-calculus are studied in op.cite. This papers fills this gap.

The discrimination between multiplicative and exponential steps by means of
tight quantitative types can be found e.g. in CBN [1], call-by-need [4], and
languages with pattern-matching primitives [7].

##  2 Call-by-Name and Call-by-Value

This section introduces the CBN and CBV specifications being able to
distinguish between multiplicative and exponential steps, as in linear logic.
Given a countably infinite set $\mathcal{X}$ of variables $x,y,z,\ldots$, we
consider the following grammars for terms ($\mathcal{T_{\lambda}}$), values
and contexts:

| _(Terms)_ | $t,u,r$ | $::=$ | $v\mid{t}\,{u}\mid{t}[{x}\backslash{u}]$
---|---|---|---
_(Values)_ | $v$ | $::=$ | $x\in\mathcal{X}\mid\lambda{x}.{t}$
_(Contexts)_ | $\mathtt{C}$ | $::=$ | $\mathtt{L}\mid\mathtt{N}\mid\mathtt{V}$
_(List Contexts)_ | $\mathtt{L}$ | $::=$ | $\Box\mid{\mathtt{L}}[{x}\backslash{t}]$
_(CBN Contexts)_ | $\mathtt{N}$ | $::=$ | $\Box\mid{\mathtt{N}}\,{t}\mid\lambda{x}.{\mathtt{N}}\mid{\mathtt{N}}[{x}\backslash{u}]$
_(CBV Contexts)_ | $\mathtt{V}$ | $::=$ | $\Box\mid{\mathtt{V}}\,{t}\mid{t}\,{\mathtt{V}}\mid{\mathtt{V}}[{x}\backslash{u}]\mid{t}[{x}\backslash{\mathtt{V}}]$

A terms of the form ${t}[{x}\backslash{u}]$ is a _closure_ , and
$[{x}\backslash{u}]$ an _explicit substitution_ (ES). Special terms are ${\tt
I}=\lambda{z}.{z}$, ${\tt K}=\lambda{x}.{\lambda{y}.{x}}$,
$\Delta=\lambda{x}.{{x}\,{x}}$, and $\Omega={\Delta}\,{\Delta}$. We use
${\mathtt{C}}\langle{t}\rangle$ for the term obtained by replacing the hole
$\Box$ of $\mathtt{C}$ by $t$. _Free_ and _bound_ variables, as well as
$\alpha$-conversion, are defined as expected. In particular,
$\mathtt{fv}({{t}[{x}\backslash{u}]})\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{fv}({t})\setminus\\{{x}\\}\cup\mathtt{fv}({u})$,
$\mathtt{fv}({\lambda{x}.{t}})\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{fv}({t})\setminus\\{{x}\\}$,
$\mathtt{bv}({{t}[{x}\backslash{u}]})\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{bv}({t})\cup\\{{x}\\}\cup\mathtt{bv}({u})$
and
$\mathtt{bv}({\lambda{x}.{t}})\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{bv}({t})\cup\\{{x}\\}$.
The notation ${{t}\left\\{{x}\backslash{u}\right\\}}$ is used for the
(capture-free) _meta-level_ substitution operation, defined, as usual, modulo
$\alpha$-conversion. Special predicates are used to distinguish different
kinds of terms surrounded by ES: $\mathsf{abs}(t)$ iff
$t={\mathtt{L}}\langle{\lambda{x}.{u}}\rangle$, $\mathsf{app}(t)$ iff
$t={\mathtt{L}}\langle{{r}\,{u}}\rangle$ and $\mathsf{var}(t)$ iff
$t={\mathtt{L}}\langle{x}\rangle$. Finally, $\mathsf{val}(t)$ iff
$\mathsf{abs}(t)$ or $\mathsf{var}(t)$.

As mentioned in the introduction, our aim is to count the reduction steps by
distinguishing their multiplicative and exponential nature. To achieve this,
the standard specifications of CBN/CBV are not adequate, so we need to
consider alternative appropriate definitions [6] making use of the following
three different rewriting rules:

$\begin{array}[]{rlll}\mbox{({\normalsize{d}}istant
{\normalsize{B}}eta)}&{{\mathtt{L}}\langle{\lambda{x}.{t}}\rangle}\,{u}&\mathrel{\mapsto_{\mathtt{dB}}}&{\mathtt{L}}\langle{{t}[{x}\backslash{u}]}\rangle\\\
\mbox{({\normalsize{s}}ubstitute
term)}&{t}[{x}\backslash{u}]&\mathrel{\mapsto_{\mathtt{sn}}}&{{t}\left\\{{x}\backslash{u}\right\\}}\\\
\mbox{({\normalsize{s}}ubstitute
{v}alue)}&{t}[{x}\backslash{{\mathtt{L}}\langle{v}\rangle}]&\mathrel{\mapsto_{\mathtt{sv}}}&{\mathtt{L}}\langle{{{t}\left\\{{x}\backslash{v}\right\\}}}\rangle\end{array}$

Rule $\mathtt{dB}$ fires $\beta$-reduction _at a distance_ by combining the
two more elementary rules:
${(\lambda{x}.{t})}\,{u}\mathrel{\mapsto}{t}[{x}\backslash{u}]$ and
${{\mathtt{L}}\langle{t}\rangle}\,{u}\mathrel{\mapsto}{\mathtt{L}}\langle{{t}\,{u}}\rangle$,
where the second one is a structural/permutation rule pushing out ES that may
block $\beta$-redexes. Rule $\mathtt{sn}$ implements standard substitution,
while $\mathtt{sv}$ restricts substitution to values and acts _at a distance_
by combining the two more elementary rules:
${t}[{x}\backslash{v}]\mathrel{\mapsto}{{t}\left\\{{x}\backslash{v}\right\\}}$
and
${t}[{x}\backslash{{\mathtt{L}}\langle{v}\rangle}]\mathrel{\mapsto}{\mathtt{L}}\langle{{t}[{x}\backslash{v}]}\rangle$.
The _call-by-name_ reduction relation $\rightarrow_{\mathtt{n}}$ is the
closure by contexts $\mathtt{N}$ of the rules $\mathtt{dB}$ and $\mathtt{sn}$,
while the _call-by-value_ reduction relation $\rightarrow_{\mathtt{v}}$ is the
closure by contexts $\mathtt{V}$ of the rules $\mathtt{dB}$ and $\mathtt{sv}$.
Equivalently,

$\mathbin{\rightarrow_{\mathtt{n}}}:=\mathtt{N}(\mathrel{\mapsto_{\mathtt{dB}}}\cup\mathrel{\mapsto_{\mathtt{sn}}})\quad$
and
$\quad\mathbin{\rightarrow_{\mathtt{v}}}:=\mathtt{V}(\mathrel{\mapsto_{\mathtt{dB}}}\cup\mathrel{\mapsto_{\mathtt{sv}}})$

The resulting CBN/CBV formulations are now based on distinguished
_multiplicative_ (cf. $\mathtt{dB}$) and _exponential_ (cf. $\mathtt{sn}$ and
$\mathtt{sv}$) steps, called resp. $\mathtt{m}$-steps and $\mathtt{e}$-steps,
thus inheriting the nature of cut elimination rules in LL. Notice that the
number of $\mathtt{m}$ and $\mathtt{e}$-steps in a normalization sequence is
not always the same: e.g. ${x}[{x}\backslash{y}]\rightarrow_{\mathtt{n}}y$ has
only one $\mathtt{e}$-step, and ${(\lambda{x}.{x})}\,{({z}\,{{\tt
I}})}\rightarrow_{\mathtt{v}}{x}[{x}\backslash{{z}\,{{\tt I}}}]$ has only one
$\mathtt{m}$-step. We write $t\not\rightarrow_{\mathtt{n}}$ (resp.
$t\not\rightarrow_{\mathtt{v}}$), and call $t$ an _$\mathtt{n}$ -normal form_
(resp. _$\mathtt{v}$ -normal form_), if $t$ cannot be reduced by means of
$\rightarrow_{\mathtt{n}}$ (resp. $\rightarrow_{\mathtt{v}}$). Both CBN and
CBV are non-deterministic: $t\rightarrow_{\mathtt{n}}u$ and
$t\rightarrow_{\mathtt{n}}s$ does not necessarily implies $u=s$. But both
calculi enjoy confluence, notably because their rules are orthogonal [38, 37].
Moreover, in each calculus, it is easy to show that any two different
reduction paths to normal form have the same number of multiplicative and
exponential steps.

CBN is to be understood as _head_ reduction [8], i.e. reduction does not take
place in arguments of applications, while CBV corresponds to _open_ CBV
reduction [6, 2], i.e. reduction does not take place inside abstractions. The
sets of $\mathtt{n}/\mathtt{v}$-normal forms can be alternatively
characterised by the following grammars [12]:

| _(CBN Neutral)_ | $\mathsf{ne}_{\mathtt{n}}$ | $::=$ | $x\in\mathcal{X}\mid{\mathsf{ne}_{\mathtt{n}}}\,{t}$
---|---|---|---
_(CBN Normal)_ | $\mathsf{no}_{\mathtt{n}}$ | $::=$ | $\lambda{x}.{\mathsf{no}_{\mathtt{n}}}\mid\mathsf{ne}_{\mathtt{n}}$
| _(CBV Variable)_ | $\mathsf{vr}_{\mathtt{v}}$ | $::=$ | $x\in\mathcal{X}\mid{\mathsf{vr}_{\mathtt{v}}}[{x}\backslash{\mathsf{ne}_{\mathtt{v}}}]$
---|---|---|---
_(CBV Neutral)_ | $\mathsf{ne}_{\mathtt{v}}$ | $::=$ | ${\mathsf{vr}_{\mathtt{v}}}\,{\mathsf{no}_{\mathtt{v}}}\mid{\mathsf{ne}_{\mathtt{v}}}\,{\mathsf{no}_{\mathtt{v}}}\mid{\mathsf{ne}_{\mathtt{v}}}[{x}\backslash{\mathsf{ne}_{\mathtt{v}}}]$
_(CBV Normal)_ | $\mathsf{no}_{\mathtt{v}}$ | $::=$ | $\lambda{x}.{t}\mid\mathsf{vr}_{\mathtt{v}}\mid\mathsf{ne}_{\mathtt{v}}\mid{\mathsf{no}_{\mathtt{v}}}[{x}\backslash{\mathsf{ne}_{\mathtt{v}}}]$

In contrast to CBN, variables are left out of the definition of neutral terms
for the CBV case, since they are now considered as values. However, even if
CBV variables are not neutral terms, neutral terms are necessarily headed by a
variable, so that variables play a double role which is difficult to be
distinguished by means of an intersection type system. We will come back to
this point in Sec. 4. Excluding variables from the set of values brings a
remarkable speed up in implementations of CBV [39], but goes beyond the
logical Girard’s translation of CBV into LL, which is the main topic of this
paper. Our chosen approach allows both CBN and CBV neutral terms to translate
to neutral terms of the $\lambda!$-calculus (cf. Sec. 5).

Deterministic Strategies for CBN and CBV. As a technical tool, in order to
count the reduction steps of CBN/CBV we first fix a deterministic version for
them. The reduction relation $\rightarrow_{\mathtt{dn}}$ is a deterministic
version of $\rightarrow_{\mathtt{n}}$ defined as:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.59262pt\hbox{$\displaystyle\penalty
1\vphantom{\mathtt{L}\rightarrow_{\mathtt{dn}}}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=94.65752pt\hbox{}}}\hbox{\kern
0.0pt\kern
0.0pt\hbox{$\displaystyle{{{\mathtt{L}}\langle{\lambda{x}.{t}}\rangle}\,{u}\rightarrow_{\mathtt{dn}}{\mathtt{L}}\langle{{t}[{x}\backslash{u}]}\rangle}$}}}}\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.3148pt\hbox{$\displaystyle\penalty
1\vphantom{\mathtt{L}\rightarrow_{\mathtt{dn}}}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=74.10188pt\hbox{}}}\hbox{\kern
0.0pt\kern
0.0pt\hbox{$\displaystyle{{t}[{x}\backslash{u}]\rightarrow_{\mathtt{dn}}{{t}\left\\{{x}\backslash{u}\right\\}}}$}}}}\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1t\rightarrow_{\mathtt{dn}}s\mbox{ and
}\neg\mathsf{abs}(t)$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=74.85432pt\hbox{}}}\hbox{\kern
0.0pt\kern
18.88666pt\hbox{$\displaystyle{{t}\,{u}\rightarrow_{\mathtt{dn}}{s}\,{u}}$}}}}\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 16.51158pt\hbox{$\displaystyle\penalty
1t\rightarrow_{\mathtt{dn}}s$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.32175pt\hbox{}}}\hbox{\kern
0.0pt\kern
0.0pt\hbox{$\displaystyle{\lambda{x}.{t}\rightarrow_{\mathtt{dn}}\lambda{x}.{u}}$}}}}$

Similarly, the reduction relation $\rightarrow_{\mathtt{dv}}$ is a
deterministic version of $\rightarrow_{\mathtt{v}}$ defined as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 34.3065pt\hbox{$\displaystyle\penalty
1\vphantom{\mathsf{abs}(t)}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=94.50195pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\mathtt{L}}\langle{\lambda{x}.{t}}\rangle}\,{u}\rightarrow_{\mathtt{dv}}{\mathtt{L}}\langle{{t}[{x}\backslash{u}]}\rangle$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
35.31575pt\hbox{$\displaystyle\penalty 1\vphantom{\mathsf{abs}(t)}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=96.52045pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{t}[{x}\backslash{{\mathtt{L}}\langle{v}\rangle}]\rightarrow_{\mathtt{dv}}{\mathtt{L}}\langle{{{t}\left\\{{x}\backslash{v}\right\\}}}\rangle$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1t\rightarrow_{\mathtt{dv}}s\quad\neg\mathsf{abs}(t)$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.3653pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
16.1088pt\hbox{$\displaystyle{t}\,{u}\rightarrow_{\mathtt{dv}}{s}\,{u}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1t\rightarrow_{\mathtt{dv}}s\quad
u\in\mathsf{ne}_{\mathtt{v}}\cup\mathsf{vr}_{\mathtt{v}}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=79.08432pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
22.4683pt\hbox{$\displaystyle{u}\,{t}\rightarrow_{\mathtt{dv}}{u}\,{s}$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
0.8843pt\hbox{$\displaystyle\penalty
1t\rightarrow_{\mathtt{dv}}s\quad\neg\mathsf{val}(t)$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.1339pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{u}[{x}\backslash{t}]\rightarrow_{\mathtt{dv}}{u}[{x}\backslash{s}]$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.93315pt\hbox{$\displaystyle\penalty 1t\rightarrow_{\mathtt{dv}}s\quad
u\in\mathsf{ne}_{\mathtt{v}}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.1339pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{t}[{x}\backslash{u}]\rightarrow_{\mathtt{dv}}{s}[{x}\backslash{u}]$}}}}\end{array}$

As a matter of notation, for $\mathcal{X}\in\\{{\mathtt{dn},\mathtt{dv}}\\}$,
we write $t\twoheadrightarrow_{\mathcal{X}}^{(\mathit{m},\mathit{e})}u$ if
$t\twoheadrightarrow_{\mathcal{X}}u$ using $\mathit{m}$ multiplicative steps
and $\mathit{e}$ exponential steps.

The normal forms of the non-deterministic and the deterministic versions of
CBN/CBV are the same, in turn characterised by the grammars
$\mathsf{no}_{\mathtt{n}}$/$\mathsf{no}_{\mathtt{v}}$ [12].

######  Proposition 2.1.

Let $t\in\mathcal{T_{\lambda}}$. Then, $t\not\rightarrow_{\mathtt{n}}$ iff
$t\not\rightarrow_{\mathtt{dn}}$ iff $t\in\mathsf{no}_{\mathtt{n}}$ and
$t\not\rightarrow_{\mathtt{v}}$ iff $t\not\rightarrow_{\mathtt{dv}}$ iff
$t\in\mathsf{no}_{\mathtt{v}}$.

######  Proof 2.2.

  1. 1.

$t\not\rightarrow_{\mathtt{n}}$ implies $t\not\rightarrow_{\mathtt{dn}}$
follows from $\rightarrow_{\mathtt{dn}}\subset\rightarrow_{\mathtt{n}}$.

  2. 2.

$t\in\mathsf{no}_{\mathtt{n}}$ iff $t\not\rightarrow_{\mathtt{n}}$ is shown
simultaneously by considering the following statements:

    1. (a)

$t\in\mathsf{ne}_{\mathtt{n}}$ iff $t\not\rightarrow_{\mathtt{n}}$ and
$\neg\mathsf{abs}(t)$.

    2. (b)

$t\in\mathsf{no}_{\mathtt{n}}$ iff $t\not\rightarrow_{\mathtt{n}}$.

    1. (a)

The left-to-right implication is straightforward. For the right-to-left
implication we reason by induction on terms. Suppose
$t\not\rightarrow_{\mathtt{n}}$ and $\neg\mathsf{abs}(t)$. If $t$ is a
substitution, then rule $\mathtt{sn}$ is applicable, contradiction. Then
$t={u}\,{u^{\prime}}$, where $\neg\mathsf{abs}(u)$ (otherwise $\mathtt{dB}$
would be applicable) and $u\not\rightarrow_{\mathtt{n}}$ (otherwise $t$ would
be $\mathtt{n}$-reducible). The i.h. (2a) gives $u\in\mathsf{ne}_{\mathtt{n}}$
and thus we conclude $t={u}\,{u^{\prime}}\in\mathsf{ne}_{\mathtt{n}}$.

    2. (b)

The left-to-right implication is straightforward. For the right-to-left
implication we reason by induction on terms. If $t=\lambda{x}.{u}$, then
$u\not\rightarrow_{\mathtt{n}}$, and the i.h. (2b) gives
$u\in\mathsf{no}_{\mathtt{n}}$, which implies in turn
$\lambda{x}.{u}\in\mathsf{no}_{\mathtt{n}}$. Otherwise, we apply the previous
case.

  3. 3.

$t\not\rightarrow_{\mathtt{dn}}$ implies $t\in\mathsf{no}_{\mathtt{n}}$
follows a straightforward adaptation of the previous right-to-left
implication.

  4. 4.

$t\not\rightarrow_{\mathtt{v}}$ implies
$t\not\twoheadrightarrow_{\mathtt{dv}}$ follows from
$\rightarrow_{\mathtt{dv}}\subset\rightarrow_{\mathtt{v}}$.

  5. 5.

$t\in\mathsf{no}_{\mathtt{v}}$ iff $t\not\rightarrow_{\mathtt{v}}$ is shown
simultaneously by considering the following statements:

    1. (a)

$t\in\mathsf{vr}_{\mathtt{v}}$ iff $t\not\rightarrow_{\mathtt{v}}$ and
$\neg\mathsf{abs}(t)$ and $\neg\mathsf{app}(t)$.

    2. (b)

$t\in\mathsf{ne}_{\mathtt{v}}$ iff $t\not\rightarrow_{\mathtt{v}}$ and
$\neg\mathsf{abs}(t)$ and $\neg\mathsf{var}(t)$.

    3. (c)

$t\in\mathsf{no}_{\mathtt{v}}$ iff $t\not\rightarrow_{\mathtt{v}}$.

    1. (a)

The left-to-right implication is straightforward. For the right-to-left
implication we reason by induction on terms. Suppose
$t\not\rightarrow_{\mathtt{v}}$ and $\neg\mathsf{abs}(t)$ and
$\neg\mathsf{app}(t)$. Then necessarily $\mathsf{var}(t)$. If
$t={u}[{x}\backslash{u^{\prime}}]$, then
$u,u^{\prime}\not\rightarrow_{\mathtt{v}}$ (otherwise $t$ would be
$\mathtt{v}$-reducible), $\neg\mathsf{abs}(u^{\prime})$ and
$\neg\mathsf{var}(u^{\prime})$ (otherwise $t$ would be
$\mathtt{sv}$-reducible), $\neg\mathsf{abs}(u)$ and $\neg\mathsf{app}(u)$. The
i.h. (5a) gives $u\in\mathsf{vr}_{\mathtt{v}}$ and
$u^{\prime}\in\mathsf{ne}_{\mathtt{v}}$, so that we conclude
$t\in\mathsf{vr}_{\mathtt{v}}$. If $t=x$ we trivially conclude
$t\in\mathsf{vr}_{\mathtt{v}}$.

    2. (b)

The left-to-right implication is straightforward. For the right-to-left
implication we reason by induction on terms. Suppose
$t\not\rightarrow_{\mathtt{v}}$ and $\neg\mathsf{abs}(t)$ and
$\neg\mathsf{var}(t)$. Then necessarily $\mathsf{app}(t)$. If
$t={u}[{x}\backslash{u^{\prime}}]$, then
$u,u^{\prime}\not\rightarrow_{\mathtt{v}}$ (otherwise $t$ would be
$\mathtt{v}$-reducible), $\neg\mathsf{abs}(u^{\prime})$ and
$\neg\mathsf{var}(u^{\prime})$ (otherwise $t$ would be
$\mathtt{sv}$-reducible), $\neg\mathsf{abs}(u)$ and $\neg\mathsf{var}(u)$. The
i.h. (5b) gives $u\in\mathsf{ne}_{\mathtt{v}}$ and
$u^{\prime}\in\mathsf{ne}_{\mathtt{v}}$, so that we conclude
$t\in\mathsf{ne}_{\mathtt{v}}$. If $t={u}\,{u^{\prime}}$, then
$u,u^{\prime}\not\rightarrow_{\mathtt{v}}$ (otherwise $t$ would be
$\mathtt{v}$-reducible), $\neg\mathsf{abs}(u)$ (otherwise $t$ would be
$\mathtt{dB}$-reducible). Moreover, $\neg\mathsf{app}(u)$ or
$\neg\mathsf{var}(u)$ holds. The i.h. (5c) gives
$u^{\prime}\in\mathsf{no}_{\mathtt{v}}$ and ($u\in\mathsf{vr}_{\mathtt{v}}$ or
$u\in\mathsf{ne}_{\mathtt{v}}$). In both cases we conclude
$t={u}\,{u^{\prime}}\in\mathsf{ne}_{\mathtt{v}}$.

    3. (c)

The left-to-right implication is straightforward. For the right-to-left
implication we reason by induction on terms. Suppose
$t\not\rightarrow_{\mathtt{v}}$. If $t=\lambda{x}.{u}$, then
$t\in\mathsf{no}_{\mathtt{v}}$ is straightforward. If
$t={u}[{x}\backslash{u^{\prime}}]$, then
$u,u^{\prime}\not\rightarrow_{\mathtt{v}}$ (otherwise $t$ would be
$\mathtt{v}$-reducible), $\neg\mathsf{abs}(u^{\prime})$ and
$\neg\mathsf{var}(u^{\prime})$ (otherwise $t$ would be
$\mathtt{sv}$-reducible). The i.h. (5c) and (5b) give
$u\in\mathsf{no}_{\mathtt{v}}$ and $u^{\prime}\in\mathsf{ne}_{\mathtt{v}}$, so
that we conclude $t\in\mathsf{no}_{\mathtt{v}}$. If $t={u}\,{u^{\prime}}$,
then $u\not\rightarrow_{\mathtt{v}}$ and
$u^{\prime}\not\rightarrow_{\mathtt{v}}$. The i.h. (5c) on $u^{\prime}$ gives
$u^{\prime}\in\mathsf{no}_{\mathtt{v}}$. Moreover, $\neg\mathsf{abs}(u)$,
otherwise $t$ would be $\mathtt{v}$-reducible. Then $\neg\mathsf{var}(u)$ or
$\neg\mathsf{app}(u)$. The i.h. (5a) or (5b) gives
$u\in\mathsf{vr}_{\mathtt{v}}$ or $u\in\mathsf{ne}_{\mathtt{v}}$. Thus
${u}\,{u^{\prime}}\in\mathsf{ne}_{\mathtt{v}}\subseteq\mathsf{no}_{\mathtt{v}}$
as required.

  6. 6.

$t\not\rightarrow_{\mathtt{dv}}$ implies $t\in\mathsf{no}_{\mathtt{v}}$
follows a straightforward adaptation of the previous right-to-left
implication.

(Head) CBN ignores reduction inside arguments of applications, while (Open)
CBV ignores reduction inside abstractions, then CBN (resp. CBV) normal forms
are measured by the following _$\mathtt{n}$ -size_ (resp. _$\mathtt{v}$
-size_) function:

$\begin{array}[]{llllll}|{x}|_{\mathtt{n}}:=0&|{\lambda{x}.{t}}|_{\mathtt{n}}:=|{t}|_{\mathtt{n}}+1&|{{t}\,{u}}|_{\mathtt{n}}:=|{t}|_{\mathtt{n}}+1&|{{t}[{x}\backslash{u}]}|_{\mathtt{n}}:=|{t}|_{\mathtt{n}}\\\
|{x}|_{\mathtt{v}}:=0&|{\lambda{x}.{t}}|_{\mathtt{v}}:=0&|{{t}\,{u}}|_{\mathtt{v}}:=|{t}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}+1&|{{t}[{x}\backslash{u}]}|_{\mathtt{v}}:=|{t}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}\end{array}$

##  3 Tight Call-by-Name

We now introduce a tight type system $\mathcal{N}$ for CBN which captures
independent exact measures for $\rightarrow_{\mathtt{n}}$-reduction sequences.
This result is not surprising, since it extends the one in [1] from the pure
$\lambda$-calculus to our CBN calculus. However, we revisit the op.cit.
approach by appropriately splitting reduction into multiplicative and
exponential steps, a reformulation necessary to establish a precise
correspondence with the tight type system for the $\lambda!$-calculus. In
particular, our _counting_ mechanism slightly differs from [1] (details
below).

In system $\mathcal{N}$ there are two base types: $\mathtt{a}$ types terms
whose normal form is an abstraction, and $\mathtt{n}$ types terms whose normal
form is CBN neutral. The grammar of types is given by:

_(Tight Types)_ | $\mathtt{tt}$ | $::=$ | $\mathtt{n}\mid\mathtt{a}$
---|---|---|---
_(Types)_ | $\sigma,\tau$ | $::=$ | $\mathtt{tt}\mid\mathcal{M}\mid{\mathcal{M}}\to{\sigma}$
_(Multitypes)_ | $\mathcal{M},\mathcal{N}$ | $::=$ |  $[\sigma_{i}]_{i\in I}$ where $I$ is a finite set

Multitypes are multisets of types. The _empty multitype_ is denoted by $[\,]$,
$\sqcup$ denotes multitype union, and $\sqsubseteq$ multitype inclusion. Also,
$|\mathcal{M}|$ denotes the size of the multitype, thus if
$\mathcal{M}=[\sigma_{i}]_{i\in I}$ then $|\mathcal{M}|=\\#(I)$. Notice that
the grammar for types slightly differs from [1], in particular types are now
allowed to be just multitypes. The main reason to adopt this change is that
this (unique) grammar is used for our three formalisms CBN, CBV, and CBPV,
changing only the definition of tight types for each case222In the
intersection type literature CBN and CBV do always adopt different grammars..

_Typing contexts_ (or just _contexts_), written $\Gamma,\Delta$, are functions
from variables to multitypes, assigning the empty multitype to all but a
finite set of variables. The domain of $\Gamma$ is given by
$\mathtt{dom}({\Gamma})\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\\{{x\mid\Gamma(x)\neq[\,]}\\}$.
The _union of contexts_ , written ${\Gamma}\mathrel{+}{\Delta}$, is defined by
$({\Gamma}\mathrel{+}{\Delta})(x)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\Gamma(x)\sqcup\Delta(x)$.
An example is
${({x}:{[\sigma]},{y}:{[\tau]})}\mathrel{+}{({x}:{[\sigma]},{z}:{[\tau]})}=({x}:{[\sigma,\sigma]},{y}:{[\tau]},{z}:{[\tau]})$.
This notion is extended to several contexts as expected, so that
${}\mathrel{+_{i\in I}}{}\Gamma_{i}$ denotes a finite union of contexts
(particularly the empty context when $I=\emptyset$). We write
${\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}$ for the context
$({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})(x)=[\,]$ and
$({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})(y)=\Gamma(y)$ if $y\neq x$.

_Type judgements_ have the form
${\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}$,
where $\Gamma$ is a typing context, $t$ is a term, $\sigma$ is a type, and the
_counters_ $(\mathit{m},\mathit{e},\mathit{s})$ are expected to provide the
following information: $\mathit{m}$ (resp. $\mathit{e}$) indicates the number
of multiplicative $\mathtt{m}$-steps (resp. exponential $\mathtt{e}$-steps) to
normal form, while $\mathit{s}$ indicates the $\mathtt{n}$-size of this normal
form. It is worth noticing that the $\lambda$-calculus hides both
multiplicative and exponential steps in one single $\beta$-reduction rule [1],
so that only two counters suffice, one for the number of $\beta$-reduction
steps, and another for the size of normal forms. Here we want to discriminate
between multiplicative/exponential steps, in the sense that the execution of
an ES generates an exponential step, but not a multiplicative one. This
becomes possible due to the CBN/CBV alternative specifications with ES that we
have adopted, and that is why we need three independent counters, in contrast
to the $\lambda$-calculus.

The type system $\mathcal{N}$ for CBN is given in Fig. 1 (_persistent_ rules)
and 2 (_consuming_ rules). A constructor is consuming (resp. persistent) if it
is consumed (resp. not consumed) during $\mathtt{n}$-reduction. For instance,
in ${{{\tt K}}\,{{\tt I}}}\,{\Omega}$ the two abstractions of ${\tt K}$ are
consuming, while the abstraction of ${\tt I}$ is persistent, and all the other
constructors are also consuming, except those of $\Omega$ that turns out to be
an untyped subterm. The persistent rules (Fig. 1) are those typing persistent
constructors, so that none of them increases the first two counters, but only
possibly the third one, which contributes to the size of the normal form. The
consuming rules (Fig. 2), in contrast, type consuming constructors, so that
they may increase the first two counters, contributing to the length of the
normalisation sequence. Notice in particular that there are only two rules
contributing to the multiplicative/exponential counting:  (1) rule
$\mathtt{({app^{\mathcal{N}}_{c}})}$ types a _consuming_ application, meaning
that its left-hand side subterm reduces to an abstraction, then causing a
multiplicative step (rule $\mathtt{dB}$) 333In both [1] and [36], it is the
consuming abstraction which contributes to the multiplicative steps. followed
later by an exponential step; while  (2) rule
$\mathtt{({es^{\mathcal{N}}_{c}})}$ types a _consuming_ substitution causing
an exponential step. In both cases, it is the constructor
application/substitution which is considered to be consumed, without any
further hypothesis on the form of the subterm that appears inside this
consuming constructor (recall that any term can be substituted in CBN). This
phenomenon facilitates in particular the identification of exponential steps
in CBN, in contrast to CBV and CBPV.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 5.88454pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{n}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.68352pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}+1})}{{{t}\,{u}}:{\mathtt{n}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{tt}}}\quad\mathsf{tight}(\Gamma(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=104.49097pt\hbox{\kern
3.00003pt$\mathtt{({abs_{p}})}$}}}\hbox{\kern 0.0pt\kern
10.02293pt\hbox{$\displaystyle{{\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}+1})}{{\lambda{x}.{t}}:{\mathtt{a}}}$}}}}\end{array}$

Figure 1: System $\mathcal{N}$ for the Call-by-Name Calculus: Persistent
Typing Rules.

$\kern-20.00003pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
30.40428pt\hbox{$\displaystyle\penalty 1\vphantom{\Gamma}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.05858pt\hbox{\kern
3.00003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\sigma]}}\vdash^{({0},{0},{0})}{{x}:{\sigma}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
27.94803pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=101.40417pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{\lambda{x}.{t}}:{{\Gamma(x)}\to{\tau}}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{{[\sigma_{i}]_{i\in
I}}\to{\tau}}}\quad({{\Delta_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=148.4926pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
13.76477pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({1+\mathit{m}+_{i\in
I}{\mathit{m}_{i}}},{1+\mathit{e}+_{i\in
I}{\mathit{e}_{i}}},{\mathit{s}+_{i\in
I}{\mathit{s}_{i}}})}{{{t}\,{u}}:{\tau}}$}}}}\\\ \\\ {tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
6.0395pt\hbox{$\displaystyle\penalty 1{\Gamma;{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}\enspace({{\Delta_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=171.84218pt\hbox{\kern
3.00003pt$\mathtt{({es^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}+_{i\in
I}{\mathit{m}_{i}}},{1+\mathit{e}+_{i\in
I}{\mathit{e}_{i}}},{\mathit{s}+_{i\in
I}{\mathit{s}_{i}}})}{{{t}[{x}\backslash{u}]}:{\tau}}$}}}}\end{array}$

Figure 2: System $\mathcal{N}$ for the Call-by-Name Calculus: Consuming Typing
Rules.

This dichotomy between consuming/persistent constructors has been first used
in [36] for the $\lambda$ and $\lambda\mu$-calculi, and adapted here for our
distant versions of CBN/CBV as well as for the $\lambda!$-calculus. We write
${}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
if there is a _(tree) type derivation_ of the judgement
${\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}$ in
system $\mathcal{N}$. The term $t$ is typable in system $\mathcal{N}$, or
$\mathcal{N}$-typable, iff there is a context $\Gamma$, a type $\sigma$ and
counters $(\mathit{m},\mathit{e},\mathit{s})$ such that
${}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$.
We use the capital Greek letters $\Phi,\Psi,\ldots$ to name type derivations,
by writing for example
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$.
As (local) counters of judgements in a given derivation $\Phi$ contribute to
the global counters of the derivation itself, there is an alternative way to
define counters associated to a derivation $\Phi$: the first counter
$\mathit{m}_{\Phi}$ is given by the number of rules
$\mathtt{({app^{\mathcal{N}}_{c}})}$ in $\Phi$, the second counter
$\mathit{e}_{\Phi}$ is the number of rules $\mathtt{({es^{\mathcal{N}}_{c}})}$
in $\Phi$ and finally the third counter $\mathit{s}_{\Phi}$ is the number of
rules $\mathtt{({app^{\mathcal{N}}_{p}})}$ and $\mathtt{({abs_{p}})}$ in
$\Phi$. We prefer however to systematically write counters in judgements to
easy the understanding of the examples and proofs.

A _multitype_ $[\sigma_{i}]_{i\in I}$ is _tight_ , written
$\mathsf{tight}([\sigma_{i}]_{i\in I})$, if $\sigma_{i}\in\mathtt{tt}$ for all
$i\in I$. A _context_ $\Gamma$ is said to be _tight_ if it assigns tight
multitypes to all variables. A _type derivation_
${\Phi}\rhd_{\mathcal{B}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
is _tight_ if $\Gamma$ is tight and $\sigma\in\mathtt{tt}$.

The proofs of soundness and completeness related to our CBN type system are
respectively based on subject reduction and expansion properties, and they are
very similar to those in [1]. The most important point to be mentioned is that
system $\mathcal{N}$ is now counting _separately_ the multiplicative and
exponential steps of $\rightarrow_{\mathtt{n}}$-reductions to normal-form.

Soundness. The soundness property is based on a series of auxiliary results.

######  Lemma 3.1 (Tight Spreading).

Let
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that $\Gamma$ is tight. If $t\in\mathsf{ne}_{\mathtt{n}}$, then
$\sigma\in\mathtt{tt}$.

######  Proof 3.2.

By induction on $\Phi$.

  * •

$\mathtt{({app^{\mathcal{N}}_{p}})}$. Then $\sigma\in\mathtt{tt}$ by
definition.

  * •

$\mathtt{({abs_{p}})}$. This case does not apply since
$t\notin\mathsf{ne}_{\mathtt{n}}$.

  * •

$\mathtt{({var_{c}})}$. This case is immediate since $\Gamma=[\sigma]$ tight
implies $\sigma\in\mathtt{tt}$.

  * •

$\mathtt{({app^{\mathcal{N}}_{c}})}$. Then $t={r}\,{u}$. If
$t\in\mathsf{ne}_{\mathtt{n}}$, then $r\in\mathsf{ne}_{\mathtt{n}}$. We have a
derivation
${\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{[{\mathcal{M}}\to{\sigma}]}}}$,
with $\Gamma^{\prime}\subseteq\Gamma$, so that $\Gamma^{\prime}$ is also
tight. The i.h. gives $[{\mathcal{M}}\to{\sigma}]\in\mathtt{tt}$, and this is
a contradiction. Hence, this case does not apply.

  * •

$\mathtt{({abs_{c}})}$ and $\mathtt{({es^{\mathcal{N}}_{c}})}$. These cases do
not apply since $t\notin\mathsf{ne}_{\mathtt{n}}$.

######  Lemma 3.3.

Let
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
tight. Then, $\mathit{m}=\mathit{e}=0$ iff $t\in\mathsf{no}_{\mathtt{n}}$.

######  Proof 3.4.

$\left.\Rightarrow\right)$ We prove simultaneously the following statements by
induction on $\Phi$.

  1. 1.

${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$
tight and $\mathsf{var}(t)$ or $\mathsf{app}(t)$ implies
$t\in\mathsf{ne}_{\mathtt{n}}$.

  2. 2.

${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$
tight and $\mathsf{abs}(t)$ implies $t\in\mathsf{no}_{\mathtt{n}}$.

  * •

$\mathtt{({var_{c}})}$. Then $t=x$ and $\mathsf{var}(t)$. By definition
$x\in\mathsf{ne}_{\mathtt{v}}$ trivially holds.

  * •

$\mathtt{({app^{\mathcal{N}}_{p}})}$. Then $t={r}\,{u}$, and
${\Gamma}\vdash^{({0},{0},{\mathit{s}-1})}{{r}:{\mathtt{n}}}$ is also tight.
We are in the case $\mathsf{app}(t)$ so we need to show
$t\in\mathsf{ne}_{\mathtt{n}}$. The i.h. (1) gives
$r\in\mathsf{ne}_{\mathtt{n}}$ and we thus conclude
${r}\,{u}\in\mathsf{ne}_{\mathtt{n}}$.

  * •

$\mathtt{({abs_{p}})}$. Then $t=\lambda{x}.{r}$, and the derivation typing $r$
is also tight and has the two first counters equal to $0$. The i.h. gives
$r\in\mathsf{no}_{\mathtt{n}}$, then we conclude
$t\in\mathsf{no}_{\mathtt{n}}$.

  * •

$\mathtt{({app^{\mathcal{N}}_{c}})}$, $\mathtt{({es^{\mathcal{N}}_{c}})}$. The
hypothesis about the counters is not verified so these cases do not apply.

  * •

$\mathtt{({abs_{c}})}$. This case does not apply since the derivation cannot
be tight.

$\left.\Leftarrow\right)$ By induction on $t$.

  * •

$t=x$. Then, $\Phi$ necessarily ends with rule $\mathtt{({var_{c}})}$ and the
statement trivially holds.

  * •

$t={r}\,{u}$. By definition $t\in\mathsf{no}_{\mathtt{n}}$ gives
$r\in\mathsf{ne}_{\mathtt{n}}$. There are two cases to consider:

    1. 1.

if $\Phi$ ends with rule $\mathtt{({app^{\mathcal{N}}_{p}})}$, then
$\sigma=\mathtt{n}$, and
${\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{r}:{\mathtt{n}}}$.
The i.h. gives $\mathit{m}=\mathit{e}=0$ and we are done.

    2. 2.

if $\Phi$ ends with rule $\mathtt{({app^{\mathcal{N}}_{c}})}$, then
${\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{[{\mathcal{M}}\to{\tau}]}}}$
where $\Gamma^{\prime}$ is tight. Moreover, Lem. 3.1 gives
$[{\mathcal{M}}\to{\tau}]\in\mathtt{tt}$ which is a contradiction. Hence, this
case does not apply.

  * •

$t=\lambda{x}.{r}$. Then $r\in\mathsf{no}_{\mathtt{n}}$ and there are two
cases to consider for $\Phi$:

    1. 1.

if $\Phi$ ends with rule $\mathtt{({abs_{p}})}$, then the subderivation of
$\Phi$ is tight, and thus property holds by the i.h.

    2. 2.

if $\Phi$ ends with rule $\mathtt{({abs_{c}})}$, then $\Phi$ cannot be tight
so this case does not apply.

  * •

$t={r}[{x}\backslash{u}]$. By definition $t\notin\mathsf{no}_{\mathtt{n}}$ so
this cases does not apply.

######  Lemma 3.5.

Let
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$.
If $\Phi$ is tight and $t\in\mathsf{no}_{\mathtt{n}}$, then
$\mathit{s}=|{t}|_{\mathtt{n}}$.

######  Proof 3.6.

By induction on $\Phi$.

  * •

$\mathtt{({var_{c}})}$. Then $t=x$ and $\mathit{s}=0=|{t}|_{\mathtt{n}}$ as
expected.

  * •

$\mathtt{({app^{\mathcal{N}}_{p}})}$. Then $t={r}\,{u}$, $\sigma=\mathtt{n}$,
and ${\Gamma}\vdash^{({0},{0},{\mathit{s}-1})}{{r}:{\mathtt{n}}}$. The i.h.
gives $\mathit{s}-1=|{r}|_{\mathtt{n}}$ and hence
$\mathit{s}=|{r}|_{\mathtt{n}}+1=|{t}|_{\mathtt{n}}$.

  * •

$\mathtt{({abs_{p}})}$. Then $t=\lambda{x}.{r}$, and the subderivation typing
$r$ is tight and has counter $\mathit{s}-1$. The i.h. gives
$\mathit{s}-1=|{r}|_{\mathtt{n}}$ and hence
$\mathit{s}=|{r}|_{\mathtt{n}}+1=|{t}|_{\mathtt{n}}$.

  * •

$\mathtt{({app^{\mathcal{N}}_{c}})}$. Then first two counters are not $0$ so
this case does not apply.

  * •

$\mathtt{({abs_{c}})}$. Then $\Phi$ is not tight so this case does not apply.

  * •

$\mathtt{({es^{\mathcal{N}}_{c}})}$. Then the second counter is not $0$ so
this cases does not apply.

######  Lemma 3.7 (Substitution).

Let ${\Phi_{t}}\rhd_{\mathcal{N}}{{\Gamma;x:[\sigma_{i}]_{i\in
I}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}}$ and
$({\Phi_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{u}:{\sigma_{i}}}})_{i\in
I}$. Then,
${\Phi_{{{t}\left\\{{x}\backslash{u}\right\\}}}}\rhd_{\mathcal{N}}{{{\Gamma}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}+_{i\in
I}\mathit{m}_{i}},{\mathit{e}+_{i\in I}\mathit{e}},{\mathit{s}+_{i\in
I}\mathit{s}_{i}})}{{{{t}\left\\{{x}\backslash{u}\right\\}}}:{\tau}}}$.

######  Proof 3.8.

By induction on $\Phi_{t}$.

  * •

$\mathtt{({var_{c}})}$. There are two cases.

    * –

$t=x$. Then ${{t}\left\\{{x}\backslash{u}\right\\}}=u$ and $|I|=1$. More
precisely,
${\Phi_{t}}\rhd_{\mathcal{N}}{{{x}:{[\sigma_{1}]}}\vdash^{({0},{0},{0})}{{x}:{\sigma_{1}}}}$.
We conclude by taking
$\Phi_{{{t}\left\\{{x}\backslash{u}\right\\}}}=\Phi^{1}_{u}$ since the
counters are as expected.

    * –

$t=y\neq x$. Then, ${{t}\left\\{{x}\backslash{u}\right\\}}=y$ and $|I|=0$.
More precisely, we have
${\Phi_{t}}\rhd_{\mathcal{N}}{{{y}:{[\tau]}}\vdash^{({0},{0},{0})}{{y}:{\tau}}}$.
Hence we conclude by taking
$\Phi_{{{t}\left\\{{x}\backslash{u}\right\\}}}=\Phi_{t}$ and the counters are
as expected.

  * •

$\mathtt{({app^{\mathcal{N}}_{p}})}$. Then $t={r}\,{s}$,
${{t}\left\\{{x}\backslash{s}\right\\}}={{{r}\left\\{{x}\backslash{v}\right\\}}}\,{{{s}\left\\{{x}\backslash{v}\right\\}}}$
and $\tau=\mathtt{n}$. We have a premise
${\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma;x:[\sigma_{i}]_{i\in
I}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}-1})}{{r}:{\mathtt{n}}}}$. By
the i.h. we get a type derivation
${\Phi_{{{r}\left\\{{x}\backslash{u}\right\\}}}}\rhd_{\mathcal{N}}{{{\Gamma}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}+_{i\in
I}\mathit{m}_{i}},{\mathit{e}+_{i\in I}\mathit{e}},{\mathit{s}-1+_{i\in
I}\mathit{s}_{i}})}{{{{r}\left\\{{x}\backslash{u}\right\\}}}:{\mathtt{n}}}}$.
We conclude by applying $\mathtt{({app^{\mathcal{N}}_{p}})}$ to this premise,
thus obtaining
${\Phi_{{{t}\left\\{{x}\backslash{u}\right\\}}}}\rhd_{\mathcal{N}}{{{\Gamma}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}+_{i\in
I}\mathit{m}_{i}},{\mathit{e}+_{i\in I}\mathit{e}},{\mathit{s}+_{i\in
I}\mathit{s}_{i}})}{{{{t}\left\\{{x}\backslash{u}\right\\}}}:{\mathtt{n}}}}$
as required.

  * •

All the other cases are straightforward by induction.

######  Lemma 3.9 (Exact Subject Reduction).

Let
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
be a tight derivation. If $t\rightarrow_{\mathtt{dn}}t^{\prime}$, then there
is
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that

  1. 1.

$\mathit{m}^{\prime}=\mathit{m}-1$ and $\mathit{e}^{\prime}=\mathit{e}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{m}$-step.

  2. 2.

$\mathit{e}^{\prime}=\mathit{e}-1$ and $\mathit{m}^{\prime}=\mathit{m}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{e}$-step.

######  Proof 3.10.

We actually prove the following stronger statement that allows us to reason
inductively:

Let $t\rightarrow_{\mathtt{dn}}t^{\prime}$ and
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that $\Gamma$ is tight, and either $\sigma\in\mathtt{tt}$ or
$\neg\mathsf{abs}(t)$. Then, there exists
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that

  1. 1.

$\mathit{m}^{\prime}=\mathit{m}-1$ and $\mathit{e}^{\prime}=\mathit{e}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{m}$-step.

  2. 2.

$\mathit{e}^{\prime}=\mathit{e}-1$ and $\mathit{m}^{\prime}=\mathit{m}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{e}$-step.

We proceed by induction on $t\rightarrow_{\mathtt{dn}}t^{\prime}$.

  * •

$t={{\mathtt{L}}\langle{\lambda{x}.{r}}\rangle}\,{u}\rightarrow_{\mathtt{dn}}{\mathtt{L}}\langle{{r}[{x}\backslash{u}]}\rangle=t^{\prime}$
is an $\mathtt{m}$-step. We proceed by induction on $\mathtt{L}$. We only show
here the case $\mathtt{L}=\Box$ as the inductive case is straightforward.

We first remark that $\Phi$ cannot end with rule $\mathtt{({app_{p}})}$ since
$\lambda{x}.{u}$ cannot be typed with $\mathtt{n}$, then $\Phi$ ends with
$\mathtt{({app^{\mathcal{N}}_{c}})}$ and has the following form:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=103.72913pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
6.91324pt\hbox{$\displaystyle{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{\lambda{x}.{r}}:{{[\sigma_{i}]_{i\in
I}}\to{\sigma}}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\quad({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=262.84348pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
49.37788pt\hbox{$\displaystyle{{\Gamma^{\prime}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({1+\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}},{1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}},{\mathit{s}_{1}+_{i\in
I}{\mathit{s}^{i}_{2}}})}{{{(\lambda{x}.{r})}\,{u}}:{\sigma}}$}}}}$

with $\mathit{m}=1+\mathit{m}_{1}+_{i\in I}{\mathit{m}^{i}_{2}}$,
$\mathit{e}=1+\mathit{e}_{1}+_{i\in I}{\mathit{e}^{i}_{2}}$ and
$\mathit{s}=\mathit{s}_{1}+_{i\in I}{\mathit{s}^{i}_{2}}$. We conclude by
$\mathtt{({es^{\mathcal{N}}_{c}})}$ with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=203.85793pt\hbox{\kern
3.00003pt$\mathtt{({es^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
16.84286pt\hbox{$\displaystyle{\Phi^{\prime}}\rhd_{\mathcal{N}}{{{\Gamma^{\prime}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}},{1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}},{\mathit{s}_{1}+_{i\in
I}{\mathit{s}^{i}_{2}}})}{{{r}[{x}\backslash{u}]}:{\sigma}}}$}}}}$

taking $\mathit{m}^{\prime}=\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}=\mathit{m}-1$ and
$\mathit{e}^{\prime}=1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}=\mathit{e}$.

  * •

$t={r}[{x}\backslash{u}]\rightarrow_{\mathtt{dn}}{{r}\left\\{{x}\backslash{u}\right\\}}=t^{\prime}$
is an $\mathtt{e}$-step. Then, rule $\mathtt{({es^{\mathcal{N}}_{c}})}$ is
necessarily used

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=203.85793pt\hbox{\kern
3.00003pt$\mathtt{({es^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
17.61287pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{N}}{{{\Gamma^{\prime}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}_{1}+_{i\in
I}\mathit{m}^{i}_{2}},{1+\mathit{e}_{1}+_{i\in
I}\mathit{e}^{i}_{2}},{\mathit{s}_{1}+_{i\in
I}\mathit{s}^{i}_{2}})}{{{r}[{x}\backslash{u}]}:{\sigma}}}$}}}}$

with $\mathit{m}=\mathit{m}_{1}+_{i\in I}\mathit{m}^{i}_{2}$,
$\mathit{e}=1+\mathit{e}_{1}+_{i\in I}\mathit{e}^{i}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+_{i\in I}\mathit{s}^{i}_{2}$. We conclude by
applying Lem. 3.7 with $\Phi_{r}$ and $\Phi_{u}$, thus obtaining
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{{\Gamma^{\prime}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}_{1}+_{i\in
I}\mathit{m}^{i}_{2}},{\mathit{e}_{1}+_{i\in
I}\mathit{e}^{i}_{2}},{\mathit{s}_{1}+_{i\in
I}\mathit{s}^{i}_{2}})}{{{{t}\left\\{{x}\backslash{u}\right\\}}}:{\sigma}}}$.
Note that the counters are as expected.

  * •

$t={r}\,{u}\rightarrow_{\mathtt{dn}}{r^{\prime}}\,{u}=t^{\prime}$, where
$r\rightarrow_{\mathtt{dn}}r^{\prime}$ and $\neg\mathsf{abs}(r)$. Then, $\Phi$
ends with rule $\mathtt{({app^{\mathcal{N}}_{p}})}$ or
$\mathtt{({app^{\mathcal{N}}_{c}})}$, and in either case the subterm $r$ has
an associated typing derivation $\Phi_{r}$ which verifies the hypothesis.
Hence, by the i.h. there exists a $\Phi_{r^{\prime}}$ with proper counters.
Thus, we can derive $\Phi^{\prime}$ applying the same rule as in $\Phi$ to
conclude.

  * •

$t=\lambda{x}.{u}\rightarrow_{\mathtt{dn}}\lambda{x}.{u^{\prime}}=t^{\prime}$,
where $r\rightarrow_{\mathtt{dn}}r^{\prime}$. By the hypothesis we have
necessarily $\sigma\in\mathtt{tt}$ since $t$ is an abstraction, then $t$ is
type with rule $\mathtt{({abs_{p}})}$. The statement then immediately follows
from the i.h.

######  Theorem 3.11 (Soundness).

If
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
is tight, then there exists $p$ such that $p\in\mathsf{no}_{\mathtt{n}}$ and
$t\twoheadrightarrow_{\mathtt{n}}^{(\mathit{m},\mathit{e})}p$ with
$\mathit{m}$ $\mathtt{m}$-steps, $\mathit{e}$ $\mathtt{e}$-steps, and
$|{p}|_{\mathtt{n}}=\mathit{s}$.

######  Proof 3.12.

We prove the statement for $\rightarrow_{\mathtt{dn}}$ and then conclude for
the general notion of reduction $\rightarrow_{\mathtt{n}}$ by the observation
that all reduction sequences to normal form have the same number of
multiplicative and exponential steps. Let
${\Phi}\rhd_{\mathcal{B}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$.
We proceed by induction on $\mathit{m}+\mathit{e}$:

  * •

If $\mathit{m}+\mathit{e}=0$, then $\mathit{m}=\mathit{e}=0$ and Lem. 3.3
gives $t\in\mathsf{no}_{\mathtt{n}}$. Moreover, by Lem. 3.5 we get both
$|{t}|_{\mathtt{n}}=\mathit{s}$. Thus, we conclude with $p=t$.

  * •

If $\mathit{m}+\mathit{e}>0$, then $t\notin\mathsf{no}_{\mathtt{n}}$ holds by
Lem. 3.3 and thus there exists $t^{\prime}$ such that
$t\twoheadrightarrow_{\mathtt{dn}}^{(1,0)}t^{\prime}$ or
$t\twoheadrightarrow_{\mathtt{dn}}^{(0,1)}t^{\prime}$ by Prop. 2.1. By Lem.
3.9 there exists a type derivation
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that $1+\mathit{m}^{\prime}+\mathit{e}^{\prime}=\mathit{m}+\mathit{e}$.
By the i.h. there exists $p\in\mathsf{no}_{\mathtt{n}}$ such that
$t^{\prime}\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m}^{\prime},\mathit{e}^{\prime})}p$
with $\mathit{s}=|{p}|_{\mathtt{n}}$. Then
$t\twoheadrightarrow_{\mathtt{dn}}^{(1,0)}t^{\prime}\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m}^{\prime},\mathit{e}^{\prime})}p$
(resp.
$t\twoheadrightarrow_{\mathtt{dn}}^{(0,1)}t^{\prime}\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m}^{\prime},\mathit{e}^{\prime})}p$)
which means $t\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m},\mathit{e})}p$, as
expected.

Completeness. Similarly, the completeness result relays on a series of
intermediate lemmas:

######  Lemma 3.13.

If $t\in\mathsf{no}_{\mathtt{n}}$, then there is a tight derivation
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{n}}})}{{t}:{\sigma}}}$.

######  Proof 3.14.

By simultaneous induction on the following claims:

  1. 1.

If $t\in\mathsf{ne}_{\mathtt{n}}$, then there exists a tight derivation
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{n}}})}{{t}:{\mathtt{n}}}}$.

  2. 2.

If $t\in\mathsf{no}_{\mathtt{n}}$, then there exists a tight derivation
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{n}}})}{{t}:{\mathtt{tt}}}}$.

  * •

$t=x$. Then, $t\in\mathsf{ne}_{\mathtt{v}}\subseteq\mathsf{no}_{\mathtt{v}}$
and we conclude both (1) and (2) by $\mathtt{({var_{c}})}$ since
$|{x}|_{\mathtt{n}}=0$.

  * •

$t={r}\,{u}$. Then, $t\in\mathsf{ne}_{\mathtt{n}}$ or
$t\in\mathsf{no}_{\mathtt{n}}$ implies $r\in\mathsf{ne}_{\mathtt{n}}$. By the
i.h. (1) on $r$ there exists a tight derivation
${\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({0},{0},{|{r}|_{\mathtt{n}}})}{{r}:{\mathtt{n}}}}$.
We conclude (1) by $\mathtt{({app^{\mathcal{N}}_{p}})}$, obtaining
$|{t}|_{\mathtt{n}}=|{r}|_{\mathtt{n}}+1$ as expected. Then (2) also holds.

  * •

$t=\lambda{x}.{r}$. Then, $t\in\mathsf{no}_{\mathtt{n}}$ implies
$r\in\mathsf{no}_{\mathtt{n}}$. By the i.h. (2) on $r$ there exists a tight
derivation
${\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime}}\vdash^{({0},{0},{|{r}|_{\mathtt{n}}})}{{r}:{\mathtt{tt}}}}$.
We conclude (2) by using $\mathtt{({abs_{p}})}$, thus obtaining
$|{t}|_{\mathtt{n}}=|{r}|_{\mathtt{n}}+1$ as expected.

  * •

$t={r}[{x}\backslash{u}]\notin\mathsf{no}_{\mathtt{n}}$. So this case does not
apply.

######  Lemma 3.15 (Anti-Substitution).

Let
${\Phi_{{{t}\left\\{{x}\backslash{u}\right\\}}}}\rhd_{\mathcal{N}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{{{t}\left\\{{x}\backslash{u}\right\\}}}:{\tau}}}$.
Then, there exist
${\Phi_{t}}\rhd_{\mathcal{N}}{{\Gamma;{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}}$ and
$({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{u}:{\sigma_{i}}}})_{i\in
I}$ such that $\Gamma^{\prime}={\Gamma}\mathrel{+_{i\in I}}{\Delta_{i}}$,
$\mathit{m}^{\prime}=\mathit{m}+_{i\in I}{\mathit{m}_{i}}$,
$\mathit{e}^{\prime}=\mathit{e}+_{i\in I}{\mathit{e}_{i}}$ and
$\mathit{s}^{\prime}=\mathit{s}+_{i\in I}{\mathit{s}_{i}}$.

######  Proof 3.16.

By induction on $t$.

  * •

$t=x$. Then, ${{t}\left\\{{x}\backslash{u}\right\\}}=u$ and we take
${\Phi_{x}}\rhd_{\mathcal{N}}{{{x}:{[\sigma_{1}]}}\vdash^{({0},{0},{0})}{{x}:{\sigma_{1}}}}$
and
${\Phi^{1}_{u}}\rhd_{\mathcal{N}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\sigma_{1}}}}$
and the property holds.

  * •

$t=y\neq x$. Then, ${{t}\left\\{{x}\backslash{v}\right\\}}=y$ and we take
${\Phi_{y}}\rhd_{\mathcal{N}}{{{y}:{[\tau]}}\vdash^{({0},{0},{0})}{{y}:{\tau}}}$
so that $|I|=0$ and the property holds.

  * •

In all the other cases the property holds by the i.h.

######  Lemma 3.17 (Exact Subject Expansion).

Let
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
be a tight derivation. If $t\rightarrow_{\mathtt{dn}}t^{\prime}$, then there
is
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that

  1. 1.

$\mathit{m}^{\prime}=\mathit{m}-1$ and $\mathit{e}^{\prime}=\mathit{e}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{m}$-step.

  2. 2.

$\mathit{e}^{\prime}=\mathit{e}-1$ and $\mathit{m}^{\prime}=\mathit{m}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{e}$-step.

######  Proof 3.18.

We actually prove the following stronger statement that allows us to reason
inductively:

Let $t\rightarrow_{\mathtt{dn}}t^{\prime}$ and
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that $\Gamma$ is tight, and either $\sigma\in\mathtt{tt}$ or
$\neg\mathsf{abs}(t)$. Then, there exists
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that

  1. 1.

$\mathit{m}^{\prime}=\mathit{m}-1$ and $\mathit{e}^{\prime}=\mathit{e}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{m}$-step.

  2. 2.

$\mathit{e}^{\prime}=\mathit{e}-1$ and $\mathit{m}^{\prime}=\mathit{m}$ if
$t\rightarrow_{\mathtt{dn}}t^{\prime}$ is an $\mathtt{e}$-step.

We proceed by induction on $t\rightarrow_{\mathtt{dn}}t^{\prime}$.

  * •

$t={{\mathtt{L}}\langle{\lambda{x}.{r}}\rangle}\,{u}\rightarrow_{\mathtt{dn}}{\mathtt{L}}\langle{{r}[{x}\backslash{u}]}\rangle=t^{\prime}$
is an $\mathtt{m}$-step. We proceed by induction on $\mathtt{L}$. We only show
here the case $\mathtt{L}=\Box$ as the inductive case is straightforward.

Then, $t^{\prime}={r}[{x}\backslash{u}]$ and $\Phi^{\prime}$ has the following
form:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=203.85793pt\hbox{\kern
3.00003pt$\mathtt{({es^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
26.65733pt\hbox{$\displaystyle{{\Gamma^{\prime}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}},{1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}},{\mathit{s}_{1}+_{i\in
I}{\mathit{s}^{i}_{2}}})}{{{r}[{x}\backslash{u}]}:{\sigma}}$}}}}$

with $\mathit{m}^{\prime}=\mathit{m}_{1}+_{i\in I}{\mathit{m}^{i}_{2}}$,
$\mathit{e}^{\prime}=1+\mathit{e}_{1}+_{i\in I}{\mathit{e}^{i}_{2}}$ and
$\mathit{s}=\mathit{s}_{1}+_{i\in I}{\mathit{s}^{i}_{2}}$. We conclude with
the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=103.72913pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
6.91324pt\hbox{$\displaystyle{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{\lambda{x}.{r}}:{{[\sigma_{i}]_{i\in
I}}\to{\sigma}}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\quad({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=262.84348pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
36.05556pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{N}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({1+\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}},{1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}},{\mathit{s}_{1}+_{i\in
I}{\mathit{s}^{i}_{2}}})}{{{(\lambda{x}.{r})}\,{u}}:{\sigma}}}$}}}}$

taking $\mathit{m}=1+\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}=\mathit{m}^{\prime}+1$ and
$\mathit{e}=1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}=\mathit{e}^{\prime}$.

  * •

$t={r}[{x}\backslash{u}]\rightarrow_{\mathtt{dn}}{{r}\left\\{{x}\backslash{u}\right\\}}=t^{\prime}$
is an $\mathtt{e}$-step. By Lem. 3.15 there exist type derivations
${\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$
and
$({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$ such that $\Gamma={\Gamma^{\prime}}\mathrel{+_{i\in I}}{\Delta_{i}}$,
$\mathit{m}^{\prime}=\mathit{m}_{1}+_{i\in I}{\mathit{m}^{i}_{2}}$,
$\mathit{e}^{\prime}=\mathit{e}_{1}+_{i\in I}{\mathit{e}^{i}_{2}}$ and
$\mathit{s}=\mathit{s}_{1}+_{i\in I}{\mathit{s}^{i}_{2}}$. We conclude by
$\mathtt{({es^{\mathcal{N}}_{c}})}$ with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{N}}{{\Gamma^{\prime};{x}:{[\sigma_{i}]_{i\in
I}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad({\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Delta_{i}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=203.85793pt\hbox{\kern
3.00003pt$\mathtt{({es^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
17.61287pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{N}}{{{\Gamma^{\prime}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}},{1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}},{\mathit{s}_{1}+_{i\in
I}{\mathit{s}^{i}_{2}}})}{{{r}[{x}\backslash{u}]}:{\sigma}}}$}}}}$

taking $\mathit{m}=\mathit{m}_{1}+_{i\in
I}{\mathit{m}^{i}_{2}}=\mathit{m}^{\prime}$ and
$\mathit{e}=1+\mathit{e}_{1}+_{i\in
I}{\mathit{e}^{i}_{2}}=\mathit{e}^{\prime}+1$.

  * •

$t={r}\,{u}\rightarrow_{\mathtt{dn}}{r^{\prime}}\,{u}=t^{\prime}$, where
$r\rightarrow_{\mathtt{dn}}r^{\prime}$ and $\neg\mathsf{abs}(r)$. Then,
$\Phi^{\prime}$ ends with rule $\mathtt{({app^{\mathcal{N}}_{p}})}$ or
$\mathtt{({app^{\mathcal{N}}_{c}})}$, and in either case the subterm
$r^{\prime}$ has an associated typing derivation $\Phi_{r^{\prime}}$ which
verifies the hypothesis since $\neg\mathsf{abs}(r)$. Hence, by i.h. there
exists a $\Phi_{r}$ with proper counters such that we can derive $\Phi$
applying the same rule as in $\Phi^{\prime}$ to conclude.

  * •

$t=\lambda{x}.{u}\rightarrow_{\mathtt{dn}}\lambda{x}.{u^{\prime}}=t^{\prime}$,
where $r\rightarrow_{\mathtt{dn}}r^{\prime}$. By the hypothesis we have
necessarily $\sigma\in\mathtt{tt}$ since $t^{\prime}$ is an abstraction, then
$t^{\prime}$ is type with rule $\mathtt{({abs_{p}})}$. The statement then
immediately follows from the i.h.

######  Theorem 3.19 (Completeness).

If $t\twoheadrightarrow_{\mathtt{n}}^{(\mathit{m},\mathit{e})}p$ with
$p\in\mathsf{no}_{\mathtt{n}}$, then there exists a tight type derivation
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{|{p}|_{\mathtt{v}}})}{{t}:{\sigma}}}$.

######  Proof 3.20.

As for soundness (Thm. 3.11) we prove the statement for
$\rightarrow_{\mathtt{dn}}$ and then conclude for the general notion of
reduction $\rightarrow_{\mathtt{n}}$. Let
$t\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m},\mathit{e})}p$. We proceed by
induction on $\mathit{m}+\mathit{e}$:

  * •

If $\mathit{m}+\mathit{e}=0$, then $\mathit{m}=\mathit{e}=0$ and thus $t=p$,
which implies $t\in\mathsf{no}_{\mathtt{n}}$. Lem. 3.13 allows to conclude.

  * •

If $\mathit{m}+\mathit{e}>0$, then there is $t^{\prime}$ such that
$t\twoheadrightarrow_{\mathtt{dn}}^{(1,0)}t^{\prime}\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m}-1,\mathit{e})}p$
or
$t\twoheadrightarrow_{\mathtt{dn}}^{(0,1)}t^{\prime}\twoheadrightarrow_{\mathtt{dn}}^{(\mathit{m},\mathit{e}-1)}p$.
By the i.h. there is a tight derivation
${\Phi^{\prime}}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{|{p}|_{\mathtt{v}}})}{{t^{\prime}}:{\sigma}}}$
such $\mathit{m}^{\prime}+\mathit{e}^{\prime}=\mathit{m}+\mathit{e}-1$. Lem.
3.17 gives a tight derivation
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}^{\prime\prime}},{\mathit{e}^{\prime\prime}},{|{p}|_{\mathtt{v}}})}{{t}:{\sigma}}}$
such
$\mathit{m}^{\prime\prime}+\mathit{e}^{\prime\prime}=\mathit{m}^{\prime}+\mathit{e}^{\prime}+1$.
We then have
$\mathit{m}^{\prime\prime}+\mathit{e}^{\prime\prime}=\mathit{m}+\mathit{e}$.
The fact that $\mathit{m}^{\prime\prime}=\mathit{m}$ and
$\mathit{e}^{\prime\prime}=\mathit{e}$ holds by a simple case analysis.

Notice that the previous theorem is stated by using the general notion of
reduction $\rightarrow_{\mathtt{n}}$, but the proofs are done using the
deterministic reduction $\rightarrow_{\mathtt{dn}}$. The equivalence holds
because any two different reduction paths to normal form have the same number
of multiplicative and exponential steps, as already remarked.

######  Example 3.21.

Consider $t_{0}={{{\tt K}}\,{({z}\,{{\tt I}})}}\,{({{\tt I}}\,{{\tt I}})}$
that $\rightarrow_{\mathtt{n}}$-reduces in 2 $\mathtt{m}$-steps and 2
$\mathtt{e}$-steps to the term ${z}\,{{\tt I}}\in\mathsf{no}_{\mathtt{n}}$,
whose $\mathtt{n}$-size is 1:

$t_{0}={\underline{{{\tt K}}\,{({z}\,{{\tt I}})}}}\,{({{\tt I}}\,{{\tt
I}})}\rightarrow_{\mathtt{dB}}\underline{{{(\lambda{y}.{x})}[{x}\backslash{{z}\,{{\tt
I}}}]}\,{({{\tt I}}\,{{\tt
I}})}}\rightarrow_{\mathtt{dB}}\underline{{{x}[{y}\backslash{{{\tt I}}\,{{\tt
I}}}]}[{x}\backslash{{z}\,{{\tt
I}}}]}\rightarrow_{\mathtt{sn}}\underline{{({z}\,{{\tt
I}})}[{y}\backslash{{{\tt I}}\,{{\tt I}}}]}\rightarrow_{\mathtt{sn}}{z}\,{{\tt
I}}$

System $\mathcal{N}$ admits a tight type derivation for $t_{0}$ with the
expected final counter $(2,2,1)$:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.78377pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=57.56754pt\hbox{\kern
2.70003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\mathtt{n}]}}\vdash^{({0},{0},{0})}{{x}:{\mathtt{n}}}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=109.87952pt\hbox{\kern
2.70003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
15.66325pt\hbox{$\displaystyle{{x}:{[\mathtt{n}]}}\vdash^{({0},{0},{0})}{{\lambda{y}.{x}}:{{[\,]}\to{\mathtt{n}}}}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=162.96649pt\hbox{\kern
2.70003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
50.3432pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{{\tt
K}}:{{[\mathtt{n}]}\to{{[\,]}\to{\mathtt{n}}}}}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.22127pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=56.44254pt\hbox{\kern
2.70003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({0},{0},{0})}{{z}:{\mathtt{n}}}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=108.75452pt\hbox{\kern
2.70003pt$\mathtt{({app^{\mathcal{N}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
25.03099pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({0},{0},{1})}{{{z}\,{{\tt
I}}}:{\mathtt{n}}}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=380.88496pt\hbox{\kern
2.70003pt$\mathtt{({app^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
147.84619pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({1},{1},{1})}{{{{\tt
K}}\,{({z}\,{{\tt I}})}}:{{[\,]}\to{\mathtt{n}}}}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=436.96194pt\hbox{\kern
2.70003pt$\mathtt{({app^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
173.13469pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({2},{2},{1})}{{{{{\tt
K}}\,{({z}\,{{\tt I}})}}\,{({{\tt I}}\,{{\tt I}})}}:{\mathtt{n}}}$}}}}$

##  4 Tight Call-by-Value

In this section we introduce a tight system $\mathcal{V}$ for CBV which
captures exact measures for $\rightarrow_{\mathtt{v}}$-reduction sequences.
Here we do not only distinguish length of reduction sequences from size of
normal forms, but also discriminate multiplicative from exponential steps.
Moreover, we establish a precise relation between the counters in CBV and
their counterparts in the $\lambda!$-calculus (cf. Sec. 8). This constitutes
one of the main contributions of the present work.

The grammar of types of system $\mathcal{V}$ is given by:

_(Tight Types)_ | $\mathtt{tt}$ | $::=$ | $\mathtt{n}\mid\mathtt{vl}\mid\mathtt{vr}$
---|---|---|---
_(Types)_ | $\sigma,\tau$ | $::=$ | $\mathtt{tt}\mid\mathcal{M}\mid{\mathcal{M}}\to{\sigma}$
_(Multitypes)_ | $\mathcal{M},\mathcal{N}$ | $::=$ |  $[\sigma_{i}]_{i\in I}$ where $I$ is a finite set

Indeed, apart from the constant $\mathtt{n}$ also used in CBN, we now
introduce constants $\mathtt{vl}$ and $\mathtt{vr}$, typing respectively,
terms reducing to values; and terms reducing to persistent variables that are
not acting as values (i.e. they are applied to some argument to produce
neutral terms). Notice that we remove the base type $\mathtt{a}$ from CBN,
since abstractions are in particular values, so they will be typed with
$\mathtt{vl}$. The notions of _tightness_ for multitypes, contexts and
derivations are exactly the same we used for CBN.

A type system for CBV must type variables without knowing yet the future role
they are going to play (head of neutral term or value). This is one of the
main difficulties behind the definition of such a system. Besides that, the
system must also be able to count multiplicative and exponential steps
independently. The resulting type system $\mathcal{V}$ for CBV is given by the
typing rules in Fig. 3 and 4, distinguishing between persistent and consuming
rules resp. As a matter of notation, given a tight type $\mathtt{tt}_{0}$ we
write $\overline{\mathtt{tt}_{0}}$ to denote a tight type different from
$\mathtt{tt}_{0}$. Thus for instance,
$\overline{\mathtt{vr}}\in\\{\mathtt{vl},\mathtt{n}\\}$.

$\kern-10.00002pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
35.62077pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=71.24155pt\hbox{\kern
3.00003pt$\mathtt{({var_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\mathtt{vr}]}}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vr}}}$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.65207pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=41.30414pt\hbox{\kern
3.00003pt$\mathtt{({val_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vl}}}$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
25.37434pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=50.74869pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{\lambda{x}.{t}}:{\mathtt{vl}}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\overline{\mathtt{vl}}}}\enspace{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\overline{\mathtt{vr}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=98.55455pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.84438pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}+1})}{{{t}\,{u}}:{\mathtt{n}}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}\enspace{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\mathtt{n}}}\enspace\mathsf{tight}(\Gamma(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=154.61362pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
7.88402pt\hbox{$\displaystyle{{({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}[{x}\backslash{u}]}:{\tau}}$}}}}\end{array}$

Figure 3: System $\mathcal{V}$ for the Call-by-Value Calculus: Persistent
Typing Rules.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.30135pt\hbox{$\displaystyle\penalty
1\vphantom{\Gamma}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=62.8527pt\hbox{\kern
3.00003pt$\mathtt{({var^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{\mathcal{M}}}\vdash^{({0},{1},{0})}{{x}:{\mathcal{M}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{[{\mathcal{M}}\to{\tau}]}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\mathcal{M}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=129.59274pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
13.2333pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}+1},{\mathit{e}+\mathit{e}^{\prime}-1},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}\,{u}}:{\tau}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{[{\mathcal{M}}\to{\tau}]}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\mathtt{n}}}\quad\mathsf{tight}(\mathcal{M})$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=173.75952pt\hbox{\kern
3.00003pt$\mathtt{({appt^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
35.3167pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}+1},{\mathit{e}+\mathit{e}^{\prime}-1},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}\,{u}}:{\tau}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 55.41255pt\hbox{$\displaystyle\penalty
1({{\Gamma_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{t}:{\tau_{i}}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=174.28519pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{}\mathrel{+_{i\in
I}}{{\Gamma_{i}}\mathrel{\setminus\\!\\!\setminus}{x}}}\vdash^{({+_{i\in
I}{\mathit{m}_{i}}},{1+_{i\in I}{\mathit{e}_{i}}},{+_{i\in
I}{\mathit{s}_{i}}})}{{\lambda{x}.{t}}:{[{\Gamma_{i}(x)}\to{\tau_{i}}]_{i\in
I}}}$}}}}\\\ \\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 7.8105pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\Gamma(x)}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=140.18817pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}[{x}\backslash{u}]}:{\sigma}}$}}}}\end{array}$

Figure 4: System $\mathcal{V}$ for the Call-by-Value Calculus: Consuming
Typing Rules.

Some rules deserve a comment. A difficult property to be statically captured
by the counters is that an exponential step can only be generated by the
meeting of a substitution constructor with an appropriate value argument. This
remark leads to the introduction of different rules for typing variables,
depending on the role they play (to be a value or not). Indeed, there are
three axioms for variables: $\mathtt{({var_{p}})}$ typing variables that will
persist as the head of a neutral term; $\mathtt{({val_{p}})}$ typing variable
values that may be substituted by other values, i.e. they are _placeholders_
for future persistent values; and $\mathtt{({var^{\mathcal{V}}_{c}})}$ typing
variable values that, in particular, may be consumed as arguments. Consuming
values are always typed with multitypes. Rule
$\mathtt{({app^{\mathcal{V}}_{p}})}$ types neutral applications, i.e. the left
premise has type $\mathtt{vr}$ or $\mathtt{n}$. Rule
$\mathtt{({abs^{\mathcal{V}}_{c}})}$ increases the second counter, just like
$\mathtt{({var^{\mathcal{V}}_{c}})}$, typing a value that is consumed as an
argument. Rules $\mathtt{({app^{\mathcal{V}}_{c}})}$ and
$\mathtt{({appt^{\mathcal{V}}_{c}})}$ increment the first counter because the
(consuming) application will be used to perform a $\mathtt{dB}$-step, while
they decrement the second counter to compensate for the left-hand-side value
that is not being consumed after all. In other words, consuming values are
systematically typed by incrementing their exponential counter by one (rules
$\mathtt{({var^{\mathcal{V}}_{c}})}$ and
$\mathtt{({abs^{\mathcal{V}}_{c}})}$), but they can finally act as
computations instead as values, notably when they are placed in a head
position, so that their exponential counter needs to be adjusted correctly
(cf. Ex. 4.27). The decrement of the exponential counters in rules
$\mathtt{({app^{\mathcal{V}}_{c}})}$ and $\mathtt{({appt^{\mathcal{V}}_{c}})}$
can also be understood by means of the subtle translation from CBV to the
$\lambda!$-calculus that we introduce in Sec. 7. Rule
$\mathtt{({appt^{\mathcal{V}}_{c}})}$ is particularly useful to type
$\mathtt{dB}$-redexes whose reduction does not create an exponential redex,
because the argument of the substitution created by the $\mathtt{dB}$-step
does not reduce to a value.

In spite of the decrements in rules $\mathtt{({app^{\mathcal{V}}_{c}})}$ and
$\mathtt{({appt^{\mathcal{V}}_{c}})}$, the counters are positive.

######  Lemma 4.1.

If
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
then $\mathit{e}\geq 0$. Moreover, if $\sigma$ is a multitype then
$\mathit{e}>0$.

######  Proof 4.2.

By induction on $\Phi$ analysing the last rule applied.

  * •

$\mathtt{({var_{p}})}$, $\mathtt{({val_{p}})}$,
$\mathtt{({abs^{\mathcal{V}}_{p}})}$, $\mathtt{({var^{\mathcal{V}}_{c}})}$.
The result is immediate.

  * •

$\mathtt{({app^{\mathcal{V}}_{p}})}$. Then $t={r}\,{u}$, $\sigma=\mathtt{n}$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and we have type derivations
$\Phi_{r}$ and $\Phi_{u}$ with counters $\mathit{e}_{1}$ and $\mathit{e}_{2}$
resp. both assigning non-multiset types. By i.h. we get $\mathit{e}_{1}\geq 0$
and $\mathit{e}_{2}\geq 0$, and hence we conclude $\mathit{e}\geq 0$.

  * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and we have type derivations
$\Phi_{r}$ and $\Phi_{u}$ with counters $\mathit{e}_{1}$ and $\mathit{e}_{2}$
resp. We conclude directly from the i.h.

  * •

$\mathtt{({app^{\mathcal{V}}_{c}})}$. Then $t={r}\,{u}$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}-1$ and we have type derivations
$\Phi_{r}$ and $\Phi_{u}$ with counters $\mathit{e}_{1}$ and $\mathit{e}_{2}$
resp. both assigning multiset types. By i.h. we get $\mathit{e}_{1}>0$ and
$\mathit{e}_{2}>0$, and hence we conclude $\mathit{e}>0$ as expected.

  * •

$\mathtt{({appt^{\mathcal{V}}_{c}})}$. Then $t={r}\,{u}$,
$\sigma\in\mathtt{tt}$, $\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}-1$ and we
have a derivation $\Phi_{r}$ with counter $\mathit{e}_{1}$ and a multiset
type, and another derivation $\Phi_{u}$ with counter $\mathit{e}_{2}$ and type
$\mathtt{n}$. By i.h. we get $\mathit{e}_{1}>0$ and $\mathit{e}_{2}\geq 0$, so
we can safely conclude $\mathit{e}\geq 0$ as expected.

  * •

$\mathtt{({abs^{\mathcal{V}}_{c}})}$. Then $t=\lambda{x}.{r}$,
$\sigma=[{\mathcal{M}_{i}}\to{\tau_{i}}]_{i\in I}$, $\mathit{e}=1+_{i\in
I}{\mathit{e}_{i}}$ for some set of indices $I$, and we have a type derivation
$\Phi^{i}_{r}$ with counter $\mathit{e}_{i}$ for each $i\in I$. By i.h. we get
$\mathit{e}_{i}\geq 0$ for every $i\in I$, and hence we conclude
$\mathit{e}>0$ as expected.

  * •

$\mathtt{({es_{c}})}$. Then $t={r}[{x}\backslash{u}]$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and we have type derivations
$\Phi_{r}$ and $\Phi_{u}$ with counters $\mathit{e}_{1}$ and $\mathit{e}_{2}$
resp. We conclude directly from the i.h.

Soundness. The soundness property is based on a series of auxiliary results
that enables to reason about tight type derivations:

######  Lemma 4.3 (Tight Spreading).

Let
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that $\Gamma$ is tight.

  1. 1.

If $t\in\mathsf{ne}_{\mathtt{v}}$ or $\mathit{m}=\mathit{e}=0$, then
$\sigma\in\mathtt{tt}$.

  2. 2.

If $\sigma=[{\mathcal{M}}\to{\tau}]$, then $t\notin\mathsf{vr}_{\mathtt{v}}$.

######  Proof 4.4.

We show simultaneously the two properties by induction on $\Phi$.

  1. 1.

We consider every possible rule.

     * •

$\mathtt{({var_{p}})}$, $\mathtt{({val_{p}})}$,
$\mathtt{({abs^{\mathcal{V}}_{p}})}$. Then $\sigma\in\mathtt{tt}$ by
definition.

     * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$. The hypothesis implies
that the type derivation $\Phi_{r}$ typing $r$ with type $\sigma$ has a tight
context, and the two first counters of $\Phi_{r}$ are equal to $0$ or
$r\in\mathsf{ne}_{\mathtt{v}}$. Then the i.h. (1) applied to $\Phi_{r}$ gives
$\sigma\in\mathtt{tt}$.

     * •

$\mathtt{({var^{\mathcal{V}}_{c}})}$. Then $t=x\notin\mathsf{ne}_{\mathtt{v}}$
and $\mathit{e}>0$. Thus, this case does not apply.

     * •

$\mathtt{({app^{\mathcal{V}}_{p}})}$, $\mathtt{({app^{\mathcal{V}}_{c}})}$.
Then $t={r}\,{u}$. The proof concludes with $\mathit{m}>0$ so let us assume
$t\in\mathsf{ne}_{\mathtt{v}}$, which means in particular that
$r\in\mathsf{vr}_{\mathtt{v}}$ or $r\in\mathsf{ne}_{\mathtt{v}}$. Then, we
have a derivation
${\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{[{\mathcal{M}}\to{\sigma}]}}}$,
with $\Gamma^{\prime}\subseteq\Gamma$, so that $\Gamma^{\prime}$ is also
tight. The i.h. (2) gives $r\notin\mathsf{vr}_{\mathtt{v}}$, so that
$r\in\mathsf{ne}_{\mathtt{v}}$. Then we can apply the i.h. (1) to $\Phi_{r}$
which gives $[{\mathcal{M}}\to{\sigma}]\in\mathtt{tt}$, and this is a
contradiction. Hence, this case does not apply.

     * •

$\mathtt{({appt^{\mathcal{V}}_{c}})}$. This case is similar to the previous
one.

     * •

$\mathtt{({abs^{\mathcal{V}}_{c}})}$. Then
$t=\lambda{x}.{u}\notin\mathsf{ne}_{\mathtt{v}}$. Moreover, by Lem. 4.1, we
have $\mathit{e}>0$. Thus, this case does not apply.

     * •

$\mathtt{({es_{c}})}$. Then $t={r}[{x}\backslash{u}]$. The hypothesis implies
that the type derivation $\Phi_{u}$ typing $u$ has a tight context, and the
two first counters of $\Phi_{u}$ are equal to $0$ or
$u\in\mathsf{ne}_{\mathtt{v}}$. Moreover, we know by construction that the
type of $u$ is a multiset. But the i.h. (1) applied to $\Phi_{u}$ gives a
tight type for $u$ which leads to a contradiction.

  2. 2.

Let $\sigma=[{\mathcal{M}}\to{\tau}]$. Suppose $t\in\mathsf{vr}_{\mathtt{v}}$.
We reason by cases.

     * •

$t=x$. Then $\Phi$ is necessarily $\mathtt{({var^{\mathcal{V}}_{c}})}$ because
of the type $\sigma$, thus $\Gamma={x}:{[{\mathcal{M}}\to{\tau}]}$ contradicts
the fact that $\Gamma$ is tight.

     * •

$t={r}[{x}\backslash{u}]$, with $r\in\mathsf{vr}_{\mathtt{v}}$ and
$u\in\mathsf{ne}_{\mathtt{v}}$. Then $\Phi$ necessarily ends with rule
$\mathtt{({es_{c}})}$ or $\mathtt{({es_{p}})}$. In the first case, $\Phi$
contains a subderivation typing $u$ with a context $\Delta\subseteq\Gamma$ and
a multiset type $\mathcal{N}$. Thus $\Delta$ is also tight so that the i.h.
(1) gives $\mathcal{N}\in\mathtt{tt}$ which is a contradiction because
$\mathcal{N}$ is a multiset. In the second case $\Phi$ contains a
subderivation typing $r$ with a tight context and the same type
$[{\mathcal{M}}\to{\tau}]$, so that the i.h. (2) gives
$r\notin\mathsf{vr}_{\mathtt{v}}$, which implies
$t\notin\mathsf{vr}_{\mathtt{v}}$, contradiction.

######  Lemma 4.5.

Let
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
tight. Then, $\mathit{m}=\mathit{e}=0$ iff $t\in\mathsf{no}_{\mathtt{v}}$.

######  Proof 4.6.

$\left.\Rightarrow\right)$ We prove simultaneously the following statements by
induction on $\Phi$.

  1. 1.

${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$
tight and $\mathsf{var}(t)$ implies $t\in\mathsf{vr}_{\mathtt{v}}$.

  2. 2.

${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$
tight and $\mathsf{app}(t)$ implies $t\in\mathsf{ne}_{\mathtt{v}}$.

  3. 3.

${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$
tight and $\mathsf{abs}(t)$ implies $t\in\mathsf{no}_{\mathtt{v}}$.

  * •

$\mathtt{({val_{p}})}$, $\mathtt{({var_{p}})}$. Then $t=x$ and
$\mathsf{var}(t)$. By definition $x\in\mathsf{vr}_{\mathtt{v}}$ trivially
holds.

  * •

$\mathtt{({app^{\mathcal{V}}_{p}})}$. Then $t={r}\,{u}$, $\sigma=\mathtt{n}$,
$\Gamma={\Gamma^{\prime}}\mathrel{+}{\Delta}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}+1$,
${\Gamma^{\prime}}\vdash^{({0},{0},{\mathit{s}^{\prime}})}{{r}:{\overline{\mathtt{vl}}}}$,
and
${\Delta}\vdash^{({0},{0},{\mathit{s}^{\prime\prime}})}{{u}:{\overline{\mathtt{vr}}}}$.
We are in the case $\mathsf{app}(t)$ so we need to show
$t\in\mathsf{ne}_{\mathtt{v}}$. Moreover, $\neg\mathsf{abs}(r)$ holds since
$r$ is typed with $\overline{\mathtt{vl}}$ (i.e. $\mathtt{vr}$ or
$\mathtt{n}$), and $\mathsf{abs}(r)$ implies $\sigma$ is $\mathtt{vl}$ or a
multiset type. By hypothesis $\Gamma^{\prime}$ is tight, hence i.h. (1) or (2)
gives $r\in\mathsf{vr}_{\mathtt{v}}$ or $r\in\mathsf{ne}_{\mathtt{v}}$
respectively. Similarly, $\Delta$ is tight and one of the i.h. gives
$u\in\mathsf{no}_{\mathtt{v}}$, since
$\mathsf{vr}_{\mathtt{v}}\subseteq\mathsf{no}_{\mathtt{v}}$ and
$\mathsf{ne}_{\mathtt{v}}\subseteq\mathsf{no}_{\mathtt{v}}$. We thus conclude
${r}\,{u}\in\mathsf{ne}_{\mathtt{v}}$.

  * •

$\mathtt{({abs^{\mathcal{V}}_{p}})}$. Then
$t=\lambda{x}.{r}\in\mathsf{no}_{\mathtt{v}}$ by definition.

  * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$,
$\Gamma={({\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$,
${\Gamma^{\prime}}\vdash^{({0},{0},{\mathit{s}^{\prime}})}{{r}:{\sigma}}$,
${\Delta}\vdash^{({0},{0},{\mathit{s}^{\prime\prime}})}{{u}:{\mathtt{n}}}$ and
$\mathsf{tight}(\Gamma^{\prime}(x))$. Moreover, note that $\mathsf{abs}(u)$
implies its type is $\mathtt{vl}$ or a multiset, while $\mathsf{var}(u)$
implies its type is $\mathtt{vr}$, $\mathtt{vl}$ or a multiset. Then,
$\neg\mathsf{abs}(u)$ and $\neg\mathsf{var}(u)$ hold since it is typed with
$\mathtt{n}$. Since ${\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}$
is tight and $\mathsf{tight}(\Gamma^{\prime}(x))$, then $\Gamma^{\prime}$ and
$\Delta$ are both tight as well. The i.h. (2) gives
$u\in\mathsf{ne}_{\mathtt{v}}$. On the other hand, some of the i.h. applies
and gives $r\in\mathsf{vr}_{\mathtt{v}}$ or $r\in\mathsf{ne}_{\mathtt{v}}$ or
$r\in\mathsf{no}_{\mathtt{v}}$. We thus conclude
$t\in\mathsf{vr}_{\mathtt{v}}$ or $t\in\mathsf{ne}_{\mathtt{v}}$ or
$t\in\mathsf{no}_{\mathtt{v}}$, respectively.

  * •

$\mathtt{({var^{\mathcal{V}}_{c}})}$. This case does not apply since it
concludes with $\mathit{e}>0$.

  * •

$\mathtt{({app^{\mathcal{V}}_{c}})}$, $\mathtt{({appt^{\mathcal{V}}_{c}})}$.
These cases do not apply since they conclude with $\mathit{m}>0$.

  * •

$\mathtt{({abs^{\mathcal{V}}_{c}})}$. This case does not apply since, by Lem.
4.1, it concludes with $\mathit{e}>0$.

  * •

$\mathtt{({es_{c}})}$. Then $t={r}[{x}\backslash{u}]$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$ and
$\Gamma={({\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}$
tight such that, in particular,
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({0},{0},{\mathit{s}^{\prime\prime}})}{{u}:{\Gamma^{\prime}(x)}}}$
with $\Delta$ tight. By Lem. 4.3 (1) on $\Phi_{u}$,
$\Gamma^{\prime}(x)\in\mathtt{tt}$ which leads to a contradiction since
$\Gamma^{\prime}(x)$ is a multiset by definition. Hence, this case does not
apply.

$\left.\Leftarrow\right)$ By induction on $t$.

  * •

$t=x$. Then, $\Phi$ necessarily ends with rule $\mathtt{({val_{p}})}$, or
$\mathtt{({var_{p}})}$ and the statement trivially holds.

  * •

$t={r}\,{u}$. By definition $t\in\mathsf{no}_{\mathtt{v}}$ gives
$r\in\mathsf{vr}_{\mathtt{v}}$ or $r\in\mathsf{ne}_{\mathtt{v}}$, and
$u\in\mathsf{no}_{\mathtt{v}}$. There are three cases to consider:

    1. 1.

if $\Phi$ ends with rule $\mathtt{({app^{\mathcal{V}}_{p}})}$, then
$\sigma=\mathtt{n}$, $\Gamma={\Gamma^{\prime}}\mathrel{+}{\Delta}$,
$\mathit{m}=\mathit{m}^{\prime}+\mathit{m}^{\prime\prime}$,
$\mathit{e}=\mathit{e}^{\prime}+\mathit{e}^{\prime\prime}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}+1$,
${\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{\overline{\mathtt{vl}}}}$,
${\Delta}\vdash^{({\mathit{m}^{\prime\prime}},{\mathit{e}^{\prime\prime}},{\mathit{s}^{\prime\prime}})}{{u}:{\overline{\mathtt{vr}}}}$.
Moreover, $\Gamma^{\prime}$ and $\Delta$ are both tight. Then, the i.h. gives
$\mathit{m}^{\prime}=\mathit{e}^{\prime}=0$ and
$\mathit{m}^{\prime\prime}=\mathit{e}^{\prime\prime}=0$. Hence,
$\mathit{m}=\mathit{e}=0$.

    2. 2.

if $\Phi$ ends with rule $\mathtt{({app^{\mathcal{V}}_{c}})}$, then
$\Gamma={\Gamma^{\prime}}\mathrel{+}{\Delta}$,
$\mathit{m}=\mathit{m}^{\prime}+\mathit{m}^{\prime\prime}+1$,
$\mathit{e}=\mathit{e}^{\prime}+\mathit{e}^{\prime\prime}-1$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$ and
${\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{[{\mathcal{M}}\to{\tau}]}}}$
where $\Gamma^{\prime}$ is tight. We know by Lem. 4.3 (2) that
$r\notin\mathsf{vr}_{\mathtt{v}}$. Then, it is necessarily the case
$r\in\mathsf{ne}_{\mathtt{v}}$ and Lem. 4.3 (1) gives
$[{\mathcal{M}}\to{\tau}]\in\mathtt{tt}$ which is a contradiction. Hence, this
case does not apply.

    3. 3.

if $\Phi$ ends with rule $\mathtt{({appt^{\mathcal{V}}_{c}})}$, this case is
similar to the previous one.

  * •

$t=\lambda{x}.{r}$. There are two cases to consider for $\Phi$:

    1. 1.

if $\Phi$ ends with rule $\mathtt{({abs^{\mathcal{V}}_{p}})}$, then
$\mathit{m}=\mathit{e}=0$ by definition.

    2. 2.

if $\Phi$ ends with rule $\mathtt{({abs^{\mathcal{V}}_{c}})}$, then $\sigma$
should be a multiset of functional types, which contradicts the hypothesis of
$\Phi$ being tight. Hence, this case does not apply.

  * •

$t={r}[{x}\backslash{u}]$. By definition $t\in\mathsf{no}_{\mathtt{v}}$
implies $r\in\mathsf{no}_{\mathtt{v}}$ and
$u\in\mathsf{ne}_{\mathtt{v}}\subseteq\mathsf{no}_{\mathtt{v}}$. Then, there
are two cases to consider for $\Phi$:

    1. 1.

if $\Phi$ ends with rule $\mathtt{({es_{p}})}$, then
$\Gamma={({\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}$,
$\mathit{m}=\mathit{m}^{\prime}+\mathit{m}^{\prime\prime}$,
$\mathit{e}=\mathit{e}^{\prime}+\mathit{e}^{\prime\prime}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$,
${\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{\sigma}}$,
${\Delta}\vdash^{({\mathit{m}^{\prime\prime}},{\mathit{e}^{\prime\prime}},{\mathit{s}^{\prime\prime}})}{{u}:{\mathtt{n}}}$
and $\mathsf{tight}(\Gamma^{\prime}(x))$. Since $\Gamma$ is tight and
$\mathsf{tight}(\Gamma^{\prime}(x))$, then $\Gamma^{\prime}$ and $\Delta$ are
both tight as well. Then, the i.h. with $r\in\mathsf{no}_{\mathtt{v}}$ and
$u\in\mathsf{no}_{\mathtt{v}}$ gives
$\mathit{m}^{\prime}=\mathit{e}^{\prime}=0$ and
$\mathit{m}^{\prime\prime}=\mathit{e}^{\prime\prime}=0$. Hence,
$\mathit{m}=\mathit{e}=0$.

    2. 2.

if $\Phi$ ends with rule $\mathtt{({es_{c}})}$, then
$\mathit{m}=\mathit{m}^{\prime}+\mathit{m}^{\prime\prime}$,
$\mathit{e}=\mathit{e}^{\prime}+\mathit{e}^{\prime\prime}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$ and
$\Gamma={({\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}$
tight such that, in particular,
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime\prime}})}{{u}:{\Gamma^{\prime}(x)}}}$
with $\Delta$ tight. Moreover, $t\in\mathsf{no}_{\mathtt{v}}$ implies
$u\in\mathsf{ne}_{\mathtt{v}}$. By Lem. 4.3 (1)
$\Gamma^{\prime}(x)\in\mathtt{tt}$ which is a contradiction since
$\Gamma^{\prime}(x)$ is a multiset type by definition. Hence, this case does
not apply.

######  Lemma 4.7.

Let
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{\mathit{s}})}{{t}:{\sigma}}}$.
If $\Phi$ is tight, then $\mathit{s}=|{t}|_{\mathtt{v}}$.

######  Proof 4.8.

By induction on $\Phi$.

  * •

$\mathtt{({var_{p}})}$, $\mathtt{({val_{p}})}$. Then $t=x$ and
$\mathit{s}=0=|{t}|_{\mathtt{v}}$ as expected.

  * •

$\mathtt{({app^{\mathcal{V}}_{p}})}$. Then $t={r}\,{u}$, $\sigma=\mathtt{n}$,
$\Gamma={\Gamma^{\prime}}\mathrel{+}{\Delta}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}+1$,
${\Gamma^{\prime}}\vdash^{({0},{0},{\mathit{s}^{\prime}})}{{r}:{\overline{\mathtt{vl}}}}$,
${\Delta}\vdash^{({0},{0},{\mathit{s}^{\prime\prime}})}{{u}:{\overline{\mathtt{vr}}}}$.
Then, $\Gamma^{\prime}$ and $\Delta$ are both tight, hence the i.h. gives
$\mathit{s}^{\prime}=|{r}|_{\mathtt{v}}$ and
$\mathit{s}^{\prime\prime}=|{u}|_{\mathtt{v}}$. Hence,
$\mathit{s}=|{r}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}+1=|{t}|_{\mathtt{v}}$.

  * •

$\mathtt{({abs^{\mathcal{V}}_{p}})}$. Then $t=\lambda{x}.{r}$, and
$\mathit{s}=0=|{t}|_{\mathtt{v}}$.

  * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$,
$\Gamma={({\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$,
${\Gamma^{\prime}}\vdash^{({0},{0},{\mathit{s}^{\prime}})}{{r}:{\sigma}}$,
${\Delta}\vdash^{({0},{0},{\mathit{s}^{\prime\prime}})}{{u}:{\mathtt{n}}}$ and
$\mathsf{tight}(\Gamma^{\prime}(x))$. Since $\Gamma$ is tight and
$\mathsf{tight}(\Gamma^{\prime}(x))$, then $\Gamma^{\prime}$ and $\Delta$ are
both tight as well. Thus, i.h. gives $\mathit{s}^{\prime}=|{r}|_{\mathtt{v}}$
and $\mathit{s}^{\prime\prime}=|{u}|_{\mathtt{v}}$. Then,
$\mathit{s}=|{r}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}=|{t}|_{\mathtt{v}}$.

  * •

$\mathtt{({var^{\mathcal{V}}_{c}})}$. This case does not apply since it
concludes with $\mathit{e}>0$.

  * •

$\mathtt{({app^{\mathcal{V}}_{c}})}$, $\mathtt{({appt^{\mathcal{V}}_{c}})}$.
These cases do not apply since they conclude with $\mathit{m}>0$.

  * •

$\mathtt{({abs^{\mathcal{V}}_{c}})}$. This case does not apply since, by Lem.
4.1, it concludes with $\mathit{e}>0$.

  * •

$\mathtt{({es_{c}})}$. Then $t={r}[{x}\backslash{u}]$,
$\mathit{s}=\mathit{s}^{\prime}+\mathit{s}^{\prime\prime}$ and
$\Gamma={({\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}$
tight such that, in particular,
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({0},{0},{\mathit{s}^{\prime\prime}})}{{u}:{\Gamma^{\prime}(x)}}}$
with $\Delta$ tight. By Lem. 4.3 (1) on $\Phi_{u}$,
$\Gamma^{\prime}(x)\in\mathtt{tt}$ which leads to a contradiction, since
$\Gamma^{\prime}(x)$ is a multiset type by definition. Hence, this case does
not apply.

A type derivation for a value with a multiset types might be split in multiple
derivations.

######  Lemma 4.9 (Split Type for Exact Value).

Let
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{v}:{\mathcal{M}}}}$
such that $\mathcal{M}={\\!}\mathrel{+_{i\in I}}{\mathcal{M}_{i}}$. Then,
there exist
$({{\Phi_{v}^{i}}\rhd_{\mathcal{V}}{{\Gamma_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{v}:{\mathcal{M}_{i}}}}})_{i\in
I}$ such that $\Gamma={\\!}\mathrel{+_{i\in I}}{\Gamma_{i}}$,
$\mathit{m}=+_{i\in I}{\mathit{m}_{i}}$, $\mathit{e}=1+_{i\in
I}{\mathit{e}_{i}}-|I|$, and $\mathit{s}=+_{i\in I}{\mathit{s}_{i}}$.

######  Proof 4.10.

By case analysis on the form of $v$.

  * •

$v=x$. By $\mathtt{({var^{\mathcal{V}}_{c}})}$
${\Phi}\rhd_{\mathcal{V}}{{{x}:{\mathcal{M}}}\vdash^{({0},{1},{0})}{{x}:{\mathcal{M}}}}$.
From $\mathcal{M}={\\!}\mathrel{+_{i\in I}}{\mathcal{M}_{i}}$ we can build
$({{\Phi^{i}_{v}}\rhd_{\mathcal{V}}{{{x}:{\mathcal{M}_{i}}}\vdash^{({0},{1},{0})}{{x}:{\mathcal{M}_{i}}}}})_{i\in
I}$ by using $\mathtt{({var^{\mathcal{V}}_{c}})}$ several times, and conclude
since $+_{i\in I}{\mathit{e}_{i}}=|I|$ and $\mathit{e}=1$. Note that the
persistent rules $\mathtt{({var_{p}})}$ and $\mathtt{({val_{p}})}$ do not
apply since they do not conclude with a multiset type.

  * •

$v=\lambda{x}.{r}$. By $\mathtt{({abs^{\mathcal{V}}_{c}})}$, we have
$\Gamma={\\!}\mathrel{+_{j\in
J}}{{\Gamma_{j}}\mathrel{\setminus\\!\\!\setminus}{x}}$,
$\mathcal{M}=[{\Gamma_{j}(x)}\to{\tau_{j}}]_{j\in J}$, $\mathit{m}=+_{j\in
J}{\mathit{m}_{j}}$, $\mathit{e}=1+_{j\in J}{\mathit{e}_{j}}$,
$\mathit{s}=+_{j\in J}{\mathit{s}_{i}}$ and
$({{\Phi^{j}_{r}}\rhd_{\mathcal{V}}{{\Gamma_{j}}\vdash^{({\mathit{m}_{j}},{\mathit{e}_{j}},{\mathit{s}_{j}})}{{r}:{\tau_{j}}}}})_{j\in
J}$ for some $J$. Let $\mathcal{M}_{i}=[{\Gamma_{k}(x)}\to{\tau_{k}}]_{k\in
K_{i}}$ for each $i\in I$, where $J=\biguplus_{i\in I}{K_{i}}$. Then, by using
$\mathtt{({abs^{\mathcal{V}}_{c}})}$ we build

$({{\Phi^{i}_{v}}\rhd_{\mathcal{V}}{{{\\!}\mathrel{+_{k\in
K_{i}}}{{\Gamma_{k}}\mathrel{\setminus\\!\\!\setminus}{x}}}\vdash^{({+_{k\in
K_{i}}{\mathit{m}_{k}}},{1+_{k\in K_{i}}{\mathit{e}_{k}}},{+_{k\in
K_{i}}{\mathit{s}_{k}}})}{{\lambda{x}.{r}}:{\mathcal{M}_{i}}}}})_{i\in I}$

Finally, we conclude since:

    * –

$\Gamma={\\!}\mathrel{+_{j\in
J}}{{\Gamma_{j}}\mathrel{\setminus\\!\\!\setminus}{x}}={\\!}\mathrel{+_{i\in
I}}{({\\!}\mathrel{+_{k\in
K_{i}}}{{\Gamma_{k}}\mathrel{\setminus\\!\\!\setminus}{x}})}$

    * –

$\mathit{m}=+_{j\in J}{\mathit{m}_{j}}=+_{i\in I}{(+_{k\in
K_{i}}{\mathit{m}_{k}})}$

    * –

$\mathit{e}=1+_{j\in J}{\mathit{e}_{j}}=1+_{i\in I}{(1+_{k\in
K_{i}}{\mathit{e}_{k}})}-|I|$

    * –

$\mathit{s}=+_{j\in J}{\mathit{s}_{j}}=+_{i\in I}{(+_{k\in
K_{i}}{\mathit{s}_{k}})}$

As before, the persistent rule $\mathtt{({abs^{\mathcal{V}}_{p}})}$ does not
apply since it does not conclude with a multiset type.

These auxiliary lemmas are used in particular to show how to compute the
counters when substituting typed values. This is the key property to obtain
subject reduction.

######  Lemma 4.11 (Substitution).

Let
${\Phi_{t}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}}$
and
${\Phi_{v}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{v}:{\Gamma(x)}}}$.
Then,
${\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}}\rhd_{\mathcal{V}}{{{{\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}-1},{\mathit{s}+\mathit{s}^{\prime}})}{{{{t}\left\\{{x}\backslash{v}\right\\}}}:{\tau}}}$.

######  Proof 4.12.

By induction on $t$.

  * •

$t=x$. Then, ${{t}\left\\{{x}\backslash{v}\right\\}}=v$ and there are three
possibilities for $\Phi_{t}$:

    * –

$\mathtt{({var_{p}})}$. Then $\tau=\mathtt{vr}$ and $\Gamma(x)=[\mathtt{vr}]$.
There is only one way of typing a value with $[\mathtt{vr}]$, namely
$\mathtt{({var^{\mathcal{V}}_{c}})}$, hence $v$ is a variable and
$\Delta={v}:{[\mathtt{vr}]}$. We conclude by taking
${\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({0},{0},{0})}{{v}:{\mathtt{vr}}}}$
by rule $\mathtt{({var_{p}})}$. Note that the counters are as expected.

    * –

$\mathtt{({val_{p}})}$. Then $\tau=\mathtt{vl}$ and $\Gamma=\emptyset$. There
are only two ways of typing a value with type $[\,]$, namely
$\mathtt{({var^{\mathcal{V}}_{c}})}$, if $v$ is a variable, and
$\mathtt{({abs^{\mathcal{V}}_{c}})}$ with $I=\emptyset$, if $v$ is an
abstraction. In both cases the counters of $\Phi_{v}$ are $(0,1,0)$. We
conclude by taking
${\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}}\rhd_{\mathcal{V}}{{}\vdash^{({0},{0},{0})}{{v}:{\mathtt{vl}}}}$
by $\mathtt{({val_{p}})}$, if $v$ is a variable, or
$\mathtt{({abs^{\mathcal{V}}_{p}})}$, if $v$ is an abstraction.

    * –

$\mathtt{({var^{\mathcal{V}}_{c}})}$. Then we have
${\Phi_{t}}\rhd_{\mathcal{V}}{{{x}:{\tau}}\vdash^{({0},{1},{0})}{{x}:{\tau}}}$,
$\tau$ being a multiset type. We conclude by taking
$\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}=\Phi_{v}$ since the counters
are as expected.

  * •

$t=y\neq x$. Then, ${{t}\left\\{{x}\backslash{v}\right\\}}=y$, and there are
three possibilities for $\Phi_{t}$: $\mathtt{({var_{p}})}$,
$\mathtt{({val_{p}})}$ and $\mathtt{({var^{\mathcal{V}}_{c}})}$, with
$\Gamma(x)=[\,]$ in all cases. As observed above the counters of $\Phi_{v}$
are $(0,1,0)$ whenever $\Gamma(x)=[\,]$, hence we conclude by taking
$\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}=\Phi_{t}$.

  * •

All the other cases are straightforward by the i.h. and Lem. 4.9.

######  Lemma 4.13 (Exact Subject Reduction).

Let
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
be a tight derivation. If $t\rightarrow_{\mathtt{dv}}t^{\prime}$, then there
is
${\Phi^{\prime}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that  (1) $\mathit{m}^{\prime}=\mathit{m}-1$and
$\mathit{e}^{\prime}=\mathit{e}$ if $t\rightarrow_{\mathtt{dv}}t^{\prime}$ is
an $\mathtt{m}$-step;  (2) $\mathit{e}^{\prime}=\mathit{e}-1$and
$\mathit{m}^{\prime}=\mathit{m}$ if $t\rightarrow_{\mathtt{dv}}t^{\prime}$ is
an $\mathtt{e}$-step.

######  Proof 4.14.

We actually prove the following stronger statement that allows us to reason
inductively:

Let $t\rightarrow_{\mathtt{dv}}t^{\prime}$ and
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that $\Gamma$ is tight, and either $\sigma\in\mathtt{tt}$ or
$\neg\mathsf{abs}(t)$. Then, there exists
${\Phi^{\prime}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that

  1. 1.

$\mathit{m}^{\prime}=\mathit{m}-1$ and $\mathit{e}^{\prime}=\mathit{e}$ if
$t\rightarrow_{\mathtt{dv}}t^{\prime}$ is an $\mathtt{m}$-step.

  2. 2.

$\mathit{e}^{\prime}=\mathit{e}-1$ and $\mathit{m}^{\prime}=\mathit{m}$ if
$t\rightarrow_{\mathtt{dv}}t^{\prime}$ is an $\mathtt{e}$-step.

We proceed by induction on $t\rightarrow_{\mathtt{dv}}t^{\prime}$.

  * •

$t={{\mathtt{L}}\langle{\lambda{x}.{r}}\rangle}\,{u}\rightarrow_{\mathtt{dv}}{\mathtt{L}}\langle{{r}[{x}\backslash{u}]}\rangle=t^{\prime}$
is an $\mathtt{m}$-step. We proceed by induction on $\mathtt{L}$. We only show
here the case $\mathtt{L}=\Box$ as the inductive case is straightforward.

We first remark that $\Phi$ cannot end with rule
$\mathtt{({app^{\mathcal{V}}_{p}})}$ since $\lambda{x}.{u}$ cannot be typed
neither with $\mathtt{vr}$ nor with $\mathtt{n}$, then there are two cases
depending on the last rule of $\Phi$.

    1. 1.

$\mathtt{({app^{\mathcal{V}}_{c}})}$. Then $\Phi$ has the following form:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.29913pt\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.29387pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}_{1}},{1+\mathit{e}_{1}},{\mathit{s}_{1}})}{{\lambda{x}.{r}}:{[{\Gamma^{\prime}(x)}\to{\sigma}]}}$}}}}\hskip
5.0pt plus 1.0fil\penalty
2{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\Gamma^{\prime}(x)}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=279.03508pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
61.70097pt\hbox{$\displaystyle{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}+1},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{(\lambda{x}.{r})}\,{u}}:{\sigma}}$}}}}$

with $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}+1$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. We conclude by
$\mathtt{({es_{c}})}$ with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\Gamma^{\prime}(x)}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=171.74017pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
5.01129pt\hbox{$\displaystyle{\Phi^{\prime}}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{u}]}:{\sigma}}}$}}}}$

taking $\mathit{m}^{\prime}=\mathit{m}_{1}+\mathit{m}_{2}=\mathit{m}-1$ and
$\mathit{e}^{\prime}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}$.

    2. 2.

$\mathtt{({appt^{\mathcal{V}}_{c}})}$. Then $\Phi$ has the following form:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.29913pt\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.29387pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}_{1}},{1+\mathit{e}_{1}},{\mathit{s}_{1}})}{{\lambda{x}.{r}}:{[{\Gamma^{\prime}(x)}\to{\sigma}]}}$}}}}\hskip
5.0pt plus 1.0fil\penalty
2{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathtt{n}}}}\quad\mathsf{tight}(\Gamma^{\prime}(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=323.20186pt\hbox{\kern
3.00003pt$\mathtt{({appt^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
83.78436pt\hbox{$\displaystyle{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}+1},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{(\lambda{x}.{r})}\,{u}}:{\sigma}}$}}}}$

with $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}+1$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. We conclude by
$\mathtt{({es_{p}})}$ with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathtt{n}}}}\quad\mathsf{tight}(\Gamma^{\prime}(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=215.90695pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
27.09468pt\hbox{$\displaystyle{\Phi^{\prime}}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{u}]}:{\sigma}}}$}}}}$

taking $\mathit{m}^{\prime}=\mathit{m}_{1}+\mathit{m}_{2}=\mathit{m}-1$ and
$\mathit{e}^{\prime}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}$.

  * •

$t={r}[{x}\backslash{{\mathtt{L}}\langle{v}\rangle}]\rightarrow_{\mathtt{dv}}{\mathtt{L}}\langle{{{r}\left\\{{x}\backslash{v}\right\\}}}\rangle=t^{\prime}$
is an $\mathtt{e}$-step. We proceed by induction on $\mathtt{L}$. We only show
here the case $\mathtt{L}=\Box$ as the inductive case is straightforward.

Then, $t={r}[{x}\backslash{v}]$. Note that $\mathtt{({es_{p}})}$ does not
apply since it requires the value $v$ to be typed with $\mathtt{n}$, which is
not possible. Thus, rule $\mathtt{({es_{c}})}$ is necessarily used and we have

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{v}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{v}:{\Gamma^{\prime}(x)}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=170.93121pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
5.6361pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{v}]}:{\sigma}}}$}}}}$

with $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. We conclude by applying Lem. 4.11
with $\Phi_{r}$ and $\Phi_{v}$, thus obtaining
${\Phi^{\prime}}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}-1},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{{t}\left\\{{x}\backslash{v}\right\\}}}:{\sigma}}}$.
Note that the counters are as expected.

  * •

$t={r}\,{u}\rightarrow_{\mathtt{dv}}{r^{\prime}}\,{u}=t^{\prime}$, where
$r\rightarrow_{\mathtt{dv}}r^{\prime}$ and $\neg\mathsf{abs}(r)$. Then, $\Phi$
ends with rule $\mathtt{({app^{\mathcal{V}}_{p}})}$,
$\mathtt{({app^{\mathcal{V}}_{c}})}$ or $\mathtt{({appt^{\mathcal{V}}_{c}})}$,
and in either case the subterm $r$ has an associated typing derivation
$\Phi_{r}$ which verifies the hypothesis since $\neg\mathsf{abs}(r)$. Hence,
by i.h. there exists a $\Phi_{r^{\prime}}$ with proper counters such that we
can derive $\Phi^{\prime}$ applying the same rule as in $\Phi$ to conclude.

  * •

$t={r}\,{u}\rightarrow_{\mathtt{dv}}{r}\,{u^{\prime}}=t^{\prime}$, where
$u\rightarrow_{\mathtt{dv}}u^{\prime}$ and
$r\in\mathsf{ne}_{\mathtt{v}}\cup\mathsf{vr}_{\mathtt{v}}$. There are two
further cases to consider:

    1. 1.

If $\Phi$ ends with rule $\mathtt{({app^{\mathcal{V}}_{p}})}$, then the
subterm $u$ has an associated typing derivation which verifies the hypothesis
(context and type are tight). Then the property holds by i.h.

    2. 2.

If $\Phi$ ends with rule $\mathtt{({app^{\mathcal{V}}_{c}})}$ or
$\mathtt{({appt^{\mathcal{V}}_{c}})}$, then the subterm $r$ has an associated
typing derivation with a tight context and a functional type
$[{\mathcal{M}}\to{\sigma}]$. Lem. 4.3 (2) gives
$r\notin\mathsf{vr}_{\mathtt{v}}$ so that $r\in\mathsf{ne}_{\mathtt{v}}$.
Then, Lem. 4.3 (1) gives $[{\mathcal{M}}\to{\sigma}]\in\mathtt{tt}$ which
leads to a contradiction. So this case is not possible.

  * •

$t={r}[{x}\backslash{u}]\rightarrow_{\mathtt{dv}}{r^{\prime}}[{x}\backslash{u}]=t^{\prime}$,
where $r\rightarrow_{\mathtt{dv}}r^{\prime}$ and
$u\in\mathsf{ne}_{\mathtt{v}}$. There are two further cases to consider:

    1. 1.

If $\Phi$ ends with rule $\mathtt{({es_{p}})}$ then the subterm $r$ has an
associated typing derivation which verifies the hypothesis (context tight and
$\neg\mathsf{abs}(r)$). Then the property holds by i.h.

    2. 2.

If $\Phi$ ends with rule $\mathtt{({es_{c}})}$ then the subterm $u$ has an
associated typing derivation with a tight context and a multiset type
$\mathcal{M}$. Lem. 4.3 (1) gives $\mathcal{M}\in\mathtt{tt}$ which leads to a
contradiction. So this case is not possible.

  * •

$t={r}[{x}\backslash{u}]\rightarrow_{\mathtt{dv}}{r}[{x}\backslash{u^{\prime}}]=t^{\prime}$,
where $u\rightarrow_{\mathtt{dv}}u^{\prime}$ and $\neg\mathsf{val}(u)$. There
are two further cases to consider:

    1. 1.

If $\Phi$ ends with rule $\mathtt{({es_{p}})}$ then the subterm $u$ has an
associated typing derivation which verifies the hypothesis (context and type
are tight). Then the property holds by the i.h.

    2. 2.

If $\Phi$ ends with rule $\mathtt{({es_{c}})}$ then the subterm $u$ has an
associated typing derivation $\Phi_{u}$ which verifies the hypothesis since
$\neg\mathsf{val}(u)$ implies $\neg\mathsf{abs}(u)$. Hence, by i.h. there
exists a $\Phi_{u^{\prime}}$ with proper counters such that we can derive
$\Phi^{\prime}$ applying $\mathtt{({es_{c}})}$ as in $\Phi$ to conclude.

An interesting remark is that types of subterms in tight derivations may
change during CBV reduction, unlike other approaches [1, 39]. To illustrate
this phenomenon, consider the following reduction ${x}[{x}\backslash{{\tt
I}}]\rightarrow_{\mathtt{dv}}{\tt I}$. The terms on the left and right hand
side can be resp. tightly typed by the following derivations (we omit the
counters):

tensy  $\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
11.32988pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=22.65976pt\hbox{\kern
3.00003pt${\mathtt{({val_{p}})}}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{}\vdash{{x}:{\mathtt{vl}}}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 14.22636pt\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
9.8611pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=19.7222pt\hbox{\kern
3.00003pt${\mathtt{({abs^{\mathcal{V}}_{c}})}}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{}\vdash{{{\tt I}}:{[\,]}}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$ ${\mathtt{({es_{c}})}}$
$\displaystyle{{}\vdash{{{x}[{x}\backslash{{\tt I}}]}:{\mathtt{vl}}}}$ tensy
${\mathtt{({abs^{\mathcal{V}}_{p}})}}$ $\displaystyle{{}\vdash{{{\tt
I}}:{\mathtt{vl}}}}$

Notice that the identity function ${\tt I}$ is typed differently in each
derivation: the substitution introduced by rule $\mathtt{({es_{c}})}$ is a
consuming constructor, which disappears when $\mathtt{sv}$-reduction consumes
its value argument, a phenomenon that is captured by means of a multitype for
the argument of the substitution. Indeed, ${\tt I}$ on the left-hand side
derivation is typed with the multitype $[\,]$. This value ${\tt I}$
substitutes a variable $x$ typed with $\mathtt{vl}$, which is just a
placeholder for a persistent value. Thus, once the substitution is performed,