# Equivalence of eval-readback and eval-apply big-step evaluators by
structuring the lambda-calculus’s strategy space

Pablo Nogueira0000-0002-8706-0027  UDIT, University of Design and Technology,
Madrid, Spain<EMAIL_ADDRESS>and  Álvaro García-
Pérez0000-0002-9558-6037  Université Paris-Saclay, CEA, List, F-91120,
Palaiseau, France<EMAIL_ADDRESS>
###### Abstract.

We study the equivalence of eval-readback and eval-apply big-step evaluators
in the general setting of the pure lambda calculus. The equivalence extends to
evaluators in other lambda calculi (applied and typed) if the evaluation order
of redexes (i.e. the evaluation strategy) is realisable. We present a proof
that one-step equivalence holds when (1) the ‘readback’ stage satisfies
straightforward well-formedness provisos, (2) the ‘eval’ stage implements a
‘uniform’ strategy, and (3) the eval-apply evaluator implements a ‘balanced
hybrid’ strategy that has ‘eval’ as a subsidiary strategy. The proof proceeds
by application of the ‘lightweight fusion by fixed-point promotion’ program
transformation on evaluator implementations to fuse readback and eval into the
balanced hybrid. The proof can be followed with no previous knowledge of the
transformation. We use Haskell 2010 as the implementation language, with all
evaluators written in monadic style to guarantee semantics (strategy)
preservation, but the choice of implementation language is immaterial.

To determine the scope of the equivalence, we provide an extensive survey of
the strategy space using canonical eval-apply evaluators. We discuss the
strategies’ properties and some of their uses and abstract machines. We
improve the formal definition of uniform and hybrid strategy, and use it to
structure the strategy space and to obtain the generic higher-order evaluators
used in the proof that deliver all plain evaluators as fixed-points by
instantiation. We introduce a systematic notation for both evaluator styles
and use it to summarise strategy and evaluator equivalences, including
(non-)equivalences within a style and (non-)equivalences between styles not
proven by the transformation.

###### Key words and phrases:

Lambda calculus, big-step evaluators, definitional interpreters, evaluation
strategies, operational semantics, program transformation, program
equivalence, functional programming.

###### Contents

  1. 1 Introduction
    1. 1.1 The context
    2. 1.2 The problem
    3. 1.3 The contributions
  2. 2 Technical preliminaries
  3. 3 The call-by-value strategy (and its variants)
  4. 4 The eval-apply evaluator style
    1. 4.1 Monadic style eval-apply
    2. 4.2 Natural semantics style eval-apply
  5. 5 A survey of the pure lambda calculus’s strategy space
    1. 5.1 Call-by-value $({\mathsf{bv}})$
    2. 5.2 Call-by-name $({\mathsf{bn}})$
    3. 5.3 Applicative order $({\rm Appl.\leavevmode\nobreak\ Opt.})$
    4. 5.4 Normal order $({\mathsf{no}})$
    5. 5.5 Head reduction $({\mathsf{hr}})$
    6. 5.6 Head spine $({\mathsf{he}})$
    7. 5.7 Strict normalisation $({\mathsf{sn}})$
    8. 5.8 Hybrid normal order $({\mathsf{hn}})$
    9. 5.9 Hybrid applicative order $({\mathsf{ha}})$
    10. 5.10 Ahead machine $({\mathsf{am}})$
    11. 5.11 Head applicative order $({\mathsf{ho}})$
    12. 5.12 Spine applicative order $({\mathsf{so}})$
    13. 5.13 Balanced spine applicative order $({\mathsf{bs}})$
    14. 5.14 Summary of the survey
  6. 6 The eval-readback evaluator style
    1. 6.1 Monadic style eval-readback
    2. 6.2 Natural semantics style eval-readback
    3. 6.3 Characterisation of the style
    4. 6.4 Equivalences within the style
  7. 7 Structuring the pure lambda calculus’s strategy space
    1. 7.1 Evaluation templates and generic evaluators
      1. 7.1.1 Eval-apply evaluation template and generic evaluator
      2. 7.1.2 Eval-readback evaluation template and generic readback
    2. 7.2 Uniform/Hybrid as structuring criteria
      1. 7.2.1 Small-step context-based reduction semantics
      2. 7.2.2 Intuition of uniform/hybrid strategy
      3. 7.2.3 Definition of uniform/hybrid strategy
    3. 7.3 Structuring the uniform space
    4. 7.4 Structuring the hybrid space
      1. 7.4.1 A systematic notation for hybrid evaluators
      2. 7.4.2 (Non-)Equivalences within the style
    5. 7.5 Structuring the eval-readback space
  8. 8 Equivalence proof by LWF transformation
    1. 8.1 Plain but arbitrary eval-readback evaluators
    2. 8.2 Plain but arbitrary balanced hybrid eval-apply evaluators
    3. 8.3 Statement of one-step equivalence
    4. 8.4 Proof by LWF transformation
  9. 9 Summary and conclusions
  10. 10 Related and future work
  11. A Pure lambda calculus concepts and notation
  12. B Call-by-value in the lambda-value calculus
  13. C Overview of LWF
  14. D Haskell’s operational semantics
  15. E Completeness of leftmost and spine strategies

##  1\. Introduction

###  1.1. The context

Big-step evaluators are ubiquitous in formal semantics and implementations of
higher-order languages based on the lambda calculus, whether research
languages or core languages of functional programming languages and proof-
assistants.

A big-step evaluator is a definition (a _definiens_) for an evaluation
strategy (the unique _definiendum_). An evaluation strategy (or just
‘strategy’) determines the evaluation order of the reducible expressions
(redexes) of terms. A strategy is a mathematical extensional object defined,
generically, as a function subset of the calculus’s reduction relation. We are
interested in history-free sequential strategies where the choice of redex is
based on fixed positional criteria independent of previous choices. A big-step
evaluator is an intensional function definition of a strategy that specifies
how the redexes are located and evaluated. It is ‘big-step’ because it
delivers the _final_ result of iterated small-step reduction. Because a big-
step evaluator defines a unique strategy, it is common to blur the distinction
and call the evaluator a strategy. A strategy can also be defined in small-
step operational semantics styles such as structural [Plo81], context-based
[Fel87], or abstract machines [Lan64, DHS00].

In practice, a big-step evaluator is typically written as a recursive function
in code [McC60] or in natural semantics [Kah87]. In code, the evaluator works
on some data-type representation of the mathematical terms. The operational
semantics of the implementation language must be taken into account to
guarantee semantics (_i.e._ strategy) preservation [Rey72]. In natural
semantics, the evaluator works on the mathematical terms and is defined by a
set of syntax-directed and deterministic inference rules describing the
function’s behaviour recursively on the subterms. A natural semantics provides
a compact two-dimensional definition, requires no knowledge of specific
programming languages, and serves as a specification of the evaluator’s
implementation in code. In a partiality setting, a big-step evaluator may
terminate (converge) on a final result, or non-terminate (diverge) because it
cannot deliver a final result when it exists (which may be delivered by other
strategies) or because no final result exists (which may be delivered by no
strategy).

Whether in code or natural semantics, big-step evaluators are written
typically in two definitional _styles_.

In _eval-apply_ style, the evaluator is defined by a _single function_. This
style appeared early in programming and formal semantics [McC60, Lan64, Rey72,
Plo75, Sto77, SS78] and was the main style until the 1990s [All78, ASS85,
FH88, Hen87, Rea89, Mac90]. In code, the eval function evaluates subterms
recursively and delegates the specific evaluation of application terms to a
mutually-recursive local apply function. This function can be anonymised using
let-clauses and pattern-matching expressions in some implementation languages.
In natural semantics, the eval-apply evaluator is defined by a single set of
inference rules for every case of term: variables, abstractions (function
bodies), and redex and non-redex applications. The apply function corresponds
to the inference rules for applications.

In _eval-readback_ style, the evaluator is defined by a _composition of two
functions_ (also called stages), namely, readback after eval. The name ‘eval-
readback’ comes from [GL02]. Two classic evaluators that conform to the style
are byName and byValue in [Pau96, p. 390]. The style is related to
normalisation-by-evaluation [BS91] (hereafter, NBE), but it should not be
confused with nor named after NBE. In the latter, a term is evaluated by first
constructing its representative in a different target domain (evaluation
stage) and then reading the representative back to a canonical result term
(reification stage). In eval-readback there is only the domain of terms. The
_less-reducing_ eval function contracts redexes to an intermediate result with
unevaluated subterms. The _further-reducing_ readback does not contract
redexes, it ‘reads back’ the intermediate result to a further-reduced result
by recursively distributing eval down the unevaluated subterms to reach
further redexes [GL02, p. 236]. Readback is a sort of ‘selective-iteration-of-
eval’ function that calls eval directly or in an eval-readback composition on
specific unevaluated subterms. The separation of evaluation in two stages can
be of help in writing an evaluator (Section 6). The separation also enables
independent optimisations. For instance, in [GL02] the eval stage is
implemented by an abstract machine and its associated compilation scheme
[Ler91].

###  1.2. The problem

We address the question of equivalence between eval-readback and eval-apply
evaluators which partly answers the question of expressive power, _i.e._
whether a strategy can or cannot be defined in both styles. Concretely, we are
primarily interested in whether the evaluators define the same strategy
(evaluate redexes in exactly the same order) rather than in whether the
evaluators deliver identical final results, although we also consider the
latter. We refer to the former equivalence as _one-step equivalence_ and to
the latter as _big-step equivalence_. We aim for a _single_ one-step
equivalence proof for a large collection of strategies. We address the problem
in the setting of the pure lambda calculus for the following reasons.

  1. (1)

The pure lambda calculus is the most general setting where more terms,
strategies, and concomitant big-step evaluators can be defined. There are many
extensions of the pure lambda calculus with their own particulars and with
significant differences among them. An evaluator of the pure lambda calculus
can be transcribed to extended applied and/or typed calculi,111 An _applied_
extension of the pure lambda calculus extends it with primitive terms and
reduction rules for them. A _typed_ extension extends it with type terms, type
rules, and possibly modified terms and reduction rules. An applied and typed
extension combines both. or can be used directly on the terms that remain
after type-checking and type-erasure [Pie02, GL02]. We choose the pure lambda
calculus not because it is untyped or unapplied, but because those properties
let us use it as a base from which to take additional restrictions (_e.g._
closed, typed, or convergent terms, etc.) assumed in other settings (_e.g._
programming languages, proof assistants, etc.) that use evaluation strategies
(_e.g._ Section 3).

Relatedly, we will use a direct data-type representation (a ‘deep embedding’
[BGG+92]) of terms in code and the default capture-avoiding substitution
operation. The equivalence results presented in this paper extend to calculi
with other term representations provided the evaluation order of redexes (the
strategy) remains unchanged, and extend to calculi where the strategy can be
simulated (_e.g._ [Plo75, Sec. 6]). Of course, an efficient term
representation is chosen with the practical goal of defining more efficient
versions of strategies that alter the evaluation order (_e.g._ call-by-need
evaluates copies of the same redex once, unlike call-by-name). Such strategies
are not realisable in the pure lambda calculus but the results in this paper
can inform further work for such strategies (Section 1.3.C1).

Indeed, we leave all efficiency considerations aside because the particulars
constrain the possible strategy space. We study strategies in the default
setting of the pure lambda calculus. In that setting there are no optimal
strategies because there are terms for which any strategy duplicates work
[Lév78, Lév80]. Our goal is to structure the strategy space to prove one-step
equivalence. Efficiency considerations can be studied afterwards in a
constrained strategy space. For the wide-range of issues regarding efficiency
see [Lév80, FH88, Lam89, GAL92, AG98, RP04, AL16, ALV21].

  2. (2)

The pure lambda calculus allows free variables and hence _open_ terms, with
the particular case of _neutral terms_ (_neutrals_ , for short).222We thank
Noam Zeilberger for pointing us to the ‘neutral’ terminology. A free variable
is not a parameter of an abstraction. The notion is relative to a term: $x$
may be free in $B$ but it is bound (not free) in $\lambda x.B$. Neutral terms
are applications of the form $x\,N_{1}\cdots N_{n}$ where $n\geq 1$. A neutral
is not a redex, and cannot evaluate to a redex unless a suitable term can be
substituted for the leftmost variable operator (called the ‘head variable’).
When the head variable is free, it may be seen as a data-type value
constructor that is applied to the $n$ operands.

  3. (3)

The pure lambda calculus allows strategies with diverse evaluation properties,
in particular:

     * •

Weak or non-weak evaluation: respectively, the non-evaluation or evaluation of
abstractions (function bodies) as in programming languages. Mind the
opposites: weak = non-evaluation of abstractions; non-weak = evaluation of
abstractions.

     * •

Strict or non-strict evaluation: respectively, the evaluation or non-
evaluation of operands of redexes before substitution. Technically, strictness
is a denotational property of functions but it can be ‘abused’ as an
evaluation property.

     * •

Head or non-head evaluation: respectively, the non-evaluation or evaluation of
(operands of) neutrals, which gives the name to strategies such as ‘head
reduction’ or ‘head spine’ (Section 5). Mind the opposites: head = non-
evaluation of neutrals; non-head = evaluation of neutrals.

     * •

Full evaluation (hereafter, full-reduction): the evaluation to a result term
with no redexes. Full-reduction with open terms is essential in optimisation
by partial evaluation and type-checking in proof-assistants and automated
reasoning, _e.g._ [GL02, Cré07, ACP+08, SR15, ABM15].333Many authors use
‘strong reduction’ rather than ‘full-reduction’. However, ‘strong’ is the
antonym of ‘weak’ which only refers to the non-evaluation of abstractions.
Also, strong reduction may be confused with ‘strong normalisation’ which is a
property of terms (fn. 7, p. 7). We use ‘full-reduction’ [SR15] for these
reasons, with a dash to make it a technical name.

These evaluation properties _and their interaction_ give rise to different
kinds of final results and properties. For example, a weak and strict strategy
does not evaluate the abstractions within the operands of the redexes it does
evaluate. A non-weak and head strategy does not evaluate the neutrals within
the abstractions it does evaluate.

In a previous work [GPN14], we showed that given an eval-readback evaluator rb
$\circ$ ev, its one-step equivalence with a given eval-apply evaluator ea can
be proven _in code_ using the ‘lightweight fusion by fixed-point promotion’
program transformation of [OS07], which we hereafter abbreviate as LWF. (We
also hereafter abbreviate evaluator names using two letters (_e.g._ ‘rb’,
‘ev’, etc.) like [Ses02], to fit their code and natural semantics definitions
in running text and figures.) The transformation fuses rb $\circ$ ev into ea
by means of strategy-preserving, simple and syntactic program-transformation
steps that are embeddable in a compiler’s inlining optimisation. The LWF
transformation had been previously used in the literature on derivations by
program transformation of operational semantics devices, but in ‘syntactic-
correspondence’ proofs between small-step evaluators and abstract machines to
fuse the decomposition and recomposition steps, _e.g._ [Dan05, DM08, DJZ11].

In [GPNS14], we used LWF to prove the one-step equivalence of one eval-
readback evaluator and one eval-apply evaluator where both implemented one
strategy of the gradually-typed lambda calculus. However, using LWF for every
possible strategy and pair of particular evaluators is menial work. Another
problem is that LWF is not invertible. An eval-readback evaluator is not
obtained by ‘de-fusing’ a given eval-readback evaluator. The eval-readback
evaluator must be conjectured, and then it must LWF-transform to the given
eval-apply evaluator. Whether an eval-readback evaluator exists for a given
eval-apply evaluator, and vice-versa, is part of the open question of
expressive power mentioned at the beginning of this section.

