1613 LABEL:LastPageFeb. 23, 2018Jan. 14, 2020

# Non-Idempotent Types for Classical Calculi in Natural Deduction Style

Delia Kesnera  and  Pierre Vialb  aUniversité de Paris and Institut
Universitaire de France (IUF), France<EMAIL_ADDRESS>bInria (LS2N CNRS),
France<EMAIL_ADDRESS>
###### Abstract.

In the first part of this paper, we define two resource aware typing systems
for the $\lambda{\mu}$-calculus based on non-idempotent intersection and union
types. The non-idempotent approach provides very simple combinatorial
arguments –based on decreasing measures of type derivations– to characterize
head and strongly normalizing terms. Moreover, typability provides upper
bounds for the lengths of the head-reduction and the maximal reduction
sequences to normal-form.

In the second part of this paper, the $\lambda{\mu}$-calculus is refined to a
small-step calculus called $\lambda\mu_{\mathtt{s}}$, which is inspired by the
substitution at a distance paradigm. The $\lambda\mu_{\mathtt{s}}$-calculus
turns out to be compatible with a natural extension of the non-idempotent
interpretations of $\lambda{\mu}$, i.e. $\lambda\mu_{\mathtt{s}}$-reduction
preserves and decreases typing derivations in an extended appropriate typing
system. We thus derive a simple arithmetical characterization of strongly
$\lambda\mu_{\mathtt{s}}$-normalizing terms by means of typing.

###### Key words and phrases:

lambda-mu-calculus, classical logic, intersection types, normalization

††terms: λμ††terms: λ††terms: λμ††terms: λ††terms: λ††terms: λ††terms:
λ††terms: λμs

##  1\. Introduction

The Curry-Howard Isomorphism is the well-known relationship between
programming languages and logical systems. While Curry first introduced the
analogy between Hilbert-style deductions and combinatory logic, Howard
highlighted the one between simply typed lambda calculus and natural
deduction. Both examples use intuitionistic logic. The extension of the Curry-
Howard Isomorphism to classical logic took more than two decades, when Griffin
[26] observed that Felleisen’s $\mathcal{C}$ operator can be typed with the
double-negation elimination. A major step in this field was done by Parigot
[42], who proposed the $\lambda{\mu}$-calculus as a simple term notation for
classical natural deduction proofs. The $\lambda{\mu}$-calculus is an
extension of the simply typed $\lambda$-calculus that encodes usual control
operators as the Felleisen’s $\mathcal{C}$ operator mentioned so far. Other
calculi were proposed since then, as for example Curien-Herbelin’s
$\overline{\lambda}\mu\tilde{\mu}$-calculus [14] based on classical sequent
calculus.

The Curry-Howard correspondence has already contributed to the understanding
of many aspects of programming languages by establishing a rich connection
between logic and computation. However, there are still some crucial aspects
of computation, like the use of resources (e.g. time and space), that still
need to be logically understood in the classical setting. Establishing the
foundations of resource consumption is nowadays a big challenge facing the
programming language community. It would lead to a new generation of
programming languages and proof assistants, with a clean type-theoretic
account of resource capabilities.

From qualitative … Several notions of type assignment systems for
$\lambda$-calculus have been defined since its creation, including among
others simple types and polymorphic types. However, even if polymorphic types
are powerful and convenient in programming practice, they have several
drawbacks. For example, it is not possible to assign a type to a term of the
form $(\lambda z.\lambda y.y(z\,\mathtt{I})(z\,\mathtt{K}))(\lambda x.x\,x)$,
where $\mathtt{I}=\lambda w.w$ and $\mathtt{K}=\lambda x.\lambda y.x$, which
can be understood as a meaningful program specified by a terminating term.
Intersection types, pioneered by Coppo and Dezani [12, 13], introduce a new
constructor $\cap$ for types, allowing the assignment of a type of the form
$((\sigma\Rightarrow\sigma)\cap\sigma)\Rightarrow\sigma$ to the term $\lambda
x.xx$. The intuition behind a term $t$ of type $\tau_{1}\cap\tau_{2}$ is that
$t$ has both types $\tau_{1}$ and $\tau_{2}$. The symbol $\cap$ is to be
understood as a mathematical intersection, so in principle, intersection type
theory was developed by using idempotent ($\sigma\cap\sigma=\sigma$),
commutative $(\sigma\cap\tau=\tau\cap\sigma)$, and associative
$((\sigma\cap\tau)\cap\delta=\sigma\cap(\tau\cap\delta))$ laws.

Intersection types have been used as a behavioural tool to reason about
several operational and semantic properties of programming languages. For
example, a $\lambda$-term/program $t$ is strongly normalizing/terminating if
and only if $t$ can be assigned a type in an appropriate intersection type
assignment system. Similarly, intersection types are able to describe and
analyze models of $\lambda$-calculus [6], characterize solvability [37], head
normalization [37], linear-head normalization [29], and weak-normalization
[37, 35] among other properties.

…to quantitative Intersection types: This technology turns out to be a
powerful tool to reason about qualitative properties of programs, but not
about quantitative ones. Indeed, for example, there is a type system
characterizing head normalization (i.e. $t$ is typable in this system if and
only if $t$ is head normalizing) and which gives simultaneously a proof that
$t$ is head-normalizing if and only if the head reduction strategy terminates
on $t$. But the type system gives no information about the number of head-
reduction steps that are necessary to obtain a head normal form. Here is where
non-idempotent types come into play, thus making a clear distinction between
$\sigma\cap\sigma$ and $\sigma$, because intuitively, using the resource
$\sigma$ twice or once is not the same from the quantitative point of view.
This change of perspective can be related to the essential spirit of Linear
Logic [23], which removes the contraction and weakening structural rules in
order to provide an explicit control of the use of logical resources, i.e. to
give a full account of the number of times that a given proposition is used to
derive a conclusion.

The case of the $\lambda$-calculus: Non-idempotent types were pioneered by
Philippa Gardner [22], Assaf Kfoury [32]. But is Daniel de Carvalho [17] who
first established in his PhD thesis a relation between the size of a typing
derivation in a non-idempotent intersection type system for the lambda-
calculus and the head/weak-normalization execution time of head/weak-
normalizing lambda-terms, respectively. Relational models of $\lambda$-calculi
based on non-idempotent types have been investigated by de Carvalho and
Ehrhard in [17, 18, 21]. The results of de Carvalho are distilled in [18].
Non-idempotency is used to reason about the longest reduction sequence of
strongly normalizing terms in both the lambda-calculus [8, 16, 9] and in
different lambda-calculi with explicit substitutions [9, 29]. Non-idempotent
types also appear in linearization of the lambda-calculus [32], type inference
and inhabitation [33, 38, 10], different characterizations of solvability
[41], verification of higher-order programs [40].

The case of the $\lambda{\mu}$-calculus: It is essential to go beyond the
$\lambda$-calculus to focus on the challenges posed by the advanced features
of modern higher-order programming languages and proof assistants. We want in
particular to associate quantitative information to languages being able to
express control operators, as they allow to enrich declarative programming
languages with imperative features.

Related works: The non-idempotent intersection and union types for
$\lambda{\mu}$-calculus that we present in this article can be seen as a
quantitative refinement of Girard’s translation of classical logic into linear
logic. Different qualitative and/or quantitative models for classical calculi
were proposed in [45, 48, 51, 3], thus limiting the characterization of
operational properties to head-normalization. Intersection and union types
were also studied in the framework of classical logic [36, 47, 34, 20], but no
work addresses the problem from a quantitative perspective. Type-theoretical
characterization of strong-normalization for classical calculi were provided
both for $\lambda{\mu}$ [49] and $\bar{\lambda}\mu\tilde{\mu}$-calculus [20],
but the (idempotent) typing systems do not allow to construct decreasing
measures for reduction, thus a resource aware semantics cannot be extracted
from those interpretations. Combinatorial strong normalization proofs for the
$\lambda{\mu}$-calculus were proposed for example in [15], but they do not
provide any explicit decreasing measure, and their use of structural induction
on simple types does not work anymore with intersection types, which are more
powerful than simple types as they do not only ensure termination but also
characterize it. Upper bounds for the $\lambda{\mu}$-calculus are studied in
[7] by passing through standard reduction and the non erasing $\lambda\mu
I$-calculus. Different small step semantics for classical calculi were
developed in the framework of neededness [5, 43], without resorting to any
resource aware semantical argument.

Contributions: Our first contribution is the definition of a resource aware
type system for the $\lambda{\mu}$-calculus based on non-idempotent
intersection and union types. The non-idempotent approach provides very simple
combinatorial arguments, only based on a decreasing measure, to characterize
head and strongly normalizing terms by means of typability. Indeed, we show
that for every typable term $t$ with type derivation $\Pi$, if $t$ reduces to
$t^{\prime}$, then $t^{\prime}$ is typable with a type derivation
$\Pi^{\prime}$ such that the measure of $\Pi$ is strictly greater than that of
$\Pi^{\prime}$. In the well-known case of the $\lambda$-calculus, such a
measure is simply based on the structure of type tree derivations and it is
given by the number of its nodes, which strictly decreases along reduction.
However, in the $\lambda{\mu}$-calculus, the creation of nested applications
during $\mu$-reduction may increase the number of nodes of the corresponding
type derivations, so that such a simple definition of measure is not
decreasing anymore. We then need to also take into account the structure
(multiplicity) of certain types appearing in the type derivations, thus
ensuring an overall decreasing of the measure during reduction. This first
result has been previously presented in [31].

The second contribution of this paper is the definition of a new small-step
operational semantics for $\lambda{\mu}$, called $\lambda\mu_{\mathtt{s}}$,
inspired from the substitution at a distance paradigm [2], which is compatible
with the non-idempotent typing system characterizing strong normalization for
$\lambda{\mu}$, in that the latter extends to $\lambda\mu_{\mathtt{s}}$. The
operational semantics of $\lambda\mu_{\mathtt{s}}$ is linear, i.e. a single
reduction step only implements substitution/replacement on one (free)
occurrence of some variable/name at a time. We then extend the typing system
for $\lambda{\mu}$ characterizing strong normalization, so that the small-step
reduction calculus $\lambda\mu_{\mathtt{s}}$ preserves (and decreases the size
of) typing derivations. We generalize the type-theoretical characterization of
strong normalization to this explicit classical calculus, thus particularly
simplifying existing proofs of strong normalization for small-step operational
semantics of classical calculi [44].

##  2\. The $\lambda{\mu}$-Calculus

This section gives the syntax (Section 2.1) and the operational semantics
(Section 2.2) of the $\lambda{\mu}-$calculus [42]. But before this we first
introduce some preliminary general notions of rewriting that will be used all
along the paper, and that are applicable to any system $\mathcal{R}$. We
denote by $\rightarrow_{\mathcal{R}}$ the (one-step) reduction relation
associated to system $\mathcal{R}$. We write $\rightarrow^{*}_{\mathcal{R}}$
for the reflexive-transitive closure of $\rightarrow_{\mathcal{R}}$, and
$\rightarrow_{\mathcal{R}}^{n}$ for the composition of $n$-steps of
$\rightarrow_{\mathcal{R}}$, thus $t\rightarrow_{\mathcal{R}}^{n}u$ denotes a
finite $\mathcal{R}$-reduction sequence of length $n$ from $t$ to $u$. A term
$t$ is in $\mathcal{R}$-normal form, written $t\in\mathcal{R}$-nf, if there is
no $t^{\prime}$ s.t. $t\rightarrow_{\mathcal{R}}t^{\prime}$; and $t$ has an
$\mathcal{R}$-normal form iff there is $t^{\prime}\in\mathcal{R}$-nf such that
$t\rightarrow^{*}_{\mathcal{R}}t^{\prime}$. A term $t$ is said to be strongly
$\mathcal{R}$-normalizing, written $t\in\mathcal{SN}(\mathcal{R})$, iff there
is no infinite $\mathcal{R}$-sequence starting at $t$. When $\mathcal{R}$ is
finitely branching and strongly $\mathcal{R}$-normalizing,
$\eta_{\mathcal{R}}(t)$ denotes the maximal length of an
$\mathcal{R}$-reduction sequence starting at $t$, we simply write $\eta(t)$ if
$\mathcal{R}$ is clear from the context.

###  2.1. Syntax

We consider a countable infinite set of variables $x,y,z,\ldots$ and
continuation names $\alpha,\beta,\gamma,\ldots$. The set of objects
($\mathcal{O}_{\lambda{\mu}}$), terms () and commands
($\mathcal{C}_{\lambda{\mu}}$) of the $\lambda{\mu}$-calculus are given by the
following grammars

$\begin{array}[]{llll}({\bf objects})&o&::=&t\mid c\\\ ({\bf
terms})&t,u,v&::=&x\mid\lambda x.t\mid tu\mid\mu\alpha.c\\\ ({\bf
commands})&c&::=&[\alpha]t\\\ \end{array}$

We write for the the set of $\lambda$-terms, which is a subset of . We
abbreviate $(\ldots((tu_{1})u_{2})\ldots u_{n})$ as $tu_{1}\ldots u_{n}$ or
$t\overline{u}$ when $n$ is clear from the context. The grammar extends
$\lambda$-terms with two new constructors: commands $[\alpha]t$ and
$\mu$-abstractions $\mu\alpha.c$. Free and bound variables of objects are
defined as expected, in particular $\mathtt{fv}(\mu\alpha.c):=\mathtt{fv}(c)$
and $\mathtt{fv}([\alpha]t):=\mathtt{fv}(t)$. Free names of objects are
defined as expected, in particular
$\mathtt{fn}(\mu\alpha.c):=\mathtt{fn}(c)\setminus\\{\alpha\\}$ and
$\mathtt{fn}([\alpha]t):=\mathtt{fn}(t)\cup\\{\alpha\\}$. Bound names are
defined accordingly.

We work with the standard notion of $\alpha$-conversion i.e. renaming of bound
variables and names, thus for example $[\delta](\mu\alpha.[\alpha](\lambda
x.x))z\equiv[\delta](\mu\beta.[\beta](\lambda y.y))z$. Substitutions are
(finite) functions from variables to terms specified by the notation
$\\{x_{1}/u_{1},\ldots,x_{n}/u_{n}\\}$ $(n\geq 0)$. Application of the
substitution $\sigma$ to the object $o$, written $o\sigma$, may require
$\alpha$-conversion in order to avoid capture of free variables/names, and it
is defined as expected. Replacements are (finite) functions from names to
terms specified by the notation
$\\{\alpha_{1}/\\!\\!/u_{1},\ldots,\alpha_{n}/\\!\\!/u_{n}\\}$ $(n\geq 0)$.
Intuitively, the operation $\\{\alpha/\\!\\!/u\\}$ passes the term $u$ as an
argument to any command of the form $[\alpha]t$, so that it replaces every
occurrence of $[\alpha]t$ in a term by $[\alpha]tu$. Formally, the application
of the replacement $\Sigma$ to the object $o$, written $o\Sigma$, may require
$\alpha$-conversion in order to avoid the capture of free variables/names, and
is defined as follows:

$\begin{array}[]{rl@{\hspace{1cm}}rl}x\\{\alpha/\\!\\!/u\\}:=&x\hfil\hskip
28.45274pt&(\lambda z.t)\\{\alpha/\\!\\!/u\\}:=&\lambda
z.t\\{\alpha/\\!\\!/u\\}\\\
([\alpha]t)\\{\alpha/\\!\\!/u\\}:=&[\alpha](t\\{\alpha/\\!\\!/u\\})u\hfil\hskip
28.45274pt&(tv)\\{\alpha/\\!\\!/u\\}:=&t\\{\alpha/\\!\\!/u\\}v\\{\alpha/\\!\\!/u\\}\\\
([\gamma]t)\\{\alpha/\\!\\!/u\\}:=&[\gamma]t\\{\alpha/\\!\\!/u\\}\quad(\gamma\not=\alpha)\hfil\hskip
28.45274pt&(\mu\gamma.c)\\{\alpha/\\!\\!/u\\}:=&\mu\gamma.c\\{\alpha/\\!\\!/u\\}\\\
\end{array}$

For example, if $\mathtt{I}=\lambda z.z$, then $(x(\mu\alpha[\alpha]y)(\lambda
z.zx))\\{x/\mathtt{I}\\}=\mathtt{I}(\mu\alpha[\alpha]y)(\lambda
z.z\mathtt{I})$, and
$([\alpha]x(\mu\beta.[\alpha]y))\\{\alpha/\\!\\!/\mathtt{I}\\}=[\alpha](x\mu\beta.[\alpha]y\mathtt{I}))\mathtt{I}$.

###  2.2. Operational Semantics

We consider the following set of contexts:

$\begin{array}[]{llll}\textbf{(term
contexts)}&\mathtt{T}&:=&\Box\mid\mathtt{T}\,t\mid t\,\mathtt{T}\mid\lambda
x.\mathtt{T}\mid\mu\alpha.\mathtt{C}\\\ \textbf{(command
contexts)}&\mathtt{C}&:=&[\alpha]\mathtt{T}\\\
\textbf{(contexts)}&\mathtt{O}&:=&\mathtt{T}\mid\mathtt{C}\end{array}$

