# Sequences and Infinitary Intersection Types

Pierre Vial  Inria Paris-Saclay, France<EMAIL_ADDRESS>
###### Abstract.

We introduce a new representation of non-idempotent intersection types, using
sequences (families indexed with natural numbers) instead of lists or
multisets. This allows scaling up intersection type theory to the infinitary
$\lambda$-calculus. We thus characterize hereditary head normalization, which
gives a positive answer to a question known as Klop’s Problem. On our way, we
use non-idempotent intersection to retrieve some well-known results on
infinitary terms.

###### Key words and phrases:

intersection types, infinitary lambda-calculus, coinduction, non-idempotent
intersection, sequence types, Böhm trees

##  1\. Presentation

Intersection types, introduceed by Coppo and Dezani [CDC78, CDC80a, MC81], are
a powerful tool to describe and characterize the semantic properties of
programs. For instance, compared to simple types, they type more terms, such
as $\Delta:=\lambda x.x\,x$, the self-application, and they allow building
models [BCDC83, ABD06, PPR17] for the $\lambda$-calculus. They also allow
capturing observational equivalence (see [Man17] for instance). Various sets
of $\lambda$-terms have been characterized with (a form of) typability within
intersection type systems.

The question was naturally raised to know whether some sets of programs
defined in terms of infinitary behaviors (for instance, as captured by Böhm
trees), such as the set of hereditary permutators (TLCA Problem # 20) could be
characterized in such a system. In particular, this led Klop and Dezani to
formulate the following question [Tat08a]: can the set of hereditary head
normalizing terms (i.e., the terms whose Böhm tree does not contain $\bot$) be
characterized by means of an intersection type system? This question was known
as Klop’s Problem. One may perhaps undestand better the definition of
hereditary head normalizing terms by interpreting them as a generalization of
weakly normalizing terms (terms which have a $\beta$-normal form) in that, $t$
is hereditary head normalizing if, at any fixed depth $d$, $t$ can be reduced
to a normal form up to subterms which occur below depth $d$. Such a term may
not have a normal form: this occurs whenever redexes cannot be completely
eliminated by reducing $t$, even if the redexes (of the reducts) of $t$ keep
on increasing in depth. For instance, $\mathtt{Y}_{f}:=\Delta_{f}\,\Delta_{f}$
(with $\Delta_{f}=\lambda x.f(x\,x)$) a variant of Curry fixpoint that will be
the case study of this article, satisfies
$\mathtt{Y}_{f}\rightarrow_{\mathtt{h}}f(\mathtt{Y}_{f})$ (it operational
semantics is given in Fig. 1). Thus, after $n$ steps of reductions,
$\mathtt{Y}_{f}$ gives $f^{n}(\mathtt{Y}_{f})$ (shortening
$f(f(\ldots(\mathtt{Y}_{f}))))$ with $n$ occurrences of $n$), which, on one
hand, shows that $\mathtt{Y}_{f}$ is not weakly normalizing, since its reducts
all have a (unique) redex. On another hand, the only redex of
$f^{n}(\mathtt{Y}_{f})$ occurs at depth $n$, which means that, above depth
$n$, $f^{n}(\mathtt{Y}_{f})$ is an normal form. Asymptotically, when $n$
converges towards $\infty$, the computation of $\mathtt{Y}_{f}$ outputs an
infinite $\lambda$-tree (corresponding to a infinite application of $f$, which
we call $f^{\infty}$) which does not contain any redex: in other words, an
infinite normal form. And this is the core reason why hereditary head
normalization pertains to an infinitary behavior.

$\mathtt{Y}_{f}$$\char 64\relax$$f$$\mathtt{Y}_{f}$$\char 64\relax$$f$$\char
64\relax$$f$$\mathtt{Y}_{f}$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\mathtt{Y}_{f}$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\char
64\relax$$f$$\mathtt{Y}_{f}\longrightarrow_{\beta}$$f(\mathtt{Y}_{f})\longrightarrow_{\beta}$$f^{2}(\mathtt{Y}_{f})\longrightarrow_{\beta}$$f^{3}(\mathtt{Y}_{f})\longrightarrow^{*}_{\beta}$$f^{n}(\mathtt{Y}_{f})$

Figure 1. $\mathtt{Y}_{f}$, a Hereditary Normalizing Term

However, Tatsuta [Tat08a, Tat08b] proved in 2008 that “infinitary behaviors”
could not be characterized in an inductive, finitary setting. In particular,
the answer to Klop’s Problem is negative in the inductive case, as Tatsuta
showed by:

  * •

making the observation that, in an inductive type system, the set of typable
terms is recursively enumerable.

  * •

proving that the set of hereditary head normalizing termsis not recursively
enumerable.

In turn, this result raised the question of whether such a characterization
could be obtained by means of an infinitary/coinductive intersection type
system.

In this article, we prove that it is possible and we give a type-theoreric
characterization of hereditary head normalization using non-idempotent
intersection. Non-idempotent intersection type systems were introduced in 1980
by Coppo, Dezani and Veneri [CDC80b] before being rediscovered by Gardner
[Gar94] and de Carvalho in his PhD [Car07, dC18], which emphasized they
quantitative aspect. They have been since extensively studied (read [BKV17]
for a survey). Non-idempotent intersection $\wedge$ does not satisfy the
equality $A\wedge A=A$ as the set-theoretic intersection does ($X\cap X=X$).
In its simplest form of this system, non-intersection is represented with
multisets (the multiset $[A,B,A]$ stands for the intersection $A\wedge B\wedge
A$) and gives a typing system with only three rules, which is recalled in Sec.
3.4. Then, reduction inside a derivation almost boils down to moving parts of
the initial derivation (see Fig. 13 and discussion in Sec. 5.4) and the proof
of soundness (if a term is typable, then it is head normalizing) becomes
trivial, since reduction decreases a positive integral measure on derivations.

To solve Klop’s Problem, we will use a quantitative, resource-aware type
system. However, it turns out that a direct coinductive adaptation of infinite
multisets cannot work for two major reasons:

  * •

It would lead to the possibility of typing some unsolvable terms111We actually
proved that the coinductive version of $\mathscr{R}_{0}$ types every term can
typed in $\mathscr{R}$, the coinductive version of $\mathscr{R}_{0}$ [Via18],
like $\Omega$. That is why a validity criterion is needed to discard
irrelevant derivations, as in other infinitary frameworks [San01]. This
validity criterion relies on the idea of approximability (every valid infinite
derivation must be, in some sense, a limit of finite derivations), which we
informally develop in Sec. 2.4, 3.6, 3.7 and formally define in Sec. 6.

  * •

Moreover, as it turns out, multisets are not fit to formally express such a
notion, because they do not allow pointing, meaning for instance that we
cannot distinguish the two occurrences of $\sigma$ in $[\sigma,\tau,\sigma]$.
This motivates the need for rigid constructions: multisets are then
(coinductively) replaced by sequences, i.e., families indexed by (non
necessarily consecutive) natural numbers called tracks (e.g.,
$(2\cdot\sigma,3\cdot\tau,9\cdot\sigma)$ instead of $[\sigma,\tau,\sigma]$).
We explain all this in Sec. 2.4 below.

This leads us to define a type system that we call system $\mathtt{S}$, in
which intersection is represented by sequences of types (intersection is said
to be sequential). Tracks, which act as identifiers, constitute the main
feature of system $\mathtt{S}$ presented here. With those pointers, any type
can be tracked through the rules of a whole typing derivation, and the
notionsof approximation and of limit of a family of derivation can be defined.

This contribution was presented in [Via17] with some proof sketches. Here, not
only we provide full proofs (which are detailled in appendices), but in the
core of the paper, we detail a crucial argument of soundness (if a term is
suitably typable, then it has a finite or infinite normal form). We also
explain in more details how infinite normal forms can be suitably typed.

The expert reader on intersection types may be surprised by the following
elements: while the subject reduction property (in its usual form) remains
simple to prove, soundness (typability implies normalization) and (infinitary)
subject expansion are quite more technical than in the usual, finite non-
idempotent case. The use of a validity criterion constrains us to prove
subject reduction while considering residuals (Sec. 5.3 and 5.5).
Approximability (derivation are limits of finite ones) raises a problem with
the left-hand side of judgments, which can be overcome by showing that they
can be, in some sense, ignored (Sec. 6.2). Typing normal forms soundly is also
technical, because we must check that it can be done while respecting
approximability (Sec. 7.1 to 7.3). At last, infinitary subject expansion is a
subtle process, based on cutting infinite derivations into finite ones,
proceeding to a substitution in a reduction path of infinite length followed
by a finite number of expansion stepsn, and then considering a suitable join
of the underlying constructions. It is incrementally explained in Sec. 2.3,
3.6 and 7.4.

### Structure of the paper.

This article is organized as follows: in Sec. 2, we recall the mechanisms of
intersection types on which we will base our approach and we present the main
difficulties we shall have to overcome, along with a sketch of the tools we
develop in this article. In Sec. 3, we formally recall the infinitary
$\lambda$-calculus and the finitary non-idempotent intersection type system of
Gardner-de Carvalho (system $\mathscr{R}_{0}$) which use multisets to
represent intersection. Sec. 3.4 is partly informal: we explain how we will be
able to perform later in this article infinitary subject expansion (bring a
typing backwards along an infinite sequence of reduction steps) and why this
actually cannot be done with multiset intersection. In Sec. 4, we formally
define system $\mathtt{S}$ and sequence types. In Sec. 5, we study the one-
step dynamics of system $\mathtt{S}$: we define residuals and we prove a
deterministic subject reduction property and the subject expansion property
Approximability is defined in Sec. 6 and the infinitary subject reduction
property and the normalization of typable terms are proved. Sec. 7 is devoted
to typing infinite normal forms and proving the infinitary subject expansion
property. This concludes the study of Klop’s Problem and of hereditary head
normalization.

This brings us to the main contribution of this article, Theorem 4: from Sec.
3.6 to Sec. 7, we solve Klop’s Problem: we give a type theoretic
characterization of hereditary head normalization. A general presentation of
the content of the appendices, in which we give technical arguments that may
be missing, is given on p. Contents of the appendices..

##  2\. Introduction

In this section, we first recall basic notions on normalization, then we
present some aspects of intersection types. We then devote our attention to
Klop’s Problem and the technical difficulties we had to overcome and the proof
techniques we had to introduce to export intersection type theories to an
infinitary setting and to characterize hereditary head normalization. Last, we
present two main tools that we use in this article: sequences and
approximations/truncations of derivations.

###  2.1. Normalization

### Evaluation strategies

We consider the following restrictions of $\beta$-reduction:

  * •

The head reduction, denoted $\rightarrow_{\mathtt{h}}$, consists in reducing
the head redex $(\lambda x.r)s$ of a head reducible term $\lambda x_{1}\ldots
x_{p}.(\lambda x.r)s\,t_{1}\ldots t_{q}$ (notice that any term that is not a
HNF is head reducible). A term $t$ is Head Normalizing (HN) if the head
reduction terminates on $t$ (and necessarily outputs a head normal form).

  * •

The leftmost-outermost reduction, denoted $\rightarrow_{\ell}$, consists in
reducing the leftmost-outermost redex of a $\beta$-reducible term $t$, i.e.,
the one whose $\lambda x$ is the leftmost one in $t$ (seen as string of
characters). A term $t$ is Weakly Normalizing (WN) if leftmost-outermost
reduction terminates on $t$ (and necessarily outputs a full normal form).

  * •

The hereditary head reduction strategy (formally defined in Sec. 3.3) also
aims at computing a full normal form: for a given term $t$, it starts by
applying the head reduction strategy on $t$ until it stops (otherwise, it
loops). In that case, the current term is of the form $\lambda x_{1}\ldots
x_{p}.x\,t_{1}\ldots t_{q}$. Then one applies the head reduction strategy on
each head argument $t_{1},\ldots,\;t_{q}$ until they are all in head normal
forms (if it does not loop for one of the $t_{i}$). Then one goes on with head
reducing each new argument at constant applicative depth and so on. The
strategy stops if a $\beta$-normal form is reached. Hereditary head reduction
may be seen as a more balanced variant of leftmost-outermost reduction.
Moreover, when hereditary head reduction strategy does not stop but keeps on
reducing deeper and deeper, it may be seen as asymptotically computing an
infinite term, as it was recalled above.

### Having a normal form

Normalization may also be associated with reduction paths of unspecified forms
(without referring to evaluation strategies). In this article, we mainly
consider the two predicates:

  * •

A $\lambda$-term $t$ has a head normal form if there is a reduction path from
$t$ to a head normal form.

  * •

A term $\lambda$-term $t$ has a full normal form if there is a reduction path
from $t$ to a full normal form.

Notice that having a head normal form seems to be more general/less
constrained than head normalization: the former pertains to the existence of a
reduction path (to a head normal form) of an unspecified form whereas the head
reduction reduces terms in a deterministic way. Thus, if the head reduction
strategy terminates on a term $t$, then $t$ clearly has a head normal form.
Moreover, it is well-known of that the converse of these two implications is
true, i.e., if a term $t$ has a head normal form then the head reduction
strategy terminates on $t$.

###  2.2. Intersection Types

We recall and discuss here some aspects of intersection types that will
interest us in this article. All these aspects are illustrated in system
$\mathscr{R}_{0}$ in the forthcoming Sec. 3.4.

Normalization (termination) is a dynamic property: it pertains to the
reduction of $\lambda$-terms, i.e., their evaluation. For instance, proving
that a term $t$ is head normalizing consists (in principle) in giving a
sequence of $\beta$-reduction steps starting at $t$ and ending with a head
normal form.

On another hand, typing is static in the following sense: in a given type
system, finding a derivation typing a term $t$ or checking that a given tree
of typing judgments is a correct derivation is done without having to perform
reduction steps but just by considering the structure of the tree and
verifying that the typing rules are correctly applied.

One of the desirable features of type systems is that some of them ensure
normalization, e.g., if a term $t$ is typable in Girard’s system F, then it is
strongly normalizing [Gir72, GLT90] (i.e., no infinite reduction path starts
at $t$). Thus, type systems provide static proofs of dynamic properties. In
some systems, when we have managed to type a program $t$, we do not need to
execute $t$ to know that $t$ is terminating. However, usually, when typability
is related to termination, e.g., in polymorphic or dependent type systems, it
is a sufficient condition for normalization but not a necessary one: many
normalizing terms are not typable. For instance, $\Delta=\lambda x.x\,x$ is
not typable in the simply typed $\lambda$-calculus, and $(\lambda z.\lambda
y.y(z\,\mathtt{I})(z\,\mathtt{K}))(\lambda x.x\,x)$, although strongly
normalizing, is not typable in system F.

The basic idea behind intersection type systems is allowing assigning several
types to variables or to terms. They often characterize (and not only ensure)
normalization properties (head, weak, weak head, strong…): in an intersection
type system, typability is usually equivalent with (a notion of)
normalization. Since the $\lambda$-calculus is Turing-complete, this makes
type inference undecidable in most intersection type systems. As an exception
to this rule, intersection types were famously used by Kobayashi and Ong
[KO09] to prove that Monadic Second Order logic is decidable for higher-order
recursion schemes.

Normalization theorems in intersection type theory. Intersection type systems
often give interesting properties pertaining to reduction strategies. To
illustrate this, let us imagine for a moment that we have an intersection type
system $\mathcal{H}$ characterizing head normalization, i.e., that satisfies
the following theorem (let us call it $T_{\text{HN}}$):

