11institutetext:  Universidad Nacional de Quilmes (CONICET), and Instituto de
Ciencias de la Computación, UBA
Argentina 22institutetext: Université Paris Cité, CNRS, IRIF
France

# Hybrid Intersection Types for PCF (Extended Version)

Pablo Barenbaum111 Partially funded by project grants PUNQ 418/22 and
PICT-2023-602.  11 Delia Kesner 22 Mariana Milicich222 This project has
received funding from the European Union’s Horizon 2020 research and
innovation programme under the Marie Skłodowska-Curie grant agreement No
945332.  22

###### Abstract

Intersection type systems have been _independently_ applied to different
evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV).
These type systems have been then generalized to different subsuming paradigms
being able, in particular, to _encode_ CBN and CBV in a _unique_ unifying
framework. However, there are no intersection type systems that explicitly
enable CBN and CBV to cohabit together, without making use of an encoding into
a common target framework.

This work proposes an intersection type system for a specific notion of
evaluation for PCF, called PCFH. Evaluation in PCFH actually has a _hybrid_
nature, in the sense that CBN and CBV operational behaviors cohabit together.
Indeed, PCFH combines a CBV-like behavior for function application with a CBN-
like behavior for recursion. This hybrid nature is reflected in the type
system, which turns out to be _sound_ and _complete_ with respect to PCFH: not
only typability implies normalization, but also the converse holds. Moreover,
the type system is _quantitative_ , in the sense that the size of typing
derivations provides upper bounds for the length of the reduction sequences to
normal form. This first type system is then refined to a _tight_ one, offering
_exact_ information regarding the length of normalization sequences. This is
the first time that a sound and complete quantitative type system has been
designed for a hybrid computational model.

##  0.1 Introduction

Evaluation strategies govern how computation proceeds in programming
languages. Two prominent strategies are _call-by-name_ (CBN) and _call-by-
value_ (CBV) [23]. In CBN, arguments are not evaluated before being consumed
by functions, while in CBV, arguments must be fully evaluated to _values_
before function application can proceed.

These two ways to perform evaluation have their own advantages and drawbacks.
CBV evaluation can sometimes be less costly than CBN, since CBV evaluates
arguments only once, while CBN may have to evaluate many copies of a single
argument. Conversely, sometimes CBN evaluation can be less costly than CBV, as
CBN does not evaluate an _unused_ argument while CBV always evaluates
arguments, even if their value is not needed. For instance, if the function
$g$ is constantly $0$ and $\Omega$ is a looping program, then $g(\Omega)$
produces $0$ as a result in CBN while CBV evaluation does not terminate.

The main motivation of this work is to enhance our understanding of the
_quantitative semantics_ of programming language constructs such as inductive
data types and recursion. The quantitative semantics of minimalistic languages
such as the $\lambda$-calculus are relatively well-understood in both the CBN
and CBV settings (see [8, 12]), but inductive data types and recursion cannot
be expressed directly, and must instead rely on some sort of _encoding_. In
this work, we study PCFH, an extension of the $\lambda$-calculus that
incorporates natural numbers, conditional expressions, and recursion through a
fixed-point operator without resorting to an encoding.

##### Non-idempotent intersection types.

Intersection types (IT), pioneered by Coppo and Dezani [9], extend simple
types with a new _intersection_ type constructor ($\cap$), in such a way that
a term is assigned the type $\tau\cap\sigma$ if and only if it is assigned
both types $\tau$ and $\sigma$. Originally, intersection is commutative,
associative and, in particular, _idempotent_ , i.e. $\tau$ and $\tau\cap\tau$
are equivalent. An intersection $\tau_{1}\cap\ldots\cap\tau_{n}$ can thus be
specified by a _set_ $\\{\tau_{1},\ldots,\tau_{n}\\}$. IT were motivated by
semantical concerns. A key property is that typability is preserved by
_conversion_ (reduction _and_ expansion), in contrast with simple types, in
which typability is preserved by reduction but not expansion. This technical
property allows to study normalization from a type theoretical point of view.
In intersection types, a term is typable if and only if it is normalizing,
while in simple types, typable terms are normalizing but the converse does not
hold.

A more recent line of research is that of _non-idempotent_ IT [17, 8], in
which $\tau\cap\tau$ is not equivalent to $\tau$. Here, an intersection
$\tau_{1}\cap\ldots\cap\tau_{n}$ may be specified by a _multiset_
$[\tau_{1},\ldots,\tau_{n}]$. These systems draw inspiration from Linear Logic
(LL) [18], as in fact, non-idempotent intersection corresponds to LL’s
multiplicative conjunction ($\otimes$) [8]. Just like in the idempotent case,
non-idempotent IT characterize normalization by means of typability [8].
Moreover, non-idempotent types have some advantages over idempotent ones; one
key benefit is their ability to capture _quantitative_ information about the
dynamic behavior of programs. For example, in non-idempotent IT one can not
only prove that a term $t$ is normalizing if and only if it is typable, but
also obtain an _upper bound_ for the length of the evaluation sequence of $t$
to normal form. Since these systems are inspired by linear logic and resource
consumption [17], they are called _quantitative_ type systems. Several works
have explored non-idempotent intersection type systems in the context of CBN
[10, 7] and CBV [12, 3, 20]. In these systems, the quantitative information
can usually be recorded using _counters_ that decorate typing judgments. For
example, a typical judgment may be of the form $\Gamma\vdash^{n}t:\tau$,
meaning that $t$ normalizes to a normal form of type $\tau$, and that the
number of reduction steps required to reduce $t$ to normal form is _bounded_
by the value of the counter $n\in\mathbb{N}$.

Quantitative properties provided by non-idempotent intersection type systems
can be refined using a syntactic property, _tightness_ , achieved by using
only _minimal_ type derivations [2]. Tightness allows to extract from typing
derivations not only _upper bounds_ but rather _exact_ quantitative
information. Indeed, in tight derivations, a concluding judgment is still of
the form $\Gamma\vdash^{n}t:\tau$, but now the counter $n\in\mathbb{N}$
indicates that _exactly_ $n$ reduction steps are required to reduce $t$ to
normal form.

##### PCF and PCFH.

_Programming Computable Functions_ (PCF) [24] is a functional programming
language designed to serve as a foundational computational model. It extends
the simply-typed $\lambda$-calculus with natural numbers, conditional
expressions, and general recursion (through a fixed-point operator). PCF is
simultaneously minimalistic, expressive, and rigorous, making it an ideal
vehicle to study programming language semantics. Historically, it has been
used to study the correspondence between operational and denotational
semantics, i.e., the _full abstraction_ problem [24, 22, 1, 16].

In this work, we study a variant of PCF called PCFH, in which function
application and evaluation of conditional expressions follow a CBV discipline.
Besides that, the rule to _unfold_ a fixed-point is the standard one, namely:

$\mathsf{fix}\,x.\,t\to t\\{x:=\mathsf{fix}\,x.\,t\\}$

A noteworthy remark is that the semantics of recursion is akin to CBN rather
than to CBV since the fixed-point can make copies of itself, which is _not_ a
value yet. Given this “mixed” operational behavior, we say that evaluation in
PCFH is _hybrid_. The fact that evaluation is hybrid is challenging from the
point of view of quantitative semantics [20, 5] because it requires
synthesizing characteristics of CBN and CBV in a single system.

##### A note on nomenclature.

Languages closely related to PCFH are sometimes said to be “call-by-value”
[11]. As explained above, evaluation in PCFH is actually hybrid because
unfolding a fixed-point may produce copies of itself, substituting a variable
by an expression that is not a value yet. We write PCFH to highlight the fact
that evaluation is hybrid, as indicated by the subscript “H”.

##### Related work.

There is a vast amount of literature on PCF. In particular, various notions of
evaluation have been proposed for PCF; for instance, [19] provides insights on
differences and similarities between CBV semantics and CBN semantics. A
probabilistic version of PCF is presented in [16], which follows a CBN
discipline but is still hybrid in that it exhibits a CBV behavior for its
conditional operator.

Furthermore, some works explore semantical aspects of PCF that are connected
to our own. In [13], Ehrhard studies an interpretation of a Call-by-Push-Value
(CBPV) $\lambda$-calculus with disjoint unions and fixed-points (encompassing
PCF) in LL, and it derives an intersection type system from the Scott model of
LL. The unfolding of a fixed-point operator can duplicate itself by copying a
value that represents its suspended computation. Technically, this is achieved
by relying on the of-course ($!$) modality of LL. The resulting type system is
in the style of Coppo–Dezani, with _idempotent_ intersections, and thus not
quantitative.

Recent work in [14] derives an intersection type system for a differential
extension of PCF from a relational semantics. It is shown that typability in
this system implies normalization by means of a reducibility argument, but the
quantitative aspect is not studied. In contrast, we prove soundness and
completeness by elementary means, and we characterize quantitative upper
bounds and exact bounds via our non-idempotent type system.

There are other languages in the literature that allow the encoding of CBN/CBV
behavior, such as Levy’s _call-by-push-value_ (CBPV) [21] and Ehrhard and
Guerrieri’s _Bang Calculus_ [15]. They attempt to unify CBN and CBV in a
single framework, but they are not hybrid because they only allow duplicating
values. Recent works [20, 5] propose quantitative type systems for _adequate_
variants of the Bang Calculus. These works study upper bounds and exact
bounds. However, they are not able to express recursion and integers directly,
but only through encodings.

##### Contributions.

As a main contribution, we propose a quantitative model for the hybrid
calculus PCFH, based on a non-idempotent intersection type system. The type
system is proved to be sound and complete with respect to the operational
semantics: it characterizes normalizing terms and provides upper bounds for
the length of reductions to normal form. A peculiar feature of this system is
that it distinguishes between those variables bound by $\lambda$-abstractions
from those bound by fixed-point operators. The former may be substituted by
_values_ while the latter may be substituted by arbitrary _expressions_. Type
assignment rules work differently for these two kinds of variables because a
value is assigned one type each time it will be used (as in CBV), while an
arbitrary expression may be copied to produce many values (as in CBN).

As a second contribution, we refine the type system to obtain a _tight_
version, which provides _exact_ bounds for reduction lengths to normal form,
instead of upper bounds.

To the best of our knowledge, this is the first quantitative type
interpretation that is adequate for a hybrid system.

##### Structure of the paper.

Section 0.2 covers the syntax and operational semantics of PCFH. Section 0.3
introduces a quantitative type system for PCFH. Finally, the paper concludes
by summarizing our work and outlining potential directions for future work.

##  0.2 The PCFH calculus

This section introduces the syntax of PCFH, together with its associated
operational semantics, which follows a hybrid evaluation. We characterize the
set of normal forms induced by the operational semantics through a grammar
(Section 0.2). Moreover, as the evaluation strategy is not necessarily
deterministic, we show that it enjoys the Diamond Property (Section 0.2),
which implies in particular that all evaluation sequences to normal form have
the same length, thus justifying the use of the proposed strategy to study
quantitative behaviors.

Given a denumerable set of variables $(x,y,z,\ldots)$, we define terms
$(t,s,u,\ldots)$, values $(\mathbf{v},\mathbf{w},\ldots)$, and natural values
$(\mathbf{k},\mathbf{l},\ldots)$ using the following grammar:

$t\mathrel{::=}x\mid\lambda x.\,t\mid t\,t\mid{\bf
0}\mid\mathbf{S}(t)\mid\mathsf{if}(t,t,x.\,t)\mid\mathsf{fix}\,x.\,t$
$\mathbf{v}\mathrel{::=}\lambda x.\,t\mid\mathbf{k}\hskip 14.22636pt\hskip
14.22636pt\mathbf{k}\mathrel{::=}{\bf 0}\mid\mathbf{S}(\mathbf{k})$

Terms include variables $x$, abstractions $\lambda x.\,t$, applications
$t\,s$, a fixed-point operator $\mathsf{fix}\,x.\,t$, as well as syntax for
natural numbers: zero ${\bf 0}$, the successor constructor $\mathbf{S}(t)$,
and a conditional operator $\mathsf{if}(t,s,x.\,u)$. Free and bound
occurrences of variables are defined as expected, considering that the free
occurrences of $x$ in $u$ are bound in $\mathsf{if}(t,s,x.\,u)$ and in
$\mathsf{fix}\,x.\,u$. Terms are considered up to $\alpha$-renaming of bound
variables. We write $t\\{x:=s\\}$ for the capture-avoiding substitution of the
free occurrences of $x$ by $s$ in $t$.