###  1.3. The contributions

The last contribution of this paper is a single proof of the one-step
equivalence of eval-readback and eval-apply evaluators for a large set of
strategies. The proof proceeds by a novel application of LWF on a _plain but
arbitrary_ eval-readback evaluator and a _plain but arbitrary_ eval-apply
evaluator which rely on a _generic_ readback evaluator and a _generic_ eval-
apply evaluator that respectively implement as fixed-points all the _plain and
concrete_ readback and eval-apply evaluators in the set. The LWF steps are
applied verbatim on the two arbitrary evaluators. These are arbitrary because
some parameters to the generic evaluators they invoke have type-checked but
undefined values (are existentially quantified in the sense of logic
programming). The concrete values substitutable for these parameters are
constrained by the provisos and the LWF steps, and collected in a list of
equations that capture the conditions for one-step equivalence.

This last contribution strongly depends on other significant contributions
that we list below in increasing order of importance and of presentation in
the paper. The list of contributions below also serves as a roadmap summary of
the paper. In Section 9 we provide a detailed technical summary of the
contributions that can be understood after reading the paper.

C1 Eval-apply style and strategy survey:

We provide an extensive survey of pure lambda calculus strategies (Section 5)
showing their canonical evaluators in natural semantics eval-apply style. We
previously overview the eval-apply style in code and natural semantics
(Section 4) using as a first example the call-by-value strategy of the pure
lambda calculus (Section 3). We discuss this strategy in detail and compare it
to other call-by-value strategies. We use the Haskell 2010 standard as the
implementation language, with all evaluators (plain and generic) written in
monadic style to guarantee semantics (strategy) preservation. However, the
choice of implementation language is immaterial (Section 4.1).

In the survey we discuss strategies that are well-known, less known, and some
interesting novel ones. We briefly recall their properties, some of their
abstract machines, and some of their uses, particularly in the evaluation of
general recursive functions, where we use simple and well-known Church
numerals as data for examples. We focus on this particular use for some
strategies because it illustrates their evaluation properties in relation to
thunking [Ing61, DH92] and direct and delimited continuation-passing styles
[HD94, BBD05]. We want to draw attention to the novel strategy ‘spine
applicative order’ that evaluates general recursive functions in delimited
continuation-passing style, _eagerly_ but with a _non-strict_ fixed-point
combinator, and with thunking ‘ _protecting by variable_ ’ instead of the
common ‘protecting by lambda’ in the literature on thunking.

As indicated in Section 1.1, we are interested in history-free sequential
strategies where the choice of redex is based on fixed positional criteria
independent of previous choices. The survey excludes history-informed,
parallel, non-deterministic, and right-to-left444A right-to-left strategy
evaluates the operand of a redex before the abstraction when it is non-weak,
and the operands of a neutral from right-to-left when it is non-head.
strategies. The survey also excludes strategies that cannot be defined in the
pure lambda calculus (_e.g._ call-by-need which requires sharing and
memoisation). Finally, the survey excludes simulations of strategies that
belong to other calculi (Section 3). The survey is nonetheless extensive and
informs future work on the other strategy spaces. Strategy equivalence must be
studied under equivalent conditions: in the same calculus, and with either the
same term representation or with the same order of redexes (strategy) under
different term representations.

C2 Characterisation of eval-readback style:

We overview the eval-readback style in code (Section 6.1) and natural
semantics (Section 6.2) using well-known evaluators in the literature and
relating them to the eval-apply evaluators in the survey. We characterise the
style precisely by means of two provisos (Section 6.3), and discuss the limit
on the amount of evaluation that can be moved between eval and readback, which
determines equivalences within the style (Section 6.4).

C3 Generic templates and evaluators:

We present a _generic_ eval-apply and a generic readback evaluator by means of
natural semantics templates and higher-order parametric evaluator
implementations in code. The generic evaluators deliver plain evaluators as
fixed-points by instantiation. The generic evaluators are obtained by
parametrising on all the _variability points_ of their respective style. The
generic eval-apply evaluator delivers all the evaluators in the survey. The
generic readback evaluator delivers all the readbacks that satisfy the
provisos. The generic evaluators let us express the evaluator space uniformly
in a single definition. We employ them in the equivalence proof by LWF.

C4 Improved definition of uniform/hybrid strategy:

We improve the formal definition of uniform vs hybrid strategy that we
presented in [GPN14, Sec. 4]. Intuitively, a hybrid (or layered, or
stratified) strategy inextricably _depends_ on other less-reducing subsidiary
strategies to evaluate particular subterms such as operators or operands. When
there is no dependency, the strategy is uniform. The dependency shows in the
evaluation sequences of the hybrid strategy which include whole evaluation
sequences of the subsidiaries for the subterms. The dependence is often
reflected in the _definitional device_ used for defining the hybrid strategy
(code or operational semantics, whether big-step, small-step, or abstract
machines) that explicitly includes the definitional device of one or more
subsidiary strategies. In this case we say the hybrid _strategy_ is defined by
a definitional device in hybrid _style_. For instance, a hybrid strategy’s
evaluator is in hybrid style when it calls a subsidiary strategy’s evaluator.

As we detail in Sections 5.8 and 5.9, the words uniform and hybrid originate
in [Ses02] where they are introduced informally and closely to the concept of
in/dependence on a subsidiary big-step evaluator in a natural semantics, what
we call uniform/hybrid _style_. We relied on the style concept in [GPNG10,
GPN13, GPNM13, GPNS14] and distinguished it from the style-independent
property in [GPN14] which we called uniform/hybrid ‘in its nature’ (rather
convolutedly). Our unsatisfactory definition and terminology may explain the
exclusive focus on style in later work on hybrid strategies (Section 7.2).
From this paper on we propose to use the ‘style’ suffix with more precision
for definitional devices and use uniform/hybrid by itself for a property of a
strategy. As explained in [GPN14] and elaborated in Section 7.2, the
distinction is essential because, depending on the type of device, it may be
possible to write uniform-style devices for hybrid strategies by hiding the
subsidiary devices, or to write hybrid-style devices for uniform strategies by
concocting spurious subsidiary devices.

In [GPN14] we formalised uniform/hybrid strategy using small-step context-
based reduction semantics [Fel87, FFF09]. Since we wish to improve on [GPN14],
in Section 7.2 we switch temporarily to that small-step definitional device
and arrive at an improved definition from illustrative examples, rather than
define the concept first and then illustrate it with examples.

We introduce in this paper the concept of a _balanced_ (opposite,
_unbalanced_) hybrid strategy. This concept is required for the equivalence
proof by LWF. A hybrid strategy uses the subsidiary to evaluate the operator
$M$ in applications $MN$ to obtain a redex $(\lambda x.B)N$. A balanced hybrid
is either a non-strict hybrid (does not evaluate $N$) or a strict hybrid that
uses the subsidiary to evaluate $N$.

C5 Structuring of the strategy space:

We structure the strategy space using the uniform/hybrid property as an
orthogonal criterion, and structure the uniform and hybrid subspaces according
to the weakness, strictness, and headness properties of strategies considered
as a triple.

The uniform strategy space makes up a lattice of eight strategies we call
_Gibbons’s Beta Cube_.555We name the cube with permission after Jeremy Gibbons
who suggested to us the use of booleans to construct a cube lattice (Section
7.3). Other unrelated named cubes in the lambda calculus literature are J. J.
Lévy’s cube of residuals [Lév78] and H. Barendregt’s ‘Lambda Cube’ of typed
lambda calculi [Bar91]. The cube contains three novel strategies. We introduce
the provisos that characterise uniform eval-apply evaluators and show that
they define uniform strategies. We also introduce a systematic notation for
encoding uniform evaluators in a triple, and study the property of absorption
among uniform strategies.

The hybrid space is larger. We introduce the provisos that characterise hybrid
eval-apply evaluators and show when they define hybrid strategies. The hybrid
evaluators rely on one uniform subsidiary evaluator to satisfy the desired
properties (completeness, spineness, etc.). In particular, the subsidiary is
always used to evaluate operators. The hybrid evaluator evaluates more redexes
than the subsidiary evaluator. We introduce a systematic notation for encoding
hybrid evaluators by means of two triples: the Beta Cube triple of the uniform
evaluator used as subsidiary by the hybrid evaluator, and the triple encoding
the hybrid’s weakness, strictness, and headness. We use the notation to
introduce novel strategies and discuss (non-)equivalences among hybrid
evaluators.

C6 Equivalence proof by LWF:

Finally, we present a proof of equivalence between eval-readback evaluators
and _balanced hybrid_ eval-apply evaluators. The proof assumes the provisos
for both styles and proceeds by application of the LWF transformation. We
start from a _plain but arbitrary_ eval-readback evaluator rb $\circ$ ev where
ev is a uniform evaluator defined as a fixed-point of the generic eval-apply
evaluator, and rb is defined as a fixed-point of the generic readback
evaluator. Some parameters of the generic evaluators are type-checked but
undefined and thus _arbitrary_. The LWF transformation fuses rb and ev into
the plain but arbitrary balanced hybrid eval-apply evaluator hy that relies on
a uniform subsidiary evaluator su where both are fixed-points of generic eval-
apply. The type-checked but undefined parameters to the generic evaluators
have their substitutable values constrained by the provisos and the LWF steps.
The possible substitutions are collected in equations. In particular, some of
the equations state that su = ev. When the equations hold then one-step
equivalence holds and thus rb $\circ$ ev $=$ hy.

balanced hybrid eval-readback evaluatorseval-apply evaluatorsLWF
transformation

An expected corollary of the proof is that hy absorbs su/ev, that is, hy
$\circ$ su $=$ hy. Absorption can be used to fuse an evaluator composition or
to defuse an evaluator into a composition.

The LWF proof does not work for _unbalanced_ hybrid strategies. These can be
defined in eval-apply style but not in an LWF-equivalent eval-readback style.
Recall from contribution C4 above that an unbalanced hybrid hy is such that
its subsidiary su evaluates applications that evaluate to a redex more than
hy. Thus, hy cannot absorb su. It might be possible to obtain an equivalence
between an eval-readback evaluator and an unbalanced hybrid eval-apply
evaluator, but LWF cannot find that equivalence.

For a few strategies the equivalence by LWF holds _modulo commuting redexes_
due to the particular steps of LWF. Commuting (_i.e._ non-overlapping) redexes
occur in the operands $N_{i}$ of a neutral $xN_{1}\cdots N_{n}$. An
equivalence modulo commuting redexes means the strategies are big-step
equivalent but differ on the point of divergence, _e.g._ one strategy
evaluates $N_{j}$ first and diverges, the other evaluates $N_{k}$ first and
diverges, with $j<k$.

C7 Summary and discussion of (non-)equivalences:

We use the systematic notation to provide an extensive summary of strategies,
evaluators, (non-)equivalences within a style, and (non-)equivalences between
styles not proven by the transformation. We also discuss the relevance of the
results in the wider context of correspondences among operational semantics
devices (Section 9).

We have listed the contributions in increasing order of importance. All of
them are necessary and interdependent, which is the justification for the
content and length of the paper. The LWF proof goes through thanks to the
generic evaluators that implement the natural semantics templates; the
templates are obtained after structuring the strategy space according to the
improved definition of uniform/hybrid strategy; and the strategy space is
presented in a survey. The LWF proof confirms the structuring is adequate. We
also provide an extensive summary and a discussion of the relevance of the
results.

The paper is divided into four main sections (Sections 4 to 8) which can be
read at separate times before the conclusions, and the related and future
work. The survey (Section 5) can be read cursorily and its details fetched on
demand when reading about the structuring (Section 7). The equivalence proof
by LWF (Section 8) can be followed with no previous knowledge of LWF, but we
provide an overview of LWF in Appendix C. The code has been type-checked and
tested, and can be obtained on request. We have addressed the content to non-
expert readers familiar with the pure lambda calculus and functional
programming. Some readers may be unfamiliar with some strategies and evaluator
styles and thus we provide the necessary background in the text (or in the
appendix when appropriate) for information or reminder.

##  2\. Technical preliminaries

We overview the pure lambda calculus notation and concepts required for this
paper in Appendix A, namely, syntax and meta-notation of terms, reduction,
evaluation sequence, evaluation strategy, completeness, and completeness _for_
a final result other than normal form. For the most part we adhere to the
standard references [CF58, Bar84, HS08]. We use the notation for capture-
avoiding substitution of [Plo75] (and justify why in Appendix A). We use
grammars in Extended Backus-Naur Form to define sets of terms. Figure 1 lists
the main sets of terms we use in this paper, which play a special role in
evaluation. They are proper subsets of the set $\Lambda$ of pure lambda
calculus terms. Appendix C provides an overview of LWF. Appendix D provides an
overview of Haskell’s operational semantics in relation to LWF. Appendix E
explains why strict strategies are incomplete and when non-strict strategies
are complete, particularly the leftmost and spine strategies discussed in the
survey. For the moment we assume the intuitive definition of uniform/hybrid
strategy and of un/balanced hybrid strategy given in Section 1.3.C4.
(Alternatively, the reader may assume the formal definition of uniform/hybrid
strategy in [GPN14].) We also assume that all the uniform-style and hybrid-
style eval-apply evaluators in the survey respectively define uniform and
hybrid strategies. The validity of this assumption will be proven in Section 7
where we give the improved formal definition of uniform/hybrid strategy. The
definition of one-step equivalence ‘modulo commuting redexes’ has been
introduced in the last paragraph of Section 1.3.C6.

$\Lambda$ | ::= | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\ |\ \lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\Lambda\ |\ \Lambda\;\Lambda$ | Terms over a set of variables  $\Lambda$ .
---|---|---|---
$\mathsf{Neu}$ | ::= | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\ \Lambda\ \\{\Lambda\\}^{*}$ |  $\mathsf{Neu}$trals: applications $x\,N_{1}\cdots N_{n}$ where $n\geq 1$.
$\mathsf{NF}$ | ::= | $\lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\mathsf{NF}$ | $|$ | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\;\\{\mathsf{NF}\\}^{*}$ |  $\mathsf{N}$ormal $\mathsf{F}$orms.
$\mathsf{WNF}$ | ::= | $\lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\Lambda$ | $|$ | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\;\\{\mathsf{WNF}\\}^{*}$ |  $\mathsf{W}$eak $\mathsf{N}$ormal $\mathsf{F}$orms.
$\mathsf{HNF}$ | ::= | $\lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\mathsf{HNF}$ | $|$ | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\;\\{\Lambda\\}^{*}$ |  $\mathsf{H}$ead $\mathsf{N}$ormal $\mathsf{F}$orms.
$\mathsf{WHNF}$ | ::= | $\lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\Lambda$ | $|$ | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\;\\{\Lambda\\}^{*}$ |  $\mathsf{W}$eak $\mathsf{H}$ead $\mathsf{N}$ormal $\mathsf{F}$orms.
$\mathsf{VHNF}$ | ::= | $\lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\mathsf{VHNF}$ | $|$ | $\rotatebox[origin={c}]{180.0}{$\Lambda$}\;\\{\mathsf{WNF}\\}^{*}$ |  $\mathsf{V}$alue $\mathsf{H}$ead $\mathsf{N}$ormal $\mathsf{F}$orms.
Figure 1. Main sets of terms in Extended BNF where $\\{\mathsf{X}\\}^{*}$
denotes zero or more occurrences of non-terminal $\mathsf{X}$, that is,
$\mathsf{X}_{1}\cdots\mathsf{X}_{n}$ with $n\geq 0$.