“Theorem $T_{\text{HN}}$: for every $\lambda$-term $t$, $t$ is is typable in
system $\mathcal{H}$ iff $t$ is head normalizing ”

In practice, this characterization theorem is proved in two steps:

  * $\Rightarrow$

A proof of “If $t$ is $\mathcal{H}$-typable (typable in system $\mathcal{H}$),
then the head reduction strategy terminates on $t$”.

  * $\Leftarrow$

A proof of “If there is a reduction path from $t$ to a HNF, then $t$ is
$\mathcal{H}$-typable”.

Soundness
Typability implies
normalization Completeness
Normalization implies
typability some reduction strategy normalizes $t$ e.g., the head red.
strat.terminates on $t$ $t$ has a normal form e.g., $\exists$ red. path
from $t$ to a HNF $t$ is typable

Figure 2. Characterizing a notion of normalization with intersection types

Observe that for $\Rightarrow$, we actually prove that a typable $t$ is
terminating for the head reduction strategy, which is a priori stronger than
just the fact that $t$ has a head normal form. This proves that, in some
sense, head reduction is complete since it computes a head normal form when it
exists. Since the termination of head reduction obviously implies having a
head normal form, the implication $\Leftarrow$ gives us theorem
$T_{\text{HN}}$ but also the following, non-trivial statement:

“A term $t$ is head normalizing

iff it is terminating for the head reduction strategy.”

A remarkable aspect of this equivalence is that it is not type-theoretic: it
states that a certain reduction strategy is complete for a certain notion of
normalization. But it was proved using types instead of syntactic techniques.
The structure of this kind of proof is summarized in Fig. 2. The arrow on the
right (typability implies normalization, or soundness) usually relies on
subject reduction, whereas the arrow on the left (normalization implies
typability, or completeness) relies on subject expansion (typing is stable
under expansion). To the best knowledge of the author, subject expansion is
specific to intersection type system, unless it is hard-coded in the typing
rules. Indeed, to perform subject expansion (going from a typing of $r[s/x]$
to one of $(\lambda x.r)s$), the variable $x$ can be assigned several types
and thus, be used as a placeholder for $s$, which can occur with several
different types in $r[s/x]$.

### Partial typings.

The possibility to partially type terms will be crucial in the core of this
article, when we need “truncate” infinite derivations typing infinite terms
into finite derivations: many intersection type systems also feature a
universal type $U$ which can be assigned to every term, so that a judgment of
the form $t:U$ is meaningless. However, such a meaningless $U$ allows
partially typing a term. Actually, every head normal form becomes typable: if
one assigns $U\rightarrow\ldots\rightarrow U\rightarrow A$ (with $n$ arrows)
and types the $t_{i}$ with $U$, then $x\,t_{1}\ldots t_{q}$ has type $A$). The
possibility to leave some arguments untyped is crucial for type systems to
remain sound while ensuring semantic guarantees are less restrictive than
strong normalization (e.g., head or weak normalization). When considering such
a universal type $U$, every term becomes typable and thus, typed judgments
should be considered sound only when $U$ does not have ill-placed occurrences,
called positive occurrences (technically, an occurrence is positive when it is
nested in an even number of arrow domains).

$\mathtt{ax}$$x:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{1}}$$\mathtt{ax}$$x:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{2}}$$\mathtt{ax}$$x:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{1}}$$\ldots,x:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{[A_{1},A_{2},A_{1}]}\vdash
r:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{B}$$\ldots\vdash\lambda
x.r:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{[A_{1},A_{2},A_{1}]\rightarrow
B}$$\Pi^{a}_{1}$$s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{1}}$$\Pi_{2}$$s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{2}}$$\Pi^{b}_{1}$$s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{1}}$$(\lambda
x.r)s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{B}$Non-
idempotently typed
redex$\Pi^{a}_{1}$$s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{1}}$$\Pi_{2}$$s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{2}}$$\Pi^{b}_{1}$$s:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{A_{1}}$$r[s/x]:\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{B}$Derivation
reduct Non-idempotency: • $x:[A_{1},A_{2},A_{1}]$ $\leadsto$ in $r$, $x$ has
been typed twice with $A_{1}$ and once with $A_{2}$ • In the redex, 3 arg.
derivations because $x$ typed 3 times • During reduction, duplication is
disallowed for types
(no arg. derivation typing is duplicated) • After reduction, the derivation
has decreased in size
(1 $\mathtt{app}$, 1 $\mathtt{abs}$ and 3 $\mathtt{ax}$-rules destroyed)

Figure 3. Non-Idempotent Typing, Reduction and Decrease

### Non-idempotent intersection

When intersection operator is not idempotent [CDC80b, Gar94, dC18], the types
$A$ and $A\wedge A$ are not equivalent anymore. This expresses the fact that,
from the quantitative point of view, using the type $A$ once or twice is not
the same. Thus, non-idempotent intersection is closely related to Girard’s
Linear Logic [Gir87]. For instance, non-idempotent type systems keep
information on how many times a variable has been assigned a type. A powerful
consequence of this is that reduction cause derivations to decrease in size
during reduction, meaning that if $\Pi$ concludes with $\Gamma\vdash t:\tau$
and $t$ head-reduces to $t^{\prime}$, then $\Pi^{\prime}$, the derivation
reduct of $\Pi$ concluding with $\Gamma\vdash t^{\prime}:\tau$, contains
stricly less judgments than $\Pi$. This illustrated with Fig. 3. This entails
that it is trivial that a typed term is head normalizing.

###  2.3. Solving Klop’s Problem

Now that we have recalled some useful fact about intersection types, we
explain in this section what are the difficulties we will meet and overcome in
this article to export (non-idempotent) intersection type theory to an
infinitary setting.

Soundness in an infinitary setting, and the need of a fine-grained notion of
residuation. In the case of finitary non-idempotent intersection type,
soundness is just based on the subject reduction property inducing the
decrease of a positive integral measure and is comparatively very simple to
prove. In the infinitary case, things are different: the soundness of a
derivation $P$ is ensured provided $P$ is, in some sense, the limit object of
finite derivations (this is the core of the approximability criterion). To be
more precise:

  * •

Defining infinite derivations by just allowing infinitary multiplicites and
nestings in multisets is unsound: for instance, the looping term $\Omega$
becomes typable. This is why we need the approximability criterion (Sec. 3.7).

  * •

If a term $t$ is typed with an approximable derivation, which is a possibly
infinite derivation that can be written as a limit (or the join) of finite
derivations, then $t$ is necessarily typable in the finitary, usual setting,
which ensures soundness (in the sense that, in the finite case, if $t$ is
typable, then it is head normalizing).

  * •

But the necessity of handling the notion of approximability while reducing
derivations (i.e., reducing there subjects) constrain us to have a more
meticulous description of the subject reduction property. Indeed, we need to
show that approximability is stable under reduction. But for this, as it will
be made clear in the paper, we need to have a precise, fine-grained notion of
residuation (Sec. 5.3 and 5.5).

  * •

At last, residuation raises a problem of its own. As we shall see, residuation
can be suitably defined only for the right-hand sides $t:T$ of typing
judgments $C\vdash t:T$ (where $C$ is the context, $t$ the subject and $T$ the
type), whereas approximability pertains to their left-hand sides too. We
explain how to overcome this problem with the crucial notion of equinecessity
(Sec. 6.2).

The infinite jump problem, or infinitary subject expansion. Another problem in
the infinitary setting is ensuring infinitary subject expansion: actually,
proving that typing is stable under one-step expansion is not really more
difficult than it is in the finite case. However, a suitable notion of
reduction path of infinite length (the so)-called productive paths, Sec. 3.3)
naturally arises when we deal with infinite terms and Böhm tree [KKSdV97]. As
a side remark, one-step subject reduction and even infinitary subject
reduction along a productive path are also trivial (as long as we do not
consider the question of approximability): the latter can be also thought as a
limit process of a finite number of reduction steps. In other words, one may
say that infinitary subject reduction is an asymptotic phenomenon. However,
the situation is different for infinitary subject expansion, because
intuitively there is a priori no way to pass incrementally222To give an idea,
if we consider a sequence of rational numbers $(x_{n})_{n\in\mathbb{N}}$ which
converges to a limit $x$ (which is rational or irrational), then passing from
$x$ to any $x_{n}$ means going backward on $\infty-n$ (which is also $\infty$)
many steps! In this respect, this is not incremental. from a limit object to
one of a finite rank (let us call that very informally the infinite jump
problem). Infinitary subject expansion is not asymptotic in nature. But as, we
shall see in Sec. 3.6, infinitary subject expansion can be performed and we
may already give some elements of understanding on the involved techniques: on
one hand, our notion of soundness—approximability—specifies that infinite
derivations are static limits of finite ones (by static, we mean that the
definition of approximability is independent from any notion of reduction). On
another hand, we have the usual notion of productive reduction paths of
infinite length in the infinitary $\lambda$-calculus, which defines a dynamic
notion of limit of a family of term: this limit is intuitvely the term which
is asymptotically outputted after an infinite number of reduction steps, as in
the example of $\mathtt{Y}_{f}$ on page 3.4.

Interestingly enough, the core technique used to perform infinitary subject
expansion is also based on approximability, and actually, on confronting these
two notions (static vs. dynamic) of limits: we use the fact that derivations
are static limits of finite derivations to (1) perform infinite subject
expansion on these finite derivations (for which the infinite jump probem has
a solution, Sec. 3.5) (2) statically build a (possibly infinite) expanded
derivation by taking the join of the resulting finite expanded derivations.

Thus, approximability is pivotal in two respects: (1) it is used to define
which infinitary derivations are semantically valid and which are not (2) it
is used to perform infinitary subject expansion.

The problem of pointing. A last technical ingredient to adapt intersection
type theory to an infinitary setting is what we call sequences in this
articles: multisets of elements which are decorated with suitable natural
numbers which we call tracks. In non-idempotent intersection type theory, it
is convenient (but not mandatory) to represent the intersection of types
$A_{1}$,…,$A_{k}$ with the multiset $[A_{1},\ldots,A_{k}]$: it allows not
needing anymore structural rules and simplifying the type system. However, it
has two drawbacks for us: it makes it impossible to have a pointing mechanism
(in the multiset $[A,B,A]$, it is impossible to point formally to one specific
occurrence of $A$) and it gives rise to non-determinism in proof reduction as
it is well-known (Sec. 5.4). Both problems, as we shall see, make it
impossible to define approximability and ensure soundness. When elements are
decorated with tracks (for instance, $[A,B,A]$ may become $(2\cdot A,4\cdot
B,7\cdot A)$ or $(3\cdot A,2\cdot B,9\cdot A)$), we recover pointing and
determinism. For instance, in $(2\cdot A,4\cdot B,7\cdot A)$, one occurrence
of $A$ is on track 2 (i.e., is decorated with 2) and the other is on track 7.
Actually, this tracking mechanism enables a fine-grained description of
residuation on typing derivation and prove soundness, as we saw just above.

###  2.4. A Glimpse at Sequences and Derivation Approximations

Now, let us give a glimpse at the notion of sequences (which refines that of
multisets) and of approximation of a derivation.

Sequences and tracking. Naive multisets do not allow defining a notion of
position: we say that they do not allow tracking. To see this, consider the
equality $[A,B,A]=[A,B]+[A]$. There is no way to associate the occurrence of
$A$ in $[A]$, located in the right-hand side of the equality to one of the two
occurrences of $A$ in $[A,B,A]$, in the left-hand side. This shows that there
is not way to point to a particular occurrence of $A$ inside $[A,B,A]$.
Actually, if we swap the two occurrences of $A$ in $[A,B,A]$, we obtain
$[A,B,A]$. If we do not do anything, we also obtain $[A,B,A]$: the possible
swap cannot be seen. It has actually no formal meaning.

To retrieve tracking and thus, the possibility to point at an element, we may
annotate elements of multisets with pairwise distinct integers, that we call
tracks. Such a decorated multiset is called a sequence and we use the
constructor $(\\_)$ for sequences instead of $[\\_]$ for multisets. For
instance, $(2\cdot A,3\cdot B,5\cdot A)$ is a sequence, there is one
occurrence of $A$ on track 2 and another on track 5. Sequences come along with
a disjoint union operator $\uplus$, e.g., $(2\cdot A,3\cdot B,5\cdot
A)=(2\cdot A,3\cdot B)\uplus(5\cdot A)$. Thanks to tracks, each occurrence of
$A$ in one side of the equality are unambiguously associated with another on
the other side, and in the left-hand side, we may point to the occurrence of
$A$ on track 2 rather than the one on track 5. Disjoint union is not defined
for two sequences sharing a same track, e.g., $(2\cdot A,3\cdot
B)\uplus(3\cdot B,5\cdot A)$ is not defined (because the two operands both use
track 3, even though the same type $B$ occurs): we say that there is a track
conflict. Moreover, $\uplus$ is a commutative and associative, but partial
operator. Observe that $(2\cdot A,3\cdot B,5\cdot A)$ may be written six
different ways, e.g., $(5\cdot A,2\cdot A,3\cdot B)$ and $(2\cdot A,5\cdot
A,3\cdot B)$: if we perform a swap in a sequence, we see it.

Our framework is deterministic, e.g., there is a unique canonical way to
produce a derivation from another one when reducing a redex, contrary to
system $\mathscr{R}_{0}$, and we can characterize infinitary semantics (more
details in Sec. 5.4).

To sum up, in many ways, sequence types work like multiset types, e.g., they
give rise to a syntax-directed, strict and relevant typing system with only
three rules, but they allow tracking, constructing a suitable pointing
mechanism inside derivations and thus, defining approximability, the validity
criterion that will help us discard the unsound coinductive derivations. This
will enable us characterizing hereditary head normalization.

Approximation. As we have hinted at in Sec. 2.3, coinductive type grammar give
rise to unsound derivations, e.g., derivations typing of $\Omega$, but we
introduce a validity criterion allowing to discard them. This criterion is
called approximability. Intuitively, an infinite proof/typing derivation is
approximable when it is obtained by superposing infinitely many finite proofs,
growing over and over, as in Fig. 4: the outer triangle represents an infinite
proof/typing derivation $\Pi$ and the inner polygons represent finite proofs
that “fit” in $\Pi$. Thus, an approximable derivation may be infinite, but it
is asymptotically obtained from finite/sound proofs. Equivalently, a
derivation is approximable when it is the join of its finite truncations, also
called approximations. The crucial intuition behind this notion is that it
allows “reducing” infinite derivations to finite ones along with the soundness
properties that come with them, such as head normalization.

Figure 4. An Approximable Derivation as an Infinite Superposition

More precisely, derivations need not being infinite to characterize head
normalization in the infinite calculus: infinite derivations are required to
characterize hereditary head normalization in an infinitary calculus, because
we need to type infinite normal forms without leaving any subterm untyped.
Moreover, finite derivations allow us to prove operational properties of the
infinite calculus in a relatively simple way (more details in Sec. 3.5). An
important idea is that any term which is approximably typable is finitarily
typable and as such, is head normalizing. The whole proof of correctness of
the system (w.r.t. hereditary head normalization) is based on this
observation.

Just to give a more precise idea of what is meant by superposition, the
derivation fragment $\Pi_{2}$ below can be superposed upon $\Pi_{1}$ (we omit
the typing assumptions and the possible premises of the top judgments):

