LONG SHORT

# The Space of Interaction

Beniamino Accattoli  Inria & École Polytechnique  Ugo Dal Lago  Università di
Bologna & Inria  Gabriele Vanoni  Università di Bologna & Inria

###### Abstract

The space complexity of functional programs is not well understood. In
particular, traditional implementation techniques are tailored to time
efficiency, and space efficiency induces time _in_ efficiencies, as it prefers
re-computing to saving. Girard’s geometry of interaction underlies an
alternative approach based on the interaction abstract machine (IAM), claimed
as space efficient in the literature. It has also been conjectured to provide
a reasonable notion of space for the $\lambda$-calculus, but such an important
result seems to be elusive.

In this paper we introduce a new intersection type system precisely measuring
the space consumption of the IAM on the typed term. Intersection types have
been repeatedly used to measure time, which they achieve by dropping
idempotency, turning intersections into _multisets_. Here we show that the
space consumption of the IAM is connected to a further structural
modification, turning multisets into _trees_. Tree intersection types lead to
a finer understanding of some space complexity results from the literature.
They also shed new light on the conjecture about reasonable space: we show
that the usual way of encoding Turing machines into the $\lambda$-calculus
_cannot_ be used to prove that the space of the IAM is a reasonable cost
model.

##  I Introduction

Type systems are a form of compositional abstraction in which the behavior of
programs, particularly higher-order programs, is described by _types_ , that
is, specifications of the kinds of objects programs expect in input and are
supposed to produce as output. Typed programs usually _cannot go wrong_ , as
types guarantee the absence of run-time errors [13]. Some type systems ensure
also other properties such as termination or (various forms of) security.

##### Intersection Types and Time Complexity

Among the many existing type systems one can define on top of the pure,
untyped, $\lambda$-calculus [11, 29], _intersection types_ have the peculiar
feature of _characterizing_ a property rather than merely _guaranteeing_ it.
This, in particular, is known to hold for various forms of termination
properties since the pioneering work by Coppo and Dezani in 1978 [14]. More
recently, a variant of intersection types has been proved to reflect
_quantitative_ properties of terms, such as the number of $\beta$-steps to
normal form, or the number of steps of the Krivine abstract machine [30]
(shortened to KAM), as discovered by de Carvalho [21, 22, 23]. The variant
requires dropping idempotency of the intersection operator, therefore
considering $A\wedge A$ as _not_ equivalent to $A$, and ultimately making the
type system strongly related to the modeling of resources as in linear logic.
Such types are sometimes called _multi types_ , as intersections become
multisets. In the last few years, de Carvalho’s results have been dissected
and generalized in various ways [7, 8, 9, 10, 12, 28, 16]. In particular,
research on the topic received renewed attention after some recent progress in
the study of reasonable cost models for the $\lambda$-calculus by Accattoli
and Dal Lago [4] made evident that counting $\beta$-steps gives rise to a
reasonable cost model for time.

##### Sharing, Time, and Space

The mainstream way of implementing the $\lambda$-calculus, at work also in the
KAM, consists of mimicking $\beta$-steps while replacing meta-level
substitutions with a finer approach based on environments. Environments are a
way of realizing a form of _subterm sharing_ , which is known to be mandatory
in order to implement $\beta$-reduction in a time-efficient way. Traditional
environment-based machines do not seem to be the right tool for space-
efficiency. The reason is that these machines create a sharing
annotation—counting as a unit of space—for _every_ $\beta$-step—that is, for
every abstract unit of time. They never garbage collect, because garbage
collection is postponable, and ignoring it is safe for time, as its cost is
negligible (it is polynomial, if not linear, in the number of $\beta$-steps).
As a consequence, their use of space is linear in their time usage, which is
the worst possible use of space. To study space efficiency, then, there are
two possible approaches: either refining environment machines with an explicit
treatment of garbage collection, or exploring alternative execution schemas.
In this work, we follow the second approach.

##### Evaluating Without Sharing

Beyond the mainstream approach, there is an alternative execution schema for
$\lambda$-terms, rooted in Girard’s Geometry of Interaction [27] and Abramsky,
Jagadeesan, and Malacaria game semantics [1], which does _not_ rely on
sharing. The _interaction abstract machine_ (shortened to IAM), first studied
by Mackie [31] and Danos & Regnier [20, 19], evaluates a $\lambda$-term
without tracing every $\beta$-step, thus disentangling time and space. As it
is the case for space-efficient Turing machines, the IAM sometimes repeats
computations to retrieve unsaved intermediate results—thus treading time for
space. Environments are replaced by a _token_ , a data structure where the
machine saves minimal information, and the repetition of computations is
realized via a sophisticated backtracking mechanism (unrelated to backtracking
as in control operators or classical logic). The minimal information in the
token amounts to tracing the points along the execution history where the IAM
may need to backtrack. The entries of the token are _trees_ of pointers called
_logged positions_ in a recent presentation of the IAM by Accattoli, Dal Lago,
and Vanoni [5] (called instead _exponential signatures_ by Danos & Regnier
[20]). Everything else is ignored, in particular the token does not record
encountered $\beta$-redexes.

Further evidence of the relavance for space of the interaction paradigm, comes
from Ghica’s _Geometry of Synthesis_ [25, 26], in which the geometry of
interaction is seen as a compilation scheme towards circuits, whose
computation space is _finite_ , and of paramount importance.

##### The Subtle Complexity of the IAM

These considerations suggest that the IAM is, roughly, bad for time and good
for space. Interestingly, the situation is subtler. About time, there are
indeed examples showing that the IAM is sometimes exponentially slower than
environment machines. The slow-down however is not uniform, as in many cases
the IAM exhibits good time performances.

The situation about space is not clear, either. The IAM has been used in the
literature for obtaining sub-linear space bounds for functional programs (Dal
Lago and Schöpp [34, 18], Mazza [32] and Ghica [25]), something hardly
achievable with traditional environment machines. Having a close look at these
results, however, one realizes that those bounds rely crucially on some tweaks
(restricting to certain $\lambda$-terms or extending the language with ad-hoc
constructs) and that they do not seem to be achievable on ordinary
$\lambda$-terms.

A further evidence of the ambiguous space behavior of the IAM is that the
folklore conjecture that the IAM space usage is a reasonable space cost model
(that is, linearly related to the one of Turing machines) has been circulating
among specialists for years, but has never found an answer.

##### Multi Types and the Time of the IAM

Very recently, there have been advances in the understanding of the subtle
time behavior of the IAM. Accattoli, Dal Lago, and Vanoni have shown in [6]
how to extract exact time bounds for the IAM from multi types derivations.
Interestingly, they use the same types as de Carvalho’s, despite the IAM and
the KAM computing in very different ways. While the time of the KAM is given
by the multiplicity of the multi sets in multi types, they show that the time
of the IAM requires to take into account also the size of the involved types.
The result also provides a high-level understanding for the time
(in)efficiency of the IAM: the inefficiency is proportional to the size of
types. Since higher-order types are bigger than first-order ones, the more a
program uses higher-order types the more its execution with the IAM is slower
than with, say, the KAM.

###  I-A Contributions of the Paper

The aim of this paper is to provide advances in the understanding of the
subtle _space_ behavior of the IAM. Inspired by the mentioned recent results
by Accattoli, Dal Lago, and Vanoni, we introduce a new variant of multi types
from which we extract _exact space bounds_ for the IAM. To our knowledge, it
is the first use of intersection/multi types to measure space.

A key point is that multi types as used in [6]—as well as in the many recent
papers to extract quantitative bounds on $\lambda$-terms cited above—cannot
measure the space consumption of the IAM, as they do not have enough
structure. Our work shows that at the type level, indeed, one needs to add a
_tree_ structure to multi sets, similarly to how measuring time requires
switching from idempotent intersections to multisets.

Once the main result is proved, we show how to use it to understand the subtle
space behavior of the IAM. Here, the main insight is a negative perspective
about the elusive conjecture that the space of the IAM is a reasonable cost
model. We also show that the new type system enlightens the key ingredients of
the sub-linear space bounds in the literature.

##### Tree Types

Usually, multi types are structured in two mutually recursive and disjoint
layers, linear types and multisets of linear types. Our types also have two
layers, but they are no longer disjoint, as multisets can also contain
multisets, not only linear types. This way multisets can naturally be seen as
_trees_ , whose internal nodes are multisets and whose leaves are linear
types. Such tree types are very natural, and probably of independent interest.
While flattening the tree structure recovers an ordinary multi type, the
converse operation cannot be done in a canonical way. This fact shows that
tree types add something new, they do not simply express a structure already
present in multi types.

Actually, the tree structure reflects information about the token. The
intuition is that while the number of leaves of a tree type counts the
different uses of a variable/argument—as for multi types—internal nodes on the
path to a leaf instead count how many backtracking pointers are stored in the
token by the time the IAM gets to that copy.

##### The Complexity Analysis

Our space bounds are obtained by building on the technique developed by
Accattoli, Dal Lago, and Vanoni in [6], which is inherently different from the
one by de Carvalho and used in other recent works. The technique in [6]
amounts to first defining an auxiliary machine evaluating multi type
derivations and showing it bisimilar to the IAM. In this way, we obtain a
representation of the states of the IAM run on the type derivation. Then,
bounds are extracted from a global analysis based on _weighted_ type
derivations. We proceed similarly, replacing multi types with tree types, and
introducing a new system of weights for space, based on the depth of tree
types as trees.

Once the subtle bisimulation is established, our space complexity analysis is
extremely simple, and also naturally provides exact bounds. This provides
evidence that our types system is not ad-hoc. On the contrary, we believe it
unveils a fundamental enrichment of multi types, deserving further studies.

##### Background on Reasonable Space

In order to discuss the mentioned conjecture about reasonable space, let us
provide some background. First of all, studying interesting space complexity
classes such as Ł, requires being able to measure _sub-linear_ space. There is
a recent result in the literature about reasonable space for the
$\lambda$-calculus, by Forster, Kunze, and Roth [24], but their cost
model—namely, the size of the term—can only measure linear and super-linear
space, and thus it is not a solution for the general problem.

Now, showing that a cost model is reasonable requires studying the
relationship with another known-to-be reasonable model, typically Turing
machines. While for time the delicate direction is the simulation of the
$\lambda$-calculus into Turing machines, for space the subtle one is the
simulation of Turing machines in the $\lambda$-calculus, as it is hard to use
as little space as a Turing machine.

The iteration of the transition function of Turing machines is a form of tail
recursion, which in the $\lambda$-calculus is encoded via fixed-point
operators. Such operators are also used to represent minimization in the
encoding of partial recursive functions. Our insight about the reasonable
space conjecture stems from an analysis of fixed-points operators in our type
system.

##### The Elusive Reasonable Space Conjecture

Our contribution here is the fact that the IAM performs poorly when evaluating
fixed-point operators, namely using an amount of space which is always at
least _linear_ in the number of performed recursive calls. This is done by
deriving the type (schema) of a specific fixed-point operator in our system,
then showing that its use of space is proportional to its use of time.

The specific operator we type is the one used in the encoding of Turing
machines in the $\lambda$-calculus used by Accattoli and Dal Lago in their
study of reasonable time [15, 3], as well as by Forster, Kunze, and Roth in
[24]. Seeing it as the natural way of encoding tail recursion, it follows that
the IAM space performance is poor with tail recursion, and, in turn, with the
natural way of encoding Turing machines.

Summing up, our insight is that a positive answer to the conjecture cannot be
done using the standard encoding of Turing machines, which explains the
elusiveness of the conjecture.

##### Trees Density

A way of abstracting away from the issue with fixed-points is to look at how
information is organized in the tree structure of tree types, itself
reflecting the structure of (logged positions in) the token. When the tree is
dense (its height is roughly the log of its number of nodes), then the IAM
execution is space-efficient, while when the tree is sparse (height close to
the number of nodes) it is inefficient—the type schema for fixed-points is
indeed sparse.

##### Perspectives

The insight about the density of trees allows to re-understand some results in
the literature, and opens new perspectives. As we detail in Section VIII, it
sheds light on Dal Lago and Schöpp’s space bounds for a functional language
[34, 18], as well as on the encoding of sub-linear space computations in the
$\lambda$-calculus by Mazza [32].

##### Proofs

Proofs are in the Appendix.

##  II Closed Call-by-Name and Abstract Machines

Let $\mathcal{V}$ be a countable set of variables. Terms of the _$\lambda$
-calculus_ $\Lambda$ are defined as follows.

$\begin{array}[]{rrcl}\textsc{$\lambda$-terms}&t,u,r&\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=&x\in\mathcal{V}\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.t\;\;\mbox{\Large{$\mid$}}\;\;tu.\end{array}$

_Free_ and _bound variables_ are defined as usual: $\lambda x.t$ binds $x$ in
$t$. A term is _closed_ when there are no free occurrences of variables in it.
Terms are considered modulo $\alpha$-equivalence, and capture-avoiding (meta-
level) substitution of all the free occurrences of $x$ for $u$ in $t$ is noted
$t\\{x{\shortleftarrow}u\\}$. Contexts are just $\lambda$-terms containing
exactly one occurrence of a special symbol, the _hole_ $\langle\cdot\rangle$,
intuitively standing for a removed subterm. Here we adopt _leveled_ contexts,
whose index, i.e. the level, stands for the number of arguments (that is, the
number of !-boxes in linear logic terminology) the hole lies in.