##  3\. The call-by-value strategy (and its variants)

To discuss an evaluator style we must first pick a strategy. In this section
we present a strategy in words to avoid the circularity of using an evaluator.
We pick the call-by-value strategy _of the pure lambda calculus_ which can be
also called ‘call-by-weak-normal-form’ where ‘value’ means ‘weak normal form’.
We present its evaluator in Section 4. At the end of this section we discuss
the similarities and differences with other call-by-value strategies.

The word ‘call-by-value’ originates in programming languages as the name for
the parameter-passing _policy_ in function and value-constructor applications
where the operand is evaluated to a ‘value’ before passed to the function or
value constructor. The notion of ‘value’ depends on the language. The policy
is concerned with operands but also with functions because they are not
evaluated in programming languages. In the pure lambda calculus, such call-by-
value policy is embodied by a weak, strict, and non-head strategy. The notion
of ‘value’ is not the expected one of normal form because then the
abstractions within operands would be evaluated fully to normal form, not
weakly. (The strategy that embodies call-by-normal-form is ‘applicative order’
discussed in the survey.) Under weak evaluation, a value is therefore a weak
normal form, similar to weak normal forms of strict functional programming
languages but with the possibility of open terms. Weak normal forms
($\mathsf{WNF}$ in Figure 1) consist of unevaluated abstractions, variables,
and neutrals with operands in weak normal form.

The weak, strict, and non-head call-by-value (call-by-$\mathsf{WNF}$) strategy
evaluates terms to $\mathsf{WNF}$ by choosing the leftmost-innermost redex not
inside an abstraction (when considering the abstract syntax tree of the term).
The strategy is an identity on variables and abstractions, and it evaluates
applications $MN$ by first evaluating $M$ recursively.

If $M$ evaluates to an abstraction $\lambda x.B$ then the application
$(\lambda x.B)N$ is a redex. The strategy evaluates the operand $N$ to
$N^{\prime}$ and then evaluates the contractum $[N^{\prime}/x](B)$.

If $M$ does not evaluate to an abstraction then it either evaluates to a
variable $x$ or to a neutral $M^{\prime}$. In both cases, the application
(either $xN$ or $M^{\prime}N$) is a neutral and the strategy evaluates the
operand $N^{\prime}$ as if the head variable (either $x$ or the head variable
of $M^{\prime}$) were a strict data-type value constructor.

Call-by-value (call-by-$\mathsf{WNF}$) is incomplete for $\mathsf{WNF}$s (and
so for $\mathsf{NF}$s) because it is strict (Appendix E). For example, it
diverges on $(\lambda y.z)\mathbf{\Omega}$ whereas other strategies converge
on $z$ which is a $\mathsf{WNF}$ (and also a $\mathsf{NF}$). It is a strategy
of the pure lambda calculus and as such it relies on its beta-rule which is
unrestricted about what can be an operand in a redex. The evaluation of the
operand is performed by the strategy. Call-by-value contracts redexes with
operands in $\mathsf{WNF}$ which include open neutrals. For instance, given
the input term redex $(\lambda y.z)(xN)$ the strategy delivers $z$ iff the
evaluation of $N$ converges on a $\mathsf{WNF}$.

Pure and applied666As explained in fn. 1 (p. 1) an applied calculus extends a
pure calculus with primitive terms and reduction rules for them. The applied
version of a pure strategy is its version in the applied calculus. one-step
equivalent versions of this strategy appear often in the literature under two
different sets of assumptions.

The first set consists of the following assumptions: _closed input terms_ ,
_weak evaluation_ (implicit in call-by-value) and the possibility of
_divergent terms_ (due to no typing or weak typing). The first two guarantee
that contracted redexes have no free variable and no open neutral operand.
This set of assumptions is the default in applied calculi modelling strict
functional programming languages where primitives and abstractions are
permissible operands. If we drop the primitives and the closed-input-terms
assumption then the strategy that remains is call-by-value as call-
by-$\mathsf{WNF}$, which evaluates redexes of closed input terms in the same
order.

This first set of assumptions has been canonical since the applied evaluator
in [Lan64, p. 316] and the SECD abstract machine [Lan64][FH88, Chp. 10] of the
ISWIM programming language [Lan65]. We find the assumptions in the big-step
evaluator ‘$\mathrm{eval}_{V}$’ and the small-step evaluator ‘$\to_{V}$’ of
[Plo75] that correspond to SECD (see Appendix B). We also find the assumptions
in evaluators that work with deeply-embedded terms that are either named
‘call-by-value’ [FF86] [FH88, Chp. 9] [Rea89, Chp. 13] [Mac90, Chps. 11–12]
[Ses02, pp. 421, 427] or have other names such as eval [Pau96, p. 390] or
‘inner machine’ [PR99, p. 17].

The second set consists of the only assumption of _convergent terms_ by
language restrictions and strong typing. The closed-input-terms assumption is
dropped (terms can be open) and weak-evaluation can be also dropped to
consider full-reducing call-by-value strategies. Type systems of programming
languages are mostly derived from System F [Car97, Pie02] and are sound for
full-reducing strategies but restricted to weak-reducing strategies [SR15, p.
3]. With stronger type systems that deliver type-erased convergent terms, the
weak-reducing call-by-$\mathsf{WNF}$ strategy works verbatim, as do full-
reducing call-by-value strategies of the pure lambda calculus that we show in
the survey. An exponent of this assumption is [GL02] which we discuss further
in Sections 5.7 and 6. It presents a full-reducing call-by-value eval-readback
evaluator called ‘strong reduction’ and denoted by $\mathcal{N}$ [GL02, p.
237]. The evaluator is developed in the context of a proof-assistant
implementation. It is defined on type-erased pure terms that are ‘strongly-
normalising’.777A term is strongly-normalising when all its evaluation
sequences converge on a normal form [Bar84]. Evaluation order is irrelevant
for such convergent terms except in the presence of effects. It uses for its
eval stage a weak-reducing evaluator $\mathcal{V}$ [GL02, p. 236] that
implements call-by-value as call-by-$\mathsf{WNF}$. To be precise,
$\mathcal{V}$ evaluates operands of neutrals right-to-left, so the equivalence
with call-by-$\mathsf{WNF}$ is modulo commuting redexes.888The result
delivered by $\mathcal{V}$ is a $\mathsf{WNF}$, not a $\mathsf{HNF}$ as stated
in [GL02, p. 236]. Both $\mathcal{V}$ and $\mathcal{N}$ are proven correct for
strongly-normalising terms [GL02, Lems. 5 & 6, pp. 237–9].

Another typed setting with convergent terms where the call-by-value strategies
of the pure lambda calculus are correct is the simply-typed lambda calculus
extended with primitives restricted to terminating structural recursion. In
this calculus self-application does not type-check, nor divergent terms built
from it [Pie02].

Call-by-value as call-by-$\mathsf{WNF}$ must not be confused with the call-by-
value strategy of the applied _lambda-value calculus_ of [Plo75]. The latter
strategy as defined by the big-step evaluator ‘$\mathrm{eval}_{V}$’ [Plo75, p.
130] is one-step equivalent to call-by-$\mathsf{WNF}$ under the first set of
assumptions, as already mentioned above. However, ‘$\mathrm{eval}_{V}$’ is a
strategy of a different calculus with a restricted beta-rule. The lambda-value
calculus is the basis of other applied call-by-value calculi [FF86, Mog91,
Wad03, CH00, KMR21, AG22]. Discussions about the pure version of lambda-value,
its operational and denotational theory, and its full-reducing strategies can
be found among others in [EHR91, EHR92, PR99, RP04, AP12, CG14, GPN16, KMR21,
AG22].

In this paper, the strict strategy space we study is the pure lambda
calculus’s, which includes call-by-value as call-by-$\mathsf{WNF}$ and its
full-reducing relatives. An alternative strict space consists of strategies
that simulate in the pure lambda calculus the strategies of the lambda-value
calculus. However, this strict space must be studied in pure lambda-value
itself together with the non-strict strategies that can be simulated in that
strict calculus [Plo75, Sec. 6]. As discussed in Section 1.2(1), we consider
the pure lambda calculus as a basis from which to consider additional
assumptions. For interested readers, in Appendix B we provide more details on
the similarities and differences with the lambda-value calculus.

##  4\. The eval-apply evaluator style

An evaluator in eval-apply style is defined by a single eval function that
recursively evaluates subterms and relies on a mutually-recursive local apply
function for the specific evaluation of application terms. As explained in
Section 1.2(1), we use a deep embedding of lambda-calculus terms into Haskell
where lambda-calculus variables are represented by strings.

      data Term = Var String | Lam String Term | App Term Term

We implement capture-avoiding substitution directly (and thus inefficiently)
according to the textbook definition [HS08]. The implementation details are
unimportant.999For interested readers, our string variables have trailing
numbers (_e.g._ "x1", "y5", etc.). Function subst pattern-matches on its third
argument and obtains fresh variables by incrementing the largest trailing
number of all the string variables of all its inputs.

      subst :: Term -> String -> Term -> Term
      subst n x b = ...  -- substitute n for x in b.

The following evaluator, named bv, implements in traditional eval-apply style
the call-by-value strategy described in words in Section 3.

      bv :: Term -> Term
      bv v@(Var _)   = v
      bv l@(Lam _ _) = l
      bv (App m n)   = apply (bv m) (bv n)
        where apply :: Term -> Term -> Term
              apply (Lam x b) n’ = bv (subst n’ x b)
              apply m’        n’ = App m’ n’

The evaluator pattern-matches on the input term. For variables (first clause)
and abstractions (second clause) it behaves as an identity. We use Haskell’s
‘as-patterns’ to simplify the code. For applications (third clause), the local
apply function is called with recursive calls to bv on the operator and the
operand. The local apply pattern-matches on the operator to evaluate it. Its
first clause evaluates the redex and its second clause evaluates the neutral.

The local apply can be anonymised in let and case expressions:

      bv :: Term -> Term
      bv v@(Var _)   = v
      bv l@(Lam _ _) = l
      bv (App m n)   = let m’ = bv m in case m’ of
                         (Lam x b) -> let n’ = bv n in bv (subst n’ x b)
                         _         -> let n’ = bv n in App m’ n’

The two let expressions for the operand n’ could be simplified or omitted
(substituting bv n for n’) but they will prove handy when we compare
evaluators and generalise in Section 7.

Readers familiar with Haskell will notice that bv actually does _not_
implement call-by-value due to the classic ‘semantics-preservation’ problem of
evaluators [Rey72]: the evaluation order of function and value-constructor
application (non-strict call-by-need) in the implementation language (Haskell)
does not match the evaluation order of function and term application (strict)
in the object language (pure lambda calculus). Concretely, the operand n’,
which is bound to the call bv n in the let expression, is passed _unevaluated_
to subst which does not demand its evaluation unless x occurs in b. Thus, for
example, if we pass to bv the input term $(\lambda x.z)\mathbf{\Omega}$ as an
expression of type Term, then the evaluator wrongly delivers $z$ (as Var "z").

In a strict implementation language, such as Standard ML or OCaml, where
function and value-constructor application are strict, the n’ parameter would
be evaluated before being passed to subst. This would also work fine for
evaluators that implement non-strict strategies such as, say, call-by-name
(Section 5.2), because in that case n’ would be bound to a term (a data-type
value) rather than to an evaluator call expression like bv n.

The problem with the strictness of subst is compounded by the _partially-
defined_ values of type Term. This type represents terms of $\Lambda$ with the
addition of the totally-undefined value $\bot$ and of partially-defined values
such as Lam "x" $\bot$, App $\bot\leavevmode\nobreak\ \bot$, etc. The first is
fine because we want to consider non-terminating strategies whose evaluators
deliver $\bot$. The second have no counterpart in $\Lambda$. It is the case
that every evaluator ev is strict, that is, ev $\bot$ = $\bot$, because it
pattern-matches on its input term. It is the case that an evaluator may not
terminate for an input term t, namely, ev t = $\bot$. However, we must avoid
ev t = p for some partially-defined term p. This can be avoided using strict
function application during evaluation.

###  4.1. Monadic style eval-apply

Strict function application can be simulated in Haskell using the principled
and flexible monadic style. We use the Haskell 2010 standard which has a well-
defined static and operational semantics (Appendix D). Evaluators are one of
the motivating applications of monads [Wad92b, Wad92a], and monadic evaluators
can be program-transformed to other operational semantics devices [ADM05].
Monads are provided in the Haskell 2010 library by means of the Monad type
class and its datatype instances. Type classes have a trivial dictionary
operational semantics [HHPW96]. The Monad type class provides operators for
monadic identity (`return`), monadic function application (`=<<`), and monadic
function composition (`<=<`), called Kleisli composition. The first two
operators are defined by programmers for the particular monad instance.
Monadic function composition is defined in the library in terms of monadic
function application. For comparison, we show in Figure 2 the type signatures
alongside ordinary identity, function application, and function composition.

      -- Identity
      id     ::            a ->   a
      return :: Monad m => a -> m a

      -- Application
      ($)   ::            (a ->   b) ->   a ->   b
      (=<<) :: Monad m => (a -> m b) -> m a -> m b

      -- Composition
      (.)   ::            (b ->   c) -> (a ->   b) -> (a ->   c)
      (<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)

      (g . f) x   = let y = f x
                    in g y

      (g <=< f) x = do y <- f x
                       g y

Figure 2. Type signatures of monadic operators alongside their ordinary
counterparts. Monadic function composition is defined in terms of monadic
function application. The do-notation is syntactic sugar for the latter.

Strict function application can be simulated by monadic application [Wad92a,
Sec. 3.2] when $\mathtt{return}\>\bot=\bot$ and
$\mathtt{f}\>\verb!=<<!\>\bot=\bot$ for any f, which is the case for some
strict monads,101010This is the case in Haskell 2010 but the latest Monad
class at the time of writing is a subclass of Functor and Applicative which
are not in the 2010 standard. Moreover, the Functor laws use non-strict
composition [Wad92a, Sec. 3.2]. To use Haskell in this setting we would have
to define an alternative strict monadic composition. In particular, we will
use the IO monad because we are interested in printing the results of
evaluation. (We will use monadic composition later on when we discuss eval-
readback evaluators in Section 6).

The monadic style has several benefits. First, we can keep Haskell which is
our preferred choice of implementation language for, among other things, its
convenient syntax for writing the generic evaluators and their fixed-points in
Sections 7.1.1 and 7.1.2. Second, we can keep subst non-monadic. Third, we can
toggle between strict and non-strict Haskell evaluation by instantiating the
evaluator’s type signature with strict and non-strict monad instances. The
non-strict Haskell evaluation of strict strategies like bv can be helpful in
iterative tracing up to particular depths [Ses02] to locate divergence points,
known in vernacular as ‘chasing bottoms’ [DJ04]. The parametrisation on a
monad type parameter requires the ‘arbitrary rank polymorphism’ type-checking
extension of the Glorious Haskell Compiler (GHC) which falls outside the
Haskell 2010 standard. Nevertheless, the extension has no run-time effect, as
it simply allows GHC to overcome the limitations of the default type-inference
algorithm by letting programmers provide type signature annotations for
perfectly type-checkable code. Hereafter, we write evaluators in monadic style
with a monad type parameter, but bear in mind that it is optional and
irrelevant for the results presented in the paper.