$\Pi_{1}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\mathtt{f}:(A\wedge B)\rightarrow
A\rightarrow C\hskip 14.22636pt\mathtt{x}:A\hskip
14.22636pt\mathtt{x}:B$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=145.26624pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
47.45197pt\hbox{$\displaystyle\mathtt{f}(\mathtt{x}):A\rightarrow C$}}}}$
$\Pi_{2}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\mathtt{f}:(A\wedge
B\wedge(B\rightarrow C))\rightarrow(A\wedge C)\rightarrow D\hskip
14.22636pt\mathtt{x}:A\hskip 14.22636pt\mathtt{x}:B\hskip
14.22636pt\mathtt{x}:B\rightarrow D$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=270.36441pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
96.6254pt\hbox{$\displaystyle\mathtt{f}(\mathtt{x}):(A\wedge C)\rightarrow
C$}}}}$

Indeed, $\Pi_{1}$ is obtained from $\Pi_{2}$ by removing the symbols colored
in red:

$\Pi_{2}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\mathtt{f}:(A\wedge
B\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\wedge(B\rightarrow
C)})\rightarrow\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(}A\wedge\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{C)}\rightarrow
D\hskip 14.22636pt\mathtt{x}:A\hskip 14.22636pt\mathtt{x}:B\hskip
14.22636pt\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathtt{x}:B\rightarrow
D}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=265.36453pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
95.51431pt\hbox{$\displaystyle\mathtt{f}(\mathtt{x}):\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(}A\wedge\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{C)}\rightarrow
C$}}}}$

Thus, $\Pi_{1}$ can be seen as a truncation or an approximation of $\Pi_{2}$.
Infinite superposition strongly hints at the presence of complete lattices and
complete partial orders, which is formalized in Sec. 6.

With this concept of approximation, we retrieve, in an infinitary setting, the
main tools of finite intersection type theory that we sketched in Sec. 2.2:
subject reduction, subject expansion, typing of normal forms). Actually,
following the scheme of Fig. 2, we will prove that hereditary head reduction
(Sec. 3.2) is asymptotically complete for infinitary weak normalization.

##  3\. Finite Intersection and Infinite Terms

In Sec. 3.2 and 3.3, we define the infinitary $\lambda$-calculus and Böhm
trees. Gardner-de Carvalho’s system $\mathscr{R}_{0}$ is recalled in Sec. 3.4,
in particular how weak normalization is characterized by considering
unforgetful derivations. In Sec. 3.5, we explain how system $\mathscr{R}_{0}$
can still be applied to infinite terms. We encounter a first use of subject
substitution, i.e., replacing the subject $t$ of a derivation $\Pi$ by another
$u$ which is equal to $t$ in the typed parts of $\Pi$. We use this to perform
an infinite subject expansion on finite derivations. We present the main ideas
to solve Klop’s Problem in Sec. 3.6 and 3.7: we informally explain (1) how
infinitary subject expansion could be performed by truncating derivations and
taking the joins of directed families (2) how coinduction gives rise unsound
derivations, e.g., derivations typing the unterminating term $\Omega$ and how
soundness can be retrieved with approximability.

###  3.1. Pointing in a $\lambda$-term

Variable $x$$x$Abstraction $\lambda x.u$$u$0$\lambda x$Application $u\,v$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{2}$$v$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{1}$$u$$\char
64\relax$

Figure 5. Lambda Terms as Labelled Trees

Lambda terms can be seen as labelled trees following the pattern of Fig. 5. We
orient these labelled trees as typing derivation usually are: the root is put
at the bottom of the figure (and not at the top), because the derivations of
the type system to come can be represented as refinements of parsing trees of
$\lambda$-terms (see in particular Fig. 11 on p. 11). We say that $u$ is the
argument of the application $t\,u$. This representation gives to the standard
notions of positions in a $\lambda$-term, represented as words on
$\\{0,1,2\\}$ (the set of words on $\\{0,1,2\\}$ is denoted
$\\{0,1,2\\}^{*}$), and support $\mathtt{supp}(t)$ of a term $t$ (the set of
positions in $t$). If $b\in\mathtt{supp}(t)$, then $t(b)$ is the label at
position $b$ in $t$ and $t|_{b}$ is the subterm rooted at $b$. For instance,
if $t:=\lambda x.x\,y$, then $\mathtt{supp}(t)=\\{\varepsilon,0,0\cdot
1,0\cdot 2\\}$ where $\varepsilon$ is the empty word, $t(\varepsilon)=\lambda
x$, $t(0)=\char 64\relax$, $t(0\cdot 1)=x$, $t(0\cdot 2)=y$ and $t|_{0}=x\,y$.
The applicative depth ad of a position $b$ in a term $t$ is the number of
times that $b$ is nested inside the arguments of an application. For instance,
if $u_{1}\,u_{2}\,u_{3}\,u_{4}$ are terms and $t=\lambda
x.((y\,u_{1})((y\,u_{2})u_{3}))u_{4}$, $b_{1}=0\cdot 1^{2}\cdot 2$,
$b_{2}=0\cdot 1\cdot 2\cdot 1\cdot 2$, $b_{3}=0\cdot 1\cdot 2^{2}$,
$b_{4}=0\cdot 1$, then $t|_{b_{i}}=u_{i}$ and $\mathtt{ad}(b_{1})=1$,
$\mathtt{ad}(b_{2})=\mathtt{ad}(b_{3})=2$, $\mathtt{ad}(b_{4})=0$. In other
words, if $b=b_{0}\cdot b_{1}\ldots\cdot b_{n}$ (with $b_{i}$ integer), then
$\mathtt{ad}(b)=\\#\\{i\in\\{0,\ldots,n\\}\,|\,b_{i}=2\\}$, i.e.,
$\mathtt{ad}(b)$ is the number of 2 that $b$ contains.

###  3.2. Infinite Lambda Terms

In this section, we present Böhm trees (chapter 10 of Barendregt [Bar85], in
particular, Theorem 10.4.2.), a notion that was suggested by the proof of the
Böhm Separation Theorem, and the construction of one of the infinitary calculi
introduced in [KKSdV97]. See also [Cza14, EHH+15, Bah18] for alternative
presentations. This infinitary calculus is a natural framework which allows
expressing Böhm trees (more precisely, its normal forms are Böhm trees without
$\bot$), but it gives us more flexibility. For instance, the computation of an
infinite normal form does not need to follow the path given by hereditary head
normalization and we have a general notion of sound computations of infinite
length, that we call here productive reduction paths. We shall generalize some
notions to the whole infinitary calculus (for instance, hereditary head
normalization will pertain both to finite and infinite terms), since it gives
a general framework where they can be expressed.

We now generalize some of the notations of Sec. 3 in an infinitary setting.
Let $\mathscr{V}$ be a countable set of term variables. The set
$\Lambda^{\infty}$ of infinitary $\lambda$-terms is coinductively defined by:

$t,u~{}:=~{}x\in\mathscr{V}~{}\|~{}(\lambda x.t)~{}\|~{}(t\char 64\relax u)$

When there is no ambiguity, we usually just write $\lambda x.t$ and
$t\,u_{1}\ldots u_{n}$ instead of $(\lambda x.t)$ and $(\ldots(t\char 64\relax
u_{1})\ldots\char 64\relax u_{n})$. If $t$ is an infinitary term, then
$\mathtt{supp}(t)$, the support of $t$ (the set of positions in $t$) is
defined by $\mathtt{supp}(x)=\\{\varepsilon\\}$, $\mathtt{supp}(\lambda
x.t)=\\{\varepsilon\\}\cup 0\cdot\mathtt{supp}(t)$ and
$\mathtt{supp}(t\,u)=\\{\varepsilon\\}\cup 1\cdot\mathtt{supp}(t)\cup
2\cdot\mathtt{supp}(u)$ by coinduction. The notations $t(b)$ and $t|_{b}$ are
defined by induction on $b$.

Let $t\in\Lambda^{\infty}$. An infinite branch of $t$ is an infinite word
$\gamma$ over $\\{0,1,2\\}$ such all the finite prefixes of $\gamma$ are in
$\mathtt{supp}(t)$. The notion of applicative depth $\mathtt{ad}(\\_)$ is
straightforwardly extended to infinite branches:

######  Example 1.

  * •

Let us formally define $f^{\infty}$, the Böhm tree of $\mathtt{Y}_{f}$, by the
equation $f^{\infty}=f(f^{\infty})$, i.e., $f^{\infty}:=f(f(f(f(\ldots))))$ is
the labelled tree such that
$\mathtt{supp}(f^{\infty})=\\{2^{n}~{}|~{}n\in\mathbb{N}\\}\cup\\{2^{n}\cdot
1\,|\,n\in\mathbb{N}\\}$, $f^{\infty}(2^{n})=\char 64\relax$ and
$f^{\infty}(2^{n}\cdot 1)=f$ for all ${n\in\mathbb{N}}$. Then, $f^{\infty}$
has one infinite branch $2^{\infty}$, which is the infinite repetition of $2$:
indeed, for all $n\in\mathbb{N}$, $2^{n}\in\mathtt{supp}(f^{\infty})$. We have
$\mathtt{ad}(2^{\infty})=+\infty$.

  * •

Likewise, the infinite term ${}^{\infty}x\in\Lambda^{\infty}$ defined by
${}^{\infty}x=({}^{\infty}x)x$, so that ${}^{\infty}x=(((\ldots)x)x)x$
satisfies
$\mathtt{supp}({}^{\infty}x)=\\{1^{n}\,|\,{n\in\mathbb{N}}\\}\cup\\{1^{n}\cdot
2\,|\,{n\in\mathbb{N}}\\}$, so $\mathtt{supp}({}^{\infty}x)$ has the infinite
branch $1^{\infty}$ (this indicates a leftward infinite branch), which
satisfies $\mathtt{ad}(1^{\infty})=0$ since 2 does not occur in $1^{\infty}$.

If $b\in\mathtt{supp}(t)$, the subterm (resp. the constructor) of $t$ at
position $b$ is denoted $t|_{b}$ (resp. $t(b)$), e.g., if $t:=\lambda
x.(x\,y)z$ and $b=0\cdot 1$ (resp. $b=0\cdot 4$), then $t|_{b}=x\,y$ and
$t(b)=\char 64\relax$) (resp. $t|_{b}=t(b)=z$).

######  Definition 1 (001-Terms).

Let $t\in\Lambda^{\infty}$. Then $t$ is a 001-term, if, for all infinite
branches $\gamma$ in $\mathtt{supp}(t)$, $\mathtt{ad}(\gamma)=\infty$. The set
of 001-terms is denoted $\Lambda^{001}$.

Once again, the vocable “001-term” comes from [KKSdV97]. For instance,
$f^{\infty}$ is a 001-term since its unique infinite branch $2^{\infty}$
satisfies $\mathtt{ad}(2^{\infty})=+\infty$, whereas ${}^{\infty}x$ defined
above is not a 001-term since its infinite branch $1^{\infty}$ satisfies
$\mathtt{ad}(1^{\infty})=0$.

###  3.3. The computation of Böhm trees

Let $t,u\in\Lambda^{\infty}$. The notation $t[u/x]$ denotes the term obtained
from $t$ by the capture-free substitution of the occurrences of $x$ with $u$
(a formal definition can be found in [KKSdV97] in the infinitary setting). One
easily checks that if $t,u$ are 001-terms, then $t[u/x]$ also is a 001-term.
The $\beta$-reduction $\rightarrow_{\\!\beta}$ is obtained by the contextual
closure of $(\lambda x.t)u\rightarrow_{\\!\beta}t[u/x]$ and
$t\stackrel{{\scriptstyle b}}{{\rightarrow}}_{\\!\beta}t^{\prime}$ denotes the
reduction of a redex at position $b$ in $t$, e.g., $\lambda y.((\lambda
x.x)u)v\stackrel{{\scriptstyle 0\cdot 1}}{{\rightarrow}}_{\\!\beta}\lambda
y.u\,v$. Thus, the relation $t\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}t^{\prime}$ is defined by induction on
$b\in\\{0,\,1,\,2\\}^{*}$.

$\begin{array}[]{c@{\sep}c@{\sep}c@{\sep}c@{\sep}c}{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
36.3524pt\hbox{$\displaystyle\penalty 1\phantom{t}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=76.31592pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle(\lambda
x.r)s\stackrel{{\scriptstyle\varepsilon}}{{\rightarrow}}_{\\!\beta}r[s/x]$}}}}\hfil\hskip
14.22636pt&{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 20.93744pt\hbox{$\displaystyle\penalty
1t\stackrel{{\scriptstyle b}}{{\rightarrow}}_{\\!\beta}t^{\prime}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=63.25319pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle\lambda
x.t\stackrel{{\scriptstyle 0\cdot b}}{{\rightarrow}}_{\\!\beta}\lambda
x.t^{\prime}$}}}}\hfil\hskip 14.22636pt&{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
12.39212pt\hbox{$\displaystyle\penalty 1t_{1}\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}t_{1}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=50.22256pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
t_{1}\,t_{2}\stackrel{{\scriptstyle 1\cdot
b}}{{\rightarrow}}_{\\!\beta}t^{\prime}_{1}\,t_{2}$}}}}\hfil\hskip
14.22636pt&{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1t_{1}\,t_{2}\stackrel{{\scriptstyle
2\cdot b}}{{\rightarrow}}_{\\!\beta}t_{1}\,t_{2}^{\prime}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=51.48259pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 13.65213pt\hbox{$\displaystyle
t_{2}\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}t^{\prime}_{2}$}}}}\hfil\hskip
14.22636pt&{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1t\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}t^{\prime}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=21.37831pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 1.50208pt\hbox{$\displaystyle
t\rightarrow_{\\!\beta}t^{\prime}$}}}}\end{array}$

The notion of normal form generalizes to $\Lambda^{001}$, e.g., a 001-Normal
Form (001-NF) is a 001-term that does not contain a redex. Thus, the set of
001-NF, denoted $\text{NF}_{\infty}$, can be defined coinductively by:

$t,\,t_{i}~{}::=~{}\lambda x_{1}\ldots x_{p}.x\,t_{1}\ldots
t_{q}~{}(p,q\geqslant 0)$

A term $t\in\Lambda^{001}$ is head normalizing if
$t\rightarrow_{\mathtt{h}}^{*}\lambda x_{1}\ldots x_{p}.x\,t_{1}\ldots t_{q}$
(with $t_{1},\ldots,t_{q}\in\Lambda^{001}$), which is a head normal form. A
term $t\in\Lambda^{001}$ is has a head normal form if there is a finite
reduction path from $t$ to a head normal form $t^{\prime}$ (i.e.,
$t\rightarrow_{\\!\beta}t^{\prime}$). In particular, the implication “$t$ is
head normalizing” $\Rightarrow$ “$t$ has a head normal form” straightforwardly
holds. The converse implication (“$t$ has a head normal form $\Rightarrow$ $t$
is head normalizing”) also holds, although the proof differs from the finite
cas [KKSdV97], and we will give a simple semantic proof of this fact in Sec.
3.5.

######  Definition 2 (Böhm tree of a term).

Let $t$ be a 001-term.
The Böhm tree $\mathtt{BT}(t)$ of $t$ is coinductively defined by:

  * •

$\mathtt{BT}(t)=\lambda x_{1}\ldots
x_{p}.x\,\mathtt{BT}(t_{1})\ldots\mathtt{BT}(t_{q})$ if
$t\rightarrow_{\mathtt{h}}^{*}\lambda x_{1}\ldots x_{p}.x\,t_{1}\ldots t_{q}$.

  * •

$\mathtt{BT}(t)=\bot$ if $t$ is not head normalizing.

