arXiv:1711.10301v1 [] 28 Nov 2017

The Maximal MAM,
a Reasonable Implementation of
the Maximal Strategy
Beniamino Accattoli
INRIA, UMR 7161, LIX, École Polytechnique, France

1

Introduction

This note is about a reasonable abstract machine, called Maximal MAM, implementing the maximal strategy of the λ-calculus, that is, the strategy that always
produces a longest evaluation sequence. The abstract machine is a minor variation over the Useful MAM of [Acc16], that is a reasonable implementation of
the leftmost-outermost strategy. Here reasonable is a technical term: an abstract machine M implementing a strategy → is reasonable when its overhead
on a given term t is polynomial with respect to the size of t and the number of
→-steps necessary to evaluate t.
The result of this note is discussed and put in context in the author’s
(In)Efficiency and Reasonable Cost Models [Acc17]. Essentially, the maximal
strategy is a peculiar case-study, for the following reasons:
• Non-trivial reasonable implementation: it is the most inefficient strategy
ever, and yet implementing it with a reasonable overhead requires the
whole heavy machinery, namely useful sharing, needed for the leftmostoutermost strategy, the other only strong strategy known to be reasonable.
• Unreasonable cost model : it is reasonably implementable—that usually is
the tricky part in the study of cost models—but its number of steps does
not provide a reasonable cost model. Indeed the strategy is so inefficient
that it cannot even simulate Turing machines, that usually is the easy part
in the study of cost models. To be precise, there are no proofs of such
impossibility, but the known encodings of Turing machines do not work
when the evaluation strategy in the λ-calculus is the maximal one.
We first define the strategy, and then show how to implement it via the Max
MAM. The technical details follow closely those in [Acc16] for the Useful MAM.
In turn, the Useful MAM is a refinement of the Strong MAM, an unreasonable
abstract machine for the leftmost-outermost strategy studied in [ABM15], that
in turn is a simplification of Cregut’s machine [Cré90, Cré07, GNM13]. The
literature about abstract machines for strong evaluation is extremely limited,
we essentially already cited all existing papers on the subject. A few further
papers [GL02, AC15, AG17] deal with abstract machines for weak evaluation
1

with open terms, that is an intermediate framework between the one of weak
evaluation with closed terms, to which the almost totality of the literature is
devoted, and the almost inexistent one of strong evaluation.

2

λ-Calculus and Maximal Evaluation

The syntax of the ordinary λ-calculus is given by the following grammar for
terms:
λ-Terms
t, u, r, s ::= x | λx.t | tu.
We use t{x u} for the usual (meta-level) notion of substitution. An abstraction
λx.t binds x in t, and we silently work modulo α-equivalence of bound variables,
e.g. (λy.(xy)){x y} = λz.(yz). We use fv(t) for the set of free variables of t.
β-reduction. We define β-reduction →β as follows:
Contexts
C ::= h·i | λx.C | Ct | tC
Rule at top level
(λx.t)u 7→β t{x u}
Contextual closure
Chti →β Chui if t 7→β u
A context C is applicative if C = Dhh·iui for some D and u. A term t is a normal
form, or simply normal, if there is no u such that t →β u, and it is neutral if
it is normal and it is not of the form λx.u (i.e. it is not an abstraction). The
position of a β-redex Chti →β Chui is the context C in which it takes place.
To ease the language, we will identify a redex with its position. A derivation
d : t →k u is a finite, possibly empty, sequence of reduction steps. We write |t|
for the size of t and |d| for the length of d.
Maximal Evaluation. The maximal strategy is the variation over leftmostoutermost (LO) evaluation in which, when the LO redex (λx.t)u is erasing (that
is, when x ∈
/ fv(t)), the strategy first evaluates (maximally) u to u′ , and then
fires the erasing redex (λx.t)u′ →β t, to avoid the erasure of the β-redexes of
u before being reduced. Of course, if u diverges than the maximal strategy
diverges, while the LO strategy would not (or, at least, not because of u). The
LO strategy is inefficient but it has the key property of being normalizing, i.e.
it reaches a normal form whenever it exists. The maximal strategy, dually, is
perpetual, that is, it diverges whenever possible. See van Raamsdonk at al.’s
[vRSSX99] for more about perpetual and maximal strategies.
We define the maximal strategy by first defining the notion of maximal
context, that is a context in which a maximal redex can appear (and not a
context that cannot be extended).
Definition 2.1 (Max Context). Maximal (or max) contexts are defined by induction as follows:

2

h·i is Max

(ax)

C is Max (λ)
λx.C is Max

C is Max
C 6= λx.D
(@l)
Ct is Max
x∈
/ fv(t)
C is Max
(gc)
(λx.t)C is Max

t is neutral
C is Max (@r)
tC is Max
We define the maximal β-reduction strategy →Maxβ as follows:
Rule at top level
(λx.t)u 7→Maxβ t{x u} if x ∈ fv(t) or u is normal
Contextual closure
Chti →Maxβ Chui if t 7→Maxβ u
As expected,
Lemma 2.2 (Basic Properties of the Maximal Strategy, Proof at page 13). Let
t be a λ-term that is not normal. Then
1. Completeness: there exists u such that t →Maxβ u.
2. Determinism: moreover, such a u is unique.
Let us point out that we talk about the maximal strategy despite the fact
that there are many maximal strategies, that can be obtained from our definition
by adding some more freedom in the choice of the redex. A typical example is
given by xtu: our strategy first reduces t and then (if t terminates) it evaluates u,
while one can interleave the evaluations of t and u and still be maximal (because
t cannot act on u in xtu). We refer it as the maximal strategy, because it is
the leftmost maximal strategy, i.e. it mostly behaves as the leftmost strategy,
it only changes its behavior on erasing redexes (and the leftmost strategy is a
sort of canonical strategy).

3

Preliminaries on Abstract Machines

We study two abstract machines, the Maximal Milner Abstract Machine (Max
MAM) (Fig. 4) and an auxiliary machine called the Checking AM (Fig. 2). The
Max MAM is a reasonable implementation of the maximal strategy resting on
labeled environments to implement useful sharing, and on the Checking AM to
produce these labels.
The Max MAM is meant to implement the maximal strategy via a decoding
function · mapping machine states to λ-terms. Machine states s are given by
a code t, that is a λ-term t not considered up to α-equivalence (which is why it
is over-lined), and some data-structures like stacks, frames, and environments.
The data-structures are used to implement the search for the next maximal
redex and a form of micro-steps substitution, and they decode to evaluation
contexts for →Maxβ . Every state s decodes to a term s, having the shape Cs hti,
where t is the code currently under evaluation and Cs is the evaluation context
given by the data-structures.
The Checking AM uses the same states and data-structures of the Max
MAM.
3

The Data-Structures. First of all, our machines are executed on wellnamed terms, that are those α-representants where all variables (both bound
and free) have distinct names. Then, the data-structures used by the machines
are defined in Fig. 1, namely:
1. Stack π: it contains the arguments of the current code;
2. Frame F : a second stack, that together with π is used to walk through the
term and search for the next redex to reduce. The items φ of a frame are of
three kinds:
1. Variables: a variable x is pushed on the frame F whenever the machines
starts evaluating under an abstraction λx.
2. Head argument contexts: t♦π is pushed on F every time evaluation enters
in the right subterm u of an application tu. The entry saves the left part
t of the application and the current stack π, to restore them when the
evaluation of the right subterm u is over.
3. Erasing Contexts: λx.tπ is pushed on F every time evaluation finds
an erasing redex (λx.t)u (that is, a redex for which x ∈
/ fv(t)). In this
case evaluation enters in the argument u to normalize it (or, possibly, to
diverge) before erasing it.
4. Global Environment E: it is used to implement micro-step substitution (i.e.
on a variable occurrence at the time), storing the arguments of β-redexes that
have been encountered so far. Most of the literature on abstract machines
uses local environments and closures. Having just one global environment
E (used only in a minority of works [FS09, SGM02, DZ13, ABM14, AC15,
ABM15, Acc16, AG17], and discussed at length in [AB17]) removes the need
for closures and simplifies the machine. On the other hand, it forces to use
α
explicit α-renamings (the operation t in ered and eabs in Fig. 4), but
this does not affect the overall complexity, as it speeds up other operations,
see [AB17]. The entries of E are of the form [x t]l , i.e. they carry a label
l used to implement usefulness, to be explained later on in this section. We
write E(x) = [x t]l when E contains [x t]l and E(x) = ⊥ when in E there
are no entries of the form [x t]l .
→→

The Decoding. Every state s decodes to a term s (see Fig. 3) of shape
Cs ht E i, where
1. t E is a λ-term, roughly obtained by applying to the code the substitution
induced by the global environment E. More precisely, the operation t E is
called unfolding and it is properly defined at the end of this section.
2. Cs is a context, that will be shown to be a max context, obtained by decoding
the stack π and the dump D and applying the unfolding. Note that, to
improve readability, π is decoded in postfix notation for plugging.
→

The Transitions. According to the distillation approach of [ABM14] (related to Danvy and Nielsen’s refocusing [DN04]) we distinguish different kinds
of transitions, whose names reflect a proof-theoretical view, as transitions can
be seen as cut-elimination steps [ABS09, ABM14]:
1. Multiplicatives m : they correspond to the firing of a β-redex (λx.t)u, except that if the argument u is not a variable and the redex is not erasing
(that happens when x ∈ fv(t)) then u is not substituted but added to the
environment;
2. Exponentials
e : they perform a clashing-avoiding substitution from the
4

✓
Frames
Frame Items
Labels
✒

F
φ
l

::=
::=
::=

ǫ | F :: φ
x | t♦π | λx.tπ
abs | (red, n ∈ N) | neu

Stacks
π ::=
Phases
ϕ ::=
Environments E ::=

Figure 1: Grammars.

→

environment on the single variable occurrence represented by the current
code. They implement micro-step substitution.
3. Commutatives c : they locate and expose the next redex according to the
maximal strategy, by rearranging the data-structures.
Both exponential and commutative transitions are invisible on the λ-calculus.
Garbage collection of environment entries that are no longer necessary is here
simply ignored, or, more precisely, it is encapsulated at the meta-level, in the
decoding function.
Labels for Useful Sharing A label l for a code in the environment can be
of three kinds. Roughly, they are:
1. Neutral, or l = neu: it marks a neutral term, that is always useless as it
is β-normal and its substitution cannot create a redex, because it is not an
abstraction;
2. Abstraction, or l = abs: it marks an abstraction, that is a term that is
at times useful to substitute. If the variable that it is meant to replace is
applied, indeed, the substitution of the abstraction creates a β-redex. But
if it is not applied, it is useless.
3. Redex, or l = red: it marks a term that contains a β-redex. It is always
useful to substitute these terms.
Actually, the explanation we just gave is oversimplified, but it provides a first
intuition about labels. In fact in an environment [x t]l :: E it is not really
t that has the property mentioned by its label, rather the term t E obtained
by unfolding the rest of the environment on t. The idea is that [x t]red states
that it is useful to substitute t to later on obtain a redex inside it (by potential
further substitutions on its variables coming from E). The precise meaning of
the labels will be given by Definition 4.2, and the properties they encode will
be made explicit by Lemma 6.11 in the Appendix (page 31).
A further subtlety is that the label red for redexes is refined as a pair (red, n),
where n is the number of substitutions in E that are needed to obtain the
maximal redex in t E . Our machines never inspect these numbers, they are
only used for the complexity analysis of Sect. 6.
→