The operational semantics of PCFH is given by a reduction relation
$\to_{\rho}$ indexed by a rule name
$\rho\in\\{\texttt{B},\texttt{I0},\texttt{IS},\texttt{F}\\}$, and it is
defined by the following set of rules:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 41.44861pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=82.89722pt\hbox{\kern
3.00003pt$\texttt{{r-beta}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle(\lambda
x.\,t)\,\mathbf{v}\to_{\texttt{B}}t\\{x:=\mathbf{v}\\}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
31.91798pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=63.83597pt\hbox{\kern
3.00003pt$\texttt{{r-if0}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{if}({\bf
0},t,x.\,s)\to_{\texttt{I0}}t$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 56.58052pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=113.16104pt\hbox{\kern
3.00003pt$\texttt{{r-ifS}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{if}(\mathbf{S}(\mathbf{k}),t,x.\,s)\to_{\texttt{IS}}s\\{x:=\mathbf{k}\\}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
50.2617pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=100.5234pt\hbox{\kern
3.00003pt$\texttt{{r-fix}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{fix}\,x.\,t\to_{\texttt{F}}t\\{x:=\mathsf{fix}\,x.\,t\\}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 6.35413pt\hbox{$\displaystyle\penalty
1t\to_{\rho}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=32.14348pt\hbox{\kern
3.00003pt$\texttt{{r-appL}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
t\,s\to_{\rho}t^{\prime}\,s$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.27774pt\hbox{$\displaystyle\penalty 1s\to_{\rho}s^{\prime}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=32.14348pt\hbox{\kern
3.00003pt$\texttt{{r-appR}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
t\,s\to_{\rho}t\,s^{\prime}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.72223pt\hbox{$\displaystyle\penalty
1t\to_{\rho}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=46.10197pt\hbox{\kern
3.00003pt$\texttt{{r-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathbf{S}(t)\to_{\rho}\mathbf{S}(t^{\prime})$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
44.73837pt\hbox{$\displaystyle\penalty 1t\to_{\rho}t^{\prime}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=108.91197pt\hbox{\kern
3.00003pt$\texttt{{r-if}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{if}(t,s,x.\,u)\to_{\rho}\mathsf{if}(t^{\prime},s,x.\,u)$}}}}\end{array}$

The resulting evaluation strategy is _closed_ (no reduction of terms with free
variables) and _weak_ (no evaluation under abstractions).

Several variants of PCF can be found in the literature. In this presentation,
function application follows a CBV discipline because the argument of an
application must be evaluated until it becomes a value, so that the rule
r-beta can be applied. The conditional operator follows a CBV discipline as
well, as the guard must be fully evaluated to a value so that one of the rules
r-if0 or r-ifS can be applied. The conditional $\mathsf{if}(t,s,x.\,u)$
returns $s$ if $t$ is zero, and $u$ if $t$ is non-zero, binding $x$ to its
predecessor. A consequence of this is that the predecessor function can be
defined using the conditional operator; e.g.
$\mathsf{if}(\mathbf{S}(\mathbf{k}),{\bf
0},x.\,x)\to_{\texttt{IS}}\mathbf{k}$, a variant which can be found in [16].

To illustrate this strategy, let us evaluate the term
$\mathsf{if}(\mathbf{S}({\bf 0}),\mathtt{id},x.\,\lambda
y.\,x)\,\mathbf{S}(\mathbf{S}({\bf 0}))$ in one step, where
$\mathtt{id}:=\lambda z.\,z$:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
77.77542pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=159.9064pt\hbox{\kern
3.00003pt$\texttt{{r-ifS}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{if}(\mathbf{S}({\bf
0}),\mathtt{id},x.\,\lambda y.\,x)\to_{\texttt{IS}}(\lambda y.\,x)\\{x:={\bf
0}\\}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=222.76416pt\hbox{\kern
3.00003pt$\texttt{{r-appL}}$}}}\hbox{\kern
15.47742pt\hbox{$\displaystyle\mathsf{if}(\mathbf{S}({\bf
0}),\mathtt{id},x.\,\lambda y.\,x)\,\mathbf{S}(\mathbf{S}({\bf
0}))\to_{\texttt{IS}}(\lambda y.\,{\bf 0})\,\mathbf{S}(\mathbf{S}({\bf
0}))$}}}}\end{array}$

After one more reduction step, by rule r-beta, we obtain $(\lambda y.\,{\bf
0})\,\mathbf{S}(\mathbf{S}({\bf 0}))\to_{\texttt{B}}{\bf 0}$.

Let us write $t\to s$ if $t\to_{\rho}s$ for some rule name $\rho$. A term $t$
is $\to$-reducible if there exists $s$ such that $t\to s$; and $t$ is
$\to$-irreducible if $t$ is not $\to$-reducible. For the example above, ${\bf
0}$ is $\to$-irreducible, while $\mathsf{if}(\mathbf{S}({\bf
0}),\mathtt{id},x.\,\lambda y.\,x)\,\mathbf{S}(\mathbf{S}({\bf 0}))$ is
$\to$-reducible.

Terms that cannot be further $\to$-reduced are also called normal forms. In
the following, we characterize the normal forms of the proposed strategy by
means of an inductive definition. Normal forms are of different kinds or
_natures_. For instance, $\lambda x.\,x\,x$ is a normal form of _abstraction_
nature, while $\mathbf{S}({\bf 0})$ is a normal form of _natural number_
nature. The preceding normal forms are intuitively “meaningful”, and they are
said to be _proper_ ; these normal forms are those that can be successfully
typed in a quantitative type system, as we discuss in the next section. In
contrast, there are intuitively “meaningless” normal forms such as
$\mathbf{S}(\lambda x.\,t)$, or ${\bf 0}\,t$, or $\mathsf{if}(\lambda
x.\,t,s,y.\,u)$. These are said to be _stuck_. Stuck normal forms do not have
any meaning, so they cannot be typed in a quantitative type system. We return
to this point in the next section.

Formally, we first distinguish between different _natures_ which will be used
to index the sets of normal forms. Thus, we establish the sets of proper
natures, $\nu\in\\{\mathsf{abs},\mathsf{nat}\\}$ and fallible natures,
$\varepsilon\in\\{\mathsf{abs},\mathsf{nat},\mathsf{stuck}\\}$.

We write $\mathsf{NF}_{\varepsilon}$ to denote the set of normal forms indexed
by a fallible nature $\varepsilon$, which is defined by the following rules:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 24.25372pt\hbox{$\displaystyle\penalty
1\vphantom{{}^{@}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=52.863pt\hbox{\kern
3.00003pt$\texttt{{nf-abs}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\lambda
x.\,t\in\mathsf{NF}_{\mathsf{abs}}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1t\in\mathsf{NF}_{\varepsilon}\hskip
14.22636pts\in\mathsf{NF}_{\varepsilon^{\prime}}\hskip
14.22636pt\varepsilon\neq\mathsf{abs}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=116.46172pt\hbox{\kern
3.00003pt$\texttt{{nf-app}}$}}}\hbox{\kern 35.11877pt\hbox{$\displaystyle
t\,s\in\mathsf{NF}_{\mathsf{stuck}}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.71393pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=33.78342pt\hbox{\kern
3.00003pt$\texttt{{nf-zero}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{\bf
0}\in\mathsf{NF}_{\mathsf{nat}}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 6.66669pt\hbox{$\displaystyle\penalty
1t\in\mathsf{NF}_{\mathsf{nat}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=48.5056pt\hbox{\kern
3.00003pt$\texttt{{nf-succ-nat}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathbf{S}(t)\in\mathsf{NF}_{\mathsf{nat}}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1t\in\mathsf{NF}_{\varepsilon}\hskip
14.22636pt\varepsilon\neq\mathsf{nat}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=73.30644pt\hbox{\kern
3.00003pt$\texttt{{nf-succ-stuck}}$}}}\hbox{\kern
10.05151pt\hbox{$\displaystyle\mathbf{S}(t)\in\mathsf{NF}_{\mathsf{stuck}}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.65099pt\hbox{$\displaystyle\penalty 1t\in\mathsf{NF}_{\varepsilon}\hskip
14.22636pt\varepsilon\neq\mathsf{nat}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=84.60841pt\hbox{\kern
3.00003pt$\texttt{{nf-if}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{if}(t,s,x.\,u)\in\mathsf{NF}_{\mathsf{stuck}}$}}}}\end{array}$

For instance, $\lambda
y.\,\mathtt{id}\,\mathtt{id}\in\mathsf{NF}_{\mathsf{abs}}$ because of rule nf-
abs, while $(\lambda y.\,y\,{\bf 0})\,\mathtt{id}$ is not in normal form since
its left subterm is in normal form but with the proper nature $\mathsf{abs}$.

The results below show that this inductively defined notion of normal form
characterizes exactly the set of irreducible terms. This syntactic
characterization is a key ingredient to show that the quantitative type system
studied in Section 0.3 is sound and complete. We start with a simple
observation regarding the expected form of normal forms based on their
assigned proper natures: lemmaformsnfnatures Let
$t\in\mathsf{NF}_{\varepsilon}$. Then:

  1. 1.

$\varepsilon=\mathsf{abs}$ if and only if $t$ is of the form $\lambda x.\,s$,

  2. 2.

$\varepsilon=\mathsf{nat}$ if and only if $t$ is of the form $\mathbf{k}$.

###### Proof.

See Section .5 for details. ∎

The characterization of normal forms then follows using the previous lemma:
[Characterization of normal forms]propositioncharacterizationNF For any closed
term $t$ the following are equivalent:

  1. 1.

There exists a fallible nature $\varepsilon$ such that
$t\in\mathsf{NF}_{\varepsilon}$.

  2. 2.

$t$ is $\to$-irreducible.

###### Proof.

See Section .5 for details. ∎

Evaluation of applications is non-deterministic, e.g. consider $((\lambda
x.\,\mathbf{S}(x))\,{\bf 0})\,(\mathsf{if}({\bf
0},\mathtt{id},y.\,y\,\mathtt{id}))$. This term reduces in one step to
$\mathbf{S}({\bf 0})\,(\mathsf{if}({\bf 0},\mathtt{id},y.\,y\,\mathtt{id}))$
by rules r-appL and r-beta, and it also reduces in one step to $((\lambda
x.\,\mathbf{S}(x))\,{\bf 0})\,\mathtt{id}$ by rule r-if0. Thus, we need to
ensure that evaluating terms leads to unique normal forms, despite some form
of non-determinism during the computation. To achieve this, we prove the
Diamond Property for the relation $\to$, saying that if a term reduces in one
step to two different terms $t_{1}$ and $t_{2}$, then both terms converge in
one step to the same common reduct. This is a strong form of confluence, which
in particular ensures that all reductions to normal form have the same length:

[Diamond property]propositiondiamond If $t\to_{\rho_{1}}t_{1}$ and
$t\to_{\rho_{2}}t_{2}$ where $t_{1}\neq t_{2}$ then there exists $t^{\prime}$
such that $t_{1}\to_{\rho_{2}}t^{\prime}$ and $t_{2}\to_{\rho_{1}}t^{\prime}$.

###### Proof.

By induction on $t$. Details in Section .5. ∎

Let us take the term of the example above to illustrate this property:

$\textstyle{((\lambda x.\,\mathbf{S}(x))\,{\bf 0})\,(\mathsf{if}({\bf
0},\mathtt{id},y.\,y\,\mathtt{id}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$BI0$\textstyle{\mathbf{S}({\bf
0})\,(\mathsf{if}({\bf
0},\mathtt{id},y.\,y\,\mathtt{id}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$I0$\textstyle{((\lambda
x.\,\mathbf{S}(x))\,{\bf
0})\,\mathtt{id}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$B$\textstyle{\mathbf{S}({\bf
0})\,\mathtt{id}}$

Moreover $\mathbf{S}({\bf 0})\,\mathtt{id}\in\mathsf{NF}_{\mathsf{stuck}}$ by
rule nf-app.

##  0.3 A Quantitative Type System for PCFH

In this section, we introduce system $\mathcal{H}$ (for _hybrid_), a non-
idempotent intersection type system for PCFH. A type derivation for a term in
system $\mathcal{H}$ provides upper bounds for its normalization sequences.
Moreover, by considering only _tight_ typing derivations, we obtain _exact_
bounds. System $\mathcal{H}$ aligns with other formulations of non-idempotent
intersection type systems and satisfies fundamental properties such as Subject
Reduction (Section 0.3.2) and Subject Expansion (Section 0.3.2). Remarkably,
this system captures the combined essence of the two underlying evaluation
strategies found in PCFH, which are CBV and CBN.

The remainder of the section unfolds as follows: Section 0.3.1 defines the set
of types and typing rules governing $\mathcal{H}$. Section 0.3.2 delves into
the proof of soundness and completeness of $\mathcal{H}$ with respect to the
evaluation strategy PCFH. For this, we show two quantitative results: Theorem
6 provides upper bounds for normalization sequences for any kind of type
derivations, while Theorem 6 provides exact bounds for normalization sequences
for those type derivations that are tight.

###  0.3.1 The Type System $\mathcal{H}$

Recall that values in PCFH are either abstractions or natural values of the
form $\mathbf{S}(\mathbf{S}(\ldots\mathbf{S}({\bf 0})))$. A value in PCFH may
be _used_ zero, one, or many times. For example, the underlined identity
function in $(\lambda f.\,f\,(f\,{\bf 0}))\,\underline{\mathtt{id}}$ is used
twice in a reduction to normal form since it is bound to the variable f that
appears twice, and the underlined zero in $(\lambda x.\,\mathsf{if}(x,{\bf
0},y.\,y))\,\underline{{\bf 0}}$ is used exactly once in a reduction to normal
form because it is bound to a single occurrence of $x$ tested for zero
equality.

A noteworthy characteristic of non-idempotent intersection type systems is
their ability to capture the several roles a single expression may play in
different contexts, so in these type systems _terms do not necessarily have a
unique type_. Indeed, in system $\mathcal{H}$, values are given a _multitype_
of the form $\mathcal{T}=[\tau_{1},\ldots,\tau_{n}]^{\nu}$, which consists of
a multiset of types $[\tau_{1},\ldots,\tau_{n}]$ decorated with a nature
$\nu$, and corresponding to the (non-idempotent) intersection
$\tau_{1}\cap\ldots\cap\tau_{n}$. Each $\tau_{i}$ corresponds to one _use_ of
the value. System $\mathcal{H}$ captures the hybrid behavior of PCFH by
splitting the typing information into two parts, called the _typing context_
and the _family context_. The typing context contains typing information for
variables bound by _abstractions_ and _conditional operators_. These variables
behave like in CBV, in the sense that they can only be substituted by _values_
, and thus they are assigned a multitype. The family context contains typing
information for variables bound by _fixed-point operators_. These variables
behave like in CBN, as they can be substituted by _unevaluated expressions_.
Since an unevaluated expression may be copied many times and each copy
produces a value, these variables are assigned a multiset of multitypes
$\mathcal{F}=\\{\\!\\!\\{\mathcal{T}_{1},\ldots,\mathcal{T}_{n}\\}\\!\\!\\}$,
called a _multitype family_.

We note $[\ldots]$ for the multisets of types and
$\\{\\!\\!\\{\ldots\\}\\!\\!\\}$ for the multisets of multitypes. This is just
for visual clarity and to emphasize the different roles they play in the type
system. However, both notations denote multisets, and both behave like non-
idempotent intersections.

Formally, types of $\mathcal{H}$ are given by the following grammar:

$\begin{array}[]{rrclrcl}(\textbf{Types})&\tau&\mathrel{::=}&\mathbb{A}\mid\mathbb{N}\\\
(\textbf{$\mathsf{abs}$-Types})&\mathbb{A}&\mathrel{::=}&\mathcal{T}^{?}\to\mathcal{T}\\\
(\textbf{$\mathsf{nat}$-Types})&\mathbb{N},\mathbb{M},\ldots&\mathrel{::=}&\mathbb{0}\mid\mathbb{S}(\mathcal{N})\\\
(\textbf{Optional
Multitypes})&\mathcal{T}^{?}&\mathrel{::=}&\bot\mid\mathcal{T}\\\
(\textbf{Multitypes})&\mathcal{T},\mathcal{S},\mathcal{U},\mathcal{R},\ldots&\mathrel{::=}&\mathcal{A}\mid\mathcal{N}\\\
(\textbf{$\mathsf{abs}$-Multitypes})&\mathcal{A},\mathcal{B}&\mathrel{::=}&[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in
I}\\\
(\textbf{$\mathsf{nat}$-Multitypes})&\mathcal{N},\mathcal{M},\mathcal{P},\ldots&\mathrel{::=}&[\mathbb{N}_{i}]^{\mathsf{nat}}_{i\in
I}\\\ (\textbf{Multitype
Families})&\mathcal{F}&\mathrel{::=}&\\{\\!\\!\\{\mathcal{T}_{i}\\}\\!\\!\\}_{i\in
I}\end{array}$

A $\nu$-multitype is a multiset of $\nu$-types decorated with a nature $\nu$.
E.g., $[\mathbb{0},\mathbb{0},\mathbb{S}([\,]^{\mathsf{nat}})]$ is a multiset
of $\mathsf{nat}$-types, and
$[\mathbb{0},\mathbb{0},\mathbb{S}([\,]^{\mathsf{nat}})]^{\mathsf{nat}}$ is a
$\mathsf{nat}$-multitype. The decoration is important to distinguish
$[\,]^{\mathsf{nat}}$ from $[\,]^{\mathsf{abs}}$, so that a clear distinction
is made between variables that are bound to natural numbers from those that
are bound to abstractions.

Note that a multitype is either a $\mathsf{nat}$-multitype or an
$\mathsf{abs}$-multitype. A $\nu$-multitype is said to be of nature $\nu$. Two
multitypes are compatible if they are of the same nature. For example,
$[\mathbb{0}]^{\mathsf{nat}}$ is compatible with
$[\mathbb{S}([\,]^{\mathsf{nat}})]^{\mathsf{nat}}$ but not with
$[\mathcal{T}^{?}\to\mathcal{T}]^{\mathsf{abs}}$. This notion is extended to
optional multitypes by declaring that $\mathcal{T}^{?}$ and $\mathcal{S}^{?}$
are compatible if either of them is $\bot$ or if they are compatible
multitypes. The sum of compatible multitypes is defined by
$[\mathbb{A}_{1},\ldots,\mathbb{A}_{n}]^{\mathsf{abs}}+[\mathbb{A}_{n+1},\ldots,\mathbb{A}_{n+m}]^{\mathsf{abs}}=[\mathbb{A}_{1},\ldots,\mathbb{A}_{n+m}]^{\mathsf{abs}}$
and, similarly,
$[\mathbb{N}_{1},\ldots,\mathbb{N}_{n}]^{\mathsf{nat}}+[\mathbb{N}_{n+1},\ldots,\mathbb{N}_{n+m}]^{\mathsf{nat}}=[\mathbb{N}_{1},\ldots,\mathbb{N}_{n+m}]^{\mathsf{nat}}$.
This operation is extended to compatible optional multitypes in the following
way: $\bot+\bot=\bot$ and $\bot+\mathcal{T}=\mathcal{T}$ and
$\mathcal{T}+\bot=\mathcal{T}$. Note that $\bot$ is the neutral element of the
sum.

A family context, written $\Phi,\Psi,\ldots$, is a function mapping variables
to multitype families such that $\Phi(x)\neq\\{\\!\\!\\{\,\\}\\!\\!\\}$ for
finitely many variables $x$. The sum of family contexts is defined by
$(\Phi+\Psi)(x)=\Phi(x)\oplus\Psi(x)$, where $\oplus$ is the sum of multisets
of multitypes, defined as the disjoint union of multisets. The domain of a
family context $\Phi$ is defined as
$\mathsf{dom}(\Phi)\overset{\textrm{def}}{=}\\{x\mid\Phi(x)\neq\\{\\!\\!\\{\,\\}\\!\\!\\}\\}$,
and $\varnothing$ denotes the empty family context, mapping every variable to
$\\{\\!\\!\\{\,\\}\\!\\!\\}$.

A typing context, written $\Gamma,\Delta,\ldots$, is a function mapping
variables to optional multitypes such that $\Gamma(x)\neq\bot$ for finitely
many variables $x$. Two typing contexts $\Gamma,\Delta$ are compatible if
$\Gamma(x)$ and $\Delta(x)$ are compatible for every variable $x$. The sum of
compatible typing contexts is defined by
$(\Gamma+\Delta)(x)=\Gamma(x)+\Delta(x)$. The domain of a typing context
$\Gamma$ is defined as
$\mathsf{dom}(\Gamma)\overset{\textrm{def}}{=}\\{x\mid\Gamma(x)\neq\bot\\}$,
and $\varnothing$ denotes the empty typing context, mapping every variable to
$[\,]$.

A binary relation of subsumption $\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{2}$ is
defined by two cases, stating that $\bot\lhd[\,]^{\nu}$ and
$\mathcal{T}\lhd\mathcal{T}$ hold. Subsumption is used to introduce a
controlled form of weakening in the system (see Example 0.3.1 below).

A multi-counter $\mathfrak{m}$ is a multiset of rule names, whose cardinality
is denoted by $\\#(\mathfrak{m})$. Typing judgments are of the form
$\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$, where $\Phi$ is a family
context, $\Gamma$ is a typing context, $t$ is a term and $\mathcal{T}$ is a
multitype. Moreover, each judgment typing a term $t$ is decorated with a
multi-counter $\mathfrak{m}$, which traces all the rewriting rules that are
used to evaluate the term $t$ to normal form. This means in particular that
$\\#(\mathfrak{m})$ reflects the length of evaluation sequences to normal
form. The decision to use counters that are multisets of rule names instead of
natural numbers is to store more precise information. Moreover, we use a
multiset rather than a 4-uple of distinct counters, as used for example in
[20], to avoid unnecessarily inflating the notation.

As mentioned before, variables can receive two distinct assignments depending
on whether they occur in the family context or the typing context. When a
variable is assigned a multitype family in the family context, it will be
involved in the evaluation of a fixed-point operator, meaning that it is
intended to be substituted by an unevaluated expression, like in CBN. Instead,
when a variable is assigned a multitype in the typing context, it is intended
to be substituted by a value, like in CBV. There is an invariant in
$\mathcal{H}$ stating that family contexts and typing contexts do not share
variables, i.e. $\mathsf{dom}(\Phi)\cap\mathsf{dom}(\Gamma)=\varnothing$. When
studying properties for $\mathcal{H}$ we assume implicitly that this invariant
holds.

Typing rules for the typing system are the following:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.49297pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=56.98593pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{1}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;x:\mathcal{T}\vdash^{[\,]}x:\mathcal{T}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
36.5486pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=73.0972pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{2}$}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
x:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\};\varnothing\vdash^{[\,]}x:\mathcal{T}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 24.77197pt\hbox{$\displaystyle\penalty
1(\Phi_{i};\Gamma_{i},x:\mathcal{T}^{?}_{i}\vdash^{\mathfrak{m}_{i}}t:\mathcal{S}_{i})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=141.7742pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle+_{i\in
I}\Phi_{i};+_{i\in I}\Gamma_{i}\vdash^{+_{i\in I}\mathfrak{m}_{i}}\lambda
x.\,t:[\mathcal{T}^{?}_{i}\to\mathcal{S}_{i}]^{\mathsf{abs}}_{i\in
I}$}}}}\end{array}$ $\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}t:[\mathcal{T}^{?}\to\mathcal{S}]^{\mathsf{abs}}\hskip
14.22636pt\mathcal{T}^{?}\lhd\mathcal{T}\hskip
14.22636pt\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}s:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=188.61572pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
35.25859pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}t\,s:\mathcal{S}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 26.31105pt\hbox{$\displaystyle\penalty
1\vphantom{{}^{@}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=56.97766pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}_{i\in
I}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty
1\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{N}\hskip
14.22636pt\mathcal{N}=+_{i\in I}\mathcal{N}_{i}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=103.41376pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
5.12839pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(t):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$}}}}\end{array}$ $\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 12.46783pt\hbox{$\displaystyle\penalty
1\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}t:[\mathbb{0}]^{\mathsf{nat}}\hskip
14.22636pt\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}s:\mathcal{T}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=159.00497pt\hbox{\kern
3.00003pt$\texttt{{t-ifZero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(t,s,x.\,u):\mathcal{T}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}t:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}\hskip
14.22636pt\mathcal{N}^{?}\lhd\mathcal{N}\hskip
14.22636pt\Phi_{2};\Gamma_{2},x:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{2}}u:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=216.44803pt\hbox{\kern
3.00003pt$\texttt{{t-ifSucc}}$}}}\hbox{\kern
28.56596pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(t,s,x.\,u):\mathcal{T}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Phi,x:\\{\\!\\!\\{\mathcal{T}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma\vdash^{\mathfrak{m}}t:\mathcal{S}\hskip
14.22636pt(\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}_{i}}\mathsf{fix}\,x.\,t:\mathcal{T}_{i})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=200.1038pt\hbox{\kern
3.00003pt$\texttt{{t-fix}}$}}}\hbox{\kern
25.74222pt\hbox{$\displaystyle\Phi+_{i\in I}\Phi_{i};\Gamma+_{i\in
I}\Gamma_{i}\vdash^{[\texttt{F}]+\mathfrak{m}+_{i\in
I}\mathfrak{m}_{i}}\mathsf{fix}\,x.\,t:\mathcal{S}$}}}}\end{array}$

The set $I$ in the typing rules above can be empty. For example, when
$I=\varnothing$ in rule t-abs, we obtain a judgment of the form
$\varnothing;\varnothing\vdash^{[\,]}\lambda x.\,t:[\,]^{\mathsf{abs}}$ with
no premises. As we discussed at the beginning of this subsection, this result
is because the abstraction is not used in the program. When $I=\varnothing$ in
rule t-fix, it means that there are zero uses of the recursive calls in the
program.

Moreover, $I=\varnothing$ in t-succ we may encounter a special case that is
the following:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 6.66669pt\hbox{$\displaystyle\penalty
1\Phi;\Gamma\vdash^{\mathfrak{m}}t:[\,]^{\mathsf{nat}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=72.06094pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(t):[\,]^{\mathsf{nat}}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.15561pt\hbox{$\displaystyle\penalty
1\Phi;\Gamma\vdash^{\mathfrak{m}}t:[\,]^{\mathsf{nat}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=99.03879pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(t):[\mathbb{S}([\,]^{\mathsf{nat}})]^{\mathsf{nat}}$}}}}\end{array}$

Note that there may be several ways to split a $\mathsf{nat}$-multitype
$\mathcal{N}$ into a sum $+_{i\in I}\mathcal{N}_{i}$ of
$\mathsf{nat}$-multitypes $\mathcal{N}_{i}$ in rule t-succ. Therefore, this
rule is non-deterministic when read from top to bottom.

A (typing) derivation is a tree obtained by applying the rules above. We write
$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ when $\pi$ is a
derivation of the judgment $\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$.

As anticipated in the introduction, the hybrid CBN/CBV operational nature of
PCFH is reflected in the quantitative type system. This is apparent by
comparing the typing rules of system $\mathcal{H}$ with the rules of
quantitative type systems for CBN/CBV in the literature. To see this formal
resemblance more clearly, consider for example the CBN quantitative type
system $\mathcal{N}$ and the CBV quantitative type system $\mathcal{V}$, both
described in [20]. Rule t-var1 of $\mathcal{H}$ types variables involved in
CBV computations, aligning with rule var${}^{\mathcal{V}}_{\texttt{c}}$ of
$\mathcal{V}$. Conversely, rule t-var2 types variables involved in CBN
computations, corresponding to rule var${}_{\texttt{c}}$ of $\mathcal{N}$. The
typing rule for abstractions, t-abs, coincides with rule
abs${}^{\mathcal{V}}_{\texttt{c}}$ of $\mathcal{V}$. The multitype in the
conclusion of rule t-abs corresponds to the number of times an abstraction is
_used_ , as in quantitative type systems for CBV [12], rather than to the
number of times the abstraction duplicates its argument, as in quantitative
type systems for CBN [17, 8], reflecting the fact that function applications
in PCFH are evaluated like in CBV. Conversely, in rule t-fix the cardinality
of the multitype family $\\{\\!\\!\\{\mathcal{T}_{i}\\}\\!\\!\\}_{i\in I}$
corresponds intuitively to the number of recursive calls, i.e. to the number
of times that the fixed-point operator duplicates itself, which is similar to
the typing rule of an application in CBN.

The goal of providing PCFH with such system is to characterize normalization
of its evaluation strategy, so, as we briefly mentioned above, the purpose of
multi-counters $\mathfrak{m}$ in $\mathcal{H}$ is to provide _upper bounds_
for the number of evaluation steps to normal form by means of its cardinality.
However, we would also like system $\mathcal{H}$ to go beyond this, by giving
_exact bounds_ , and for that, we make use of special derivations called
_tight_. A multitype is tight if it is of the form $[\,]^{\nu}$. A derivation
$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ is tight if $\Phi$ and
$\Gamma$ are both empty and if the multitype $\mathcal{T}$ is tight.

For example, the following derivation types the term $\lambda x.\,x\,{\bf 0}$:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
73.97728pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=152.31012pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{1}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;x:[[\,]^{\mathsf{nat}}\to[\,]^{\mathsf{abs}}]^{\mathsf{abs}}\vdash^{[\,]}x:[[\,]^{\mathsf{nat}}\to[\,]^{\mathsf{abs}}]^{\mathsf{abs}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}\hskip
14.22636pt\begin{array}[]{c}\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
24.64436pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=53.64429pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\,]^{\mathsf{nat}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=357.30739pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
110.78188pt\hbox{$\displaystyle\varnothing;x:[[\,]^{\mathsf{abs}}\to[\,]^{\mathsf{nat}}]^{\mathsf{abs}}\vdash^{[\texttt{B}]}x\,{\bf
0}:[[\,]^{\mathsf{abs}}]^{\mathsf{abs}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=424.8596pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern
134.97467pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\texttt{B}]}\lambda
x.\,x\,{\bf
0}:[[[\,]^{\mathsf{nat}}\to[\,]^{\mathsf{abs}}]^{\mathsf{abs}}\to[\,]^{\mathsf{abs}}]^{\mathsf{abs}}$}}}}\end{array}$

and the derivation is not tight since the resulting multitype for the term is
not empty. Moreover, the multi-counter is not an exact bound but rather an
upper bound, given that this term is a normal form.

On the other hand, we can also build a _tight_ derivation for the same term,
ending in $\varnothing;\varnothing\vdash^{[\,]}\lambda x.\,x\,{\bf
0}:[\,]^{\mathsf{abs}}$ by rule t-abs with no premises. Furthermore, the
multi-counter here provides an exact bound.

##### Controlled weakening

As mentioned in the introduction, due to their quantitative nature, non-
idempotent intersection type systems are _resource-aware_. In consonance with
this, system $\mathcal{H}$ is _linear_ , hence every single type assumption is
used only once. However, in two specific points a controlled form of
_weakening_ is needed, namely in the t-app and t-ifSucc rules, reflected in
the premises that contain the subsumption relation
$\mathcal{T}^{?}\lhd\mathcal{T}$. This allows a variable to be bound to a
value which is then _discarded_ without being used. Observe that the
subsumption relation $\lhd$ is used for controlling the CBV-like behavior. For
example, in a term like $(\lambda x.\,{\bf 0})\,t$, the argument $t$ must be
fully evaluated to a value before the application can proceed. Since system
$\mathcal{H}$ intends to characterize normalization, this means that $t$ must
be typed to ensure that it is normalizing. If the type of $t$ is $\mathcal{T}$
then, in principle, $x$ should also be of type $\mathcal{T}$. But by
linearity, ${\bf 0}$ is only typable under the empty typing contexts. Assuming
that $t$ is a closed term of type $[\,]^{\mathsf{nat}}$, a type derivation can
be given as follows:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
35.002pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=74.35956pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing,x:\bot\vdash^{[\,]}{\bf
0}:[\,]^{\mathsf{nat}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=143.60619pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern
21.53555pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}\lambda
x.\,{\bf 0}:[\bot\to[\,]^{\mathsf{nat}}]^{\mathsf{abs}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}\hskip 14.22636pt\bot\lhd[\,]^{\mathsf{nat}}\hskip
14.22636pt\begin{array}[]{c}\vdots\\\
\varnothing;\varnothing\vdash^{\mathfrak{m}}t:[\,]^{\mathsf{nat}}\end{array}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=328.56664pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
114.8869pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\texttt{B}]+\mathfrak{m}}(\lambda
x.\,{\bf 0})\,t:[\,]^{\mathsf{nat}}$}}}}\end{array}$

Note that $\bot\lhd[\,]^{\mathsf{nat}}$ implies the hypothesis $x:\bot$
appears on the typing judgment of ${\bf 0}$, while it forces the argument $t$
on the right premise to be typable. Also, recall that $\varnothing,x:\bot$ is
equal to $\varnothing$.

Let us now give an example of a type derivation for fixed-point operators, so
let $t:=(\mathsf{fix}\,f.\,\lambda n.\,\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))))\,\mathbf{S}({\bf 0})$, where the left
subterm is a function returning the double of any natural number: e.g. $t$
computes the double of $\mathbf{S}(\mathbf{S}({\bf 0}))$. Let
$\mathcal{N}:=[\mathbb{S}([\mathbb{0}]^{\mathsf{nat}})]^{\mathsf{nat}}$,
$\mathcal{M}:=[\mathbb{0}]^{\mathsf{nat}}$,
$\mathcal{A}:=[\mathcal{N}\to[\,]^{\mathsf{nat}}]^{\mathsf{abs}}$ and
$\mathcal{B}:=[\mathcal{M}\to[\,]^{\mathsf{nat}}]^{\mathsf{abs}}$.

A tight type derivation for $t$ follows:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.60637pt\hbox{$\displaystyle\penalty
1\pi_{\text{rec1}}\hskip 14.22636pt\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.1833pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=44.72217pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:\mathcal{M}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\end{array}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=113.9688pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
27.40111pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}\mathbf{S}({\bf
0}):\mathcal{N}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\end{array}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=242.90924pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\texttt{B},\texttt{F},\texttt{IS},\texttt{B},\texttt{F},\texttt{I0}]}(\mathsf{fix}\,f.\,\lambda
n.\,\mathsf{if}(n,{\bf 0},m.\,\mathbf{S}(\mathbf{S}(f\,m))))\,\mathbf{S}({\bf
0}):[\,]^{\mathsf{nat}}$}}}}\end{array}$