For instance, $\mathtt{BT}(\Omega)=\bot$ where $\Omega=(\lambda
x.x\,x)(\lambda x.x\,x)$, if $t$ a 001-normal form then $\mathtt{BT}(t)=t$ and
$\mathtt{BT}(\mathtt{Y}_{f})=f^{\infty}$. Intuitively, the computation of Böhm
trees is done by a possibly infinite series of head reductions at deeper and
deeper levels. This corresponds to the asymptotic reduction strategy known as
hereditary head reduction.

More formally, we define $\rightarrow_{\mathtt{hh}}$, a non-deterministic
version of hereditary head reduction as follows: if $t$ is a reducible
001-term, we define $\mathtt{adr}(t)$, the applicative depth of reduction of
$t$ as the minimal applicative depth of a redex inside $t$. There may be
several such redexes, e.g., if $t:=x\,(\mathtt{I}\,\mathtt{I})\Omega$, then
$\mathtt{adr}(t)=1$ and both $(\mathtt{I}\,\mathtt{I})$ and $\Omega$ are redex
occuring at applicative depth 1.

We then set $t\rightarrow_{\mathtt{hh}}t^{\prime}$ whenever
$t\rightarrow_{\\!\beta}t^{\prime}$ and the contracted redex occurs at
applicative depth $\mathtt{adr}(t)$, thus, with the same example, we have both
$t\rightarrow_{\mathtt{hh}}x\,\mathtt{I}\,\Omega$ and
$t\rightarrow_{\mathtt{hh}}t$. We can also define a (deterministic) parallel
version of this reduction, by specifying that, when $t$ is reducible, all
redexes occuring at applicative depth $\mathtt{adr}(t)$ are simulateneously
contracted:
$x\,(\mathtt{I}\,\mathtt{I})\,(\mathtt{I}\,\mathtt{I})\,(x\,(\mathtt{I}\,x))$
would give $x\,\mathtt{I}\,\mathtt{I}\,(x(\mathtt{I}\,x))$.

######  Observation 3.

Let $t$ be a 001-term. Then $t$ is hereditary head normalizing iff, for all
$d\in\mathbb{N}$, there is a term $t^{\prime}$ such that
$\mathtt{adr}(t^{\prime})\geqslant d$ and
$t\rightarrow_{\mathtt{hh}}^{*}t^{\prime}$.

### Infinitary convergence.

When $t$ is hereditarily head normalizing ($\mathtt{BT}(t)$ does not contain
$\bot$), hereditary head reduction is productive in the sense that, whenever
we wait sufficiently many evaluation steps, the term will not change under any
fixed applicative depth (Observation 3). This is actually why hereditary head
reduction computes something (in this case, the Böhm tree of $t$). More
generally, some reduction paths of an unspecified form have an infinite length
but asymptotically produce a term:

######  Definition 4 (Productive reduction paths).

Let $t=t_{0}\stackrel{{\scriptstyle
b_{0}}}{{\rightarrow}}_{\\!\beta}t_{1}\stackrel{{\scriptstyle
b_{1}}}{{\rightarrow}}_{\\!\beta}t_{2}\ldots t_{n}\stackrel{{\scriptstyle
b_{n}}}{{\rightarrow}}_{\\!\beta}t_{n+1}\ldots$ be a reduction path of length
$\ell\leqslant\infty$.
Then, this reduction path is said to be productive if either it is of finite
length ($\ell\in\mathbb{N}$), or $\ell=\infty$ and $\mathtt{ad}(b_{n})$ tends
to infinity (remember that $\mathtt{ad}(\cdot)$ is applicative depth).

A productive reduction path is called a strongly converging reduction sequence
in [KKSdV97], in which numerous examples are found. When $\mathtt{BT}(t)$ does
not contain $\bot$, the hereditary head reduction strategy on a term $t$ gives
a particular case of productive path.

######  Lemma 5 (Limit of a productive path).

Let $t=t_{0}\stackrel{{\scriptstyle
b_{0}}}{{\rightarrow}}_{\\!\beta}t_{1}\stackrel{{\scriptstyle
b_{1}}}{{\rightarrow}}_{\\!\beta}t_{2}\ldots t_{n}\stackrel{{\scriptstyle
b_{n}}}{{\rightarrow}}_{\\!\beta}t_{n+1}\ldots$ be a productive reduction path
of infinite length.
Then, there is a unique 001-term $t^{\prime}$ such that, for every $d\geqslant
0$, there is $N\in\mathbb{N}$ such that, for all $n\geqslant N$,
$\mathtt{supp}(t_{n})\cap\\{b\in\\{0,1,2\\}^{*}\,|\,\mathtt{ad}(b)\leqslant
d\\}=\mathtt{supp}(t^{\prime})\cap\\{b\in\\{0,1,2\\}^{*}\,|\,\mathtt{ad}(b)\leqslant
d\\}$ and $t_{n}(b)=t^{\prime}(b)$ on
$\mathtt{supp}(t^{\prime})\cap\\{b\in\\{0,1,2\\}^{*}\,|\,\mathtt{ad}(b)\leqslant
d\\}$.

The existence and the unicity of the term $t^{\prime}$ in the statement of
Lemma 5 is easy to prove, and $t^{\prime}$ is called the limit of the
productive path. Intuitively, the lemma specifies that, when $t^{\prime}$ is
the limit of $(t_{n})_{n\geqslant 0}$, then $t^{\prime}$ induces the same tree
as $t_{n}$ at fixed applicative depth after sufficiently many reduction steps,
as expected.

######  Notation 1.

We write $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$ if
$t\rightarrow_{\\!\beta}^{*}t^{\prime}$ or $t^{\prime}$ is the limit of a
productive path starting at $t$.

For instance, if $\Delta_{f}=\lambda x.f(x\,x)$,
$\mathtt{Y}_{f}=\Delta_{f}\,\Delta_{f}$ (with $f\in\mathscr{V}$), then
$\mathtt{Y}_{f}\stackrel{{\scriptstyle\varepsilon}}{{\rightarrow}}_{\\!\beta}f(\mathtt{Y}_{f})$,
which gives the productive path
$\mathtt{Y}_{f}\stackrel{{\scriptstyle\varepsilon}}{{\rightarrow}}_{\\!\beta}f(\mathtt{Y}_{f})\stackrel{{\scriptstyle
2}}{{\rightarrow}}_{\\!\beta}\ldots
f^{n}(\mathtt{Y}_{f})\stackrel{{\scriptstyle
2^{n}}}{{\rightarrow}}_{\\!\beta}f^{n+1}(\mathtt{Y}_{f})\ldots$ since
$\mathtt{ad}(2^{n})=n\longrightarrow\infty$. The limit of this path, which
implements hereditary head reduction on $\mathtt{Y}_{f}$, is $f^{\infty}$,
i.e., we have $\mathtt{Y}_{f}{\rightarrow_{\\!\beta}^{\infty}}f^{\infty}$.
This formalizes observations on the first page on this article. More
generally, if $t$ is hereditary head normalizing, by Observation 3, hereditary
head reduction on $t$ defines a productive reduction path whose limit is the
normal form of $t$, whether this path is finite or not. As a counter-example,
$t:=x\,\mathtt{Y}_{f}\,\Omega$ is not hereditary head normalizing and
$\rightarrow_{\mathtt{hh}}$ does not stop on $t$, since
$t\rightarrow_{\mathtt{hh}}x\,(f\,\mathtt{Y}_{f})\Omega\rightarrow_{\mathtt{hh}}x\,(f\,\mathtt{Y}_{f})\Omega$.
However, the computation of $\mathtt{Y}_{f}$ in $t$ gives a productive
reduction path from $t$ to $x\,f^{\infty}\,\Omega$.

Notice that $\Omega\rightarrow_{\\!\beta}\Omega\rightarrow_{\\!\beta}\ldots$
is not a productive path (although the term does not change) since all
reduction steps occur at null applicative depth.

By Observation 3, a term $t$ is hereditarily head normalizing iff
$\rightarrow_{\mathtt{hh}}$ on $t$ defines a productive reduction path (whose
limit is necessarily a 001-normal form by construction, whether this path is
of finite length or not). Let us now have look at the alternative notion of
infinite normalization.

######  Definition 6.

A 001-term $t$ has an infinitary normal form if there is a 001-normal form
$t^{\prime}$ such that $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$ (for
some productive path).

The reader may keep in mind that, when we say that $t$ has an infinitary
normal form $t^{\prime}$, $t^{\prime}$ can be either finite or infinite.

It is known that $t$ has an infinitary normal form iff $t$ is hereditarily
head normalizing, i.e., iff the Böhm tree of $t$ does not contain $\bot$.
Notice that, if $\mathtt{BT}(t)$ does not contain $\bot$ (e.g., when
$t=\mathtt{Y}_{f}$), then it is obvious that $t$ has an infinitary normal form
by Definitions 2 and 4, but the converse implication is not, especially in the
infinite case [KKSdV97]. The statement is proved in [KKSdV97] in a syntactical
way, but Theorem 4 shall give an alternative semantic proof of this fact.
Notice that, contrary to the finite case, this does not hold for leftmost-
outermost reduction strategy. If $t:=\mathtt{Y}_{f}\,\mathtt{Y}_{f}$, whose
Böhm tree $t^{\prime}:=(f^{\infty})f^{\infty}$ does not contain $\bot$, the
leftmost-outermost strategy asymptotically computes
$f^{\infty}\,\mathtt{Y}_{f}$ and not $t^{\prime}$: hereditary head reduction
can be interpreted as a well-balanced version of l.o. reduction.

######  Remark 1 (Variants of the infinitary $\lambda$-calculus).

The infinitary $\lambda$-calculus has actually seven main variants, which were
introduced by Klop and its collaborators [KKSdV97]. Among those, only three
behave well, i.e., satisfy the weakened form of confluence. The infinitary
calculus that is considered here is one of these 3 calculi, which is referred
to as $\Lambda^{001}$. Its normal forms, as we shall recall in Sec. 3.3, are
the Böhm trees (without $\bot$). The two other well-behaved infinitary calculi
are $\Lambda^{111}$ and $\Lambda^{101}$ and their normal forms respectively
correspond to the Berarducci trees [BI93, Ber96] and the Lévy-Longo trees
[L7́5, Lon83].

###  3.4. The Finitary Type System $\mathscr{R}_{0}$ and Unforgetfulness

In this section, we present a well-known variant system of Gardner-de
Carvalho’s using multisets to represent non-idempotent intersection. This
system characterizes head normalization. We state its main properties (subject
reduction and expansion) and then we explain how it also enables
characterizing weak normalization, using unforgetfulness.

System $\mathscr{R}_{0}$ features non-idempotent intersection types [Car07,
Gar94], given by the following inductive grammar:

$\sigma,\,\tau\hskip 14.22636pt::=o\hskip 14.22636pt|\hskip
14.22636pt[\sigma_{i}]_{{i\in I}}\rightarrow\tau$

where the constructor $[\,]$ is used for finite multisets ($I$ is finite), and
the type variable $o$ ranges over a countable set $\mathscr{O}$. We write
$[\sigma]_{n}$ to denote the multiset containing $\sigma$ with multiplicity
$n$. The multiset $[\sigma_{i}]_{{i\in I}}$ is meant to be the non-idempotent
intersection of the types $\sigma_{i}$, taking into account their
multiplicity, and intersection is strict, i.e., does not occur on codomain of
arrows.

In system $\mathscr{R}_{0}$, a judgment is a triple $\Gamma\vdash t:\tau$,
where $\Gamma$ is a context, i.e., a total function from the set $\mathscr{V}$
of term variables to the set of multiset types $[\sigma_{i}]_{{i\in I}}$, $t$
is a (finite or infinite) 001-term and $\tau$ is a type. The context
$x:[\sigma_{i}]_{{i\in I}}$ is the context $\Gamma$ such that
$\Gamma(x)=[\sigma_{i}]_{{i\in I}}$ and $\Gamma(y)=[\,]$ for all $y\neq x$.
The multiset union +, satisfying e.g.,
$[\tau,\sigma]+[\sigma]=[\tau,\sigma,\sigma]$, is extended point-wise on
contexts, e.g., $\Gamma+\Delta$ maps $x$ on $\Gamma(x)+\Delta(x)$. We set
$\mathtt{dom}(\Gamma)=\\{x\in\mathscr{V}\,|\,\Gamma(x)\neq[\,]\\}$, the domain
of the context $\Gamma$. When
$\mathtt{dom}(\Gamma)\cap\mathtt{dom}(\Delta)=\emptyset$, we may write
$\Gamma;\Delta$ instead of $\Gamma+\Delta$. The set of
$\mathscr{R}_{0}$-derivations is defined inductively by the rules in Fig. 6:

$\begin{array}[t]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 25.64218pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=54.06215pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\tau]\vdash x:\tau$}}}}\hskip 14.22636pt\hskip 14.22636pt{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
4.02779pt\hbox{$\displaystyle\penalty 1\Gamma;x:[\sigma_{i}]_{{i\in I}}\vdash
t:\tau$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=79.76584pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda x.t:[\sigma_{i}]_{{i\in
I}}\rightarrow\tau$}}}}\\\\[17.07182pt] {tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:[\sigma_{i}]_{{i\in I}}\rightarrow\tau\hskip 14.22636pt(\Delta_{i}\vdash
u:\sigma_{i})_{{i\in I}}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=135.19333pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
33.76056pt\hbox{$\displaystyle\Gamma+_{{i\in I}}\Delta_{i}\vdash
t\,u:\tau$}}}}\end{array}$

Figure 6. System $\mathscr{R}_{0}$

We write $\Pi\rhd\Gamma\vdash t:\tau$ to mean that the finite derivation $\Pi$
concludes with the judgment $\Gamma\vdash t:\tau$ and $\rhd\Gamma\vdash
t:\tau$ to mean that $\Gamma\vdash t:\tau$ is derivable.

No weakening is allowed (relevance). In particular, the $\mathtt{ax}$-rule
concludes with $x:[\sigma]\vdash x:\sigma$ and not with
$\Gamma,x:[\sigma_{i}]_{{i\in I}}\vdash x:\sigma_{i_{0}}$ (for some $i_{0}\in
I$). Since contexts are total, if $\Gamma\vdash t:\tau$ and
$x\notin\mathtt{dom}(\Gamma)$, then $\lambda x.t$ is always typable: rule
$\mathtt{abs}$ gives $\Gamma\vdash\lambda x.t:[\,]\rightarrow\tau$. Relevance
ensures that $\lambda x.x$ (resp. $\lambda x.y$) can be typed with
$[\tau]\rightarrow\tau$ (resp. $[\,]\rightarrow\tau$), but not with
$[\tau,\sigma]\rightarrow\tau$ (resp. $[\tau]\rightarrow\tau$).

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 27.03107pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=54.06213pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\tau]\vdash x:\tau$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=98.55878pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern
15.99832pt\hbox{$\displaystyle\vdash\lambda
x.x:[\tau]\rightarrow\tau$}}}}\hskip 14.22636pt\hskip 14.22636pt\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 26.5774pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=53.15479pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
y:[\tau]\vdash y:\tau$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=97.65143pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern 5.13615pt\hbox{$\displaystyle
x:[\tau]\vdash\lambda x.y:[\,]\rightarrow\tau$}}}}$

A straightforward induction shows that if $\Gamma\vdash t:\tau$ is derivable,
then $\mathtt{dom}(\Gamma)$ is finite. The definition below allows formulating
quantitative properties of the system.

######  Remark 2 (Relevance and redundancy of context).