The hole $\Box$ can be replaced by a term: indeed, $\mathtt{T}[t]$ and
$\mathtt{C}[t]$ denote the replacement of $\Box$ in the context by the term
$t$.

The $\lambda\mu$-calculus is given by the set of objects introduced in Section
2.1 and the reduction relation $\rightarrow_{\lambda{\mu}}$, sometimes simply
written $\rightarrow$, which is the closure by all contexts of the following
rewriting rules:

$\begin{array}[]{lll}(\lambda x.t)u&\mapsto_{\beta}&t\\{x/u\\}\\\
(\mu\alpha.c)u&\mapsto_{\mu}&\mu\alpha.c\\{\alpha/\\!\\!/u\\}\\\ \end{array}$

defined by means of the substitution and replacement application notions given
in Section 2.1. A redex is a term of the form $(\lambda x.t)u$ or
$(\mu\alpha.c)u$.

An alternative specification of the $\mu$-rule [4] is given by
$(\mu\alpha.c)u\mapsto_{\mu}\mu\gamma.c\\{\alpha/\\!\\!/\gamma.u\\}$, where
$\\{\alpha/\\!\\!/\gamma.u\\}$ denotes the fresh replacement meta-operation
assigning $[\gamma](t\\{\alpha/\\!\\!/\gamma.u\\})u$ to $[\alpha]t$ (thus
changing the name of the command), in contrast to the standard replacement
operation $\\{\alpha/\\!\\!/u\\}$ introduced in Section 2.1. We remark however
that the resulting terms $\mu\alpha.c\\{\alpha/\\!\\!/u\\}$ and
$\mu\gamma.c\\{\alpha/\\!\\!/\gamma.u\\}$ are $\alpha$-equivalent; thus e.g.
$\mu\alpha.([\alpha]x)\\{\alpha/\\!\\!/u\\}=\mu\alpha.[\alpha]xu\equiv\mu\gamma.[\gamma]xu=\mu\gamma.([\alpha]x)\\{\alpha/\\!\\!/\gamma.u\\}$.
We will come back to this alternative definition of $\mu$-reduction in Section
7.

A simple example is given by the following $\lambda{\mu}$-reduction sequence:

$\begin{array}[]{lll}(\lambda x.\mu\alpha.[\alpha]x(\lambda
y.\mu\delta.[\alpha]y))\ \mathtt{I}\ \mathtt{I}&\rightarrow_{\beta}\\\
(\mu\alpha.[\alpha](\mathtt{I}(\lambda
y.\mu\delta.[\alpha]y)))\mathtt{I}&\rightarrow_{\beta}\\\
(\mu\alpha.[\alpha](\lambda
y.\mu\delta.[\alpha]y))\mathtt{I}&\rightarrow_{\mu}\\\
\mu\alpha.[\alpha](\lambda
y.\mu\delta.[\alpha]y\mathtt{I})\mathtt{I}&\rightarrow_{\beta}\\\
\mu\alpha.[\alpha](\mu\delta.[\alpha]\mathtt{I}\mathtt{I})&\rightarrow_{\beta}\\\
\mu\alpha.[\alpha](\mu\delta.[\alpha]\mathtt{I})&\\\ \end{array}$

Another typical example, given by Parigot [42], which illustrates the
expressivity of the $\lambda{\mu}$-calculus is the control operator call-cc
[26], coming from Scheme and enabling backtracking, specified in the
$\lambda{\mu}$-calculus by the term $\lambda x.\mu\alpha.[\alpha]x(\lambda
y.\mu\delta.[\alpha]y)$. The term call-cc is assigned $((A\rightarrow
B)\rightarrow A)\rightarrow A$ (Peirce’s Law) in the simply typed
$\lambda{\mu}$-calculus.

A reduction step $o\rightarrow o^{\prime}$ is said to be erasing iff
$o=\mathtt{O}[(\lambda x.u)v]$ and $x\notin\mathtt{fv}(u)$ and
$o^{\prime}=\mathtt{O}[u\\{x/v\\}]=\mathtt{O}[u]$, or
$o=\mathtt{O}[(\mu\alpha.c)u]$ and $\alpha\notin\mathtt{fn}(c)$ and
$o^{\prime}=\mathtt{O}[\mu\alpha.c\\{\alpha/\\!\\!/u\\}]=\mathtt{O}[\mu\alpha.c]$.
Thus e.g. $(\lambda x.z)y\rightarrow_{\beta}z$ and
$(\mu\alpha.[\beta]x)\mathtt{I}\rightarrow_{\mu}\mu\alpha.[\beta]x$ are
erasing steps. A reduction step $o\rightarrow o^{\prime}$ which is not erasing
is called non-erasing. Note that reduction is stable by substitution and
replacement.

A head-context is a context defined by the following grammar:

$\begin{array}[]{llll}\mathtt{HO}&::=&\mathtt{HT}\mid\mathtt{HC}\\\
\mathtt{HT}&::=&\Box\,t_{1}\ldots t_{n}~{}(n\geqslant 0)\mid\lambda
x.\mathtt{HT}\mid\mu\alpha.\mathtt{HC}\\\
\mathtt{HC}&::=&[\alpha]\mathtt{HT}\\\ \end{array}$

A head-normal form is an object of the form $\mathtt{HO}[x]$, where $x$ is any
variable replacing the constant $\Box$. Thus for example
$\mu\alpha.[\beta]\lambda y.x(\lambda z.z)$ is a head-normal form. An object
$o\in\mathcal{O}_{\lambda{\mu}}$ is said to be head-normalizing, written
$o\in\mathcal{HN}(\lambda{\mu})$, if
$o\rightarrow^{*}_{\lambda{\mu}}o^{\prime}$, for some head-normal form
$o^{\prime}$. Remark that $o\in\mathcal{HN}(\lambda{\mu})$ does not imply
$o\in\mathcal{SN}(\lambda{\mu})$ while the converse necessarily holds. We
write $\mathcal{HN}(\lambda)$ and $\mathcal{SN}(\lambda)$ when $t$ is
restricted to be a $\lambda$-term and the reduction system is restricted to
the $\beta$-reduction rule.

A redex $r$ in an object of the form $o=\mathtt{HO}[r]$ is called the head-
redex of $t$. The reduction step $o\rightarrow_{\lambda{\mu}}o^{\prime}$
contracting the head-redex of $o$ is called a head-reduction step. The head
reduction strategy is a deterministic strategy on the set
$\mathcal{O}_{\lambda{\mu}}$ performing always head-steps, so that the head
reduction strategy only stops on head normal forms. If the head-strategy
starting at $o$ terminates, then $o\in\mathcal{HN}(\lambda{\mu})$, while the
converse direction is not straightforward (cf. Theorem 8).

##  3\. Quantitative Type Systems for the $\lambda$-Calculus

As mentioned before, our results rely on typability of $\lambda{\mu}$-terms in
suitable systems with non-idempotent types. Since the $\lambda{\mu}$-calculus
embeds the $\lambda$-calculus, we start by recalling the well-known [22, 17,
10] quantitative type systems for $\lambda$-calculus, called here
$\mathcal{H}_{\lambda}$ and $\mathcal{S}_{\lambda}$. We then reformulate them,
using a different syntactical view, resulting in the typing systems
$\mathcal{H}^{\prime}_{\lambda}$ and $\mathcal{S}^{\prime}_{\lambda}$, that
are subsumed by the formalisms we adopt in Section 4 for $\lambda{\mu}$.

We start by fixing a countable set of base types $a,b,c\ldots$, then we
introduce two different categories of types specified by the following
grammars:

$\begin{array}[]{llll}(\mbox{{\bf Intersection
Types}})&\mathcal{I}&::=&[\sigma_{k}]_{{k\in K}}\\\ (\mbox{{\bf
Types}})&\sigma,\tau&::=&a\mid\mathcal{I}\Rightarrow\sigma\\\ \end{array}$

An intersection type $[\sigma_{k}]_{k\in\\{1..n\\}}$ is a multiset that can be
understood as a type $\sigma_{1}\cap\ldots\cap\sigma_{n}$, where $\cap$ is
associative and commutative, but non-idempotent. Thus, $[\,]$ is the empty
intersection type. The  non-deterministic choice relation $\mathcal{R}^{*}$
between intersection types is defined by $[\sigma_{k}]_{{k\in
K}}\mathcal{R}^{*}[\sigma_{k}]_{{k\in K}}$ when $K\neq\emptyset$ and
$[\sigma_{k}]_{{k\in K}}\mathcal{R}^{*}[\tau]$ (for any type $\tau$) when
$K=\emptyset$. By making a slight abuse of notation, this choice relation is
going to be used as a non-deterministic operation $\\_^{*}$ (rather than a
relation $\mathcal{R}^{*}$) as follows:

$[\sigma_{k}]_{{k\in K}}^{*}:=\left\\{\begin{array}[]{ll}[\tau]&\mbox{ if
}K=\emptyset\mbox{ and $\tau$ is any arbitrary type}\\\ [\sigma_{k}]_{{k\in
K}}&\mbox{ if }K\neq\emptyset\end{array}\right.$

Variable assignments (written $\Gamma$) are total functions from variables to
intersection types. We may write $\emptyset$ to denote the variable assignment
that associates the empty intersection type $[\,]$ to every variable. The
domain of $\Gamma$ is given by
$\mathtt{dom}(\Gamma):=\\{x\mid\Gamma(x)\neq[\,]\\}$, so that when
$x\notin\mathtt{dom}(\Gamma)$, then $\Gamma(x)$ stands for $[\,]$. We write
$x:\mathcal{I}$ (even when $\mathcal{I}=[\,]$) for the assignment mapping $x$
to $\mathcal{I}$ and all $y\neq x$ to $[\,]$. We write
$\Gamma\wedge\Gamma^{\prime}$ for $x\mapsto\Gamma(x)+\Gamma^{\prime}(x)$,
where $+$ is multiset union, so that
$\mathtt{dom}(\Gamma\wedge\Gamma^{\prime})=\mathtt{dom}(\Gamma)\cup\mathtt{dom}(\Gamma^{\prime})$.
When $\mathtt{dom}(\Gamma)\cap\mathtt{dom}(\Gamma^{\prime})$, then
$\Gamma\wedge\Gamma^{\prime}$ may also be written as $\Gamma;\Gamma^{\prime}$.
We write $\Gamma\setminus\\!\\!\\!\setminus\,x$ for the assignment defined by
$(\Gamma\setminus\\!\\!\\!\setminus\,x)(x)=[\,]$ and
$(\Gamma\setminus\\!\\!\\!\setminus\,x)(y)=\Gamma(y)$ if $y\neq x$.

To present/discuss different typing systems, we consider the following
derivability notions. A type judgment is a triple $\Gamma\vdash t:\sigma$,
where $\Gamma$ is a variable assignment, $t$ a term and $\sigma$ a type. A
(type) derivation in system $\mathcal{X}$ is a tree obtained by applying the
(inductive) rules of the type system $\mathcal{X}$, where each node
corresponds to the application of some typing rule. We write
$\Phi\triangleright_{\mathcal{X}}\Gamma\vdash t:\sigma$ if $\Phi$ is a type
derivation concluding with the type judgment $\Gamma\vdash t:\sigma$, and just
$\triangleright_{\mathcal{X}}\ \Gamma\vdash t:\sigma$ if there exists $\Phi$
such that $\Phi\triangleright_{\mathcal{X}}\Gamma\vdash t:\sigma$. A term $t$
is $\mathcal{X}$-typable iff there is a derivation in $\mathcal{X}$ typing
$t$, i.e. if there is $\Phi$ such that
$\Phi\triangleright_{\mathcal{X}}\Gamma\vdash t:\sigma$. We may omit the index
$\mathcal{X}$ if the name of the system is clear from the context.

###  3.1. Characterizing Head $\beta$-Normalizing $\lambda$-Terms

We discuss in this section typing systems being able to characterize head
$\beta$-normalizing $\lambda$-terms. We first consider system
$\mathcal{H}_{\lambda}$ in Figure 2, first appearing in [22], then in [17].

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 23.07814pt\hbox{$\displaystyle\penalty
1\phantom{}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=46.15628pt\hbox{\kern
2.70003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{x:[\tau]}\vdash x:\tau$}}}}\hskip
5.69046pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 31.40317pt\hbox{$\displaystyle\penalty 1{\Gamma}\vdash
t:\tau$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=91.11574pt\hbox{\kern
2.70003pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{\Gamma\setminus\\!\\!\\!\setminus\,x}\vdash\lambda{x}.t:{\Gamma(x)}\Rightarrow{\tau}$}}}}\hskip
5.69046pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1{\Gamma}\vdash t:{[\sigma_{k}]_{{k\in
K}}}\Rightarrow{\tau}\quad({\Gamma_{k}}\vdash u:\sigma_{k})_{{k\in K}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=122.28651pt\hbox{\kern
2.70003pt$(\Rightarrow_{{\mathtt{e}}})$}}}\hbox{\kern 0.0pt\kern
27.06697pt\hbox{$\displaystyle{\Gamma\wedge\wedge_{{k\in K}}\Gamma_{k}}\vdash
t\,u:\tau$}}}}\end{array}$

Figure 1. System $\mathcal{H}_{\lambda}$

$\begin{array}[]{c}\mbox{ Rule }(\texttt{ax})\quad\mbox{ Rule
}(\Rightarrow_{\mathtt{i}})\qquad{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
8.89177pt\hbox{$\displaystyle\penalty 1(\Gamma_{k}\vdash t:\sigma_{k})_{{k\in
K}}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=70.64978pt\hbox{\kern
2.70003pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\wedge_{{k\in K}}\Gamma_{k}\Vdash
t:[\sigma_{k}]_{{k\in K}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:\mathcal{I}\Rightarrow\sigma\quad\Gamma^{\prime}\Vdash u:\mathcal{I}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=82.6809pt\hbox{\kern
2.70003pt$(\Rightarrow_{{\mathtt{e}}})$}}}\hbox{\kern 0.0pt\kern
15.75002pt\hbox{$\displaystyle\Gamma\wedge\Gamma^{\prime}\vdash
t\,u:\sigma$}}}}\end{array}$

Figure 2. System $\mathcal{H}^{\prime}_{\lambda}$

Notice that $K=\emptyset$ in rule $(\Rightarrow_{{\mathtt{e}}})$ allows to
type an application $t\,u$ without necessarily typing the subterm $u$. Thus,
if $\Omega=(\lambda x.xx)(\lambda x.xx)$, then from the judgment
$x:[\sigma]\vdash x:\sigma$ we can derive for example
$x:[\sigma]\vdash(\lambda y.x)\Omega:\sigma$.

System $\mathcal{H}_{\lambda}$ characterizes head $\beta$-normalization:

######  Theorem 1.

Let $t\\!\in$. Then $t$ is $\mathcal{H}_{\lambda}$-typable iff
$t\\!\in\mathcal{HN}(\lambda)$ iff the head-strategy terminates on $t$.

Moreover, the implication typability implies termination of the head-strategy
can be shown by simple arithmetical arguments provided by the quantitative
flavour of the typing system $\mathcal{H}_{\lambda}$, in contrast to classical
reducibility arguments usually invoked in other cases [24, 35]. Actually, the
arithmetical arguments give the following quantitative property:

######  Theorem 2.

If $t$ is $\mathcal{H}_{\lambda}$-typable with tree derivation $\Pi$, then the
size (number of nodes) of $\Pi$ gives an upper bound to the length of the
head-reduction strategy starting at $t$.

To reformulate system $\mathcal{H}_{\lambda}$ in a different way, we now
distinguish two sorts of judgments: regular judgments of the form
$\Gamma\vdash t:\sigma$ assigning types to terms, and auxiliary judgments of
the form $\Gamma\Vdash t:\mathcal{I}$ assigning intersection types to terms.

An equivalent formulation of system $\mathcal{H}_{\lambda}$, called
$\mathcal{H}^{\prime}_{\lambda}$, is given in Figure 2, (where we always use
the name $(\Rightarrow_{{\mathtt{e}}})$ for the rule typing the application
term, even if the rule is different from that in system
$\mathcal{H}_{\lambda}$). There are two inherited forms of type derivations:
regular (resp. auxiliary) derivations are those that conclude with regular
(resp. auxiliary) judgments. Notice that $K=\emptyset$ in rule $(\wedge)$
gives $\emptyset\Vdash u:[\,]$ for any term $u$, e.g.
$\emptyset\Vdash\Omega:[\,]$, so that one can also derive
$x:[\tau]\vdash(\lambda y.x)\Omega:\tau$ in this system. Notice also that
systems $\mathcal{H}_{\lambda}$ and $\mathcal{H}^{\prime}_{\lambda}$ are
relevant, i.e. they lack weakening. Equivalence between
$\mathcal{H}_{\lambda}$ and $\mathcal{H}^{\prime}_{\lambda}$ gives the
following result:

######  Corollary 3.

Let $t\\!\in$. Then $t$ is $\mathcal{H}^{\prime}_{\lambda}$-typable iff
$t\\!\in\mathcal{HN}(\lambda)$ iff the head-strategy terminates on $t$.