$\begin{array}[]{rclrrrcl}\lx@intercol\hfil\textsc{Leveled
contexts}\hfil\lx@intercol\\\ C_{0}&\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=&\langle\cdot\rangle\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.C_{0}\;\;\mbox{\Large{$\mid$}}\;\;C_{0}t;\\\
C_{n+1}&\mathrel{\mathop{\mathchar 58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=&C_{n+1}t\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.C_{n+1}\;\;\mbox{\Large{$\mid$}}\;\;tC_{n}.\end{array}$

We simply write $C$ for a context whenever the level is not relevant. The
operation replacing the hole $\langle\cdot\rangle$ with a term $t$ in a
context $C$ is noted $C\langle t\rangle$ and called _plugging_.

The operational semantics that we adopt here is weak head evaluation
$\rightarrow_{wh}$, defined as follows:

$(\lambda y.t)ur_{1}\ldots r_{h}\ \ \rightarrow_{wh}\ \
t\\{y{\shortleftarrow}u\\}r_{1}\ldots r_{h}.$

where $t\\{y{\shortleftarrow}u\\}$ is our notation for meta-level
substitution. We further restrict the setting by considering only closed
terms, and refer to our framework as _Closed Call-by-Name_ (shortened to
Closed CbN). Basic well known facts are that in Closed CbN the normal forms
are precisely the abstractions and that $\rightarrow_{wh}$ is deterministic.

##### Abstract Machines Glossary

In this paper, an _abstract machine_ $\mathrm{M}=(s,\rightarrow)$ is a
transition system $\rightarrow$ over a set of states, noted $s$. The machine
considered in this paper moves over the code without ever changing it. A
_position_ in a term $t$ is represented as a pair $(u,C)$ of a sub-term $u$
and a context $C$ such that $C\langle u\rangle=t$. States are composed by a
position $(u,C)$ plus some data structures. A state is _initial_ , and noted
$s_{t}$, if it is positioned on $(t,\langle\cdot\rangle)$, $t$ is closed, and
all the data structures are empty—$t$ is always implicitly considered closed,
without further mention. A state is _final_ if no transitions apply.

A _run_ $\rho\mathrel{\mathop{\mathchar
58\relax}}s\rightarrow^{*}{s^{\prime}}$ is a possibly empty sequence of
transitions, whose length is noted $|\rho|$. An _initial run_ is a run from an
initial state $s_{t}$, and it is also called _a run from $t$_. A state $s$ is
_reachable_ if it is the target state of an initial run. A _complete run_ is
an initial run ending on a final state.

##  III The Interaction Abstract Machine, Revisited

In this section we provide an overview of the Interaction Abstract Machine
(IAM). We adopt the $\lambda$-calculus presentation of the IAM, rather called
$\lambda$IAM and recently developed by Accattoli, Dal Lago, and Vanoni in
[5]—we refer to their work for an in-depth study of the $\lambda$IAM. The
literature usually studies the ($\lambda$)IAM with respect to head evaluation
of potentially open terms, here we only deal with Closed CbN, which is closer
to the practice of functional programming. Keep in mind that the $\lambda$IAM
is an unusual machine, and that finding it hard to grasp is normal. Also, in
[5] there is an alternative explanation of the $\lambda$IAM, that may be
helpful, together with the relationship with proof nets, which is however not
needed here.

<EMAIL_ADDRESS>Positions}&l\mathrel{\mathop{\mathchar 58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=(t,C_{n},L_{n})\hfil\hskip
42.67912pt&\textsc{Tapes}&T\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=\epsilon\;\;\mbox{\Large{$\mid$}}\;\;\bullet{\cdot}T\;\;\mbox{\Large{$\mid$}}\;\;l{\cdot}T\\\
\textsc{Logs}&L_{0}\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar 58\relax}}=\epsilon\qquad
L_{n+1}\mathrel{\mathop{\mathchar 58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=l{\cdot}L_{n}\hfil\hskip
42.67912pt&\textsc{Direction}&d\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\;\;\mbox{\Large{$\mid$}}\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\textsc{States}&s\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar 58\relax}}=(t,C,L,T,d)\hfil\hskip
42.67912pt&&\\\ \end{array}$

<EMAIL_ADDRESS>l@{\hspace{.25cm}}l<EMAIL_ADDRESS>l<EMAIL_ADDRESS>7.11317pt&\mathsf{Context}\hfil\hskip 7.11317pt&\mathsf{Log}\hfil\hskip
7.11317pt&\mathsf{Tape}&&\mathsf{Sub}\mbox{-}\mathsf{term}\hfil\hskip
7.11317pt&\mathsf{Context}\hfil\hskip 7.11317pt&\mathsf{Log}\hfil\hskip
7.11317pt&\mathsf{Tape}\\\ \hline\cr\hfil\hskip 7.11317pt\\\\[-8.0pt]
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{tu}}}\hfil\hskip
7.11317pt&C\hfil\hskip 7.11317pt&L\hfil\hskip 7.11317pt&T&\rightarrow_{\bullet
1}&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{t}}}\hfil\hskip
7.11317pt&C\langle\langle\cdot\rangle u\rangle\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&\bullet{\cdot}T\\\\[3.0pt]
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
x.t}}}\hfil\hskip 7.11317pt&C\hfil\hskip 7.11317pt&L\hfil\hskip
7.11317pt&\bullet{\cdot}T&\rightarrow_{\bullet
2}&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{t}}}\hfil\hskip
7.11317pt&C\langle\lambda x.\langle\cdot\rangle\rangle\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&T\\\\[3.0pt]
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{x}}}\hfil\hskip
7.11317pt&C\langle\lambda x.D_{n}\rangle\hfil\hskip
7.11317pt&L_{n}{\cdot}L\hfil\hskip
7.11317pt&T&\rightarrow_{{\mathsf{var}}}&\lambda x.D_{n}\langle
x\rangle\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C}}}\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&(x,\lambda x.D_{n},L_{n}){\cdot}T\\\\[3.0pt]
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
x.D_{n}\langle x\rangle}}}\hfil\hskip 7.11317pt&C\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&(x,\lambda
x.D_{n},L_{n}){\cdot}T&\rightarrow_{\mathsf{bt}2}&x\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C\langle\lambda
x.D_{n}\rangle}}}\hfil\hskip 7.11317pt&L_{n}{\cdot}L\hfil\hskip
7.11317pt&T\\\\[3.0pt] \cline{1-9}\cr\hfil\hskip 7.11317pt\\\\[-8.0pt]
t\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C\langle\langle\cdot\rangle
u\rangle}}}\hfil\hskip 7.11317pt&L\hfil\hskip
7.11317pt&\bullet{\cdot}T&\rightarrow_{\bullet 3}&tu\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C}}}\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&T\\\\[3.0pt] t\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C\langle\lambda
x.\langle\cdot\rangle\rangle}}}\hfil\hskip 7.11317pt&L\hfil\hskip
7.11317pt&T&\rightarrow_{\bullet 4}&\lambda x.t\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C}}}\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&\bullet{\cdot}T\\\\[3.0pt] t\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C\langle\langle\cdot\rangle
u\rangle}}}\hfil\hskip 7.11317pt&L\hfil\hskip
7.11317pt&l{\cdot}T&\rightarrow_{\mathsf{arg}}&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{u}}}\hfil\hskip
7.11317pt&C\langle t\langle\cdot\rangle\rangle\hfil\hskip
7.11317pt&l{\cdot}L\hfil\hskip 7.11317pt&T\\\\[3.0pt] t\hfil\hskip
7.11317pt&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C\langle
u\langle\cdot\rangle\rangle}}}\hfil\hskip 7.11317pt&l{\cdot}L\hfil\hskip
7.11317pt&T&\rightarrow_{\mathsf{bt}1}&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{u}}}\hfil\hskip
7.11317pt&C\langle\langle\cdot\rangle t\rangle\hfil\hskip
7.11317pt&L\hfil\hskip 7.11317pt&l{\cdot}T\\\\[3.0pt]
\cline{1-9}\cr\end{array}}$

Figure 1: Data structures and transitions of the $\lambda$ Interaction
Abstract Machine ($\lambda$IAM).

##### Bird’s Eye view of the $\lambda$IAM

Intuitively, the behaviour of the $\lambda$IAM can be seen as that of a token
that travels around the syntax tree of the program under evaluation. Similarly
to environment machines such as Krivine’s, it looks for the head variable of a
term. The peculiarity of the $\lambda$IAM is that it does not store the
encountered $\beta$-redexes in an environment. When it finds the head
variable, the $\lambda$IAM looks for the argument which should replace it,
because having no environment, it cannot simply look it up. These two search
mechanisms are realized by two different phases and directions of exploration
of the code, noted
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$.
The functioning is actually more involved because there is also a backtracking
mechanism (which however has nothing to do with backtracking as modeled by
classical logic and continuations), requiring to save and manipulate code
positions in the token. Last, the machine never duplicates the code, but it
distinguishes different uses of a same code (position) using _logs_. There are
no easy intuitions about how logs handle different uses—this is both the magic
and the mystery of the geometry of interaction.

#####  $\lambda$IAM States

The data structures of the $\lambda$IAM are in Fig. 1. The $\lambda$IAM
travels on a $\lambda$-term $t$ carrying data structures—representing the
token—storing information about the computation and determining the next
transition to apply. It travels according to a _direction_ of navigation that
is either
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
or
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$,
pronounced _down_ and _up_.

The _token_ is given by two stacks, called _log_ and _tape_ , whose main
components are _logged positions_. Roughly, a log is a trace of the relevant
positions in the history of a computation, and a logged position is a position
plus a log, meant to trace the history that led to that position. Logs and
logged positions are defined by mutual induction. Note that in the definition
of a logged position, the log is required to have length $n$, where $n$ is the
level of the context of the position. We use $\cdot$ also to concatenate logs,
writing, e.g., $L_{n}\cdot L$, using $L$ for a log of unspecified length. The
_tape_ $T$ is a list of logged positions plus occurrences of the special
symbol $\bullet$, needed to record the crossing of abstractions and
applications.

A _state_ of the machine is given by a position and a token (that is, a log
$L$ and a tape $T$), together with a _direction_. Initial states have the form
$s_{t}\mathrel{\mathop{\mathchar
58\relax}}=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{t}}},\langle\cdot\rangle,\epsilon,\epsilon)$.
Directions are often omitted and represented via colors and underlining:
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
is represented by a  red and underlined code term,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$
by a  blue and underlined code context.

##### Transitions

The transitions of the $\lambda$IAM are in Fig. 1. Their union is noted
$\rightarrow_{\lambda\textsc{IAM}}$. The idea is that
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$-states
$({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{t}}},C,L,T)$
are queries about the head variable of (the head normal form of) $t$ and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$-states
$(t,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{C}}},L,T)$
are queries about the argument of an abstraction. A key point is that
navigation is done locally, moving only between adjacent
positions111Transitions $\rightarrow_{{\mathsf{var}}}$ and
$\rightarrow_{\mathsf{bt}2}$ might not look local, as they jump from a bound
variable occurrence to its binder, and viceversa. If $\lambda$-terms are
represented by implementing occurrences as pointers to their binders, as in
the proof net representation of $\lambda$-terms—upon which some concrete
implementation schemes are based, see [2]—then they are local.. Intuitively,
the machine evaluates the term $t$ until the head abstraction of the head
normal form is found (more explanations below). The transitions realize three
entangled mechanisms.

##### Mechanism 1: Search Up to $\beta$-Redexes

Note that $\rightarrow_{\bullet 1}$ skips the argument and adds a $\bullet$ on
the tape. The idea is that $\bullet$ keeps track that an argument has been
encountered—its identity is however forgotten. Then $\rightarrow_{\bullet 2}$
does the dual job: it skips an abstraction when the tape carries a $\bullet$,
that is, the trace of a previously encountered argument. Note that, when the
$\lambda$IAM moves through a $\beta$-redex with the two steps one after the
other, the token is left unchanged. This mechanism thus realizes search _up to
$\beta$-redexes_, that is, without ever recording them. Note that
$\rightarrow_{\bullet 3}$ and $\rightarrow_{\bullet 4}$ do the same during the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$
phase.

Let us illustrate this mechanism with an example: the first steps of
evaluation on the term $\mathsf{I}((\lambda x.xx)\mathsf{I})$, where
$\mathsf{I}$ is the identity combinator. One can notice that the $\lambda$IAM
traverses one $\beta$-redexes without altering the token, that is empty both
at the beginning and at the end.

<EMAIL_ADDRESS>2.84544pt&\mathsf{Sub}\mbox{-}\mathsf{term}&\mathsf{Context}&\mathsf{Log}&\mathsf{Tape}&\mathsf{Dir}\\\
\cline{1-6}\cr\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{(\lambda
z.z)((\lambda
x.xx)\mathsf{I})}}}&\langle\cdot\rangle&\epsilon&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\bullet 1}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
z.z}}}&\langle\cdot\rangle((\lambda
x.xx)\mathsf{I})&\epsilon&\bullet&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\bullet 1}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{z}}}&(\lambda
z.\langle\cdot\rangle)((\lambda
x.xx)\mathsf{I})&\epsilon&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\end{array}}$

##### Mechanism 2: Finding Variables and Arguments

As a first approximation, navigating in direction
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
corresponds to looking for the head variable of the term code, while
navigating with direction
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$
corresponds to looking for the sub-term to replace the previously found head
variable, what we call _the argument_. More precisely, when the head variable
$x$ of the active subterm is found, transition $\rightarrow_{{\mathsf{var}}}$
switches direction from
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$,
and the machine starts looking for potential substitutions for $x$. The
$\lambda$IAM then moves to the position of the binder $\lambda x$ of $x$, and
starts exploring the context $C$, looking for the first argument up to
$\beta$-redexes. The relative position of $x$ w.r.t. its binder is recorded in
a new logged position that is added to the tape. Since the machine moves out
of a context of level $n$, namely $D_{n}$, the logged position contains the
first $n$ logged positions of the log. Roughly, this is an encoding of the run
that led from the level of $\lambda x.D_{n}\langle x\rangle$ to the occurrence
of $x$ at hand, in case the machine would later need to backtrack.

When the argument $t$ for the abstraction binding the variable $x$ in $l$ is
found, transition $\rightarrow_{\mathsf{arg}}$ switches direction from
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$
to
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$,
making the machine looking for the head variable of $t$. Note that moving to
$t$, the level increases, and that the logged position $l$ is moved from the
tape to the log. The idea is that $l$ is now a completed argument query, and
it becomes part of the history of how the machine got to the current position,
to be potentially used for backtracking. We continue the example of the
previous point: the machine finds the head variable $z$ and looks for its
argument in
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$
mode. When it has been found, the direction turns to
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
again and the process continues as before: first the head variable is found
and then the machine looks for its argument. Let us set
$l_{z}\mathrel{\mathop{\mathchar 58\relax}}=(z,(\lambda
z.\langle\cdot\rangle)((\lambda x.xx)\mathsf{I}),\epsilon)$,
$l_{\langle\cdot\rangle x}\mathrel{\mathop{\mathchar 58\relax}}=(x,\lambda
x.\langle\cdot\rangle x,\epsilon)$ and $l_{y}\mathrel{\mathop{\mathchar
58\relax}}=(y,\lambda y.\langle\cdot\rangle,\epsilon)$.

<EMAIL_ADDRESS>2.84544pt&\mathsf{Sub}\mbox{-}\mathsf{term}&\mathsf{Context}&\mathsf{Log}&\mathsf{Tape}&\mathsf{Dir}\\\
\cline{1-6}\cr\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{z}}}&(\lambda
z.\langle\cdot\rangle)((\lambda
x.xx)\mathsf{I})&\epsilon&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{{\mathsf{var}}}\hfil\hskip 2.84544pt&\lambda
z.z&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\langle\cdot\rangle((\lambda
x.xx)\mathsf{I})}}}&\epsilon&l_{z}&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\rightarrow_{\mathsf{arg}}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{(\lambda
x.xx)\mathsf{I}}}}&\mathsf{I}\langle\cdot\rangle&l_{z}&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\bullet 1}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
x.xx}}}&\mathsf{I}(\langle\cdot\rangle\mathsf{I})&l_{z}&\bullet&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\bullet 2}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{xx}}}&\mathsf{I}((\lambda
x.\langle\cdot\rangle)\mathsf{I}&l_{z}&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\bullet 1}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{x}}}&\mathsf{I}((\lambda
x.\langle\cdot\rangle
x)\mathsf{I})&l_{z}&\bullet&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{{\mathsf{var}}}\hfil\hskip 2.84544pt&\lambda
x.xx&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\mathsf{I}(\langle\cdot\rangle(\lambda
y.y))}}}&l_{z}&l_{\langle\cdot\rangle
x}\cdot\bullet&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\rightarrow_{\mathsf{arg}}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
y.y}}}&\mathsf{I}((\lambda x.xx)\langle\cdot\rangle)&l_{\langle\cdot\rangle
x}\cdot
l_{z}&\bullet&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\bullet 2}\hfil\hskip
2.84544pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{y}}}&\mathsf{I}((\lambda
x.xx)(\lambda y.\langle\cdot\rangle))&l_{\langle\cdot\rangle x}\cdot
l_{z}&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{{\mathsf{var}}}\hfil\hskip 2.84544pt&\lambda
y.y&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\mathsf{I}((\lambda
x.xx)\langle\cdot\rangle)}}}&l_{\langle\cdot\rangle x}\cdot
l_{z}&l_{y}&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\end{array}}$