Grafting and Unfoldings The unfolding of the environment E on a code t
is defined as the recursive capture-allowing substitution (called grafting) of the
entries of E on t. For lack of space, the precise definition has been moved to
the Appendix (page 13).

4

The Checking Abstract Machine

The Checking Abstract Machine (Checking AM) is defined in Fig. 2 and it is a
variation over the very similar auxiliary checking machine for the Useful MAM
in [Acc16]. The difference between the two is in the two new transitions ⇀c7
5

ǫ | t :: π
H|N
ǫ | [x t]l :: E

✏
✑

✬

Frame
F
F

Code
tu
λx.t

Stack Env
π
E
u :: π
E

Ph
H ⇀Hc1
H ⇀o1

Frame
Code
t
F
output (red, 1)

F

λx.t

u :: π

H

F :: λx.tπ

F
F

λx.t
x

F

x

F

x

F :: x
F :: t♦π
F :: λx.tπ
F
ǫ
ǫ

t
u
u
t
tu
λx.t

F :: x
t
ǫ
output (red, n + 1)
if E(x) = [x t](red,n)
u :: π
E
H ⇀o3
output (red, 2)
if E(x) = [x t]abs
π
E
H ⇀Hc3
x
π
E
N
F
if E(x) = ⊥ or E(x) = [x t]neu or (E(x) = [x t]abs and π = ǫ)
F
ǫ
E
N ⇀Nc4
λx.t
ǫ
E
N
F
ǫ
E
N ⇀Nc5
tu
π
E
N
ǫ
E
N ⇀o6
output (red, 1)
u :: π
E
N ⇀Nc6
u
ǫ
E
H
F :: t♦π
ǫ
E
N ⇀o4
output neu
ǫ
E
N ⇀o5
output abs

✫

E
E

Hc7

u

⇀Hc2
⇀o2

H
H

ǫ

Figure 2: The Checking Abstract Machine (Checking AM).

h·i
πhh·iui
Dhπhth·iii
Dhπh(λx.t)h·iii

F :: x := Dhλx.h·ii
Cs := Dhπi E
s := Dhπhtii E = Cs ht
where s = (F, t, π, E)

Ei

Figure 3: Decoding.

and ⇀o6 (that is also why in Fig. 2 they are misplaced with respect to the
progressing numbering), plus the side condition if x ∈ fv(t) in ⇀o1 .
The Checking AM starts executions on states of the form (ǫ, t, ǫ, E, H), with
the aim of checking the usefulness of t with respect to the environment E, i.e. it
walks through t and whenever it encounters a variable x it looks up its usefulness
in E.
The Checking AM has seven commutative transitions, noted ⇀ci with i =
1, .., 7, used to walk through the term, and six output transitions, noted ⇀oj
with j = 1, .., 6, that produce the value of the test for usefulness, to be later used
by the Max MAM. The exploration is done in two alternating phases, evaluation
H and backtracking N. Evaluation explores the current code (morally towards
the head, except when it encounters an erasing redex, that is when it first
explores the right subterm) storing in the stack and in the frame the parts of
the code that it leaves behind. Backtracking comes back to an argument that
was stored in the frame, when the current head has already been checked. Note
that the Checking AM never modifies the environment, it only looks it up, nor it
erases or duplicates any piece of code, it only walks through the data structures.
Let us explain the transitions. First the commutative ones:
• ⇀Hc1 : the code is an application tu and the machine starts exploring the
left subterm t, storing u on top of the stack π.
6

✩

✪

✘

→

:=
:=
:=
:=

→

ǫ
u :: π
F :: t♦π
F :: λx.tπ
✚

Ph
H

if x ∈ fv(t)
E
H
if x ∈
/ fv(t)
E
H

→

✛

ǫ
π

E

Stack Env
u :: π
E

✙

• ⇀Hc7 : the code λx.t and the first argument u on the stack form an erasing
redex (by hypothesis x ∈
/ fv(t)). The machine has found a β-redex but it
cannot output yet, because it does not know what number n to associate
to the label l = (red, n). Indeed, (λx.t)u is the next β-redex to reduce
only if u is normal, otherwise the next one will be in u and obtaining it
may require many substitution steps. Therefore, the machine stores λx.t
and the current stack π on the frame F and starts checking u (with an
empty stack).
• ⇀Hc2 : the code is an abstraction λx.t and the machine goes under the
abstraction, storing x on top of the frame F .
• ⇀Hc3 : the machine finds a variable x that either has no associated entry
in the environment (if E(x) = ⊥) or its associated entry [x t]l in the
environment is useless. This can happen if either l = neu, i.e. substituting
t would only lead to a neutral term, or l = abs, i.e. substituting t would
provide an abstraction, but the stack is empty, and so it is useless to
substitute the abstraction because no β-redexes will be obtained. Thus
the machine switches to the backtracking phase (N), whose aim is to undo
the frame to obtain a new subterm to explore.
• ⇀Nc4 : it is the inverse of ⇀Hc2 , it puts back on the code an abstraction
that was previously stored in the frame.
• ⇀Nc5 : backtracking from the evaluation of an argument u, it restores the
application tu and the stack π that were previously stored in the frame.
• ⇀Nc6 : backtracking from the evaluation of the left subterm t of an application tu, the machine starts evaluating the right subterm (by switching
to the evaluation phase H) with an empty stack ǫ, storing on the frame
the pair t♦π of the left subterm and the previous stack π.
Then the output transitions:
• ⇀o1 : the machine finds a non-erasing β-redex, namely (λx.t)u (by hypothesis x ∈ fv(t), and thus outputs a label saying that it requires only one
substitution step (namely substituting the term the machine was executed
on) to eventually find a β-redex.
• ⇀o2 : the machine finds a variable x whose associated entry [x t](red,n)
in the environment is labeled with (red, n), and so outputs a label saying
that it takes n + 1 substitution steps to eventually find a β-redex (n plus
1 for the term the machine was executed on).
• ⇀o3 : the machine finds a variable x whose associated entry [x t]abs in
the environment is labeled with abs, so t is an abstraction, and the stack
is non-empty. Since substituting the abstraction will create a β-redex,
the machine outputs a label saying that it takes two substitution steps to
obtain a β-redex, one for the term the machine was executed on and one
for the abstraction t.
• ⇀o6 : the machine went through the whole code u and found no redexes.
Then u is normal and together with the erasing abstraction λx.t in the
7

frame it forms an erasing redex ready to fire, and so the output is a label
saying that it requires only one substitution step (namely substituting the
term the machine was executed on) to eventually find a β-redex.
• ⇀o4 : the machine went through the whole term, that is an application,
and found no redex, nor any redex that can be obtained by substituting
from the environment. Thus that term is neutral and so the machine
outputs the corresponding label.
• ⇀o5 : as for the previous transition, except that the term is an abstraction,
and so the output is the abs label.
The fact that commutative transitions only walk through the code, without
changing anything, is formalized by the following lemma, that is crucial for the
proof of correctness of the Checking AM (forthcoming Theorem 4.3).
Lemma 4.1 (Commutative Transparency, Proof at P. 14). Let s = (F, t, π, E, ϕ)
′
(F ′ , t , π ′ , E, ϕ′ ) = s′ . Then
′

1. Decoding Without Unfolding: F hhtiπi = F ′ hht iπ ′ i, and
2. Decoding With Unfolding: s = s′ .
For the analysis of the properties of the Checking AM we need a notion of
well-labeled environment, i.e. of environment where the labels are consistent
with their intended meaning. It is a technical notion also providing enough
information to perform the complexity analysis, later on. Moreover, it includes
two structural properties of environments: 1) in [x t]l the code t cannot be a
variable, and 2) there cannot be two entries associated to the same variables.
Definition 4.2 (Well-Labeled Environments). Well-labeled environments E
are defined by
1. Empty: ǫ is well-labeled;
2. Inductive: [x t]l :: E ′ is well-labeled if E ′ is well-labeled, x is fresh with
respect to t and E ′ , and
→

(a) Abstractions: if l = abs then t and t

E′

are normal abstractions;
→ →

(b) Neutral Terms: if l = neu then t is an application and t

E′

is neutral.

(c) Redexes: if l = (red, n) then t is not a variable, t E ′ contains a
β-redex. Moreover, there is a Max-context C such that t = Chui and
• if n = 1 then u is a 7→Maxβ -redex,
• if n > 1 then u = x and E ′ = E ′′ :: [y u]l :: E ′′′ with
– if n > 2 then l = (red, n − 1)
– if n = 2 then l = (red, 1) or (l = abs and C is applicative).
The study of the Checking AM requires some technical invariants proved in
the appendix (page 15). The next theorem provides the main properties of the
Checking AM, i.e. that when executed on t and E it provides a label l to extend
E with a consistent entry for t (i.e. such that [x t]l :: E is well-labeled), and
that such an execution takes time linear in the size of t.
8

c1,2,3,4,5,6,7

Let us explain an important point about the complexity of the machine transition. Variables are meant to be implemented as memory locations and variable
occurrences as pointers to those location. Therefore, the global environment E
is a store and can be accessed randomly, that is, with no need to go through it
sequentially. With this hypothesis on the representation of terms, see [AB17]
for an actual implementation, all the transitions of the Checking AM but ⇀Hc7
/ fv(t) in ⇀Hc7
and ⇀o1 can be implemented in constant time. The check x ∈ / ∈
and ⇀o1 at first sight requires time proportional to the size of the initial term,
but in fact it can be implemented in O(1) if one assumes a stronger hypothesis
on the representation of terms: a variable is a data-type with a memory location plus pointers to its occurrences. Then all transitions can be implemented
in O(1). Anyway, this hypothesis is not essential for the implementation to be
reasonable. If dropped, the subterm property (Lemma 6.9.1) guarantees that
the size of terms does not explode and that the check x ∈ / ∈
/ fv(t) can be
done in reasonable time. The hypothesis, however, simplifies considerably the
analysis.
Theorem 4.3 (Checking AM Properties, Proof at Page 18). Let t be a code
and E a global environment.
1. Determinism and Progress: the Checking AM is deterministic and there
always is a transition that applies;
2. Termination and Complexity: the execution of the Checking AM on t and
E always terminates, taking O(|t|) steps, moreover
3. Correctness: if E is well-labeled, x is fresh with respect to E and t, and l
is the output then [x t]l :: E is well-labeled.

5

The Maximal Milner Abstract Machine

The Maximal Milner Abstract Machine, or Max MAM, is defined in Fig. 4 and it
is a small variation over the Useful MAM of [Acc16] (as for the Checking AM, the
difference is in the two new transitions, Hc7 and m3 , plus the side condition
if x ∈ fv(t) in m2 ). It is very similar to the Checking AM, in particular
it has exactly the same commutative transitions, and the same organization in
evaluating and backtracking phases. The difference with respect to the Checking
AM is that the output transitions are replaced by micro-step computational
rules that reduce β-redexes and implement useful substitutions. Let us explain
them:
• Multiplicative Transition m1 : when the argument of the β-redex (λx.t)y is
a variable y then it is immediately substituted in t. This happens because
1) such substitution are not costly (by the subterm invariant, Lemma 6.9 in
the Appendix, their cost is bound by the size of t that is bound by the size
of the initial term); 2) because in this way the environment stays compact;
3) because in this way the labels for useful sharing are slightly simpler.
• Multiplicative Transition m2 : since the argument u is not a variable and
the redex is not erasing (x ∈ fv(t) by hypothesis) then the redex is fired by
adding the entry [x u]l to the environment, with l obtained by running the
Checking AM on u and E.