The transcription of the naive bv evaluator to monadic style is immediate with
Haskell’s do-notation:

      bv :: Monad m => Term -> m  Term
      -- may assume    Term -> IO Term
      bv v@(Var _)   = return v
      bv l@(Lam _ _) = return l
      bv (App m n)   = do m’ <- bv m
                          case m’ of
                            (Lam x b) -> do n’ <- bv n
                                            bv (subst n’ x b)
                            _         -> do n’ <- bv n
                                            return (App m’ n’)

The type of bv is bounded-quantified on a monad type parameter m, which can be
instantiated to a strict or non-strict monad instance using a type annotation
when executing the evaluator, _e.g._ (bv :: IO Term) t. If we wish, we can
assume m already instantiated to the IO monad, as shown in the comment. Notice
that m also occurs as a value variable (operator m) on the third clause for
applications. This is usual Haskell coding style, as type and value variables
have independent scopes.

The use of Haskell, monadic style, and strict monad instances are not required
for the proof by LWF. Haskell 2010 is used as a vehicle for communication and,
at any rate, we could treat all our code as convenient syntactic sugar for a
strict implementation language. LWF is a simple, syntactic, and non-invertible
transformation that only requires evaluators to be strict on their first
parameter (Appendix C), which is the case for every evaluator because the
first parameter is the input term. LWF does not involve equational reasoning,
although monadic equational reasoning in Haskell is perfectly possible, _e.g._
[GH11]. The LWF proof presented in this paper can be obtained using a strict
implementation language with non-monadic code (as demonstrated in [GPN14] for
two plain evaluators) or with monadic code.

###  4.2. Natural semantics style eval-apply

A natural semantics is a proof-theory of syntax-directed and deterministic
(exhaustive and non-overlapping) inference rules [Kah87]. Every rule has zero
or more antecedent formulas shown in order (left-to-right) above a line and
only one consequent formula shown below the line. Every rule states that the
formula below is the case if all formulas above are the case. A rule with no
formulas above is an axiom. A formula holds iff a stacking up of rules (an
evaluation tree) ends in axioms.

An eval-apply evaluator in natural semantics consists of a set of inference
rules that specify the evaluator’s behaviour recursively on the subterms. The
call-by-value evaluator ${\mathsf{bv}}$ below is defined in natural semantics
by four rules: one for evaluating variables, one for evaluating abstractions,
one for evaluating applications which unfold to a redex to be contracted, and
one for evaluating applications which unfold to neutrals. *[left=var] bv(x) =
x *[left=abs] bv(λx.B) = λx.B *[left=con] bv(M) = λx.B bv(N) = N’
bv([N’/x](B)) = B’ bv(MN) = B’ *[left=neu] bv(M) = M’ M’ ／≡λx.B bv(N) = N’
bv(MN) = M’N’Every formula of the form ${\mathsf{bv}}(M)=N$ reads ‘$N$ is the
result in the finite evaluation sequence of $M$ under ${\mathsf{bv}}$’. The
formula is proven by the finite evaluation tree above it. When
${\mathsf{bv}}(M)$ has an infinite evaluation sequence (${\mathsf{bv}}$
diverges on $M$) then it has an infinite evaluation tree and we write
${\mathsf{bv}}(M)=\bot$ to indicate it. (The symbol ‘$\bot$’ is meta-notation
because $\bot\not\in\Lambda$.)

Let us explain the rules. The var axiom states that ${\mathsf{bv}}$ is an
identity on variables (they are normal forms). The abs axiom states that
${\mathsf{bv}}$ is also an identity on abstractions (${\mathsf{bv}}$ is
‘weak’). The con rule states that the application $MN$ evaluates by
${\mathsf{bv}}$ to a term $B^{\prime}$ if ${\mathsf{bv}}$ evaluates the
operator $M$ to an abstraction with body $B$, and also evaluates the operand
$N$ to a term $N^{\prime}$, and also evaluates the contractum to a result
$B^{\prime}$. The neu rule states that the application $MN$ evaluates by
${\mathsf{bv}}$ to a neutral $M^{\prime}N^{\prime}$ if ${\mathsf{bv}}$
evaluates the operator $M$ to a non-abstraction $M$’ (_i.e._ a variable or a
neutral), and also evaluates the operand $N$ to a result $N^{\prime}$. The
eval-apply natural semantics corresponds with the eval-apply evaluator in
code, where the con and neu rules are implemented by apply.

In rule con, the contractum’s occurrence within the ${\mathsf{bv}}$ function
is a notational convenience. The contractum can be placed as a premise right
before the last premise that evaluates it. *[left=con]*⋮bv(M) = λx.B *⋮bv(N) =
N’ [N’/x](B) ≡B’ *⋮bv(B’) = B” bv(MN) = B” With this modification it is easier
to illustrate the connection between an evaluation tree and an evaluation
sequence. The latter can be obtained by the in-order traversal of the con
rules in an evaluation tree. The in-order traversal of the con rule is as
follows: in-order traversal of the stacked evaluation tree (vertical dots)
above the first and then above the second premises, contractum premise in the
middle, followed by the in-order traversal of the stacked evaluation tree
above the last premise. The redex is obtained from the abstractions and
operands. Figure LABEL:fig:example-nat-sem illustrates with an example.

##  5\. A survey of the pure lambda calculus’s strategy space

This section provides a survey of pure lambda calculus strategies, their
properties (some of which are features of their definition and serve as
classification criteria), some of their abstract machines, and some of their
uses to illustrate the properties. The strategies are defined through their
canonical eval-apply evaluators in natural semantics. For ease of reference,
all the evaluators are collected in two figures. Figure 4 (page 4) shows the
evaluators for the main well-known strategies in the literature. Figure 5
(page 5) shows the evaluators for less known but equally important strategies.
The last three are novel and of particular interest. We discuss each
evaluator/strategy in a separate section. With the exception of the novel
strategies, the details discussed in the survey are known and can be found in
the cited literature. Readers are under no obligation to read the whole
survey. It can be read cursorily with particulars fetched on demand when
reading about the structuring of the strategy space (Section 7). The role of
the survey is to illustrate a varied strategy space that is nonetheless
determined by a few variability points. The survey is thus wide in strategies
but not deep in strategy details because its scope is restricted to what is
needed for the structuring. A summary can be found at the end of the survey
(Section 5.14).

All evaluators are defined in natural semantics by four rules named var, abs,
con and neu which have been explained in Section 4.2. We omit the var rule in
the figures because every evaluator is an identity on variables. We also omit
the rule names because we always show them in order (abs, con, and neu) from
left to right, top to bottom. The con and neu rules are related by their first
premises. In all the con rules the first premise has the form
${\mathsf{ea}}(M)=\lambda x.B$ (here ${\mathsf{ea}}$ is a generic name for
eval-apply evaluator) which states that the operator $M$ evaluates to an
abstraction. In all the neu rules the first and second premises respectively
have the form ${\mathsf{ea}}(M)=M^{\prime}$ and $M^{\prime}\not\equiv\lambda
x.B$ which state that the operator $M$ does not evaluate to an abstraction.

The first six evaluators in Figure 4 and the first two in Figure 5 are
discussed in [Ses02] which classifies strategies according to three criteria:
weakness, strictness, and kind of final result. The present survey can be seen
as an extension of that work where we add more strategies, properties,
classification criteria, and background. In particular, we indicate whether
the evaluators are in uniform or hybrid _style_ , and whether they are
_balanced_ hybrid (Section 1.3.C4). In Section 7 we will confirm that all the
uniform-style and hybrid-style evaluators in the survey respectively define
uniform and hybrid strategies.

Call-by-value (${\mathsf{bv}}$) or call-by-$\mathsf{WNF}$:

bv(λx.B) = λx.B bv(M) = λx.B bv(N) = N’ bv([N’/x](B)) = B’ bv(MN) = B’ bv(M) =
M’ M’ ／≡λx.B bv(N) = N’ bv(MN) = M’N’

Call-by-name (${\mathsf{bn}}$):

bn(λx.B) = λx.B bn(M) = λx.B bn([N/x](B)) = B’ bn(MN) = B’ bn(M) = M’ M’
／≡λx.B bn(MN) = M’N

Applicative order (${\rm Appl.\leavevmode\nobreak\ Opt.}$) or call-
by-$\mathsf{NF}$:

Appl. Opt.(B) = B’Appl. Opt.(λx.B) = λx.B’ Appl. Opt.(M) = λx.B Appl. Opt.(N)
= N’ Appl. Opt.([N’/x](B)) = B’ Appl. Opt.(MN) = B’ Appl. Opt.(M) = M’ M’
／≡λx.B Appl. Opt.(N) = N’ Appl. Opt.(MN) = M’N’

Normal order (${\mathsf{no}}$):

no(B) = B’no(λx.B) = λx.B’ bn(M) = λx.B no([N/x](B)) = B’ no(MN) = B’ bn(M) =
M’ M’ ／≡λx.B no(M’) = M” no(N) = N’ no(MN) = M” N’

Head reduction (${\mathsf{hr}}$):

hr(B) = B’hr(λx.B) = λx.B’ bn(M) = λx.B hr([N/x](B)) = B’ hr(MN) = B’ bn(M) =
M’ M’ ／≡λx.B hr(M’) = M” hr(MN) = M”N

Head spine (${\mathsf{he}}$):

he(B) = B’he(λx.B) = λx.B’ he(M) = λx.B he([N/x](B)) = B’ he(MN) = B’ he(M) =
M’ M’ ／≡λx.B he(MN) = M’N

Strict normalisation (${\mathsf{sn}}$):

sn(B) = B’ sn(λx.B) = λx.B’ bv(M) = λx.B bv(N) = N’ sn([N’/x](B)) = B’ sn(MN)
= B’ bv(M) = M’ M’ ／≡λx.B sn(M’) = M” sn(N) = N’ sn(MN) = M”N’

Figure 4. Canonical eval-apply evaluators in natural semantics for the
foremost strategies in the literature.

###  5.1. Call-by-value $({\mathsf{bv}})$

We have already discussed this strategy and its eval-apply evaluator
${\mathsf{bv}}$ in Sections 3 and 4. The strategy is named call-by-value where
‘value’ means ‘weak normal form’ (call-by-$\mathsf{WNF}$ for short). It
chooses the leftmost-innermost redex not inside an abstraction. It is weak,
strict, non-head, and incomplete (because it is strict, Appendix E). It
delivers weak normal forms as results. The call-by-value evaluator
(${\mathsf{bv}}$) is defined in uniform style. The strategy is uniform.

As discussed in Section 3, the SECD abstract machine [Lan64][FH88, Chp. 10]
implements an applied version of call-by-value as call-by-$\mathsf{WNF}$ when
input terms are closed [Ses02, p 421]. The CAM abstract machine [CCM84][FH88,
Chp. 13] ultimately implements call-by-value like SECD. The ZAM abstract
machine of the ZINC project [Ler91] implements the weak evaluator
$\mathcal{V}$ mentioned in Section 3, which evaluates neutral operands right-
to-left and is thus one-step equivalent to call-by-value (${\mathsf{bv}}$)
modulo commuting redexes. The CEK abstract machine [FF86] is related to the
call-by-value strategy defined by the ‘$\mathrm{eval}_{V}$’ big-step evaluator
of the lambda-value calculus [Plo75]. The seminal framework for environment-
based call-by-value abstract machines for a calculus of closures can be found
in [Cur91, BD07]. In [BD07], the name ‘call-by-value’ is reserved for the
abstract machine whereas the strategy is called ‘applicative-order’. However,
‘applicative order’ is usually used for the full-reducing call-by-value (call-
by-$\mathsf{NF}$) strategy of the pure lambda calculus (Section 5.3).
Traditionally, environment-based abstract machines correspond with calculi
with closures or explicit substitutions. In [ABM14], the authors use the
linear substitution calculus to vanish some machine transitions and ‘distill’
abstract machines from the calculus while preserving the time complexity of
the execution.

###  5.2. Call-by-name $({\mathsf{bn}})$

This strategy chooses the leftmost-outermost redex not inside an abstraction.
It is weak, non-strict, head, and delivers (and is complete for) weak head
normal forms ($\mathsf{WHNF}$ in Figure 1). These consist of variables and
non-evaluated abstractions and neutrals.

The abs rule does not evaluate abstractions (weak). The con rule evaluates the
operator to an abstraction (goes left) and then the operand $N$ is passed
unevaluated (non-strict ‘by name’) to the substitution. The neu rule also
leaves the neutral’s operand $N$ unevaluated (head), as if the head variable
were a non-strict data-type value constructor. The call-by-name evaluator
(${\mathsf{bn}}$) is defined in uniform style. The strategy is uniform.

The presence of rule neu marks the difference with the call-by-name strategy
of applied versions of the pure lambda calculus for modelling programming
languages where open terms are disallowed. As pointed out in [Ses02, p. 425],
it is well-known that with closed input terms call-by-name (${\mathsf{bn}}$)
is identical to those strategies and to the big-step evaluator
‘$\mathrm{Eval}_{N}$’ of [Plo75]. The latter does not consider neutrals.
Interestingly, the small-step call-by-name evaluator ‘$\to_{N}$’ does evaluate
neutrals [Plo75, p. 146, 4th rule] but to a limited extent, as also pointed
out in [Ses02, p. 421]. For example, $x\,((\lambda z.z)\,v)$ evaluates to
$x\,v$ but $x\,y\,((\lambda z.z)\,v)$ is a stuck term. The
‘$\mathrm{Eval}_{N}$’ and ‘$\to_{N}$’ evaluators are one-step equivalent
(proven on paper [Plo75, Thm. 2, p. 146], not by program transformation) under
the assumption of closed input terms.

Call-by-name is the basis for the call-by-need evaluation mechanism of non-
strict functional programming languages (broadly, call-by-name with sharing
and memoisation [FH88, Chp. 11]). The seminal framework for environment-based
call-by-name abstract machines for a calculus of closures can be found in
[Cur91, BD07]. The Krivine abstract machine (KAM) [Kri07] implements call-by-
name and has been the inspiration for abstract machines of proof-assistants
which add capabilities for full-reduction on KAM, although there exist full-
reducing versions of KAM (Section 5.4).

###  5.3. Applicative order $({\rm Appl.\leavevmode\nobreak\ Opt.})$

This strategy chooses the leftmost-innermost redex (whether or not inside an
abstraction). It is non-weak, strict, non-head, full-reducing, and incomplete.
It delivers normal forms as results ($\mathsf{NF}$ in Figure 1).

The abs rule does evaluate abstractions (non-weak). The con rule evaluates the
operator to an abstraction in $\mathsf{NF}$ (goes left), then the operand to
$\mathsf{NF}$ (strict), and then the contractum to $\mathsf{NF}$. The neu rule
evaluates the operator to $\mathsf{NF}$ (goes left), and then the operand to
$\mathsf{NF}$ (non-head). The applicative order evaluator (${\rm
Appl.\leavevmode\nobreak\ Opt.}$) is defined in uniform style. The strategy is
uniform.

Because applicative order evaluates operands to normal form before
contraction, it is sometimes referred to as ‘call-by-value’ where value means
‘normal form’ (‘call-by-normal-form’ or call-by-$\mathsf{NF}$ for short). It
should not be called ‘call-by-value’ in applied versions of the pure lambda
calculus for modelling programming languages because functions are not
evaluated and the corresponding strategy is call-by-value (Section 5.1). As a
historical curiosity, applicative order is called ‘standard order’ in [FH88,
Chp. 6] perhaps because evaluating operands before contraction was somehow
considered standard. However, ‘standard’ has a technical meaning in reduction
(Section 5.4) which does not apply to applicative order. An early abstract
machine for applicative order based on a modification of the SECD abstract
machine can be found in [McG70].