##### Mechanism 3: Backtracking

It is started by transition $\rightarrow_{\mathsf{bt}1}$. The idea is that the
search for an argument of the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$-phase
has to temporarily stop, because there are no arguments left at the current
level. The search of the argument then has to be done among the arguments of
the variable occurrence that triggered the search, encoded in $l$. Then the
machine enters into backtracking mode, which is denoted by a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$-phase
with a logged position on the tape, to reach the position in $l$. Backtracking
is over when $\rightarrow_{\mathsf{bt}2}$ is fired.

The
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$-phase
and the logged position on the tape mean that the $\lambda$IAM is
backtracking. During backtracking, the machine is not looking for the head
variable of the current code $\lambda x.t$, it is rather going back to the
variable position in the tape, to find its argument. This is realized by
moving to the position in the tape and changing direction. Moreover, the log
$L_{n}$ encapsulated in the logged position is put back on the global log. An
invariant guarantees that the logged position on the tape always contains a
position relative to the active abstraction.

In our example, a backtracking phase starts when the $\lambda$IAM looks for
the argument of $y$. Since $\lambda y.y$ has been virtually substituted for
$x$, its argument is actually the second occurrence of $x$. Backtracking
retrieves the variable which a term was virtually substituted for.

<EMAIL_ADDRESS>5.69046pt&\mathsf{Sub}\mbox{-}\mathsf{term}&\mathsf{Context}&\mathsf{Log}&\mathsf{Tape}&\mathsf{Dir}\\\
\cline{1-6}\cr\hfil\hskip 5.69046pt&\lambda
y.y&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\mathsf{I}((\lambda
x.xx)\langle\cdot\rangle)}}}&l_{\langle\cdot\rangle x}\cdot
l_{z}&l_{y}&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\rightarrow_{\mathsf{bt}1}\hfil\hskip
5.69046pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
x.xx}}}&\mathsf{I}(\langle\cdot\rangle\mathsf{I})&l_{z}&l_{\langle\cdot\rangle
x}\cdot
l_{y}&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{\mathsf{bt}2}\hfil\hskip
5.69046pt&x&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\mathsf{I}((\lambda
x.\langle\cdot\rangle
x)\mathsf{I})}}}&l_{z}&l_{y}&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\rightarrow_{\mathsf{arg}}\hfil\hskip
5.69046pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{x}}}&\mathsf{I}((\lambda
x.x\langle\cdot\rangle)\mathsf{I})&l_{y}\cdot
l_{z}&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\end{array}}$

For the sake of completeness, we conclude the example, which runs until the
head abstraction of the weak head normal form of the term under evaluation,
namely the second occurrence of I, is found. We set
$l_{x\langle\cdot\rangle}\mathrel{\mathop{\mathchar 58\relax}}=(x,\lambda
x.x\langle\cdot\rangle,l_{y})$.

<EMAIL_ADDRESS>5.69046pt&\mathsf{Sub}\mbox{-}\mathsf{term}&\mathsf{Context}&\mathsf{Log}&\mathsf{Tape}&\mathsf{Dir}\\\
\cline{1-6}\cr\hfil\hskip
5.69046pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{x}}}&\mathsf{I}((\lambda
x.x\langle\cdot\rangle)\mathsf{I})&l_{y}\cdot
l_{z}&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\rightarrow_{{\mathsf{var}}}\hfil\hskip 5.69046pt&\lambda
x.xx&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\mathsf{I}(\langle\cdot\rangle(\lambda
y.y))}}}&l_{z}&l_{x\langle\cdot\rangle}&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}\\\
\rightarrow_{\mathsf{arg}}\hfil\hskip
5.69046pt&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
y.y}}}&\mathsf{I}((\lambda
x.xx)\langle\cdot\rangle)&l_{x\langle\cdot\rangle}\cdot
l_{z}&\epsilon&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}\\\
\end{array}}$

##### Basic invariants

Given a state $(t,C,L,T,d)$, the log and the tape, i.e. the token, verify two
easy invariants connecting them to the position $(t,C)$ and the direction $d$.
The log $L$ and the current position $(t,C)$ form a logged position, i.e. the
length of $L$ is exactly the level of the code context $C$222 Then, the length
of $L$ is exactly the number of (linear logic) _boxes_ in which the code term
is contained.. This fact guarantees that the $\lambda$IAM never gets stuck
because the log is too short for transitions $\rightarrow_{{\mathsf{var}}}$
and $\rightarrow_{\mathsf{bt}1}$ to apply.

About the tape, note that every time the machine switches from a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$-state
to an
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$-state
(or vice versa), a logged position is pushed (or popped) from the tape $T$.
Thus, for reachable states, the number of logged positions in $T$ gives the
direction of the state. These intuitions are formalized by the _tape and
direction_ invariant below. Given a direction $d$ we use $d^{n}$ for the
direction obtained by switching $d$ exactly $n$ times (i.e.,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}^{0}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}^{0}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}^{n+1}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}^{n}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}^{n+1}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}^{n}$).

######  Lemma III.1 ($\lambda$IAM basic invariants).

Let $s=(t,C_{n},L,T,d)$ be a reachable state and $|T|_{l}$ the number of
logged positions in $T$. Then

  1. 1.

_Position and log_ : $(t,C_{n},L)$ is a logged position, and

  2. 2.

_Tape and direction_ :
$d={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}^{|T|_{l}}$.

##### Final States

If the $\lambda$IAM starts on the initial state $s_{t}$, the execution may
either never stop or end in a state $s$ of the shape
$s=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\underline{\lambda
x.u}}},C,L,\epsilon)$. The fact that no other shapes are possible for $s$ is
proved in [5].

$\begin{array}[]{c@{\hspace{1cm}}c@{\hspace{1cm}}c}x\mathrel{\mathop{\mathchar
58\relax}}[A]\vdash x\mathrel{\mathop{\mathchar 58\relax}}A\hfil\hskip
28.45274pt&\Gamma\vdash\lambda x.t\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow A\Gamma,x\mathrel{\mathop{\mathchar 58\relax}}T\vdash
t\mathrel{\mathop{\mathchar 58\relax}}A\hfil\hskip
28.45274pt&\Gamma\uplus\Delta\vdash tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\Gamma\vdash t\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow A\Delta\vdash u\mathrel{\mathop{\mathchar
58\relax}}T\\\\[8.0pt] \Gamma\vdash\lambda x.t\mathrel{\mathop{\mathchar
58\relax}}\star\hfil\hskip 28.45274pt&[\uplus_{i=1}^{n}\Gamma_{i}]\vdash
t\mathrel{\mathop{\mathchar 58\relax}}[G_{1},\hbox
to6.00006pt{.\hss.},G_{n}]\lx@proof@logical@and\Gamma_{i}\vdash
t\mathrel{\mathop{\mathchar 58\relax}}G_{i}1\leq i\leq n\hfil\hskip
28.45274pt&\vdash t\mathrel{\mathop{\mathchar
58\relax}}[\cdot]\par\par\end{array}$ Figure 2: The tree type system.

##### Implementation

Usually, the $\lambda$IAM is shown to implement (a micro-step variant of) head
reduction. The details are quite different from those in the usual notion of
implementation for environment machines, such as the KAM. Essentially, it is
shown that the $\lambda$IAM induces a semantics
$\llbracket\cdot\rrbracket_{\text{$\lambda$IAM}}$ of terms that is a sound and
adequate with respect to head reduction, rather than showing a bisimulation
between the machine and head reduction—this is explained at length in [5]. For
the sake of simplicity, here we restrict to Closed CbN. The $\lambda$IAM
semantics then reduces to observing termination: $\llbracket
t\rrbracket_{\text{$\lambda$IAM}}$ is defined if and only if weak head
reduction terminates on $t$. Therefore, we avoid discussing semantics and only
study termination. We say that the _$\lambda$ IAM implements Closed CbN_ when
its execution from the initial state $s_{t}$ reaches a final state if and only
if $\rightarrow_{wh}$ terminates on $t$, for every closed term $t$.

######  Theorem III.2 ([5]).

The $\lambda$IAM implements Closed CbN.

#####  $\lambda$IAM Space Consumption

The space needed to represent a $\lambda$IAM state is given by the following
definition (the meta-variable $\Gamma$ to denote either a tape $T$ or a log
$L$):

$\begin{array}[]{rclrcl}\lx@intercol\hfil|(t,C,L,T,d)|_{\mathsf{sp}}\mathrel{\mathop{\mathchar
<EMAIL_ADDRESS>|(x,D,L^{\prime})|_{\mathsf{sp}}&\mathrel{\mathop{\mathchar
58\relax}}=&\mathsf{X}+|L^{\prime}|_{\mathsf{sp}}&|\epsilon|_{\mathsf{sp}}&\mathrel{\mathop{\mathchar
58\relax}}=&0\\\\[3.0pt]
|l\cdot\Gamma|_{\mathsf{sp}}&\mathrel{\mathop{\mathchar
58\relax}}=&|l|_{\mathsf{sp}}+|\Gamma|_{\mathsf{sp}}&|\bullet\cdot
T|_{\mathsf{sp}}&\mathrel{\mathop{\mathchar
58\relax}}=&1+|T|_{\mathsf{sp}}\end{array}$

The value of the unknown $\mathsf{X}$ is simply the size of a pointer to a
subterm of the term under evaluation, i.e. $\mathsf{X}=\log|C\langle
t\rangle|$. Then, we are able to define the space of a $\lambda$IAM run by
taking the maximum size of the states reached during the run.

######  Definition III.3.

Let $\rho\mathrel{\mathop{\mathchar
58\relax}}s_{0}\rightarrow_{\lambda\textsc{IAM}}^{*}s$ be a $\lambda$IAM run.
Then,

$|\rho|_{\mathsf{sp}}\mathrel{\mathop{\mathchar
58\relax}}=\max_{{s^{\prime}}\in\rho}|{s^{\prime}}|_{\mathsf{sp}}$

It is worth noticing what happens in the case of diverging computations. In
principle, two cases could occur: either the space consumption is finite, or
it is infinite. Actually, it is easy to prove that the first case is not
possible.

######  Proposition III.4.

Let $\rho$ be an infinite $\lambda$IAM run.
Then $|\rho|_{\mathsf{sp}}=\infty$.

##  IV Tree (Intersection) Types

Here we introduce a type system that we shall use to measure the space used by
$\lambda$IAM runs.

##### From Intersections Types to Tree Types

The framework that we adopt is the one of intersection types, with three
tweaks:

  1. 1.

_No idempotency_ : we use the non-idempotent variant, where the intersection
type $A\wedge A$ is not equivalent to $A$, and with strong ties to linear
logic and time analyses, because it takes into account how many times a
resource/type $A$ is used, and not just whether $A$ is used or not. Non-
idempotent intersections are multisets, which is why these types are sometimes
called _multi types_ and an intersection $A\wedge B\wedge A$ is rather noted
$[A,B,A]$.

  2. 2.

_Nesting/tree shape_ : multi types are usually defined by two mutually
dependent layers, a linear one containing ground types and (linear) arrow
types, and the multiset level containing linear types. Here we also have two
layers, except that we allow multisets to also contain multisets, thus we can
have $[A,[[B,B],A,[A]],A,B]$. A nested multiset is a _tree_ whose leaves are
linear types and whose internal nodes are nested multisets.

  3. 3.

_No commutativity_ : we also consider _non-commutative_ tree types. Removing
commutativity turns multisets into lists, or sequences, and trees into ordered
trees. Removing commutativity is an inessential tweak. Our study does not
depend on the ordered structure, we shall only need bijections between
multisets, to describe the reformulation of the $\lambda$IAM on type
derivations, and these bijections are just more easily managed if
commutativity is removed. This _rigid_ approach is also used by Tsukada,
Asada, and Ong [35] and Mazza, Pellissier, and Vial [33]. The inessential
aspect is stressed by referring to our types as to _tree types_ , rather than
as to _ordered tree types_ , despite adopting the ordered variant.

##### Basic Definitions

As for multi types, there are two mutually defined layers of types, _linear
types_ and _tree types_.

<EMAIL_ADDRESS>types}&A,A^{\prime}&\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=&\star\mathrel{\big{|}}T\rightarrow A\hfil\hskip 17.07182pt\\\
\textsc{Tree types}&T,T^{\prime}&\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=&[G_{1},\ldots,G_{n}]\hfil\hskip 17.07182pt&n\geq 0\\\
\textsc{(Generic) Types}&G,G^{\prime}&\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=&A\mathrel{\big{|}}T\hfil\hskip 17.07182pt\end{array}$

Note that there is a ground type $\star$, which can be thought as the type of
normal forms, that in Closed CbN are precisely abstractions. Note also that
arrow (linear) types $T\rightarrow A$ can have a tree type only on the left.
About trees, since commutativity is ruled out, we have, for instance, that
$[A,A^{\prime}]\neq[A^{\prime},A]$. Note that the empty tree type/sequence is
a valid type, which is noted $[\cdot]$. The concatenation of two sequences $T$
and $T^{\prime}$ is noted $T\uplus T^{\prime}$. We use $|T|$ for the length of
$T$ as a sequence, that is, $|[G_{1},\hbox
to6.00006pt{.\hss.},G_{n}]|\mathrel{\mathop{\mathchar 58\relax}}=n$.

Type judgments have the form $\Gamma\vdash t\mathrel{\mathop{\mathchar
58\relax}}G$, where $\Gamma$ is a type environment, defined below. Type
derivations are noted $\pi$ and we write $\pi\;\triangleright\Gamma\vdash
t\mathrel{\mathop{\mathchar 58\relax}}G$ for a type derivation $\pi$ of ending
judgment $\Gamma\vdash t\mathrel{\mathop{\mathchar 58\relax}}G$. Type
environments, ranged over by $\Gamma,\Delta$ are total maps from variables to
tree types such that only finitely many variables are mapped to non-empty tree
types, and we write $\Gamma=x_{1}\mathrel{\mathop{\mathchar
58\relax}}T_{1},\ldots,x_{n}\mathrel{\mathop{\mathchar 58\relax}}T_{n}$ if
$dom(\Gamma)=\mathinner{\left\\{x_{1},\ldots,x_{n}\right\\}}$—note that type
environments _are_ commutative, what is non-commutative is the sequence
constructor $[\cdot]$, only. Given two type environments $\Gamma,\Delta$, we
use $\Gamma\uplus\Delta$ for the type environment assigning to every variable
$x$ the list $\Gamma(x)\uplus\Delta(x)$.

The typing rules are in Fig. 2. With respect to the literature, the difference
is in rule T-many. There are two differences. The first one is the already
mentioned fact that premises may assign both linear types and tree types,
while the literature usually only allows linear types. The second one is that
the rule surrounds $\Gamma\mathrel{\mathop{\mathchar
58\relax}}=\uplus_{i=1}^{n}\Gamma_{i}$ with an additional nesting level—the
notation $[\Gamma]$ standing for the type environment
$x_{1}\mathrel{\mathop{\mathchar
58\relax}}[T_{1}],\ldots,x_{n}\mathrel{\mathop{\mathchar 58\relax}}[T_{n}]$ if
$\Gamma=x_{1}\mathrel{\mathop{\mathchar
58\relax}}T_{1},\ldots,x_{n}\mathrel{\mathop{\mathchar 58\relax}}T_{n}$.

##### A Small Example

We show an instance of the rule T-many in the delicate case in which the
premises contain the same free variable $x$.

$x\mathrel{\mathop{\mathchar 58\relax}}[[A_{1},A_{2}]]\vdash
t\mathrel{\mathop{\mathchar 58\relax}}[G_{1},G_{2}]\lx@proof@logical@and
x\mathrel{\mathop{\mathchar 58\relax}}[A_{1}]\vdash
t\mathrel{\mathop{\mathchar 58\relax}}G_{1}x\mathrel{\mathop{\mathchar
58\relax}}[A_{2}]\vdash t\mathrel{\mathop{\mathchar 58\relax}}G_{2}$

In particular, please note that first $[A_{1}]$ and $[A_{2}]$ are joined, and
then they are surrounded by an additional nesting level. The other option
would have been $x\mathrel{\mathop{\mathchar 58\relax}}[[A_{1}],[A_{2}]]$, but
it is not what T-many does.

##### Leaves Extraction and Leaf Contexts

Every tree type $T$ induces the sequence $\underline{T}$— equivalently, the
flat tree type—of its leaves, defined by the following _leaves extraction_
operation.

$\small\begin{array}[]{r<EMAIL_ADDRESS>58\relax}}=[\cdot]\hskip 9.38945pt&([A]\uplus
T)^{\ell}\mathrel{\mathop{\mathchar 58\relax}}=[A]\uplus T^{\ell}\hfil\hskip
9.38945pt&([T^{\prime}]\uplus T)^{\ell}\mathrel{\mathop{\mathchar
58\relax}}=T^{\prime\ell}\uplus T^{\ell}\end{array}$