Contexts are actually superfluous in system $\mathscr{R}_{0}$, since, by
induction on $\Pi\rhd\Gamma\vdash t:\tau$, for all $x\in\mathscr{V}$,
$\Gamma(x)$ is the multiset of the types assigned to $x$ in axiom rules. All
the cases are straightforward. In a non-relevant system, this does not hold,
since $x$ may have been assigned types via the weakening rule. However, we
prefer to keep contexts explicit in system $\mathscr{R}_{0}$ although they are
superfluous, since they make the system easier to formulate.

######  Definition 7.

Let $\Pi$ be a $\mathscr{R}_{0}$-derivation. Then the size of $\Pi$, denoted
$\mathtt{sz}(\Pi)$, is the number of judgments in $\mathscr{R}_{0}$.

Observe that system $\mathscr{R}_{0}$ is essentially finite (a derivation
contains a finite number of judgments, judgments contains finite number of
types, types are finite trees), although it may type infinite terms, which can
appear as untyped arguments of applications, e.g., $f^{\infty}$
($:=f(f^{\infty})$) in:

$\Pi^{\prime}_{1}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 44.1525pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=91.08278pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:[[\,]\rightarrow o]\vdash f:[\,]\rightarrow o$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=135.57942pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern 29.726pt\hbox{$\displaystyle
f:[[\,]\rightarrow o]\vdash f^{\infty}:o$}}}}$

The derivation $\Pi^{\prime}_{1}$ is finite: it contains only two judgments,
and finite types and contexts.

System $\mathscr{R}_{0}$ enjoys both subject reduction and expansion, meaning
that types are invariant under (anti-)reduction (if $t\rightarrow t^{\prime}$,
then $\rhd\Gamma\vdash t:\tau$ iff $\rhd\Gamma\vdash t^{\prime}:\tau$). Notice
the decrement of size in subject reduction statement.

######  Proposition 8 (Weighted Subject Reduction and Expansion in system
$\mathscr{R}_{0}$).

Assume $t\rightarrow_{\\!\beta}t^{\prime}$.

  1. (1)

If $\Gamma\vdash t:\tau$ is $\mathscr{R}_{0}$-derivable, so is $\Gamma\vdash
t^{\prime}:\tau$. Moreover, if $\Pi\rhd\Gamma\vdash t:\tau$, then there is
$\Pi^{\prime}\rhd\Gamma\vdash t^{\prime}:\tau$ such that
$\mathtt{sz}(\Pi^{\prime})\leqslant\mathtt{sz}(\Pi)$, with actually
$\mathtt{sz}(\Pi^{\prime})<\mathtt{sz}(\Pi)$ when
$t\rightarrow_{\mathtt{h}}t^{\prime}$.

  2. (2)

If $\Gamma\vdash t^{\prime}:\tau$ is $\mathscr{R}_{0}$-derivable, so is
$\Gamma\vdash t:\tau$.

###### Proof.

Both points are proved by induction on the position of the reduction, using
the following Substitution and Anti-Substitution Lemmas in the base case. ∎

######  Lemma 9 (Substitution and Anti-Substitution in $\mathscr{R}_{0}$).

Let $r$ and $s$ be two 001-terms.

  * •

If $\Pi\rhd\Gamma;x:[\sigma_{i}]_{{i\in I}}\vdash r:\tau$ and, $\forall{i\in
I}$, $\Phi_{i}\rhd\Delta_{i}\vdash s:\sigma_{i}$, then there is a derivation
$\Pi^{\prime}\rhd\Gamma+(+_{i\in I}\Delta_{i})\vdash r[s/x]:\tau$ such that
$\mathtt{sz}(\Pi^{\prime})=\mathtt{sz}(\Pi)+(+_{i\in
I}\mathtt{sz}(\Phi_{i}))-\\#I$ where $\\#I$ is the cardinality of $I$.

  * •

If $\Pi^{\prime}\rhd\Gamma^{\prime}\vdash r[s/x]:\tau$, then there are
derivations $\Pi\rhd\Gamma;x:[\sigma_{i}]_{{i\in I}}\vdash r:\tau$ and
$\forall{i\in I}$, $\Phi_{i}\rhd\Delta_{i}\vdash s:\sigma_{i}$ such that
$\Gamma^{\prime}=\Gamma+(+_{i\in I}\Delta_{i})$.

###### Proof.

Substitution is proved by structural induction on $\Pi$. Anti-substitution is
proved by induction on $\Pi^{\prime}$, with a case-analysis on the last
constructor of $r$. ∎

The following result was proved in [Car07] for $\Lambda$. We have slightly
adapted it for $\Lambda^{001}$:

######  Theorem 1 (de Carvalho).

A 001-term is HN iff it is typable in system $\mathscr{R}_{0}$.

###### Proof.

Assume that $\Pi\rhd\Gamma\vdash t:\tau$. Let $n=\mathtt{sz}(\Pi)$. Then
weighted subject reduction entails that the head reduction strategy outputs a
HNF in less than $n$ steps. Conversely, head normal forms are easily
$\mathscr{R}_{0}$-typable: to type $\lambda x_{1}\ldots x_{p}.x\,t_{1}\ldots
t_{q}$, we just need to assign
$[\,]\rightarrow\ldots\rightarrow[\,]\rightarrow o$ (with $q$ arrows) to the
head variable $x$, so that $t_{1},\ldots,t_{q}$ are left untyped. We then use
subject expansion to conclude that every HN term is typable. ∎

Characterizing finitary weak normalization. A term $t\in\Lambda^{001}$ is
finitarily weakly normalizing when leftmost-outermost reduction terminates on
$t$ and outputs a finite normal form $t^{\prime}$ (note that if $u$ is
infinite, then $(\lambda x.y)u$ is infinite but reduces to the finite normal
form $y$ and is thus finitarily weakly normalizing in the sense that we
consider here).

To understand how it is done, observe first that system $\mathscr{R}_{0}$
characterizes head normalization (and not weak normalization) because the
arguments of a head variable can be left untyped: for instance, $x$ is
assigned $[\,]\rightarrow\tau$, then $x\,t$ is typable with type $\tau$ for
any term $t$ – which is left untyped as a subterm of $x\,t$ – even if $t$ is
not head normalizing.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 43.41982pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=89.61742pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[[\,]\rightarrow\tau]\vdash x:[\,]\rightarrow\tau$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=134.11406pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
28.49828pt\hbox{$\displaystyle x:[[\,]\rightarrow\tau]\vdash x\,t:\tau$}}}}$

As we explained in Sec. 2.2 (Partial typings), the possibility to have untyped
arguments is crucial to characterize head normalization because this does not
forbid, e.g., the head normal form $x\,\Omega$ to be typed.

On the other hand, in order to characterize weak normalization, we must
guarantee somehow that every subterm is typed, except the subterms that can be
erased in a reduction paths, e.g., the subterm $u$ in $(\lambda x.y)u$ should
not be typed, since $(\lambda x.y)u\rightarrow_{\\!\beta}y$. To achieve this,
$[\,]$ should not occur at bad positions in a derivation $\Pi$. Actually, it
is enough to only look at the judgment concluding $\Pi$. We recall that $[\,]$
occurs negatively in $[\,]\rightarrow\tau$ and that $[\,]$ occurs positively
(resp. negatively) in $[\sigma_{i}]_{{i\in I}}\rightarrow\tau$ if $[\,]$
occurs positively (resp. negatively) in $\tau$ or negatively (resp.
positively) in some $\sigma_{i}$, i.e., the polarity of the occurrences of
$[\,]$ in a type is preserved in the codomain of arrows and inverted in the
domain of arrows.

We say here that judgment $\Gamma\vdash t:\tau$ is unforgetful when $[\,]$
occurs neither negatively in any $\Gamma(x)$ nor positively in $\tau$. A term
$t$ is unforgetfully typable if an unforgetful judgment $\Gamma\vdash t:\tau$
is derivable. This is given by the following theorem [dC18], which is the non-
idempotent counterpart of a similar characterization with idempotent
intersection based on unforgetfulness:

######  Theorem 2.

A term $t$ is finitarily weakly normalizing iff it is unforgetfully typable in
system $\mathscr{R}_{0}$

A straightforward induction shows that, when $\Pi\rhd\Gamma\vdash t:\tau$ is
unforgetful, (1) if $t$ is reducible, then every redex of minimal applicative
depth is typed, and (2) if $t$ is a normal form, then every subterm of $t$ is
typed in $\Pi$ (thus, no part of the normal form of a term $t$ is “forgotten”
in an unforgetful derivation), which roughly justifies why the above theorem
holds. In general, the unforgetfulness criterion gives a characterization of
weak normalization in any type system which characterizes head normalization.

For now (in particular for Sec. 3.6), it is enough to keep in mind that a
sufficient condition of unforgetfulness is to be $[\,]$-free: $t$ is weakly
normalizing as soon as $\rhd\Gamma\vdash t:\tau$, where $\Gamma$ and $\tau$ do
not contain $[\,]$. Throughout this article, we will frequently invoke system
$\mathscr{R}_{0}$ and this section to illustrate or motivate our choices.

###  3.5. Infinitary subject reduction and expansion for finite derivations

Now, let us explain why subject reduction and expansion hold for infinite
productive reduction path (and not just finite ones). The fact that if
$\rhd\Gamma\vdash t:\tau$ and $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$
then there is $\rhd\Gamma\vdash t^{\prime}:\tau$ (infinitary subject
reduction) is actually an easy consequence of the definition of productive
paths (Definition 4). In contrast, the fact that if $\Pi\rhd\Gamma\vdash
t^{\prime}:\tau$ and $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$, then
$\rhd\Gamma\vdash t:\tau$ (infinitary subject expansion) relies on the
finiteness of the derivations in $\mathscr{R}_{0}$ and a technical observation
that we call subject substitution and that will be a key tool in Sec. 3.6 and
7.4 to obtain full infinitary subject expansion. Let us prove the infinitary
subject reduction property.

######  Proposition 10 (Infinitary suject reduction (system
$\mathscr{R}_{0}$)).

If $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$ and
$\rhd_{\mathscr{R}_{0}}\Gamma\vdash t:\tau$, then
$\rhd_{\mathscr{R}_{0}}\Gamma\vdash t^{\prime}:\tau$.

###### Proof.

Assume $\Pi\rhd_{\mathscr{R}_{0}}\Gamma\vdash t:\tau$ and
$\Pi=:\Pi_{0}\stackrel{{\scriptstyle
b_{0}}}{{\rightarrow}}_{\\!\beta}\Pi_{1}\stackrel{{\scriptstyle
b_{1}}}{{\rightarrow}}_{\\!\beta}\Pi_{2}\ldots$ the derivations obtained by
subject reduction along the given path
$t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$. For every $k\in\mathbb{N}$,
let $N_{k}$ be such that, for all $n\geqslant N_{k}$,
$\mathtt{ad}(b_{n})>k+1$.

Let $\Pi^{\prime}$ be the derivation typing $t^{\prime}$ defined as follows:
under applicative depth $k$, $\Pi^{\prime}$ is the same as $\Pi_{n}$ for any
$n\geqslant N_{k}$ except that the judgments of $\Pi^{\prime}$ type
$t^{\prime}$ and its subterms instead of $t_{n}$ and its subterms.

This definition is licit, because, under applicative depth $\Pi_{n}$ and
$\Pi_{n^{\prime}}$ do not differ whenever $n,n^{\prime}\geqslant N_{k}$,
except for untyped parts of their subjects, which also proves that
$\Pi^{\prime}$ is correct. ∎

One notices that the proof of Proposition 10 does not use anywhere the
finiteness of the derivations (we perform subject substitution but only at
fixed depth $k$ after a sufficient number of steps $N_{k}$). The statement and
its proof shall still be valid in the infinitary system (Proposition 36, which
we prove more formally).

But as we explained in Sec. 2.3, naively, subject expansion is not an
asymptotic process. However, there is a way to by-pass the “infinite jump
problem” by using the fact the derivations are finite: one may replace the
limit $t^{\prime}$ of a productive path with some $t_{n}$ when $n$ is big
enough, without compromising the correctness of the derivation.

Actually, in a derivation $\Pi$ whose subject is $t_{1}$, we may replace
$t_{1}$ with any term $t_{2}$ which coincide with $t_{1}$ on the typed parts
inside $\Pi$. We name this phenonemon subject substitution.

######  Example 2.

Consider:

$\Pi_{1}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 45.2844pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=90.56879pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[[\,]\rightarrow o]\vdash x:[\,]\rightarrow o$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=124.78761pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 16.10007pt\hbox{$\displaystyle
x:[[\,]\rightarrow o]\vdash x(y\,z):o$}}}}\hskip 14.22636pt\hskip
14.22636pt\hskip 14.22636pt\Pi_{2}={tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 45.2844pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=90.56879pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[[\,]\rightarrow o]\vdash x:[\,]\rightarrow o$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=124.78761pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 21.5538pt\hbox{$\displaystyle
x:[[\,]\rightarrow o]\vdash x\,\Omega:o$}}}}$

We transform $\Pi_{1}$ into $\Pi_{2}$ by substituting the subject $x(y\,z)$
with $x\,\Omega$. This is licit because we replace $y\,z$, which is an untyped
subterm of $x(y\,z)$ in the derivation $\Pi_{1}$.

To formulate subject substitution, we need to define the set of positions of
the typed subterms in a derivation $\Pi$:

######  Definition 11.

Let $\Pi$ a derivation typing a term $t$. We define the set
$\hat{\Pi}\subset\mathtt{supp}(t)$ of the typed positions in $\Pi$ by the
following induction on $\Pi$:

  * •

If $\Pi$ ends with an axiom rule ($t=x$), then
$\hat{\Pi}=\\{\varepsilon\\}=\mathtt{supp}(t)$.

  * •

If $\Pi$ ends with an $\mathtt{abs}$-rule ($t=\lambda x.t_{0}$) and $\Pi_{0}$
is its depth 1 subderivation, then $\hat{\Pi}=\\{\varepsilon\\}\cup
0\cdot\hat{\Pi}_{{}_{0}}$.

  * •

If $\Pi$ ends with an $\mathtt{app}$-rule ($t=t_{1}\,t_{2}$), $\Pi_{1}$ is its
left premise (concluding with $t_{1}:[\sigma_{i}]_{{i\in I}}\rightarrow\tau$)
and the $(\Pi_{i})_{{i\in I}}$ (concluding respectively with
$t_{2}:\sigma_{i}$) are its right premises, then
$\hat{\Pi}=\\{\varepsilon\\}\cup 1\cdot\hat{\Pi}_{{}_{1}}\cup(\cup_{{i\in
I}}2\cdot\hat{\Pi}_{{}_{i}})$

In the $\mathtt{app}$-case, if $I=\emptyset$, $t_{2}$ is not typed and we only
have $\hat{\Pi}=\\{\varepsilon\\}\cup 1\cdot\hat{\Pi}_{{}_{1}}$ , as expected.
In the typings of $x(y\,z)$ and $x\,\Omega$ in Example 2, we have
$\hat{\Pi}_{1}=\hat{\Pi}_{2}=\\{\varepsilon,1\\}$. The applicative depth of a
typed position inside $\Pi$ cannot exceed the size of $\Pi$ (this can be
proved by induction on $\Pi$):

######  Observation 12.

Let $\Pi$ be a $\mathscr{R}_{0}$-derivation. If $b\in\hat{\Pi}$, then
$\mathtt{ad}(b)<\mathtt{sz}(\Pi)$.

######  Lemma 13 (Subject Substitution).