Auxiliary judgments turn out to substantially lighten the notations and to
make the statements (and their proofs) more readable.

###  3.2. Characterizing Strongly $\beta$-Normalizing $\lambda$-Terms

We now discuss typing systems being able to characterize strongly
$\beta$-normalizing $\lambda$-terms. We first consider system
$\mathcal{S}_{\lambda}$ in Figure 4, which appears in [11] (slight variants
appear in [16, 9, 29]). Rule $(\Rightarrow_{{\mathtt{e}_{1}}})$ forces the
erasable argument (the subterm $u$) to be typed, even if the type of $u$ (i.e.
$\sigma$) is not being used in the conclusion of the judgment. Thus, in
contrast to system $\mathcal{H}_{\lambda}$, every subterm of a typed term is
now typed.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 23.07814pt\hbox{$\displaystyle\penalty
1\phantom{}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=46.15628pt\hbox{\kern
2.70003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{x:[\tau]}\vdash x:\tau$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
31.40317pt\hbox{$\displaystyle\penalty 1{\Gamma}\vdash t:\tau$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=91.11574pt\hbox{\kern
2.70003pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{\Gamma\setminus\\!\\!\\!\setminus\,x}\vdash\lambda{x}.t:{\Gamma(x)}\Rightarrow{\tau}$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash t:{[\;]}\Rightarrow{\tau}\quad{\Delta}\vdash u:\sigma$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=84.60428pt\hbox{\kern
2.70003pt$(\Rightarrow_{{\mathtt{e}_{1}}})$}}}\hbox{\kern 0.0pt\kern
16.07137pt\hbox{$\displaystyle{\Gamma\wedge\Delta}\vdash
t\,u:\tau$}}}}\\\\[17.07164pt] {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\Gamma}\vdash
t:{[\sigma_{k}]_{{k\in K}}}\Rightarrow{\tau}\quad({\Delta_{k}}\vdash
u:\sigma_{k})_{{k\in K}}\quad K\neq\emptyset$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=157.69904pt\hbox{\kern
2.70003pt$(\Rightarrow_{{\mathtt{e}_{2}}})$}}}\hbox{\kern 0.0pt\kern
43.83574pt\hbox{$\displaystyle{\Gamma\wedge\wedge_{{k\in K}}\Delta_{k}}\vdash
t\,u:\tau$}}}}\end{array}$

Figure 3. System $\mathcal{S}_{\lambda}$

$\begin{array}[]{c}\mbox{ Rule }(\texttt{ax})\quad\mbox{ Rule
}(\Rightarrow_{\mathtt{i}})\quad{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
8.89177pt\hbox{$\displaystyle\penalty 1(\Gamma_{k}\vdash t:\sigma_{k})_{{k\in
K}}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=70.64978pt\hbox{\kern
2.70003pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\wedge_{{k\in K}}\Gamma_{k}\Vdash
t:[\sigma_{k}]_{{k\in K}}$}}}}\hskip 5.69046pt{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash t:{\mathcal{I}}\Rightarrow{\tau}\hskip 5.69046pt\Delta\Vdash
u:\mathcal{I}^{*}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=78.67203pt\hbox{\kern
2.70003pt$(\Rightarrow_{\mathtt{e}*})$}}}\hbox{\kern 0.0pt\kern
13.85524pt\hbox{$\displaystyle{\Gamma\wedge\Delta}\vdash
tu:\tau$}}}}\end{array}$

Figure 4. System $\mathcal{S}^{\prime}_{\lambda}$

System $\mathcal{S}_{\lambda}$ characterizes strong $\beta$-normalization:

######  Lemma 4.

Let $t\in$. Then $t$ is $\mathcal{S}_{\lambda}$-typable iff
$t\in\mathcal{SN}(\lambda)$.

As before, the implication typability implies normalization can be show by
simple arithmetical arguments provided by the quantitative flavour of the
typing system $\mathcal{S}_{\lambda}$. Actually, the proof of Lemma 4 gives
the following bound:

######  Theorem 5.

If $t$ is $\mathcal{S}_{\lambda}$-typable with tree derivation $\Pi$, then the
size (number of nodes) of $\Pi$ gives an upper bound to the length of any
reduction path starting at $t$.

An equivalent formulation of system $\mathcal{S}_{\lambda}$, called
$\mathcal{S}^{\prime}_{\lambda}$, is given in Figure 4. As before, we use
regular as well as auxiliary judgments. Notice that $K=\emptyset$ in rule
$(\wedge)$ is still possible, but derivations of the form $\Vdash t:[\,]$,
representing untyped terms, will never be used. The choice operation $\\_^{*}$
(defined at the beginning of Section 3) in rule $(\Rightarrow_{\mathtt{e}*})$
is used to impose arbitrary types for erasable terms, i.e. when $t$ has type
$[\,]\Rightarrow\tau$, then $u$ needs to be typed with an arbitrary type
$[\sigma]$, thus the auxiliary judgment typing $u$ on the right premise of
$(\Rightarrow_{\mathtt{e}*})$ can never assign $[\,]$ to $u$. This should be
understood as a form of restricted weakening on the argument $u$, , which is
only performed before the application of rule $(\Rightarrow_{\mathtt{e}*})$
and only when the functional type is of the form $[\,]\rightarrow\mathcal{U}$.

######  Example 3.1.

Here is an example of type derivation in system
$\mathcal{S}^{\prime}_{\lambda}$.

${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\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.37366pt\hbox{$\displaystyle\penalty
1\phantom{}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=56.74731pt\hbox{\kern
3.00003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\sigma]\vdash x:\sigma$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=109.02176pt\hbox{\kern
3.00003pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
6.97873pt\hbox{$\displaystyle x:[\sigma]\vdash\lambda
y.x:[\,]\Rightarrow\sigma$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\quad\hskip
5.0pt plus 1.0fil{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 26.4061pt\hbox{$\displaystyle\penalty
1\phantom{}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=52.8122pt\hbox{\kern
3.00003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
z:[\tau]\vdash z:\tau$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=105.08664pt\hbox{\kern
3.00003pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern 22.80388pt\hbox{$\displaystyle
z:[\tau]\Vdash z:[\tau]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=326.32393pt\hbox{\kern
3.00003pt$(\Rightarrow_{\mathtt{e}*})$}}}\hbox{\kern 0.0pt\kern
106.68706pt\hbox{$\displaystyle x:[\sigma],z:[\tau]\vdash(\lambda
y.x)z:\sigma$}}}}$

Since $\mathcal{S}_{\lambda}$ and $\mathcal{S}^{\prime}_{\lambda}$ are
equivalent, we also have:

######  Corollary 6.

Let $t\\!\in$. Then $t$ is $\mathcal{S}^{\prime}_{\lambda}$-typable iff
$t\\!\in\mathcal{SN}(\lambda)$.

##  4\. Quantitative Type Systems for the $\lambda{\mu}$-Calculus

We present in this section two quantitative systems for the
$\lambda{\mu}$-calculus, systems $\mathcal{H}_{\lambda{\mu}}$ (Section 4.2)
and $\mathcal{S}_{\lambda{\mu}}$ (Section 4.4), characterizing, respectively,
head and strong $\lambda{\mu}$-normalizing objects. Since $\lambda$-calculus
is embedded in the $\lambda{\mu}$-calculus, then the starting points to design
$\mathcal{H}_{\lambda{\mu}}$ and $\mathcal{S}_{\lambda{\mu}}$ are,
respectively, systems $\mathcal{H}^{\prime}_{\lambda}$ and
$\mathcal{S}^{\prime}_{\lambda}$, introduced in Section 3.

###  4.1. Types

We consider a countable set of base types $a,b,c\ldots$ and the following
categories of types:

$\begin{array}[]{llll}(\mbox{{\bf Object
Types}})&\mathcal{A}&:=&\mathcal{C}\mid\mathcal{U}\\\ (\mbox{{\bf Command
Type}})&\mathcal{C}&:=&\\#\\\ (\mbox{{\bf Union
Types}})&\mathcal{U},\mathcal{V}&::=&\langle\sigma_{k}\rangle_{{k\in K}}\\\
(\mbox{{\bf Intersection
Types}})&\mathcal{I},\mathcal{J}&::=&[\mathcal{U}_{k}]_{{k\in K}}\\\
(\mbox{{\bf Types}})&\sigma,\tau&::=&a\mid\mathcal{I}\Rightarrow\mathcal{U}\\\
(\mbox{{\bf Blind Types}})&\xi&::=&a\mid[\,]\Rightarrow\langle\xi\rangle\\\
\end{array}$

The constant $\\#$ is used to type commands, union types to type terms, and
intersection types to type variables (thus left-hand sides of arrows). We
assume $K$ to be any finite set. Both $[\sigma_{k}]_{k\in\\{1..n\\}}$ and
$\langle\sigma_{k}\rangle_{k\in\\{1..n\\}}$ can be seen as multisets,
representing, respectively, $\sigma_{1}\cap\ldots\cap\sigma_{n}$ and
$\sigma_{1}\cup\ldots\cup\sigma_{n}$, where $\cap$ and $\cup$ are both
associative, commutative, but non-idempotent. We may omit the indices in the
simplest case: thus $[\mathcal{U}]$ and $\langle\sigma\rangle$ denote
singleton multisets. We define the operator $\wedge$ (resp. $\vee$) on
intersection (resp. union) multiset types by : $[\mathcal{U}_{k}]_{{k\in
K}}\wedge[{\mathcal{V}}_{\ell}]_{{\ell\in L}}:=[\mathcal{U}_{k}]_{{k\in
K}}+[{\mathcal{V}}_{\ell}]_{{\ell\in L}}$ and $\langle\sigma_{k}\rangle_{{k\in
K}}\vee\langle\tau_{\ell}\rangle_{{\ell\in
L}}:=\langle\sigma_{k}\rangle_{{k\in K}}+\langle\tau_{\ell}\rangle_{{\ell\in
L}}$, where $+$ always means multiset union. The non-deterministic choice
operation (resulting from a non-deterministic choice relation, as in Section
3) is now not only defined on intersection but also on union types:

$\begin{array}[]{lll}[\mathcal{U}_{k}]_{{k\in
K}}^{*}&:=&\left\\{\begin{array}[]{ll}[\mathcal{U}]&\mbox{ if
}K=\emptyset\mbox{ and $\mathcal{U}\neq\langle\,\rangle$ is any arbitrary non-
empty union type}\\\ [\mathcal{U}_{k}]_{{k\in K}}&\mbox{ if
}K\neq\emptyset\end{array}\right.\\\ \langle\sigma_{k}\rangle_{{k\in
K}}^{*}&:=&\left\\{\begin{array}[]{ll}\langle\xi\rangle&\mbox{ if
}K=\emptyset\mbox{ and $\xi$ is any arbitrary blind type}\\\
\langle\sigma_{k}\rangle_{{k\in K}}&\mbox{ if
}K\neq\emptyset\end{array}\right.\end{array}$

The choice operation for union type is defined so that (1) the empty union
cannot be assigned to $\mu$-abstractions (2) subject reduction is guaranteed
in system $\mathcal{H}_{\lambda{\mu}}$ for erasing steps
$(\mu\alpha.c)u\rightarrow_{\mu}\mu\alpha.c$, where
$\alpha\notin\mathtt{fn}(c)$. We present concrete examples in Section 4.3
which illustrates the need of non-empty union types and blind types to
guarantee subject reduction.

The arity of types and union multiset types is defined by induction: for types
$\sigma$, if $\sigma=\mathcal{I}\Rightarrow\mathcal{U}$, then
$\mathtt{ar}(\sigma):=\mathtt{ar}(\mathcal{U})+1$, otherwise,
$\mathtt{ar}(\sigma):=0$; for union multiset types,
$\mathtt{ar}(\langle\sigma_{k}\rangle_{{k\in K}}):=\Sigma_{{k\in K}}\
\mathtt{ar}(\sigma_{k})$. Thus, the arity of a type counts the number of its
top-level arrows. The cardinality of multisets is defined by
$|[\mathcal{U}_{k}]_{{k\in K}}|=|\langle\sigma_{k}\rangle_{{k\in K}}|:=|K|$.

Variable assignments (written $\Gamma$), are, as before, total functions from
variables to intersection multiset types. Similarly, name assignments (written
$\Delta$), are total functions from names to union multiset types. The domain
of $\Delta$ is given by
$\mathtt{dom}(\Delta):=\\{\alpha\mid\Delta(\alpha)\neq\langle\,\rangle\\}$,
where $\langle\,\rangle$ is the empty union multiset, so that when
$\alpha\notin\mathtt{dom}(\Delta)$, $\Delta(\alpha)$ stands for
$\langle\,\rangle$. We may write $\emptyset$ to denote the name assignment
that associates the empty union type $\langle\,\rangle$ to every name. We
write $\Delta\vee\Delta^{\prime}$ for
$\alpha\mapsto\Delta(\alpha)\vee\Delta^{\prime}(\alpha)$, so that
$\mathtt{dom}(\Delta\vee\Delta^{\prime})=\mathtt{dom}(\Delta)\cup\mathtt{dom}(\Delta^{\prime})$.

When $\mathtt{dom}(\Delta)\cap\mathtt{dom}(\Delta^{\prime})=\emptyset$, we may
write $\Delta;\Delta^{\prime}$ for $\Delta\vee\Delta^{\prime}$. We write
$\alpha:\mathcal{U}$ (even when $\alpha=\langle\,\rangle$) for the name
assignment mapping $\alpha$ to $\mathcal{U}$ and all $\beta\neq\alpha$ to
$\langle\,\rangle$. We write $\Delta\setminus\\!\\!\\!\setminus\,\alpha$ for
the name assignment defined by
$(\Delta\setminus\\!\\!\\!\setminus\,\alpha)(\alpha)=\langle\,\rangle$ and
$(\Delta\setminus\\!\\!\\!\setminus\,\beta)(\alpha)=\Delta(\beta)$ if
$\beta\neq\alpha$.

We now present our typing systems $\mathcal{H}_{\lambda{\mu}}$ and
$\mathcal{S}_{\lambda{\mu}}$, both having regular (resp. auxiliary) judgments
of the form $\Gamma\vdash t:\mathcal{U}\mid\Delta$ (resp. $\Gamma\Vdash
t:\mathcal{I}\mid\Delta$), together with their respective notions of regular
and auxiliary derivations. An important syntactical property they enjoy is
that both are syntax directed, i.e. for each (regular/auxiliary) typing
judgment $j$ there is a unique typing rule whose conclusion matches the
judgment $j$. This makes our proofs much simpler than those arising with
idempotent types, which are based on long generation lemmas (e.g. [9, 47]).

###  4.2. System $\mathcal{H}_{\lambda{\mu}}$

In this section we present a quantitative typing system for $\lambda{\mu}$,
called $\mathcal{H}_{\lambda{\mu}}$, characterizing head
$\lambda{\mu}$-normalization. It can be seen as a first intuitive step to
understand the typing system $\mathcal{S}_{\lambda{\mu}}$, introduced later in
Section 4.4, and characterizing strong $\lambda{\mu}$-normalization. However,
to avoid redundancy, the properties of the two systems are not described in
the same way:

  * •

For $\mathcal{H}_{\lambda{\mu}}$, we provide informal discussions to explain
the main requirements needed to capture quantitative information in the
presence of classical feature (names, $\mu$-redexes). We particularly focus on
the necessity of banning empty union types. We do not give the proofs of the
properties of $\mathcal{H}_{\lambda{\mu}}$, because they are simpler than
those of system $\mathcal{S}_{\lambda{\mu}}$.

  * •

For $\mathcal{S}_{\lambda{\mu}}$, we provide a more compact presentation,
since the main technical key choices used for $\mathcal{H}_{\lambda{\mu}}$ are
still valid. However, full statements and proofs of the properties of
$\mathcal{S}_{\lambda{\mu}}$ are detailed.

The (syntax directed) rules of the typing system $\mathcal{H}_{\lambda{\mu}}$
are presented in Figure 5.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 16.23889pt\hbox{$\displaystyle\penalty
1\mathcal{U}\neq\langle\,\rangle$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=53.58893pt\hbox{\kern
2.40002pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\mathcal{U}]\vdash x:\mathcal{U}\mid\emptyset$}}}}\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 34.02504pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:\mathcal{U}\mid\Delta$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=105.93903pt\hbox{\kern
2.40002pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\setminus\\!\\!\\!\setminus\,x\vdash\lambda
x.t:\langle\Gamma(x)\Rightarrow\mathcal{U}\rangle\mid\Delta$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
22.28432pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:\mathcal{U}\mid\Delta$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=82.45758pt\hbox{\kern
2.40002pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash[\alpha]t:\\#\mid\Delta\vee\\{\alpha:\mathcal{U}\\}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 23.70663pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
c:\\#\mid\Delta$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=88.20871pt\hbox{\kern
2.40002pt$(\\#_{\mathtt{e}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mu\alpha.c:\Delta(\alpha)^{*}\mid\Delta\setminus\\!\\!\\!\setminus\,\alpha$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.58534pt\hbox{$\displaystyle\penalty 1(\Gamma_{k}\vdash
t:\mathcal{U}_{k}\mid\Delta_{k})_{{k\in K}}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=90.06496pt\hbox{\kern
2.40002pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\wedge_{{k\in K}}\Gamma_{k}\Vdash
t:[\mathcal{U}_{k}]_{{k\in K}}\mid\vee_{{k\in K}}\Delta_{k}$}}}}\\\ \\\
{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma_{t}\vdash
t:\langle\mathcal{I}_{k}\Rightarrow\mathcal{U}_{k}\rangle_{{k\in
K}}\mid\Delta_{t}\quad\Gamma_{u}\Vdash u:\wedge_{{k\in
K}}\mathcal{I}_{k}\mid\Delta_{u}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=137.75743pt\hbox{\kern
2.40002pt$(\Rightarrow_{{\mathtt{e}}})$}}}\hbox{\kern 0.0pt\kern
22.93268pt\hbox{$\displaystyle\Gamma_{t}\wedge\Gamma_{u}\vdash tu:\vee_{{k\in
K}}\mathcal{U}_{k}\mid\Delta_{t}\vee\Delta_{u}$}}}}\\\ \\\ \end{array}$ Figure
5. System $\mathcal{H}_{\lambda{\mu}}$