We shall describe the leaves of a tree type also via a notion of leaf context.

<EMAIL_ADDRESS>ctxs}\hskip
14.22636pt&\mathbb{L}\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar 58\relax}}=[G_{1},\hbox
to6.00006pt{.\hss.},\langle\cdot\rangle,\hbox
to6.00006pt{.\hss.},G_{n}]\mathrel{\big{|}}[G_{1},\hbox
to6.00006pt{.\hss.},\mathbb{L},\hbox to6.00006pt{.\hss.},G_{n}]\end{array}$

If $T^{\ell}=[A_{1},\hbox to6.00006pt{.\hss.},A_{n}]$ then for every $A_{i}$
there is a leaf context $\mathbb{L}^{i}$ such that $T=\mathbb{L}^{i}\langle
A_{i}\rangle$. Therefore, we shall use the notation $T=\mathbb{L}^{i}\langle
A\rangle$, or even simply $T^{i}=A$, to say that the linear type $A$ is the
$i$-th leaf of $T$.

In the following we use two basic properties of the type system, collected in
the following straightforward lemma. One is the absence of weakening, and the
other one is a correspondence between sequence types and axioms.

######  Lemma IV.1 (Relevance and axiom sequences).

If $\pi\;\triangleright\Gamma\vdash t\mathrel{\mathop{\mathchar 58\relax}}A$
then $dom(\Gamma)\subseteq\mathsf{fv}(t)$, thus if $t$ is closed then $\Gamma$
is empty. Moreover, there are exactly $|\Gamma(x)^{\ell}|$ axioms typing $x$
in $\pi$, which appear from left to right as leaves of $\pi$ (seen as an
ordered tree) in the order given by $\Gamma(x)^{\ell}=[A_{1},\ldots,A_{k}]$
and that the $i$-th axiom types $x$ with $A_{i}$.

##### Characterization of Termination

It is well-known that intersection and multi types characterize Closed CbN
termination, that is, they type _all_ and only those $\lambda$-terms that
terminate with respect to Closed CbN. Moreover, every term that is Closed CbN
normalizable can be typed with $\star$. The same characterization holds with
tree types, following the standard recipe333Namely, substitution lemma plus
subject reduction for correctness, and anti-substitution lemma, subject
expansion, and typability of all normal forms for completeness (here trivial,
because all normal forms are typed by $\textsc{T-}\lambda_{\star}$). for multi
types, without surprises. See the Appendix for details.

######  Theorem IV.2 (Correctness and completeness of tree types for Closed
CbN).

A closed term $t$ is Closed CbN normalizable if and only if there exists a
tree type derivation $\pi\;\triangleright\vdash t\mathrel{\mathop{\mathchar
58\relax}}\star$.

##### Relationship with Multi Types

The leaves extraction operation can easily be extended to a flattening
function turning a tree type into a multi type. Flattening can also be
extended to derivations, by collapsing trees of T-many rules into the more
traditional rule for multi sets that does not _nodify_ the type context. In
this way, one obtains a forgetful transformation, easily defined by induction
on derivations. A converse _lifting_ transformation, however, cannot be
defined by induction on derivations—it is unclear how to define it on
applications. This fact is evidence that tree types are strictly richer than
multi types, because the tree structure cannot be inferred from the multiset
one.

##  V The Tree IAM

This section introduces a machine evaluating type derivations, the _Tree IAM_
, or _TIAM_ , that mimics the $\lambda$IAM directly on top of a type
derivation $\pi$. It is the key tool that we shall use to measure the space
cost of $\lambda$IAM runs. The TIAM is a very minor variation over the similar
SIAM machine evaluating type derivations for sequence types by Accattoli, Dal
Lago, and Vanoni in [6]. This and the next section mostly just recall and
adapt notions and results from that paper.

##### Preamble about Duplications and (No) Logs

$\beta$-reducing a $\lambda$-term (potentially) duplicates arguments, whose
different copies may be used differently, typically being applied to different
further arguments. The $\lambda$IAM never duplicate arguments, but has
nonetheless to distinguish different uses of the same piece of code. This is
why it uses _logged_ positions instead of simple positions: the log is a trace
of (part of) the previous run that allows to distinguishing different uses of
the position.

The key point of multi/tree type derivations is that duplication is explicitly
accounted for, _in advance_ , by multisets/trees: all arguments come with as
many type derivations as the times they are duplicated during evaluation. With
tree types, the number of copies is the number of leaves of the tree. Note
that a multi/tree type derivation may be way bigger than the term itself,
while this is not possible with, say, simple types.

The intuition behind the TIAM is that the walk over the code done by the
$\lambda$IAM can be rephrased and simplified on multi/tree type derivations,
because the mechanism of logs—needed to distinguish different copies of
arguments—is no longer needed, since all copies are already there: simple
positions in the type derivation (not in the term!) are informative enough.

$\begin{array}[]{ccc||ccc}\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{tu}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle(=A)\lx@proof@logical@and\vdash
t\mathrel{\mathop{\mathchar 58\relax}}T\rightarrow
A\vdash&\rightarrow_{\bullet 1}&\vdash tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{t}}\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle\vdash&\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\lambda
x.t}}\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle\vdash
t\mathrel{\mathop{\mathchar
58\relax}}A(=\mathbb{A}\langle\star\rangle)&\rightarrow_{\bullet
2}&\vdash\lambda x.t\mathrel{\mathop{\mathchar 58\relax}}T\rightarrow
A\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{t}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle\\\\[8.0pt]
\hline\cr&&&\\\ \vdash tu\mathrel{\mathop{\mathchar
58\relax}}A(=\mathbb{A}\langle\star\rangle)\lx@proof@logical@and\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{t}}\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle\vdash\par&\rightarrow_{\bullet
3}&\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{tu}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle\lx@proof@logical@and\vdash
t\mathrel{\mathop{\mathchar 58\relax}}T\rightarrow A\vdash&\vdash\lambda
x.t\mathrel{\mathop{\mathchar 58\relax}}T\rightarrow
A\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{t}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle(=A)&\rightarrow_{\bullet
4}&\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\lambda
x.t}}\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle\vdash
t\mathrel{\mathop{\mathchar 58\relax}}A\\\\[8.0pt] \hline\cr&&&\\\
\vdash\lambda x.C\langle x\rangle\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle A_{i}\rangle\rightarrow
A^{\prime}\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{x}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle_{i}(=A_{i})&\rightarrow_{{\mathsf{var}}}&\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\lambda
x.C\langle x\rangle}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle_{i}\rangle\rightarrow
A^{\prime}\vdash x\mathrel{\mathop{\mathchar
58\relax}}A_{i}&\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\lambda
x.C\langle x\rangle}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle_{i}\rangle\rightarrow
A^{\prime}\vdash x\mathrel{\mathop{\mathchar
58\relax}}A_{i}(=\mathbb{A}\langle\star\rangle_{i})&\rightarrow_{\mathsf{bt}2}&\vdash\lambda
x.C\langle x\rangle\mathrel{\mathop{\mathchar 58\relax}}\mathbb{L}\langle
A_{i}\rangle\rightarrow
A^{\prime}\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{x}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle_{i}\\\\[8.0pt]
\hline\cr\\\ \end{array}$
---
$\begin{array}[]{ccccccc }\vdash tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{t}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle_{i}\rangle\rightarrow
A\vdash u\mathrel{\mathop{\mathchar
58\relax}}T(=\mathbb{L}\langle\mathbb{A}\langle\star\rangle_{i})\rangle\ldots\
\vdash u\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star\rangle_{i}\
\ldots&\rightarrow_{\mathsf{arg}}&\vdash tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\vdash t\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow A\vdash u\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle\mathbb{A}\langle\star\rangle_{i}\rangle\ldots\
\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{u}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle_{i}\
\ldots\par\\\\[8.0pt] \hline\cr\\\ \vdash tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\vdash t\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow A\vdash u\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle\mathbb{A}\langle\star\rangle_{i}\rangle(=T)\ldots\
\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{u}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}\rangle_{i}\
\ldots&\rightarrow_{\mathsf{bt}1}&\vdash tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\vdash{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{t}}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{L}\langle\mathbb{A}\langle\star_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}\rangle_{i}\rangle\rightarrow
A\vdash u\mathrel{\mathop{\mathchar 58\relax}}T\ldots\ \vdash
u\mathrel{\mathop{\mathchar 58\relax}}\mathbb{A}\langle\star\rangle_{i}\
\ldots\end{array}$
Figure 3: The transitions of the Tree IAM (TIAM).

##### The TIAM

On the one hand, the TIAM is simpler than the $\lambda$IAM because it has no
logs, on the other hand, it is more technical to define because tree type
derivations are less easily manipulated than $\lambda$-terms. The underlying
idea however is simple. The TIAM moves over a fixed type derivation
$\pi\;\triangleright\vdash t\mathrel{\mathop{\mathchar 58\relax}}\star$, to be
thought as the code, following the occurrence of $\star$ in the final judgment
through $\pi$, according to the transitions in Fig. 3. We shall now explain
every involved concept.

The position of the machine is given by an occurrence of a type judgment444A
judgment may occur repeatedly in a derivation, which is why we talk about
_occurrences_ of judgments. To avoid too many technicalities, however, we
usually just write the judgment, leaving implicit that we refer to an
occurrence of that judgment. $J$ of $\pi$. As the $\lambda$IAM, the TIAM has
two possible directions, noted
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}$
and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}$555Type
derivations are upside-down wrt to the term structure, then direction
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\downarrow}}$
of the $\lambda$IAM becomes here
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\uparrow}}$
is
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}$..
In direction
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}$
the machine looks at the rule above the focused judgment, in direction
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}$
at the rule below. The only “data structure”—encoding the tape of the
$\lambda$IAM, as we shall explain—is a type context $\mathbb{A}$ isolating an
occurrence of $\star$ in the type $A$ of the focused judgment (occurrence)
$\Gamma\vdash u\mathrel{\mathop{\mathchar 58\relax}}A$, defined as follows
(careful to not confuse type contexts $\mathbb{A}$ and $\mathbb{T}$ with type
environments $\Gamma$):

<EMAIL_ADDRESS>ctxs}\hskip
11.38092pt&\mathbb{A}\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=\langle\cdot\rangle\mathrel{\big{|}}T\rightarrow\mathbb{A}\mathrel{\big{|}}\mathbb{T}\rightarrow
A\\\\[3.0pt] \textsc{Tree ctxs}\hskip
11.38092pt&\mathbb{T}\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar 58\relax}}=[G_{1},\hbox
to6.00006pt{.\hss.},\mathbb{G},\hbox to6.00006pt{.\hss.},G_{n}]\\\\[3.0pt]
\textsc{Type ctxs}\hskip 11.38092pt&\mathbb{G}\mathrel{\mathop{\mathchar
58\relax}}\mathrel{\mathop{\mathchar
58\relax}}=\mathbb{A}\mathrel{\big{|}}\mathbb{T}\end{array}$

Summing up, a state $s$ is a quadruple $(\pi,J,\mathbb{A},d)$. If $J$ is in
the form $\Gamma\vdash u\mathrel{\mathop{\mathchar 58\relax}}A$, we often
write $s$ as $\vdash u\mathrel{\mathop{\mathchar
58\relax}}\mathbb{A}\langle\star_{d}\rangle$, where
$\mathbb{A}\langle\star\rangle=A$. We shall see that type environments play no
role.

##### Intuitions about Positions (and Logs)

The intuition is that the active position $(t,C_{n})$ of a $\lambda$IAM state
corresponds to the judgment occurrence $J$ in the TIAM, or, more precisely, to
its position in the type derivation $\pi$. The sub-term $t$ is exactly the
term typed by $J$. The context $C_{n}$ is exactly the context giving the term
$C_{n}\langle t\rangle$ typed by the final judgment of $\pi$. The level $n$ of
the context $C_{n}$ of the active position counts the number of arguments in
which the hole of $C_{n}$ is contained. On the type derivation, each such
argument is associated to a T-@ rule having the current judgment $J$ in its
right sub-derivation. Last, note that in the $\lambda$IAM the current log
$L_{n}$ has length equal to $n$. We shall see in the next section that one can
recover the log $L_{n}$ applying an extraction process to the T-@ rules found
descending from $J$ towards the final judgment.