Let $t,u\in\Lambda^{\infty}$. If $\Pi\rhd_{\mathscr{R}_{0}}\Gamma\vdash
t:\tau$, $\hat{\Pi}\subseteq\mathtt{supp}(u)$ and, for all $b\in\hat{\Pi}$,
$u(b)=t(b)$, then there exists a $\mathscr{R}_{0}$-derivation $\Psi$ such that
$\Psi\rhd\Gamma\vdash u:\tau$ and $\hat{\Psi}=\hat{\Pi}$.

###### Proof.

Straightforward by induction on $\Pi$. ∎

To obtain infinitary subject expansion in $\mathscr{R}_{0}$, the idea is to
perform subject substitution in the considered infinite productive reduction
path. Indeed, if $\Pi$ types $t$ and $t$ and $u$ differ only for positions
$b\in\\{0,1,2\\}^{*}$ such that $|b|>\mathtt{sz}(\Pi)$ (where $|b|$ is the
length of $b$), then Lemma 13 can be applied on $\Pi$.

Contrary to infinitary subject reduction, the proof of infinitary subject
expansion below crucially relies on the fact that
$\mathscr{R}_{0}$-derivations are finite, in order to perform a subject
substitution:

######  Proposition 14 (Infinitary suject expansion (system
$\mathscr{R}_{0}$)).

If $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$ and
$\rhd_{\mathscr{R}_{0}}\Gamma\vdash t^{\prime}:B$, then
$\rhd_{\mathscr{R}_{0}}\Gamma\vdash t:B$.

###### Proof.

When $t{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$ in a finite number of
steps, this is an obvious consequence of Proposition 8. Let us then assume
that $t=t_{0}\stackrel{{\scriptstyle
b_{0}}}{{\rightarrow}}_{\\!\beta}t_{1}\stackrel{{\scriptstyle
b_{1}}}{{\rightarrow}}_{\\!\beta}t_{2}{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$
is an infinite path and that $\Pi^{\prime}\rhd_{\mathscr{R}_{0}}\Gamma\vdash
t^{\prime}:\tau$. Let $k=\mathtt{sz}(\Pi^{\prime})$. Let $N$ such that, for
all $n\geqslant N$, $\mathtt{ad}(b_{n})>k$ (such a $n$ exists, since the
reduction path is productive). By definition of the limit (Lemma 5), this
implies that
$\mathtt{supp}(t_{N})\cap\\{b\in\\{0,1,2\\}^{*}\,|\,\mathtt{ad}(b)\leqslant
k\\}=\mathtt{supp}(t^{\prime})\cap\\{b\in\\{0,1,2\\}^{*}\,|\,\mathtt{ad}(b)\leqslant
k\\}$ and that, on this set, $t_{N}(b)=t^{\prime}(b)$. In particular, by
Observation 12, $t_{N}(b)=t^{\prime}(b)$ is well-defined and holds on
$\hat{\Pi}^{\prime}$.

By subject substitution (Lemma 13) applied to $\Pi^{\prime}$ and $t_{N}$,
there is a derivation $\Pi_{N}\rhd\Gamma\vdash t_{N}:\tau$.

By Proposition 8 applied $N$ times, there is $\Pi\rhd\Gamma\vdash t:\tau$ such
that $\mathtt{sz}(\Pi)\leqslant k$. This concludes the proof. ∎

######  Remark 3.

  * •

One may take a moment to consider the proof of Lemma 14 with that of Lemma 10.
As noticed in Sec. 2.3, we need to overcome the “infinite jump problem”. Here,
it is pivotal that, under some applicative depth $k$, the subject $t^{\prime}$
of the derivation to expand is left untyped. This allows us to “jump” from
$t^{\prime}$ to some $t_{N}$ for a sufficiently large $N$ which is similar to
$t^{\prime}$ under applicative depth $k$. Note that no such need arises while
proving Lemma 10, since, for infinitary subject reduction, we define
$\Pi^{\prime}$, the derivation typing the limit, incrementally.

  * •

The lemmas of this section all apply to $\Lambda^{\infty}$ (Sec. 3.2) and not
only to $\Lambda^{001}$ with minor changes. In particular, for any
$t\in\Lambda^{\infty}$, there is a reduction path from $t$ to a head normal
form iff the head reduction terminates on $t$. Notice that some
$t\in\Lambda^{\infty}$ are headless, e.g., ${}^{\infty}x$ from Example 1,
which has neither a head variable nor a head redex, because of its leftward
infinite branch, but such a headless term is not typable in $\mathscr{R}_{0}$.

###  3.6. Roadmap to solve Klop’s Problem

Since hereditary head normalization is a form of infinitary weak
normalization, we want to adapt the proof of Proposition 2 which gives a type-
theoretic characterization of finitary weak normalization. To achieve this, we
need:

  * •

Typing (infinitary) normal forms in unforgetful judgment (in this section,
$f^{\infty}$).

  * •

Using a form of infinitary subject expansion to obtain a derivation typing the
expanded term (here, $\mathtt{Y}_{f}$)

The second point (infinitary subject expansion) is delicate, but we give
intuitions about how it may be achieved just below. We will actually follow
some of the ideas that were given in Sec. 2.3. This will allow us to present
the key notions of truncation and approximability. Fig. 7 illustrates the main
ideas of this section.

A complete trial on $\mathtt{Y}_{f}$. The first point (typing 001-normal
forms) is easier to grasp: notice that in a type system characterizing
infinitary weak normalization, derivations should be able to type infinite
normal forms fully, i.e., without leaving subterms untyped. For instance, the
following derivation $\Pi^{\prime}$, which fully types $f^{\infty}$, should be
allowed (this derivation is also represented on top of Fig. 7):

$\Pi^{\prime}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 48.72198pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=97.44397pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:[[o]\rightarrow o]\vdash f:[o]\rightarrow o$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\\\ \hskip 14.22636pt\Pi^{\prime}\rhd f:[[o]\rightarrow
o]_{\omega}\vdash f^{\infty}:o$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=141.94061pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
30.96228pt\hbox{$\displaystyle f:[[o]\rightarrow o]_{\omega}\vdash
f^{\infty}:o$}}}}$

To define $\Pi^{\prime}$, we have informally used an infinitary version of
system $\mathscr{R}_{0}$ that we call system $\mathscr{R}$ (system
$\mathscr{R}$ is formally defined in Appendix E). System $\mathscr{R}$ allows
infinite multisets (e.g., $[o]_{\omega}$ is the multiset in which $o$ occurs
with an infinite multiplicity, so that $[o]_{\omega}=[o]+[o]_{\omega}$),
proofs of infinite depth and also infinitary nestings, e.g., the type $\sigma$
defined by $\sigma=[\sigma]\rightarrow o$, so that
$\sigma=[[\ldots]\rightarrow o]\rightarrow o$, is legal.

$\Pi^{\prime}\rhd
f:\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[[o]\rightarrow
o]_{\omega}}\vdash
f^{\infty}:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{o}$
$\Pi^{\prime}$ is an infinite derivation typing the infinite term $f^{\infty}$
Every Variable is Typed
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\char 64\relax$$\Pi^{\prime}$ can be truncated into e.g.,
,$\Pi^{\prime}_{3}\rhd
f:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[[o]\rightarrow
o]_{2}+[[\,]\rightarrow o]}\vdash
f^{\infty}:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{o}$
Both $\Pi^{\prime}_{3}$ and $\Pi^{\prime}_{4}$ are finite derivations typing
the infinite term $f^{\infty}$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[\phantom{o}]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\char 64\relax$or$\Pi^{\prime}_{4}\rhd
f:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[[o]\rightarrow
o]_{3}+[[\,]\rightarrow o]}\vdash
f^{\infty}:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{o}$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[\phantom{o}]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\char 64\relax$ The untyped parts of the subject can be
substituted e.g., $f^{\infty}$ can be replaced by $f^{4}(\mathtt{Y}_{f})$ in
$\Pi^{\prime}_{3}$ and $\Pi^{\prime}_{4}$, yielding respectively…
$\Pi^{4}_{3}\rhd
f:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[[o]\rightarrow
o]_{2}+[[\,]\rightarrow o]}\vdash
f^{4}(\mathtt{Y}_{f}):\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{o}$
Both $\Pi^{4}_{3}$ and $\Pi^{4}_{4}$ are finite derivations typing the finite
term $f^{4}(\mathtt{Y}_{f})$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[\phantom{o}]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\mathtt{Y}_{f}$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\char 64\relax$$\Pi^{4}_{4}\rhd
f:\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[[o]\rightarrow
o]_{3}+[[\,]\rightarrow o]}\vdash
f^{4}(\mathtt{Y}_{f}):\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{o}$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[\phantom{o}]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$o$$\mathtt{Y}_{f}$$f$$\char 64\relax$$f$$\char 64\relax$$f$$\char
64\relax$$f$$\char 64\relax$ Figure 7. Truncation and Subject Substitution

Step 1 (truncations/approximations). Notice that $\Pi^{\prime}$ is of
infinitary depth and fully types $f^{\infty}$ (i.e., no subterm of
$f^{\infty}$ is left untyped in $\Pi^{\prime}$). Actually, $\Pi^{\prime}$ is
$[\,]$-free and in particular, it is unforgetful (recall the discussion
surrounding Theorem 2).

Thus, $\Pi^{\prime}$ is the kind of derivation we want to expand, as to get a
derivation $\Pi$ typing $\mathtt{Y}_{f}$ and witnessing that this term is
infinitarily weakly normalizing. Since
$\mathtt{Y}_{f}{\rightarrow_{\\!\beta}^{\infty}}f^{\infty}$ (infinite number
of reduction steps), we are stuck in the “infinite jumb problem”: indeed, the
pivotal argument in Proposition 14 allowing to “jump back” from the limit of a
productive path to a term of this path is that the subject is partially typed,
which allows performing subject substitution. Here, not such thing occurs,
since no subterm of $f^{\infty}$ is untyped in $\Pi^{\prime}$.

But notice that $\Pi^{\prime}$ can be truncated into the derivation
$\Pi^{\prime}_{n}$ below, for any $n\geqslant 1$. To define these derivations,
we have set $\Gamma_{n}=f:[[o]\rightarrow o]_{n-1}+[[\,]\rightarrow o]$ and we
write $x:\tau$ instead of $x:[\tau]\vdash x:\tau$ for $\mathtt{ax}$-rules:

$\Pi^{\prime}_{n}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 20.05547pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=40.11093pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:[o]\rightarrow o$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\parbox[b]{113.81102pt}{ $\begin{array}[b]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 20.05547pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=40.11093pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:[o]\rightarrow o$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 27.43459pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=54.86917pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma_{1}\vdash f:[\,]\rightarrow o$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=99.36581pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
29.726pt\hbox{$\displaystyle\Gamma_{1}\vdash f^{\infty}:o$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=234.30338pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
97.19478pt\hbox{$\displaystyle\Gamma_{2}\vdash f^{\infty}:o$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2\\\ \vdots\\\ \Gamma_{n-1}\vdash
f^{\infty}:o\end{array}$}\phantom{aa}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=208.99037pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
84.25761pt\hbox{$\displaystyle\Gamma_{n}\vdash f^{\infty}:o$}}}}$

Derivations $\Pi^{\prime}_{3}$ and $\Pi^{\prime}_{4}$ are represented in the
middle of Fig. 7. By truncation or approximation, we mean, as suggested in
Sec. 2.4, that the finite derivation $\Pi^{\prime}_{n}$ can be informally
obtained from the infinite one $\Pi^{\prime}$ by erasing some elements from
the infinite multisets appearing in the derivation. We also informally write
$\Pi^{\prime}_{1}\leqslant\Pi^{\prime}_{2}\leqslant\Pi^{\prime}_{3}\ldots$ to
mean that $\Pi^{\prime}_{n}$ approximates $\Pi^{\prime}_{n+1}$. Thus,
$\Pi^{\prime}_{n}\leqslant\Pi^{\prime}$ for all ${n\in\mathbb{N}}$.

Conversely, we see that $\Pi^{\prime}$ is the graphical join of the
$\Pi^{\prime}_{n}$: $\Pi^{\prime}$ is obtained by superposing suitably all the
derivations $\Pi^{\prime}_{n}$ on the same infinite sheet of paper.

Step 2 (expand the finite approximations).

  * •

Substituting $f^{\infty}$. Observe now that, although we do not know yet how
to expand $\Pi^{\prime}$, we can expand the $\Pi^{\prime}_{n}$, because the
$\Pi^{\prime}_{n}$ are $\mathscr{R}_{0}$-derivations (thus, they are finite):
by subject expansion in system $\mathscr{R}_{0}$ (Proposition 8), for all
$n\geqslant 1$, there is a $\mathscr{R}_{0}$-derivation $\Pi^{\prime}_{n}$
concluding with $\Gamma_{n}\vdash\mathtt{Y}_{f}:o$. In the particular case of
$\Pi^{\prime}$, we can detail the process: (1) $\Pi^{\prime}_{n}$ leaves
$f^{\infty}$ untyped beyond depth $n$ and (2) for any $k\geqslant n$,
$f^{\infty}$ and $f^{k}(\mathtt{Y}_{f})$ are similar below depth $n$, so using
subject substitution, for any $k\geqslant n$, $\Pi^{\prime}_{n}$ yields a
derivation $\Pi^{k}_{n}$ typing $f^{k}(\mathtt{Y}_{f})$. We have represented
$\Pi^{4}_{3}$ and $\Pi^{4}_{4}$ at the bottom of Fig. 7.

  * •

Finite expansions. Thus, $\Pi_{n}^{k}$ types $f^{k}(\mathtt{Y}_{f})$, the rank
$k$ reduct of $\mathtt{Y}_{f}$, so we can expand it $k$ times, obtaining a
derivation $\Pi_{n}$. It can easily be observed that $\Pi_{n}$ does not depend
on $k$, because $\Pi^{k}_{n}$ and $\Pi^{n}_{n}$ have the same typed parts.

Step 3 (joining the finite expansions). We can then define $\Pi$, the expected
expansion of $\Pi^{\prime}$, as the join of all the derivations $\Pi_{n}$.
This is justified by the following points:

  * (1)

for any ${n\in\mathbb{N}}$, we have
$\Pi^{n}_{0}\leqslant\Pi^{n}_{1}\leqslant\ldots\leqslant\Pi^{n}_{n}$ (see Fig.
7, bottom)

  * (2)

proof reduction and expansion are monotonic in this333But proof reduction is
not monotonic in all cases, simply because, in general, it is non-
deterministic in system $\mathscr{R}_{0}$. See Sec. 5.4 case. Thus, since
$\Pi_{0}$, $\Pi_{1}$,…, $\Pi_{n}$ are respectively obtained after $n$
expansion steps from $\Pi^{n}_{0}$, $\Pi^{n}_{1}$,…, $\Pi^{n}_{n}$, we have
$\Pi_{0}\leqslant\Pi_{1}\leqslant\ldots\leqslant\Pi_{n}$. This intuitively
explains why the $\Pi_{n}$ (typing $\mathtt{Y}_{f}$) have an infinitary join
$\Pi$, although the construction of this join is delicate for reasons to be
presented in the next section.

Summary. Thus, given an infinite derivation $\Pi^{\prime}$ typing $t^{\prime}$
and a productive reduction path
$t=t_{0}\rightarrow_{\\!\beta}t_{1}\rightarrow_{\\!\beta}\ldots{\rightarrow_{\\!\beta}^{\infty}}t^{\prime}$,
the main ingredients to perform infinitary subject expansion are:

  * 1.

Approximating $\Pi^{\prime}$ into a family of finite derivations
$\,\\!{}^{f}\\!\Pi^{\prime}$ also typing $t^{\prime}$, so that $\Pi^{\prime}$
is the (asymptotic) join of the $\,\\!{}^{f}\\!\Pi^{\prime}$.

  * 2.a.