9

✬

Frame
Code Stack Env
F
tu
π
E
F
λx.t y :: π
E
F
λx.t u :: π
E
if x ∈ fv(t) and u is not a
F
λx.t u :: π
E
F
F

λx.t
x

ǫ
π

E
E

F

x

u :: π

E

F

x

π

E

F :: x
F :: t♦π
F :: λx.tπ
F

t
u
u
t

ǫ
ǫ
ǫ
u :: π

E
E
E
E

if

✫
α
t

Ph
Frame
Code Stack
Env
Ph
F
H
t
u :: π
E
H
Hc1
H
t{x y}
π
E
H
F
m1
H
t
π
[x u]l :: E H
F
m2
variable and l is the output of the Checking AM on u and E
F :: λx.tπ
H
u
ǫ
E
H
Hc7
if x ∈
/ fv(t) and u is not a variable
F :: x
H
t
ǫ
E
H
Hc2
α
H
F
t
π
E
H
ered
if E(x) = [x t](red,n)
α
H
F
t
u :: π
E
H
eabs
if E(x) = [x t]abs
H
x
π
E
N
F
Hc3
E(x) = ⊥ or E(x) = [x t]neu or (E(x) = [x t]abs and π = ǫ)
N
λx.t
ǫ
E
N
F
Nc4
N
tu
π
E
N
F
Nc5
N
t
π
E
H
F
m3
F :: t♦π
N
u
ǫ
E
H
Nc6

is any code α-equivalent to t such that it is well-named and its bound names are fresh with
respect to those in the other machine components.

Figure 4: The Maximum (Useful) Milner Abstract Machine (Max MAM).

• Multiplicative Transition m3 : an invariant of the machine is that when it
backtracks (phase N) the code is normal (see Lemma 6.6.2a in the Appendix,
page 20). Moreover, every abstraction λx.t in an erasing redex entry λx.tπ
in the frame is such that x ∈
/ fv(t) (Lemma 6.6.4). Then in m3 the code u
is normal and together with λx.t it forms an erasing 7→Maxβ redex. Correctly,
the machine throws away u and switches to evaluating t (note the change of
phase from N to H).
• Exponential Transition ered : the environment entry associated to x is labeled with (red, n) thus it is useful to substitute t. The idea is that in at
most n additional substitution steps (shuffled with commutative steps) a βredex will be obtained. To avoid variable clashes the substitution α-renames
t.
• Exponential Transition eabs : the environment associates an abstraction to
x and the stack is non empty, so it is useful to substitute the abstraction
(again, α-renaming to avoid variable clashes). Note that if the stack is empty
the machine rather backtracks using Hc3 .
The Max MAM starts executions on initial states of the form (ǫ, t, ǫ, ǫ, H),
where t is such that any two variables (bound or free) have distinct names, and
any other component is empty. A state s is reachable if there are an initial state
s′ and a Max MAM execution ρ : s′ ∗ s, and it is final if no transitions apply.
The theorem of correctness and completeness of the machine with respect
to →Maxβ follows. It rests on a technical development that is in the appendix,
starting at page 20. The bisimulation is weak because transitions other than m
are invisible on the λ-calculus. For a machine execution ρ we denote with |ρ|
(resp. |ρ|x ) the number of transitions (resp. x-transitions for x ∈ {m, e, c, . . .})
in ρ.

10

✩

✪

Theorem 5.1 (Weak Bisimulation, Proof at Page 25). Let s be an initial Max
MAM state of code t.
1. Simulation: for every execution ρ : s
d : s →∗Maxβ s′ such that |d| = |ρ|m ;

∗

s′ there exists a derivation

2. Reverse Simulation: for every derivation d : t →∗Maxβ u there is an execution ρ : s ∗ s′ such that s′ = u and |d| = |ρ|m .

6

Quantitative Analysis

The complexity analysis of the Max MAM is omitted because it follows exactly,
by changing only minimal details, the one for the Useful MAM in [Acc16]. All
the details can be found in the Appendix, starting from page 25.
Let us anyway provide the schema of the analysis. First of all one proves a
subterm invariant, proving that most codes in the state of the Max MAM are
subcodes of the initial code. Then the proof of the polynomial bound of the
overhead is in three steps.
1. Exponential vs Multiplicative Transitions: we bound the number |ρ|e of exponential transitions of an execution ρ using the number |ρ|m of multiplicative
transitions of ρ, that by Theorem 5.1 corresponds to the number of maximal
β-steps on the λ-calculus. The bound is quadratic.
2. Commutative vs Exponential Transitions: we bound the number |ρ|c of commutative transitions of ρ by using the number of exponential transitions and
the size of the initial term. The bound is linear in both quantities.
3. Global bound : we multiply the number of each kind of transition for the cost
of that kind (everything is constant time but for exponential transitions,
that are linear in the size of the initial term), and then sum over the kind of
transitions.
Concretely, one obtains the following theorem.
Theorem 6.1 (Max MAM Overhead Bound, Proof at Page 34). Let d : t →∗Maxβ
u be a maximal derivation and ρ be the Max MAM execution simulating d given
by Theorem 5.1.2. Then:
1. Length: |ρ| = O((1 + |d|2 ) · |t|).
2. Cost: ρ is implementable on RAM in O((1 + |d|2 ) · |t|) steps.

References
[AB17]

Beniamino Accattoli and Bruno Barras. Environments and the complexity of abstract machines. In PPDP 2017, pages 4–16, 2017.

[ABM14]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In ICFP 2014, pages 363–376, 2014.

[ABM15]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A
strong distillery. In APLAS 2015, pages 231–250, 2015.

11

[ABS09]

Zena M. Ariola, Aaron Bohannon, and Amr Sabry. Sequent calculi
and abstract machines. ACM Trans. Program. Lang. Syst., 31(4),
2009.

[AC15]

Beniamino Accattoli and Claudio Sacerdoti Coen. On the relative
usefulness of fireballs. In LICS 2015, pages 141–155, 2015.

[Acc16]

Beniamino Accattoli. The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. In WoLLIC 2016, pages 1–21, 2016.

[Acc17]

Beniamino Accattoli. (In)Efficiency and Reasonable Cost Models.
In LSFA 2017, 2017.

[AG17]

Beniamino Accattoli and Giulio Guerrieri. Implementing open callby-value. In FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised
Selected Papers, pages 1–19, 2017.

[AL16]

Beniamino Accattoli and Ugo Dal Lago. (Leftmost-Outermost)
Beta-Reduction is Invariant, Indeed. LMCS, 12(1), 2016.

[Cré90]

Pierre Crégut. An abstract machine for lambda-terms normalization. In LISP and Functional Programming, pages 333–340, 1990.

[Cré07]

Pierre Crégut. Strongly reducing variants of the Krivine abstract
machine. Higher-Order and Symbolic Computation, 20(3):209–230,
2007.

[DN04]

Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Technical Report RS-04-26, BRICS, 2004.

[DZ13]

Olivier Danvy and Ian Zerny. A synthetic operational account of
call-by-need evaluation. In PPDP, pages 97–108, 2013.

[FGSW07] Daniel P. Friedman, Abdulaziz Ghuloum, Jeremy G. Siek, and Onnie Lynn Winebarger. Improving the lazy Krivine machine. HigherOrder and Symbolic Computation, 20(3):271–293, 2007.
[FS09]

Maribel Fernández and Nikolaos Siafakas. New developments in
environment machines. Electr. Notes Theor. Comput. Sci., 237:57–
73, 2009.

[GL02]

Benjamin Grégoire and Xavier Leroy. A compiled implementation
of strong reduction. In (ICFP ’02)., pages 235–246, 2002.

[GNM13]

Álvaro Garcı́a-Pérez, Pablo Nogueira, and Juan José MorenoNavarro. Deriving the full-reducing krivine machine from the smallstep operational semantics of normal order. In PPDP, pages 85–96,
2013.

[Ses97]

Peter Sestoft. Deriving a lazy abstract machine. J. Funct. Program.,
7(3):231–264, 1997.

[SGM02]

David Sands, Jörgen Gustavsson, and Andrew Moran. Lambda
calculi and linear speedups. In The Essence of Computation, pages
60–84, 2002.
12

[vRSSX99] Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen, and
Hongwei Xi. Perpetual reductions in lambda-calculus. Inf. Comput.,
149(2):173–225, 1999.
[Wan07]

Mitchell Wand. On the correctness of the krivine machine. HigherOrder and Symbolic Computation, 20(3):231–235, 2007.

Proof Appendix
6.1

Proof of the properties of the Maximal Strategy (L.2.2,
p. 3)

Proof. By induction on t. Cases:
• Variable, i.e. t = x. Then t is normal, absurd.
• Abstraction, i.e. t = λx.r. Then by i.h. there exists s such that r →Maxβ s.
By rule (λ), t = λx.r →Maxβ λx.s, i.e. just take u := λx.s. Determinism:
it follows from the i.h.
• Application, i.e. t = rs. Two cases:
– r is an abstraction, i.e. r = λx.p. Two sub-cases:
∗ x ∈ r or s is normal. Then t = (λx.p)s 7→Maxβ p{x s}. Determinism: the rules for Max contexts do not allow to evaluate in r,
because λz.r is applied, nor to evaluate in s (if it is not normal)
because then x ∈ r and so rule (gc) cannot be applied.
∗ x∈
/ r and s is not normal. By i.h. there exists a unique q such
that s →Maxβ q, that is, there is a perpetual context C such that
s = Chs′ i →Maxβ Chq ′ i with s′ 7→Maxβ q ′ . By rule (gc), (λx.p)C is
a Max-context and t = (λx.p)Chs′ i →Maxβ (λx.p)Chq ′ i. Clearly,
there cannot be any →Maxβ redex in r, so determinism holds.
– r is not an abstraction. Two sub-cases:
∗ r is not normal. Then by i.h. there exists unique p such that
r →Maxβ p, By rule (@l), t = rs →Maxβ ps. Since r reduces, it is
not neutral and so there cannot be →Maxβ redexes in s (because
rule (gc)does not apply).
∗ r is normal and thus neutral. Then s is not normal (otherwise
t is normal, absurd). By i.h. there exists unique p such that
s →Maxβ p. By rule (@r), t = rs →Maxβ rp, and since r is neutral
this is the unique →Maxβ redex of t.

6.2

Definition of Grafting and Unfolding, and their Properties

The unfolding of the environment E on a code t is defined as the recursive
capture-allowing substitution (called grafting) of the entries of E on t.

13

Definition 6.2 (Grafting and Environment Unfolding). The operation of grafting t{|x u|} is defined by
(rs){|x u|}
x{|x u|}

:= r{|x u|}s{|x u|}
:= u

(λy.r){|x u|} :=
y{|x u|} :=

λy.r{|x u|}
y

Given an environment E we define the unfolding of E on a code t as follows:
[x u]l ::E

u Er E
λx.u E

x
x

[x u]l ::E ′

t{|x u|}

:=

→

t

ǫ

→

t

:=

→

t

E

or equivalently as:
u
x

E′

x

:=

→

[y u]l ::E ′

:=
:=

→→

→→

E

:=
:=

→→

E

→

→→

(ur)
(λx.u)

E′

ǫ

→