${\footnotesize\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}3\mathsf{X}}}(\lambda
z.z)((\lambda x.xx)(\lambda y.y))\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{1}}}\lx@proof@logical@and\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}}}\lambda
z.z\mathrel{\mathop{\mathchar
58\relax}}[\star_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{4}}}]\rightarrow\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{2}}}z\mathrel{\mathop{\mathchar
58\relax}}[\star]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}0}}z\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{3}}}\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}3\mathsf{X}}}(\lambda
x.xx)(\lambda y.y)\mathrel{\mathop{\mathchar
58\relax}}[\star]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}2\mathsf{X}}}(\lambda
x.xx)(\lambda y.y)\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{5}}}}\lx@proof@logical@and\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}2\mathsf{X}}}\lambda
x.{xx}\mathrel{\mathop{\mathchar
58\relax}}[[\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{13}}}}]\rightarrow\star_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{9}}}},[\star_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{16}}}}]]\rightarrow\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{6}}}}x\mathrel{\mathop{\mathchar
58\relax}}[[\star]\rightarrow\star,[\star]]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}}}xx\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{7}}}}\lx@proof@logical@and
x\mathrel{\mathop{\mathchar
58\relax}}[[\star]\rightarrow\star]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}}}x\mathrel{\mathop{\mathchar
58\relax}}[\star_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{14}}}}]\rightarrow\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{8}}}}x\mathrel{\mathop{\mathchar
58\relax}}[[\star]]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}}}x\mathrel{\mathop{\mathchar
58\relax}}[\star]x\mathrel{\mathop{\mathchar
58\relax}}[\star]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}0}}x\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{15}}}}\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}2\mathsf{X}}}\lambda
y.y\mathrel{\mathop{\mathchar
58\relax}}[[\star]\rightarrow\star,[\star]]\lx@proof@logical@and\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}}}\lambda
y.y\mathrel{\mathop{\mathchar
58\relax}}[\star_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{12}}}}]\rightarrow\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{10}}}}y\mathrel{\mathop{\mathchar
58\relax}}[\star]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}0}}y\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{11}}}}\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}}}\lambda
y.y\mathrel{\mathop{\mathchar
58\relax}}[\star]\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}0}}\lambda
y.y\mathrel{\mathop{\mathchar
58\relax}}\star_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{17}}}}}$
Figure 4: An example of TIAM execution.

##### Transitions

The TIAM starts on the final judgment of $\pi$, with empty type context
$\mathbb{A}=\langle\cdot\rangle$ and direction
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}$.
It moves from judgment to judgment, following occurrences of $\star$ around
$\pi$. To specify the transitions, we use the leaf contexts defined in the
previous section.

The transitions are in Fig. 3, their union is noted
$\rightarrow_{\textsc{TIAM}}$. We now explain them one by one—the transitions
have the labels of $\lambda$IAM transitions, because they correspond to each
other, as we shall show.

Let’s start with the simplest, $\rightarrow_{\bullet 2}$. The state focuses on
the conclusion judgment $J$ of a $\textsc{T-}\lambda$ rule with direction
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\uparrow}}$.
The eventual type environment $\Gamma$ is omitted because the transition does
not depend on it—none of the transitions does, so type environments are
omitted from all transitions. The judgment assigns type $T\rightarrow A$ to
$\lambda x.t$, and the type context is $T\rightarrow\mathbb{A}$, that is, it
selects an occurrence of $\star$ in the target type
$A=\mathbb{A}\langle\star\rangle$. The transition then simply moves to the
judgment above, stripping down the type context to $\mathbb{A}$, and keeping
the same direction. Transition $\bullet 4$ does the opposite move, in
direction
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\downarrow}}$,
and transitions $\bullet 1$ and $\bullet 3$ behave similarly on T-@ rules: the
extra premise $\vdash$ simply denotes the right premise of the T-@ rule that
is left unspecified since not relevant to the transition.

Transitions $\rightarrow_{\mathsf{arg}}$: the focus is on the left premise of
a T-@ rule, of type $T\rightarrow A^{\prime}$ isolating $\star$ inside the
$i$-th leaf $A_{i}$ of the tree type $T$. The transition then moves the state
of the TIAM to the $i$-th leaf of the tree of T-many rules on the right
premise, changing direction. Transition $\rightarrow_{\mathsf{bt}1}$ does the
opposite move.

Transitions $\rightarrow_{{\mathsf{var}}}$ and $\rightarrow_{\mathsf{bt}2}$
are based on the axiom sequences property of Lemma IV.1. Consider a
$\textsc{T-}\lambda$ rule occurrence whose right-hand type of the conclusion
is $T\rightarrow A^{\prime}$. The premise has shape
$\Gamma,x\mathrel{\mathop{\mathchar 58\relax}}T\vdash
t\mathrel{\mathop{\mathchar 58\relax}}A^{\prime}$, and by the lemma there is a
bijection between the leaves in $T$ and the axioms on $x$, respecting the
order in $T^{\ell}$. The left side of $\rightarrow_{\mathsf{bt}2}$ focuses on
the $i$-th leaf $A_{i}$ of $T$ and the TIAM moves to the judgment of the axiom
corresponding to that type, which is exactly the $i$-th from left to right
seeing the derivation as a tree where the children of nodes are ordered as in
the typing rules. Transition $\rightarrow_{{\mathsf{var}}}$ does the opposite
move, which can always happen because the code is the type derivation of a
closed term.

The only typing rule not inducing a transition is
$\textsc{T-}\lambda_{\star}$. Accordingly, when the TIAM reaches a
$\textsc{T-}\lambda_{\star}$ rule, it is in a final state. Exactly as the
$\lambda$IAM, the TIAM is bi-deterministic.

######  Proposition V.1.

The TIAM is bi-deterministic for each type derivation
$\pi\;\triangleright\vdash t\mathrel{\mathop{\mathchar 58\relax}}\star$.

##### An example

In Fig. 4 we present the very same example analyzed in Section III. We have
reported its type derivation, with the occurrences of $\star$ on the right of
$\vdash$ annotated with increasing integers and a direction. The occurrence of
$\star$ marked with 1 represents the first state, and so on. One can
immediately notice that every occurrence of $\star$ is visited exactly once.
Moreover, the sequence of the visited subterms is the same as the one obtained
in the example of Section III. Please note that judgments are decorated with
weights (such as $\mathsf{X}$), which shall be introduced only in Sect. VII,
in order to later provide an example of decoration—they can be safely ignored
for now.

##  VI The $\lambda$IAM and TIAM Bisimulation

The aim of this section is to explain the strong bisimulation between the TIAM
and the $\lambda$IAM, that is essentially the same between the SIAM and the
$\lambda$IAM studied in [6]. A striking point of the TIAM is that it does not
have the log nor the tape. They are encoded in the position of the judgment
occurrence $J$ and in the type context $\mathbb{A}$ of its states, as we shall
show.

##### Relating Logs and Tapes with Typed Positions

In the $\lambda$IAM, the log $L=l_{1}{\cdot}\ldots{\cdot}l_{n}$ has a logged
position for every argument $u_{1},\ldots,u_{n}$ in which the position of the
current state is contained. The argument $u_{i}$ is the answer to the query of
an argument for the variable in the logged position $l_{i}$. The TIAM does not
keep a trace of the variables for which it completed a query, but the answers
to those (forgotten) queries are simply given by the sub-derivations for
$u_{1},\ldots,u_{n}$ in which the current judgment occurrence $J$ is
contained—the way in which $l_{k}$ identifies a copy of $u_{k}$ in the
$\lambda$IAM corresponds on the type derivation $\pi$ to the index $i$ of the
leaf (in the tree of sub-derivations) typing $u_{k}$ in which $J$ is located.
Note that the $\lambda$IAM manipulates the log only via transitions
$\rightarrow_{\mathsf{arg}}$ and $\rightarrow_{\mathsf{bt}1}$, that on the
TIAM correspond exactly to entering/exiting derivations for arguments. The
tape, instead, contains logged positions for which the $\lambda$IAM either has
not yet found the associated argument, or it is backtracking to. Note that the
$\lambda$IAM puts logged positions on the tape via transitions
$\rightarrow_{{\mathsf{var}}}$ and $\rightarrow_{\mathsf{bt}1}$, and removes
them using $\rightarrow_{\mathsf{arg}}$ and $\rightarrow_{\mathsf{bt}2}$. By
looking at Fig. 3, it is clear that there is a logged position on the
$\lambda$IAM tape for every type sequence of the flattening of $T$ in which it
lies the hole $\langle\cdot\rangle$ of the current type context $\mathbb{A}$
of the TIAM.

##### Extracting $\lambda$IAM States

These ideas are used to extract from every TIAM state $s$ a $\lambda$IAM state
$\mathsf{ext}(s)$ in a quite technical way. In particular, the extraction
process retrieves a log $L_{\mathsf{ext}}(s)$ from the judgement $J$ of $s$
and a tape $T_{\mathsf{ext}}(s)$ from the type context $\mathbb{A}$ of $s$,
using a sophisticated _T-exhaustible invariant_ of the TIAM to retrieve the
exact shape of the logged positions in $L_{\mathsf{ext}}(s)$ and
$T_{\mathsf{ext}}(s)$.

Let us give a high-level description of how extraction works. The invariant is
based on the pairing of every TIAM state $s$ with a set of _test states_ ,
some coming from the judgment $J$ of $s$, called _judgment tests_ , and some
coming from the type context $\mathbb{A}$, called _type (context) tests_. The
invariant guarantees a certain recursive property of each test state. The
extraction process uses this property to extract a logged position
$l_{{s^{\prime}}}$ from each test state ${s^{\prime}}$ of $s$.

Given a TIAM state $s=(\pi,J,\mathbb{A},d)$, its judgment tests are associated
to the T-@ rules having $J$ in their right sub-derivation. Their extractions
give logged positions $l_{1}\cdot\hbox to6.00006pt{.\hss.}\cdot l_{n}$ forming
the extracted log $L_{\mathsf{ext}}(s)$, following the correspondence
described above.

Type tests are associated to the leaf contexts surrounding the hole of
$\mathbb{A}$. The extraction of the tape $T_{\mathsf{ext}}(s)$ from
$\mathbb{A}$ is done according to the following schema:

$\begin{array}[]{lcl}T_{\mathsf{ext}}(\langle\cdot\rangle)&\mathrel{\mathop{\mathchar
58\relax}}=&\epsilon\\\
T_{\mathsf{ext}}(T\rightarrow\mathbb{A})&\mathrel{\mathop{\mathchar
58\relax}}=&\bullet\cdot T_{\mathsf{ext}}(\mathbb{A})\\\
T_{\mathsf{ext}}(\mathbb{L}\langle\mathbb{A}\rangle\rightarrow
A^{\prime})&\mathrel{\mathop{\mathchar
58\relax}}=&l_{\mathsf{ext}}(s_{\mathbb{L}})\cdot
T_{\mathsf{ext}}(\mathbb{A})\end{array}$

where $s_{\mathbb{L}}$ is the state test associated to the leaf context
$\mathbb{L}$.

For lack of space, and because this is essentially identical to what is done
in [6] for the SIAM, the technical development is in [TRPOPL2021]Appendix VI.
The extraction process induces a relation
$s\simeq_{\mathsf{ext}}\mathsf{ext}(s)$ that is easily proved to be a strong
bisimulation between the TIAM and the $\lambda$IAM.

######  Proposition VI.1 (TIAM and $\lambda$IAM bisimulation).

Let $t$ a closed term and $\pi\;\triangleright\vdash
t\mathrel{\mathop{\mathchar 58\relax}}\star$ a tree type derivation. Then
$\simeq_{\mathsf{ext}}$ is a strong bisimulation between TIAM states on $\pi$
and $\lambda$IAM states on $t$. Moreover, if
$s_{\pi}\simeq_{\mathsf{ext}}s_{\lambda}$ then $s_{\pi}$ is TIAM reachable if
and only if $s_{\lambda}$ is $\lambda$IAM reachable.

The _moreover_ part of the above statement hints at a bijection between _all_
the states in $\pi$ and reachable $\lambda$IAM states. However, there still
could be the possibility that some of the states in $\pi$ are not reachable.
This is actually _not_ the case, and the technical development is in the
Appendix.

######  Proposition VI.2.

Let $t$ a closed term and $\pi\;\triangleright\vdash
t\mathrel{\mathop{\mathchar 58\relax}}\star$ a tree type derivation. Then
every state of $\pi$ is reached exactly once.

$\small\begin{array}[]{c@{\hspace{1cm}}c@{\hspace{1cm}}c}x\mathrel{\mathop{\mathchar
58\relax}}[A]\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathinner{\\!\left\lVert
A\right\rVert}}}}{{\vdash}}x\mathrel{\mathop{\mathchar 58\relax}}A\hfil\hskip
28.45274pt&\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\max\\{w,\,\mathinner{\\!\left\lVert
T\rightarrow A\right\rVert}\\}}}}{{\vdash}}\lambda
x.t\mathrel{\mathop{\mathchar 58\relax}}T\rightarrow
A\Gamma,x\mathrel{\mathop{\mathchar
58\relax}}T\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}A\hfil\hskip
28.45274pt&\Gamma\uplus\Delta\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\max\\{w,v\\}}}}{{\vdash}}tu\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}T\rightarrow
A\Delta\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}v}}}{{\vdash}}u\mathrel{\mathop{\mathchar
58\relax}}T\\\\[8.0pt]
\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}0}}}{{\vdash}}\lambda
x.t\mathrel{\mathop{\mathchar 58\relax}}\star\hfil\hskip
28.45274pt&[\uplus_{i=1}^{n}\Gamma_{i}]\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\mathsf{X}+\max_{i}\mathinner{\left\\{w_{i}\right\\}}}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}[G_{1},\hbox
to5.40005pt{.\hss.},G_{n}]\lx@proof@logical@and\Gamma_{i}\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w_{i}}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}G_{i}1\leq i\leq n\hfil\hskip
28.45274pt&\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}0}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}[\cdot]\end{array}$ Figure 5: The tree type system with weights.

##  VII Measuring the Space of Interactions

This section contains the main contribution of the article: it gives a way of
measuring the space consumed by the complete $\lambda$IAM run on the term $t$
via a quantitative analysis of the tree type derivation for $t$. We proceed in
two steps.

  1. 1.

_The space of single extracted states_ : given a TIAM state
$s=(\pi,J,\mathbb{A},d)$, we show how to measure the space of the extracted
$\lambda$IAM state $\mathsf{ext}(s)$ from $\pi$, $J$, and $\mathbb{A}$.

  2. 2.

_The space of the whole execution_ : we refine tree type derivations adding
_weights_ on judgments, and show that the weight of the final judgment
coincides with the maximum space consumption over all extracted states, that
is, along the whole $\lambda$IAM execution.

##### The Undetermined Pointers Size $\mathsf{X}$

A technical point common to both parts is that the quantitative study of tree
types derivations is relative to an undetermined value $\mathsf{X}$. The
reason for using $\mathsf{X}$ is that our space analyses have both local and
global components. Locally, we count how many occurrences of $\bullet$ and how
many logged positions are involved in a state (for step 1) or in all states in
and above that judgment (for step 2). The global component comes from the fact
that all logged positions of the $\lambda$IAM, independently of where they
arise, are implemented via pointers to the _global_ code. Essentially,
$\mathsf{X}$ is meant to be replaced, at the very end of both analyses, by the
size of pointers to the $\lambda$IAM global code, that is, by $\log|t|$, where
$t$ is the term typed in the final judgment of the type derivation $\pi$.
Therefore, locally our measures shall include $\mathsf{X}$, which shall
substituted at the end with $\log|t|$.

###  VII-A The Space of Single Extracted States

##### Trees and the Size of Extracted Logged Positions

Basically, given a TIAM state $s=(\pi,J,\mathbb{A},d)$, the size of logged
positions in $\mathsf{ext}(s)$ is obtained by counting $\mathsf{X}$ for

  * •