Note that the argument $\mathbf{S}({\bf 0})$ is typed with the singleton
$\mathsf{nat}$-multitype $\mathcal{N}$. This reflects the single use of
$\mathbf{S}({\bf 0})$, as it corresponds to a single occurrence of $n$ tested
for zero equality. Moreover, its subterm ${\bf 0}$ is assigned the singleton
$\mathsf{nat}$-multitype $\mathcal{M}$, since it is bound to a single
occurrence of $n$ which is also tested for zero equality in the base case of
the recursive function.

The typing derivation for the left subterm (the fixed-point operator) follows:

$\centering\pi_{\text{rec1}}:=\left(\scalebox{0.87}{
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.67415pt\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
29.05783pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=58.11566pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{1}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;n:\mathcal{N}\vdash^{[\,]}n:\mathcal{N}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}\hskip
14.22636pt\pi_{\text{cond}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=188.78172pt\hbox{\kern
3.00003pt$\texttt{{t-ifSucc}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
f:\\{\\!\\!\\{\mathcal{B}\\}\\!\\!\\};n:\mathcal{N}\vdash^{[\texttt{IS},\texttt{B}]}\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))):[\,]^{\mathsf{nat}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=266.05617pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern 40.59831pt\hbox{$\displaystyle
f:\\{\\!\\!\\{\mathcal{B}\\}\\!\\!\\};\varnothing\vdash^{[\texttt{IS},\texttt{B}]}\lambda
n.\,\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))):\mathcal{A}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}\pi_{\text{rec2}}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=347.66864pt\hbox{\kern
3.00003pt$\texttt{{t-fix}}$}}}\hbox{\kern
74.32413pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\texttt{F},\texttt{IS},\texttt{B},\texttt{F},\texttt{I0}]}\mathsf{fix}\,f.\,\lambda
n.\,\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))):\mathcal{A}$}}}}\end{array}$
}\right)\@add@centering$

on which the function $\lambda n.\,\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m)))$ must be typed considering that $n$ shall
be bound to $\mathbf{S}({\bf 0})$, so that $n$ is of type $\mathcal{N}$.
Moreover, $f$ is bound to the result of the recursive call, typed in
$\pi_{\text{rec2}}$:

$\pi_{\text{rec2}}:=\left(\scalebox{0.82}{
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.54672pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.449pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{1}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;n:\mathcal{M}\vdash^{[\,]}n:\mathcal{M}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
24.64436pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=53.64429pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\,]^{\mathsf{nat}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=252.21991pt\hbox{\kern
3.00003pt$\texttt{{t-ifZero}}$}}}\hbox{\kern
47.27478pt\hbox{$\displaystyle\varnothing;n:\mathcal{M}\vdash^{[\texttt{I0}]}\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))):[\,]^{\mathsf{nat}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=328.96657pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern
88.65085pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\texttt{I0}]}\lambda
n.\,\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))):\mathcal{B}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=394.90765pt\hbox{\kern
3.00003pt$\texttt{{t-fix}}$}}}\hbox{\kern
106.86308pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\texttt{F},\texttt{I0}]}\mathsf{fix}\,f.\,\lambda
n.\,\mathsf{if}(n,{\bf
0},m.\,\mathbf{S}(\mathbf{S}(f\,m))):\mathcal{B}$}}}}\end{array}$ }\right)$

This derivation is the one in charge of typing the base case, hence $\lambda
n.\,\mathsf{if}(n,{\bf 0},m.\,\mathbf{S}(\mathbf{S}(f\,m)))$ is typed
considering that $n$ is bound to ${\bf 0}$, so that $n$ is of type
$\mathcal{M}$. Since $\pi_{\text{rec2}}$ corresponds to a base case, there are
no right premises in the rule t-fix.

We finish with the derivation of the _else_ branch of the conditional:

$\centering\pi_{\text{cond}}:=\left(\scalebox{0.79}{
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
34.48894pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=73.33344pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{2}$}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
f:\\{\\!\\!\\{\mathcal{B}\\}\\!\\!\\};\varnothing\vdash^{[\,]}f:\mathcal{B}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
31.32451pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.00458pt\hbox{\kern
3.00003pt$\texttt{{t-var${}_{1}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;m:\mathcal{M}\vdash^{[\,]}m:\mathcal{M}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=276.09799pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern 81.47719pt\hbox{$\displaystyle
f:\\{\\!\\!\\{\mathcal{B}\\}\\!\\!\\};m:\mathcal{M}\vdash^{[\texttt{B}]}f\,m:[\,]^{\mathsf{nat}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=343.6502pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern 108.58661pt\hbox{$\displaystyle
f:\\{\\!\\!\\{\mathcal{B}\\}\\!\\!\\};m:\mathcal{M}\vdash^{[\texttt{B}]}\mathbf{S}(f\,m):[\,]^{\mathsf{nat}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=413.48016pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern 136.8349pt\hbox{$\displaystyle
f:\\{\\!\\!\\{\mathcal{B}\\}\\!\\!\\};m:\mathcal{M}\vdash^{[\texttt{B}]}\mathbf{S}(\mathbf{S}(f\,m)):[\,]^{\mathsf{nat}}$}}}}\end{array}$
}\right)\@add@centering$

here, the term $\mathbf{S}(\mathbf{S}(f\,m))$ represents the result of
doubling $\mathbf{S}({\bf 0})$, which is the normal form of $t$. As the normal
form is not “used” in any way (i.e. there are no further interactions with the
environment), it is typed with $[\,]^{\mathsf{nat}}$.

###  0.3.2 Properties of $\mathcal{H}$

This subsection develops the meta-theory of system $\mathcal{H}$ and proves
the main results of this work. We begin by studying basic properties of the
typing system, such as relevance and splitting lemmas. Then, we state
auxiliary lemmas to prove soundness for system $\mathcal{H}$, as well as
auxiliary lemmas to prove completeness.

A first remark states that a natural number must be typed with a
$\mathsf{nat}$-multitype:

######  Remark 1.

If $\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{k}:\mathcal{T}$, then
$\mathcal{T}$ is of the form $\mathcal{N}$.

Recall that System $\mathcal{H}$ is linear so, in particular, all assumptions
are used. This property is known as _relevance_ :

######  Lemma 2 (Relevance).

If $\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ then
$\mathsf{dom}(\Phi)\cup\mathsf{dom}(\Gamma)\subseteq\mathsf{fv}(t)$.

###### Proof.

The proof is straightforward by induction on $\pi$. ∎

The next lemma establishes the equivalence between two different conditions
regarding the typability of a value. Specifically, it states that a value is
typable with a family context, a typing context, and a multi-counter that are
empty if and only if it is typed with an empty $\nu$-multiset, for any proper
nature $\nu$.

######  Lemma 3.

Let $\mathbf{v}$ be a value. Then the following are equivalent:

  1. 1.

$\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{v}:[\,]^{\nu}$, where
$\nu=\mathsf{abs}$ if $\mathbf{v}$ is an abstraction, and $\nu=\mathsf{nat}$
if $\mathbf{v}=\mathbf{k}$

  2. 2.

$\Phi=\varnothing$, $\Gamma=\varnothing$ and $\mathfrak{m}=[\,]$

###### Proof.

We prove both items by induction on $\mathbf{v}$. Cases $\mathbf{v}=\lambda
x.\,t$ and $\mathbf{v}={\bf 0}$ are trivial. Case
$\mathbf{v}=\mathbf{S}(\mathbf{l})$ is straightforward using the IH. ∎

The following property establishes a form of stability of the subsumption
relation concerning the sum operator. [Multitype Splitting
Lemma]lemmamultitypesplitting The following hold:

  1. 1.

If $\bot\lhd\mathcal{T}$ then $\mathcal{T}$ is of the form $[\,]^{\nu}$ for
some proper nature $\nu$.

  2. 2.

$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd\mathcal{T}$ if and only if there
exist multitypes $\mathcal{T}_{1},\mathcal{T}_{2}$ such that
$\mathcal{T}=\mathcal{T}_{1}+\mathcal{T}_{2}$ and
$\mathcal{T}^{?}_{i}\lhd\mathcal{T}_{i}$ for all $i\in\\{1,2\\}$.

  3. 3.

$+_{i\in I}\mathcal{T}^{?}_{i}\lhd\mathcal{T}$ if and only if either $I$ is
empty and $\mathcal{T}=[\,]^{\nu}$ for some proper nature $\nu$, or $I$ is
non-empty and there exist multitypes $(\mathcal{T}_{i})_{i\in I}$ such that
$\mathcal{T}=+_{i\in I}\mathcal{T}_{i}$ and
$\mathcal{T}^{?}_{i}\lhd\mathcal{T}_{i}$ for all ${i\in I}$.

The . ‣ Properties of $\mathcal{H}$ is used to split and merge the type
derivation of values:

######  Lemma 4 (Generalized Value Splitting / Merging).

Let $I$ be a finite set, $(\mathcal{T}^{?}_{i})_{i\in I}$ a family of optional
multitypes and $(\mathcal{F}_{i})_{i\in I}$ a family of multitype families.
Then the following are equivalent:

  1. 1.

$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{v}:\mathcal{T}$ with
$\mathcal{T}$ a multitype such that $+_{i\in
I}\mathcal{T}^{?}_{i}\lhd\mathcal{T}$

  2. 2.

There exist family contexts $(\Phi_{i})_{i\in I}$, typing contexts
$(\Gamma_{i})_{i\in I}$, multi-counters $(\mathfrak{m}_{i})_{i\in I}$ and
multitypes $(\mathcal{T}_{i})_{i\in I}$ such that $\Phi=+_{i\in I}\Phi_{i}$
and $\Gamma=+_{i\in I}\Gamma_{i}$ and $\mathfrak{m}=+_{i\in
I}\mathfrak{m}_{i}$ and
$\pi_{i}\rhd\Phi_{i};\Gamma_{i}\vdash\mathbf{v}:\mathcal{T}_{i}$ and
$\mathcal{T}^{?}_{i}\lhd\mathcal{T}_{i}$ for all ${i\in I}$.

###### Proof.

The proof is straightforward by induction on the cardinality of $I$, using
Lemma 7. ∎

#### Lemmas for Soundness

To show that the type system $\mathcal{H}$ is sound, we follow well-known
techniques for non-idempotent types (see [7, 2]). First, a Subject Reduction
lemma is established, which is in turn based on two substitution lemmas: one
for each kind of substitution that PCFH has.

[Value Substitution Lemma]lemmavaluesubstitution Let
$\zeta\rhd\Psi;\Delta\vdash^{\mathfrak{n}}\mathbf{v}:\mathcal{S}$ and let
$\mathcal{S}^{?}$ be such that $\mathcal{S}^{?}\lhd\mathcal{S}$. If
$\pi\rhd\Phi;\Gamma,x:\mathcal{S}^{?}\vdash^{\mathfrak{m}}t:\mathcal{T}$ then
there exists a derivation $\pi^{\prime}$ such that
$\pi^{\prime}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}t\\{x:=\mathbf{v}\\}:\mathcal{T}$.

[Substitution Lemma]lemmasubstitution Let $I$ be a finite set, and
$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I}$ a family of type derivations. If
$\pi\rhd\Phi,x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ then there exists a derivation
$\pi^{\prime}$ such that $\pi^{\prime}\rhd\Phi+_{i\in I}\Psi_{i};\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in
I}\mathfrak{n}_{i}}t\\{x:=q\\}:\mathcal{T}$.

Both substitution lemmas are proved by induction on $\pi$. Details are in
Section .6.

Now we move to Subject Reduction, which gives preservation of types. Moreover,
it also provides quantitative information in the sense that the multi-counter
for typing $t^{\prime}$ is smaller than the multi-counter for typing $t$, by
exactly one element.

[Subject Reduction]lemmasubjectreduction Let $t$ be such that
$t\to_{\rho}t^{\prime}$ and
$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$. Then there exist a
derivation $\pi^{\prime}$ and a multi-counter $\mathfrak{m}^{\prime}$ such
that $[\rho]+\mathfrak{m}^{\prime}=\mathfrak{m}$ and
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}t^{\prime}:\mathcal{T}$.

###### Proof.

By induction on the derivation of $t\to_{\rho}t^{\prime}$. We show only cases
r-beta and r-fix to see how the substitution lemmas are applied; the remaining
cases are in Section .6.

  * •

r-beta. Then $t=(\lambda
x.\,s)\,\mathbf{v}\to_{\texttt{B}}s\\{x:=\mathbf{v}\\}=t^{\prime}$. The
conclusion of $\pi$ can then only be derived using rule t-app, so $\pi$ has
the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.44878pt\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}s:\mathcal{T}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=100.67267pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\lambda
x.\,s:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}(1)\ \mathcal{S}^{?}\lhd\mathcal{S}\hskip
14.22636pt\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=288.15718pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
72.03276pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}(\lambda
x.\,s)\,\mathbf{v}:\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$. Given (1), we
can apply Section 0.3.2 to $\pi_{1}$ with $\pi_{2}$, yielding
$\pi^{\prime}\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{\mathfrak{m}_{1}+\mathfrak{m}_{2}}s\\{x:=\mathbf{v}\\}:\mathcal{T}$,
and we conclude with
$\mathfrak{m}^{\prime}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$, since
$[\texttt{B}]+\mathfrak{m}^{\prime}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}=\mathfrak{m}$.

  * •

t-fix. Then
$t=\mathsf{fix}\,x.\,s\to_{\rho}s\\{x:=\mathsf{fix}\,x.\,s\\}=t^{\prime}$. The
conclusion of $\pi$ can then only be derived by rule t-fix, so $\pi$ has the
form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{0}\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}s:\mathcal{T}\hskip
14.22636pt(\pi_{i}\rhd\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}_{i}}\mathsf{fix}\,x.\,s:\mathcal{S}_{i})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=241.14198pt\hbox{\kern
3.00003pt$\texttt{{t-fix}}$}}}\hbox{\kern
43.51196pt\hbox{$\displaystyle\Phi_{0}+_{i\in I}\Phi_{i};\Gamma_{0}+_{i\in
I}\Gamma_{i}\vdash^{[\texttt{F}]+\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}}\mathsf{fix}\,x.\,s:\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{0}+_{i\in I}\Phi_{i}$ and $\Gamma=\Gamma_{0}+_{i\in
I}\Gamma_{i}$ and $\mathfrak{m}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{m}_{i}$.
By Section 0.3.2 on $\pi_{0}$ with $(\pi_{i})_{i\in I}$ we obtain
$\pi^{\prime}\rhd\Phi_{0}+_{i\in I}\Phi_{i};\Gamma_{0}+_{i\in
I}\Gamma_{i}\vdash^{\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}}s\\{x:=\mathsf{fix}\,x.\,s\\}:\mathcal{T}$. We let
$\mathfrak{m}^{\prime}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{m}_{i}$ and we
conclude since
$[\texttt{F}]+\mathfrak{m}^{\prime}=[\texttt{F}]+\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}=\mathfrak{m}$. ∎

#### Lemmas for Completeness

To show that the type system $\mathcal{H}$ is complete, the procedure is
analogous to the one to prove soundness. First, a Subject Expansion lemma is
required, which is in turn based on two anti-substitution lemmas: one for each
kind of substitution that PCFH has.

[Value Anti-Substitution]lemmavalueantisubstitution Let
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}t\\{x:=\mathbf{v}\\}:\mathcal{T}$.
Then there exist family contexts $\Phi_{1}$, $\Phi_{2}$, typing contexts
$\Gamma_{1}$, $\Gamma_{2}$, multi-counters $\mathfrak{m}_{1}$,
$\mathfrak{m}_{2}$, an optional multitype $\mathcal{S}^{?}$ and a multitype
$\mathcal{S}$ satisfying:

  1. 1.

$\pi\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}t:\mathcal{T}$

  2. 2.

$\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$

  3. 3.

$\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$\mathcal{S}^{?}\lhd\mathcal{S}$

[Anti-Substitution]lemmaantisubstitution Let
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}t\\{x:=q\\}:\mathcal{T}$.
Then there exist a finite set $I$, family contexts $\Phi_{0}$,
$(\Psi_{i})_{i\in I}$, typing contexts $\Gamma_{0}$, $(\Delta_{i})_{i\in I}$,
multi-counters $\mathfrak{m}_{0}$, $(\mathfrak{n}_{i})_{i\in I}$ and
multitypes $(\mathcal{S}_{i})_{i\in I}$ satisfying:

  1. 1.

$\pi\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}t:\mathcal{T}$

  2. 2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I}$

  3. 3.

$\Phi=\Phi_{0}+_{i\in I}\Psi_{i}$ and $\Gamma=\Gamma_{0}+_{i\in I}\Delta_{i}$
and $\mathfrak{m}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{n}_{i}$

Both anti-substitution lemmas are proved by induction on $\pi$. Details are in
Section .6.

We can proceed now to show Subject Expansion, which is analogous to Subject
Reduction in Section 0.3.2. However, it goes in the opposite direction of the
reduction relation $t\to_{\rho}t^{\prime}$: given a type derivation of
$t^{\prime}$, it proves that $t$ has the same type as $t^{\prime}$.

[Subject Expansion]lemmasubjectexpansion Let $t\to_{\rho}t^{\prime}$ and
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}t^{\prime}:\mathcal{T}$.
Then there exist a derivation $\pi$ and a multi-counter $\mathfrak{m}$ such
that $\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$ and
$\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$.

###### Proof.

By induction on the derivation of $t\to_{\rho}t^{\prime}$. Details are in
Section .6. ∎

Furthermore, to prove completeness (i.e. normalization implies typability) it
is necessary to show that non-stuck normal forms are typable. As stated in
Section 0.2, the focus is only on proper normal forms since the stuck ones do
not have any meaning, i.e. they represent computation errors that type systems
such as $\mathcal{H}$ do not capture. [Normal Forms are Typable]lemmaNFtypable
Let $t\in\mathsf{NF}_{\nu}$ with $\nu$ a proper nature. Then
$\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ for some
$\mathfrak{m},\Phi,\Gamma,\mathcal{T}$.

###### Proof.

See Section .6 for details. ∎

We can even state a stronger result than the previous one, namely that proper
normal forms can be obtained from a _tight_ derivation. Moreover, the multi-
counter of such tight derivations is empty, which is crucial to obtain exact
bounds by tight type derivations:

######  Lemma 5 (Normal Forms are Tight Typable).