For instance, (λx.y) [y xx]neu = λx.(xx). The unfolding is extended to
contexts as expected (i.e. recursively propagating the unfolding and setting
h·i E = E).
Let us explain the need for grafting. In [ABM15], the Strong MAM is decoded to the LSC, that is a calculus with explicit substitutions, i.e. a calculus
able to represent the environment of the Strong MAM. Matching the representation of the environment on the Strong MAM and on the LSC does not need
grafting but it is, however, a quite technical affair. Useful sharing adds many
further complications in establishing such a matching, because useful evaluation computes a shared representation of the normal form and forces some of
the explicit substitutions to stay under abstractions. The difficulty is such, in
fact, that we found much easier to decode directly to the λ-calculus rather than
to the LSC. Such an alternative solution, however, has to push the substitution
induced by the environment through abstractions, which is why we use grafting.
The following easy properties will be used to prove the correctness of the
machine (in Lemma 6.7).
→

Lemma 6.3 (Properties of Grafting and Unfolding).
1. If the bound names of t do not appear free in u then t{x u} = t{|x u|}.
E}

= t{x u}

E.

→

6.3

u

→

E {x

→

2. If moreover they do not appear free in E then t

Proof of the Commutative Transparency Lemma (L.4.1,
p. 8)

1. Transitions:
• Case (F, tu, π, E, H)
Dhhtiu :: πi.

Hc1

(F, t, u :: π, E, H). We have Dhπhtuii =

• Case (F, λx.t, u :: π, E, H) Hc7 (F :: λx.tπ, u, ǫ, E, H). We have
Dhhλx.tiu :: πi = Dhπh(λx.t)uii = (F :: λx.tπ)hui.
• Case (F, λx.t, ǫ, E, H)
F :: xhti.
• Case (F, x, π, E, H)

Hc2

Hc3

• Case (F :: x, t, ǫ, E, N)

(F :: x, t, ǫ, E, H). We have F hλx.ti =

(F, x, π, E, N). Nothing to prove.
Nc4

(F, λx.t, ǫ, E, N). Exactly as

14

Hc2 .

x

• Case (F :: t♦π, u, ǫ, E, N)
Dhπhtuii.

Nc5

(F, tu, π, E, N). We have (F :: t♦π)hui =

• Case (F, t, u :: π, E, N) Nc6 (F :: t♦π, u, ǫ, E, H). We have Dhhtiu :: πi =
Dhπhtuii = (F :: t♦π)hui.

6.4

E

′

=P.1 F ′ hht iπ ′ i

= s′ .

→

→

2. We have s = F hhtiπi

E

The Checking AM Invariants Lemma (L.6.5, p. 15)

Before the invariants we need a lemma to be used in the proof of the decoding
invariant.
Lemma 6.4. Let C be a context.
1. Right Extension: Ch·i is Max iff Chh·iui is Max;
2. Left Neutral Extension: Ch·i is Max and u is neutral iff Chuh·ii is Max;
3. Abstraction Extension: Ch·i is Max and not applicative iff Chλx.h·ii is
Max.
4. Erasing Redexes Extension: Ch·i is Max and x ∈
/ fv(t) iff Ch(λx.t)h·ii is
Max.
→

5. Unfolding Removal: if C

E

is Max then C is Max.

Proof. By induction on the predicate C is Max (Definition 2.1, page 2).
Now, some terminology:
• A state s is initial if it is of the form (ǫ, t, ǫ, E, H) with E well-labeled, t
well-named and such that the variables abstracted in t do not occur in E.
• A state s is reachable if there are an initial state s′ and a Checking AM
execution ρ : s′ ⇀∗ s.
Finally:
Lemma 6.5 (Checking AM Invariants, Proof at P. 15). Let F | u | π | E | ϕ be
a Checking AM state reachable from an initial state of code t0 . Then
1. Normal Form:
→

(a) Backtracking Code: if ϕ = N, then u
empty, then u E is neutral;

E

is normal, and if π is non-

→

→

(b) Frame: if F = F ′ :: r♦π ′ :: F ′′ , then r

E

is neutral.

2. Subterm:
(a) Evaluating Code: if ϕ = H, then u is a subterm of t0 ;
(b) Stack: any code in the stack π is a subterm of t0 ;
(c) Frame:
i. Head Contexts: if F = F ′ :: r♦π ′ :: F ′′ , then any code in π ′ is a
subterm of t0 ;
15

ii. Erasing Redexes: if F = F ′ :: λx.rπ ′ :: F ′′ , then λx.r and any
code in π ′ are subterms of t0 ;
→

3. Erasing Redexes: if F = F ′ :: λx.rπ ′ :: F ′′ then x does not occur in E,
x∈
/ fv(r), and x ∈
/ fv(r E ).
4. Decoding: Cs is a Max context.
Proof.
1. Normal Form: the invariant trivially holds for an initial state ǫ | t | ǫ |
E | H. For a non-empty evaluation sequence we list the cases for the last
transition. We omit Hc1 because it follows immediately from the i.h.
• Case (F, λx.t, ǫ, E, H)

Hc2

(F :: x, t, ǫ, E, H).

(a) Backtracking Code: trivial since ϕ 6= N.
(b) Frame: it follows by the i.h., since the transition only extends F
with an item that is not a head context.
• Case (F, λx.t, u :: π, E, H)
fv(t).

Hc7

/
(F :: λx.tπ, u, ǫ, E, H) with x ∈

(a) Backtracking Code: trivial since ϕ 6= N.
(b) Frame: it follows by the i.h., since the transition only extends F
with an item that is not a head context.
• Case (F, x, π, E, H) Hc3 (F, x, π, E, N) with E(x) = ⊥ or E(x) =
[x u]neu or (E(x) = [x u]abs and π = ǫ).
→

(a) Backtracking Code: three cases depending on E:
i. E(x) = ⊥: then x E = x, that is both a normal and a
neutral term.
ii. E(x) = [x u]neu : more precisely E = E1 :: [x u]neu :: E2 .
Then we have x E = x E1 ::[x u]neu ::E2 = x [x u]neu ::E2 =
u E2 that is a neutral term because E is well-labeled. Note
that E1 cannot bound x because of the freshness requirements in the definition of well-labeled environment.
iii. E(x) = [x u]abs and π = ǫ: similarly to the previous case
we obtain that x E is a normal abstraction.
(b) Frame: it follows from the i.h., as F is unchanged.
→

→

→

→

→

• Case (F :: x, t, ǫ, E, N)

(F, λx.t, ǫ, E, N).

Nc4

→

(a) Backtracking Code: by i.h. we know that t E is a normal term.
Then (λx.t) E = λx.t E is a normal term. The stack is empty,
so we conclude.
(b) Frame: it follows from the i.h., as F is unchanged.
→

→

• Case (F :: t♦π, u, ǫ, E, N)

Nc5

(F, tu, π, E, N).
→

(a) Backtracking Code: by i.h. we have that u E is a normal term
while by Point 1b of the i.h. t E is a neutral term. Therefore
(tu) E = t E u E is a neutral term.
(b) Frame: it follows from the i.h., as F is unchanged.
→

→

→

→

• Case (F, t, u :: π, E, N)

Nc6

(F :: t♦π, u, ǫ, E, H).

16

→

(a) Backtracking Code: trivial since ϕ 6= N.
(b) Frame: t E is a neutral term by Point 1a of the i.h., the rest
follows from the i.h.
2. Subterm: This is a special case of the more refined subterm invariant of
the Max MAM (Lemma 6.9.1, page 26).

→

3. Erasing Redexes: the invariant trivially holds for an initial state ǫ | t |
ǫ | E | H. For a non-empty evaluation sequence, for all transitions
but Hc7 the statement follows immediately from the i.h. because they
all leave untouched the erasing redex items in the frame. So consider
(F, λx.r, u :: π, E, H)
Hc7 (F :: λx.rπ, u, π, E, H). By the hypothesis on the transition, we have x ∈
/ fv(r). By the subterm invariant
(Lemma 6.5.2a), λx.r is a subterm of the initial term and so, by the hypotheses on initial states, x does not occur in E. Last, since x does not
occur in E nor in r, clearly it does not occur in r E .

→

4. Decoding: the invariant trivially holds for an initial state ǫ | t | ǫ | E | H.
For a non-empty evaluation sequence we list the cases for the last transition. To simplify the reasoning in the following case analysis we let implicit
that the unfolding spreads on all the subterms, i.e. that Dhhtiπi E =
F E hht E iπ E i. Cases:
→

→

→

→

→

• Case s′ = (F, tu, π, E, H) Hc1 (F, t, u :: π, E, H) = s. By Lemma 6.4.1,
Cs = Dhh·iu :: πi E is Max iff Cs′ = Dhh·iπi E is Max, and Cs′ is
Max by i.h.

→

→

→

→

/
• Case (F, λx.r, u :: π, E, H) Hc7 (F :: λx.rπ, u, ǫ, E, H) with x ∈
fv(t).
By i.h., Cs′ = F hh·iu :: πi E = F E hh·iu E :: π E i is Max, and by
Lemma 6.4.1 F E hh·iπ E i is Max. By the erasing redexes invariant (Lemma 6.5.3), we have x ∈
/ fv(r E ). Then by Lemma 6.4.4
F E hh(λx.r E )h·iiπ E i = F hh(λx.r)h·iiπi E = Cs′ is Max.
→

→

→

→

→

→

→

→

→

• Case s′ = (F, λx.t, ǫ, E, H) Hc2 (F :: x, t, ǫ, E, H) = s. We have
Cs = Dhλx.h·ii E and by i.h. we know that Dh·i E = Cs′ is Max.
Note that by definition the decoding of frames cannot be applicative.
Then Cs is Max by Lemma 6.4.3.

→

• Case s′ = (F, x, π, E, H) Hc3 (F, x, π, E, N) = s with E(x) = ⊥
or E(x) = [x u]neu or (E(x) = [x u]abs and π = ǫ). We have
Cs = Dhh·iπi E = Cs′ , and so the statement follows immediately
from the i.h.
→

→

• Case s′ = (F :: x, t, ǫ, E, N) Nc4 (F, λx.t, ǫ, E, N) = s.
We have Cs = Dh·i E and by i.h. we know that Dhλx.h·ii
is Max. Then Cs is Max by Lemma 6.4.3.

E

= Cs′

→

→

• Case s′ = (F :: t♦π, u, ǫ, E, N) Nc5 (F, tu, π, E, N) = s. By i.h.
Cs′ = Dhhth·iiπi E is Max, and so by Lemma 6.4.2 Dhh·iπi E = Cs
is Max.

17

→

→

→

• Case s′ = (F, t, u :: π, E, N) Nc6 (F :: t♦π, u, ǫ, E, H) = s. By
i.h. Cs′ = Dhh·iπi E = F E hh·iπ E i is Max, and by Lemma 6.5.1a

→

applied to s′ we obtain that t E is neutral (because the stack is nonempty). So by Lemma 6.4.2 F E hht E h·iiπ E i = F hhth·iiπi E = Cs
is Max.
→

→

→

→

6.5

Proof of the Checking AM Properties Theorem (Thm 4.3,
p. 9)

Proof.
1. An inspection of the transition rules shows that there always is one and
exactly one transition of the Checking AM that applies: for each phase (H
and N) consider each case of the code (application, abstraction, variable)
and the various combinations stack/frame.
2. By the previous point, the executions of the Checking AM are sequences
of commutative steps that either diverge or are followed by an output
transition. We now introduce a measure and prove that the sequence of
commutative steps is always finite. In particular, it is bounded by the size
of the initial term.
Consider the following notion of size for stacks, frames, and states:
|ǫ| :=
|t :: π| :=
|(F, t, π, E, H)| :=

0
|t| + |π|
|F | + |π| + |t|

|F :: x|
|F :: t♦π|
|F :: λx.tπ|
|(F, t, π, E, N)|

:=
:=
:=
:=

|F |
|π| + |F |
|t| + |π| + |F |
|F | + |π|

The proof of the bound is in 3 steps:
(a) Evaluation Commutative Steps Are Bound by the Size of the Initial
Term.
By direct inspection of the rules of the machine it can be checked
that:
′
• Evaluation Commutative Rules Decrease the Size: if s
a s
with a ∈ {Hc1 , Hc2 , Hc3 , Hc7 } then |s′ | < |s|;
• Backtracking Transitions do not Change the Size: if s a s′ with
a ∈ {Nc4 , Nc5 , Nc6 } then |s′ | = |s|.

Then a straightforward induction on the length of an execution ρ
shows that
|s′ | ≤ |s| − |ρ|Hc
i.e. that |ρ|Hc ≤ |s| − |s′ | ≤ |s| = |(ǫ, t, ǫ, E, H)| = |t|.
(b) Backtracking Commutative Steps Are Bound by the Evaluation Ones.
We have to estimate |ρ|Nc = |ρ|Nc4 + |ρ|Nc5 + |ρ|Nc6 . Note that
i. |ρ|Nc4 ≤ |ρ|Hc2 , as
Nc4 ;
ii. |ρ|Nc5 ≤ |ρ|Nc6 , as
Nc6 ;

Nc4

pops variables from F , pushed only by

Nc5

pops pairs t♦π from F , pushed only by

18

iii. |ρ|Nc6 ≤ |ρ|Hc3 , as
by Hc3 .

ends backtracking phases, started only

Nc6

Then |ρ|Nc ≤ |ρ|Hc2 + 2|ρ|Hc3 ≤ 2|ρ|Hc .
(c) Bounding All Commutative Steps by the Size of the Intial Term. We
have |ρ|c = |ρ|Hc + |ρ|Nc ≤P.2 = |ρ|Hc + 2|ρ|Hc ≤P.1 3 · |t|.

→

3. By the previous points executions of the Checking AM are sequences of
commutative transitions followed by an output transition, i.e. they have
the form s ⇀∗c s′ ⇀o l where l is the output label of the machine. The
initial state by hypothesis is s := (ǫ, t, , E, H). Since commutative transitions do not change the decoding (Lemma 4.1), we have s′ = s = t E . To
prove that [x t]l :: E is well-labeled—that requires to prove properties of
t E —we will then look at s′ and at the various possible output transitions.
Five cases:
→

• s′ = (F, λy.r, u :: π, E, H) ⇀o1 (red, 1) with y ∈ fv(r). Then
E hh(λy.r E )u E iπ E i

→

that has a β-redex.
Now, we show that t decomposes as a 7→Maxβ -redex in a Max context. By Lemma 6.5.4, F hh·iu :: πi E = Cs′ is a Max context. By
Lemma 6.4.5, F hh·iu :: πi is also Max. Then F hh·iπi is Max by
Lemma 6.4.1. Moreover, (λy.r)u is a 7→Maxβ redex because y ∈ fv(r)
by hypothesis. Finally, t = F hh(λy.r)uiπi by Lemma 4.1.1.
The Checking AM is executed only on terms that are not variables,
and so [x t](red,1) :: E is well-labeled.
• s′ = (F, y, π, E, H) ⇀o2 (red, n + 1) with E(y) = [y u](red,n) . Then
=F

E hhy E iπ E i

→

E

→

= s′ = F hhyiπi

→

E

→

→

t

→

Since E is well-labeled and E(y) = [y u](red,n) we have that y E
contains a β-redex, and so does t E .
Now, we show that t decomposes as a variable in a Max context. By
Lemma 6.5.4, F hh·iπi E = Cs′ is a Max context. By Lemma 6.4.5,
F hh·iπi is also Max. Finally, t = F hhyiπi by Lemma 4.1.1.
Therefore [x t](red,n+1) :: E is well-labeled.
→

→

• s′ = (F, y, u :: π, E, H) ⇀o3 (red, 2) with E(y) = [y u]abs . Then
=F

E hhy E u E iπ E i

→

E

→

= F hhyuiπi

→

E

→

= s′ = F hhyiu :: πi

→

E

→

→

t

→

Since E is well-labeled and E(y) = [x u]abs we have that y E is an
abstraction and so t E contains the β-redex y E u E .
Now, we show that t decomposes as a variable in an applicative Max
context. By Lemma 6.5.4, F hh·iu :: πi E = Cs′ is a Max context. By
Lemma 6.4.5, F hh·iu :: πi is also Max. Additionally, it is applicative.
Finally, t = F hhyiu :: πi by Lemma 4.1.1.
Therefore [x t](red,2) :: E is well-labeled.
→

→

→

→

19

→

=F

E

→

= F hh(λy.r)uiπi

→

E

→

= s′ = F hhλy.riu :: πi

→

E

→

→

t

→→

→

→→

• s′ = (ǫ, ur, ǫ, E, N) ⇀o4 neu. Then t = ur by the commutative
transparency lemma (Lemma 4.1.1), and so t is an application. By
the normal form invariant (Lemma 6.5.1a), t E = (ur) E is normal.
Moreover, it is an application, because (ur) E = u E r E , and so it
is neutral. Then [x t]neu :: E is well-labeled.

→

→

• s′ = (ǫ, λy.u, ǫ, E, N) ⇀o5 abs. Then t = λy.u by the commutative
transparency lemma (Lemma 4.1.1), and so t is an abstraction. By
the normal form invariant (Lemma 6.5.1a), t E = (λy.u) E is normal. Moreover, it is an abstraction, because (λy.u) E = λy.u E .
Then [x t]abs :: E is well-labeled.
→

→

• s′ = (F :: λy.rπ, u, ǫ, E, N) ⇀o6 (red, 1). Then
→

E hh(λy.r E )u E iπ E i

=F

→

E

→

= s′ = F hh(λy.r)uiπi

→

E

→

→

t

→

that has a β-redex.
Now, we show that t decomposes as a 7→Maxβ -redex in a Max context. By Lemma 6.5.4, F hh(λy.r)h·iiπi E = Cs′ is a Max context. By Lemma 6.4.5, F hh(λy.r)h·iiπi is also Max. Then F hh·iπi
is Max by Lemma 6.4.1. Moreover, by the normal form invariant
(Lemma 6.5.1a) u is normal and by the erasing redexes invariant
(Lemma 6.5.3) y does not occur in r. Then (λy.r)u is a 7→Maxβ redex.
Finally, t = F hh(λy.r)uiπi by Lemma 4.1.1.
The Checking AM is executed only on terms that are not variables,
and so [x t](red,1) :: E is well-labeled.

6.6

Useful MAM Qualitative Study (L.6.6, p. 20)

Four invariants are required. The normal form and decoding invariants are
exactly those of the Checking AM (and the proof for the commutative transitions
is the same). The environment labels invariant follows from the correctness of
the Checking AM (Theorem 4.3.2). The name invariant is used in the proof of
Lemma 6.7.
Lemma 6.6 (Max MAM Qualitative Invariants, Proof at Page 20). Let s =
F | u | π | E | ϕ be a state reachable from an initial term t0 . Then:
1. Environment Labels: E is well-labeled.
2. Normal Form:
→

(a) Backtracking Code: if ϕ = N, then u
empty, then u E is neutral;

E

is normal, and if π is non-

→

→

(b) Frame: if F = F ′ :: r♦π ′ :: F ′′ , then r

E

is neutral.

3. Name:
(a) Substitutions: if E = E ′ :: [x t] :: E ′′ then x is fresh wrt t and E ′′ ;
(b) Abstractions and Evaluation: if ϕ = H and λx.t is a subterm of u,
π, or π ′ (if F = F ′ :: r♦π ′ :: F ′′ ) or of a erasing redex item in F
then x may occur only in t;
20

(c) Abstractions and Backtracking: if ϕ = N and λx.t is a subterm of π
or π ′ (if F = F ′ :: r♦π ′ :: F ′′ ) or of a erasing redex item in F then
x may occur only in t.
E.

→

/ r and x ∈
/r
4. Erasing Redexes: if F = F ′ :: λx.rπ ′ :: F ′′ , then x ∈
5. Decoding: Cs is a Max context.
Proof.

1. Environment Labels: the only transition that extends the environment is
m2 , and it preserves well-labeledness by Theorem 4.3.3.
2. Normal Form: for the commutative transitions the proof is exactly as
for the Checking AM, see Lemma 6.5.1 whose proof is at page 15. For
the multiplicative and exponential transitions the invariant holds trivially:
the backtracking code part because these transition cannot happen during
backtracking (note that m3 may happen during backtracking but it ends
in a evaluating state, for which then nothing has to be proven), and the
frame part because they do not touch the head context items in the frame.
3. Name: the invariant trivially holds for an initial state ǫ | t | ǫ | ǫ | H. For
a non-empty evaluation sequence we list the cases for the last transition.
• Principal Cases:
– Case s′ = (F, λx.t, y :: π, E, H) m1 (F, t{x y}, π, E, H) = s.
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows from the i.h.
– Case s′ = (F, λx.t, u :: π, E, H) m2 (F, t, π, [x u]l :: E, H) = s
with u not a variable and x ∈ fv(t).
(a) Substitution: it follows from the i.h. for abstractions in the
evaluation phase (Point 3b).
(b) Abstractions and Evaluation: it follows from the i.h.
α
– Case s′ = (F, x, π, E, H) ered (F, t , π, E, H) = s with E(x) =
[x u](red,n) .
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows by the i.h. and the
α
fact that in t the abstracted variables are renamed (wrt t)
with fresh names.
α
– Case s′ = (F, x, u :: π, E, H) eabs (F, t , u :: π, E, H) = s with
abs
E(x) = [x u] .
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows by the i.h. and the
α
fact that in t the abstracted variables are renamed (wrt t)
with fresh names.
– Case (F :: λx.tπ, u, ǫ, E, N) m3 (F, t, π, E, H).
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows by the i.h.
• Commutative Cases:
21

– Case s′ = (F, tu, π, E, H) Hc1 (F, t, u :: π, E, H) = s.
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows from the i.h.
– Case (F, λx.r, u :: π, E, H) Hc7 (F :: λx.rπ, u, ǫ, E, H) with
x∈
/ fv(t).
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows from the i.h.
– Case s′ = (F, λx.t, ǫ, E, H) Hc2 (F :: x, t, ǫ, E, H) = s.
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows from the i.h.
– Case s′ = (F, x, π, E, H) Hc3 (F, x, π, E, N) = s with E(x) =
⊥ or E(x) = [x u]neu or (E(x) = [x u]abs and π = ǫ) .
(a) Substitution: it follows from the i.h.
3. Abstractions and Backtracking: it follows from the i.h. of
Abstraction and Evaluation (Point 3b).
– Case s′ = (F :: x, t, ǫ, E, N) Nc4 (F, λx.t, ǫ, E, N) = s.
(a) Substitution: it follows from the i.h.
3. Abstractions and Backtracking: it follows from the i.h.
– Case s′ = (F :: t♦π, u, ǫ, E, N) Nc5 (F, tu, π, E, N) = s.
(a) Substitution: it follows from the i.h.
3. Abstractions and Backtracking: it follows from the i.h.
– Case s′ = (F, t, u :: π, E, N) Nc6 (F :: t♦π, u, ǫ, E, H) = s.
(a) Substitution: it follows from the i.h.
(b) Abstractions and Evaluation: it follows from the i.h. for
Abstractions and Backtracking (Point 3c)

→

4. Erasing: the invariant trivially holds for an initial state ǫ | t | ǫ | ǫ |
H. For a non-empty evaluation sequence, for all transitions but Hc7
the statement follows immediately from the i.h. because they all leave
untouched the erasing redex items in the frame (but for m3 that, however,
simply removes one such entry and so trivially preserves the invariant).
So consider (F, λx.r, u :: π, E, H) Hc7 (F :: λx.rπ, u, π, E, H). By the
hypothesis on the transition, we have x ∈
/ fv(r). By the name invariant
(Lemma 6.6.3b), x does not occur in E. Last, since x does not occur in
E nor in r, clearly it does not occur in r E .

→

5. Decoding: the invariant trivially holds for an initial state ǫ | t | ǫ | ǫ | H.
For a non-empty evaluation sequence we list the cases for the last transition. To simplify the reasoning in the following case analysis we let implicit
that the unfolding spreads on all the subterms, i.e. that Dhhtiπi E =
F E hht E iπ E i.
→

→

→

• Principal Cases:

22

→

→

– Case s′ = (F, λx.t, y :: π, E, H) m1 (F, t{x y}, π, E, H) = s.
By Lemma 6.4.1, Cs = Dhh·iπi E is Max iff Cs′ = Dhh·iy :: πi
is Max, and Cs′ is Max by i.h.

E

→

– Case s′ = (F, λx.t, u :: π, E, H) m2 (F, t, π, [x u]l :: E, H) = s
with x ∈ fv(t).
We have to prove that Cs′ = Dhh·iπi [x u]l ::E is Max. By the
name invariant for abstractions (Lemma 6.6.3b) we have that x
does not occur in F nor π, and so Dhh·iπi [x u]l ::E = Dhh·iπi E .
Now, by Lemma 6.4.1 Dhh·iπi E is Max iff Dhh·iu :: πi E is Max,
that holds by i.h., because this is exactly Cs′ .
α
– Case s′ = (F, x, π, E, H) ered (F, t , π, E, H) = s with E(x) =
[x u](red,n) . We have Cs = Dhh·iπi E = Cs′ , and so the statement follows immediately from the i.h.
α
– Case s′ = (F, x, u :: π, E, H) eabs (F, t , u :: π, E, H) = s with
abs
E(x) = [x u] . We have Cs = Dhh·iπi E = Cs′ , and so the
statement follows immediately from the i.h.
– Case s′ = (F :: λx.tπ, u, ǫ, E, N) m3 (F, t, π, E, H) = s.
We have Cs = Dhh·iπi E = F E hht E iπ E i. By the erasing redexes invariant (Lemma 6.6.4), x ∈
/ r E . Then, by Lemma 6.4.4
Cs is Max if and only if F E hh(λx.r E )h·iiπ E i = F hh(λy.r)h·iiπi
Cs′ is Max, that holds by i.h.
→

→

→

→

→

→

→

→

→

→

→

→

→

→

→

E

=

• Commutative Cases: exactly as in the proof of Lemma 6.5.4.

We can now show how every single transition projects on the λ-calculus, and
in particular that multiplicative transitions project to Max β-steps.
Lemma 6.7 (One-Step Weak Simulation). Let s be a reachable state.
1. Commutative: if s

c1,2,3,4,5,6,7

2. Exponential: if s

eabs,red

3. Multiplicative: if s

m1,2,3

s′ then s = s′ ;

s′ then s = s′ ;
s′ then s →Maxβ s′ .

Proof.
1. Commutative: the proof is exactly as the one for the Checking AM (Lemma 4.1.2),
that can be found at page 15.
2. Exponential :
α

• Case s = (F, x, π, E, H) ered (F, t , π, E, H) = s′ with E(x) =
[x t](red,n) . Then E = E ′ :: [x t](red,n) :: E ′′ for some environments E ′ , and E ′′ . Remember that terms are considered up to αequivalence.
Ei

=

Cs′ ht

E ′′ i

= Cs′ ht

Ei

→

Cs′ hx

→

=

→

s

= s′

α

→

→

In the chain of equalities we can replace t E ′′ with t E because by
well-labeledness the variables bound by E ′ are fresh with respect to
t.
• Case s = (F, x, u :: π, E, H) eabs (F, t , u :: π, E, H) = s′ with
E(x) = [x t]abs . The proof that s = s′ is exactly as in the previous
case.
23

3. Multiplicative:
→

• Case s = (F, λx.t, y :: π, E, H) m1 (F, t{x y}, π, E, H) = s′ . Note
that Cs′ = Dhπi E is Max by the decoding invariant (Lemma 6.6.5).
Note also that by the name invariant (Lemma 6.6.3b) x can only
occur in t. Then:
(F, λx.t, y :: π, E, H) =
=
=
→Maxβ
=L.6.6.3b&L.6.3.2
=

→

F hhλx.tiy :: πi E
F hh(λx.t)yiπi E
Cs′ h(λx.t E )y E i
Cs′ ht E {x y E }i
Cs′ ht{x y} E i
(F, t{x y}, π, E, H)
→→→

→

→

→

→

→

l
′
• Case s = (F, λx.t, u :: π, E, H)
m2 (F, t, π, [x u] :: E, H) = s
with u not a variable. By the name invariant (Lemma 6.6.3b) x
can only occur in t and so Cs′ = Dhh·iπi [x u]l ::E = Dhh·iπi E =
F E hh·iπ E i. Moreover, such a context is Max by the decoding
invariant (Lemma 6.6.5). Then:

→

→

=
=
=
→Maxβ
=L.6.6.3b&L.6.3.2
=
=L.6.6.3b&L.6.3.1
=L.6.6.3b
=
=

F hhλx.tiu :: πi E
F hh(λx.t)uiπi E
F E hh(λx.t E )u E iπ E i
F E hht E {x u E }iπ E i
F E hht{x u} E iπ E i
F hht{x u}iπi E
F hht{|x u|}iπi E
F hhtiπi{|x u|} E
F hhtiπi [x u]l ::E
(F, t, π, [x u]l :: E, H)
→→

(F, λx.t, u :: π, E, H)

→→

→→

→

→

→ →→→

→

→→→

→

→

F hh(λx.t)uiπi E
F E hh(λx.t E )u
F E hht E iπ E i
Dhhtiπi E

→

E iπ E i

→

→→

→→

→→

(F :: λx.tπ, u, ǫ, E, N) =
=
→Maxβ
=

→

→

→

• Case s = (F :: λx.tπ, u, ǫ, E, N) m3 (F, t, π, E, H) = s′ .
Note that Cs′ = Dhh·iπi E = F E hh·iπ E i is Max by the decoding
invariant (Lemma 6.6.5). Then:

=

(F, t, π, E, H)

We also need to show that the Max MAM computes β-normal forms.
Lemma 6.8 (Progress). Let s be a reachable final state. Then s is β-normal.

→

Proof. A simple inspection of the machine transitions shows that final states
have the form (ǫ, t, ǫ, E, N). Then by the normal form invariant (Lemma 6.6.2a)
s = t E is β-normal.

24

6.7

Proof of the Weak Bisimulation Theorem (Thm 5.1,
p. 10)

Proof.
1. By induction on the length |ρ| of ρ, using the one-step weak simulation
lemma (Lemma 6.7). If ρ is empty then the empty derivation satisfies the
statement. If ρ is given by σ : s ∗ s′′ followed by s′′
s′ then by i.h.
∗
′′
′′
′
there exists e : s →Maxβ s s.t. |e| = |σ|m . Cases of s
s:
(a) Commutative or Exponential. Then s′′ = s′ by Lemma 6.7.1 and
Lemma 6.7.2, and the statement holds taking d := e because |d| =
|e| =i.h. |σ|m = |ρ|m .
(b) Multiplicative. Then s′′ →Maxβ s′ by Lemma 6.7.3 and defining d as
e followed by such a step we obtain |d| = |e| + 1 =i.h. |σ|m + 1 = |ρ|m .
2. We use nfec (s) to denote the normal form of s with respect to exponential
and commutative transitions, that exists and is unique because c ∪ e
terminates (termination is given by forthcoming Theorem 6.12 and Theorem 6.14, that are postponed because they actually give precise complexity
bounds, not just termination) and the machine is deterministic (as it can
be seen by an easy inspection of the transitions). The proof is by induction on the length of d. If d is empty then the empty execution satisfies
the statement.
If d is given by e : t →∗Maxβ r followed by r →Maxβ u then by i.h. there
is an execution σ : s ∗ s′′ s.t. r = s′′ and |σ|m = |e|. Note that since
exponential and commutative transitions are mapped on equalities, σ can
be extended as σ ′ : s ∗ s′′ ∗ered ,eabs ,c1,2,3,4,5,6 nfec (s′′ ) with nfec (s′′ ) = r
and |σ ′ |m = |e|. By the progress property (Lemma 6.8) nfec (s′′ ) cannot be
a final state, otherwise r = nfec (s′′ ) could not reduce. Then nfec (s′′ ) m
s′ (the transition is necessarily multiplicative because nfec (s′′ ) is normal
with respect to the other transitions). By the one-step weak simulation
lemma (Lemma 6.7.3) nfec (s′′ ) = r →Maxβ s′ and by determinism of →Maxβ
(Lemma 2.2.2) s′ = u. Then the execution ρ defined as σ ′ followed by
nfec (s′′ ) m s′ satisfy the statement, as |ρ|m = |σ ′ |m + 1 = |σ|m + 1 =
|e| + 1 = |d|.

6.8

Quantitative Analysis

The complexity analyses of this section rely on two additional invariants of the
Max MAM, the subterm and the environment size invariants.
The subterm invariant bounds the size of the duplicated subterms and it is
crucial. For us, u is a subterm of t if it does so up to variable names, both free
and bound. More precisely: define t− as t in which all variables (including those
appearing in binders) are replaced by a fixed symbol ∗. Then, we will consider
u to be a subterm of t whenever u− is a subterm of t− in the usual sense. The
key property ensured by this definition is that the size |u| of u is bounded by
|t|.

25

Lemma 6.9 (Max MAM Quantitative Invariants). Let s = F | u | π | E | ϕ be
a state reachable by the execution ρ from the initial code t0 .
1. Subterm:
(a) Evaluating Code: if ϕ = H, then u is a subterm of t0 ;
(b) Stack: any code in the stack π is a subterm of t0 ;
(c) Frame:
i. Head Contexts: if F = F ′ :: r♦π ′ :: F ′′ , then any code in π ′ is a
subterm of t0 ;
ii. Erasing Redexes: if F = F ′ :: λx.rπ ′ :: F ′′ , then λx.r and any
code in π ′ are subterms of t0 ;
(d) Global Environment: if E = E ′ :: [x r]l :: E ′′ , then r is a subterm
of t0 ;
2. Environment Size: the length of the global environment E is bound by |ρ|m .
Proof.
1. Subterm: the invariant trivially holds for the initial state ǫ | t0 | ǫ |
ǫ | H. In the inductive case we look at the last transition:
• Principal Cases:
– Case s′ = (F, λx.t, y :: π, E, H)

m1

(F, t{x y}, π, E, H) = s.

(a) Evaluating Code: note that according to our definition of
subterm t{x y} is a subterm of λx.t.
(b) Stack : note that any piece code in π is also in u :: π.
(c) Frame: it follows from the i.h., since F is not modified.
(d) Environment : it follows from the i.h., since E is not modified.
– Case s′ = (F, λx.t, u :: π, E, H) m2 (F, t, π, [x u]l :: E, H) = s
with u not a variable.
(a)
(b)
(c)
(d)

Evaluating Code: note that t is a subterm of λx.t.
Stack : note that any piece code in π is also in u :: π.
Frame: it follows from the i.h., since F is not modified.
Environment : the new environment is of the form [x u]l ::
E. Pieces of code in E are subterms of t0 by i.h.. Moreover
u is the top of the stack u :: π so it is also a subterm of t0 .
α
– Case s′ = (F, x, π, E, H) ered (F, t , π, E, H) = s with E(x) =
(red,n)
[x u]
.
(a) Evaluating Code: note that t is bound by E. By i.h., it is a
α
subterm of t0 . So t is also a subterm of t0 .
(b) Stack : it follows from the i.h., since the stack π is unchanged.
(c) Frame: it follows from the i.h., since the frame F is unchanged.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
α
– Case s′ = (F, x, u :: π, E, H) eabs (F, t , u :: π, E, H) = s with
abs
E(x) = [x u] .
26

(a) Evaluating Code: note that t is bound by E. By i.h., it is a
α
subterm of t0 . So t is also a subterm of t0 .
(b) Stack : it follows from the i.h., since the stack u :: π is unchanged.
(c) Frame: it follows from the i.h., since the frame F is unchanged.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
– Case s = (F :: λx.tπ, u, ǫ, E, N) m3 (F, t, π, E, H) = s′ .
(a) Evaluating Code: by the frame part of the i.h. λx.t is a
α
subterm of t0 , and so is t. So t is also a subterm of t0 .
(b) Stack : by the frame part of the i.h. the codes in π are
subterms of t0 .
(c) Frame: it follows from the i.h.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
• Commutative Cases:
– Case s′ = (F, tu, π, E, H) Hc1 (F, t, u :: π, E, H) = s.
(a) Evaluating Code: by i.h., tu is a subterm of t0 , so t is also a
subterm of t0 .
(b) Stack : by i.h., tu is a subterm of t0 , so u is also a subterm
of t0 . Moreover, any piece of code in π is a subterm of t0 by
i.h..
(c) Frame: it follows from the i.h., since the frame F is unchanged.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
– Case s′ = (F, λx.t, u :: π, E, H)
s.

Hc7

(F :: λx.tπ, u, ǫ, E, H) =

(a) Evaluating Code: by i.h., λx.t is a subterm of t0 , so t is also
a subterm of t0 .
(b) Stack : nothing to prove.
(c) Frame: for all entries in F it follows from the i.h., for the
new entry it follows by the evaluating code and stack part of
the i.h.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
– Case s′ = (F, λx.t, ǫ, E, H) Hc2 (F :: x, t, ǫ, E, H) = s.
(a) Evaluating Code: note that t is a subterm of λx.t which is
in turn a subterm of t0 by i.h..
(b) Stack : trivial since the stack π is empty.
(c) Frame: any pair of the form u♦π ′ or λx.uπ ′ in the frame
x :: F is also already present in F , so it follows by the i.h.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
27

– Case s′ = (F, x, π, E, H) Hc3 (F, x, π, E, N) = s with E(x) =
⊥ or E(x) = [x u]neu or (E(x) = [x u]abs and π = ǫ) .
(a) Evaluating Code: trivial since ϕ 6= H.
(b) Stack : it follows from the i.h., since the stack π is unchanged.
(c) Frame: it follows from the i.h., since the frame F is unchanged.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
– Case s′ = (F :: x, t, ǫ, E, N) Nc4 (F, λx.t, ǫ, E, N) = s.
(a) Evaluating Code: trivial since ϕ 6= H.
(b) Stack : trivial since the stack is empty.
(c) Frame: any pair of the form u♦π or λx.uπ ′ in the frame F
is also in the frame x :: F , so it follows from the i.h..
(d) Environment : any substitution of the form [y u] in the environment Nx :: E is also in the environment E, so u is a
subterm of t0 by i.h..
– Case s′ = (F :: t♦π, u, ǫ, E, N) Nc5 (F, tu, π, E, N) = s.
(a) Evaluating Code: trivial since ϕ 6= H.
(b) Stack : the stack π occurs at the left-hand side in the frame
t♦π :: F , so by i.h. we know that any piece of code in π is a
subterm of t0 .
(c) Frame: any pair r♦π or λx.uπ ′ in the frame F is also in
the frame t♦π :: F , so it follows from the i.h.
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
– Case s′ = (F, t, u :: π, E, N) Nc6 (F :: t♦π, u, ǫ, E, H) = s.
(a) Evaluating Code: note that u is an element of the stack at
the left-hand side of the transition, so by i.h. u is a subterm
of t0 .
(b) Stack : trivial since the stack is empty.
(c) Frame: any pair in the frame t♦π :: F or λx.uπ ′ is also in
the frame F except for t♦π. Consider a piece of code s in
the stack π. It is trivially also a piece of code in the stack
u :: π, so by the second point of the i.h. we have that s is a
subterm of t0 .
(d) Environment : it follows from the i.h., since the environment
E is unchanged.
2. Environment Size: simply note that the only transition that extends the
environment is m2 .
The proof of the polynomial bound of the overhead is in three steps. First,
we bound the number |ρ|e of exponential transitions of an execution ρ using
the number |ρ|m of multiplicative transitions of ρ, that by Theorem 5.1 corresponds to the number of Max β-steps on the λ-calculus. Second, we bound the
number |ρ|c of commutative transitions of ρ by using the number of exponential
transitions and the size of the initial term. Third, we put everything together.
28

Multiplicative vs Exponential Analysis This step requires two auxiliary
lemmas. The first one essentially states that commutative transitions eat normal
and neutral terms, as well as Max contexts.
Lemma 6.10. Let s = F | t | π | E | H be a state and E be well-labeled. Then
E

is a normal term and π = ǫ then s

2. If t

E

is a neutral term then s

→ →

1. If t

∗
c

∗
c

F | t | π | E | N.

F | t | π | E | N.

→

3. If t = Chui with C E a Max context then there exist F ′ and π ′ such
that s ∗c F ′ | u | π ′ | E | H. Moreover, if C is applicative then π ′ is
non-empty.
The first two points rest on the following inductive mutually inductive definition of normal and neutral terms:
x is neutral

t is neutral
u is normal
tu is neutral

t is neutral
t is normal

t is normal
λx.t is normal

And the following two immediate properties:
E

is normal then t is normal;

2. If t

E

is neutral then t is neutral.

→ →

1. If t

Now we can proceed with the proof.
Proof.
→

1. If t E is normal then t is normal. By induction on the derivation of t is
normal. Cases:
→

• Neutral, i.e. t is neutral. If t E is neutral then it follows by Point 2.
Otherwise t = x and t E is an abstraction, i.e. E = E ′ :: [x u]abs ::
E ′′ . Then:
F | x | ǫ | E | H Hc3 F | x | ǫ | E | N
→

→

→

• Abstraction, i.e. t = λx.u with u normal. Since t E = λx.u E is
normal then u E is normal and we can use the i.h. on it. Then
→

F | λx.u | ǫ | E | H
(i.h.)

F :: x | u | ǫ | E | H
F :: x | u | ǫ | E | N

Hc2
∗
c

Hc2

F | λx.u | ǫ | E | N

→

2. If t E is neutral then t is neutral. By induction on the derivation of t is
neutral. Cases:
→

• Variable, i.e. t = x. If t E is neutral then either E(x) = ⊥ or
E = E ′ :: [x u]neu :: E ′′ . In both cases:
F |x|π|E|H

29

Hc3

F |x|π|E|N

→

• Application, i.e. t = ur with u neutral and r normal. Since ur E is
neutral, u E is neutral and r E is normal, so that we can use Point
1 and the i.h. on them. Then
→

→

F | ur | π | E | H
(i.h.)

Hc1
∗
c

(Point 1)

Nc6
∗
c

| u | r :: π | E | H
| u | r :: π | E | N
:: u♦π | r | ǫ | E | H
:: u♦π | r | ǫ | E | N

F
F
F
F

F | ur | π | E | N

Nc5

→

3. If C E is a Max context then C is a Max context by Lemma 6.4.5. By
induction on C being Max (Definition Definition 2.1, page 2). If C is
empty then it is immediate. The other cases:
→

→

→

→

• Application Left (rule (@l)), i.e. C = Dr with D Max and D 6= λx.E.
Since C E = D E r E , we have that D E is a Max context and we
can apply the i.h. to it. Then:
s = F | Dhuir | π | E | H

F | Dhui | r :: π | E | H

Hc1

Now, if D is empty then C is applicative, the stack is non-empty, and
the statement is proved. Otherwise, it follows from the i.h.:
F | Dhui | r :: π | E | H

∗

c
|{z}

F ′ | u | π′ | E | H

i.h.

• Abstraction (rule (λ)), i.e. C = λx.D with D Max. As in the previous
case, it is immediately seen that we can apply the i.h. to D.
s = F | λx.Dhui | π | E | H

Hc1

F :: x | Dhui | π | E | H

∗

c
|{z}

F ′ | u | π′ | E | H

i.h.

→

→→

→

The moreover part follows from the i.h.
• Application Right (rule (@r)), i.e. C = rD with D Max and r neutral.
Since C E = r E D E , we have that r is neutral (and so we can apply
point 2) and D E is a Max context and so we can use the i.h. on it.
s = F | rDhui | π | E | H
(Point 2)

Hc1
∗
c
Nc6

F | r | Dhui :: π | E | H
F | r | Dhui :: π | E | N
F :: r♦π | Dhui | ǫ | E | H

∗

c
|{z}

F ′ | u | π′ | E | H

(i.h.)

Hc1
Hc7
∗
c

|{z}
(i.h.)

30

→

s = F | (λx.r)Dhui | π | E | H

→

→

→

The moreover part follows from the i.h.
• Erasing Redex (rule (gc)), i.e. C = (λx.r)D with D Max and
x∈
/ fv(r). Since C E = (λx.r E )D E we have that D E is a Max
context and so we can use the i.h. on it.
F | λx.r | Dhui :: π | E | H
F :: λx.rπ | Dhui | π | E | H
F ′ | u | π′ | E | H

The moreover part follows from the i.h.

The second lemma uses Lemma 6.10 and the environment labels invariant
(Lemma 6.6.1) to show that the exponential transitions of the Max MAM are
indeed useful, as they head towards a multiplicative transition, that is towards
β-redexes.
Lemma 6.11 (Useful Exponentials Lead to Multiplicatives). Let s be a reachable state such that s e(red,n) s′ .
1. If n = 1 then s′

∗
c

m

s′′ ;

2. If n = 2 then s′

∗
c

eabs

3. If n > 1 then s′

∗
c

e(red,n−1)

∗
c

m

s′′ or s′

∗
c

e(red,1)

s′′ ;

s′′ .
α

Proof. We have (F, x, π, E, H) ered (F, t , π, E, H) with E(x) = [x t](red,n) .
By the labeled environment invariant (Lemma 6.6.1), E is well-labeled. Then
α
t = Chui with C Max context. By Lemma 6.10.3 we obtain
s′ = F | Chui | π | E | H

∗
c

F ′ | u | π′ | E | H

Three cases:
1. n = 1) then by well-labeledness u is a 7→Maxβ -redex (λx.r)s, that is, either
x∈
/ fv(r) or s is normal. First, we have
F ′ | (λx.r)s | π ′ | E | H