_Extracted tape_ : every sequence constructor $[\cdot]$ surrounding the hole
$\langle\cdot\rangle$ in $\mathbb{A}$;

  * •

_Extracted log_ : every T-many rule on the path from $J$ to the final judgment
of $\pi$.

Clearly, it is the newly introduced tree structure that allows to measure the
size of extracted logged positions, as expected.

First, we define a size of type contexts meant to measure the size of the
extracted tapes.

######  Definition VII.1 (Branch size of type contexts/extracted tapes).

Let $s=(\pi,J,\mathbb{A},d)$ be a TIAM state. The branch size
$|\cdot|_{{\mathsf{b}}}$ for type contexts is defined as follows:

<EMAIL_ADDRESS>rcl}|\langle\cdot\rangle|_{{\mathsf{b}}}&\mathrel{\mathop{\mathchar
58\relax}}=&0\hfil\hskip
14.22636pt&|T\rightarrow\mathbb{A}|_{{\mathsf{b}}}&\mathrel{\mathop{\mathchar
58\relax}}=&1+|\mathbb{A}|_{{\mathsf{b}}}\\\\[2.0pt] |\mathbb{T}\rightarrow
A|_{{\mathsf{b}}}&\mathrel{\mathop{\mathchar
58\relax}}=&|\mathbb{T}|_{{\mathsf{b}}}\hfil\hskip 14.22636pt&|[G_{1},\hbox
to6.00006pt{.\hss.},\mathbb{G},\hbox
to6.00006pt{.\hss.},G_{n}]|_{{\mathsf{b}}}&\mathrel{\mathop{\mathchar
58\relax}}=&\mathsf{X}+|\mathbb{G}|_{{\mathsf{b}}}\end{array}$

Let us interpret the branch size with respect to the tape extraction schema of
the previous section. The $+1$ in the clause for $T\rightarrow\mathbb{A}$ is
there to count $\bullet$. The clause for sequences instead gives
$|\mathbb{L}|=n\cdot\mathsf{X}$ if the hole has height $n$ in the leaf context
$\mathbb{L}$ seen as a tree—whence the name _branch size_.

Then, we define a branch size for judgments, meant to measure the size of
extracted logs, and a branch size for states.

######  Definition VII.2.

Let $s=(\pi,J,\mathbb{A},d)$ be a TIAM state.

  * •

_Branch size of judgments/extracted logs_ : let $n$ be the number of T-many
rules encountered descending from $J$ to the root of $\pi$. Then
$|J|_{{\mathsf{b}}}\mathrel{\mathop{\mathchar 58\relax}}=n\cdot\mathsf{X}$.

  * •

_Branch size of TIAM states_ : $|s|_{{\mathsf{b}}}\mathrel{\mathop{\mathchar
58\relax}}=|\mathbb{A}|_{{\mathsf{b}}}+|J|_{{\mathsf{b}}}$.

We prove that the defined branch sizes do correspond to their intended
meanings, that is, the branch sizes of extracted logs and tapes, showing that
the size of TIAM states captures the space size of the extracted $\lambda$IAM
state.

######  Proposition VII.3 (Space of Single Extracted States).

Let $s=(\pi,J,\mathbb{A},d)$ be a reachable TIAM state. Then
$|\mathbb{A}|_{{\mathsf{b}}}=|T_{\mathsf{ext}}(s)|_{\mathsf{sp}}$ and
$|J|_{{\mathsf{b}}}=|L_{\mathsf{ext}}(s)|_{\mathsf{sp}}$, and thus
$|s|_{{\mathsf{b}}}=|\mathsf{ext}(s)|_{\mathsf{sp}}$. Moreover,

  1. 1.

if $L_{\mathsf{ext}}(s)=l_{1}\hbox to6.00006pt{.\hss.}l_{n}$, and let $h_{i}$
be the number of T-many rules of the $i^{th}$ T-many rule tree found
descending from $J$ to the root of $\pi$, then $|l_{i}|_{\mathsf{sp}}=h_{i}$;

  2. 2.

for each extracted tape position $l$, i.e. for each $\mathbb{G}$ such that
$\mathbb{A}=\mathbb{G}\langle\mathbb{L}\langle\mathbb{A}^{\prime}\langle\star\rangle\rangle\rightarrow
A\rangle$, then $|l|_{\mathsf{sp}}=|\mathbb{L}|{\cdot}\mathsf{X}$.

##### The Need for Tree Types

A subtle point is that the tree structure of types is not needed in order to
define the extraction process—indeed, $\lambda$IAM states are extracted from
_sequence_ type derivations in [6]. Extraction is an indirect process—a sort
of logical relation—whose functioning is guaranteed by an invariant (the
T-exhaustible invariant in the Appendix). The process does not describe
explicitly the shape of the extracted logged positions, it only guarantees
that adequate logged positions exist. Without tree types, the structure of
multi types derivations somehow encodes enough information to retrieve
$\mathsf{ext}(s)$, but how many logged positions are involved can be
discovered only by unfolding the whole extraction process, the information is
not encoded into the types themselves.

There is a further subtlety. Tree types trace the _number_ of pointers as
precisely described by the _moreover_ part of Prop. VII.3, but do not describe
the internal structure of logged positions. Given a TIAM state $s$, we can
easily know the length of $L_{\mathsf{ext}}(s)$ and $T_{\mathsf{ext}}(s)$, and
know the number of pointers to implement each logged position $l$ in them,
which is enough to measure space. The internal structure of $l$, however,
cannot be read from tree types. Again, it is determined only by unfolding the
whole extraction process.

###  VII-B The Space of the Whole Execution

##### Type Weights

To obtain the space cost of the whole execution we endow tree types
derivations with _weights_ 666We introduce a different word for measuring
space of the whole execution, because judgments are measured in two different
ways: the _branch size_ measures what is below the judgment, and corresponds
to the size of the extracted log for a state, the _weight_ measures what is
above a judgment, and gives the maximum space over all states in the rooted
sub-derivation.. In turn, we first have to define a notion of weight for
types. The intuition is that we are taking the max of the branch size for type
contexts $\mathbb{G}$ used above, over all the ways of writing a type $G$ as
$\mathbb{G}\langle\star\rangle$, as confirmed by the associated lemma.

<EMAIL_ADDRESS>c}\mathinner{\\!\left\lVert\star\right\rVert}\mathrel{\mathop{\mathchar
58\relax}}=0\hfil\hskip 25.6073pt&\mathinner{\\!\left\lVert T\rightarrow
A\right\rVert}\mathrel{\mathop{\mathchar
58\relax}}=\max\\{\mathinner{\\!\left\lVert
T\right\rVert},\mathinner{\\!\left\lVert A\right\rVert}+1\\}\\\\[7.0pt]
\lx@intercol\hfil\mathinner{\\!\left\lVert[G_{1},\hbox
to6.00006pt{.\hss.},G_{n}]\right\rVert}\mathrel{\mathop{\mathchar
58\relax}}=\mathsf{X}+\max_{i}\\{\mathinner{\\!\left\lVert
G_{i}\right\rVert}\\}\hfil\lx@intercol\end{array}$

######  Lemma VII.4.

Let $G$ be a type. Then $\mathinner{\\!\left\lVert
G\right\rVert}=\max_{\mathbb{G}|G=\mathbb{G}\langle\star\rangle}|\mathbb{G}|_{{\mathsf{b}}}$.

Note that, via the space of single extracted states (Prop. VII.3), the
previous lemma states that the size of $G$ is the maximum space of all the
tapes extracted from TIAM states over a same judgment $\Gamma\vdash
t\mathrel{\mathop{\mathchar 58\relax}}G$.

##### Judgements and Derivations Weights

Weights are extended to judgments in Fig. 5, and the weight of a derivation is
the weight of its final judgment. The idea is that the weight $w$ of a
weighted judgment
$J=\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}G$ gives the maximum space of all the states over $J$
and—crucially—above $J$.

Now, we prove that the weight of a judgment $J$ is greater than the maximum
size of the tape of the states in its derivation.

######  Lemma VII.5 (Judgment weights bound extracted tapes).

Let $\pi\mathrel{\mathop{\mathchar
58\relax}}\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}G$ be a weighted derivation and $\mathcal{J}$ be the set of all the
judgments occurring in $\pi$. Then $w\geq\max_{\Delta\vdash
u\mathrel{\mathop{\mathchar
58\relax}}G^{\prime}\in\mathcal{J}}\mathinner{\\!\left\lVert
G^{\prime}\right\rVert}$.

Judgement weights actually take also logs into account.

######  Lemma VII.6 (Weights bound also extracted logs).

Let
$\pi\;\triangleright\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}G$ be a weighted derivation. Then $w\geq v+|J|_{{\mathsf{b}}}$ for
every weighted judgment $J$
$\vdash^{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}v}}$
in $\pi$.

We then obtain that the weight of a derivation $\pi$ for $t$ bounds the space
used by the TIAM execution of $\pi$, and so by the $\lambda$IAM execution of
$t$.

######  Theorem VII.7 ($\lambda$IAM space bounds).

Let
$\pi\;\triangleright\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}\star$ be a weighted tree types derivation. Then
$|\mathsf{ext}(s)|_{\mathsf{sp}}\leq w$ for every
$s\in{\mathsf{states}}(\pi)$.

Last, we show that weights provide _exact_ bounds, as there always is a
witness state using as much space as in the weight.

######  Proposition VII.8 (Weight witness).

Let
$\pi\;\triangleright\Gamma\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}G$ be a weighted derivation and $G\neq[\cdot]$. Then there exists a
TIAM state $s$ over $\pi$ such that $w=|s|_{{\mathsf{b}}}$.

We can then conclude our complexity analysis.

######  Corollary VII.9 ($\lambda$IAM exact bound via tree types derivations).

Let
$\pi\;\triangleright\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}w}}}{{\vdash}}t\mathrel{\mathop{\mathchar
58\relax}}\star$ be a tree types derivation and $\rho$ the complete
$\lambda$IAM run on $t$. Then $|\rho|_{\mathtt{s}}=w$.

Now, the reader can fully understand and appreciate the weights in the
derivation of Fig. 4. Please note that we have considered
$\max\\{1,\mathsf{X}\\}=\mathsf{X}$ when assigning the weights.

##  VIII On the $\lambda$IAM Space (In)Efficiency

##### Tree Density

As we have proved in the last section, the space consumed by a $\lambda$IAM
run ultimately depends on the level of nesting of tree types. Let us be
slightly more precise. When we are dealing with multi types, the argument $u$
of an application $tu$ has to be typed with a multiset, say
$M\mathrel{\mathop{\mathchar 58\relax}}=[\star,\hbox
to6.00006pt{.\hss.},\star]$ where $|M|=n$ and $n$ is the number of times that
$u$ shall be copied. In our type system, $M$ can be represented as a tree $T$,
capturing the space needed for evaluating the copies of $u$, in several ways.
In the tree type derivation for $tu$ only one of these representations is
used, and depends on the type of $t$. The important point is that different
representations lead to very different space consumptions. The ideal case is
the flat representation $T_{f}\mathrel{\mathop{\mathchar
58\relax}}=[\star,\hbox to6.00006pt{.\hss.},\star]$, for which
$\mathinner{\\!\left\lVert T_{f}\right\rVert}=\mathsf{X}$. Another good case
is given by a full binary tree $T_{b}$, or, more generally, by a tree $T_{d}$
whose height is logarithmic in $n$, so that $\mathinner{\\!\left\lVert
T_{d}\right\rVert}=\log n\cdot\mathsf{X}$. Let us deem this case _dense_. A
bad case is given by linearly shaped trees such as
$T_{l}\mathrel{\mathop{\mathchar 58\relax}}=T_{n}$, where
$T_{0}\mathrel{\mathop{\mathchar 58\relax}}=[\star]$ and
$T_{n+1}\mathrel{\mathop{\mathchar 58\relax}}=[\star,T_{n}]$, for which
$\mathinner{\\!\left\lVert
T_{s}\right\rVert}=(n+1)\cdot\mathsf{X}\geq\mathinner{\\!\left\lVert
T_{d}\right\rVert}$. We call _sparse_ a tree with $n$ leaves and height $n$
like $T_{l}$. Not that there can even be worse, as in general a tree can have
an arbitrary number of internal nodes, for instance a multi set $[\star]$ can
be represented as a tree also as $[[[[\star]]]]$—again, it depends on the type
of $t$. Intuitively, if a term can be typed with flat or dense trees, the
$\lambda$IAM evaluates it space _efficiently_ , while in the case of sparse
trees (or worse) the evaluation is space _inefficient_.

##### Fixed-Points Are Sparse

As is well known, the $\lambda$-calculus is a universal (or Turing complete)
model of computation. The fundamental ingredient that allows one to achieve
universality is the presence of fixed-point combinators. These combinators
allow for an encoding of general recursion, as needed when simulating, e.g.,
partial recursive functions or Turing machines. In particular, the fixed point
combinator can capture unbounded iteration (i.e. while loops) or tail-
recursion, as needed e.g. in the encoding of minimization from Kleene algebra.

As an example, consider how the encoding of a Turing machine $M$ may look
like, in the $\lambda$-calculus. Let $t_{M}$ be the encoding of $M$’s
transition function (which is typically very simple if states and tapes are
encoded using, e.g., Scott’s numerals [36]). Then, the (recursively defined)
function that iterates $t_{M}$, thus capturing the overall behavior of $M$,
can be written as follows:

$\textsf{iter}=\underbrace{(\lambda f.{\lambda s.\texttt{if}\text{ }s\text{ is
final }\texttt{then}\text{ halt }\texttt{else}\text{
}f(t_{M}s)})}_{\textsf{iteraux}}\textsf{iter}$

How can we build a solution to this equation in the form of a $\lambda$-term?
Apart from an encoding of the conditional operator, itself very easy to write,
we need a fixed-point combinator $\Theta$, such as Turing’s:

$\Theta\mathrel{\mathop{\mathchar
58\relax}}=\theta\theta\qquad\qquad\text{where
}\quad\theta\mathrel{\mathop{\mathchar 58\relax}}=\lambda x.{\lambda
y.{y(xxy)}}$

We highlight that $\Theta t\rightarrow_{wh}(\lambda y.{y(\Theta
y)})t\rightarrow_{wh}t(\Theta t)$. Then, we can set, as expected,
$\textsf{iter}\mathrel{\mathop{\mathchar 58\relax}}=\Theta\textsf{iteraux}$.

Let us analyze how $\Theta$ implements recursion, independently on what the
argument of $\Theta$ is. Please note that during the reduction of $\Theta t$,
the variable $y$ is substituted for the term $t$, which after two
$\beta$-steps appears twice, once in head position (call this occurrence
$t_{0}$), and once applied to $\Theta$. The latter copy of $t$, together with
$\Theta$, can be copied potentially many times, depending on how $t_{0}$ uses
its argument. Some of these copies, say $m$, will eventually appear in head
position, and the same process starts again. In other words, the copies of $t$
that the combinator $\Theta$ will eventually create can be organized in a
tree, see Figure 6(a). This is a faithful description of how recursion
unfolds, independently on how $t$ uses its argument.