For each approximation $\,\\!{}^{f}\\!\Pi^{\prime}$, replacing $t^{\prime}$
with $t_{n}$ for a sufficiently large $n$ ($n$ depends on
$\,\\!{}^{f}\\!\Pi^{\prime}$). This gives $\,\\!{}^{f}\\!\Pi^{n}$, which is
also finite, but types the term $t_{n}$ instead of $t^{\prime}$.

  * 2.b.

For each $\,\\!{}^{f}\\!P^{\prime}$, expanding $\,\\!{}^{f}\\!\Pi^{n}$ $n$
times. This gives $\,\\!{}^{f}\\!\Pi$, which type $t$.

  * 3.

Obtaining $\Pi$, the expansion of $\Pi^{\prime}$, whose subject is $t$, by
taking the join of the finite $\,\\!{}^{f}\\!\Pi$ while
$\,\\!{}^{f}\\!P^{\prime}$ ranges over the approximations of $\Pi^{\prime}$.

###  3.7. Problems with infinitary typing and how to solve them

Thus, the ideas of truncation, subject substitution and join guides us about
how to perform $\infty$-subject expansion. The particular form of $\Pi_{n}$
and $\Pi$ does not matter (but they are given in Appendix A for the curious
reader). Let us just say here that the $\Pi_{n}$ involve a family of finite
types $(\rho)_{n\geqslant 1}$ inductively defined by $\rho_{1}=[\,]\rightarrow
o$ and $\rho_{n+1}=[\rho_{k}]_{1\leqslant k\leqslant n}\rightarrow o$ and
$\Pi$, their infinite join, involves an infinite type $\rho$ satisfying
$\rho=[\rho]_{\omega}\rightarrow o$: if $t$ and $u$ are typed with $\rho$,
then $t\,u$ may be typed with $o$.

Problem 1 ($\Omega$ is typable). Unfortunately, it is not difficult to see
that the equality $\rho=[\rho]_{\omega}\rightarrow o$ also allows the non-head
normalizing term $\Omega=\Delta\Delta$ to be typed.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 27.82968pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=55.65936pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\rho]\vdash x:\rho$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip
14.22636pt\big{(}\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
27.82968pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=55.65936pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\rho]\vdash x:\rho$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\big{)}_{\omega}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=227.35747pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
81.96555pt\hbox{$\displaystyle x:[\rho]_{\omega}\vdash x\,x:o$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=277.68745pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern
122.0921pt\hbox{$\displaystyle\vdash\Delta:\rho$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip
14.22636pt\big{(}\vdash\Delta:\rho\big{)}_{\omega}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=384.1773pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
176.05406pt\hbox{$\displaystyle\vdash\Omega:o$}}}}$

This last observation shows that the naive extension of the standard non-
idempotent type system to infinite terms is unsound as non-head normalizing
terms can be typed (actually, every term is typable in system $\mathscr{R}$
[Via18]: this means that every $\lambda$-term has a non-empty denotation in
the infinitary relational model). Therefore, we need to discriminate between
sound derivations (like $\Pi$ typing $\mathtt{Y}_{f}$) and unsound ones. For
that, we define an infinitary derivation $\Pi$ to be valid or approximable
when it is the join of all its finite approximations (Figure 4). For instance,
$\Pi^{\prime}$ is approximable (it is the join of the $\Pi^{\prime}_{n}$) and
$\Pi$, defined as the join of the directed family $(\Pi_{n})_{n\geqslant 1}$
is approximable.

Problem 2 (validity is not definable with multisets). It turns out that
approximability cannot be formally defined in system $\mathscr{R}$, i.e., with
multisets as intersection types. We managed to define in the example of
$\mathtt{Y}_{f}$ and $f^{\infty}$ only because we explained the concept
informally and in those terms, two equal subterms are assigned the same
typing. Intuitively, approximability cannot be defined in system $\mathscr{R}$
because multisets disable tracking, as explained in Sec. 2.4. Another
(informal) argument will be given later in Sec. 5.4: since proof reduction is
not deterministic in system $\mathscr{R}$, the reduction dynamics of a
$\mathscr{R}$-derivation $\Pi$ may be very different from that of finite its
approximations. We give a formal argument, to long to be presented in the core
of this article, in Appendix E.4, once we have presented system $\mathtt{S}$
and defined approximability in this system: we find two distinct
$\mathtt{S}$-derivations $P_{1}$ and $P_{2}$, which both collapse on the same
$\mathscr{R}$-derivation $\Pi$, but such that $P_{1}$ is approximable (in
system $\mathtt{S}$) whereas $P_{2}$ is not. This proves that approximability
cannot be lifted from $\mathscr{R}$ to $\mathtt{S}$.

##  4\. Tracking types in derivations

In this section, we define system $\mathtt{S}$, which is based on the key
construct of sequence (presented in Sec. 2.4) which we use to represent
intersection in a rigid way, i.e., which enables tracking.

  * •

We first coinductively define arrow types as function types whose domains are
sequence of types. A notion of typing judgment naturally follows.

  * •

We then define derivations trees such that arguments of applications are typed
with a sequence of judgments.

### General notations

Some of these notations generalize or refine those of Sec. 3.

  * •

A track $k$ is any natural number. When $k\geqslant 2$, $k$ is called an
argument track. As for $\lambda$-terms, 0 is dedicated to the constructor
$\lambda x$, 1 is dedicated to the left-hand side of applications. Not only 2
but all the $k\geqslant 2$ to the possibly multiple typings of the arguments
of applications. For instance, in system $\mathtt{S}$, while typing an
application $t\,u$, a subderivation on track $9$ (or on track 2, track 3 and
so on) will be a subderivation typing the argument $u$. This also explains why
0 and 1 will have a particular status in the definitions to come, and
motivates the definition of collapse below.

  * •

The set of finite words on $\mathbb{N}$ is denoted with $\mathbb{N}^{*}$,
$\varepsilon$ is the empty word, $a\cdot a^{\prime}$ the concatenation of $a$
and $a^{\prime}$. The prefix order $\leqslant$ is defined on $\mathbb{N}^{*}$
by $a\leqslant a^{\prime}$ if there is $a_{0}$ such that $a^{\prime}=a\cdot
a_{0}$, e.g., $2\cdot 3\leqslant 2\cdot 3\cdot 0\cdot 1$. When the denotation
is clear, we may just write $2031$ instead of $2\cdot 0\cdot 3\cdot 1$.

  * •

The applicative depth $\mathtt{ad}(a)$ generalizes to any
$a\in\mathbb{N}^{*}$: it still represents the number of nestings inside
arguments, i.e., $\mathtt{ad}(a)$ is defined inductively by
$\mathtt{ad}(\varepsilon)=0$, $\mathtt{ad}(a\cdot k)=\mathtt{ad}(a)$ if $k=0$
or $k=1$ and $\mathtt{ad}(a\cdot k)=\mathtt{ad}(a)+1$ if $k\geqslant 2$.

  * •

The collapse is defined on $\mathbb{N}$ by $\overline{k}=\min(k,2)$ and on
$\mathbb{N}^{*}$ inductively by $\overline{\varepsilon}=\varepsilon$,
$\overline{a\cdot k}=\overline{a}\cdot\overline{k}$, e.g., $\overline{7}=2$,
$\overline{1}=1$ and $\overline{2\cdot 3\cdot 0\cdot 1}=2\cdot 2\cdot 0\cdot
1$. Intuitively, the collapse converts a position in system $\mathtt{S}$ into
a position in a $\lambda$-term (with only 0s, 1s or 2s) .
This extends to words of infinite length, the collapse of $3^{\omega}$ and
$(1\cdot 2\cdot 3)^{\omega}$ are $2^{\omega}$ and $(1\cdot 2^{2})^{\omega}$.

  * •

A sequence of elements of a set $X$ is a family $(k\cdot x_{k})_{{k\in K}}$
with $K\subseteq\mathbb{N}\setminus\\{0,1\\}$ and $x_{k}\in X$. In this case,
if $k_{0}\in K$, $x_{k_{0}}$ is the element of $(k\cdot x_{k})_{{k\in K}}$ on
track $k_{0}$. We often write $(k\cdot x_{k})_{{k\in K}}$ for $(x_{k})_{{k\in
K}}$, which, for instance, allows us to denote by $(2\cdot a,4\cdot b,5\cdot
a)$ or $(4\cdot b,2\cdot a,5\cdot a)$ the sequence $(x_{k})_{{k\in K}}$ with
$K=\\{2,4,5\\}$, $x_{2}=x_{5}=a$ and $x_{4}=b$. In this sequence, the element
on track 4 is $b$. If $S=(k\cdot x_{k})_{k\in K}$ is a sequence, we write
$K=\mathtt{Rt}(S)$ ($\mathtt{Rt}$ stands for “roots”, which are the top-level
tracks of $S$). Sequences come along with an (infinitary) disjoint union
operator, denoted $\uplus$: let $S_{j}:=(k\cdot x_{k,j})_{{k\in K}_{j}}$ be
sequences for all ${j\in J}$ (where $J$ is a possibly infinite set):

    * –

If the $(K_{j})_{{j\in J}}$ are pairwise disjoint, then $\uplus_{j\in J}S_{j}$
is the sequence $(k\cdot x_{k})_{{k\in K}}$ where $K=\vee_{j\in J}K_{j}$ and,
for all ${k\in K}$, $x_{k}=x_{k,j}$ where $j$ is the unique index such that
$k\in K_{j}$. In that case, we say that the $S_{j}$ are disjoint.

    * –

If the $(K_{j})_{{j\in J}}$ are not pairwise disjoint, then $\uplus_{j\in
J}S_{j}$ is not defined.

When $J$ is finite, we use $\uplus$ as an infix operator: $S_{1}\uplus S_{2}$
etc.

The operator $\uplus$ is partial, and infinitarily associative and
commutative. For instance, $(2\cdot a,\,3\cdot b,\,8\cdot a)\uplus(4\cdot
a,\,9\cdot c)=(4\cdot a,\,9\cdot c)\uplus(2\cdot a,\,3\cdot b,\,8\cdot
a)=(2\cdot a,\,3\cdot b,\,4\cdot a,\,8\cdot a,\,9\cdot c)$, but $(2\cdot
a,\,3\cdot b,\,8\cdot a)\uplus(3\cdot b,\,9\cdot c)$ is not defined, because
track 3 is in the roots of both sequences (track conflict).

  * •

A tree $A$ of $\mathbb{N}^{*}$ is a non-empty subset of $\mathbb{N}^{*}$ that
is downward-closed for the prefix order ($a\leqslant a^{\prime}\in A$ implies
$a\in A$). A forest is a set of the form $A\setminus\\{\varepsilon\\}$ for
some tree $A$ such that $0,\,1\notin A$. Formally, a labelled tree $T$ (resp.
labelled forest $F$) is a function to a set $\Sigma$, whose domain, called its
support $\mathtt{supp}(T)$ (resp. $\mathtt{supp}(F)$), is a tree (resp. a
forest). If $U=T$ or $U=F$, then $U|_{a}$ is the function defined on
$\\{a_{0}\in\mathbb{N}^{*}\,|\,a\cdot a_{0}\in\mathtt{supp}(U)\\}$ and
$U|_{a}(a_{0})=U(a\cdot a_{0})$. If $U$ is a labelled tree (resp. forest and
$a\neq\varepsilon$), then $U|_{a}$ is a tree.

###  4.1. Rigid Types

We start now to implement the ideas of Sec. 2.4 to overcome the problems
concluding Sec. 3.7: to enable tracking (so that we may define
approximability), every argument derivation or type in the domain of an arrow
must now receive a track for label.

Let $\mathscr{O}$ be a countable set of types variables (metavariable $o$).
The sets of (rigid) types $\mathtt{Typ}^{111}$ (metavariables $T$, $S_{i}$, …)
is coinductively defined in Fig. 8.

$\begin{array}[]{lll}T,\,S_{k}&::=&o\hskip 14.22636pt\|\hskip
14.22636pt(k\cdot S_{k})_{k\in K}\rightarrow T\\\\[2.84544pt] \end{array}$

Figure 8. $\mathtt{S}$-Types

A sequence type $F=(k\cdot S_{k})_{k\in K}$ is a sequence of types in the
above meaning and is seen as an intersection of the types $S_{k}$. We write
$(\,)$ for the empty sequence, i.e., the sequence type whose support is empty.
A sequence type of the form $(k\cdot T)$ is called a singleton sequence type.
Note that, in $(k\cdot S_{k})_{{k\in K}}$, $K$ may be an infinite subset of
$\mathbb{N}\setminus\\{0,1\\}$ and that the definition allows infinitely many
nestings of sequences in types.

######  Remark 4.

The equality between two types (resp. sequence types) may be defined by mutual
coinduction: $F\rightarrow T=F^{\prime}\rightarrow T^{\prime}$ if
$F=F^{\prime}$ and $T=T^{\prime}$ and $(T_{k})_{k\in K}=(T^{\prime}_{k})_{k\in
K^{\prime}}$ if $K=K^{\prime}$ and for all $k\in K,~{}T_{k}=T_{k}^{\prime}$.

The support of a type (resp. a sequence type), which is a tree of
$\mathbb{N}^{*}$ (resp. a forest), is defined by mutual coinduction:
$\mathtt{supp}(o)=\\{\varepsilon\\},~{}\mathtt{supp}(F\rightarrow
T)=\\{\varepsilon\\}\cup\mathtt{supp}(F)\cup 1\cdot\mathtt{supp}(T)$ and
$\mathtt{supp}((T_{k})_{k\in K})=\cup_{k\in K}k\cdot\mathtt{supp}(T_{k})$.

Thus, $\mathtt{S}$-types may be seen as labelled trees. For instance,
$(7\mathord{\cdot}o_{1},3\mathord{\cdot}o_{2},2\mathord{\cdot}o_{1})\rightarrow
o$ is represented in Fig. 9

Thus, for types, track 1 is dedicated to the codomains of arrows.

$\rightarrow$$o$$1$ $o_{1}$$2$ $o_{2}$$3$ $o_{1}$$7$

Figure 9. The $\mathtt{S}$-type
$(7\mathord{\cdot}o_{1},3\mathord{\cdot}o_{2},2\mathord{\cdot}o_{1})\rightarrow
o$ as a tree

A type of $\mathtt{Typ}^{111}$ is in the set $\mathtt{Typ}^{001}$ if its
support does not hold an infinite branch ending by $1^{\omega}$. For instance,
this excludes the $T$ defined by $T=(\,)\rightarrow T$ (i.e.,
$T=(\,)\rightarrow(\,)\rightarrow\ldots$). This restriction means that we may
only have finite series of arrows in a type. Indeed, 001-normal forms, even
though they may be infinite, contain only finite series of abstraction nodes
(e.g., $\lambda x.\lambda x\ldots$ is not legal).

We just write $\mathtt{Typ}$ for $\mathtt{Typ}^{001}$ and consider only
sequence types which hold only types from $\mathtt{Typ}$.

When a family of sequence types $(F^{i})_{{i\in I}}$ is disjoint, then there
is no overlapping of typing information between the $F^{i}$, and $\uplus_{i\in
I}F^{i}$ is defined.

###  4.2. Rigid Derivations