Let $t\in\mathsf{NF}_{\nu}$ with $\nu$ a proper nature. Then
$\varnothing;\varnothing\vdash^{[\,]}t:[\,]^{\nu}$.

###### Proof.

By induction on the derivation of $t\in\mathsf{NF}_{\nu}$. Recall cases nf-
app, nf-succ-stuck and nf-if do not apply since $\mathsf{stuck}$ is not a
proper nature.

  1. 1.

nf-abs. Then $t=\lambda x.\,s\in\mathsf{NF}_{\mathsf{abs}}$ and indeed
$\varnothing;\varnothing\vdash^{[\,]}\lambda x.\,s:[\,]^{\mathsf{abs}}$ by
t-abs.

  2. 2.

nf-zero. Then $t={\bf 0}\in\mathsf{NF}_{\mathsf{nat}}$ and indeed
$\varnothing;\varnothing\vdash^{[\,]}{\bf 0}:[\,]^{\mathsf{nat}}$ by t-zero.

  3. 3.

nf-succ-nat. Then $t=\mathbf{S}(s)\in\mathsf{NF}_{\mathsf{nat}}$ where
$s\in\mathsf{NF}_{\mathsf{nat}}$. By IH on $s\in\mathsf{NF}_{\mathsf{nat}}$,
$\varnothing;\varnothing\vdash^{[\,]}s:[\,]^{\mathsf{nat}}$, hence
$\varnothing;\varnothing\vdash^{[\,]}\mathbf{S}(s):[\,]^{\mathsf{nat}}$ by
applying t-succ. ∎

#### Soundness and Completeness of System $\mathcal{H}$

We now turn to the main results of this paper, which are the properties of
soundness and completeness of $\mathcal{H}$. Both properties give an
equivalence between typability and normalization. The following theorem
provides upper bounds for normalization sequences of a given term, for which
no tightness condition is required:

######  Theorem 6 (Soundness and Completeness of System $\mathcal{H}$ with
Upper Bounds).

Let $t$ be a closed term, and $\nu$ be a proper nature. The following are
equivalent:

  1. 1.

$\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$

  2. 2.

There exists a sequence of steps
$t=t_{0}\to_{\rho_{1}}t_{1}\ldots\to_{\rho_{n}}t_{n}$ where
$t_{n}\in\mathsf{NF}_{\nu}$ and
$\\#(\mathfrak{m})\geq\\#([\rho_{1},\ldots,\rho_{n}])$.

###### Proof.

($1\Rightarrow 2$) By induction on the size of $\mathfrak{m}$, analyzing
whether $t\in\mathsf{NF}_{\nu}$ or not.

  * •

If $t\in\mathsf{NF}_{\nu}$, then $t$ is of the form $\lambda x.\,s$, ${\bf
0}$, or $\mathbf{S}(\mathbf{k})$, since $\nu$ is a proper nature. Hence $t$
can only be derived by rule t-abs, t-zero, or t-succ respectively. In the
three cases, we can take the empty evaluation sequence and we are done.

  * •

If $t\notin\mathsf{NF}_{\nu}$. Then by Section 0.2 it must exist a term
$t^{\prime}$ and a rule name $\rho$ such that $t\to_{\rho}t^{\prime}$. By
Lemmas for Soundness there exists $\mathfrak{m}^{\prime}$ such that
$\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$, and
$\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}t^{\prime}:\mathcal{T}$. By IH on
$\mathfrak{m}^{\prime}$, there exists a sequence of steps
$t^{\prime}\to_{\rho_{1}}t_{1}\ldots\to_{\rho_{n}}t_{n}$ where
$t_{n}\in\mathsf{NF}_{\nu}$ and
$\\#(\mathfrak{m}^{\prime})\geq\\#([\rho_{1},\ldots,\rho_{n}])$. By joining
this sequence with the step $t\to_{\rho}t^{\prime}$ we obtain the sequence
$t\to_{\rho}t^{\prime}\to_{\rho_{1}}t_{1}\ldots\to_{\rho_{n}}t_{n}$, where
$\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$, and therefore
$\\#(\mathfrak{m})\geq\\#([\rho,\rho_{1},\ldots,\rho_{n}])$.

($2\Rightarrow 1$) By induction on $n$.

  1. 1.

$n=0$. Then $t\in\mathsf{NF}_{\nu}$, and we conclude with
$\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ by Section 0.3.2.

  2. 2.

$n>0$, assuming the property holds for $n-1$. Taking the reduction sequence of
$(n-1)$ steps from $t_{1}$ to $t_{n}$, and
$\\#(\mathfrak{m}^{\prime})\geq\\#([\rho_{2},\ldots,\rho_{n}])$ we can apply
the IH, yielding $\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}t_{1}:\mathcal{T}$.
Since $t\to_{\rho_{1}}t_{1}$, then
$\Phi;\Gamma\vdash^{\mathfrak{m}}t:\mathcal{T}$ by Lemmas for Completeness,
with $\mathfrak{m}=[\rho_{1}]+\mathfrak{m}^{\prime}$, so we conclude with
$\\#(\mathfrak{m})\geq\\#([\rho_{1},\rho_{2},\ldots,\rho_{n}])$. ∎

Soundness and completeness of system $\mathcal{H}$ restricting type
derivations to tight ones provide exact bounds for normalization sequences of
a given term:

[Tight Soundness and Completeness of System
$\mathcal{H}$]theoremtightsoundnesscompleteness Let $t$ be a closed term, and
$\nu$ be a proper nature. The following are equivalent:

  1. 1.

$\varnothing;\varnothing\vdash^{\mathfrak{m}}t:[\,]^{\nu}$ with $\pi$ a tight
derivation

  2. 2.

There exists a sequence of steps
$t=t_{0}\to_{\rho_{1}}t_{1}\ldots\to_{\rho_{n}}t_{n}$ where
$t_{n}\in\mathsf{NF}_{\nu}$ and $\mathfrak{m}=[\rho_{1},\ldots,\rho_{n}]$.

###### Proof.

Follows the same structure as in Theorem 6, mutatis mutandis. The full proof
is in Section .6.

To prove soundness $(1\Rightarrow 2)$, in the case where
$t\in\mathsf{NF}_{\nu}$, we know that $t$ must be a value, hence the typing
derivation $\varnothing;\varnothing\vdash^{\mathfrak{m}}t:[\,]^{\nu}$ of the
hypothesis must be such that $\mathfrak{m}=[\,]$ by Lemma 3. To prove
completeness $(2\Rightarrow 1)$, we resort to the stronger Lemma 5, rather
than just to Section 0.3.2, to ensure that we can construct a typing
derivation of the form $\varnothing;\varnothing\vdash^{[\,]}t:[\,]^{\nu}$. ∎

##  0.4 Conclusions

This paper proposes a quantitative study of a hybrid evaluation strategy for
PCF, called PCFH, without relying on any encoding of natural numbers or fixed-
point operators.

Our key contribution is a quantitative semantics for PCFH, by means of a non-
idempotent intersection type system called $\mathcal{H}$, which is sound and
complete with respect to the strategy. System $\mathcal{H}$ highlights the
hybrid nature of the PCFH semantics, in the sense that CBN and CBV
quantitative behaviors coexist within the same framework. Moreover, not only
$\mathcal{H}$ provides upper bounds for the length of normalization sequences
to normal form, but we also achieve exact bounds by refining the typing
derivations of $\mathcal{H}$ to those that are _tight_.

Frameworks such as CBPV or the _Bang Calculus_ are able to _encode_ both CBN
and CBV cohesively, by distinguishing _values_ from _computations_ , instead
of exhibiting explicitly the hybrid behavior they have. Therefore, it would be
worth studying whether PCFH can be embedded into such calculi.

An interesting question is whether the quantitative information of other
hybrid settings can be expressed using type systems such as $\mathcal{H}$.
Another question for future work is the study of the inhabitation problem in a
hybrid-type setting, which we conjecture to be decidable, given that it was
already proven to be decidable in CBN [6], CBV, and CBPV [4].

## References

  * [1] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria.  Full abstraction for PCF.  Inf. Comput., 163(2):409–470, 2000.
  * [2] Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner.  Tight typings and split bounds, fully developed.  J. Funct. Program., 30:e14, 2020.
  * [3] Beniamino Accattoli and Giulio Guerrieri.  Types of fireballs.  In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 45–66. Springer, 2018.
  * [4] Victor Arrial, Giulio Guerrieri, and Delia Kesner.  Quantitative inhabitation for different lambda calculi in a unifying framework.  Proc. ACM Program. Lang., 7(POPL):1483–1513, 2023.
  * [5] Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso.  The bang calculus revisited.  Inf. Comput., 293:105047, 2023.
  * [6] Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca.  The inhabitation problem for non-idempotent intersection types.  In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 341–354. Springer, 2014.
  * [7] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura.  Non-idempotent intersection types for the lambda-calculus.  Log. J. IGPL, 25(4):431–464, 2017.
  * [8] Daniel de Carvalho.  Sémantiques de la logique linéaire et temps de calcul.  PhD thesis, Ecole Doctorale Physique et Sciences de la Matière (Marseille), 2007.
  * [9] Mario Coppo and Mariangiola Dezani-Ciancaglini.  An extension of the basic functionality theory for the $\lambda$-calculus.  Notre Dame J. Formal Log., 21(4):685–693, 1980.
  * [10] Daniel de Carvalho.  Execution time of lambda-terms via denotational semantics and intersection types.  CoRR, abs/0905.4251, 2009.
  * [11] Gilles Dowek and Jean-Jacques Lévy.  Introduction to the Theory of Programming Languages.  Undergraduate Topics in Computer Science. Springer, 2011.
  * [12] Thomas Ehrhard.  Collapsing non-idempotent intersection types.  In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 259–273. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012.
  * [13] Thomas Ehrhard.  Call-by-push-value from a linear logic point of view.  In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 202–228. Springer, 2016.
  * [14] Thomas Ehrhard.  A coherent differential PCF.  Log. Methods Comput. Sci., 19(4), 2023.
  * [15] Thomas Ehrhard and Giulio Guerrieri.  The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value.  In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 174–187. ACM, 2016.
  * [16] Thomas Ehrhard, Michele Pagani, and Christine Tasson.  Full abstraction for probabilistic PCF.  J. ACM, 65(4):23:1–23:44, 2018.
  * [17] Philippa Gardner.  Discovering needed reductions using type theory.  In Theoretical Aspects of Computer Software, pages 555–574. Springer, 1994.
  * [18] Jean-Yves Girard.  Linear logic.  Theor. Comput. Sci., 50:1–102, 1987.
  * [19] Kohei Honda and Nobuko Yoshida.  Game-theoretic analysis of call-by-value computation.  Theor. Comput. Sci., 221(1-2):393–456, 1999.
  * [20] Delia Kesner and Andrés Viso.  Encoding tight typing in a unified framework.  In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 27:1–27:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022\.
  * [21] Paul Blain Levy.  Call-by-push-value: A subsuming paradigm.  In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA’99, L’Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 228–242. Springer, 1999.
  * [22] Robin Milner.  Fully abstract models of typed _lambda_ -calculi.  Theor. Comput. Sci., 4(1):1–22, 1977.
  * [23] Gordon D. Plotkin.  Call-by-name, call-by-value and the lambda-calculus.  Theor. Comput. Sci., 1(2):125–159, 1975.
  * [24] Gordon D. Plotkin.  LCF considered as a programming language.  Theor. Comput. Sci., 5(3):223–255, 1977.

## Technical Appendix

##  .5 Omitted proofs of Section 0.2

*

###### Proof.

By induction on the derivation of the judgment
$t\in\mathsf{NF}_{\varepsilon}$.

  * •

nf-abs. Then $t=\lambda x.\,s\in\mathsf{NF}_{\mathsf{abs}}$, where
$\varepsilon=\mathsf{abs}$. This case checks item 1.

  * •

nf-app. Then $t=s\,u\in\mathsf{NF}_{\mathsf{stuck}}$, where
$\varepsilon=\mathsf{stuck}$. This case trivially holds since $t$ is not an
abstraction nor $\mathbf{k}$, and also
$\varepsilon\notin\\{\mathsf{abs},\mathsf{nat}\\}$.

  * •

nf-zero. Then $t={\bf 0}\in\mathsf{NF}_{\mathsf{nat}}$, where
$\varepsilon=\mathsf{nat}$. This case checks item 2.

  * •

nf-succ-nat. Then $t=\mathbf{S}(s)\in\mathsf{NF}_{\mathsf{nat}}$, where
$\varepsilon=\mathsf{nat}$, and it is derived from
$s\in\mathsf{NF}_{\mathsf{nat}}$. Then $s$ is of the form $\mathbf{k}$ by the
IH on $s$. Hence by definition, this case checks item 2.

  * •

nf-succ-stuck. Then $t=\mathbf{S}(s)\in\mathsf{NF}_{\mathsf{stuck}}$, where
$\varepsilon=\mathsf{stuck}$, and it is derived from
$s\in\mathsf{NF}_{\varepsilon^{\prime}}$,
$\varepsilon^{\prime}\neq\mathsf{nat}$. By the IH on $s$, $s$ is not of the
form $\mathbf{k}$. Hence by definition, $\mathbf{S}(s)$ is not an abstraction
nor a $\mathbf{k}$, so this case also holds.

  * •

nf-if. Then $t=\mathsf{if}(s,u,x.\,r)\in\mathsf{NF}_{\mathsf{stuck}}$, where
$\varepsilon=\mathsf{stuck}$. This case trivially holds since
$\varepsilon\notin\\{\mathsf{abs},\mathsf{nat}\\}$ and $t$ is not an
abstraction nor of the form $\mathbf{k}$.

∎

*

###### Proof.

$1\Rightarrow 2)$ By induction on the derivation of the judgment
$t\in\mathsf{NF}_{\varepsilon}$. Note that cases nf-abs and nf-zero are
immediate since there are no rules for reducing abstractions or zero.

  * •

nf-app. Then $t=s\,u\in\mathsf{NF}_{\mathsf{stuck}}$ is derived from
$s\in\mathsf{NF}_{\varepsilon}$ and $u\in\mathsf{NF}_{\varepsilon^{\prime}}$,
with $\varepsilon\neq\mathsf{abs}$. Hence $s$ is $\to$-irreducible by IH on
$s$, and $u$ is $\to$-irreducible by IH on $u$. Moreover, it follows from
Section 0.2 that $s$ is not an abstraction since $\varepsilon\neq\mathsf{abs}$
by hypothesis. Therefore $s\,u$ is $\to$-irreducible since it is not a redex
nor its subterms reduce.

  * •

nf-succ-nat. Then $t=\mathbf{S}(u)\in\mathsf{NF}_{\mathsf{nat}}$ is derived
from $u\in\mathsf{NF}_{\mathsf{nat}}$. The only rule to evaluate $t$ is
r-succ. But given that $u$ is $\to$-irreducible by the IH on $u$, then
$\mathbf{S}(u)$ does not reduce.

  * •

nf-succ-stuck. Analogous to the previous case.

  * •

nf-if. Then $t=\mathsf{if}(s,u,x.\,r)\in\mathsf{NF}_{\mathsf{stuck}}$ is
derived from $s\in\mathsf{NF}_{\varepsilon}$, with
$\varepsilon\neq\mathsf{nat}$. Hence $s$ is $\to$-irreducible by IH on $s$.
Moreover, it follows from Section 0.2 that $s$ is not of the form $\mathbf{k}$
since $\varepsilon\neq\mathsf{nat}$ by hypothesis. Therefore
$\mathsf{if}(s,u,x.\,r)$ is $\to$-irreducible since it is not a redex nor $s$
reduces.

$2\Rightarrow 1)$ By induction on $t$, with $t$ closed so that $t\neq x$. Note
that case $t=\mathsf{fix}\,x.\,s$ is not possible since rule r-fix states that
any term of the form $\mathsf{fix}\,x.\,s$ reduces.

  * •

$t=\lambda x.\,s$. Assuming $\varepsilon=\mathsf{abs}$ and applying rule nf-
abs then $\lambda x.\,s\in\mathsf{NF}_{\mathsf{abs}}$.

  * •