F ′ | (λx.r) | s :: π ′ | E | H

Hc1

m

s′′

Then there are 3 possible cases:
(a) s is a variable. Then
(b) x ∈ fv(r). Then

m2

m1

applies.

applies.

(c) x ∈
/ fv(r) and s is normal and not a variable. Then:
F ′ | (λx.r) | s :: π ′ | E | H

m

s′′

Hc7
∗
c

F :: λx.rπ | s | ǫ | E | H
F :: λx.rπ | s | ǫ | E | N

|{z}
(L.6.10.1)
m3

F |r|π|E|N

2. n = 2, E ′ = E ′′ :: [y r]l :: E ′′′ with l = abs, and C is applicative) By
well-labeledness u is a variable y and r = λz.s. Then:
s

e(red,2)

F | Chyi | π | E | H

∗

c
|{z}
(L.6.10.3)

F ′ | y | π′ | E | H

′

Always by Lemma 6.10.3, the stack π ′ is non-empty, say π ′ = t :: π ′′ .
Then we continue with:
′

eabs

F | λz.s | t :: π ′′ | E | H
31

Now we repeat the resoning for the case n = 1 completing the execution
with ∗c m .
3. n > 1 and E ′ = E ′′ :: [y r]l :: E ′′′ with l = (red, n − 1)) By welllabeledness u is a variable y. Then:
s