Rule $(\Rightarrow_{{\mathtt{e}}})$ is to be understood as a logical
admissible rule: if union (resp. intersection) is interpreted as the
$\mathtt{OR}$ (resp. $\mathtt{AND}$) logical connective, then
$\mathtt{OR}_{{k\in K}}\ (\mathcal{I}_{k}\Rightarrow\mathcal{U}_{k})$ and
$(\mathtt{AND}_{{k\in K}}\ \mathcal{I}_{k})$ implies $(\mathtt{OR}_{{k\in K}}\
\mathcal{U}_{k})$. As in the simply typed $\lambda{\mu}$-calculus [42], the
$(\\#_{\mathtt{i}})$ rule saves a type $\mathcal{U}$ for the name $\alpha$,
however, in our system, the corresponding name assignment
$\Delta\vee\\{\alpha:\mathcal{U}\\}$, specified by means of $\vee$, collects
all the types that $\alpha$ has been assigned during the derivation. Notice
that the $(\\#_{\mathtt{e}})$-rule is not deterministic since
$\Delta(\alpha)^{*}$ denotes an arbitrary union type when $\Delta(\alpha)$ is
$\langle\,\rangle$, a technical requirement which is discussed at the end of
the section.

In the simply typed $\lambda{\mu}$-calculus, $\mbox{\bf call-cc}=\lambda
y.\mu\alpha.[\alpha]y(\lambda x.\mu\beta.[\alpha]x)$ would be typed with
$((a\Rightarrow b)\Rightarrow a)\Rightarrow a$ (Peirce’s Law), so that the
fact that $\alpha$ is used twice in the type derivation would not be
explicitly materialized with simple types (same comment applies to idempotent
intersection/union types). This makes a strong contrast with the derivation in
Figure 6, where $\mathcal{A}:=\langle a\rangle$, $\mathcal{B}:=\langle
b\rangle$,
$\mathcal{U}_{y}:=\langle[\langle[\mathcal{A}]\Rightarrow\mathcal{B}\rangle]\Rightarrow\mathcal{A}\rangle$,
and call-cc is typed with the union type
$\langle[\langle[\langle[\mathcal{A}]\Rightarrow\mathcal{B}\rangle]\Rightarrow\mathcal{A}\rangle]\Rightarrow(\mathcal{A}\vee\mathcal{A})\rangle$.

${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\hskip 5.0pt plus
1.0fil{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\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 35.9857pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=71.9714pt\hbox{\kern
3.00003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
y:[\mathcal{U}_{y}]\vdash y:\mathcal{U}_{y}\mid\emptyset$}}}}\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{$\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\hskip 5.0pt plus
1.0fil{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\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 33.49289pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=66.98578pt\hbox{\kern
3.00003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\mathcal{A}]\vdash x:\mathcal{A}\mid\emptyset$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=119.26022pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
12.51799pt\hbox{$\displaystyle
x:[\mathcal{A}]\vdash[\alpha]x:\\#\mid\alpha:\mathcal{A}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=171.14577pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{e}})$}}}\hbox{\kern 0.0pt\kern
31.02269pt\hbox{$\displaystyle
x:[\mathcal{A}]\vdash\mu\beta.[\alpha]x:\mathcal{B}\mid\alpha:\mathcal{A}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=223.96465pt\hbox{\kern
3.00003pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
46.18204pt\hbox{$\displaystyle\phantom{.}\vdash\lambda
x.\mu\beta.[\alpha]x:\langle[\mathcal{A}]\Rightarrow\mathcal{B}\rangle\mid\alpha:\mathcal{A}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=277.51685pt\hbox{\kern
3.00003pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
67.12491pt\hbox{$\displaystyle\Vdash\lambda
x.\mu\beta.[\alpha]x:[\langle[\mathcal{A}]\Rightarrow\mathcal{B}\rangle]\mid\alpha:\mathcal{A}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=459.65237pt\hbox{\kern
3.00003pt$(\Rightarrow_{{\mathtt{e}}})$}}}\hbox{\kern 0.0pt\kern
159.30504pt\hbox{$\displaystyle y:[\mathcal{U}_{y}]\vdash y(\lambda
x.\mu\beta.[\alpha]x):\mathcal{A}\mid\alpha:\mathcal{A}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=488.8712pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
160.43813pt\hbox{$\displaystyle y:[\mathcal{U}_{y}]\vdash[\alpha]y(\lambda
x.\mu\beta.[\alpha]x):\\#\mid\alpha:\mathcal{A}\vee\mathcal{A}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=518.09003pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{e}})$}}}\hbox{\kern 0.0pt\kern
174.25702pt\hbox{$\displaystyle
y:[\mathcal{U}_{y}]\vdash\mu\alpha.[\alpha]y(\lambda
x.\mu\beta.[\alpha]x):\mathcal{A}\vee\mathcal{A}\mid\emptyset$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=547.30885pt\hbox{\kern
3.00003pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
140.40909pt\hbox{$\displaystyle\vdash\lambda y.\mu\alpha.[\alpha]y(\lambda
x.\mu\beta.[\alpha]x):\langle[\langle[\langle[\mathcal{A}]\Rightarrow\mathcal{B}\rangle]\Rightarrow\mathcal{A}\rangle]\Rightarrow(\mathcal{A}\vee\mathcal{A})\rangle\mid\emptyset$}}}}$

Figure 6. Typing call-cc

This example suggests to distinguish two different uses of names:

  * •

The name $\alpha$ is saved twice by a $(\\#_{\mathtt{i}})$ rule : once for $x$
and once for $y(\lambda x.\mu\beta.[\alpha]x)$, both times with type
$\mathcal{A}$. After that, the abstraction $\mu\alpha.[\alpha]y(\lambda
x.\mu\beta.[\alpha]x)$ restores the union of the two types that were
previously stored by $\alpha$ (by means of the two
$(\\#_{\mathtt{i}})$-rules). A similar phenomenon occurs with rule
$(\Rightarrow_{\mathtt{i}})$, which restores the types of the abstracted
variables.

  * •

The name $\beta$ is not free in $[\alpha]x$, so that a new union type
$\mathcal{B}$ is introduced to type the abstraction $\mu\beta.[\alpha]x$. From
a logical point of view, this corresponds to a weakening on the right hand-
side of the sequent, which is necessary, for instance, to derive the non-
idempotent counterpart of Peirce’s Law (cf. Fig. 6). Consequently, $\lambda$
and $\mu$-abstractions are not treated symmetrically: when $x$ is not free in
$t$, then $\lambda x.t$ will be typed with
$\langle[\,]\Rightarrow\sigma\rangle$ (where $\sigma$ is the type of $t$), and
no new arbitrary intersection type is introduced for the abstracted variable
$x$.

An interesting observation is about the restriction of system
$\mathcal{H}_{\lambda{\mu}}$ to the pure $\lambda$-calculus: union types, name
assignments and rules $(\\#_{\mathtt{e}})$ and $(\\#_{\mathtt{i}})$ are ruled
out, so that every union multiset takes the single form $\langle\tau\rangle$,
which can be simply identified with $\tau$. Thus, the restricted typing system
$\mathcal{H}_{\lambda{\mu}}$ becomes system $\mathcal{H}^{\prime}_{\lambda}$
in Figure 2.

Another observation is about the property of relevance of assignments.
Although there is a restricted form of weakening in system
$\mathcal{H}_{\lambda{\mu}}$ (allowing for example to derive the non-
idempotent counterpart of Peirce’s Law, see the top $(\\#_{\mathtt{e}})$-rule
in Fig. 6), if $\Gamma\vdash o:\mathcal{A}\mid\Delta$ is derivable, then any
$x\in\mathtt{dom}(\Gamma)$ (resp. $\alpha\in\mathtt{dom}(\Delta)$) has at
least one free occurrence in $o$. Formally,

######  Lemma 7 (Relevance for System $\mathcal{H}_{\lambda{\mu}}$).

Let $o\in\mathcal{O}_{\lambda{\mu}}$. If $\Phi\triangleright\Gamma\vdash
o:\mathcal{A}\mid\Delta$, then $\mathtt{dom}(\Gamma)\subseteq\mathtt{fv}(o)$
and $\mathtt{dom}(\Delta)\subseteq\mathtt{fn}(o)$.

######  Proof 4.1.

By induction on $\Phi$.

We define now our notion of derivation size, which is a natural number
representing the amount of information in tree derivations. For any type
derivation $\Phi$, $\mathtt{sz}\left(\Phi\right)$ is inductively defined by
the following rules, where we use an abbreviated, self-understanding notation
for the premises.

$\begin{array}[]{lll}\mathtt{sz}\left({tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
33.49289pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=66.98578pt\hbox{\kern
3.00003pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\mathcal{U}]\vdash x:\mathcal{U}\mid\emptyset$}}}}\right)&:=&1\\\ \\\
\mathtt{sz}\left({tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 53.81168pt\hbox{$\displaystyle\penalty 1\Phi_{t}\rhd
t$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=130.4789pt\hbox{\kern
3.00003pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\setminus\\!\\!\\!\setminus\,x\vdash\lambda
x.t:\langle\Gamma(x)\Rightarrow\mathcal{U}\rangle\mid\Delta$}}}}\right)&:=&\mathtt{sz}\left(\Phi_{t}\right)+1\\\
\\\ \mathtt{sz}\left({tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{\kern 37.81638pt\hbox{$\displaystyle\penalty 1\Phi_{t}\rhd
t$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=98.4883pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash[\alpha]t:\\#\mid\Delta\vee\\{\alpha:\mathcal{U}\\}$}}}}\right)&:=&\mathtt{sz}\left(\Phi_{t}\right)+\mathtt{ar}(\mathcal{U})\\\
\\\ \mathtt{sz}\left({tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{\kern 44.53252pt\hbox{$\displaystyle\penalty 1\Phi_{c}\rhd
c$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=113.03822pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{e}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mu\alpha.c:\Delta(\alpha)^{*}\mid\Delta\setminus\\!\\!\\!\setminus\,\alpha$}}}}\right)&:=&\mathtt{sz}\left(\Phi_{c}\right)+1\\\
\\\ \mathtt{sz}\left({tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{\kern 34.44826pt\hbox{$\displaystyle\penalty
1(\Phi_{k}\rhd t)_{{k\in K}}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=112.58095pt\hbox{\kern
3.00003pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\wedge_{{k\in K}}\Gamma_{k}\Vdash
t:[\mathcal{U}_{k}]_{{k\in K}}\mid\vee_{{k\in
K}}\Delta_{k}$}}}}\right)&:=&\Sigma_{{k\in K}}\
\mathtt{sz}\left(\Phi_{k}\right)\\\ \\\ \mathtt{sz}\left({tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{t}\rhd t:\langle\mathcal{I}_{k}\rightarrow\mathcal{U}_{k}\rangle_{{k\in
K}}\quad\Phi_{u}\rhd u$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=106.61752pt\hbox{\kern
3.00003pt$$}}}\hbox{\kern 0.0pt\kern
15.89601pt\hbox{$\displaystyle\Gamma\vdash tu:\vee_{{k\in
K}}\mathcal{V}_{k}\mid\Delta$}}}}\
(\Rightarrow_{{\mathtt{e}}})\right)&:=&\mathtt{sz}\left(\Phi_{t}\right)+\mathtt{sz}\left(\Phi_{u}\right)+|K|\end{array}$

System $\mathcal{H}_{\lambda{\mu}}$ behaves as expected, in particular, typing
is stable by reduction (Subject Reduction) and anti-reduction (Subject
Expansion):

[Weighted Subject Reduction for $\mathcal{H}_{\lambda{\mu}}$] Let
$\Phi\triangleright{\Gamma}\vdash o:\mathcal{A}\mid\Delta$. If $o\rightarrow
o^{\prime}$, then there exists a derivation
$\Phi^{\prime}\triangleright{\Gamma}\vdash o^{\prime}:\mathcal{A}\mid\Delta$
such that
$\mathtt{sz}\left(\Phi^{\prime}\right)\leq\mathtt{sz}\left(\Phi\right)$.
Moreover, if the reduced redex is typed, then
$\mathtt{sz}\left(\Phi^{\prime}\right)<\mathtt{sz}\left(\Phi\right)$.

An important remark is that, if the arity of the types were not taken into
account in the size of the rules $(\\#_{\mathtt{i}})$, then we would only have
$\mathtt{sz}\left(\Phi^{\prime}\right)=\mathtt{sz}\left(\Phi\right)$ (and not
$\mathtt{sz}\left(\Phi^{\prime}\right)<\mathtt{sz}\left(\Phi\right)$) for the
$\mu$-reduction steps. Intuitively, the $\mu$-reduction
$(\mu\alpha.c)u\rightarrow_{\mu}\mu\alpha.c\\{\alpha/\\!\\!/u\\}$ dispatches
the $(\Rightarrow_{{\mathtt{e}}})$-rule typing the root of the $\mu$-redex
$(\mu\alpha.c)u$ into several created $(\Rightarrow_{{\mathtt{e}}})$-rules in
the reduct, but neither an increase nor a decrease of the measure is ensured.
The solution to recover this key feature (i.e. the decrease) is suggested by
the effect of $\mu$-reduction on the $(\\#_{\mathtt{i}})$-rules associated to
$\alpha$ (see Figure 7): indeed, $\mu$-reduction replaces every named term
$[\alpha]v$ by $[\alpha]vu$, where $u$ is the argument of the $\mu$-redex, so
that the saved types are smaller under the created
$(\Rightarrow_{{\mathtt{e}}})$-rules than the ones in the original derivation.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 24.45259pt\hbox{$\displaystyle\penalty 1\ldots\vdash
v:\langle\mathcal{I}_{k}\rightarrow\mathcal{U}_{k}\rangle_{k\in
K}\mid\ldots$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=127.83167pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\ldots\vdash[\alpha]v:\\#\mid\ldots\vee\\{\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{U}_{k}\rangle_{{k\in
K}}\\}$}}}}$
becomes

${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\ldots\vdash
v:\langle\mathcal{I}_{k}\rightarrow\mathcal{U}_{k}\rangle_{k\in
K}\mid\ldots\qquad\ldots\Vdash u:\wedge_{{k\in
K}}\mathcal{I}_{k}\mid\ldots$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=162.77988pt\hbox{\kern
3.00003pt$(\Rightarrow_{{\mathtt{e}}})$}}}\hbox{\kern 0.0pt\kern
44.63805pt\hbox{$\displaystyle\ldots\vdash v\,u:\vee_{k\in
K}\mathcal{U}_{k}\mid\ldots$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=217.26541pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
47.42822pt\hbox{$\displaystyle\ldots\vdash[\alpha]v\,u:\\#\mid\ldots\vee\\{\alpha:\vee_{k\in
K}\mathcal{U}_{k}\\}$}}}}$

Figure 7. Effect of $\mu$-reduction on rule $(\\#_{\mathtt{i}})$

As expected from an intersection (and union) type system, head normal forms
are typable in system $\mathcal{H}_{\lambda{\mu}}$. Moreover, subject
expansion holds for $\mathcal{H}_{\lambda{\mu}}$, meaning that typing is
stable under anti-reduction. Note that we do not state a weighted subject
expansion property (although this would be possible) only because this is not
necessary to prove the final characterization property of system
$\mathcal{H}_{\lambda{\mu}}$ (cf. Theorem 8).

[Subject Expansion for $\mathcal{H}_{\lambda{\mu}}$] Let
$\Phi^{\prime}\rhd\Gamma^{\prime}\vdash
o^{\prime}:\mathcal{A}\mid\Delta^{\prime}$. If $o\rightarrow o^{\prime}$, then
there is $\Phi\rhd\Gamma^{\prime}\vdash o:\mathcal{A}\mid\Delta^{\prime}$.

Note in particular that the head strategy only reduces typed redexes (the head
redex of a head reducible typed term is necessarily typed), so that finally,
we can state our type-theoretic characterization of head normalization for the
$\lambda{\mu}$-calculus:

######  Theorem 8.

Let $o\in\mathcal{O}_{\lambda{\mu}}$. Then $o$ is
$\mathcal{H}_{\lambda{\mu}}$-typable iff $o\in\mathcal{HN}(\lambda{\mu})$ iff
the head-strategy terminates on $o$. Moreover, if $o$ is
$\mathcal{H}_{\lambda{\mu}}$-typable with tree derivation $\Pi$, then
$\mathtt{sz}\left(\Pi\right)$ gives an upper bound to the length of the head-
reduction strategy starting at $o$.

We do not provide the proofs of these properties and the last theorem, because
it uses special cases of the more general technology that we are going to
develop later to deal with strong normalization. Notice however that Theorem 8
ensures that the head-strategy is complete for head-normalization in
$\lambda{\mu}$.

###  4.3. Discussion

Now that we have stated the main result of this section, based on the key
(weighted) subject reduction property, let us come back to the design choices
of our development, in particular:

  * •

The choice $\\_^{*}$ operator in rule $(\\#_{\mathtt{e}})$ requires the types
to be blind, and

  * •

The union types are non-empty.

Blind types raised in rule $(\\#_{\mathtt{e}})$ guarantee that terms do not
have empty union types, the necessity of which is a delicate constraint
discussed later. In the meantime, we start by justifying the particular form
they adopt (arrows with empty domains), which is easier to justify. Thus,
consider the following example: let $t_{1}=\mu\beta.[\gamma]x$ with
$\beta\neq\gamma$ and $x\neq y$, so that $t_{1}\,y\rightarrow_{\mu}t_{1}$. A
typing derivation of $t_{1}$ necessarily concludes with
$x:[\mathcal{V}_{x}]\vdash
t_{1}:\langle\,\rangle^{*}\mid\gamma:\mathcal{V}_{x}$, for some union type
$\mathcal{V}_{x}$. Let us assume, only temporarily, that a non-blind type can
be chosen by the non-deterministic operator in rule $(\\#_{\mathtt{e}})$ e.g.
$\langle\,\rangle^{*}=\langle[\mathcal{U}]\Rightarrow\mathcal{U}\rangle$ for
some union type $\mathcal{U}$. If we then assign $\mathcal{U}$ to $y$, the
judgment $y:[\mathcal{U}];x:[\mathcal{V}_{x}]\vdash
t_{1}\;y:\mathcal{U}\mid\gamma:\mathcal{V}_{x}$ is derivable by rule
$(\Rightarrow_{{\mathtt{e}}})$. However, by relevance (Lemma 7), the judgment
$y:[\mathcal{U}];x:[\mathcal{V}_{x}]\vdash
t_{1}:\mathcal{U}\mid\gamma:\mathcal{V}_{x}$ cannot be derivable since
$y\notin\mathtt{fv}(t_{1})$. Thus, subject reduction simply fails. Note that
if $\langle\,\rangle^{*}$ chooses a blind type, for example
$\langle[\,]\Rightarrow\langle a\rangle\rangle$, then $y$ is untyped in the
derivation of $t_{1}y$, i.e. $x:[\mathcal{V}_{x}]\vdash
t_{1}\;y:\mathcal{U}\mid\gamma:\mathcal{V}_{x}$, so that subject reduction
holds.

We now explain why union types are non-empty. In particular, there are two
different typing rules requiring union types to be non-empty: rule
$(\texttt{ax})$ and rule $(\\#_{\mathtt{e}})$. To illustrate the necessity of
non-empty union types for $\mu$-abstractions, i.e. rule $(\\#_{\mathtt{e}})$,
let us assume, again temporarily, that an empty union type is introduced by
the rule $(\\#_{\mathtt{e}})$ when $\alpha\notin\mathtt{dom}(\Delta)$, and
call such an instance $(\\#_{\mathtt{empty}})$ when this happens. Similarly,
let us also call the instance of an application rule to be
$(\Rightarrow_{{\mathtt{empty}}})$ when the union type of its left-hand side
is empty.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash c:\\#\mid\Delta\ \hskip
14.22636pt\alpha\notin\mathtt{dom}(\Delta)$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=119.81192pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{empty}})$}}}\hbox{\kern 0.0pt\kern
26.46161pt\hbox{$\displaystyle\Gamma\vdash\mu\alpha.c:\langle\,\rangle\mid\Delta$}}}}\quad\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:\langle\,\rangle\mid\Delta\quad\emptyset\Vdash
u:[\,]\mid\emptyset$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=110.02959pt\hbox{\kern
3.00003pt$(\Rightarrow_{{\mathtt{empty}}})$}}}\hbox{\kern 0.0pt\kern
27.49983pt\hbox{$\displaystyle\Gamma\vdash tu:\langle\,\rangle\mid\Delta$}}}}$