$t=s\,u$. Since $s\,u$ is $\to$-irreducible, it follows that both $s$ and $u$
are also $\to$-irreducible, as otherwise $t$ would reduce by rules r-appL or
r-appR. Consequently, there exists a fallible nature $\varepsilon_{1}$ such
that $s\in\mathsf{NF}_{\varepsilon_{1}}$ and another fallible nature
$\varepsilon_{2}$ such that $u\in\mathsf{NF}_{\varepsilon_{2}}$, by IH on $s$
and $u$ respectively. It is worth noting that $s$ cannot be of the form
$\lambda x.\,s^{\prime}$, since otherwise $t$ would reduce by rule r-beta.
Hence, it must be the case that $\varepsilon_{1}\neq\mathsf{abs}$ by Section
0.2. Then $s\,u\in\mathsf{NF}_{\mathsf{stuck}}$ by applying rule nf-app, with
$\varepsilon=\mathsf{stuck}$.

  * •

$t={\bf 0}$. Assuming $\varepsilon=\mathsf{nat}$ and applying rule nf-zero
then ${\bf 0}\in\mathsf{NF}_{\mathsf{nat}}$.

  * •

$t=\mathbf{S}(s)$. Since $\mathbf{S}(s)$ is $\to$-irreducible, it follows that
$s$ is also $\to$-irreducible, as otherwise $t$ would reduce by rule r-succ.
Then there exists a fallible nature $\varepsilon^{\prime}$ such that
$s\in\mathsf{NF}_{\varepsilon^{\prime}}$ by IH on $s$. To conclude, we apply
rule nf-succ-nat if $\varepsilon^{\prime}=\mathsf{nat}$ or rule nf-succ-stuck
otherwise, and derive $\mathbf{S}(s)\in\mathsf{NF}_{\mathsf{nat}}$ if
$\varepsilon^{\prime}=\mathsf{nat}$, otherwise
$\mathbf{S}(s)\in\mathsf{NF}_{\mathsf{stuck}}$.

  * •

$t=\mathsf{if}(s,u,x.\,r)$. Since $\mathsf{if}(s,u,x.\,r)$ is
$\to$-irreducible, it follows that $s$ is also $\to$-irreducible, as otherwise
$t$ would reduce by rule r-if. Then there exists a fallible nature
$\varepsilon^{\prime}$ such that $s\in\mathsf{NF}_{\varepsilon^{\prime}}$ by
IH on $s$. Moreover, $s$ is not of the form ${\bf 0}$ nor
$\mathbf{S}(\mathbf{k})$, otherwise $t$ would reduce by rule r-if0 or r-ifS,
respectively. Therefore it must be the case that
$\varepsilon^{\prime}\neq\mathsf{nat}$ by Section 0.2. Then
$\mathsf{if}(s,u,x.\,r)\in\mathsf{NF}_{\mathsf{stuck}}$ by applying rule nf-
if, with $\varepsilon=\mathsf{stuck}$.

∎

⋄*

###### Proof.

By induction on $t$. Note cases $t=x$, $t=\lambda x.\,s$ and $t={\bf 0}$ are
impossible by hypothesis.

  * •

$t=s\,u$. We can reduce an application using rules r-beta, r-appL and r-appR,
so we have the following cases:

    * –

r-beta/r-beta. This case does not apply since we would have that
$t_{1}=t_{2}$, which contradicts the hypothesis.

    * –

r-beta/r-appL. We have $t=(\lambda
x.\,s^{\prime})\,\mathbf{v}\to_{\texttt{B}}s^{\prime}\\{x:=\mathbf{v}\\}=t_{1}$,
where $s=\lambda x.\,s^{\prime}$, $u=\mathbf{v}$, and $\rho_{1}=\texttt{B}$.
On the other hand, $t=(\lambda
x.\,s^{\prime})\,\mathbf{v}\to_{\rho_{2}}s_{2}\,\mathbf{v}=t_{2}$ is derived
from $\lambda x.\,s^{\prime}\to_{\rho_{2}}s_{2}$, but this is not possible
since there are no rules to reduce abstractions.

    * –

r-beta/r-appR. Analogous to the previous case.

    * –

r-appL/r-appL. We have $t=s\,u\to_{\rho_{1}}s_{1}\,u=t_{1}$ derived from
$s\to_{\rho_{1}}s_{1}$, and we have $t=s\,u\to_{\rho_{2}}s_{2}\,u=t_{2}$
derived from $s\to_{\rho_{2}}s_{2}$, where $s_{1}\neq s_{2}$ since
$s_{1}\,u\neq s_{2}\,u$ by hypothesis. We apply the IH on $s$, yielding
$s^{\prime}$ such that $s_{1}\to_{\rho_{2}}s^{\prime}$ and
$s_{2}\to_{\rho_{1}}s^{\prime}$. Applying rule r-appL to both $s_{1}$ and
$s_{2}$, we obtain $t_{1}=s_{1}\,u\to_{\rho_{2}}s^{\prime}\,u=t^{\prime}$ and
$t_{2}=s_{2}\,u\to_{\rho_{1}}s^{\prime}\,u=t^{\prime}$ respectively. The
following diagram summarizes the proof:

$\textstyle{t=s\,u\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\scriptstyle{\rho_{2}}$$\textstyle{s_{1}\,u=t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{2}}$$\textstyle{t_{2}=s_{2}\,u\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\textstyle{s^{\prime}\,u=t^{\prime}}$

    * –

r-appR/r-appR. Analogous to the previous case.

    * –

r-appL/r-appR. We have $t=s\,u\to_{\rho_{1}}s_{1}\,u=t_{1}$ derived from (1)
$s\to_{\rho_{1}}s_{1}$, and on the other hand we have
$t=s\,u\to_{\rho_{2}}s\,u_{2}=t_{2}$ derived from (2) $u\to_{\rho_{2}}u_{2}$.
Given (2), we can apply rule r-appR to $s_{1}\,u$, yielding
$t_{1}=s_{1}\,u\to_{\rho_{2}}s_{1}\,u_{2}=t^{\prime}$. Lastly, given (1), we
can apply rule r-appL to $s\,u_{2}$, yielding
$t_{2}=s\,u_{2}\to_{\rho_{1}}s_{1}\,u_{2}=t^{\prime}$. The following diagram
summarizes the proof:

$\textstyle{t=s\,u\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\scriptstyle{\rho_{2}}$$\textstyle{s_{1}\,u=t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{2}}$$\textstyle{t_{2}=s\,u_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\textstyle{s_{1}\,u_{2}=t^{\prime}}$

  * •

$t=\mathbf{S}(s)$. The only rule to reduce $t$ is r-succ. Hence, we have
$t=\mathbf{S}(s)\to_{\rho_{1}}\mathbf{S}(s_{1})=t_{1}$, derived from
$s\to_{\rho_{1}}s_{1}$, and on the other hand
$t=\mathbf{S}(s)\to_{\rho_{2}}\mathbf{S}(s_{2})=t_{2}$, derived from
$s\to_{\rho_{2}}s_{2}$, where $s_{1}\neq s_{2}$ since
$\mathbf{S}(s_{1})\neq\mathbf{S}(s_{2})$ by hypothesis. We can apply the IH on
$s$, yielding $s^{\prime}$ such that $s_{1}\to_{\rho_{2}}s^{\prime}$ and
$s_{2}\to_{\rho_{1}}s^{\prime}$. Applying rule r-succ to both $s_{1}$ and
$s_{2}$, we obtain $\mathbf{S}(s_{1})\to_{\rho_{2}}\mathbf{S}(s^{\prime})$ and
$\mathbf{S}(s_{2})\to_{\rho_{1}}\mathbf{S}(s^{\prime})$, respectively. The
following diagram summarizes the proof:

$\textstyle{t=\mathbf{S}(s)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\scriptstyle{\rho_{2}}$$\textstyle{\mathbf{S}(s_{1})=t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{2}}$$\textstyle{t_{2}=\mathbf{S}(s_{2})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\textstyle{\mathbf{S}(s^{\prime})=t^{\prime}}$

  * •

$t=\mathsf{if}(s,u,x.\,r)$. We can reduce $t$ using rules r-if0, r-ifS and
r-if, so we have the following cases:

    * –

r-if0/r-if0. This case does not apply since it should be that $t_{1}=t_{2}$,
which contradicts the hypothesis.

    * –

r-ifS/r-ifS. Analogous to the previous case.

    * –

r-if0/r-ifS. This case is not possible since on the one hand we have $s={\bf
0}$ given that $t$ reduces by rule r-if0, but on the other hand,
$s=\mathbf{S}(\mathbf{k})$ since $t$ also reduces by rule r-ifS.

    * –

r-if0/r-if. We have $t=\mathsf{if}({\bf 0},u,x.\,r)\to_{\texttt{I0}}u=t_{1}$,
where $s={\bf 0}$ and $\rho_{1}=\texttt{I0}$. On the other hand
$t=\mathsf{if}({\bf 0},u,x.\,r)\to_{\rho_{2}}\mathsf{if}(s_{2},u,x.\,r)=t_{2}$
is derived from ${\bf 0}\to_{\rho_{2}}s_{2}$, but this is not possible since
there are no rules to reduce ${\bf 0}$.

    * –

r-ifS/r-if. We have
$t=\mathsf{if}(\mathbf{S}(\mathbf{k}),u,x.\,r)\to_{\texttt{IS}}r\\{x:=\mathbf{k}\\}=t_{1}$
where $s=\mathbf{S}(\mathbf{k})$ and $\rho_{1}=\texttt{IS}$, and we have
$t=\mathsf{if}(\mathbf{S}(\mathbf{k}),u,x.\,r)\to_{\rho_{2}}\mathsf{if}(s_{2},u,x.\,r)=t_{2}$
derived from $\mathbf{S}(\mathbf{k})\to_{\rho_{2}}s_{2}$. This reduction can
only be derived by rule r-succ, hence $s_{2}=\mathbf{S}(s^{\prime}_{2})$, and
the reduction is derived from $\mathbf{k}\to_{\rho_{2}}s^{\prime}_{2}$, but
this is not possible since $\mathbf{k}$ is a value.

    * –

r-if/ r-if. We have
$t=\mathsf{if}(s,u,x.\,r)\to_{\rho_{1}}\mathsf{if}(s_{1},u,x.\,r)=t_{1}$
derived from $s\to_{\rho_{1}}s_{1}$, and we have
$t=\mathsf{if}(s,u,x.\,r)\to_{\rho_{2}}\mathsf{if}(s_{2},u,x.\,r)=t_{2}$
derived from $s\to_{\rho_{2}}s_{2}$, where $s_{1}\neq s_{2}$ since
$\mathsf{if}(s_{1},u,x.\,r)\neq\mathsf{if}(s_{2},u,x.\,r)$ by hypothesis. We
apply the IH on $s$, yielding $s^{\prime}$ such that
$s_{1}\to_{\rho_{2}}s^{\prime}$ and $s_{2}\to_{\rho_{1}}s^{\prime}$. Applying
rule r-if to both $s_{1}$ and $s_{2}$, we obtain
$t_{1}=\mathsf{if}(s_{1},u,x.\,r)\to_{\rho_{2}}\mathsf{if}(s^{\prime},u,x.\,r)=t^{\prime}$
and
$t_{2}=\mathsf{if}(s_{2},u,x.\,r)\to_{\rho_{1}}\mathsf{if}(s^{\prime},u,x.\,r)=t^{\prime}$
respectively. The following diagram summarizes the proof:

$\textstyle{t=\mathsf{if}(s,u,x.\,r)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\scriptstyle{\rho_{2}}$$\textstyle{\mathsf{if}(s_{1},u,x.\,r)=t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{2}}$$\textstyle{t_{2}=\mathsf{if}(s_{2},u,x.\,r)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{1}}$$\textstyle{\mathsf{if}(s^{\prime},u,x.\,r)=t^{\prime}}$

  * •

$t=\mathsf{fix}\,x.\,s$. This case does not apply since we would have that
$t_{1}=t_{2}$, which contradicts the hypothesis.

∎

##  .6 Omitted proofs of Section 0.3

Let I and J be two sets. We write $I\uplus J$ to denote the disjoint union of
$I$ and $J$.

*

###### Proof.

The first item is immediate by definition of $\lhd$. Both directions of the
third item follow from the first two items by induction on the cardinality of
$I$, which is a finite set. For the direction $(\Rightarrow)$ of the second
item, we consider four subcases, depending on whether each of
$\mathcal{T}^{?}_{1}$ and $\mathcal{T}^{?}_{2}$ is $\bot$ or not. We only
discuss three subcases, as two of them are symmetric:

  * •

If $\mathcal{T}^{?}_{1}=\mathcal{T}^{?}_{2}=\bot$, then
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}=\bot\lhd\mathcal{T}$ so $\mathcal{T}$
is of the form $[\,]^{\nu}$ for some proper nature $\nu$. It suffices to take
$\mathcal{T}_{1}=\mathcal{T}_{2}:=[\,]^{\nu}$, as then
$\mathcal{T}=[\,]^{\nu}=[\,]^{\nu}+[\,]^{\nu}=\mathcal{T}_{1}+\mathcal{T}_{2}$,
and $\mathcal{T}^{?}_{i}=\bot\lhd[\,]^{\nu}=\mathcal{T}_{i}$ for all
$i\in\\{1,2\\}$.

  * •

If $\mathcal{T}^{?}_{1}\neq\bot$ and $\mathcal{T}^{?}_{2}=\bot$, then
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}=\mathcal{T}^{?}_{1}+\bot=\mathcal{T}^{?}_{1}\lhd\mathcal{T}$.
There are two subcases, depending on whether $\mathcal{T}$ is an
$\mathsf{abs}$-multitype or a $\mathsf{nat}$-multitype. We only treat the
first case, the second one being symmetric. Let $\mathcal{T}$ be of the form
$[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in I}$. Then
$\mathcal{T}^{?}_{1}=\mathcal{T}=[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in I}$ by
definition of $\lhd$, since $\mathcal{T}^{?}_{1}\lhd\mathcal{T}$ and
$\mathcal{T}^{?}_{1}\neq\bot$. It suffices to take
$\mathcal{T}_{1}:=[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in I}$ and
$\mathcal{T}_{2}:=[\,]^{\mathsf{abs}}$, as then
$\mathcal{T}=[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in
I}=[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in
I}+[\,]^{\mathsf{abs}}=\mathcal{T}_{1}+\mathcal{T}_{2}$, where
$\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{1}$ and
$\mathcal{T}^{?}_{2}=\bot\lhd[\,]^{\mathsf{abs}}$.

  * •

If $\mathcal{T}^{?}_{1}\neq\bot$ and $\mathcal{T}^{?}_{2}\neq\bot$, then since
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}$ is well-defined we know that
$\mathcal{T}^{?}_{1}$ and $\mathcal{T}^{?}_{2}$ must be compatible. There are
two cases, depending on whether they are $\mathsf{abs}$-multitypes or optional
$\mathsf{nat}$-multitypes. We only treat the first case, the second one being
symmetric. Then there exist sets $I,J$ such that
$\mathcal{T}^{?}_{1}=[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in I}$ and
$\mathcal{T}^{?}_{2}=[\mathbb{A}_{j}]^{\mathsf{abs}}_{j\in J}$. Furthermore,
by hypothesis
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}=[\mathbb{A}_{k}]^{\mathsf{abs}}_{k\in
I\cup J}\lhd\mathcal{T}$, so
$\mathcal{T}=[\mathbb{A}_{k}]^{\mathsf{abs}}_{k\in I\cup J}$, and it suffices
to take $\mathcal{T}_{1}:=[\mathbb{A}_{i}]^{\mathsf{abs}}_{i\in I}$ and
$\mathcal{T}_{2}:=[\mathbb{A}_{j}]^{\mathsf{abs}}_{j\in J}$.

For the direction $(\Leftarrow)$, we want to show that if there exist
multitypes $\mathcal{T}_{1},\mathcal{T}_{2}$ such that
$\mathcal{T}=\mathcal{T}_{1}+\mathcal{T}_{2}$ and
$\mathcal{T}^{?}_{i}\lhd\mathcal{T}_{i}$ for all $i\in\\{1,2\\}$, then we have
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd\mathcal{T}$, we consider four
subcases again, depending on whether each of $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$ are empty or not. The steps are analogous as the other
direction. ∎

######  Lemma 7 (Value Splitting / Merging).

Let $\mathcal{T}^{?}_{1},\mathcal{T}^{?}_{2}$ be optional multitypes, and let
$\mathcal{F}_{1},\mathcal{F}_{2}$ be multitype families. Then the following
are equivalent:

  1. 1.

$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{v}:\mathcal{T}$ with
$\mathcal{T}$ a multitype such that
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd\mathcal{T}$

  2. 2.

There exist family contexts $\Phi_{1},\Phi_{2}$, typing contexts
$\Gamma_{1},\Gamma_{2}$, multi-counters $\mathfrak{m}_{1},\mathfrak{m}_{2}$,
and multitypes $\mathcal{T}_{1},\mathcal{T}_{2}$ such that
$\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$, and for all $i=1,2$,
$\pi_{i}\rhd\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}_{i}}\mathbf{v}:\mathcal{T}_{i}$
and $\mathcal{T}^{?}_{i}\lhd\mathcal{T}_{i}$.

###### Proof.

$1\Rightarrow 2)$ We proceed by induction on $\pi$. Since $\mathbf{v}$ is
value, the only rules that apply are t-abs, t-zero and t-succ.

  * •