e(red,n)

F | Chyi | π | E | H

∗

c
|{z}
(L.6.10.3)

F ′ | y | π′ | E | H

e(red,n−1)

Finally, using the environment size invariant (Lemma 6.9.2) we obtain the local boundedness property, that is used to infer a quadratic bound via a standard
reasoning (already employed in [AL16]).
Theorem 6.12 (Exponentials vs Multiplicatives). Let s be an initial Max MAM
state and ρ : s ∗ s′ .
1. Local Boundedness: if σ : s′

∗

s′′ and |σ|m = 0 then |σ|e ≤ |ρ|m ;

2. Exponentials are Quadratic in the Multiplicatives: |ρ|e ∈ O(|ρ|2m ).
Remark 6.13. In the following proof we use the fact that in from the definition
of well-labeled environment (Definition 4.2, page 8) it immediately follows that
if E = E ′ :: [x t](red,n) :: E ′′ is well-labeled then the length of E ′′ , and thus of
E, is at least n.
Proof.
1. We prove that |σ|e ≤ |E|. The statement follows from the environment
size invariant (Lemma 6.9.2), for which |E| ≤ |ρ|m .
If |σ|e = 0 it is immediate. Then assume |σ|e > 0, so that there is a first
exponential transition in σ, i.e. σ has a prefix s′ ∗c e s′′′ followed by an
execution τ : s′′′ ∗ s′′ such that |τ |m = 0. Cases of the first exponential
transition e :
• Case eabs : the next transition is necessarily multiplicative, and so
τ is empty. Then |σ|e = 1. Since the environment is non-empty
(otherwise eabs could not apply), |σ|e ≤ |E| holds.
• Case e(red,n) : we prove by induction on n that |σ|e ≤ n, that gives
what we want because n ≤ |E| by Remark 6.13. Cases:
– n = 1) Then τ has the form s′′′ ∗c s′′ by Lemma 6.11.1, and so
|σ|e = 1.
– n = 2) Then τ is a prefix of ∗c eabs ∗c or ∗c e(red,1) by
Lemma 6.11.2. In both cases |σ|e ≤ 2.
– n > 2) Then by Lemma 6.11.3 τ is either shorter or equal to
∗
∗
e(red,n−1) ,
e(red,n−1) , and so |σ|e ≤ 2, or it is longer than
c
c
′
∗
i.e. it writes as c followed by an execution τ starting with
′
e(red,n−1) . By i.h. |τ | ≤ n − 1 and so |σ| ≤ n.