For instance, given $t_{1}:=\mu\beta.[\gamma]x$, where $\beta\neq\gamma$,
every derivation typing $t_{1}$ concludes with rule $(\\#_{\mathtt{empty}})$
typing a judgment of the form $x:[\mathcal{V}_{x}]\vdash
t_{1}:\langle\,\rangle\mid\gamma:\mathcal{V}_{x}$.

Assume now that a derivation $\Pi_{c}$ typing a command $c$ contains $k$ empty
rules $(\\#_{\mathtt{empty}})$ w.r.t. the name $\alpha$, and that $\Pi_{c}$ is
a subderivation of some other derivation typing a $\mu$-redex $(\mu\alpha.c)u$
for some term $u$. Let us give an example with $k=2$ by setting
$c:=[\alpha]t_{2}$, where $t_{2}:=\mu\beta^{\prime}.[\alpha]t_{1}$ and
$t_{1}:=\mu\beta.[\gamma]x$ as before. Then, the (empty union) types of the
terms $t_{1}$ and $t_{2}$ are saved by $\alpha$, simply because $\beta$ (resp.
$\beta^{\prime}$) does not occur free in the body of $t_{1}$ (resp. $t_{2}$).
Thus, while typing command $c$, the name $\alpha$ is necessarily typed with
$\langle\,\rangle\vee\langle\,\rangle=\langle\,\rangle$.

Formally, let $\mathcal{V}_{x}$ be any (non-empty) union type. Then,

${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\hskip 5.0pt plus
1.0fil{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\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 45.34296pt\hbox{$\displaystyle\penalty 1\vdots$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=98.18591pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle
x:[\mathcal{V}_{x}]\vdash[\gamma]x:\\#\mid\gamma:\mathcal{V}_{x}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=150.07146pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{empty}}\mbox{ for }\beta)$}}}\hbox{\kern 0.0pt\kern
31.7946pt\hbox{$\displaystyle x:[\mathcal{V}_{x}]\vdash
t_{1}:\langle\,\rangle\mid\gamma:\mathcal{V}_{x}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=239.94109pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
71.30865pt\hbox{$\displaystyle
x:[\mathcal{V}_{x}]\vdash[\alpha]t_{1}:\\#\mid\gamma:\mathcal{V}_{x}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=291.82663pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{empty}}\mbox{ for }\beta^{\prime})$}}}\hbox{\kern
0.0pt\kern 87.86284pt\hbox{$\displaystyle
x:[\mathcal{V}_{x}]\vdash\mu\beta^{\prime}.[\alpha]t_{1}:\langle\,\rangle\mid\gamma:\mathcal{V}_{x}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=383.23625pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
122.86913pt\hbox{$\displaystyle
x:[\mathcal{V}_{x}]\vdash[\alpha](\mu\beta^{\prime}.[\alpha]t_{1}):\\#\mid\gamma:\mathcal{V}_{x}$}}}}$

Let us now use $c=[\alpha]t_{2}$ inside the $\mu$-reduction:
$t=(\mu\alpha.[\alpha]t_{2})u\rightarrow_{\mu}\mu\alpha.[\alpha](t_{3}u)=t^{\prime}$,
where $t_{3}:=\mu\beta^{\prime}.[\alpha](t_{1}u)$. Then $u$ is necessarily
typed as follows:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 24.80655pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=49.6131pt\hbox{\kern
3.00003pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\emptyset\vdash u:[\,]\mid\emptyset$}}}}$

Let us call $\Pi$ (resp. $\Pi^{\prime}$) the type derivation of $t$ (resp
$t^{\prime}$). Note that the $\mu$-reduction transforms each rule
$(\\#_{\mathtt{i}})$ of $\Pi$ into a rule $(\Rightarrow_{{\mathtt{empty}}})$
followed by $(\\#_{\mathtt{i}})$ in $\Pi^{\prime}$ (see Figure 8). Thus, if
$\Pi_{c}$ contains $k$ rules $(\\#_{\mathtt{i}})$ introducing $\alpha$, then
the derivation obtained by subject reduction typing $c\\{\alpha/\\!\\!/u\\}$
contains $k$ new rules $(\Rightarrow_{{\mathtt{empty}}})$, each followed by a
rule $(\\#_{\mathtt{i}})$. Indeed, one may check in the example above that the
derivation $\Pi^{\prime}$ contains two rules
$(\Rightarrow_{{\mathtt{empty}}})$ and two rules $(\\#_{\mathtt{i}})$
introducing $\alpha$, whereas $\Pi$ contains two rules $(\\#_{\mathtt{i}})$
introducing $\alpha$, and just one rule $(\Rightarrow_{{\mathtt{empty}}})$
(the one typing the root of the redex).

In general, one can check that whatever the size definition is for rules
$(\Rightarrow_{{\mathtt{e}}})$, $(\\#_{\mathtt{empty}})$ and
$(\Rightarrow_{{\mathtt{empty}}})$, the derivation size cannot decrease for
any choice of $k\geqslant 0$: indeed, if rule $(\\#_{\mathtt{empty}})$ is
used, the (possibly empty) type of a term $\mu\alpha.c$ holds no information
capturing the number of free occurrences of $\alpha$ in the command $c$, so
that there is no local way to know how many times the argument $u$ should be
typed in the whole derivation of the term $(\mu\alpha.c)u$ (compare Figure 8
to Figure 7).

The reader will notice that the same kind of phenomenon occurs, when in the
previous example, the term $t_{1}$ is replaced with a variable $x$ of type
$\langle\,\rangle$: then
$t=(\mu\alpha.[\alpha](\mu\beta^{\prime}.[\alpha]x))u\rightarrow_{\mu}\mu\alpha.[\alpha]((\mu\beta^{\prime}.[\alpha](xu))u)=t^{\prime}$,
the type derivation of $t^{\prime}$ contains two rules
$(\Rightarrow_{{\mathtt{empty}}})$ whereas the type derivation of $t$ contains
just one rule $(\Rightarrow_{{\mathtt{empty}}})$. This explains why one cannot
assign the empty union type in the rule $(\texttt{ax})$.

All these arguments to forbid the empty union type in our system are not only
valid for system $\mathcal{H}_{\lambda{\mu}}$, but also apply to the system
$\mathcal{S}_{\lambda{\mu}}$, introduced later in Section. 4.4.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 5.42076pt\hbox{$\displaystyle\penalty 1\ldots\vdash
v:\langle\,\rangle\mid\ldots$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=57.15851pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\ldots\vdash[\alpha]v:\\#\mid\ldots$}}}}\hskip
28.45274pt\text{becomes}\hskip 28.45274pt{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\ldots\vdash
v:\langle\,\rangle\mid\ldots\hskip 14.22636pt\ldots\Vdash
u:[\,]\mid\ldots$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=111.26767pt\hbox{\kern
3.00003pt$(\Rightarrow_{{\mathtt{e}}})$}}}\hbox{\kern 0.0pt\kern
29.61305pt\hbox{$\displaystyle\ldots\vdash
vu:\langle\,\rangle\mid\ldots$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=165.7532pt\hbox{\kern
3.00003pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
50.60175pt\hbox{$\displaystyle\ldots\vdash[\alpha]v\,u:\\#\mid\ldots$}}}}$

Figure 8. Effect of $\mu$-reduction on empty types

###  4.4. System $\mathcal{S}_{\lambda{\mu}}$

This section presents a quantitative typing system characterizing strongly
normalizing $\lambda{\mu}$-terms. The (syntax directed) typing rules of the
system $\mathcal{S}_{\lambda{\mu}}$ appear in Figure 9.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 16.23889pt\hbox{$\displaystyle\penalty
1\mathcal{U}\neq\langle\,\rangle$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=53.58893pt\hbox{\kern
2.40002pt$(\texttt{ax})$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\mathcal{U}]\vdash x:\mathcal{U}\mid\emptyset$}}}}\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 34.02504pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:\mathcal{U}\mid\Delta$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=105.93903pt\hbox{\kern
2.40002pt$(\Rightarrow_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\setminus\\!\\!\\!\setminus\,x\vdash\lambda
x.t:\langle\Gamma(x)\Rightarrow\mathcal{U}\rangle\mid\Delta$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
22.28432pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:\mathcal{U}\mid\Delta$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=82.45758pt\hbox{\kern
2.40002pt$(\\#_{\mathtt{i}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash[\alpha]t:\\#\mid\Delta\vee\\{\alpha:\mathcal{U}\\}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 24.81773pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
c:\\#\mid\Delta$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=90.43091pt\hbox{\kern
2.40002pt$(\\#_{\mathtt{e}})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mu\alpha.c:\Delta(\alpha)^{*}\mid\Delta\setminus\\!\\!\\!\setminus\,\alpha$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.58534pt\hbox{$\displaystyle\penalty 1(\Gamma_{k}\vdash
t:\mathcal{U}_{k}\mid\Delta_{k})_{{k\in K}}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=90.06496pt\hbox{\kern
2.40002pt$(\wedge)$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\wedge_{{k\in K}}\Gamma_{k}\Vdash
t:[\mathcal{U}_{k}]_{{k\in K}}\mid\vee_{{k\in K}}\Delta_{k}$}}}}\\\ \\\
{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma_{t}\vdash
t:\langle\mathcal{I}_{k}\Rightarrow\mathcal{U}_{k}\rangle_{{k\in
K}}\mid\Delta_{t}\hskip 14.22636pt\Gamma_{u}\Vdash u:\wedge_{{k\in K}}\
\mathcal{I}_{k}^{*}\mid\Delta_{u}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=147.98378pt\hbox{\kern
2.40002pt$(\Rightarrow_{\mathtt{e}*})$}}}\hbox{\kern 0.0pt\kern
28.04585pt\hbox{$\displaystyle\Gamma_{t}\wedge\Gamma_{u}\vdash tu:\vee_{{k\in
K}}\mathcal{U}_{k}\mid\Delta_{t}\vee\Delta_{u}$}}}}\end{array}$
Figure 9. System $\mathcal{S}_{\lambda{\mu}}$

As in system $\mathcal{S}^{\prime}_{\lambda}$, the non-deterministic choice
operator $\\_^{*}$ is used to choose arbitrary types for erasable terms, so
that no subterm is untyped, thus ensuring strong $\lambda{\mu}$-normalization.
The use of $\\_^{*}$ in the $(\\#_{\mathtt{e}})$-rule (raising a non-empty
union type) can be seen as a weakening on the name $\alpha$ (on the right
hand-side of the sequent) followed by a $\mu$-abstraction, while its use in
rule $(\Rightarrow_{\mathtt{e}*})$ (raising a non-empty intersection type)
should be seen weakening on the left-hand side (domain) of an arrow type. We
still consider the definition of size given before, as the choice operator
does not play any particular new role here.

As in system $\mathcal{H}_{\lambda{\mu}}$, every term is typed with a non-
empty union type:

######  Lemma 9.

If $\triangleright\Gamma\vdash t:\mathcal{U}\mid\Delta$, then
$\mathcal{U}\neq\langle\,\rangle$.

As well as in the case of $\mathcal{H}_{\lambda{\mu}}$, system
$\mathcal{S}_{\lambda{\mu}}$ can be restricted to the pure $\lambda$-calculus.
By the same observations made at the end of Section 4.2, we get the typing
system $\mathcal{S}^{\prime}_{\lambda}$ in Figure 4 that characterizes strong
$\beta$-normalization.

Relevance in system $\mathcal{S}_{\lambda{\mu}}$ is stated as follows:

######  Lemma 10 (Relevance for System $\mathcal{S}_{\lambda{\mu}}$).

Let $o\in\mathcal{O}_{\lambda{\mu}}$. If $\Phi\triangleright\Gamma\vdash
o:\mathcal{A}\mid\Delta$, then $\mathtt{dom}(\Gamma)=\mathtt{fv}(o)$ and
$\mathtt{dom}(\Delta)=\mathtt{fn}(o)$.

######  Proof 4.2.

By induction on $\Phi$.

Note the difference between Lemma 7 (inclusion) and Lemma 10 (equality): this
is because in $\mathcal{S}_{\lambda{\mu}}$ we use a choice operator in the
$(\Rightarrow_{\mathtt{e}*})$-rule to prevent any subterm of a typed term to
be left untyped.

The definition of $\mathtt{sz}\left(\right)$ is extended to system
$\mathcal{S}_{\lambda{\mu}}$ as expected. Hence,
$\mathtt{sz}\left(\Phi\right)\geq 1$ holds for any regular derivation $\Phi$,
whereas, by definition, the derivation of the empty auxiliary judgment
$\emptyset\Vdash t:[\,]\mid\emptyset$ has size $0$.

##  5\. Typing Properties

This section shows two fundamental properties of reduction (i.e. forward) and
anti-reduction (i.e. backward) of system $\mathcal{S}_{\lambda{\mu}}$. In
Section 5.1, we analyze the subject reduction (SR) property, and we prove that
reduction preserves typing and decreases the size of type derivations (that is
why we call it weighted SR). The proof of this property makes use of two
fundamental properties (Lemmas 12 and 13) guaranteeing well-typedness of the
meta-operations of substitution and replacement. Section 5.2 is devoted to
subject expansion (SE), which states that non-erasing anti-reduction preserves
types. The proof uses the fact that reverse substitution (Lemma 14) and
reverse replacement (Lemma 15) preserve types.

We start by stating an interesting property, to be used in our forthcoming
lemmas, that allows us to split and merge auxiliary derivations typing the
same term:

######  Lemma 11.

Let $\mathcal{I}=\wedge_{{k\in K}}\mathcal{I}_{k}$. Then
$\Phi\triangleright\Gamma\Vdash t:\mathcal{I}\mid\Delta$ iff there exist
$(\Gamma_{k})_{{k\in K}},(\Delta_{k})_{{k\in K}}$ s.t.
$(\Phi_{k}\triangleright\Gamma_{k}\Vdash
t:\mathcal{I}_{k}\mid\Delta_{k})_{{k\in K}}$, $\Gamma=\wedge_{{k\in
K}}\Gamma_{k}$ and $\Delta=\vee_{{k\in K}}\Delta_{k}$. Moreover,
$\mathtt{sz}\left(\Phi\right)=\Sigma_{{k\in
K}}\mathtt{sz}\left(\Phi_{k}\right)$.

###  5.1. Forward Properties

We first state the substitution lemma, which guarantees that typing is stable
by substitution. The lemma also establishes the size of the derivation tree of
a substituted object from the sizes of the derivations trees of its
components.

######  Lemma 12 (Substitution).

Let $\Theta_{u}\triangleright\Gamma_{u}\Vdash u:\mathcal{I}\mid\Delta_{u}$. If
$\Phi_{o}\triangleright\Gamma;x:\mathcal{I}\vdash o:\mathcal{A}\mid\Delta$,
then there is $\Phi_{o\\{x/u\\}}$ such that

  * •

$\Phi_{o\\{x/u\\}}\rhd\Gamma\wedge\Gamma_{u}\vdash
o\\{x/u\\}:\mathcal{A}\mid\Delta\vee\Delta_{u}$.

  * •

$\mathtt{sz}\left(\Phi_{o\\{x/u\\}}\right)=\mathtt{sz}\left(\Phi_{o}\right)+\mathtt{sz}\left(\Theta_{u}\right)-|\mathcal{I}|$.

######  Proof 5.1.

By induction on $\Phi_{o}$ using Lemmas 10 and 11. See the Appendix for
details.

Typing is also stable by replacement. Moreover, we can specify the exact size
of the derivation tree of the replaced object from the sizes of its
components.

######  Lemma 13 (Replacement).

Let $\Theta_{u}\triangleright\Gamma_{u}\Vdash u:\wedge_{{k\in K}}\
(\mathcal{I}_{k}^{*})\mid\Delta_{u}$ where $\alpha\notin\mathtt{fn}(u)$. If
$\Phi_{o}\triangleright{\Gamma}\vdash
o:\mathcal{A}\mid\alpha:\langle\mathcal{I}_{k}\Rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}};\Delta$, then there is $\Phi_{o\\{\alpha/\\!\\!/u\\}}$ such that :

  * •

$\Phi_{o\\{\alpha/\\!\\!/u\\}}\triangleright{\Gamma\wedge\Gamma_{u}}\vdash
o\\{\alpha/\\!\\!/u\\}:\mathcal{A}\mid\alpha:\vee_{{k\in
K}}\mathcal{V}_{k};\Delta\vee\Delta_{u}$.

  * •

$\mathtt{sz}\left(\Phi_{o\\{\alpha/\\!\\!/u\\}}\right)=\mathtt{sz}\left(\Phi_{o}\right)+\mathtt{sz}\left(\Theta_{u}\right)$.

######  Proof 5.2.

By induction on $\Phi$ using Lemmas 10 and 11. See the Appendix for details.

Notice that the type of $\alpha$ in the conclusion of the derivation
$\Phi_{o\\{\alpha/\\!\\!/u\\}}$ (which is $\vee_{{k\in K}}\mathcal{V}_{k}$) is
strictly smaller than that of the conclusion of the derivation $\Phi_{o}$
(which is $\langle\mathcal{I}_{k}\Rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}$) if and only if $K\neq\emptyset$.

Lemmas 12 and 13 are used in the proof of the following key property.

[Weighted Subject Reduction for $\mathcal{S}_{\lambda{\mu}}$] Let
$\Phi\triangleright{\Gamma}\vdash o:\mathcal{A}\mid\Delta$. If $o\rightarrow
o^{\prime}$ is a non-erasing step, then there exists a derivation
$\Phi^{\prime}\triangleright{\Gamma}\vdash o^{\prime}:\mathcal{A}\mid\Delta$
such that
$\mathtt{sz}\left(\Phi\right)>\mathtt{sz}\left(\Phi^{\prime}\right)$.

######  Proof 5.3.

By induction on $o\rightarrow o^{\prime}$ using Lemmas 10, 12 and 13. See the
Appendix for details.

It is now worth discussing the erasing cases. Note that variable and name
assignments are not necessarily preserved by erasing reductions. For example,
consider $t=(\lambda y.x)z\rightarrow x=t^{\prime}$. The term $t$ is typed
with a variable assignment whose domain is $\\{x,z\\}$, while $t^{\prime}$ can
only be typed with an assignment whose domain is $\\{x\\}$. Concretely,
starting from a derivation of $x:[\langle a\rangle],z:[\langle
b\rangle]\vdash(\lambda y.x)z:\langle a\rangle$ (see Example 3.1 on page 3.1),
we can derive $x:[\langle a\rangle]\vdash x:\langle a\rangle$ but not
$x:[\langle a\rangle],z:[\langle b\rangle]\vdash x:\langle a\rangle$, so that
the type is preserved while the variable assignment is not.

$\Pi_{r}$$r:\mathcal{U}$$\lambda x$$\lambda
x.r:\langle[\,]\rightarrow\mathcal{U}\rangle$$\char
64\relax$$\Gamma_{r}+\Gamma_{s}\vdash(\lambda
x.r)s:\mathcal{U}\mid\Delta_{r}+\Delta_{s}$$\Pi_{s}$$s:\mathcal{V}$$x\notin\mathtt{fv}(r)$$\Pi_{r}$$\Gamma_{r}\vdash
r:\mathcal{U}\mid\Delta_{r}$ Figure 10. Proof reduction (erasing
$\beta$-redex)

Type systems lacking (full) subject reduction are unusual, but (1) our
restricted form of subject reduction, for non-erasing steps only, is
sufficient for our purpose (see how we deal with the erasing steps in the
proof of Lemma 17), (2) strong normalization differs from head normalization
in that, whereas “$(\lambda x.r)s$ is HN” is equivalent to “$r\\{x/r\\}$ is
HN”, “$(\lambda x.r)s$ is SN” not equivalent to “$r\\{x/s\\}$ is SN” (except
in the non-erasing cases). In other words, contrary to the HN case, erasing
reductions lose information about the fact that terms are or are not SN. This
loss of information (occurring in the erasing case) is what makes subject
reduction in system $\mathcal{S}_{\lambda{\mu}}$ fail in general. This is
illustrated in Fig. 10: there are two derivations
$\Pi_{r}\triangleright\Gamma_{r}\vdash r:\mathcal{U}\mid$ and
$\Pi_{s}\triangleright\Gamma_{s}\vdash s:\mathcal{V}\mid\Delta_{s}$ with
$x\notin\mathtt{fv}(r)$, which are subderivations of $\Pi$ typing the redex
$(\lambda x.r)s$, which concludes with $\Gamma_{r}+\Gamma_{s}\vdash(\lambda
x.s)r\mid\Delta_{r}+\Delta_{s}$ (this is represented on the left-hand side of
Fig. 10). The type $\mathcal{V}$ can be seen as an instance of the choice
operator $[\,]^{*}$. The derivation typing the reduct $r$ is just $\Pi_{r}$
(on the right-hand side). All typing information pertaining to $s$ has
disappeared (i.e. has been lost), which explains why the variable/name
assignments are modified ($\Gamma_{r}/\Delta_{r}$ instead of
$\Gamma_{r}+\Gamma_{s}/\Delta_{r}+\Delta_{s}$). We will come back to the
semantics of strong normalization in Section 6.2.

###  5.2. Backward Properties

Subject expansion is based on two technical properties: the first one, called
reverse substitution, allows us to extract type information for an object $o$
and a term $u$ from the type derivation of $o\\{x/u\\}$; similarly, the second
one, called reverse replacement, gives type information for a command $c$ and
a term $u$ from the type derivation of $c\\{\alpha/\\!\\!/u\\}$. Both of them
are proved by induction on derivations using Lemmas 10 and 11. Formally,

######  Lemma 14 (Reverse Substitution).

Let $\Phi^{\prime}\triangleright\Gamma^{\prime}\vdash
o\\{x/u\\}:\mathcal{A}\mid\Delta^{\prime}$ Then there exist
$\Gamma,\Delta,\mathcal{I},\Gamma_{u},\Delta_{u}$ such that:

  * •

$\Gamma^{\prime}=\Gamma\wedge\Gamma_{u}$,

  * •

$\Delta^{\prime}=\Delta\vee\Delta_{u}$,

  * •

$\triangleright\Gamma;x:\mathcal{I}\vdash o:\mathcal{A}\mid\Delta$

  * •

$\triangleright\Gamma_{u}\Vdash u:\mathcal{I}\mid\Delta_{u}$.

######  Proof 5.4.

By induction on $\Phi^{\prime}$ using Lemmas 10 and 11. See the Appendix for
details.

######  Lemma 15 (Reverse Replacement).

Let $\Phi^{\prime}\rhd\Gamma^{\prime}\vdash
o\\{\alpha/\\!\\!/u\\}:\mathcal{A}\mid\alpha:\mathcal{V};\Delta^{\prime}$,
where $\alpha\notin\mathtt{fn}(u)$. Then there exist
$\Gamma,\Delta,\Gamma_{u},\Delta_{u},(\mathcal{I}_{k})_{{k\in
K}},(\mathcal{V}_{k})_{{k\in K}}$ such that:

  * •

$\Gamma^{\prime}=\Gamma\wedge\Gamma_{u}$,

  * •

$\Delta^{\prime}=\Delta\vee\Delta_{u}$,

  * •

$\mathcal{V}=\vee_{{k\in K}}\mathcal{V}_{k}$,

  * •

$\triangleright\Gamma\vdash
o:\mathcal{A}\mid\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}};\Delta$, and

  * •

$\triangleright\Gamma_{u}\Vdash u:\wedge_{{k\in
K}}\mathcal{I}_{k}^{*}\mid\Delta_{u}$

######  Proof 5.5.

By induction on $\Phi^{\prime}$ using Lemmas 10 and 11. See the Appendix for
details.

The following property will be used in Section 6 to show that normalization
implies typability.

[Subject Expansion for $\mathcal{S}_{\lambda{\mu}}$] Assume
$\Phi^{\prime}\rhd\Gamma^{\prime}\vdash
o^{\prime}:\mathcal{A}\mid\Delta^{\prime}$. If $o\rightarrow o^{\prime}$ is a
non-erasing step, then there is $\Phi\rhd\Gamma^{\prime}\vdash
o:\mathcal{A}\mid\Delta^{\prime}$.

######  Proof 5.6.

By induction on $\rightarrow$ using Lemma 10, 14 and 15. See the Appendix for
details.

##  6\. Strongly Normalizing $\lambda{\mu}$-Objects

###  6.1. Type-theoretic characterization, with quantitative bounds

In this section, we show the characterization of strongly-normalizing terms of
the $\lambda\mu$-calculus by means of the typing system introduced in Section
4, i.e. we show that an $\lambda{\mu}$-object $o$ is strongly-normalizing iff
$t$ is $\mathcal{S}_{\lambda{\mu}}$-typable.

As defined in Section 2, for any $\lambda{\mu}$-object $o$, we write $\eta(o)$
for the length of the maximal reduction sequence starting at $o$. Remark that
$\eta(o)<\infty$ iff $o\in\mathcal{SN}(\lambda{\mu})$. The following equations
will play a key role in our proof of Lemma 17.

######  Lemma 16.

$\begin{array}[]{llll}\eta(x\,t_{1}\ldots t_{n})&=&+_{i=1\ldots
n}\eta(t_{i})\\\ \eta(\lambda x.t)&=&\eta(t)\\\ \eta(\mu\alpha.c)&=&\eta(c)\\\
\eta([\alpha]t)&=&\eta(t)\\\ \eta((\lambda
x.t)u\,\overline{v})&=&\eta(t\\{x/u\\}\overline{v})+1&\mbox{ if
}x\in\mathtt{fv}(t)\\\ \eta((\lambda
x.t)u\,\overline{v})&=&\eta(u)+\eta(t\overline{v})+1&\mbox{ if
}x\notin\mathtt{fv}(t)\\\
\eta((\mu\alpha.c)u\overline{v})&=&\eta((\mu\alpha.c\\{\alpha/\\!\\!/u\\})\overline{v})+1&\mbox{
if }\alpha\in\mathtt{fv}(c)\\\
\eta((\mu\alpha.c)u\overline{v})&=&\eta(u)+\eta((\mu\alpha.c)\overline{v})+1&\mbox{
if }\alpha\notin\mathtt{fv}(c)\\\ \end{array}$

######  Proof 6.1.

The proof follows the same lines of that of the $\lambda$-calculus (see [50],
Fundamental Lemma of Maximality 3.18). We only briefly discuss the two last
cases.

  * •

Let $o=(\mu\alpha.c)u\,\overline{v}$, where $\alpha\in\mathtt{fv}(c)$. Take
any reduction sequence $\rho$ to normal form starting at $o$, it is
straightforward to see that $\rho$ must reduce the head redex
$(\mu\alpha.c)u$, so that $\rho$ has necessarily the form
$o\rightarrow^{*}_{\lambda{\mu}}(\mu\alpha.c^{\prime})u^{\prime}\,\overline{v^{\prime}}\rightarrow_{\lambda{\mu}}(\mu\alpha.c^{\prime}\\{\alpha/\\!\\!/u^{\prime}\\})\overline{v^{\prime}}\rightarrow_{\lambda{\mu}}\ldots$,
where $c\rightarrow^{*}_{\lambda{\mu}}c^{\prime}$,
$u\rightarrow^{*}_{\lambda{\mu}}u$ and
$\overline{v}\rightarrow^{*}_{\lambda{\mu}}\overline{v^{\prime}}$. Then $\rho$
can be transformed into another (potentially longer) reduction sequence
$\rho^{\prime}$ of the form
$o\rightarrow_{\lambda{\mu}}(\mu\alpha.c\\{\alpha/\\!\\!/u\\})\overline{v}\rightarrow^{*}_{\lambda{\mu}}\mu\alpha.c^{\prime}\\{\alpha/\\!\\!/u^{\prime}\\})\overline{v^{\prime}}\rightarrow_{\lambda{\mu}}\ldots$.
Thus
$\eta((\mu\alpha.c)u\,\overline{v})\leq\eta((\mu\alpha.c\\{\alpha/\\!\\!/u\\})\overline{v})+1$
holds. The converse inequality is easy.

  * •

Let $o=(\mu\alpha.c)u\,\overline{v}$, where $\alpha\notin\mathtt{fv}(c)$.
Again, take any reduction sequence $\rho$ to normal form starting at $o$, it
is again straightforward to see that $\rho$ must reduce the head redex
$(\mu\alpha.c)u$, so that $\rho$ has necessarily the form
$o\rightarrow^{*}_{\lambda{\mu}}(\mu\alpha.c^{\prime})u^{\prime}\,\overline{v^{\prime}}\rightarrow_{\lambda{\mu}}(\mu\alpha.c^{\prime})\overline{v^{\prime}}\rightarrow_{\lambda{\mu}}\ldots$,
where $c\rightarrow^{*}_{\lambda{\mu}}c^{\prime}$,
$u\rightarrow^{*}_{\lambda{\mu}}u$ and
$\overline{v}\rightarrow^{*}_{\lambda{\mu}}\overline{v^{\prime}}$. Then $\rho$
can be transformed into another (potentially longer) reduction sequence
$\rho^{\prime}$ of the form
$o\rightarrow^{*}_{\lambda{\mu}}(\mu\alpha.c)\mathtt{nf}(u)\,\overline{v}\rightarrow_{\lambda{\mu}}(\mu\alpha.c)\overline{v}\rightarrow^{*}_{\lambda{\mu}}(\mu\alpha.c^{\prime})\overline{v^{\prime}}\rightarrow_{\lambda{\mu}}\ldots$,
where $\mathtt{nf}(u)$ denotes the normal form of $u$. Thus,
$\eta((\mu\alpha.c)u\,\overline{v})\leq\eta(u)+\eta((\mu\alpha.c)\overline{v})+1$.
The converse inequality is easy.

The proof of our main result (Theorem 19) relies on the following two
ingredients:

  * •

Every $\mathcal{S}_{\lambda{\mu}}$-typable object is in
$\mathcal{SN}(\lambda{\mu})$ (Lemma 17).

  * •

Every object in $\mathcal{SN}(\lambda{\mu})$ is
$\mathcal{S}_{\lambda{\mu}}$-typable (Lemma 18).

We first show that any typable object $o$ belongs to
$\mathcal{SN}(\lambda{\mu})$.

######  Lemma 17.

If $o$ is $\mathcal{S}_{\lambda{\mu}}$-typable, i.e.
$\Phi\triangleright\Gamma\vdash o:\mathcal{A}\mid\Delta$, then
$\eta(o)\leq\mathtt{sz}\left(\Phi\right)$. Thus
$o\in\mathcal{SN}(\lambda{\mu})$.

######  Proof 6.2.

We show $\eta(o)\leq\mathtt{sz}\left(\Phi\right)$ by induction on
$\mathtt{sz}\left(\Phi\right)$, where $\Phi\triangleright\Gamma\vdash
o:\mathcal{A}\mid\Delta$. When $\Phi$ does not end with the rule
$(\Rightarrow_{{\mathtt{e}}})$ the proof holds straightforwardly by the i.h.
so we consider that $\Phi$ ends with $(\Rightarrow_{{\mathtt{e}}})$, where
$\mathcal{A}=\mathcal{U}$ and $o=x\,t_{1}\ldots t_{n}$ or
$o=(\mu\alpha.c)t_{1}\ldots t_{n}$ or $o=(\lambda x.u)t_{1}\ldots t_{n}$, with
$n\geq 1$.

In all the three cases for $o$, there are subderivations
$(\Phi_{i})_{i\in\\{1\ldots n\\}}$ such that
$\mathtt{sz}\left(\Phi_{i}\right)<\mathtt{sz}\left(\Phi\right)$ so that the
i.h. gives $\eta(t_{i})\leq\mathtt{sz}\left(\Phi_{i}\right)$. Now, there are
three different cases to consider:

  * (1)

If $o=x\,t_{1}\ldots t_{n}$, then there are non-empty subderivations
$\Phi_{1}\ldots\Phi_{n}$ of $\Phi$ typing $t_{1}\ldots t_{n}$ respectively.
Since $+_{i=1\ldots
n}\mathtt{sz}\left(\Phi_{i}\right)+n+1\leq\mathtt{sz}\left(\Phi\right)$, the
i.h. gives $\eta(t_{i})\leq\mathtt{sz}\left(\Phi_{i}\right)$ for $1\leq i\leq
n$. We conclude since $\eta(x\,t_{1}\ldots t_{n})=+_{i=1\ldots n}\eta(t_{i})$.

  * (2)

If $o=(\mu\alpha.c)t_{1}\ldots t_{n}$, there are two cases:

    * –

$\alpha\in\mathtt{fn}(c)$. Using Property 5.2, we get
$\Phi^{\prime}\triangleright{\Gamma}\vdash(\mu\alpha.c\\{\alpha/\\!\\!/t_{1}\\})t_{2}\ldots
t_{n}:\mathcal{U}\mid\Delta$ and
$\mathtt{sz}\left(\Phi^{\prime}\right)<\mathtt{sz}\left(\Phi\right)$. Then the
i.h. gives $\eta((\mu\alpha.c\\{\alpha/\\!\\!/t_{1}\\})t_{2}\ldots
t_{n})\leq\mathtt{sz}\left(\Phi^{\prime}\right)$. We conclude since
$\eta(o)=\eta((\mu\alpha.c\\{\alpha/\\!\\!/t_{1}\\})t_{2}\ldots
t_{n})+1\leq\mathtt{sz}\left(\Phi^{\prime}\right)+1\leq\mathtt{sz}\left(\Phi\right)$.

    * –

$\alpha\notin\mathtt{fn}(c)$. Then $\Phi$ is of the 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\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_{\mu\alpha.c}\triangleright\ldots\vdash\mu\alpha.c:\langle\xi_{0}\rangle\mid\ldots\hskip
14.22636pt\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_{1}\triangleright\ldots\vdash t_{1}:\mathcal{V}_{1}\mid\ldots$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=60.62222pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
2.2334pt\hbox{$\displaystyle\ldots\vdash
t_{1}:[\mathcal{V}_{1}]\mid\ldots$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=200.03908pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
60.40701pt\hbox{$\displaystyle\ldots\vdash(\mu\alpha.c)t_{1}:\langle\xi_{1}\rangle\mid\ldots$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=234.2579pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
113.37895pt\hbox{$\displaystyle\vdots$}}}}\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{$\displaystyle\penalty
1\Phi_{n}\triangleright\ldots\vdash t_{n}:\mathcal{V}_{n}\mid\ldots$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=62.30615pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
2.51405pt\hbox{$\displaystyle\ldots\vdash
t_{n}:[\mathcal{V}_{n}]\mid\ldots$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=379.22807pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
163.60008pt\hbox{$\displaystyle\ldots\vdash
o:\langle\xi_{n}\rangle\mid\ldots$}}}}$

with $\mathcal{U}=\langle\xi_{n}\rangle$. The type $\langle\xi_{0}\rangle$ is
obtained by choice because Lemma 10 guarantees that no $\alpha$ is typed in
the name assignments of the left derivations. Note that
$\mathtt{sz}\left(\Phi\right)=+_{i=1\ldots
n}\mathtt{sz}\left(\Phi_{i}\right)+\mathtt{sz}\left(\Phi_{\mu\alpha.c}\right)+n$
since the $\xi_{i}$ are all blind. We then build the following derivation:

$\Phi_{o^{\prime}}={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^{\prime}_{\mu\alpha.c}\triangleright\ldots\vdash\mu\alpha.c:\langle\xi_{1}\rangle\mid\ldots\hskip
14.22636pt\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_{2}\triangleright\ldots\vdash t_{2}:\mathcal{V}_{2}\mid\ldots$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=60.62222pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
2.2334pt\hbox{$\displaystyle\ldots\vdash
t_{2}:[\mathcal{V}_{2}]\mid\ldots$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=190.6435pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
91.57175pt\hbox{$\displaystyle\vdots$}}}}\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{$\displaystyle\penalty
1\Phi_{n}\triangleright\ldots\vdash t_{n}:\mathcal{V}_{n}\mid\ldots$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=62.30615pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
2.51405pt\hbox{$\displaystyle\ldots\vdash
t_{n}:[\mathcal{V}_{n}]\mid\ldots$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=335.61366pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
142.41173pt\hbox{$\displaystyle\ldots\vdash
o^{\prime}:\langle\xi_{n}\rangle\mid\ldots$}}}}$

with $o^{\prime}=(\mu\alpha.c)t_{2}\ldots t_{n}$ and
$\Phi^{\prime}_{\mu\alpha.c}$ the derivation $\Phi_{\mu\alpha.c}$ where the
choice operator raises $\xi_{1}$ instead of $\xi_{0}$ (actually, any blind
type of arity $\geq n-1$ would do). In particular,
$\mathtt{sz}\left(\Phi^{\prime}_{\mu\alpha.c}\right)=\mathtt{sz}\left(\Phi_{\mu\alpha.c}\right)$,
so that $\mathtt{sz}\left(\Phi_{o^{\prime}}\right)=+_{i=2\ldots
n}\mathtt{sz}\left(\Phi_{i}\right)+\mathtt{sz}\left(\Phi_{\mu\alpha.c}\right)+n-1<\mathtt{sz}\left(\Phi\right)$.
We also have $\mathtt{sz}\left(\Phi_{1}\right)<\mathtt{sz}\left(\Phi\right)$.
The i.h. then gives
$\eta(o^{\prime})\leq\mathtt{sz}\left(\Phi_{o^{\prime}}\right)$ and
$\eta(t_{1})\leq\mathtt{sz}\left(\Phi_{1}\right)$. We conclude since:

$\begin{array}[t]{c@{\;}l@{\;}l}\eta((\mu\alpha.c)t_{1}\ldots
t_{n})&=&\eta((\mu\alpha.c)t_{2}\ldots t_{n})+\eta(t_{1})+1\\\ &\leq_{{\it
i.h.}}&\mathtt{sz}\left(\Phi_{o^{\prime}}\right)+\mathtt{sz}\left(\Phi_{1}\right)+1\\\
&=&+_{i=2\ldots
n}\mathtt{sz}\left(\Phi_{i}\right)+\mathtt{sz}\left(\Phi_{\mu\alpha.c}\right)+n-1+\mathtt{sz}\left(\Phi_{1}\right)+1\\\
&=&\mathtt{sz}\left(\Phi\right)\end{array}$

  * (3)

If $o=(\lambda x.u)t_{1}\ldots t_{n}$, we reason similarly to the previous
case.

######  Lemma 18.

If $o\in\mathcal{SN}(\lambda{\mu})$, then $o$ is
$\mathcal{S}_{\lambda{\mu}}$-typable.

######  Proof 6.3.

By induction on $\langle\eta(o),|o|\rangle$. If $o$ is not an application
$t\,u$, the inductive step is straightforward. We only detail the case when
$o$ is an application.

  * •

If $o=x\,t_{1}\ldots t_{n}$, the property is straightforward.

  * •

If $o=(\mu\alpha.c)t_{1}\ldots t_{n}$, we set
$o^{\prime}=(\mu\alpha.c\\{\alpha/\\!\\!/t_{1}\\})t_{2}\ldots t_{n}$. There
are two cases:

    * –

$\alpha\in\mathtt{fn}(c)$. Then $\eta(o)=\eta(o^{\prime})+1$. By the i.h.,
there is $\Phi_{o^{\prime}}\triangleright\Gamma^{\prime}\vdash
o^{\prime}:\mathcal{U}\mid\Delta^{\prime}$. By Property 5.5, there is
$\Phi\triangleright\Gamma^{\prime}\vdash o:\mathcal{U}\mid\Delta^{\prime}$ and
we are done.

    * –

$\alpha\notin\mathtt{fn}(c)$. Then $o^{\prime}=(\mu\alpha.c)t_{2}\ldots t_{n}$
and $\eta(o)=\eta(o^{\prime})+\eta(t_{1})+1$. By the i.h., there are typing
derivations $\Phi_{o^{\prime}}\triangleright\Gamma^{\prime}\vdash
o^{\prime}:\mathcal{U}\mid\Delta^{\prime}$ and
$\Phi_{1}\triangleright\Gamma_{1}\vdash t_{1}:\mathcal{V}_{1}\mid\Delta_{1}$.
Since $\alpha\notin\mathtt{fn}(c)$, Lemma 10 entails that $\Phi_{o^{\prime}}$
is of the following form, where $\xi_{1}$ is a blind type:

${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^{\prime}_{\mu\alpha.c}\triangleright\mu\alpha.c:\langle\xi_{1}\rangle\hskip
14.22636pt\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_{2}\triangleright t_{2}:\mathcal{V}_{2}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=36.73334pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 4.45557pt\hbox{$\displaystyle
t_{2}:[\mathcal{V}_{2}]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=142.86572pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
67.68286pt\hbox{$\displaystyle\vdots$}}}}\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{$\displaystyle\penalty
1\Phi_{n}\triangleright t_{n}:\mathcal{V}_{n}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=38.41727pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 4.73622pt\hbox{$\displaystyle
t_{n}:[\mathcal{V}_{n}]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=263.947pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
103.51678pt\hbox{$\displaystyle\Gamma^{\prime}\vdash
o:\langle\xi_{n}\rangle\mid\Delta^{\prime}$}}}}$

We then set $\Phi$ as follows:

${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\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_{\mu\alpha.c}\triangleright\mu\alpha.c:\langle\xi_{0}\rangle\hskip
14.22636pt\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_{1}\triangleright\Gamma_{1}\vdash
t_{1}:\mathcal{V}_{1}\mid\Delta_{1}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=70.24994pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 21.21387pt\hbox{$\displaystyle
t_{1}:[\mathcal{V}_{1}]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=185.77791pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
66.33195pt\hbox{$\displaystyle(\mu\alpha.c)t_{1}:\langle\xi_{1}\rangle$}}}}\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{$\displaystyle\penalty 1\Phi_{2}\triangleright
t_{2}:\mathcal{V}_{2}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=36.73334pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 4.45557pt\hbox{$\displaystyle
t_{2}:[\mathcal{V}_{2}]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=305.17526pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
148.83763pt\hbox{$\displaystyle\vdots$}}}}\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{$\displaystyle\penalty
1\Phi_{n}\triangleright t_{n}:\mathcal{V}_{n}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=38.41727pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 4.73622pt\hbox{$\displaystyle
t_{n}:[\mathcal{V}_{n}]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=426.25655pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
164.5799pt\hbox{$\displaystyle\Gamma^{\prime}+\Gamma_{1}\vdash
o:\langle\xi_{n}\rangle\mid\Delta^{\prime}+\Delta_{1}$}}}}$