t-abs. Then $\mathbf{v}=\lambda x.\,t$, and $\pi\rhd+_{i\in I}\Phi_{i};+_{i\in
I}\Gamma_{i}\vdash^{+_{i\in I}\mathfrak{m}_{i}}\lambda
x.\,t:[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in I}$, where
$\Phi=+_{i\in I}\Phi_{i}$ and $\Gamma=+_{i\in I}\Gamma_{i}$ and
$\mathfrak{m}=+_{i\in I}\mathfrak{m}_{i}$ and
$\mathcal{T}=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in I}$.
The judgment is derived from
$\pi^{\prime}_{i}\rhd\Phi_{i};\Gamma_{i},x:\mathcal{S}^{?}_{i}\vdash^{\mathfrak{m}_{i}}t:\mathcal{U}_{i}$
for each ${i\in I}$. Given that
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I}$, then there are two subcases to analyze, depending on whether
$\mathcal{T}$ is empty or not:

    * –

If $\mathcal{T}=[\,]$, then
$\mathcal{T}=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I}=[\,]^{\mathsf{abs}}$, so $I=\varnothing$. Therefore $\pi$ has no premises
and moreover $\Phi=\varnothing$ and $\Gamma=\varnothing$ and
$\mathfrak{m}=[\,]$. Taking $\Phi_{1}=\Phi_{2}:=\varnothing$ and
$\Gamma_{1}=\Gamma_{2}:=\varnothing$ and
$\mathfrak{m}_{1}=\mathfrak{m}_{2}:=[\,]$ and
$\mathcal{T}_{1}=\mathcal{T}_{2}:=[\,]^{\mathsf{abs}}$, we obtain the
derivations $\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\lambda
x.\,t:\mathcal{T}_{1}$ and
$\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\lambda
x.\,t:\mathcal{T}_{2}$ by applying rule t-abs. Then
$\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{1}$ and
$\mathcal{T}^{?}_{2}\lhd\mathcal{T}_{2}$ by Lemma 3 (item 2). It is trivial to
check that the conditions hold, since $\pi_{1}=\pi_{2}=\pi$.

    * –

If $\mathcal{T}\neq[\,]$, then $I\neq\varnothing$, so we can split it as
$I=I_{1}\uplus I_{2}$ such that
$\mathcal{T}_{1}=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{1}}$ and
$\mathcal{T}_{2}=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{2}}$. Taking $\Phi_{1}:=+_{i\in I_{1}}\Phi_{i}$ and $\Phi_{2}:=+_{i\in
I_{2}}\Phi_{i}$, and $\Gamma_{1}:=+_{i\in I_{1}}\Gamma_{i}$ and
$\Gamma_{2}:=+_{i\in I_{2}}\Gamma_{i}$, and $\mathfrak{m}_{1}:=+_{i\in
I_{1}}\mathfrak{m}_{i}$ and $\mathfrak{m}_{2}:=+_{i\in
I_{2}}\mathfrak{m}_{i}$, and
$\mathcal{T}_{1}:=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{1}}$ and
$\mathcal{T}_{2}:=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{2}}$, we can then split $(\pi^{\prime}_{i})_{i\in I}$ into
$(\pi^{\prime}_{i})_{i\in I_{1}}$ and $(\pi^{\prime}_{i})_{i\in I_{2}}$. We
can easily check that $\Phi=\Phi_{1}+\Phi_{2}$ and
$\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$\mathcal{T}=\mathcal{T}_{1}+\mathcal{T}_{2}$. Applying rule t-abs to both
groups of derivations, we obtain
$\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\lambda
x.\,t:\mathcal{T}_{1}$ and
$\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\lambda
x.\,t:\mathcal{T}_{2}$. And moreover $\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{1}$
and $\mathcal{T}^{?}_{2}\lhd\mathcal{T}_{2}$ by Lemma 3 (item 2).

  * •

t-zero. Then $\mathbf{v}={\bf 0}$ and
$\pi\rhd\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}_{i\in I}$, where $\Phi=\varnothing$ and
$\Gamma=\varnothing$ and $\mathfrak{m}=[\,]$ and
$\mathcal{T}=[\mathbb{0}]^{\mathsf{nat}}_{i\in I}$. Since
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd[\mathbb{0}]^{\mathsf{nat}}_{i\in
I}$, there are two subcases to analyze, depending on whether $\mathcal{T}$ is
empty or not:

    * –

If $\mathcal{T}=[\,]$, then $\mathcal{T}^{?}_{1}=\mathcal{T}^{?}_{2}=\bot$ and
$[\mathbb{0}]^{\mathsf{nat}}_{i\in I}=[\,]^{\mathsf{nat}}$, so
$I=\varnothing$. This subcase is analogous to the subcase $\mathcal{T}=[\,]$
for t-abs.

    * –

If $\mathcal{T}\neq[\,]$, then $I\neq\varnothing$, so we can split it as
$I=I_{1}\uplus I_{2}$ so that $[\mathbb{0}]^{\mathsf{nat}}_{i\in
I}=[\mathbb{0}]^{\mathsf{nat}}_{i\in I_{1}}+[\mathbb{0}]^{\mathsf{nat}}_{i\in
I_{2}}$. Moreover, there exist multitypes $\mathcal{T}_{1},\mathcal{T}_{2}$
such that $\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{1}$ and
$\mathcal{T}^{?}_{2}\lhd\mathcal{T}_{2}$ by Lemma 3 (item 2). Taking
$\Phi_{1}=\Phi_{2}:=\varnothing$, and $\Gamma_{1}=\Gamma_{2}:=\varnothing$,
and $\mathfrak{m}_{1}=\mathfrak{m}_{2}:=[\,]$, and $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$, we check $\Phi=\varnothing=\Phi_{1}+\Phi_{2}$ and
$\Gamma=\varnothing=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\,]=\mathfrak{m}_{1}+\mathfrak{m}_{2}$. By rule t-zero we
obtain the derivations $\pi_{1}\rhd\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}_{i\in I_{1}}$ and
$\pi_{2}\rhd\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}_{i\in I_{2}}$.

  * •

t-succ. Then $\mathbf{v}=\mathbf{S}(\mathbf{k})$ and
$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(\mathbf{k}):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$, where $\mathcal{T}=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$. The judgment is derived from
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{k}:+_{i\in
I}\mathcal{N}_{i}$. Since
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$, there are two subcases to analyze, depending on whether $\mathcal{T}$ is
empty or not:

    * –

Analogous to the subcase $\mathcal{T}=[\,]$ in cases t-abs and t-zero.

    * –

If $\mathcal{T}\neq[\,]$, then $I\neq\varnothing$, so we can split it as
$I=I_{1}\uplus I_{2}$ so that
$[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{1}}+[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{2}}=\mathcal{T}_{1}+\mathcal{T}_{2}$. Then
$\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{1}$ and
$\mathcal{T}^{?}_{2}\lhd\mathcal{T}_{2}$ by Lemma 3 (item 2). Moreover, the
premise can be written as
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{k}:+_{i\in
I_{1}}\mathcal{N}_{i}+_{i\in I_{2}}\mathcal{N}_{i}$, and $+_{i\in
I_{1}}\mathcal{N}_{i}+_{i\in I_{2}}\mathcal{N}_{i}\lhd+_{i\in
I_{1}}\mathcal{N}_{i}+_{i\in I_{2}}\mathcal{N}_{i}$ by definition. We can
apply IH on $\pi^{\prime}$, yielding that there exist family contexts
$\Phi_{1}$, $\Phi_{2}$, typing contexts $\Gamma_{1}$, $\Gamma_{2}$, multi-
counters $\mathfrak{m}_{1}$, $\mathfrak{m}_{2}$ and multitypes
$\mathcal{N}_{1},\mathcal{N}_{2}$ such that $\Phi=\Phi_{1}+\Phi_{2}$ and
$\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$, and the derivations
$\pi^{\prime}_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\mathbf{k}:\mathcal{N}_{1}$
and
$\pi^{\prime}_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{k}:\mathcal{N}_{2}$
hold, with $+_{i\in I_{1}}\mathcal{N}_{i}\lhd\mathcal{N}_{1}$ and $+_{i\in
I_{2}}\mathcal{N}_{i}\lhd\mathcal{N}_{2}$. Taking $\Phi_{1},\Phi_{2}$ and
$\Gamma_{1},\Gamma_{2}$ and $\mathfrak{m}_{1},\mathfrak{m}_{2}$ and the
previously defined
$\mathcal{T}_{1}:=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in I_{1}}$
and $\mathcal{T}_{2}:=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{2}}$, then $\mathcal{T}=\mathcal{T}_{1}+\mathcal{T}_{2}$; the remainder
conditions are already checked in the IH. Applying rule t-succ to both
$\pi^{\prime}_{1}$ and $\pi^{\prime}_{2}$, we obtain
$\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\mathbf{S}(\mathbf{k}):\mathcal{T}_{1}$
and
$\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{S}(\mathbf{k}):\mathcal{T}_{2}$,
with $\mathcal{T}^{?}_{1}\lhd\mathcal{T}_{1}$ and
$\mathcal{T}^{?}_{2}\lhd\mathcal{T}_{2}$.

$2\Rightarrow 1)$ We proceed by induction on $\pi_{1}$ and $\pi_{2}$. Since
$\mathbf{v}$ is value, the only rules that apply are t-abs, t-zero and t-succ.

  * •

t-abs. Then $\mathbf{v}=\lambda x.\,t$, and we have sets $I_{1}$ and $I_{2}$
such that $\pi_{1}$ is of the form

$\pi_{1}:=\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 17.39723pt\hbox{$\displaystyle\penalty
1(\pi_{i}\rhd\Phi_{i};\Gamma_{i},x:\mathcal{S}^{?}_{i}\vdash^{\mathfrak{m}_{i}}t:\mathcal{U}_{i})_{i\in
I_{1}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=146.53203pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle+_{i\in
I_{1}}\Phi_{i};+_{i\in I_{1}}\Gamma_{i}\vdash^{+_{i\in
I_{1}}\mathfrak{m}_{i}}\lambda
x.\,t:[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{1}}$}}}}\end{array}$

where $\Phi_{1}=+_{i\in I_{1}}\Phi_{i}$ and $\Gamma_{1}=+_{i\in
I_{1}}\Gamma_{i}$ and $\mathfrak{m}_{1}=+_{i\in I_{1}}\mathfrak{m}_{i}$ and
$\mathcal{T}_{1}=[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{1}}$. And on the other hand $\pi_{2}$ is of the form

$\pi_{2}:=\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 17.39723pt\hbox{$\displaystyle\penalty
1(\pi_{i}\rhd\Phi_{i};\Gamma_{i},x:\mathcal{S}^{?}_{i}\vdash^{\mathfrak{m}_{i}}t:\mathcal{U}_{i})_{i\in
I_{2}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=146.53203pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle+_{i\in
I_{2}}\Phi_{i};+_{i\in I_{2}}\Gamma_{i}\vdash^{+_{i\in
I_{2}}\mathfrak{m}_{i}}\lambda
x.\,t:[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{2}}$}}}}\end{array}$

where $\Phi_{2}=+_{i\in I_{2}}\Phi_{i}$ and $\Gamma_{2}=+_{i\in
I_{2}}\Gamma_{i}$ $\mathfrak{m}_{2}=+_{i\in I_{2}}\mathfrak{m}_{i}$ and and
$\mathcal{T}_{2}=[\mathcal{S}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{2}}$. Moreover $\Phi=\Phi_{1}+\Phi_{2}=+_{i\in I_{1}}\Phi_{i}+_{i\in
I_{2}}\Phi_{i}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}=+_{i\in
I_{1}}\Gamma_{i}+_{i\in I_{2}}\Gamma_{i}$ and
$\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}=+_{i\in
I_{1}}\mathfrak{m}_{i}+_{i\in I_{2}}\mathfrak{m}_{i}$ and
$\mathcal{T}^{?}_{1}\lhd[\mathcal{S}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{1}}$ and
$\mathcal{T}^{?}_{2}\lhd[\mathcal{S}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{2}}$. By joining the premises of $\pi_{1}$ and $\pi_{2}$, and applying rule
t-abs we yield

$\pi:=\left(\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 24.13885pt\hbox{$\displaystyle\penalty
1(\pi_{i}\rhd];\Phi_{i}\vdash^{\mathfrak{m}_{i}}\Gamma_{i},x:\mathcal{S}^{?}_{i}:t{\mathcal{U}_{i}})_{i\in
I_{1}\uplus I_{2}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=169.27199pt\hbox{\kern
3.00003pt$\texttt{{t-abs${}_{\mathsf{v}}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle+_{i\in I_{1}\uplus I_{2}}\Phi_{i};+_{i\in
I_{1}\uplus I_{2}}\Gamma_{i}\vdash^{+_{i\in I_{1}\uplus
I_{2}}\mathfrak{m}_{i}}\lambda
x.\,t:[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in I_{1}\uplus
I_{2}}$}}}}\end{array}\right)$

and
$\mathcal{T}^{?}_{1}+\mathcal{T}^{?}_{2}\lhd[\mathcal{S}^{?}_{i}\to\mathcal{U}_{i}]^{\mathsf{abs}}_{i\in
I_{1}\uplus I_{2}}$ holds by Lemma 3 (item 3).

  * •

t-zero. Analogous to the previous case.

  * •

t-succ. Then $\mathbf{v}=\mathbf{S}(\mathbf{k})$, and we have sets $I_{1}$ and
$I_{2}$ such that $\pi_{1}$ is of the form

$\pi_{1}:=\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 5.34245pt\hbox{$\displaystyle\penalty
1\pi^{\prime}_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\mathbf{k}:+_{i\in
I_{1}}\mathcal{N}_{i}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=99.24599pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\mathbf{S}(\mathbf{k}):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{1}}$}}}}\end{array}$

where $\mathcal{T}_{1}=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{1}}$. And on the other hand $\pi_{2}$ is of the form

$\pi_{2}:=\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 5.34245pt\hbox{$\displaystyle\penalty
1\pi^{\prime}_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{k}:+_{i\in
I_{2}}\mathcal{N}_{i}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=99.24599pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{S}(\mathbf{k}):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{2}}$}}}}\end{array}$

where $\mathcal{T}_{2}=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{2}}$. Moreover $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$
and $\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$\mathcal{T}^{?}_{1}\lhd[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{1}}$ and
$\mathcal{T}^{?}_{2}\lhd[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{2}}$. Let $j=1,2$, then let us define the optional multitype
$\mathcal{S}^{?}_{j}$ as

$\mathcal{S}^{?}_{j}:=\left\\{\begin{array}[]{ll}\bot&\text{if
}\mathcal{T}^{?}_{j}=\bot\\\ +_{i\in
I_{j}}\mathcal{N}_{i}&\text{otherwise}\end{array}\right.$

so that $\mathcal{S}^{?}_{1}\lhd+_{i\in I_{1}}\mathcal{N}_{i}$ and
$\mathcal{S}^{?}_{2}\lhd+_{i\in I_{2}}\mathcal{N}_{i}$. We can apply the IH,
yielding
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{k}:\mathcal{N}$,
where $\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}\lhd\mathcal{N}$. Moreover,
$\mathcal{N}=+_{i\in I_{1}}\mathcal{N}_{i}+_{i\in I_{2}}\mathcal{N}_{i}$ by
Lemma 3 (item 3). Applying rule t-succ, we conclude
$\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(\mathbf{k}):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I_{1}\uplus I_{2}}$.

∎

*

###### Proof.

We proceed by induction on $\pi$.

  1. 1.