Applicative order illustrates that weakness and strictness are separate
classification criteria, and that the notion of ‘value’ is determined by the
properties of the strategy that determine how operands of redexes are
evaluated.

###  5.4. Normal order $({\mathsf{no}})$

This strategy chooses the leftmost-outermost redex. It is non-weak, non-
strict, non-head, full-reducing, and delivers (and is complete for) normal
forms ($\mathsf{NF}$). In the lambda-calculus literature, a leftmost-outermost
redex is simply called ‘leftmost’ and normal order is called ‘leftmost
reduction’ [CF58, HS08, Bar84]. Note that call-by-name (${\mathsf{bn}}$) is
another leftmost strategy, but does not evaluate leftmost redexes inside
abstractions.

The abs rule evaluates abstractions (non-weak). The con rule is more
sophisticated. Given an application $MN$, normal order evaluates the operator
$M$ first (goes left), but when the operator evaluates to an abstraction
$\lambda x.B$ then the application $(\lambda x.B)N$ is the leftmost-outermost
redex to be contracted. Normal order must not evaluate the abstraction body
$B$. That would be going innermost, like applicative order. Normal order
contracts the outermost redex $(\lambda x.B)N$ passing $N$ unevaluated to the
substitution (non-strict). To avoid the full evaluation of abstractions in
operator position, normal order relies on the weak call-by-name strategy
(${\mathsf{bn}}$) as subsidiary. Finally, the neu rule evaluates the operator
further and also evaluates the operand (non-head), because the aim is to
deliver a normal form.

The normal order evaluator (${\mathsf{no}}$) is hybrid in style, and it is
balanced, as it evaluates applications $MN$ in rule con before contraction
(substitution) as much as its subsidiary call-by-name (${\mathsf{bn}}$). The
strategy is balanced hybrid.

Normal order is the ‘standard’ full-reducing and complete strategy of the pure
lambda calculus, both in the colloquial sense (it is the _de facto_ strategy
used for full evaluation in the calculus) and in the technical sense (roughly,
it does not evaluate a redex to the left of the one just contracted [Bar84,
HS08]). Due to the possibility of non-termination, normal order is a semi-
decision procedure for the ‘has-a-normal-form’ property of terms. Because
normal order is non-weak, it is inaccurate to refer to it as call-by-name in
applied versions of the pure lambda calculus for modelling programming
languages where functions are unevaluated. To our knowledge, no programming
language has normal order as its evaluation strategy. It would evaluate
functions non-strictly and value constructors strictly (no partially-defined
terms). The opposite, strict function evaluation with non-strict value
constructors was used by the Hope programming language [FH88].

The abstract machine KN [Cré07] implements normal order in lockstep [GPN19].
KN is the full-reducing version of the KAM machine mentioned in Section 5.2.
In [ABM15], the authors present a KN-based full-reducing abstract machine with
a global environment (the Strong Milner Abstract Machine) using the
‘distillery’ approach from the linear substitution calculus mentioned in
Section 5.1. The underlying strategy, ‘linear leftmost-outermost reduction’ is
a refinement of normal order and an extension of linear head reduction [DR04].

As motivated in Section 1.3.C1, we illustrate normal order’s evaluation
properties in the evaluation of general recursive functions on Church
numerals. Because normal order is full-reducing and complete, it delivers
Church numeral results in their original representation as normal forms. For
illustration we use the typical factorial example.111111The factorial function
is actually _primitive_ recursive, but the discussion applies to any _general_
recursive function. The boldface terms denote the Church-encoded intended
arithmetic functions and constants.

$\mathbf{F}\equiv\lambda f.\lambda
n.\,\mathbf{Cond}\,(\mathbf{IsZero}\,n)\,\mathbf{One}\,(\mathbf{Mult}\,n\,(f\,(\mathbf{Pred}\,n)))$

Given a Church numeral $\mathbf{n}$, the evaluation of
$(\mathbf{Y}\,\mathbf{F}\,\mathbf{n})$ under ${\mathsf{no}}$ delivers the
Church numeral for the factorial of $\mathbf{n}$. The term $\mathbf{Y}$ is the
standard non-strict fixed-point combinator (Appendix A). The weak-reducing
strategies we have discussed can also be used but they deliver terms with
unevaluated ‘recursive’ calls. Applicative order cannot be used because it
evaluates every subterm fully to normal form, including the fixed-point
combinators which have no normal form. Strict strategies require other
combinators and encodings. We defer this discussion to Section 5.7.

###  5.5. Head reduction $({\mathsf{hr}})$

This strategy, defined in [Wad76, p. 504], chooses the head redex, _i.e._ the
redex that occurs in head position (Appendix A). It is a non-weak, non-strict,
and head strategy that delivers (and is complete for) head normal forms
($\mathsf{HNF}$ in Figure 1). These are approximate normal forms where
neutrals are unevaluated. The head redex is in left position and thus head
reduction is also a ‘leftmost’ strategy, concretely, an approximation of
leftmost normal order.

The abs rule evaluates abstractions (non-weak). Like normal order, head
reduction relies on weak call-by-name (${\mathsf{bn}}$) as subsidiary in rules
con and neu to avoid the evaluation of abstractions in operator position.
Unlike normal order, head reduction does not evaluate neutrals (head). Indeed,
normal order and head reduction differ only in rule neu. The difference can be
expressed in jest: unlike head reduction, normal order lost is head in pursuit
of the normal form. Like normal order (${\mathsf{no}}$), head reduction
(${\mathsf{hr}}$) is a balanced hybrid evaluator and strategy.

Head reduction is a semi-decision procedure for the ‘useful-as-a-function’
property of terms, called ‘solvability’ in the jargon [Wad76, Bar84]. Solvable
terms consist of terms that evaluate to $\mathsf{NF}$ as well as terms that do
not evaluate to $\mathsf{NF}$ but may deliver a $\mathsf{NF}$ when used as
functions on suitable operands.

###  5.6. Head spine $({\mathsf{he}})$

This strategy, defined in [BKKS87, p. 209], is the first _spine_ strategy in
the survey. Spine strategies are non-strict and go under lambda just enough to
uphold completeness (Appendix E). They evaluate the term’s spine when
depicting the term as a tree. They are big-step equivalent to a leftmost
strategy but evaluate operators more eagerly to and yet are complete for
$\mathsf{HNF}$. Concretely, spine strategies evaluate operators to
$\mathsf{HNF}$ whereas their big-step equivalent leftmost strategies evaluate
operators to less evaluated $\mathsf{WHNF}$. The leftmost counterpart of head
spine (${\mathsf{he}}$) is head reduction (${\mathsf{hr}}$). Both evaluate
only needed redexes to $\mathsf{HNF}$ in the same number of different steps.

Head spine is non-weak, non-strict, and head, and delivers (and is complete
for) $\mathsf{HNF}$s. The head spine evaluator (${\mathsf{he}}$) is uniform in
style. The strategy is uniform. The classic eval-apply evaluator headNF in
[Pau96, p. 390] literally implements the head spine ${\mathsf{he}}$ evaluator
in code (Section 6).

The more eager evaluation of an abstraction operator to $\mathsf{HNF}$ may
eliminate copies of the bound variable in the body and thus require less
copies of the operand. The trivial example is $(\lambda x.(\lambda y.\lambda
z.y)\,x\,x)N$. With head reduction the operand $N$ is copied twice. With head
spine the operator evaluates to $(\lambda x.x)$ and the operand $N$ is copied
once. But this need not always be the case, compare with $(\lambda
x.\mathbf{Y}x)N$, and the cost of copying is implementation dependent (Section
5.14).

###  5.7. Strict normalisation $({\mathsf{sn}})$

This strategy chooses the leftmost-innermost redex but it evaluates operators
to $\mathsf{WNF}$ using call-by-value (${\mathsf{bv}}$) as subsidiary. If the
result is an abstraction (rule con) then it also evaluates the redex’s operand
to $\mathsf{WNF}$ using call-by-value. The contractum is evaluated fully to
normal form. If the result is not an abstraction (rule neu) then it evaluates
the neutral fully to normal form. It evaluates abstractions fully to normal
form (rule abs).

Strict normalisation is non-weak, strict, non-head, full-reducing, and
incomplete. Like normal order (${\mathsf{no}}$), strict normalisation
(${\mathsf{sn}}$) is a balanced hybrid evaluator and strategy.

We introduced this strategy and its natural semantics evaluator in [GPN14, pp.
195-6] but under the name byValue because it is equivalent to the eval-
readback evaluator byValue in [Pau96, p. 390]. In turn, the byValue evaluator
is identical to the ‘strong reduction’ ($\mathcal{N}$) eval-readback evaluator
in [GL02, p. 237], save for the evaluation order of operands of neutrals
(left-to-right in byValue and right-to-left in $\mathcal{N}$). We discuss both
evaluators in detail in Section 6. Recall from Section 3 that $\mathcal{N}$ is
complete for convergent terms. Thus, byValue and ‘strict normalisation’
(${\mathsf{sn}}$) are also complete for convergent terms. The proof by LWF
will show that strict normalisation and byValue are one-step equivalent modulo
commuting redexes (Section 8).

As noted in [GPN14, Sec. 9], the byValue evaluator is a seminal definition of
a full-reducing call-by-value strategy of the pure lambda calculus. This
definition predates later ones such as $\mathcal{N}$ [GL02]. Abstract machines
for full-reducing call-by-value are scarce. The call-by-value abstract
machines SECD [Lan64][FH88, Chp. 10], CAM [CCM84][FH88, Chp. 13] and ZAM
[GL02] are weak-reducing. An abstract machine for a full-reducing call-by-
value strategy of the pure lambda calculus with right-to-left evaluation of
operands of neutrals _and_ of redexes is presented in [BBCD20], with its
performance improved in [BCD21]. Interestingly, the abstract machine is
obtained by deconstructing the normal order KN machine, using program
transformation and the concept of hybrid style. The machine uses a right-to-
left weak call-by-value subsidiary. The relation with right-to-left versions
of ‘strict normalisation’ and byValue (and $\mathcal{N}$) remains to be
explored.

A seminal full-reducing call-by-value strategy for the lambda-value calculus
of [Plo75] is defined by the abstract machine obtained as a instance of the
‘principal reduction machine’ of [RP04, p. 70]. A related full-reducing call-
by-value strategy, called ‘value normal order’, is presented in [GPN16, Sec.
7.1]. The latter differs from the former in that blocks are evaluated left-to-
right.

Strict normalisation can be used to evaluate general recursive functions on
Church numerals using the strict fixed-point combinator $\mathbf{Z}$ and
thunking ‘protecting by lambda’. Thunking [Ing61, DH92] consists in delaying
the evaluation of subterms that have recursive calls which may diverge. These
subterms are ‘serious’ in opposition to the ‘trivial’ subterms that converge
[Rey72, p. 382]. The serious subterms are delayed by placing them inside an
abstraction, hence ‘protecting by lambda’. To illustrate, take the following
thunked definition of the factorial function:

$\mathbf{F}\equiv\lambda f.\lambda
n.\,\mathbf{Cond}\,(\mathbf{IsZero}\,n)\,(\lambda v.\,\mathbf{One})\,(\lambda
v.\,\mathbf{Mult}\,n\,(f\,(\mathbf{Pred}\,n)))$

Given a Church numeral $\mathbf{n}$, the term
$(\mathbf{Z}\,\mathbf{F}\,\mathbf{n}\,\mathbf{T})$ evaluates under
${\mathsf{sn}}$ to the Church numeral for the factorial of $\mathbf{n}$. An
arbitrary closed term $\mathbf{T}$, _e.g._ the identity $\mathbf{I}$, can be
passed to unthunk. The serious subterm
$(\mathbf{Z}\,\mathbf{F})\,(\mathbf{Pred}\,n)$ is protected by the binding
$\lambda v$.

A continuation-passing style encoding is also possible using the identity as
initial continuation:

$\mathbf{F}\equiv\lambda f.\lambda
n.\,\mathbf{Cond}\,(\mathbf{IsZero}\,n)\,(\lambda
k.\,k\,\mathbf{One})\,(\lambda k.\,f\,(\mathbf{Pred}\,n)\,(\lambda
x.k\,(\mathbf{Mult}\,n\,x)))$

The serious subterm $(\mathbf{Z}\,\mathbf{F})(\mathbf{Pred}\,n)(\lambda
x.k\,(\mathbf{Mult}\,n\,x))$ is protected by $\lambda k$. At each step the
passed continuation $k$ is composed with the multiplication which is passed as
a new continuation $\lambda x.k(\mathbf{Mult}\,n\,x)$.

Hybrid normal order (${\mathsf{hn}}$):

hn(B) = B’hn(λx.B) = λx.B’ he(M) = λx.B hn([N/x](B)) = B’ hn(MN) = B’ he(M) =
M’ M’ ／≡λx.B hn(M’) = M” hn(N) = N’ hn(MN) = M”N’

Hybrid applicative order (${\mathsf{ha}}$):

ha(B) = B’ha(λx.B) = λx.B’ bv(M) = λx.B ha(N) = N’ ha([N’/x](B)) = B’ ha(MN) =
B’ bv(M) = M’ M’ ／≡λx.B ha(M’) = M” ha(N) = N’ ha(MN) = M”N’

Ahead machine (${\mathsf{am}}$):

am(B) = B’am(λx.B) = λx.B’ bv(M) = λx.B bv(N) = N’ am([N’/x](B)) = B’ am(MN) =
B’ bv(M) = M’ M’ ／≡λx.B am(M’) = M” bv(N) = N’ am(MN) = M”N’

Head applicative order (${\mathsf{ho}}$):

ho(B) = B’ho(λx.B) = λx.B’ ho(M) = λx.B ho(N) = N’ ho([N’/x](B)) = B’ ho(MN) =
B’ ho(M) = M’ M’ ／≡λx.B ho(MN) = M’N

Spine applicative order (${\mathsf{so}}$):

so(B) = B’so(λx.B) = λx.B’ ho(M) = λx.B so(N) = N’ so([N’/x](B)) = B’ so(MN) =
B’ ho(M) = M’ M’ ／≡λx.B so(M’) = M” so(N) = N’ so(MN) = M”N’

Balanced spine applicative order (${\mathsf{bs}}$):

bs(B) = B’bs(λx.B) = λx.B’ ho(M) = λx.B ho(N) = N’ bs([N’/x](B)) = B’ bs(MN) =
B’ ho(M) = M’ M’ ／≡λx.B bs(M’) = M” bs(N) = N’ bs(MN) = M”N’

Figure 5. Canonical eval-apply evaluators in natural semantics for less known
strategies.

###  5.8. Hybrid normal order $({\mathsf{hn}})$

Hereafter we discuss the evaluators in Figure 5 (page 5). Hybrid normal order
is non-weak, non-strict, non-head, full-reducing, and delivers (and is
complete for) normal forms ($\mathsf{NF}$). This strategy is presented in
[Ses02, p. 429] and given its name because it ‘is a hybrid of head spine
reduction and normal order reduction’. The word ‘hybrid’ is used here
informally but closely to the concept of dependence on a subsidiary evaluator,
what we call hybrid _style_ (Section 1.3.C4). The idea is that hybrid normal
order (${\mathsf{hn}}$) is obtained from normal order (${\mathsf{no}}$) by
replacing from the latter the subsidiary call-by-name (${\mathsf{bn}}$) by
head spine (${\mathsf{he}}$). More precisely, hybrid normal order is the spine
counterpart of leftmost normal order because it relies on a spine subsidiary
to evaluate operators up to $\mathsf{HNF}$, whereas normal order relies on a
leftmost subsidiary to evaluate operators to $\mathsf{WHNF}$ (Section 5.6).
Normal order is itself hybrid, so ‘hybrid normal order’ can be confusing, but
it is the original name given in [Ses02, p. 429] where ‘hybrid’ is part of the
name, not an adjective. Hybrid normal order (${\mathsf{hn}}$) is a balanced
hybrid evaluator and strategy.