If $t=\textsf{iteraux}$, however, the situation is much simpler: $t$ uses its
argument at most once, and the complicated tree in Figure 6(a) becomes the one
in Figure 6(b). Every copy $t_{01^{n}}$ of $t$ either brings $\Theta
t_{1^{n+1}}$ in head position (without copying it), or discards it, depending
on whether the current state is final or not. Saying it another way, the
height of the tree in Figure 6(b) is nothing more than the number of reduction
steps the Turing machine $M$ performs.

(a) (b)

Figure 6: Different ways $\Theta$ can copy its argument.

In order to understand if the $\lambda$IAM could be reasonable in space, i.e.
if it can simulate Turing machines with a constant overhead in space, we apply
our technique by giving $\Theta$ a suitable type (schema)
$\mathbb{F}_{n}^{{\overline{A}}}$, depending on a list of types
${\overline{A}}\mathrel{\mathop{\mathchar 58\relax}}=A_{n},\hbox
to6.00006pt{.\hss.},A_{0}$ and on $n$, which is the number of times the fixed
point is unfolded. In particular, $\mathbb{F}_{n}^{{\overline{A}}}$ turns out
to be _sparse_. The details of the technical development can be found in the
Appendix.

######  Proposition VIII.1.

For each $n\geq 0$, and for each list of types ${\overline{A}}$ such that
$|{\overline{A}}|\geq n+1$,
$\stackrel{{\scriptstyle{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\geq(2n+1)\mathsf{X}}}}{{\vdash}}\Theta\mathrel{\mathop{\mathchar
58\relax}}\mathbb{F}_{n}^{{\overline{A}}}$.

In particular, $\Theta\mathrel{\mathop{\mathchar
58\relax}}\mathbb{F}_{n}^{{\overline{A}}}$ when $\Theta$ is unfolded $n$ times
and thus, inside the encoding of a Turing machine $M$ which takes $n$ steps to
halt. This way the $\lambda$IAM, independently of the space consumption of
$M$, requires space at least linear in the number of reduction steps it
performs, and there is thus no hope to stay within sub-linear space
constraints.

##### (In)Efficiency in Related Works

How could we reconcile all this with the claims from the literature about the
existence of sub-linear space bounds (Mazza [32] and Dal Lago and Schöpp [17,
18]) within the realm of geometry of interaction machines? The answer is
relatively simple: the kind of machines considered in the cited works are
_fundamentally different_ than ours, being based on the idea that the
information stored in logged positions can be taken to be a natural number
_smaller or equal to_ the cardinality of the underlying multi type. In Mazza
[32], this is possible due to the peculiarities of the underlying type system.
There, the use of non-linearity is much more restricted than in the
$\lambda$-calculus, being based on parsimonious types. This allows for tail-
recursive schemas _only_ : in our terminology, all trees are linearly shaped,
and then logged positions can be represented differently and with less space,
namely by simply taking the height of the tree. The works by Dal Lago and
Schöpp [17, 18] rely on the fact that the underlying type system is resource-
aware, this way allowing for a different representation of logged positions as
natural numbers rather than trees. Moreover, space-efficient simulations are
done via an ad-hoc combinator for skewed iterations, thus circumventing the
problem with fixed-point operators. This, unfortunately, is not available in
the realm of the $\lambda$-calculus.

A question, however, remains. Is it possible _at all_ that the $\lambda$IAM
consumes an amount of computation _space_ significantly smaller than
computation _time_? The answer is positive: there is a family of terms
$\\{t_{i}\\}_{i\in\mathbb{N}}$ such that $t_{i}$ reduces in Closed CbN to
normal form in time exponential in $i$ (namely, taking an exponential number
of $\beta$-steps) but requires space linear in $i$, when reduced by the
$\lambda$IAM. Details are in the Appendix.

##  IX Conclusions

Space efficiency of higher-order languages accommodating sub-linear complexity
is a topic about which almost nothing is known. The literature has suggested
that the right tool to achieve it is the alternative paradigm of the IAM, a
machine rooted in the geometry of interaction, without however clarifying
whether its use of space can be used as a reasonable space cost model.

In this paper we develop a sharp tool—a type system—for the understanding of
the space consumption of the ($\lambda$)IAM. Our new tree intersection types
provide—for the first time—exact space bounds, via a simple system of weights
measuring the depth of the tree structure in the types.

The tree structure seems to naturally complement the multiset one needed for
measuring time, and it is of independent interest, given the relevance of
intersection types in semantics. For instance, can such a structure be seen in
game semantics? What does it measure with respect to cut-elimination or
environment machines?

Beyond the theoretical result, the type system has a direct application, as we
show by studying the space usage of the IAM on the traditional encoding of
Turing machines. Such a usage turns out to be very inefficient, providing
negative insights on the elusive conjecture about the reasonable space usage
of the IAM.

Acknowledgements. The second author is funded by the ERC CoG “DIAPASoN” (GA
818616). This work has been partially funded by the ANR JCJC grant “COCA HOLA”
(ANR-16-CE40-004-01).

## References

  * [1] S. Abramsky, R. Jagadeesan, and P. Malacaria, “Full abstraction for PCF,” _Inf. Comput._ , vol. 163, no. 2, pp. 409–470, 2000.
  * [2] B. Accattoli and B. Barras, “Environments and the complexity of abstract machines,” in _Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017_ , W. Vanhoof and B. Pientka, Eds. ACM, 2017, pp. 4–16.
  * [3] B. Accattoli and U. Dal Lago, “On the invariance of the unitary cost model for head reduction,” in _23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan_ , ser. LIPIcs, A. Tiwari, Ed., vol. 15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 22–37.
  * [4] ——, “(Leftmost-Outermost) Beta Reduction is Invariant, Indeed,” _Logical Methods in Computer Science_ , vol. 12, no. 1, 2016.
  * [5] B. Accattoli, U. Dal Lago, and G. Vanoni, “The machinery of interaction,” in _PPDP ’20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020_. ACM, 2020, pp. 4:1–4:15.
  * [6] ——, “The (in)efficiency of interaction,” _Proc. ACM Program. Lang._ , vol. 5, no. POPL, pp. 1–33, 2021.
  * [7] B. Accattoli, S. Graham-Lengrand, and D. Kesner, “Tight typings and split bounds, fully developed,” _J. Funct. Program._ , vol. 30, p. e14, 2020.
  * [8] B. Accattoli and G. Guerrieri, “Types of fireballs,” in _Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings_ , ser. Lecture Notes in Computer Science, S. Ryu, Ed., vol. 11275. Springer, 2018, pp. 45–66.
  * [9] B. Accattoli, G. Guerrieri, and M. Leberle, “Types by need,” in _28th European Symposium on Programming, ESOP 2019,Prague, Czech Republic, April 6-11, 2019, Proceedings_ , ser. Lecture Notes in Computer Science, vol. 11423\. Springer, 2019, pp. 410–439.
  * [10] S. Alves, D. Kesner, and D. Ventura, “A quantitative understanding of pattern matching,” in _25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway_ , 2019, pp. 3:1–3:36.
  * [11] H. P. Barendregt, _The lambda calculus: its syntax and semantics_. North-Holland, 1984.
  * [12] A. Bucciarelli, D. Kesner, A. Ríos, and A. Viso, “The bang calculus revisited,” in _Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings_ , ser. Lecture Notes in Computer Science, K. Nakano and K. Sagonas, Eds., vol. 12073\. Springer, 2020, pp. 13–32.
  * [13] L. Cardelli, “Type systems,” in _The Computer Science and Engineering Handbook_ , A. B. Tucker, Ed. CRC Press, 1997, pp. 2208–2236.
  * [14] M. Coppo and M. Dezani-Ciancaglini, “A new type assignment for $\lambda$-terms,” _Arch. Math. Log._ , vol. 19, no. 1, pp. 139–156, 1978\.
  * [15] U. Dal Lago and B. Accattoli, “Encoding turing machines into the deterministic lambda-calculus,” _CoRR_ , vol. abs/1711.10078, 2017.
  * [16] U. Dal Lago, C. Faggian, and S. Ronchi Della Rocca, “Intersection types and (positive) almost-sure termination,” _Proc. ACM Program. Lang._ , vol. 5, no. POPL, pp. 1–32, 2021.
  * [17] U. Dal Lago and U. Schöpp, “Functional programming in sublinear space,” in _19th European Symposium on Programming, ESOP 2010, Paphos, Cyprus, March 20-28, 2010, Proceedings._ , ser. Lecture Notes in Computer Science, A. D. Gordon, Ed., vol. 6012. Springer, 2010, pp. 205–225.
  * [18] U. Dal Lago and U. Schöpp, “Computation by interaction for space-bounded functional programming,” _Information and Computation_ , vol. 248, pp. 150–194, 2016.
  * [19] V. Danos, H. Herbelin, and L. Regnier, “Game semantics & abstract machines,” in _Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996_. IEEE Computer Society, 1996, pp. 394–405.
  * [20] V. Danos and L. Regnier, “Proof-nets and the hilbert space,” in _Proceedings of the Workshop on Advances in Linear Logic_. USA: Cambridge University Press, 1995, p. 307–328.
  * [21] D. de Carvalho, “Sémantiques de la logique linéaire et temps de calcul,” Thèse de Doctorat, Université Aix-Marseille II, 2007.
  * [22] ——, “Execution time of $\lambda$-terms via denotational semantics and intersection types,” _Math. Str. in Comput. Sci._ , vol. 28, no. 7, pp. 1169–1203, 2018.
  * [23] D. de Carvalho, M. Pagani, and L. Tortora de Falco, “A semantic measure of the execution time in linear logic,” _Theoretical Computer Science_ , vol. 412, no. 20, pp. 1884–1902, 2011.
  * [24] Y. Forster, F. Kunze, and M. Roth, “The weak call-by-value $\lambda$-calculus is reasonable for both time and space,” _Proc. ACM Program. Lang._ , vol. 4, no. POPL, pp. 27:1–27:23, 2020.
  * [25] D. R. Ghica, “Geometry of Synthesis: A Structured Approach to VLSI Design,” in _Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007_ , M. Hofmann and M. Felleisen, Eds. ACM, 2007, pp. 363–375.
  * [26] D. R. Ghica and A. I. Smith, “Geometry of synthesis II: from games to delay-insensitive circuits,” in _Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010, Ottawa, Ontario, Canada, May 6-10, 2010_ , ser. Electronic Notes in Theoretical Computer Science, M. W. Mislove and P. Selinger, Eds., vol. 265. Elsevier, 2010, pp. 301–324.
  * [27] J.-Y. Girard, “Geometry of interaction 1: Interpretation of system f,” in _Logic Colloquium ’88_ , ser. Studies in Logic and the Foundations of Mathematics, R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, Eds. Elsevier, 1989, vol. 127, pp. 221 – 260.
  * [28] D. Kesner and P. Vial, “Consuming and persistent types for classical logic,” in _LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020_ , H. Hermanns, L. Zhang, N. Kobayashi, and D. Miller, Eds. ACM, 2020, pp. 619–632.
  * [29] J. Krivine, _Lambda-calculus, types and models_ , ser. Ellis Horwood series in computers and their applications. Masson, 1993.
  * [30] J.-L. Krivine, “A Call-by-name Lambda-calculus Machine,” _Higher Order Symbol. Comput._ , vol. 20, no. 3, pp. 199–207, 2007.
  * [31] I. Mackie, “The Geometry of Interaction Machine,” in _Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995_ , R. K. Cytron and P. Lee, Eds. ACM Press, 1995, pp. 198–208.
  * [32] D. Mazza, “Simple parsimonious types and logarithmic space,” in _24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany_ , ser. LIPIcs, S. Kreutzer, Ed., vol. 41. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 24–40.
  * [33] D. Mazza, L. Pellissier, and P. Vial, “Polyadic approximations, fibrations and intersection types,” _Proc. ACM Program. Lang._ , vol. 2, no. POPL, pp. 6:1–6:28, 2018.
  * [34] U. Schopp, “Stratified bounded affine logic for logarithmic space,” in _22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings_. IEEE Computer Society, 2007, pp. 411–420.
  * [35] T. Tsukada, K. Asada, and C.-H. L. Ong, “Generalised species of rigid resource terms,” in _32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017_. IEEE Computer Society, 2017, pp. 1–12.
  * [36] C. P. Wadsworth, “Some unusual $\lambda$-calculus numeral systems,” in _To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism_ , J. P. Seldin and J. R. Hindley, Eds., 1980, pp. 215–230.

##  Appendix A Proof of Proposition III.4

A key property of the $\lambda$IAM is bi-determinism, or reversibility: the
machine is deterministic, and moreover for each state $s$ there is at most one
state $s^{\prime}$ such that $s^{\prime}\rightarrow_{\lambda\textsc{IAM}}s$.
The property follows by simply inspecting the rules. Moreover, a run can be
reverted by just switching the direction.

######  Proposition A.1 (Reversibility).

If
$(t,C,L,T,d)\rightarrow_{\lambda\textsc{IAM}}(u,D,L^{\prime},T^{\prime},d^{\prime})$,
then $(u,D,L^{\prime},T^{\prime},d^{\prime
1})\rightarrow_{\lambda\textsc{IAM}}(t,C,L,T,d^{1})$.

From bi-determinism it is immediate to prove acyclicity for reachable states.

######  Proposition A.2.

Let $s$ be a reachable $\lambda$IAM state. Then $s$ is reached exactly once.

###### Proof.

We proceed by induction on the length of the run
$\rho\mathrel{\mathop{\mathchar
58\relax}}s_{0}\rightarrow_{\lambda\textsc{IAM}}^{*}s$. If $|\rho|=0$, the
result is trivial. Otherwise, if $|\rho|>0$, we have
$\rho\mathrel{\mathop{\mathchar
58\relax}}s_{0}\rightarrow_{\lambda\textsc{IAM}}^{*}{s^{\prime}}\rightarrow_{\lambda\textsc{IAM}}s$.
Let us call $\sigma\mathrel{\mathop{\mathchar
58\relax}}s_{0}\rightarrow_{\lambda\textsc{IAM}}^{*}{s^{\prime}}$. By i.h.,
every state in $\sigma$ is reached exactly once. Then $s$ cannot be part of
$\sigma$, because otherwise it would have two different predecessors,
contradicting bi-determinism. Thus $s$ is reached exactly once in $\rho$. ∎

Then, since there are no cycles, an infinite run goes through infinite
different states and thus consumes unbounded space.

######  Proposition A.3.

Let $\rho$ be an infinite $\lambda$IAM run. Then
$|\rho|_{\mathsf{sp}}=\infty$.

###### Proof.

The result comes from the fact that in finite amount of memory, only a finite
amount of configurations can be encoded. Since in an infinite run, an infinite
number of _different states_ are reached, then the $\lambda$IAM needs an
unbounded space to perform the computation. ∎

##  Appendix B Correctness and Completeness of the Tree Type System

The size $|\pi|$ of a tree types derivation $\pi$ is the number of its rules
that are not $\textsc{T}_{\textsc{many}}$. It is the quantity that is used to
prove the termination argument for typed terms.

##### Correctness

In order to prove that typability implies termination via a simple
combinatorial argument, we need to refine the standard statements of the
substitution lemma and of subject reduction with quantitative information.