A $\mathtt{S}$-context $C$ is a total function from $\mathscr{V}$ to the set
of (001-)sequence types, for instance, $x:(S_{k})_{{k\in K}}$ is the context
which assigns $(S_{k})_{{k\in K}}$ to $x$ and $(\,)$ to every other variable.
The domain of $C$ is $\mathtt{dom}(C)=\\{x\in\mathscr{V}\,|\,C(x)\neq(\,)\\}$.
We define the join of contexts pointwise. If
$\mathtt{dom}(C)\cap\mathtt{dom}(D)=\emptyset$, we may write $C;D$ instead of
$C\uplus D$. A judgment is a triple of the form $C\vdash t:T$, where $C$ is a
context, $t$ a 001-term and $T$ is a (001-)type. A sequence judgment is a
sequence of judgments $(C_{k}\vdash t:T_{k})_{k\in K}$ (notice that these
judgments have the same subject $t$). For instance, if $5\in K$, then the
judgment on track 5 is $C_{5}\vdash t:S_{5}$.

The set of $\mathtt{S}$-derivations (metavariable $P$) is defined
coinductively by the rules of Fig. 10.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 35.98589pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=74.74956pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:(k\cdot T)\vdash x:T$}}}}\hskip 14.22636pt\hskip 14.22636pt\hskip
14.22636pt{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 4.0278pt\hbox{$\displaystyle\penalty 1C;x:(S_{k})_{{k\in
K}}\vdash t:T$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=92.03621pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
C\vdash\lambda x.t:(S_{k})_{{k\in K}}\rightarrow T$}}}}\\\\[19.91684pt]
{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1C\vdash t:(S_{k})_{{k\in K}}\rightarrow
T\hskip 14.22636pt(D_{k}\vdash u:S_{k})_{{k\in K}}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=154.42416pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
28.73729pt\hbox{$\displaystyle C\uplus(\uplus_{{k\in K}}D_{k})\vdash
t\,u:T$}}}}\end{array}$

Figure 10. System $\mathtt{S}$

In the axiom rule, $k$ is called an axiom track. In the $\mathtt{app}$-rule,
the contexts must be disjoint, so that no track conflict occurs. Otherwise,
$\mathtt{app}$-rule cannot be applied.

Derivations from system $\mathtt{S}$ may be seen as labelled trees: we define
the support of $P\rhd C\vdash t:T$ coinductively:
$\mathtt{supp}(P)=\\{\varepsilon\\}$ if $P$ is an axiom rule,
$\mathtt{supp}(P)=\\{\varepsilon\\}\cup 0\mathord{\cdot}\mathtt{supp}(P_{0})$
if $t=\lambda x.t_{0}$ and $P_{0}$ is the subderivation typing $t_{0}$,
$\mathtt{supp}(P)=\\{\varepsilon\\}\cup
1\mathord{\cdot}\mathtt{supp}(P_{1})\cup_{{k\in
K}}k\mathord{\cdot}\mathtt{supp}(P_{k})$ if $t=t_{1}\,t_{2},~{}P_{1}$ is the
left subderivation typing $t_{1}$ and $P_{k}$ the subderivation typing $t_{2}$
on track $k$. The $P_{k}$ ($k\in K$) are called argument derivations.
Graphically, an $\mathtt{app}$-rule may be represented as in the top of Fig.
11:

$C\vdash
t:(2\mathord{\cdot}S_{2},3\mathord{\cdot}S_{3},5\mathord{\cdot}S_{5})\rightarrow
T$$D_{2}\vdash u:S_{2}$$D_{3}\vdash u:S_{3}$$D_{5}\vdash u:S_{5}$$C\uplus
D_{2}\uplus D_{3}\uplus D_{5}\vdash t\,u:T$1235Application node as a labelled
tree ${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1C\vdash
t:(2\mathord{\cdot}S_{2},3\mathord{\cdot}S_{3},5\mathord{\cdot}S_{5})\rightarrow
T\hskip 14.22636pt\hskip 5.69046ptD_{2}\vdash
u:S_{2}~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}\hskip
14.22636ptD_{3}\vdash
u:S_{3}~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[3]}\hskip
14.22636ptD_{5}\vdash
u:S_{5}~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[5]}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=344.248pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 117.7345pt\hbox{$\displaystyle C\uplus
D_{2}\uplus D_{3}\uplus D_{5}\vdash t\,u:T$}}}}$Compact representation

Figure 11. Representing $\mathtt{app}$-nodes in system $\mathtt{S}$

In this figure, argument judgments are on tracks 2, 4 and 5 (indicated in red)
and the left-hand side judgment is on track 1 (compare with Fig. 5). The same
$\mathtt{app}$-rule has an alternative representation at the bottom of Fig.
11, where argument tracks are indicated between red square brackets inside the
argument judgments, whereas track 1 is omitted.

######  Example 3.

In order to gain space, we do not write right-hand sides of axioms. We set
$S_{\mathtt{ex}}=(8\mathord{\cdot}o,3\mathord{\cdot}o^{\prime},2\mathord{\cdot}o)\rightarrow
o^{\prime}$. We indicate the track of argument derivations between brackets
e.g.,
$x:\\!(2\mathord{\cdot}o^{\prime})\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[3]}$
means that judgment $x:\\!(2\mathord{\cdot}o^{\prime})\vdash
x\\!:\\!o^{\prime}$ is on track 3.

$P_{\mathtt{ex}}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 17.8229pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=38.4236pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:\\!\\!(4\mathord{\cdot}S_{\mathtt{ex}})$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\hskip 17.07182pt\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.00345pt\hbox{$\displaystyle\penalty 1\phantom{.}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=32.78468pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:\\!(9\mathord{\cdot}o)$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}\hskip
14.22636pt\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.77345pt\hbox{$\displaystyle\penalty 1\phantom{.}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=34.32469pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:\\!(2\mathord{\cdot}o^{\prime})$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[3]}\hskip
14.22636pt\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.00345pt\hbox{$\displaystyle\penalty 1\phantom{.}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=32.78468pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:\\!(5\mathord{\cdot}o)$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[8]}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=398.49542pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
102.65057pt\hbox{$\displaystyle
x:(2\mathord{\cdot}o^{\prime},4\mathord{\cdot}(8\mathord{\cdot}o,3\mathord{\cdot}o^{\prime},2\mathord{\cdot}o)\rightarrow
o^{\prime},5\mathord{\cdot}o,9\mathord{\cdot}o)\vdash xx:o^{\prime}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=443.82541pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern
119.06557pt\hbox{$\displaystyle\vdash\lambda
x.xx:(2\mathord{\cdot}o^{\prime},4\mathord{\cdot}(8\mathord{\cdot}o,3\mathord{\cdot}o^{\prime},2\mathord{\cdot}o)\rightarrow
o^{\prime},5\mathord{\cdot}o,9\mathord{\cdot}o)\rightarrow o^{\prime}$}}}}$

In the $\mathtt{ax}$-rule concluding with $x:(5\mathord{\cdot}o)\vdash x:o$,
the axiom track is 5.

In Example 3 above,
$\mathtt{supp}(P_{\mathtt{ex}})=\\{\varepsilon,0,0\mathord{\cdot}1,0\mathord{\cdot}2,0\mathord{\cdot}3,0\mathord{\cdot}8\\}$
and we have $P_{\mathtt{ex}}(0\mathord{\cdot}8)=x:(5\mathord{\cdot}o)\vdash
x:o$. In particular, this judgment is on the argument track 8 of the
$\mathtt{app}$-rule at position 0.

Collapse. When we forget about tracks, a sequence naturally collapses on a
multiset e.g., $(3\mathord{\cdot}a,5\mathord{\cdot}b,8\mathord{\cdot}a)$
collapses on $[a,b,a]$. If this collapse is performed (coinductively)for all
the sequences nested in derivations, then the derivations of $\mathtt{S}$ will
collapse on derivations of $\mathscr{R}$. For instance, if we set
$\sigma_{\mathtt{ex}}=[o,o^{\prime},o]\rightarrow o^{\prime}$, the derivation
$P_{\mathtt{ex}}$ of Example 3 collapses on:

$\Pi_{\mathtt{ex}}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 37.04755pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 11.21465pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=25.20708pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:\sigma_{\mathtt{ex}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\\\ \hskip 5.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 10.83675pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=24.45128pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[o]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\\\ \hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 11.60675pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=25.99129pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[o^{\prime}]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\\\ \hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 10.83675pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=24.45128pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[o]$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=134.3052pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[o^{\prime},[o,o^{\prime},o]\rightarrow o^{\prime},o,o]\vdash
xx:o^{\prime}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=168.52403pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern
12.24826pt\hbox{$\displaystyle\vdash\lambda
x.xx:[o^{\prime},[o,o^{\prime},o]\rightarrow o^{\prime},o,o]\rightarrow
o^{\prime}$}}}}$

######  Remark 5.

The collapse turns out to be surjective: every $\mathtt{S}$-derivation is the
collapse of a $\mathscr{R}$-derivation (it is non-trivial). Tracks can be
interpreted as a very low-level specification for derivations, but as we said,
they are necessary to express approximability and to prove the main
interesting properties of system $\mathtt{S}$. However, while working with
derivations and understanding some of the main intuitions of this article, it
is still easier to just use multiset intersection and put tracks under the
carpet.

Useful notations. For the proofs of Sec. 7, the following notations will be
needed. The reader who does not want to read the proofs can skip them.

  * •

For applications: assume that $P$ types $t$, $a\in\mathtt{supp}(P)$ and
$a=a_{*}\mathord{\cdot}1^{n}$. Then $t|_{a_{*}}$ is of the form
$t|_{a}\,t_{1}\ldots t_{n}$

    * –

The set $\mathtt{ArgTr}^{i}_{P}(a)$ (for $1\leqslant i\leqslant n$) contains
the tracks of argument derivations typing the $i$-th argument $t_{i}$ below
$a$.

    * –

The set $\mathtt{ArgPos}^{i}_{P}(a)$ contains the positions of those
subderivations.

Formally, we set $1\leqslant i\leqslant n$,
$\mathtt{ArgTr}^{i}_{P}(a)=\\{k\geqslant
2\,|\,a_{*}\mathord{\cdot}1^{n-i}\mathord{\cdot}k\in\mathtt{supp}(P)\\}$ and
$\mathtt{ArgPos}^{i}_{P}(a)=a_{*}\mathord{\cdot}1^{n-i}\mathord{\cdot}\mathtt{ArgTr}^{i}(a)=\\{a_{*}\mathord{\cdot}1^{n-i}\mathord{\cdot}k\in\mathtt{supp}(P)\,|\,k\geqslant
2\\}$. When $i$ is omitted, $i=1$ is assumed, i.e.,
$\mathtt{ArgTr}_{P}(a)=\mathtt{ArgTr}^{1}_{P}(a)$.

  * •

For variables and binding: If $a\in A:=\mathtt{supp}(P)$ and
$x\in\mathscr{V}$, we set $\mathtt{Ax}^{P}_{a}(x)=\\{a_{0}\in A\,|\,a\leqslant
a_{0},\,t(a)=x,\nexists a_{0}^{\prime},\,a\leqslant a_{0}^{\prime}\leqslant
a_{0},\,t(a^{\prime}_{0})=\lambda x\\}$. Thus, $\mathtt{Ax}^{P}_{a}(x)$ is the
set of positions of $\mathtt{ax}$-rules in $P$ above $a$ typing occurrences of
$x$ that are not bound at $a$. If $a_{0}\in A$ is an axiom, we write
$\mathtt{tr}^{P}(a_{0})$ for its associated axiom track.

  * •

We write $\mathtt{Ax}^{P}$ for the set of all axiom positions in
$\mathtt{supp}(P)$.

Usually, $P$ is implicit and we write only $\mathtt{ArgTr}^{i}(a)$,
$\mathtt{ArgPos}^{i}(a)$, $\mathtt{Ax}_{a}(x)$ and $\mathtt{tr}(a)$.

For instance, in $P_{\mathtt{ex}}$ (Example 3),
$\mathtt{ArgTr}^{1}(0\mathord{\cdot}1)=\\{2,3,8\\}$ and
$\mathtt{ArgPos}^{1}(0\mathord{\cdot}1)=\\{0\mathord{\cdot}2,0\mathord{\cdot}3,0\mathord{\cdot}8\\}$
(with $a_{0}=0$). Moreover, $\mathtt{Ax}_{0}(x)=\\{01,02,03,08\\}$,
$\mathtt{Ax}_{\varepsilon}(x)=\emptyset$ and $\mathtt{tr}(01)=4$,
$\mathtt{tr}^{P}(08)=5$, whereas $\mathtt{tr}^{P}(0)$ is not defined.

##  5\. Statics and Dynamics

In this section, we present bipositions, which allow pointing inside
$\mathtt{S}$-derivation (Sec. 5.1). We use this notion to present and prove
the subject reduction and the subject expansion properties (Sec. 5.3). Proof
expansion is actually defined uniformly. We notice that proof reduction is
deterministic in system $\mathtt{S}$. This leads us to define a notion of
residuation and to formulate a first argument showing that approximability is
indeed not definable while working with multiset intersection (Sec. 5.4).

###  5.1. Bipositions and Bisupport

In a rigid setting as system $\mathtt{S}$, we can identify and point to every
part of a derivation, thus allowing to formulate many useful notions.

If $a\in\mathtt{supp}(P)$, then $a$ points to a judgment inside $P$ typing
$t|_{\overline{a}}$. We write this judgment $\mathtt{C}(a)\vdash
t|_{\overline{a}}:\mathtt{T}(a)$: we say $a$ is an outer position of $P$
($\overline{a}$ is defined on p. • ‣ 4). The context $\mathtt{C}(a)$ and the
type $\mathtt{T}(a)$ should be written $\mathtt{C}^{P}(a)$ and
$\mathtt{T}^{P}(a)$ but we often omit $P$. From now on, we shall also write
$t|_{a}$ and $t(a)$ instead of $t|_{\overline{a}}$ and $t(\overline{a})$.

In Example 3, $P_{\mathtt{ex}}(01)=x:(4\cdot S)\vdash x:S$, so
$\mathtt{C}(01)=x:(4\cdot S)$ i.e., $\mathtt{C}(01)(x)=(4\cdot S)$. Since
$S=(8\cdot o,3\cdot o^{\prime},2\cdot o)\rightarrow o^{\prime}$, we have
$\mathtt{C}(01)(x)(4)=\rightarrow$, $\mathtt{C}(01)(x)(43)=o^{\prime},\
\mathtt{T}(01)(\varepsilon)=\rightarrow$, $\mathtt{T}(01)(1)=o^{\prime}$.
Likewise, $P_{\mathtt{ex}}(03)=x:(2\cdot o^{\prime})\vdash o^{\prime}$, so
that $\mathtt{C}(03)=x:(2\cdot o^{\prime})$ and $\mathtt{T}(03)=o^{\prime}$.
Thus, $\mathtt{C}(03)(x)(2)=o^{\prime}$ and
$\mathtt{T}(03)(\varepsilon)=o^{\prime}$. We also have
$\mathtt{C}(0)(x)=(2\cdot o^{\prime},4\cdot(8\cdot o,3\cdot o^{\prime},2\cdot
o)\rightarrow o^{\prime},5\cdot o,9\cdot o)$, so that
$\mathtt{C}(0)(x)(2)=o^{\prime}$ and $\mathtt{C}(0)(x)(42)=o$.

This motivates the notion of bipositions: a biposition (metavariable
$\mathtt{p}$) is a pointer into a type nested in a judgment of a derivation.

######  Definition 15 (Bisupport).

  * •

A pair $(a,c)$ is a right biposition of $P$ if $a\in\mathtt{supp}(P)$ and
$c\in\mathtt{supp}(\mathtt{T}^{P}(a))$.

  * •