where $\Phi_{\mu\alpha.c}$ is exactly as $\Phi^{\prime}_{\mu\alpha.c}$ except
that we raise the blind type $\xi_{0}=[\,]\rightarrow\langle\xi_{1}\rangle$
instead of $\xi_{1}$ (actually, any blind type of arity $\geq n$ would do).

  * •

If $o=(\lambda x.t)u\,\overline{v}$, we reason similarly to the previous case.

Lemmas 17 and 18 allow us to conclude with the main result of this paper which
is the equivalence between typability and strong-normalization for the
$\lambda{\mu}$-calculus. Notice that no reducibility argument was used in the
whole proof.

######  Theorem 19.

Let $o\in\mathcal{O}_{\lambda{\mu}}$. Then $o$ is typable in system
$\mathcal{S}_{\lambda{\mu}}$ iff $o\in\mathcal{SN}(\lambda{\mu})$. Moreover,
if $o$ is $\mathcal{S}_{\lambda{\mu}}$-typable with tree derivation $\Pi$,
then $\mathtt{sz}\left(\Pi\right)$ gives an upper bound to the maximal length
of a reduction sequence starting at $o$.

###  6.2. Discussion

As we have observed in the end of Section 5.1, subject reduction for erasing
steps fails in system $\mathcal{S}_{\lambda{\mu}}$. The same is true for
subject expansion. This naturally rise the question: why subject reduction and
expansion should hold in system $\mathcal{H}_{\lambda{\mu}}$ (related to HN)
and not in $\mathcal{S}_{\lambda{\mu}}$ (related to SN)? The difference of
treatment lies in the semantics of what these two systems are designed to
capture:

  * •