The next lemma is used in the substitution lemma (namely, the implication from
left to right), and shall also be used in the anti-substitution lemma (the
converse implication).

######  Lemma B.1 (Tree splitting and merging).

Let $T=T_{1}\uplus\hbox to6.00006pt{.\hss.}\uplus T_{k}$. Then there exists
$\pi\;\triangleright[\Gamma]\vdash t\mathrel{\mathop{\mathchar 58\relax}}T$ if
and only if there exist $\pi_{i}\;\triangleright[\Gamma_{i}]\vdash
t\mathrel{\mathop{\mathchar 58\relax}}T_{i}$ for
$i\in\mathinner{\left\\{1,\hbox to6.00006pt{.\hss.},k\right\\}}$. Moreover,
$[\Gamma]=[\Gamma_{1}\uplus\hbox to6.00006pt{.\hss.}\uplus\Gamma_{k}]$ and
$|\pi|=\sum_{i=1}^{n}|\pi_{i}|$.

###### Proof.

We prove the statement by first examining the rule T-many, which is the last
rule used in $\pi$, as $t$ is typed with a tree type.

$[\uplus_{i=1}^{n}\Gamma_{i}]\vdash t\mathrel{\mathop{\mathchar
58\relax}}[G_{1},\hbox to6.00006pt{.\hss.},G_{n}]=T_{1}\uplus\hbox
to6.00006pt{.\hss.}\uplus T_{k}\lx@proof@logical@and\Gamma_{i}\vdash
t\mathrel{\mathop{\mathchar 58\relax}}G_{i}1\leq i\leq n$

We can prove the statement considering $k$ derivations, each of them deriving
the judgment $t\mathrel{\mathop{\mathchar 58\relax}}T_{j}$.

$[\uplus_{i=1}^{|T_{j}|}\Gamma_{i}]\vdash t\mathrel{\mathop{\mathchar
58\relax}}[G_{1},\hbox
to6.00006pt{.\hss.},G_{|T_{j}|}]=T_{j}\lx@proof@logical@and\Gamma_{i}\vdash
t\mathrel{\mathop{\mathchar 58\relax}}G_{i}1\leq i\leq|T_{j}|$

∎

######  Lemma B.2 (Quantitative substitution).

Let $\pi_{t}\;\triangleright\Gamma,x\mathrel{\mathop{\mathchar
58\relax}}T\vdash t\mathrel{\mathop{\mathchar 58\relax}}G$ and
$\pi_{u}\;\triangleright\vdash u\mathrel{\mathop{\mathchar 58\relax}}T$. Then
there exists $\pi_{t\\{x{\shortleftarrow}u\\}}\;\triangleright\Gamma\vdash
t\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}A$ such that
$|\pi_{t\\{x{\shortleftarrow}u\\}}|=|\pi_{t}|+|\pi_{u}|-|T^{\ell}|$.

###### Proof.

By induction on the derivation $\pi_{t}$.

  * •

_Rule T-Var_. Two sub-cases:

    1. 1.

$t=x$: then $t\\{x{\shortleftarrow}u\\}=u$, $G=A$, and $T=[A]$ is a singleton.
Then the hypothesis $\pi_{u}\;\triangleright\vdash u\mathrel{\mathop{\mathchar
58\relax}}T$ is necessarily obtained by applying a unary T-many rule to a
derivation of the form $\pi^{\prime}_{u}\;\triangleright\vdash
u\mathrel{\mathop{\mathchar 58\relax}}A$. The typing derivation
$\pi_{t\\{x{\shortleftarrow}u\\}}\mathrel{\mathop{\mathchar
58\relax}}=\pi^{\prime}_{u}$ satisfies the statement because
$|\pi_{t\\{x{\shortleftarrow}u\\}}|=|\pi^{\prime}_{u}|=1+|\pi^{\prime}_{u}|-1=|\pi_{t}|+|\pi_{u}|-|T^{\ell}|$.

    2. 2.

$t=y$: then $t\\{x{\shortleftarrow}u\\}=y$ and $T=[\cdot]$. Then the
hypothesis $\pi_{u}\;\triangleright\vdash u\mathrel{\mathop{\mathchar
58\relax}}T$ is necessarily obtained by applying a T-none rule, and
$|\pi_{u}|=0$. The typing derivation
$\pi_{t\\{x{\shortleftarrow}u\\}}\mathrel{\mathop{\mathchar
58\relax}}=\pi_{t}$ satisfies the statement because
$|\pi_{t\\{x{\shortleftarrow}u\\}}|=|\pi_{t}|=|\pi_{t}|+0-0=|\pi_{t}|+|\pi_{u}|-|T^{\ell}|$.

  * •

_Rule $\textsc{T-}\lambda_{\star}$_. Then $t=\lambda y.r$, $G=\star$, and
$T=[\cdot]$. It goes as for the second variable case ($t=y$). Namely, the
hypothesis $\pi_{u}\;\triangleright\vdash u\mathrel{\mathop{\mathchar
58\relax}}T$ is necessarily obtained by applying a T-none rule, and
$|\pi_{u}|=0$. The typing derivation $\pi_{t\\{x{\shortleftarrow}u\\}}$ is
also a single $\textsc{T-}\lambda_{\star}$ rule, because
$t\\{x{\shortleftarrow}u\\}=(\lambda y.r)\\{x{\shortleftarrow}u\\}=\lambda
y.r\\{x{\shortleftarrow}u\\}$ is also an abstraction. Note that
$\pi_{t\\{x{\shortleftarrow}u\\}}$ satisfies the statement because
$|\pi_{t\\{x{\shortleftarrow}u\\}}|=|\pi_{t}|=|\pi_{t}|+0-0=|\pi_{t}|+|\pi_{u}|-|T^{\ell}|$.

  * •

_Rule $\textsc{T-}\lambda$_. Then $\pi_{t}$ has the following shape:

$\Gamma,x\mathrel{\mathop{\mathchar 58\relax}}T\vdash\lambda
y.r\mathrel{\mathop{\mathchar 58\relax}}T^{\prime}\rightarrow
A^{\prime}\pi_{r}\;\triangleright\Gamma,x\mathrel{\mathop{\mathchar
58\relax}}T,y\mathrel{\mathop{\mathchar 58\relax}}T^{\prime}\vdash
r\mathrel{\mathop{\mathchar 58\relax}}A^{\prime}$

with $t=\lambda y.r$ and $G=T^{\prime}\rightarrow A^{\prime}$. By i.h., there
exists a derivation
$\pi_{r\\{x{\shortleftarrow}u\\}}\;\triangleright\Gamma,y\mathrel{\mathop{\mathchar
58\relax}}T^{\prime}\vdash
r\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}A^{\prime}$
such that $|\pi_{r\\{x{\shortleftarrow}u\\}}|=|\pi_{r}|+|\pi_{u}|-|T^{\ell}|$.
Applying back rule $\textsc{T-}\lambda$ we obtain $\pi_{(\lambda
y.r)\\{x{\shortleftarrow}u\\}}$

$\Gamma\vdash\lambda y.r\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar
58\relax}}T^{\prime}\rightarrow
A^{\prime}\pi_{r\\{x{\shortleftarrow}u\\}}\;\triangleright\Gamma,y\mathrel{\mathop{\mathchar
58\relax}}T^{\prime}\vdash
r\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}A^{\prime}$

which satisfies $|\pi_{(\lambda
y.r)\\{x{\shortleftarrow}u\\}}|=|\pi_{r\\{x{\shortleftarrow}u\\}}|+1=_{\textit{i.h.}}|\pi_{r}|+|\pi_{u}|-|T^{\ell}|+1=|\pi_{\lambda
y.r}|+|\pi_{u}|-|T^{\ell}|$.

  * •

_Rule T-@_. Then $\pi_{t}$ has the following shape:

$x\mathrel{\mathop{\mathchar 58\relax}}T_{1}\uplus
T_{2},\Gamma\uplus\Delta\vdash rw\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\pi_{r}\;\triangleright
x\mathrel{\mathop{\mathchar 58\relax}}T_{1},\Gamma\vdash
r\mathrel{\mathop{\mathchar 58\relax}}T^{\prime}\rightarrow
A\pi_{w}\;\triangleright x\mathrel{\mathop{\mathchar
58\relax}}T_{2},\Delta\vdash w\mathrel{\mathop{\mathchar 58\relax}}T^{\prime}$

with $t=rw$, $G=A$, and $T=T_{1}\uplus T_{2}$. By Lemma B.1, the hypothesis
$\pi_{u}\;\triangleright\vdash u\mathrel{\mathop{\mathchar 58\relax}}T$ splits
into two derivations $\pi_{u}^{1}\;\triangleright\vdash
u\mathrel{\mathop{\mathchar 58\relax}}T_{1}$ and
$\pi_{u}^{2}\;\triangleright\vdash u\mathrel{\mathop{\mathchar
58\relax}}T_{2}$ such that $|\pi_{u}|=|\pi_{u}^{1}|+|\pi_{u}^{2}|$. By i.h.,
there exist:

    1. 1.

$\pi_{r\\{x{\shortleftarrow}u\\}}\;\triangleright\Gamma\vdash
r\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar
58\relax}}T^{\prime}\rightarrow A$ such that
$|\pi_{r\\{x{\shortleftarrow}u\\}}|=|\pi_{r}|+|\pi_{u}^{1}|-|T^{\ell}_{1}|$,
and

    2. 2.

$\pi_{w\\{x{\shortleftarrow}u\\}}\;\triangleright\Delta\vdash
w\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}T^{\prime}$
such that
$|\pi_{w\\{x{\shortleftarrow}u\\}}|=|\pi_{w}|+|\pi_{u}^{2}|-|T^{\ell}_{2}|$.

Note that
$(rw)\\{x{\shortleftarrow}u\\}=r\\{x{\shortleftarrow}u\\}w\\{x{\shortleftarrow}u\\}$.
Then the derivation $\pi_{(rw)\\{x{\shortleftarrow}u\\}}$ is defined as
follows:

$\Gamma\uplus\Delta\vdash
r\\{x{\shortleftarrow}u\\}w\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar
58\relax}}A\lx@proof@logical@and\pi_{r\\{x{\shortleftarrow}u\\}}\;\triangleright\Gamma\vdash
r\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar
58\relax}}T^{\prime}\rightarrow
A\pi_{w\\{x{\shortleftarrow}u\\}}\;\triangleright\Delta\vdash
w\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}T^{\prime}$

for which

$\begin{array}[]{rll}|\pi_{(rw)\\{x{\shortleftarrow}u\\}}|&=&|\pi_{r\\{x{\shortleftarrow}u\\}}|+|\pi_{w\\{x{\shortleftarrow}u\\}}|+1\\\
&=_{\textit{i.h.}}&|\pi_{r}|+|\pi_{u}^{1}|-|T^{\ell}_{1}|+|\pi_{w}|+|\pi_{u}^{2}|-|T^{\ell}_{2}|+1\\\
&=&(|\pi_{r}|+|\pi_{w}|+1)+(|\pi_{u}^{1}|+|\pi_{u}^{2}|)-(|T^{\ell}_{1}|+|T^{\ell}_{2}|)\\\
&=&|\pi_{rw}|+|\pi_{u}|-|T^{\ell}|\end{array}$

  * •

_Rule T-none_. Then $G=[\cdot]$, and $T=[\cdot]$. It goes as for the second
variable case ($t=y$). Namely, the hypothesis $\pi_{u}\;\triangleright\vdash
u\mathrel{\mathop{\mathchar 58\relax}}T$ is necessarily obtained by applying
another T-none rule, and $|\pi_{u}|=0$. The typing derivation
$\pi_{t\\{x{\shortleftarrow}u\\}}$ is also a single T-none rule for the term
$t\\{x{\shortleftarrow}u\\}$. Note that $\pi_{t\\{x{\shortleftarrow}u\\}}$
satisfies the statement because
$|\pi_{t\\{x{\shortleftarrow}u\\}}|=|\pi_{t}|=|\pi_{t}|+0-0=|\pi_{t}|+|\pi_{u}|-|T^{\ell}|$.

  * •

_Rule T-many_. Then $\pi_{t}$ has the following shape:

$[\uplus_{i=1}^{n}\Gamma_{i}],x\mathrel{\mathop{\mathchar
58\relax}}[\uplus_{i=1}^{n}T_{i}]\vdash t\mathrel{\mathop{\mathchar
58\relax}}[G_{1},\hbox
to6.00006pt{.\hss.},G_{n}]\lx@proof@logical@and\Gamma_{i},x\mathrel{\mathop{\mathchar
58\relax}}T_{i}\vdash t\mathrel{\mathop{\mathchar 58\relax}}G_{i}1\leq i\leq
n$

By Lemma B.1, the hypothesis $\pi_{u}\;\triangleright\vdash
u\mathrel{\mathop{\mathchar 58\relax}}T$ splits into $n$ derivations
$\pi_{u}^{i}\;\triangleright\vdash u\mathrel{\mathop{\mathchar
58\relax}}T_{i}$ with $i\in\mathinner{\left\\{1,\hbox
to6.00006pt{.\hss.},n\right\\}}$ such that
$|\pi_{u}|=\sum_{i=1}^{n}|\pi_{u}^{i}|$. By i.h., there exist $n$ derivations
$\pi_{t\\{x{\shortleftarrow}u\\}}^{i}\;\triangleright\Gamma_{i}\vdash
t\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}G_{i}$ such
that
$|\pi_{t\\{x{\shortleftarrow}u\\}}|^{i}=|\pi_{t}|^{i}+|\pi_{u}^{i}|-|T^{\ell}_{i}|$.
Then the derivation $\pi_{t\\{x{\shortleftarrow}u\\}}$ is defined as follows:

$[\uplus_{i=1}^{n}\Gamma_{i}]\vdash
t\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}[G_{1},\hbox
to6.00006pt{.\hss.},G_{n}]\lx@proof@logical@and\pi_{t\\{x{\shortleftarrow}u\\}}^{i}\;\triangleright\Gamma_{i}\vdash
t\\{x{\shortleftarrow}u\\}\mathrel{\mathop{\mathchar 58\relax}}G_{i}1\leq
i\leq n$

for which

$\begin{array}[]{rll}|\pi_{t\\{x{\shortleftarrow}u\\}}|&=&\sum_{i=1}^{n}|\pi_{t\\{x{\shortleftarrow}u\\}}|^{i}\\\
&=_{\textit{i.h.}}&\sum_{i=1}^{n}(|\pi_{t}|^{i}+|\pi_{u}^{i}|-|T^{\ell}_{i}|)\\\
&=&\sum_{i=1}^{n}|\pi_{t}|^{i}+\sum_{i=1}^{n}|\pi_{u}^{i}|-\sum_{i=1}^{n}|T^{\ell}_{i}|\\\
&=&|\pi_{t}|+|\pi_{u}|-|T^{\ell}|\end{array}$

∎

######  Proposition B.3 (Quantitative Subject Reduction).

If $t$ is closed, $\pi\;\triangleright\vdash t\mathrel{\mathop{\mathchar
58\relax}}A$, and $t\rightarrow_{wh}u$ then there exists