The eval-apply hybrid normal order evaluator (${\mathsf{hn}}$) is one-step
equivalent to the classic eval-readback evaluator byName in [Pau96, p. 390]
(Section 6). This is proven by the LWF-transformation on evaluator
implementations of Section 8. (Recall from Section 5.6 that hybrid normal
order’s subsidiary, head spine (${\mathsf{he}}$), is literally implemented in
code by headNF which is the eval stage of the eval-readback evaluator byName
(Section 6).

###  5.9. Hybrid applicative order $({\mathsf{ha}})$

Hybrid applicative order is non-weak, strict, non-head, full-reducing,
incomplete, and delivers normal forms ($\mathsf{NF}$). This strategy is
presented in [Ses02, p. 428] and given its name because it ‘is a hybrid of
call-by-value and applicative order reduction’. The word ‘hybrid’ is used
again informally and closely to the concept of dependence on a subsidiary
evaluator, what we call hybrid _style_. Hybrid applicative order
(${\mathsf{ha}}$) relies on weak call-by-value (${\mathsf{bv}}$) as subsidiary
to evaluate operators, just like normal order (${\mathsf{no}}$) relies on weak
call-by-name (${\mathsf{bn}}$) as subsidiary for that. In short, hybrid
applicative order (${\mathsf{ha}}$) differs from applicative order (${\rm
Appl.\leavevmode\nobreak\ Opt.}$) in that it does not evaluate abstractions in
operator position. Although hybrid applicative order (${\mathsf{ha}}$) is
incomplete, it can find more normal forms than applicative order (${\rm
Appl.\leavevmode\nobreak\ Opt.}$) because it is less eager (less undue
divergence) and in fewer steps than normal order (${\mathsf{no}}$) because it
evaluates less duplicated redexes [Ses02].

Hybrid applicative order (${\mathsf{ha}}$) is a hybrid evaluator and strategy,
_but it is unbalanced_ : it evaluates operands of redexes _more_ than its
subsidiary ${\mathsf{bv}}$ because it calls itself recursively on the operand
rather than calling ${\mathsf{bv}}$. The assertion in [Ses02, p. 428] that
hybrid applicative order is equivalent to the classic eval-readback byValue
evaluator is thus incorrect: hybrid applicative order does not evaluate
operands of redexes using ${\mathsf{bv}}$ (Section 6).

Hybrid applicative order can be used to evaluate general recursive functions
on natural numbers with the same fixed-point combinator and thunking style
than strict normalisation (${\mathsf{sn}}$). But hybrid applicative order is
more eager on operands.

###  5.10. Ahead machine $({\mathsf{am}})$

This strategy is defined in [PR99, Def. 5.1]. It uses call-by-value
(${\mathsf{bv}}$) as subsidiary to evaluate operators and operands in redexes,
like strict normalisation (${\mathsf{sn}}$), but it also uses call-by-value to
evaluate neutrals. (Recall from Section 3 that in [PR99, p. 17] call-by-value
(${\mathsf{bv}}$) is called ‘inner machine’.) Ahead machine evaluates
abstractions using itself recursively.

Ahead machine is non-weak, strict, non-head, incomplete, and delivers so-
called ‘value head normal forms’ ($\mathsf{VHNF}$ in Figure 1) which are terms
in $\mathsf{WNF}\cap\mathsf{HNF}$. Ahead machine (${\mathsf{am}}$) is a
balanced hybrid evaluator and strategy. Although it is incomplete in the pure
lambda calculus, it is a semi-decision procedure for an approximate notion of
solvability in the pure lambda-value calculus [PR99].

###  5.11. Head applicative order $({\mathsf{ho}})$

This is a novel strategy. It is the natural head variation of applicative
order (${\rm Appl.\leavevmode\nobreak\ Opt.}$). Its rule structure is similar
to ${\rm Appl.\leavevmode\nobreak\ Opt.}$’s save for the neu rule where
neutrals are not evaluated. Head applicative order (${\mathsf{ho}}$) is non-
weak, strict, head, incomplete, and delivers head normal forms
($\mathsf{HNF}$). It is a uniform evaluator and strategy.

###  5.12. Spine applicative order $({\mathsf{so}})$

This is a novel strategy. It is non-weak, strict, non-head, full-reducing, and
incomplete, and delivers $\mathsf{NF}$s. It is the spine-ish counterpart of
hybrid applicative order (${\mathsf{ha}}$). Recall from Section 5.6 that spine
strategies, which live in the non-strict subspace, evaluate the term’s spine
and operators to $\mathsf{HNF}$. A spine strategy is big-step equivalent to a
leftmost strategy that evaluates operators to $\mathsf{WHNF}$. In the strict
space we cannot speak of spineness literally, because evaluated operands are
not in the term’s spine, but we think the spine analogy is pertinent when
operators are evaluated to $\mathsf{HNF}$ by a strict subsidiary. Spine
applicative order (${\mathsf{so}}$) evaluates operators to $\mathsf{HNF}$
using head applicative order (${\mathsf{ho}}$), whereas hybrid applicative
order (${\mathsf{ha}}$) evaluates operators to $\mathsf{WNF}$ using call-by-
value (${\mathsf{bv}}$). Spine applicative order (${\mathsf{so}}$) is a hybrid
strategy _but it is unbalanced_ : it evaluates operands of redexes _more_ than
its subsidiary by calling itself recursively.

Spine applicative order (${\mathsf{so}}$) is more eager than hybrid
applicative order (${\mathsf{ha}}$). It has several interesting features.
First, it is the _most eager_ hybrid strategy in the survey. Second, it
evaluates general recursive functions on Church numerals with thunking
‘protecting by variable’ (rather than ‘by lambda’), with delimited CPS
(continuation-passing style) [BBD05], and with the _non-strict_ fixed-point
combinator $\mathbf{Y}$. (Notice the contrast: ‘most eager’ and ‘non-strict
fixed-point’.) To illustrate, take the delimited-CPS definition of the
factorial function:

$\mathbf{F}\equiv\lambda f.\lambda n.\lambda
k.\,\mathbf{Cond}\,(\mathbf{IsZero}\,n)\,(k\,\mathbf{One})\,(k\,(f\,(\mathbf{Pred}\,n)\,(\mathbf{Mult}\,n)))$

Given a Church numeral $\mathbf{n}$, the term
$(\mathbf{Y}\,\mathbf{F}\,\mathbf{n}\,\mathbf{I})$ evaluates under
${\mathsf{so}}$ to the Church numeral for the factorial of $\mathbf{n}$. The
identity $\mathbf{I}$ is passed as the initial continuation. The variable $k$,
which stands for the delimited continuation, protects the ‘serious’ subterm
$(\mathbf{Y}\,\mathbf{F})\,(\mathbf{Pred}\,n)\,(\mathbf{Mult}\,n)$. In the
evaluation under ${\mathsf{so}}$ there are no administrative evaluation steps
resulting from a strict fixed-point combinator and from the composition of
continuations because they are used at each call, passing the multiplication
$(\mathbf{Mult}\,n)$ as a continuation to each serious subterm.

###  5.13. Balanced spine applicative order $({\mathsf{bs}})$

This is a novel strategy. It is a balanced hybrid variation of spine
applicative order (${\mathsf{so}}$) where the subsidiary, head applicative
order (${\mathsf{ho}}$), is employed to evaluate operands of redexes to
recover the balanced property. It is non-weak, strict, non-head, full-
reducing, incomplete, and delivers $\mathsf{NF}$s. Although it is less eager
than spine applicative order (${\mathsf{so}}$), balanced spine applicative
order (${\mathsf{bs}}$) can be used to evaluate general recursive functions in
the same fashion as ${\mathsf{so}}$.

###  5.14. Summary of the survey

Figure 6 (page 6) summarises the strategies, their properties, and their use
in evaluating general recursive functions. Applicative order (${\rm
Appl.\leavevmode\nobreak\ Opt.}$) is missing from the bottom table because, as
explained in Section 5.4, it evaluates every subterm fully to normal form,
including the fixed-point combinators which have no normal form, and thus it
defeats any thunking mechanism.

The four criteria of weakness, strictness, headness, and dependency on a less-
reducing subsidiary (hybridity) are the few variability points in the natural
semantics rules. Their configurations determine the strategy space. The staged
evaluation of the operator in rule neu is not a variability point as it is
subsumed by the uniform/hybrid configuration: only hybrid strategies use the
staged evaluation because they use the subsidiary to evaluate operators.

Strategies and properties
---
${\mathsf{bv}}$ | weak | strict | non-head |  to $\mathsf{WNF}$ | incomplete |  | uniform
${\mathsf{bn}}$ | weak | non-strict | head |  to $\mathsf{WHNF}$ | complete-for | leftmost | uniform
${\rm Appl.\leavevmode\nobreak\ Opt.}$ | non-weak | strict | non-head |  to $\mathsf{NF}$ | incomplete |  | uniform
${\mathsf{no}}$ | non-weak | non-strict | non-head |  to $\mathsf{NF}$ | complete-for | leftmost | hybrid bal.
${\mathsf{hr}}$ | non-weak | non-strict | head |  to $\mathsf{HNF}$ | complete-for | leftmost | hybrid bal.
${\mathsf{he}}$ | non-weak | non-strict | head |  to $\mathsf{HNF}$ | complete-for | spine | uniform
${\mathsf{sn}}$ | non-weak | strict | non-head |  to $\mathsf{NF}$ | incomplete |  | hybrid bal.
${\mathsf{hn}}$ | non-weak | non-strict | non-head |  to $\mathsf{NF}$ | complete-for | spine | hybrid bal.
${\mathsf{ha}}$ | non-weak | strict | non-head |  to $\mathsf{NF}$ | incomplete |  | hybrid
${\mathsf{am}}$ | non-weak | strict | non-head |  to $\mathsf{VHNF}$ | incomplete |  | hybrid bal.
${\mathsf{ho}}$ | non-weak | strict | head |  to $\mathsf{HNF}$ | incomplete |  | uniform
${\mathsf{so}}$ | non-weak | strict | non-head |  to $\mathsf{NF}$ | incomplete |  | hybrid
${\mathsf{bs}}$ | non-weak | strict | non-head |  to $\mathsf{NF}$ | incomplete |  | hybrid bal.

Big-step equivalence
---
Leftmost | Spine
${\mathsf{no}}$ | ${\mathsf{hn}}$
${\mathsf{hr}}$ | ${\mathsf{he}}$

Usage in evaluating general recursive functions
---
Strategy | Result | Combinator | Style | Thunking
${\mathsf{bn}}$ | $\mathsf{WHNF}$ | $\mathbf{Y}$ | direct style | none
${\mathsf{hr}}$, ${\mathsf{he}}$ | $\mathsf{HNF}$ | $\mathbf{Y}$ | direct style | none
${\mathsf{no}}$, ${\mathsf{hn}}$ | $\mathsf{NF}$ | $\mathbf{Y}$ | direct style | none
${\mathsf{bv}}$ | $\mathsf{WNF}$ | $\mathbf{Z}$ | direct style | protecting by lambda
${\mathsf{am}}$ | $\mathsf{VHNF}$ | $\mathbf{Z}$ | direct style | protecting by lambda
${\mathsf{sn}}$, ${\mathsf{ha}}$ | $\mathsf{NF}$ | $\mathbf{Z}$ | direct style | protecting by lambda
${\mathsf{ho}}$ | $\mathsf{HNF}$ | $\mathbf{Y}$ | delimited CPS | protecting by variable
${\mathsf{so}}$, ${\mathsf{bs}}$ | $\mathsf{NF}$ | $\mathbf{Y}$ | delimited CPS | protecting by variable

Figure 6. Summary of strategies, properties, and use in evaluating general
recursive functions.

Each strategy has its uses which depend on the context. As mentioned in
Section 1.2(1), there is no optimal strategy in terms of time (_e.g._
contraction counts) or space (_e.g._ term size) because there are terms for
which any strategy duplicates work [Lév78, Lév80, Lam89, AG98]. And
optimisations are implementation dependent, particularly on term
representation. For example, we implement evaluators in Haskell where we can
share our deeply-embedded terms:

        m :: Term
        m = App n n
        where n :: Term
              n = ... -- some large term

There is only a copy of n in m. The evaluation of ev m does not overwrite m
because they are different Haskell expressions. The first may be memoised but
the second remains intact. We have left efficiency considerations aside
because the particulars constrain the strategy space.

We end this summary drawing the reader’s attention to a symmetry which may be
related to the notion of duality [CH00]. Call-by-name (${\mathsf{bn}}$) and
call-by-value (${\mathsf{bv}}$) are uniform and weak-reducing. These
strategies are respectively used as subsidiaries by hybrid and full-reducing
normal order (${\mathsf{no}}$) and strict normalisation (${\mathsf{sn}}$).
Normal order uses call-by-name as subsidiary on operators. Strict
normalisation uses call-by-value on operators and on operands. Call-by-name is
dual to lambda-value’s call-by-value [Wad03]. We conjecture that, with
convergent terms, call-by-value as call-to-$\mathsf{WNF}$ is dual to call-by-
name in the weak-reducing space, and strict normalisation is dual to normal
order in the full-reducing space.

##  6\. The eval-readback evaluator style

An evaluator in eval-readback style is defined as the composition of two
functions: a less-reducing ‘eval’ function that contracts redexes to an
intermediate result with no redex in outermost position, and a further-
reducing ‘readback’ function that ‘reads back’ the intermediate result to
distribute ‘eval’ down the appropriate unevaluated subterms of the
intermediate result to reach further redexes. The style is related to the
staged evaluation of normalisation-by-evaluation [BS91] but without recourse
to an external domain. The separation of evaluation in eval and readback
stages can be of help in writing evaluators. For example, the eval stage can
be simply weak or non-head and written in uniform eval-apply style. The
readback stage can then distribute eval under lambda, or within neutral
operands, or both. The separation also enables independent optimisations, as
mentioned in the introduction.

We illustrate the style using first the two classic eval-readback evaluators
byValue and byName in [Pau96, p. 390]. We discuss other eval-readback
evaluators later in the section. The byValue and byName evaluators are both
full-reducing and deliver normal forms. The first is strict and incomplete.
The second is non-strict and complete for $\mathsf{NF}$. We first show and
discuss them in their original (non-monadic) definitions in the strict
Standard ML programming language but adapted to our data-type Term and subst
function (in the original, terms have strings only for free variables and de
Bruijn indices for bound variables). We want readers to recognise the original
definitions and to compare them to the monadic Haskell versions in Section
6.1. Also, the original non-monadic definitions are trivial to compare with
the also non-monadic definition of the ‘strong reduction’ evaluator [GL02, p.
237] which we have claimed (Section 5.7) in to be identical to byValue modulo
commuting redexes.

The byValue evaluator is the composition of an eval evaluator, simply called
eval, and a readback evaluator called bodies. The eval evaluator is literally
the Standard ML version of the non-monadic call-by-value evaluator bv
discussed in Section 5.1, which works directly in strict Standard ML.

      fun eval (App(m,n)) =
        (case eval m of
                   Lam(x,b) => eval (subst x (eval n) b)
                 | m’       => App(m’, eval n))
        | eval t          = t

      fun byValue t = bodies (eval t)
      and bodies (Lam(x,b)) = Lam(x, byValue b)
        | bodies (App(m,n)) = App(bodies m, bodies n)
        | bodies t          = t

The readback evaluator bodies delivers a $\mathsf{NF}$ by fully evaluating the
abstraction bodies (hence its name ‘bodies’) in the $\mathsf{WNF}$ delivered
by eval. As the shape of a $\mathsf{WNF}$ indicates, the unevaluated
abstractions occur at the top level or within the operands of neutrals.

In its first clause, bodies evaluates an abstraction to $\mathsf{NF}$ by
calling the eval-readback composition (byValue) that recursively distributes
eval down the body. In its second clause, bodies calls itself recursively on
the operator of the neutral to distribute itself down nested applications, and
on the operand to reach the unevaluated abstractions on which it will
eventually call the eval-readback composition (byValue) of the first clause.
Finally, bodies is the identity on variables. It has no clause for redexes
because it is a readback and merely distributes evaluation.

As anticipated in Section 5.7, byValue is the precursor of the eval-readback
‘strong reduction’ evaluator $\mathcal{N}$ in [GL02, p. 237]. The latter only
differs from the former in that neutrals have their operands flattened and
evaluated right-to-left. This is illustrated by the following definition of
$\mathcal{N}$ that mirrors the original in [GL02, p. 237] but with left-to-
right evaluation. The $W_{i}$ terms stand for $\mathsf{WNF}$s.

$\begin{array}[]{rcl}\mathcal{N}&=&\mathcal{R}\circ\mathcal{V}\\\
\mathcal{R}(\lambda x.B)&=&\lambda x.\mathcal{N}(B)\\\
\mathcal{R}(x\,W_{1}\cdots
W_{n})&=&x\,\mathcal{R}(W_{1})\cdots\mathcal{R}(W_{n})\qquad n\geq
0\end{array}$

If we substitute byValue for $\mathcal{N}$, bodies for $\mathcal{R}$, and eval
for $\mathcal{V}$ we obtain byValue.

As discussed in Sections 5.1 and 5.7, strong reduction is incomplete in the
pure lambda calculus with arbitrary terms, but it is complete with convergent
strongly-normalising terms, as would be any strategy in that setting.

The byName evaluator is the composition of an eval evaluator called headNF and
a readback evaluator called args. The eval evaluator headNF literally
implements in code the head spine (${\mathsf{he}}$) eval-apply evaluator of
Section 5.6.

      fun headNF (Lam(x,b)) = Lam(x, headNF b)
        | headNF (App(m,n)) =
            (case headNF m of
                Lam(x,b) => headNF (subst x n b)
              | m’       => App(m’, n))
        | headNF t          = t

      fun byName t = args (headNF t)
      and args (Lam(x,b))   = Lam(x, args b)
        | args (App(m,n))   = App(args m, byName n)
        | args t            = t

The readback evaluator args delivers a $\mathsf{NF}$ by fully evaluating the
unevaluated (operands of) neutrals (‘arguments’, hence its name ‘args’) in the
$\mathsf{HNF}$ delivered by headNF. As the shape of a $\mathsf{HNF}$
indicates, the unevaluated neutrals occur at the top level or within
abstraction bodies.

In its first clause, args evaluates an abstraction to $\mathsf{NF}$ by calling
itself recursively to reach the unevaluated neutrals on whose operands it will
eventually call the eval-readback composition (byName) of the second clause.
In the second clause, args calls itself recursively on the operator of the
neutral to distribute itself down nested applications, and calls the eval-
readback composition (byName) that recursively distributes headNF down the
operand. Finally, args is the identity on variables. It has no clause for
redexes because it is a readback and merely distributes evaluation.

Recall from Section 5.8 that eval-readback byName is one-step equivalent to
the eval-apply hybrid normal order evaluator (${\mathsf{hn}}$) discussed in
that section. This can be gleaned from their respective definitions and is
proven by the LWF-transformation on evaluator implementations of Section 8.

###  6.1. Monadic style eval-readback

We show the monadic definitions of byValue and byName in Haskell. Recall from
the previous section that eval is identical to bv, and headNF is identical to
he. Hereafter we use the latter names in code and natural semantics. We omit
in this section their already given eval-apply monadic definitions.

In monadic style, byValue and byName are defined by a monadic (Kleisli)
composition. We have respectively replaced the calls to byValue and byName in
bodies and args by their respective definitions as Kleisli compositions.

      byValue :: Monad m => Term -> m Term
      byValue =  bodies <=< bv

      bodies :: Monad m => Term -> m Term
      bodies v@(Var _)   = return v
      bodies l@(Lam x b) = do b’ <- (bodies <=< bv) b
                              return (Lam x b’)
      bodies (App m n)   = do m’ <- bodies m
                              n’ <- bodies n
                              return (App m’ n’)

      byName :: Monad m => Term -> m Term
      byName =  args <=< he

      args :: Monad m => Term -> m Term
      args v@(Var _)   = return v
      args l@(Lam x b) = do b’ <- args b
                            return (Lam x b’)
      args (App m n)   = do m’ <- args m
                            n’ <- (args <=< he) n
                            return (App m’ n’)

For a different example, we show the eval-readback evaluator for normal order
in [GPN14, p. 183], which is the composition of the eval-apply call-by-name
evaluator bn (the monadic implementation of the call-by-name evaluator
(${\mathsf{bn}}$) of Section 5.2) and the following readback evaluator rn
(from readback normal order):

      no :: Monad m => Term -> m Term
      no =  rn <=< bn

      rn :: Monad m => Term -> m Term
      rn v@(Var _)   = return v
      rn l@(Lam x b) = do b’ <- (rn <=< bn) b
                          return (Lam x b’)
      rn (App m n)   = do m’ <- rn m
                          n’ <- (rn <=< bn) n
                          return (App m’ n’)

As a proper readback, rn has no clause for redexes because it simply
distributes evaluation (the Kleisli composition) on the unevaluated
abstractions and neutrals of the $\mathsf{WHNF}$ delivered by bn in order to
obtain a $\mathsf{NF}$. A $\mathsf{WHNF}$ has no redex in outermost position.

The eval-readback examples so far implement full-reducing strategies. But the
style can be used for less-reducing strategies. One example that is a
variation of byValue is the ‘ahead machine’ [PR99, Def. 5.1] discussed in
Section 5.10. In its eval-apply definition the strategy uses weak, strict and
non-head call-by-value bv to evaluate operators and operands. Its eval-
readback version uses bv for eval, like byValue, but its readback does not
distribute evaluation on operands. We call this readback bodies2 for easy
comparison with bodies. We use the identity strategy id for the non-evaluation
of operands.

      am :: Monad m => Term -> m Term
      am =  bodies2 <=< bv

      bodies2 :: Monad m => Term -> m Term
      bodies2 v@(Var _) = return v
      bodies2 (Lam x b) = do b’ <- (bodies2 <=< bv) b
                             return (Lam x b’)
      bodies2 (App m n) = do m’ <- bodies2 m
                             n’ <- id n
                             return (App m’ n’)

Another less-reducing example is yet another variation of byValue that also
uses bv for eval but the readback calls eval (bv) directly on abstraction
bodies rather than the Kleisli composition. This evaluator and the strategy it
implements does not appear in the literature. The strategy delivers a
$\mathsf{WNF}$ where the abstractions in the spine are evaluated. We refrain
from naming the strategy and will use the systematic notation that we
introduce in Section 7.5 to identify it as
${\mathsf{E}}{\mathsf{R}}\circ{\mathsf{bv}}$. We call the readback bodies3 for
easy comparison with bodies.

      unnamed :: Monad m => Term -> m Term
      unnamed =  bodies3 <=< bv

      bodies3 :: Monad m => Term -> m Term
      bodies3 v@(Var _) = return v
      bodies3 (Lam x b) = do b’ <- bv b
                             return (Lam x b’)
      bodies3 (App m n) = do m’ <- bodies3 m
                             n’ <- bodies3 n
                             return (App m’ n’)

###  6.2. Natural semantics style eval-readback

In natural semantics, an eval-readback evaluator requires two separate sets of
rules, one for eval and one for readback. Readback _has no_ con _rule_ as it
simply distributes evaluation in its abs and neu rules to reach the redexes
within the intermediate form which are evaluated by eval (which does have a
con rule). Figure 7 (page 7) shows the natural semantics for the readbacks
discussed in code in Section 6.1. We omit var rules because readbacks are
identities on variables. The compositions are meta-notation to abbreviate a
sequence of two premises, _e.g._
$({\mathsf{bodies}}\circ{\mathsf{bv}})(B)=B^{\prime\prime}$ abbreviates the
sequence of premise ${\mathsf{bv}}(B)=B^{\prime}$ followed by premise
${\mathsf{bodies}}(B^{\prime})=B^{\prime\prime}$. A proper natural semantics
needs separate premises on which to stack evaluation trees, but we use
compositions to abbreviate and to match the compositions in code. Compositions
will be also handy when we generalise in Section 7.1. The identity strategy
${\mathsf{id}}$ is used for non-evaluation instead of an omitted premise.

byValue’s readback (${\mathsf{bodies}}$):

*[left=abs] (bodies∘bv)(B) = B”bodies(λx.B) = λx.B” *[left=neu] bodies(M) = M’ bodies(N) = N’ bodies(MN) = M’N’

byName’s readback (${\mathsf{args}}$):

*[left=abs] args(B’) = B’ args(λx.B) = λx.B’ *[left=neu] args(M) = M’ (args∘he)(N) = N” args(MN) = M’N”

Normal order’s readback (${\mathsf{rn}}$):

*[left=abs] (rn∘bn)(B) = B” rn(λx.B) = λx.B” *[left=neu] rn(M) = M’ (rn∘bn)(N) = N” rn(MN) = M’N”

Ahead machine’s readback (${\mathsf{bodies}}_{2}$):

*[left=abs] (bodies_2 ∘bv)(B) = B” bodies_2(λx.B) = λx.B” *[left=neu] bodies_2(M) = M’ id(N) = N bodies_2(MN) = M’ N

A novel strategy’s readback (${\mathsf{bodies}}_{3}$); the strategy is
${\mathsf{E}}{\mathsf{R}}\circ{\mathsf{bv}}$ (Section 7.5):

*[left=abs] bv(B) = B’ bodies_3(λx.B) = λx.B’ *[left=neu] bodies_3(M) = M’ bodies_3(N) = N’ bodies_3(MN) = M’ N’

Figure 7. Natural semantics of readback evaluators discussed in Section 6.1.
The var rules are omitted because readbacks are identities on variables. There
is no con rule because readbacks merely distribute evaluation and do not
contract redexes. The identity strategy ${\mathsf{id}}$ is used for non-
evaluation instead of an omitted premise. The compositions are meta-notation.

###  6.3. Characterisation of the style

The examples so far illustrate some of the variations within the style. But we
must rule out spurious eval-readback evaluators defined by concocting vacuous
readbacks. For example, the uniform eval-apply ${\mathsf{bv}}$ used as an eval
stage can be defined spuriously in eval-readback style as the composition
${\mathsf{rb}}\circ{\mathsf{bv}}$ where ${\mathsf{rb}}$ is the following
vacuous readback:  *[left=abs] id(B) = B rb(λx.B) = λx.B *[left=neu] id(M) = M
id(N) = N rb(MN) = M N Substituting ${\mathsf{rb}}$ for the identity strategy
${\mathsf{id}}$ in any of the premises obtains a merely recursive readback
that is also vacuous.

Readback must be called after eval and it must evaluate more than eval by
calling eval either directly or in an eval-readback composition over some
terms that were unevaluated by eval. For that, readback must also call itself
recursively or in a composition. The following provisos characterise authentic
readbacks in natural semantics:

  1. (er1)

Readback must call itself recursively on the operator $M$ to distribute itself
down nested applications. (Notice that eval also calls itself recursively on
operators.)

  2. (er2)

In the other two premises, namely, evaluation of the body $B$ (non-weakness)
and evaluation of the operand $N$ (non-headness):

    1. (rb-ev)

Readback must call _eval_ on at least one of the two premises where eval was
the identity, calling eval directly or in an eval-readback composition.

    2. (rb-rb)

Readback must call _readback_ recursively on at least one of the two premises.
In the case where eval was the identity on the premise, readback must call the
eval-readback composition.

The proviso (er2) holds when readback calls the eval-readback composition on
one of the two premises and the identity on the other premise. It also holds
when readback calls eval on a premise unevaluated by eval and calls readback
on the other premise evaluated by eval. Other combinations are possible, all
of which call eval at least once and readback at least once, directly on in a
composition. It is trivial to check that the provisos guarantee
${\mathsf{rb}}\circ{\mathsf{ev}}\not={\mathsf{ev}}$ and
${\mathsf{rb}}\circ{\mathsf{ev}}\not={\mathsf{rb}}$.

###  6.4. Equivalences within the style

The splitting into eval and readback stages provides a modular approach but
the stages are tied-in by eval’s evaluation of redexes which restricts the
amount of evaluation that can be moved from eval to readback and vice-versa.
For illustration, consider the weak, non-strict, and non-head strategy
implemented by the following eval-_apply_ evaluator ${\mathsf{ea}}$:  id(B) =
B ea(λx.B) = λx.B ea(M) = λx.B ea([N/x](B)) = B’ ea(MN) = B’ ea(M) = M’
M’／≡λx.B ea(N) = N’ ea(MN) = M’N’This novel strategy has an interesting
property and will be discussed and named ${\mathsf{IIS}}$ in Section 7.3. The
point now is that a one-step equivalent eval-_readback_ evaluator is easily
defined by moving the evaluation of neutrals to a readback ${\mathsf{rb}}$ so
that ${\mathsf{ea}}={\mathsf{rb}}\circ{\mathsf{bn}}$ where ${\mathsf{bn}}$
(call-by-name) is the head version of ${\mathsf{ea}}$. We show the definition
of ${\mathsf{rb}}$. The definition of ${\mathsf{bn}}$ is in Figure 4.  id(B) =
B rb(λx.B) = λx.B rb(M) = M’(rb∘bn)(N) = N’ rb(MN) = M’N’ How much evaluation
can be moved between eval and readback to obtain equivalent eval-readback
evaluators depends on the equivalence of eval-readback and eval-apply
evaluators, because eval is naturally defined in eval-apply style as a uniform
evaluator and the question relates to how much evaluation can be moved between
the uniform subsidiary and the hybrid.

##  7\. Structuring the pure lambda calculus’s strategy space

###  7.1. Evaluation templates and generic evaluators

The four criteria of weakness, strictness, headness, and dependency on a less-
reducing subsidiary are manifested in the natural semantics by the presence or
absence of a formula for evaluation. For instance, strictness is manifested in
the con rule by the presence of a formula for the evaluation of the operand
$N$. Non-strictness is manifested by the absence of the formula. Both formulas
can be generalised into a single formula
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}(N)=N^{\prime}$
where
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$
is a parameter. For strict evaluation,
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$
is instantiated to a recursive call or to a subsidiary call. For non-strict
evaluation,
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$
is instantiated to ${\mathsf{id}}$.