32

F ′ | r | π′ | E | H

2. This is a standard reasoning: since by local boundedness (the previous
point) m-free sequences have a number of e-transitions that are bound by
the number of preceding m-transitions, the sum of all e-transitions is bound
by the square of m-transitions. It is analogous to the proof of Theorem
7.2.3 in [AL16].

Commutative vs Exponential Analysis The second step is to bound the
number of commutative transitions. Since the commutative part of the Max
MAM is essentially the same as the commutative part of the Strong MAM of
[ABM15], the proof of such bound is essentially the same as in [ABM15]. It
relies on the subterm invariant (Lemma 6.9.1).
Theorem 6.14 (Commutatives vs Exponentials). Let ρ : s
MAM execution from an initial state of code t. Then:

∗

s′ be a Max

1. Commutative Evaluation Steps are Bilinear: |ρ|Hc ≤ (1 + |ρ|e ) · |t|.
2. Commutative Evaluation Bounds Backtracking: |ρ|Nc ≤ 2 · |ρ|Hc .
3. Commutative Transitions are Bilinear: |ρ|c ≤ 3 · (1 + |ρ|e ) · |t|.
Proof.
1. We use the following notion of size for stacks/frames/states:
|ǫ| :=
|t :: π| :=
|(F, t, π, E, H)| :=