$\mathcal{H}_{\lambda{\mu}}$ captures head normalization (Theorem 8) i.e. a
$\lambda{\mu}$-object $o$ reduces to a HNF iff $o$ is
$\mathcal{H}_{\lambda{\mu}}$-typable. The first crucial observation about
these first results is that no ”semantic information” with respect to head
normalization is lost during (arbitrary) reduction. We make this notion more
concrete below. Indeed, if $o\rightarrow o^{\prime}$ (whether this step is
erasing or not), then, by confluence, $o$ is HN iff $o^{\prime}$ is HN, and
this is why we want both subject reduction and subject expansion for
$\mathcal{H}_{\lambda{\mu}}$ to hold. Moreover, $o$ and $o^{\prime}$ have head
normal forms of the same shape. Intuitively, it is no more difficult to prove
that $o^{\prime}$ is HN than to prove that $o$ is HN, and vice-versa. Of
course, the step $o\rightarrow o^{\prime}$ may erase some reduction paths that
exist in $o$, but these (erased) reduction paths are irrelevant to the fact
that $o$ is HN or not: no semantic information pertaining to HN has been lost.
This situation is very different in system $\mathcal{S}_{\lambda{\mu}}$.

  * •

$\mathcal{S}_{\lambda{\mu}}$ captures strong normalization (Theorem 19), which
is different from weak and head normalization because it is a property about
the finiteness of all reduction paths, and not about the existence of at least
one reduction path to a normal form. This difference is materialized by the
following three observations.

    * –

If $o\rightarrow o^{\prime}$, then “$o$ is SN” and “$o^{\prime}$ is SN” are
not equivalent propositions, e.g.$(\lambda x.y)\Omega\rightarrow y$, $(\lambda
x.y)\Omega$ is not SN whereas $y$ is. In particular, no type system
characterizing SN satisfies subject expansion.

    * –

If $o\rightarrow o^{\prime}$ and “$o$ is SN”, then “$o^{\prime}$ is always
SN”, but some important semantic information may be lost with respect to
strong normalization! For instance, if $u$ is SN but the normal form of $u$
cannot be reached in less than 1000 reductions steps, then $(\lambda x.y)u$ is
also SN, but the (erasing) reduction step $(\lambda x.y)u\rightarrow y$ loses
information regarding the reduction paths starting at $(\lambda x.y)u$: the
reduction obliterates reduction paths in $u$ (intuitively, on may not know if
$y$ originates from $(\lambda x.y)u$, or $(\lambda x.y)x$, or $(\lambda
x.y)\Omega$…). This is a loss, which explains why full subject reduction does
not hold for system $\mathcal{S}_{\lambda{\mu}}$. Moreover, this also suggests
that full subject reduction would arguably be less faithful to the semantics
of strong normalization. Note that (full) subject reduction could be obtained
by just allowing weakening in the typing system, while preserving the
characterization theorem. But weakening does not restore subject expansion,
since SN is not stable under expansion.

    * –