Eval-apply evaluation template:

*[left=abs] la(B) = B’ea(λx.B) = λx.B’ *[left=con] op_1(M) = λx.B ar_1(N) = N’ ea([N’/x](B)) = B’ ea(MN) = B’ *[left=neu] op_1(M) = M’ M’ ／≡λx.B op_2(M’) = M” ar_2(N) = N’ ea(MN) = M”N’

Eval-apply instantiation table:

$\begin{array}[]{lc|ccccc}\hline\cr\text{Name}&\text{Eval-
apply}\leavevmode\nobreak\
({\mathsf{ea}})&{\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}&{\mathsf{op_{1}}}&{\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}&{\mathsf{op_{2}}}&{\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}\\\
\hline\cr\text{Call-by-
value}&{\mathsf{bv}}&{\mathsf{id}}&{\mathsf{bv}}&{\mathsf{bv}}&{\mathsf{id}}&{\mathsf{bv}}\\\
\text{Call-by-
name}&{\mathsf{bn}}&{\mathsf{id}}&{\mathsf{bn}}&{\mathsf{id}}&{\mathsf{id}}&{\mathsf{id}}\\\
\text{Applicative order}&{\rm Appl.\leavevmode\nobreak\ Opt.}&{\rm
Appl.\leavevmode\nobreak\ Opt.}&{\rm Appl.\leavevmode\nobreak\ Opt.}&{\rm
Appl.\leavevmode\nobreak\ Opt.}&{\mathsf{id}}&{\rm Appl.\leavevmode\nobreak\
Opt.}\\\ \text{Normal
order}&{\mathsf{no}}&{\mathsf{no}}&{\mathsf{bn}}&{\mathsf{id}}&{\mathsf{no}}&{\mathsf{no}}\\\
\text{Head
reduction}&{\mathsf{hr}}&{\mathsf{hr}}&{\mathsf{bn}}&{\mathsf{id}}&{\mathsf{hr}}&{\mathsf{id}}\\\
\text{Head
spine}&{\mathsf{he}}&{\mathsf{he}}&{\mathsf{he}}&{\mathsf{id}}&{\mathsf{id}}&{\mathsf{id}}\\\
\text{Strict
normalisation}&{\mathsf{sn}}&{\mathsf{sn}}&{\mathsf{bv}}&{\mathsf{bv}}&{\mathsf{sn}}&{\mathsf{sn}}\\\
\text{Hybrid normal
order}&{\mathsf{hn}}&{\mathsf{hn}}&{\mathsf{he}}&{\mathsf{id}}&{\mathsf{hn}}&{\mathsf{hn}}\\\
\text{Hybrid applicative
order}&{\mathsf{ha}}&{\mathsf{ha}}&{\mathsf{bv}}&{\mathsf{ha}}&{\mathsf{ha}}&{\mathsf{ha}}\\\
\text{Ahead
machine}&{\mathsf{am}}&{\mathsf{am}}&{\mathsf{bv}}&{\mathsf{bv}}&{\mathsf{am}}&{\mathsf{bv}}\\\
\text{Head applicative
order}&{\mathsf{ho}}&{\mathsf{ho}}&{\mathsf{ho}}&{\mathsf{ho}}&{\mathsf{id}}&{\mathsf{id}}\\\
\text{Spine applicative
order}&{\mathsf{so}}&{\mathsf{so}}&{\mathsf{ho}}&{\mathsf{so}}&{\mathsf{so}}&{\mathsf{so}}\\\
\text{Balanced spine applicative
order}&{\mathsf{bs}}&{\mathsf{bs}}&{\mathsf{ho}}&{\mathsf{ho}}&{\mathsf{bs}}&{\mathsf{bs}}\\\
\hline\cr\end{array}$