0
|t| + |π|
|F | + |π| + |t|

|F :: x|
|F :: t♦π|
|F :: λx.tπ|
|(F, t, π, E, N)|

:=
:=
:=
:=

|F |
|π| + |F |
|t| + |π| + |F |
|F | + |π|

By direct inspection of the rules of the machine it can be checked that:
• Exponentials Increase the Size: if s e s′ is an exponential transition,
then |s′ | ≤ |s| + |t| where |t| is the size of the initial term; this is a
consequence of the fact that exponential steps retrieve a piece of
code from the environment, which is a subterm of the initial term by
Lemma 6.9.1;
• Commutative Evaluation Transitions Decrease the Size: if s a s′
with a ∈ {Hc1 , Hc2 , Hc3 , Hc7 } then |s′ | < |s| (for Hc3 because the
transition switches to backtracking, and thus the size of the code is
no longer taken into account);
• Multiplicative Transitions and Backtracking Transitions Decrease or
do not Change the Size: if s a s′ with a ∈ {m1 , m2 , m3 , Nc4 , Nc5 , Nc6 }
then |s′ | ≤ |s|.
Then a straightforward induction on |ρ| shows that
|s′ | ≤ |s| + |ρ|e · |t| − |ρ|Hc
i.e. that |ρ|Hc ≤ |s| + |ρ|e · |t| − |s′ |.

33

Now note that | · | is always non-negative and that since s is initial we
have |s| = |t|. We can then conclude with
|ρ|Hc

≤ |s| + |ρ|e · |t| − |s′ |
≤ |s| + |ρ|e · |t|
= |t| + |ρ|e · |t| =

(1 + |ρ|e ) · |t|

2. We have to estimate |ρ|Nc = |ρ|Nc4 + |ρ|Nc5 + |ρ|Nc6 . Note that
(a) |ρ|Nc4 ≤ |ρ|Hc2 , as
(b) |ρ|Nc5 ≤ |ρ|Nc6 , as
Nc6 ;
(c) |ρ|Nc6 ≤ |ρ|Hc3 , as
Hc3 .

Nc4

pops variables from F , pushed only by

pops pairs t♦π from F , pushed only by

Nc5

Nc6

Hc2 ;

ends backtracking phases, started only by

Then |ρ|Nc ≤ |ρ|Hc2 + 2|ρ|Hc3 ≤ 2|ρ|Hc .
3. We have |ρ|c = |ρ|Hc +|ρ|Nc ≤P.2 |ρ|Hc +2|ρ|Hc = 3|ρ|Hc ≤P.1 3·(1+|ρ|e )·|t|.

The Main Theorem Putting together the matching between Max β-steps
and multiplicative transitions (Theorem 5.1), the quadratic bound on the exponentials via the multiplicatives (Theorem 6.12.2) and the bilinear bound on the
commutatives (Theorem 6.14.3) we obtain that the number of the Max MAM
transitions to implement a Max β-derivation d is at most quadratic in the length
of d and linear in the size of t. Moreover, the subterm invariant (Lemma 6.9.1)
and the analysis of the Checking AM (Theorem 4.3.2) allow to bound the cost
of implementing the execution on RAM.
Theorem (Max MAM Overhead Bound). Let d : t →∗Maxβ u be a maximal
derivation and ρ be the Max MAM execution simulating d given by Theorem 5.1.2.
Then:
1. Length: |ρ| = O((1 + |d|2 ) · |t|).
2. Cost: ρ is implementable on RAM in O((1 + |d|2 ) · |t|) steps.
Proof.
1. By definition, the length of the execution ρ simulating d is given by |ρ| =
|ρ|m + |ρ|e + |ρ|c . Now, by Theorem 6.12.2 we have |ρ|e = O(|ρ|2m ) and
by Theorem 6.14.3 we have |ρ|c = O((1 + |ρ|e ) · |t|) = O((1 + |ρ|2m ) · |t|).
Therefore, |ρ| = O((1 + |ρ|e ) · |t|) = O((1 + |ρ|2m ) · |t|). By Theorem 5.1.2
|ρ|m = |d|, and so |ρ| = O((1 + |d|2 ) · |t|).
2. The cost of implementing ρ is the sum of the costs of implementing the
multiplicative, exponential, and commutative transitions. Remember that
the idea is that variables are implemented as references, so that environment can be accessed in constant time (i.e. they do not need to be accessed
sequentially). Moreover, we assuming the strong hypothesis on the representation of terms explained in the paragraph before Theorem 4.3 (page
/ fv(t) in m2 and Hc7 can be done
9), so that the tests x ∈ fv(t) and x ∈
in constant time:
34

(a) Commutative: every commutative transition takes constant time. At
the previous point we bounded their number with O((1 + |d|2 ) · |t|),
which is then also the cost of all the commutative transitions together.
(b) Multiplicative:
• a m1 transition costs O(|t|) because it requires to rename the
current code, whose size is bound by the size of the initial term
by the subterm invariant (Lemma 6.9.1a).
• A m2 transition costs O(|t|) because checking x ∈ fv(t) can
be done in constant time and executing the Checking AM on u
takes O(|u|) commutative steps (Theorem 4.3.2), commutative
steps take constant time, and the size of u is bound by |t| by the
subterm invariant (Lemma 6.9.1b).
• A m2 transition takes constant time.
Therefore, all together the multiplicative transitions cost O(|d| · |t|).
(c) Exponential : At the previous point we bounded their number with
|ρ|e = O(|d|2 ). Each exponential step copies a term from the environment, that by the subterm invariant (Lemma 6.9.1d) costs at
2
most O(|t|), and so their full cost is O((1 + |d|) · |t| ) (note that this
is exactly the cost of the commutative transitions, but it is obtained
in a different way).
2

Then implementing ρ on RAM takes O((1 + |d|) · |t| ) steps.

Remark 6.15. Our bound is quadratic in the number of the Max β-steps but we
believe that it is not tight. In fact, our transition m1 is a standard optimisation,
used for instance in Wand’s [Wan07] (section 2), Friedman et al.’s [FGSW07]
(section 4), and Sestoft’s [Ses97] (section 4), and motivated as an optimization
about space. In Sands, Gustavsson, and Moran’s [SGM02], however, it is shown
that it lowers the overhead for time from quadratic to linear (with respect to the
number of β-steps) for call-by-name evaluation in a weak setting. Unfortunately,
the simple proof used in [SGM02] does not scale up to our setting, nor we have
an alternative proof that the overhead is linear. We conjecture, however, that it
does.

35