t-var1. Then $\pi\rhd\varnothing;y:\mathcal{T}\vdash^{[\,]}y:\mathcal{T}$,
where $\Phi=\varnothing$ and $(\Gamma,x:\mathcal{S}^{?})=(y:\mathcal{T})$ and
$\mathfrak{m}=[\,]$ and $t=y$. We consider two subcases, depending on whether
$x=y$ or not:

    1. 1.1

If $x=y$, then $\Gamma=\varnothing$ and $\mathcal{S}^{?}=\mathcal{T}$. Since
$\mathcal{S}^{?}=\mathcal{T}\lhd\mathcal{S}$, then $\mathcal{S}=\mathcal{T}$.
We conclude by letting $\pi^{\prime}:=\zeta$.

    2. 1.2

If $x\neq y$, then $\Gamma=(y:\mathcal{T})$ and thus $\mathcal{S}^{?}=\bot$.
By hypothesis,
$\zeta\rhd\Psi;\Delta\vdash^{\mathfrak{n}}\mathbf{v}:\mathcal{S}$ and moreover
$\mathcal{S}^{?}=\bot\lhd\mathcal{S}$, which means that $\mathcal{S}$ must be
of the form $[\,]^{\nu}$ for some proper nature $\nu$. Hence
$\Psi=\varnothing$ and $\Delta=\varnothing$ and $\mathfrak{n}=[\,]$ by Lemma
3. We conclude by letting $\pi^{\prime}:=\pi$.

  2. 2.

t-var2. Then $\pi\rhd
y:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\};\varnothing\vdash^{[\,]}y:\mathcal{T}$,
where $\Phi=y:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\}$ and
$(\Gamma,x:\mathcal{S}^{?})=\varnothing$ and $\mathfrak{m}=[\,]$ and $t=y$.
Moreover, $\Gamma=\varnothing$ and $\mathcal{S}^{?}=\bot$, since $x$ must be
different from $y$ by the invariant. The rest of the proofs is analogous to
subcase $x\neq y$ from t-var1.

  3. 3.

t-abs. Then $\pi\rhd+_{i\in I}\Phi_{i};+_{i\in I}\Gamma_{i},x:+_{i\in
I}\mathcal{S}^{?}_{i}\vdash^{+_{i\in I}\mathfrak{m}_{i}}\lambda
y.\,s:[\mathcal{U}^{?}_{i}\to\mathcal{R}_{i}]^{\mathsf{abs}}_{i\in I}$, where
$\Phi=+_{i\in I}\Phi_{i}$ and $\Gamma=+_{i\in I}\Gamma_{i}$ and
$\mathcal{S}^{?}=+_{i\in I}\mathcal{S}^{?}_{i}$ and $\mathfrak{m}=+_{i\in
I}\mathfrak{m}_{i}$ and $t=\lambda y.\,s$ and
$\mathcal{T}=[\mathcal{U}^{?}_{i}\to\mathcal{R}_{i}]^{\mathsf{abs}}_{i\in I}$.
The judgment is derived from
$(\pi_{i}\rhd\Phi_{i};\Gamma_{i},x:\mathcal{S}^{?}_{i},y:\mathcal{U}^{?}_{i}\vdash^{\mathfrak{m}_{i}}s:\mathcal{R}_{i})_{i\in
I}$. Since $+_{i\in I}\mathcal{S}^{?}_{i}=\mathcal{S}^{?}\lhd\mathcal{S}$,
then by Lemma 4 there exist family contexts $(\Psi_{i})_{i\in I}$, typing
contexts $(\Delta_{i})_{i\in I}$, multi-counters $(\mathfrak{n}_{i})_{i\in I}$
and multitypes $(\mathcal{S}_{i})_{i\in I}$ such that $\Psi=+_{i\in
I}\Psi_{i}$ and $\Delta=+_{i\in I}\Delta_{i}$ and $\mathfrak{n}=+_{i\in
I}\mathfrak{n}_{i}$ and for all ${i\in I}$
$\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}\mathbf{v}:\mathcal{S}_{i}$
and $\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$. We can apply the IH on $\pi_{i}$
with $\zeta_{i}$, yielding
$(\pi^{\prime}_{i}\rhd\Phi_{i}+\Psi_{i};(\Gamma_{i},y:\mathcal{U}^{?}_{i})+\Delta_{i}\vdash^{\mathfrak{m}_{i}+\mathfrak{n}_{i}}s\\{x:=\mathbf{v}\\}:\mathcal{R}_{i})_{i\in
I}$. By Lemma 2 and $\alpha$-conversion we can write
$(\Gamma_{i},y:\mathcal{U}^{?}_{i})+\Delta_{i}$ as
$(\Gamma_{i}+\Delta_{i}),y:\mathcal{U}^{?}_{i}$. Then we can apply rule t-abs
to $(\pi^{\prime}_{i})_{i\in I}$, yielding $\pi^{\prime}\rhd+_{i\in
I}(\Phi_{i}+\Psi_{i});+_{i\in I}(\Gamma_{i}+\Delta_{i})\vdash^{+_{i\in
I}(\mathfrak{m}_{i}+\mathfrak{n}_{i})}\lambda
y.\,s\\{x:=\mathbf{v}\\}:[\mathcal{U}^{?}_{i}\to\mathcal{R}_{i}]^{\mathsf{abs}}_{i\in
I}$, and we are done since $\lambda y.\,s\\{x:=\mathbf{v}\\}=(\lambda
y.\,s)\\{x:=\mathbf{v}\\}$.

  4. 4.

t-app. Then
$\pi\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2},x:\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}s\,u:\mathcal{T}$,
where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathcal{S}^{?}=\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and $t=s\,u$,
and the judgment is derived from
$\pi_{1}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$
and
$\pi_{2}\rhd\Phi_{2};\Gamma_{2},x:\mathcal{S}^{?}_{2}\vdash^{\mathfrak{m}_{2}}u:\mathcal{U}$
and (1) $\mathcal{U}^{?}\lhd\mathcal{U}$. By Lemma 7 there exist family
contexts $\Psi_{1}$, $\Psi_{2}$, typing contexts $\Delta_{1}$, $\Delta_{2}$,
multi-counters $\mathfrak{n}_{1}$, $\mathfrak{n}_{2}$ and multitypes
$\mathcal{S}_{1}$, $\mathcal{S}_{2}$ such that $\Psi=\Psi_{1}+\Psi_{2}$ and
$\Delta=\Delta_{1}+\Delta_{2}$ and
$\mathfrak{n}=\mathfrak{n}_{1}+\mathfrak{n}_{2}$ and for each $i=1,2$ we have
$\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}\mathbf{v}:\mathcal{S}_{i}$
and $\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$. By IH on $\pi_{1}$ with
$\zeta_{1}$ and $\pi_{2}$ with $\zeta_{2}$ we have
$\pi^{\prime}_{1}\rhd\Phi_{1}+\Psi_{1};\Gamma_{1}+\Delta_{1}\vdash^{\mathfrak{m}_{1}+\mathfrak{n}_{1}}s\\{x:=\mathbf{v}\\}:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$
and
$\pi^{\prime}_{2}\rhd\Phi_{2}+\Psi_{2};\Gamma_{2}+\Delta_{2}\vdash^{\mathfrak{m}_{2}+\mathfrak{n}_{2}}u\\{x:=\mathbf{v}\\}:\mathcal{U}$.
We can apply rule t-app with $\pi^{\prime}_{1}$, $\pi^{\prime}_{2}$ and (3) as
premises, yielding
$\pi^{\prime}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}s\\{x:=\mathbf{v}\\}\,u\\{x:=\mathbf{v}\\}:\mathcal{T}$,
and we are done since
$s\\{x:=\mathbf{v}\\}\,u\\{x:=\mathbf{v}\\}=(s\,u)\\{x:=\mathbf{v}\\}$.

  5. 5.

t-zero. Then $\pi\rhd\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}_{i\in I}$, where $\Phi=\varnothing$ and
$\Gamma=\varnothing$ and $\mathcal{S}^{?}=\bot$ and $\mathfrak{m}=[\,]$ and
$t={\bf 0}$ and $\mathcal{T}=[\mathbb{0}]^{\mathsf{nat}}_{i\in I}$. Since
$\bot\lhd\mathcal{S}$, then $\mathcal{S}$ is of the form $[\,]^{\nu}$, for
some proper nature $\nu$. Moreover, $\Psi=\varnothing$ and
$\Delta=\varnothing$ and $\mathfrak{n}=[\,]$ by Lemma 3. We conclude by
letting $\pi^{\prime}:=\pi$, since ${\bf 0}\\{x:=\mathbf{v}\\}={\bf 0}$.

  6. 6.

t-succ. Then
$\pi\rhd\Phi;\Gamma,x:\mathcal{S}^{?}\vdash^{\mathfrak{m}}\mathbf{S}(u):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$, where $t=\mathbf{S}(u)$ and
$\mathcal{T}=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in I}$. The
judgment is derived from
$\pi_{0}\rhd\Phi;\Gamma,x:\mathcal{S}^{?}\vdash^{\mathfrak{m}}u:+_{i\in
I}\mathcal{N}_{i}$. Applying the IH on $\pi_{0}$ with $\zeta$ we obtain
$\pi^{\prime}_{0}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}u\\{x:=\mathbf{v}\\}:+_{i\in
I}\mathcal{N}_{i}$. Applying rule t-succ we conclude with
$\pi^{\prime}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}\mathbf{S}(u\\{x:=\mathbf{v}\\}):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$, and we are done since
$\mathbf{S}(u\\{x:=\mathbf{v}\\})=(\mathbf{S}(u))\\{x:=\mathbf{v}\\}$.

  7. 7.

t-ifZero. Then
$\pi\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2},x:\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}\vdash^{[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(s,u,y.\,r):\mathcal{T}$
where $\Phi=\Phi_{1}+\Phi_{2}$, $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathcal{S}^{?}=\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}$ and
$\mathfrak{m}=[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$t=\mathsf{if}(s,u,y.\,r)$. The judgment is derived from
$\pi_{1}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathbb{0}]^{\mathsf{nat}}$
and
$\pi_{2}\rhd\Phi_{2};\Gamma_{2},x:\mathcal{S}^{?}_{2}\vdash^{\mathfrak{m}_{2}}u:\mathcal{T}$.
We may assume $y\notin\\{x\\}\cup\mathsf{fv}(\mathbf{v})$ by
$\alpha$-conversion. By Lemma 7, there exist family contexts $\Psi_{1}$,
$\Psi_{2}$, typing contexts $\Delta_{1}$, $\Delta_{2}$, multi-counters
$\mathfrak{n}_{1}$, $\mathfrak{n}_{2}$ and multitypes $\mathcal{S}_{1}$,
$\mathcal{S}_{2}$ such that $\Psi=\Psi_{1}+\Psi_{2}$ and
$\Delta=\Delta_{1}+\Delta_{2}$ and
$\mathfrak{n}=\mathfrak{n}_{1}+\mathfrak{n}_{2}$ and for each $i=1,2$ we have
$\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}\mathbf{v}:\mathcal{S}_{i}$
and $\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$. By IH on $\pi_{1}$ with
$\zeta_{1}$ and $\pi_{2}$ with $\zeta_{2}$ we have
$\pi^{\prime}_{1}\rhd\Phi_{1}+\Psi_{1};\Gamma_{1}+\Delta_{1}\vdash^{\mathfrak{m}_{1}+\mathfrak{n}_{1}}s\\{x:=\mathbf{v}\\}:[\mathbb{0}]^{\mathsf{nat}}$
and
$\pi^{\prime}_{2}\rhd\Phi_{2}+\Psi_{2};\Gamma_{2}+\Delta_{2}\vdash^{\mathfrak{m}_{1}+\mathfrak{n}_{1}}u\\{x:=\mathbf{v}\\}:\mathcal{T}$.
Applying rule t-ifZero we conclude with
$\pi^{\prime}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}\mathsf{if}(s\\{x:=\mathbf{v}\\},u\\{x:=\mathbf{v}\\},y.\,r\\{x:=\mathbf{v}\\}):\mathcal{T}$,
and we are done since
$\mathsf{if}(s\\{x:=\mathbf{v}\\},u\\{x:=\mathbf{v}\\},y.\,r\\{x:=\mathbf{v}\\})=(\mathsf{if}(s,u,y.\,r))\\{x:=\mathbf{v}\\}$

  8. 8.

t-ifSucc. Then
$\pi\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2},x:\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}\vdash^{[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(s,u,y.\,r):\mathcal{T}$
where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathcal{S}^{?}=\mathcal{S}^{?}_{1}+\mathcal{S}^{?}_{2}$ and
$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$t=\mathsf{if}(s,u,y.\,r)$. The judgment is derived from
$\pi_{1}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$
and
$\pi_{2}\rhd\Phi_{2};\Gamma_{2},x:\mathcal{S}^{?}_{2},y:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{2}}r:\mathcal{T}$
and (1) $\mathcal{N}^{?}\lhd\mathcal{N}$. We may assume
$y\notin\\{x\\}\cup\mathsf{fv}(\mathbf{v})$ by $\alpha$-conversion. By Lemma 7
there exist family contexts $\Psi_{1}$, $\Psi_{2}$, typing contexts
$\Delta_{1}$, $\Delta_{2}$, multi-counters $\mathfrak{n}_{1}$,
$\mathfrak{n}_{2}$ and multitypes $\mathcal{S}_{1}$, $\mathcal{S}_{2}$ such
that $\Psi=\Psi_{1}+\Psi_{2}$ and $\Delta=\Delta_{1}+\Delta_{2}$ and
$\mathfrak{n}=\mathfrak{n}_{1}+\mathfrak{n}_{2}$ and such that for each
$i=1,2$ we have
$\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}\mathbf{v}:\mathcal{S}_{i}$
and $\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$. By IH on $\pi_{1}$ with
$\zeta_{1}$ and $\pi_{2}$ with $\zeta_{2}$ we have
$\pi^{\prime}_{1}\rhd\Phi_{1}+\Psi_{1};\Gamma_{1}+\Delta_{1}\vdash^{\mathfrak{m}_{1}+\mathfrak{n}_{1}}s\\{x:=\mathbf{v}\\}:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$
and
$\pi^{\prime}_{2}\rhd\Phi_{2}+\Psi_{2};(\Gamma_{2},y:\mathcal{N}^{?})+\Delta_{2}\vdash^{\mathfrak{m}_{2}+\mathfrak{n}_{2}}r\\{x:=\mathbf{v}\\}:\mathcal{T}$.
By Lemma 2 and $\alpha$-conversion we can write
$(\Gamma_{2},y:\mathcal{N}^{?})+\Delta_{2}$ as
$\Gamma_{2}+\Delta_{2},y:\mathcal{N}^{?}$. Applying rule t-ifSucc with
$\pi^{\prime}_{1}$, $\pi^{\prime}_{2}$ and (1) as premises we conclude with
$\pi^{\prime}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}\mathsf{if}(s\\{x:=\mathbf{v}\\},u\\{x:=\mathbf{v}\\},y.\,r\\{x:=\mathbf{v}\\}):\mathcal{T}$.

  9. 9.

t-fix. Then $\pi\rhd\Phi_{0}+_{i\in I}\Phi_{i};\Gamma_{0}+_{i\in
I}\Gamma_{i},x:\mathcal{S}^{?}_{0}+_{i\in
I}\mathcal{S}^{?}_{i}\vdash^{[\texttt{F}]+\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}}\mathsf{fix}\,y.\,s:\mathcal{T}$ where
$\Phi=\Phi_{0}+_{i\in I}\Phi_{i}$ and $\Gamma=\Gamma_{0}+_{i\in I}\Gamma_{i}$
and $\mathcal{S}^{?}=\mathcal{S}^{?}_{0}+_{i\in I}\mathcal{S}^{?}_{i}$ and
$\mathfrak{m}=[\texttt{F}]+\mathfrak{m}_{0}+_{i\in I}\mathfrak{m}_{i}$ and
$t=\mathsf{fix}\,y.\,s$. The judgment is derived from
$\pi_{0}\rhd\Phi_{0},y:\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0},x:\mathcal{S}^{?}_{0}\vdash^{\mathfrak{m}_{0}}s:\mathcal{T}$ and
$\pi_{i}\rhd\Phi_{i};\Gamma_{i},x:\mathcal{S}^{?}_{i}\vdash^{\mathfrak{m}_{i}}\mathsf{fix}\,y.\,s:\mathcal{U}_{i}$
for each ${i\in I}$. We may assume $y\notin\\{x\\}\cup\mathsf{fv}(\mathbf{v})$