Eval-apply generic evaluator:

            type Red = forall m. Monad m => Term -> m Term
            gen_eval_apply :: Red -> Red -> Red -> Red -> Red -> Red
            gen_eval_apply la op1 ar1 op2 ar2 t = case t of
              v@(Var _) -> return v
              (Lam x b) -> do b’ <- la b
                              return (Lam x b’)
              (App m n) -> do m’ <- op1 m
                              case m’ of (Lam x b) -> do n’ <- ar1 n
                                                         this (subst n’ x b)
                                         _         -> do m’’ <- op2 m’
                                                         n’  <- ar2 n
                                                         return (App m’’ n’)
              where this = gen_eval_apply la op1 ar1 op2 ar2

            id :: Red
            id =  return

            bal_hybrid_sn :: Red
            bal_hybrid_sn =  sn
              where bv :: Red
                    bv =  gen_eval_apply id bv bv id bv
                    sn :: Red
                    sn =  gen_eval_apply sn bv bv sn sn

Figure 8. Eval-apply evaluation template, instantiation table, and generic
evaluator.

####  7.1.1. Eval-apply evaluation template and generic evaluator

The eval-apply evaluation template shown at the top of Figure 8 (page 8)
generalises every formula with a parameter. The template defines an eval-apply
evaluator ${\mathsf{ea}}$ with evaluator parameters
${\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}$,
${\mathsf{op_{1}}}$,
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$,
${\mathsf{op_{2}}}$ and
${\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}$.
The coloured parameters respectively determine the evaluator’s weakness,
strictness, and headness. (We explain the need for colours in a moment.) The
use of parameters also permits the instantiation of subsidiaries and the
control of staged evaluation in rule neu (${\mathsf{op_{1}}}$ followed by
${\mathsf{op_{2}}}$). Concretely, in the abs rule, the
${\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}$
parameter determines the evaluation of
(${\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}$mbda)
abstractions. In the leftmost formula of con and neu, the _shared_
${\mathsf{op_{1}}}$ parameter determines the evaluation of operators in
applications. In the con rule, the
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$
parameter determines the evaluation of operands (arguments) of redexes. In the
neu rule, the ${\mathsf{op_{2}}}$ parameter determines the further evaluation
of operators of neutrals. The
${\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}$
parameter determines the evaluation of operands of neutrals. The values
provided for all these parameters, and their interaction, determine the type
of evaluation and form of final result ($\mathsf{WHNF}$, $\mathsf{WNF}$,
etc.). The meaning of the numbering of parameters differ. The
${\mathsf{op_{1}}}$ and ${\mathsf{op_{2}}}$ parameters are stages (neu)
whereas
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$
and
${\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}$
are independent parameters for respectively evaluating operands in a redex
(con) and in a neutral (neu). Thus, we use colours for the important
parameters
${\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}$,
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$,
and
${\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}$.
The colours are also a visual aid and will be most useful from Section 7.3
onwards.

Recall from Section 5.14 that the staged evaluation of the operator in rule
neu with ${\mathsf{op_{1}}}$ and ${\mathsf{op_{2}}}$ is not a variability
point because it is subsumed by the uniform/hybrid configuration. Only hybrid
strategies use ${\mathsf{op_{2}}}$ in neu because they use the subsidiary on
${\mathsf{op_{1}}}$ in neu and con. Consequently, there is no
${\mathsf{op_{2}}}$ parameter in rule con. It would be nonsensical because the
strategy would evaluate the operator beyond the abstraction but would contract
the redex with the abstraction.

The instantiation table at the middle of Figure 8 shows that the evaluation
template expresses all the eval-apply evaluators in Figures 4 and 5. More
evaluators can be obtained by playing with the parameters. This is how we
originally obtained head applicative order (${\mathsf{ho}}$), spine
applicative order (${\mathsf{so}}$), and balanced spine applicative order
(${\mathsf{bs}}$). We will obtain more novel evaluators in this fashion
throughout this Section 7.

The code at the bottom of Figure 8 shows a generic (higher-order, parametric)
eval-apply evaluator gen_eval_apply that implements the eval-apply evaluation
template. It takes five plain evaluator parameters and delivers a plain
evaluator. The type Red (from Reducer) is the type of a plain evaluator
(Section 4). The local identifier this is an abbreviation to get a fixed-point
definition. Plain evaluators are obtained as fixed-points of the generic
evaluator. The figure shows the example for strict normalisation, which we
call bal_hybrid_sn in order to define sn and bv as fixed points of
gen_eval_apply.

####  7.1.2. Eval-readback evaluation template and generic readback

An evaluation template for eval-readback evaluators can be similarly provided.
Actually, only a template for readback is needed because eval is naturally
expressed in eval-apply style. Rarely will it be expressed in eval-readback
style, and rarely still with the latter’s eval again in eval-readback style,
etc. Eventually, the last eval is written in eval-apply style.

Considering the readback rules and provisos in Sections 6 and 5.4, and
assuming the abbreviation of compositions introduced in Section 6, there are
two possible parameters for a readback evaluator ${\mathsf{rb}}$ in its abs
and neu rules, namely
${\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}$
and
${\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}$.
Readback has no con rule (no ${\mathsf{op_{1}}}$ and
${\color[rgb]{1.0,0.65,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1.0,0.65,0.0}{\mathsf{ar_{1}}}}$
parameters) because the intermediate results delivered by eval have no redexes
in outermost position. Also, according to proviso (er1), the
${\mathsf{op_{2}}}$ parameter must be a recursive call to readback to
distribute it down nested applications.

Readback evaluation template:

*[left=abs] la(B) = B’ rb(λx.B) = λx.B’ *[left=neu] rb(M) = M’ ar_2(N) = N’ rb(MN) = M’N’

Eval-readback instantiation table:

$\begin{array}[]{lcc|ccc}\\\
\hline\cr\text{Name}&\text{Eval}&\text{Readback}\leavevmode\nobreak\
({\mathsf{rb}})&{\color[rgb]{0.9,0.17,0.31}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.17,0.31}{{\mathsf{la}}}}&{\color[rgb]{0.0,0.58,0.71}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.58,0.71}{\mathsf{ar_{2}}}}\\\
\hline\cr\mathtt{byValue}&{\mathsf{bv}}&{\mathsf{bodies}}&{\mathsf{bodies}}\circ{\mathsf{bv}}&{\mathsf{bodies}}\\\
\mathtt{byName}&{\mathsf{he}}&{\mathsf{args}}&{\mathsf{args}}&{\mathsf{args}}\circ{\mathsf{he}}\\\
\text{Normal
order}&{\mathsf{bn}}&{\mathsf{rn}}&{\mathsf{rn}}\circ{\mathsf{bn}}&{\mathsf{rn}}\circ{\mathsf{bn}}\\\
\text{Ahead
machine}&{\mathsf{bv}}&{\mathsf{bodies}}_{2}&{\mathsf{bodies}}_{2}\circ{\mathsf{bv}}&{\mathsf{id}}\\\
\mathit{unnamed}&{\mathsf{bv}}&{\mathsf{bodies}}_{3}&{\mathsf{bv}}&{\mathsf{bodies}}_{3}\\\
\hline\cr\end{array}$

Readback generic evaluator:

            type Red = forall m. Monad m => Term -> m Term
            gen_readback :: Red -> Red -> Red
            gen_readback la ar2 t = case t of
              v@(Var _) -> return v
              (Lam s b) -> do b’ <- la b
                              return (Lam s b’)
              (App m n) -> do m’ <- this m
                              n’ <- ar2 n
                              return (App m’ n’)
              where this = gen_readback la ar2

            eval_readback_byValue :: Red
            eval_readback_byValue =  bodies <=< bv
              where bv     :: Red
                    bv     =  gen_eval_apply id bv bv id bv
                    bodies :: Red
                    bodies =  gen_readback (bodies <=< bv) bodies

Figure 9. Readback evaluation template, instantiation table, and generic
readback evaluator.

Figure 9 (page 9) shows the readback evaluation template, an instantiation
table that expresses all the readback evaluators discussed in Section 6, and a
generic (higher-order, parametric) readback evaluator that implements the
readback evaluation template. Plain eval-readback evaluators are obtained by
monadic composition of an eval defined using gen_eval_apply and a readback
defined using gen_readback. The figure shows an example for byValue, which we
call eval_readback_byValue in order to define bv and bodies as fixed points.
We will define more eval-readback evaluators in Section 7.5 by playing with
the parameters.

###  7.2. Uniform/Hybrid as structuring criteria

The interaction of weakness, strictness and headness affects the amount of
evaluation. Hence, these criteria do not provide an orthogonal classification
of the strategy space. An orthogonal classification is provided by the
uniform/hybrid criterion that splits the strategy space in two and is
independent of the other three criteria.

As discussed in Section 1.3.C4, we must distinguish uniform/hybrid strategy
from uniform/hybrid-style definitional device because it may be possible to
write the device in uniform style (without subsidiary devices) for what is
actually a hybrid strategy. We provide examples in Section 7.2.2. It may be
also possible to take a uniform-style device and concoct a one-step equivalent
hybrid-style device that uses spurious subsidiary devices. We will show an
example in Section 7.4 (page 11).

Hybrid-style definitional devices have appeared and continue to appear in the
literature, either under no denomination (_e.g._ [Rea89, Mac90, Pau96,
Pie02]), or under names such as ‘levelled’ or ‘of-level-$n$’ (_e.g._ [PR99,
RP04]), ‘stratified’ (_e.g._ [AP12, CG14]), or ‘layered’ (see [GPN14] for
references). There are many hybrid evaluators and strategies (see Figure 13 on
page 13). The notion has proven useful beyond operational semantics in gradual
typing [GPNS14], solvability [CG14, GPN16, AG22] and, recently, reduction
theories for effect handlers [SPB23]. The notion of style is fruitfully
employed in machine-checked program derivations of operational semantics
devices [BCZ17, BC19, BBCD20]. In that work ‘uniform/hybrid’ is associated
with grammars of small-step context-based reduction (operational) semantics
with one/multiple non-terminals. This befits the notion of style, as we
elaborate in Section 7.2.2, but the style notion is sufficient to achieve
their aims. The concept of hybrid style is also intuitively connected to that
of a staged eval-readback evaluator [Pau96, GL02]. Making the connection
precise is partly the motivation for this paper.

In the introduction we gave an intuitive definition of uniform/hybrid strategy
in terms of in/dependence on less-reducing subsidiary strategies. In [GPN14]
we formalised the notion of uniform/hybrid strategy (which we redundantly
called in that paper ‘uniform/hybrid strategy in its nature’) using small-step
context-based reduction semantics [Fel87, FFF09]. This operational semantics
style works with the notion of a one-step strategy (Appendix A), namely, a
total function (a subset of the reduction relation) that takes an input term
and locates and contracts a redex. An evaluation sequence is obtained by
iteration. A strategy can be defined extensionally by its set of so-called
‘contexts’ which are terms with one hole where the latter marks the redex
position. The extensional definition is captured intensionally by a context-
based reduction semantics which basically defines the set of contexts and
permissible redexes using context-free grammars. Since we wish to improve on
[GPN14], in this section we temporarily leave the big-step style and switch to
that small-step definitional device. We provide a quick overview of it in
Section 7.2.1. We provide the necessary intuitions for the formal definition
of uniform/hybrid strategy in Section 7.2.2 using illustrative examples. We
arrive at the formal definition in Section 7.2.3.

####  7.2.1. Small-step context-based reduction semantics

A _context_ is a term with one hole, the latter written  $\Box$ . For example,
$\lambda x.\scalebox{0.6}[1.0]{$\Box$}x$ is a context. The set of contexts
$\mathsf{C}$ is defined by adding a hole to terms:
$\mathsf{C}::=\scalebox{0.6}[1.0]{$\Box$}\ |\
\lambda\rotatebox[origin={c}]{180.0}{$\Lambda$}.\mathsf{C}\ |\
\mathsf{C}\,\Lambda\ |\ \Lambda\,\mathsf{C}$.121212Throughout the paper we are
overloading non-terminal symbols to denote the sets generated by them, _e.g._
$\mathsf{C}$ also denotes the set generated by that non-terminal. We use
$\mathcal{C}_{1}$, $\mathcal{C}_{2}$, etc., for contexts in $\mathsf{C}$.