If $o\rightarrow o^{\prime}$ and “$o^{\prime}$ is SN implies $o$ is SN”, then
the reduction step is called perpetual: perpetual strategies are precisely
those that are used to study strong normalization.

Again, it is interesting to note that, when $o\rightarrow o^{\prime}$ is non-
erasing, then $o$ is SN iff $o^{\prime}$ is SN, and any reduction path in $o$
has residuals in $o^{\prime}$. This explains why a typing system for strong
normalization should satisfy subject reduction and subject expansion for non-
erasing steps (which is sufficient to prove the characterization theorem),
while this is not necessary for erasing steps.

These observations summarize why our typing systems enjoy full subject
reduction and subject expansion in one case ($\mathcal{H}_{\lambda{\mu}}$) and
only subject reduction and subject expansion for non-erasing steps in the
other ($\mathcal{S}_{\lambda{\mu}}$).

##  7\. The $\lambda\mu_{\mathtt{s}}$-calculus

This section introduces the syntax (Section 7.1) and the operational semantics
(Section 7.2) of the $\lambda\mu_{\mathtt{s}}$-calculus, a small-step
refinement of $\lambda{\mu}$, for which the typing system
$\mathcal{S}_{\lambda{\mu}}$ naturally extends. The restriction of the
$\lambda\mu_{\mathtt{s}}$-calculus to intuitionistic logic is known as the
linear substitution calculus [1], deeply studied in rewriting theory and
complexity analysis.

###  7.1. Syntax

The set of objects ($\mathcal{O}_{\lambda\mu_{\mathtt{s}}}$), terms () and
commands ($\mathcal{C}_{\lambda\mu_{\mathtt{s}}}$) of the
$\lambda\mu_{\mathtt{s}}$-calculus are given by the following grammars

$\begin{array}[]{llll}(\textbf{objects})&o&::=&t\mid c\\\
(\textbf{terms})&t,u&::=&x\mid\lambda x.t\mid tu\mid\mu\alpha.c\mid t[x/u]\\\
(\textbf{commands})&c&::=&[\alpha]t\mid
c\langle\alpha/\\!\\!/\beta.u\rangle\\\ \end{array}$

The construction $[x/u]$ (resp. $\langle\alpha/\\!\\!/\beta.u\rangle$) is
called an explicit substitution (ES) (resp. explicit replacement (ER)). Remark
that ES do not apply to commands and ER do not apply to terms. An ES $[x/u]$
implements the meta-substitution operator $\\{x/u\\}$ while an ER
$\langle\alpha/\\!\\!/\beta.u\rangle$ implements the fresh replacement meta-
operator $\\{\alpha/\\!\\!/\beta.u\\}$ introduced in Section 2.2, i.e. the
small step computation of $c\langle\alpha/\\!\\!/\beta.u\rangle$ replaces only
one occurrence of $[\alpha]t$ inside $c$ by
$[\beta]t\langle\alpha/\\!\\!/\beta.u\rangle u$. As in Section 2.1, the size
of an object $o$ is denoted by $|o|$.

The notions of free and bound variables and names are extended as expected, in
particular
$\mathtt{fv}(t[x/u]):=(\mathtt{fv}(t)\setminus\\{x\\})\cup\mathtt{fv}(u)$ and
$\mathtt{fn}(c\langle\alpha/\\!\\!/\beta.u\rangle):=(\mathtt{fn}(c)\setminus\\{\alpha\\})\cup\\{\beta\\}\cup\mathtt{fn}(u)$.
The derived notion of $\alpha$-conversion (i.e. renaming of bound variables
and names) will be assumed in the rest of the paper. Thus e.g.
$([\gamma]x[x/y])\langle\gamma/\\!\\!/\beta.z\rangle=_{\alpha}([\gamma^{\prime}]x^{\prime}[x^{\prime}/y])\langle\gamma^{\prime}/\\!\\!/\beta.z\rangle$.
The number of free occurrences of the variable $x$ (resp. the name $\alpha$)
in $o$ is denoted by $|o|_{x}$ (resp. $|o|_{\alpha}$).

List ($\mathtt{L}$), term ($\mathtt{TT},\mathtt{CT},\mathtt{OT}$), and command
($\mathtt{TC},\mathtt{CC},\mathtt{OC}$) contexts are respectively defined by
the following grammars:

$\begin{array}[]{llll}\mathtt{L}::=\Box\mid\mathtt{L}[x/u]\\\
\mathtt{TT}::=\Box\mid\lambda x.\mathtt{TT}\mid\mathtt{TT}\,t\mid
t\,\mathtt{TT}\mid\mu\alpha.\mathtt{CT}\mid\mathtt{TT}[x/t]\mid
t[x/\mathtt{TT}]\\\
\mathtt{CT}::=[\alpha]\mathtt{TT}\mid\mathtt{CT}\langle\alpha/\\!\\!/\beta.u\rangle\mid
c\langle\alpha/\\!\\!/\beta.\mathtt{TT}\rangle\\\
\mathtt{OT}::=\mathtt{TT}\mid\mathtt{CT}\\\ \mathtt{TC}::=\lambda
x.\mathtt{TC}\mid\mathtt{TC}\,t\mid
t\,\mathtt{TC}\mid\mu\alpha.\mathtt{CC}\mid\mathtt{TC}[x/t]\mid
t[x/\mathtt{TC}]\\\
\mathtt{CC}::=\boxdot\mid[\alpha]\mathtt{TC}\mid\mathtt{CC}\langle\alpha/\\!\\!/\beta.u\rangle\mid
c\langle\alpha/\\!\\!/\beta.\mathtt{TC}\rangle\\\
\mathtt{OC}::=\mathtt{TC}\mid\mathtt{CC}\\\ \end{array}$

The hole $\Box$ (resp. $\boxdot$) can be replaced by a term (resp. a command).
Indeed, $\mathtt{L}[t]$ denotes the replacement of $\Box$ in $\mathtt{L}$ by
the term $t$ (similarly for $\mathtt{TT}[t]$, $\mathtt{CT}[t]$ and
$\mathtt{OT}$), while $\mathtt{CC}[c]$ denotes the replacement of $\boxdot$ in
$\mathtt{CC}$ by the command $c$ (similarly for $\mathtt{TC}$ and
$\mathtt{OC}$). Every meta-expression $\mathtt{X}\mathtt{Y}$ with
$\mathtt{X}\in\\{\mathtt{T},\mathtt{C}\\}$ and
$\mathtt{Y}\in\\{\mathtt{T},\mathtt{C}\\}$ must be interpreted as a context
taking an object $\mathtt{Y}$ and yielding an object $\mathtt{X}$: e.g.
$\mathtt{TC}$ denotes a context that takes a command ($\mathtt{C}$ on the
right) and outputs a term ($\mathtt{T}$ on the left).

We write $\mathtt{OT}^{\mathcal{S}}$ for a term context $\mathtt{OT}$ which
does not capture the free variables and names in the set $\mathcal{S}$, i.e.
there are no abstractions and substitutions in the context that bind the
symbols in $\mathcal{S}$. For instance $\mathtt{TT}=\lambda y.\Box$ can be
specified as $\mathtt{TT}^{x}$ while $\mathtt{TT}=\lambda x.\Box$ cannot. In
order to emphasize this particular property we may write
$\mathtt{TT}^{\mathcal{S}}{[}\\!{[}t{]}\\!{]}$ instead of
$\mathtt{TT}^{\mathcal{S}}[t]$, and we may omit $\mathcal{S}$ when it is clear
from the context. Same concepts apply to command contexts, i.e.
$\mathtt{OC}^{\mathcal{S}}$ does not capture the variables and names in
$\mathcal{S}$ and the notation used for that is
$\mathtt{OC}^{\mathcal{S}}{[}\\!{[}c{]}\\!{]}$.

###  7.2. Operational Semantics

The reduction rules of the $\lambda\mu_{\mathtt{s}}$-calculus aim to give a
small-step semantics to the $\lambda{\mu}$-calculus, based on the
substitution/replacement at a distance paradigm [2, 1]. The reduction relation
$\lambda\mu_{\mathtt{s}}$ of the calculus is given by the context closure of
the following rewriting rules.

<EMAIL_ADDRESS>x.t]\,u\hfil\hskip 5.69046pt&\mapsto_{\mathtt{B}}\hfil\hskip
5.69046pt&\mathtt{L}[t[x/u]]\hfil\hskip 5.69046pt\\\
\mathtt{TT}{[}\\!{[}x{]}\\!{]}[x/u]\hfil\hskip
5.69046pt&\mapsto_{\mathtt{c}_{v}}\hfil\hskip
5.69046pt&\mathtt{TT}{[}\\!{[}u{]}\\!{]}[x/u]\hfil\hskip 5.69046pt&\mbox{if
}|\mathtt{TT}{[}\\!{[}x{]}\\!{]}|_{x}>1\hfil\hskip 5.69046pt\\\
\mathtt{TT}{[}\\!{[}x{]}\\!{]}[x/u]\hfil\hskip
5.69046pt&\mapsto_{\mathtt{d}_{v}}\hfil\hskip
5.69046pt&\mathtt{TT}{[}\\!{[}u{]}\\!{]}\hfil\hskip 5.69046pt&\mbox{if
}|\mathtt{TT}{[}\\!{[}x{]}\\!{]}|_{x}=1\hfil\hskip 5.69046pt\\\
t[x/u]\hfil\hskip 5.69046pt&\mapsto_{\mathtt{w}_{v}}\hfil\hskip
5.69046pt&t\hfil\hskip 5.69046pt&\mbox{if }x\notin\mathtt{fv}(t)\hfil\hskip
5.69046pt\\\ \mathtt{L}[\mu\alpha.c]\,u\hfil\hskip
5.69046pt&\mapsto_{\mathtt{M}}\hfil\hskip
5.69046pt&\mathtt{L}[\mu\gamma.c\langle\alpha/\\!\\!/\gamma.u\rangle]\hfil\hskip
5.69046pt&\mbox{if }\gamma\mbox{ is fresh }\hfil\hskip 5.69046pt\\\
\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}\langle\alpha/\\!\\!/\gamma.u\rangle\hfil\hskip
5.69046pt&\mapsto_{\mathtt{c}_{n}}\hfil\hskip
5.69046pt&\mathtt{CC}{[}\\!{[}[\gamma]tu{]}\\!{]}\langle\alpha/\\!\\!/\gamma.u\rangle\hfil\hskip
5.69046pt&\mbox{if
}|\mathtt{CC}{[}\\!{[}[\alpha]t]{]}\\!{]}|_{\alpha}>1\hfil\hskip 5.69046pt\\\
\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}\langle\alpha/\\!\\!/\gamma.u\rangle\hfil\hskip
5.69046pt&\mapsto_{\mathtt{d}_{n}}\hfil\hskip
5.69046pt&\mathtt{CC}{[}\\!{[}[\gamma]tu{]}\\!{]}\hfil\hskip
5.69046pt&\mbox{if
}|\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}|_{\alpha}=1\hfil\hskip 5.69046pt\\\
c\langle\alpha/\\!\\!/\gamma.u\rangle\hfil\hskip
5.69046pt&\mapsto_{\mathtt{w}_{n}}\hfil\hskip 5.69046pt&c\hfil\hskip
5.69046pt&\mbox{if }\alpha\notin\mathtt{fn}(c)\hfil\hskip 5.69046pt\\\
\end{array}$

where $\mathtt{TT}$ is to be understood as $\mathtt{TT}^{x}$ and $\mathtt{CC}$
as $\mathtt{CC}^{\alpha,\gamma}$.

We use $\rightarrow_{\mathtt{w}}$ for the reduction relation generated by the
set of rules $\\{\mapsto_{\mathtt{w}_{v}},\mapsto_{\mathtt{w}_{n}}\\}$ and
$\rightarrow_{\lambda{\overline{\mu\mathtt{s}}}}$ for the non-erasing
reduction relation
$\rightarrow_{\lambda\mu_{\mathtt{s}}}\setminus\rightarrow_{\mathtt{w}}$. For
instance, the big step reduction

$(\mu\alpha.[\alpha]x(\mu\beta.[\alpha]\lambda
x.xx))u\rightarrow_{\mu}\mu\gamma.[\gamma]x(\mu\beta.[\gamma](\lambda
x.xx)u))u$

where $\alpha$ has been alpha-renamed to $\gamma$, can be now emulated by 3
small steps :

$\begin{array}[]{l}(\mu\alpha.[\alpha]x(\mu\beta.[\alpha]\lambda x.xx))u\\\
\rightarrow_{\mathtt{M}}\mu\gamma.([\alpha]x(\mu\beta.[\alpha]\lambda
x.xx))\langle\alpha/\\!\\!/\gamma.u\rangle\\\
\rightarrow_{\mathtt{c}_{n}}\mu\gamma.([\alpha]x(\mu\beta.[\gamma](\lambda
x.xx)u))\langle\alpha/\\!\\!/\gamma.u\rangle\\\
\rightarrow_{\mathtt{d}_{n}}\mu\gamma.[\gamma]x(\mu\beta.[\gamma](\lambda
x.xx)u))u\end{array}$

Notice that the occurrences of $\alpha$ are (arbitrarily) replaced by $\gamma$
one after another, thus replacement is linearly processed. When there is just
one occurrence of $\alpha$ left, the small reduction step $\mathtt{d}_{n}$
performs the last replacement and erases the remaining ER
$\langle\alpha/\\!\\!/\gamma.u\rangle$ to complete the operation.

More generally, not only the syntax of the $\lambda\mu_{\mathtt{s}}$-calculus
can be seen as a refinement of the $\lambda{\mu}$-calculus, but also its
operational semantics. Formally,

######  Lemma 20.

If $o\in\mathcal{O}_{\lambda{\mu}}$, then
$o\rightarrow_{\lambda{\mu}}o^{\prime}$ implies
$o\rightarrow^{+}_{\lambda\mu_{\mathtt{s}}}o^{\prime}$.

######  Proof 7.1.

By induction on the reduction relation $\rightarrow_{\lambda{\mu}}$.

Moreover, we can project $\lambda\mu_{\mathtt{s}}$-reduction sequences into
$\lambda{\mu}$-reduction sequences. Indeed, consider the projection function
$\mathtt{P}(\\_)$ computing all the explicit substitutions and replacements of
an object, thus in particular
$\mathtt{P}(t[x/u]):=\mathtt{P}(t)\\{x/\mathtt{P}(u)\\}$ and
$\mathtt{P}(c\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle):=\mathtt{P}(c)\\{\alpha/\\!\\!/\alpha^{\prime}.\mathtt{P}(u)\\}$.
Then,

######  Lemma 21.

If $o\in\mathcal{O}_{\lambda\mu_{\mathtt{s}}}$, then
$o\rightarrow_{\lambda\mu_{\mathtt{s}}}o^{\prime}$ implies
$\mathtt{P}(o)\rightarrow^{*}_{\lambda{\mu}}\mathtt{P}(o^{\prime})$.

######  Proof 7.2.

By induction on the reduction relation
$\rightarrow_{\lambda\mu_{\mathtt{s}}}$.

###  7.3. Typing System

In this section we extend the (quantitative) typing system
$\mathcal{S}_{\lambda{\mu}}$ in order to capture the
$\lambda\mu_{\mathtt{s}}$-calculus, the aim being to characterize the set of
strongly $\lambda\mu_{\mathtt{s}}$-normalizing objects by using quantitative
arguments.

More precisely, system $\mathcal{S}_{\lambda{\mu}}$ is enriched with the two
typing rules in Figure 11.

${\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma_{t};x:\mathcal{I}\vdash
t:\mathcal{U}\mid\Delta_{t}\hskip 14.22636pt\Gamma_{u}\Vdash
u:\mathcal{I}^{*}\mid\Delta_{u}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=135.31078pt\hbox{\kern
3.00003pt$(\mathtt{s})$}}}\hbox{\kern 0.0pt\kern
10.73535pt\hbox{$\displaystyle\Gamma_{t}\wedge\Gamma_{u}\vdash
t[x/u]:\mathcal{U}\mid\Delta_{t}\vee\Delta_{u}$}}}}\\\ \\\ {{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma_{c}\vdash
c:\\#\mid\Delta_{c};\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\\!\\!\\!\\!\hskip 14.22636pt\Gamma_{u}\Vdash u:({\wedge_{{k\in
K}}\mathcal{I}_{k}^{*}})^{*}\mid\Delta_{u}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=202.41653pt\hbox{\kern
3.00003pt$(\mathtt{r})$}}}\hbox{\kern 0.0pt\kern
9.3809pt\hbox{$\displaystyle\Gamma_{c}\wedge\Gamma_{u}\vdash