not every evaluator in CPS functionally-corresponds with a source direct-style eval-apply evaluator, but those that do can be transformed back and forth.

As elegantly argued in [DM09, pp. 545–547], straying from the image of the transformation (staying within the rings of more expressive power) with good reasons is a clear indication that a useful control structure or operator may be missing in the source space. For instance, programmers write evaluators in CPS with non-tail calls ‘thereby introducing the notion of delimited control [...] ; this effect can be obtained in direct style [in the source space] by adding [...] delimited-control operators [...]’ [DM09, p. 546]. Similarly in the space of structured programs, the case against the GOTO statement in [Dij68] is not that it is unconditionally harmful but that ‘straying with good reason is a clear indication that a useful control construct is missing in the source language. For example, C and Pascal programmers condone the use of GOTO for error cases because these languages lack an exception mechanism’ [DM09, p. 546].

There may be good reasons for straying from the image of the LWF transformation in the case of unbalanced hybrid strategies, such as hybrid applicative order (ha) and spine applicative order (so). Readback is a selective-iteration-of-eval function. An unbalanced strategy requires more work than eval on operands of redexes beyond distributing eval on abstractions and neutrals. There may be a missing control structure X that enables the equivalence between eval-readback-with-X and arbitrary hybrid eval-apply evaluators.

The bottom diagram in Figure 15 shows a wider correspondence diagram between operational semantics devices [GPN14, p. 177]. The transformation steps employed by the correspondences are semantics-preserving and the implementation of the devices in code define the same evaluation strategy. The figure shows on the left the functional correspondence zoomed out. On the right it shows the so-called ‘syntactic correspondence’ to abstract machines from small-step evaluators that implement context-based reduction semantics [Dan05, BD07, DM08, DJZ11]. The small-step evaluator (called a ‘reduction-based normaliser’ in [Dan05]) is a loop that iterates the following steps: (i) the decomposition of the term into a unique context with the permissible redex within the hole, (ii) the contraction, and (iii) the recomposition of the contractum into a term. The evaluator transforms to an abstract machine by the following non-invertible steps: refocusing (which optimises the iteration loop), LWF to fuse decomposition and recomposition, and inlining of iteration. Notice the different use of LWF to which we have already pointed to in the introduction. There is a further unnamed transformation from small-step structural operational semantics (SOS) to small-step context-based reduction semantics witnessed by the ‘search function’ that implements the compatibility rules of the SOS that traverse a term to locate the redex. An implementation of a search function transforms to the small-step evaluator by the following non-invertible steps: CPS-transformation, simplification, defunctionalisation, and turning the search function into a decomposition function which, additionally to the next redex, delivers the context. The simplification and defunctionalisation of the search function reveals the continuation stack, which is not revealed by a whole implementation of a SOS that searches the input term, contracts the redex, and delivers the next reduct.

Syntactic correspondences have been shown for specific uniform and hybrid strategies, weak-reducing and full-reducing, and connected through the functional correspondence with big-step eval-apply evaluators [Mun08, GPN13, DMM13, GPNM13, DJ13, GPN14, BCZ17]. The further connection with eval-readback evaluators is provided by our one-step equivalence proof. The eval-readback evaluators are obtained from balanced hybrid eval-apply evaluators by instantiating the equations (Proposition 8.1).
## 10. RELATED WORK

We have discussed related work throughout the paper, especially in the introduction and Sections 3, 5, 7.2, and Appendix B. Big-step evaluators are ubiquitous in the literature on lambda calculus and functional programming. We have not found higher-order generic evaluators like those of Section 7.1 in the literature, but we believe they must have been considered before.

The survey and structuring of the strategy space presented in this paper significantly emend and amend the seminal survey and structuring presented in [GPNG10, Gar14] which in turn extend the survey and structuring in [Ses02]. The LWF transformation presented in this paper on plain arbitrary evaluators that instantiate generic evaluators is simpler and more direct than the LWF transformation in [Gar14] on generic evaluators that work with boolean triples and the hybridisation operation (◊).

A recent work [BCD22] presents a strategy space (called a zoo) that includes call-by-name, call-by-value (call-by-WNF and lambda-value's), head and full-reducing versions, and non-deterministic and right-to-left versions. The work focuses on small-step context-based reduction semantics to define strategies, using defunctionalised continuations that include contexts and other useful information. It connects the uniform-style property (grammars with one non-terminal, i.e. one continuation stack) with determinism, and it structures the space by building strategies from (or decomposing strategies into) combinations of basic fine-grained sets of contexts (weak contexts, head contexts, left or right contexts, etc.) and subsets of specific terms (intermediate and final results). A hybrid strategy as presented in this paper is such that it has contexts in one (maybe more) of its building fine-grained contexts not closed under inclusion. The idea of combining fine-grained contexts is related to the notion of dependence [GPN14]. Despite the differences between our approach and [BCD22], both find and structure many identical left-to-right deterministic strategies: all the well-known strategies and the novel uniform ones presented in [GPNG10, Gar14], e.g. IIS and ISI are respectively low and cbwh in [BCD22]. The zoo does not consider many hybrid strategies (am, ha, so, bs, and the unnamed hybrids in Figure 13), but both strategy spaces might be unified or superseded by extending the catalogue of basic fine-grained contexts with those required to define, through their combination, the full hybrid space. We take this as a confirmation that the notion of uniform/hybrid strategy is a fruitful structuring criterion.

Hybrid strategies abound. They are essential to completeness and 'completeness for' in the non-strict and strict spaces. For the non-strict strategies, the underlying explanatory technical notion is 'needed reduction' (Appendix E) which can be extended to 'completeness for' other kinds of final result than normal forms. We summarise the completeness for some uniform and balanced hybrid strategies in Figure 6 (page 30):

* `bn`, `IIS`, `hr`, and `no` are respectively complete for WHNF, WNF, HNF, and NF by the Quasi-Leftmost Reduction Theorem (Appendix E).

* `he` and `hn` are respectively complete for HNF and NF, with redexes in $(\lambda x.HNF)\Lambda$ by the Needed Reduction Theorem (Appendix E).<fnref n="16" />

Completeness results can be given for strict strategies (which are incomplete in the pure lambda calculus) using notions of reduction other than the $\beta$-rule, namely, using calculi with

<footnote n="16">¹⁶By the properties of HNF, it turns out that restricting the redexes to $(\lambda x.HNF)\Lambda$ does not alter the completeness of `he` and `hn` with unrestricted redexes.</footnote>
notions of reduction with permissible redexes where the operand and/or the operator has to
be in some final form. Concretely, we conjecture the following:

* bv, am, and sn are respectively complete for WNF, VHNF, and NF with redexes in $(\lambda x.\Lambda)\text{WNF}$.

* ho and bs are respectively complete for HNF and NF with redexes in $(\lambda x.HNF)HNF$.

The conjectures rest on these principles:

(1) The strategies above are outermost when taking into account the corresponding notion of permissible redex, i.e. an outermost non-permissible redex may become the next permissible redex to be contracted iff contracting some inner permissible redex makes the outer one a permissible redex.

(2) All the notions of permissible redexes are stable under contraction, i.e. a permissible redex remains so when any of its permissible sub-redexes is contracted.

(3) Contraction of permissible redexes is confluent, i.e. given a term with two permissible redexes, the terms resulting after the contraction of the two permissible redexes in different order reduce to a common term.

We finally discuss the connection between hybridity, outermost, completeness-for, 'refocusing', and 'backward overlaps' [DJ13]. A set of reduction rules is backward overlapping if a subterm of the left hand side of one rule unifies with the right hand side of the same or a different rule. Intuitively, this means that a potential redex (the term that will unify with the left hand side of the first rule) will turn into an actual redex after contracting some sub-redex (the redex whose contractum is the right hand side of the second rule) of the former one. As pointed out in [DJ13], in the presence of backward overlaps the 'refocusing' techniques that deforest the recomposition and decomposition of a contractum in a context-based reduction semantics may miss the outer redex when this context-based reduction semantics implements an outermost strategy (i.e. refocusing will carry on decomposing the term at the scope of the inner redex, instead of recomposing the term up to the scope of the outer redex). In order to prevent this, [DJ13] propose a backtracking step that will recompose the term just enough to reach the scope of the outer redex.

All the strategies discussed in the paragraph above about 'completeness-for' are outermost, and the notions of reduction induced by the corresponding permissible redexes are backward overlapping. (An outer non-permissible redex may turn into a permissible redex by contracting some inner permissible redex.) Some of the strategies are uniform, because their permissible redexes do not contain any permissible sub-redexes to be contracted according to the strategy, and the problem of missing an outer redex by decomposing at the scope of the inner redex never occurs. This is easy to see in the non-strict case, where the operator $(\lambda x.\Lambda)$ in WHNF is irreducible for bn and IIS, and the operator $(\lambda x.HNF)$ in HNF is irreducible for he, and where the operands of a permissible redex are never reduced. It can also be seen in the strict case, where the operator $(\lambda x.\Lambda)$ in WNF and the operand in WNF are irreducible for bv, and where the operator $(\lambda x.HNF)$ in HNF and the operand in HNF are irreducible for ho. The remaining outermost and complete-for strategies are inexorably hybrid because their permissible redexes may contain permissible sub-redexes. In this case, a less-reducing subsidiary strategy must be called at the scope of the potential redex (at the operator in the non-strict case, and at the operator and the operand in the strict case) in order to find the inner redexes that will turn the outermost potential redex into an actual one, but without reducing any further. In [GPN13], a refocusing solution based on the shape invariant of the continuation stack used in the decomposition step is shown to be applicable to such hybrid
strategies. This solution is also applicable to the outermost strategy presented in [DJ13],
which is hybrid.

11. FUTURE WORK

We list a few of many possibilities for future work. To analyse the strategies that stray from
the image of the LWF transformation and their possible relation with control operators
mentioned in the conclusion. To investigate one-step equivalence when the subsidiary
evaluator implements a shallow hybrid strategy (Section 7.4.1). To investigate the relationship
between, on the one side, non-strict leftmost-outermost and spine strategies, and on the
other side, strict leftmost-innermost and spine-ish strategies, especially in the wider context
of ‘needed reduction’ (Appendix E). To (dis)prove the duality conjecture (Section 5.14). To
transcribe the structuring of the strategy space to the search-function side of the syntactic
correspondence in order to derive plain but arbitrary small-step evaluators and abstract
machines that connect to the functional correspondence. To investigate the connection with
the small-step framework in [BCD22]. To mechanise the LWF proof involving constraints on
parameters. To develop the functional correspondence from parametric eval-apply evaluators
into parametric abstract machines. To apply the principles and criteria presented in this
paper to structuring the strategy space of calculi with explicit substitutions.

ACKNOWLEDGEMENTS

Our interest in strategies and evaluators was stimulated by the textbooks and papers cited
in the introduction. The following were particularly influential: [FH88, Chp. 9], [Rea89,
Chp. 13], [Mac90, Chps. 11–12], and [McC60, Lan64, Rey72, Plo75, Ses02, GL02, ABDM03].
We thank Emilio J. Gallego Arias for contributing to [GPNG10]. We thank the following
people for their feedback and encouragement at talks and presentations on the survey and
structuring material in [GPNG10, Gar14]: Olivier Danvy, Jan Midtgaard, Ian Zerny, Peter
Sestoft, Ruy Ley-Wild, Noam Zeilberger, Richard Bird, Jeremy Gibbons, Ralf Hinze, Geraint
Jones, Bruno Oliveira, Meng Wang, and Nicolas Wu. We specially thank Jeremy Gibbons for
permission to name the Beta Cube after him. We thank Tomasz Drab for a discussion on the
strategy space in [BCD22] and the strategy space presented in this paper. We finally thank
the three anonymous reviewers of *LMCS* for accepting to review such a long paper and for
their insightful criticism and suggestions which have led us to make important corrections,
clarifications, and additions.

APPENDIX A. PURE LAMBDA CALCULUS CONCEPTS AND NOTATION

The set $\Lambda$ of pure lambda calculus terms consists of variables, abstractions, and applications. Uppercase, possibly primed, letters (e.g. $B$, $M$, $N$, $M'$, $M''$, etc.) range over $\Lambda$. Lowercase, also possibly primed, letters (e.g. $x$, $y$, $z$, $x'$, $x''$, etc.) range over a countably-infinite set of variables $V$. Lowercase variables act also as *meta-variables* ranging over $V$ when used in term forms. For example, the concrete term $\lambda y.zy$ with parameter $y$ is of the form $\lambda x.B$ where $x$ is a meta-variable. We say $x$ is the parameter and $B$ is the *body*. A *free variable* is not a parameter of an abstraction. Terms with at least one free variable are *open terms*. Terms without free variables are *closed terms*. In an application $MN$ we say $M$ is the *operator* and $N$ is the *operand*. The application operation is denoted by tiny
whitespace or by juxtaposition. Abstractions associate to the right. Applications associate to the left and bind stronger than abstractions. A few example terms: $x$, $xy$, $xx$, $\lambda x.x$, $\lambda x.\lambda y.yx$, $x(\lambda x.x)$, $xy(\lambda x.x)$, $(\lambda y.y)(xy)$, and $(\lambda x.y)(xyz)(\lambda x.\lambda y(xy))$. Uppercase boldface letters stand for concrete terms. For example, **I** abbreviates the identity term $\lambda x.x$, and **Y** abbreviates the non-strict fixed-point combinator $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$. For more fixed-point combinators and their explanation see [Ros50, p. 130], [CF58, p. 178], [HS08, p. 36], and [Bar84, p. 131].

Every term of $\Lambda$ has the form $\lambda x_1 \dots \lambda x_n . H N_1 \dots N_m$ with $n, m \ge 0$. The head term $H$ is either a variable (the 'head variable') or a redex (the 'head redex'). A redex is an application of the form $(\lambda x.B)N$. We write an arrow $\to$ to denote one-step beta-reduction. We write $[N/x](B)$ for the capture-avoiding substitution of the operand $N$ for the free occurrences (if any) of parameter $x$ in the abstraction body $B$. The resulting term is called a *contractum*. The function notation $[N/x](B)$ that wraps the subject of the substitution $B$ in parentheses comes from [Plo75]. This notation is itself based on the original notation $[N/x]B$ without parenthesis of [CF58]. Both notations flow in English when read from left to right: 'substitute $N$ for free $x$ in $B'$. The action is substitute-for, not replace-by. Other notations are, of course, valid.

Normal forms, collected in set NF (Figure 1), are terms without redexes. They consist of variables, and abstractions and applications in normal form. Neutrals have been introduced in Section 1.3. Examples of neutrals are $xy$, $x(\lambda x.y)$, and $x((\lambda x.y)z)(y(\lambda x.x))$. The last neutral has a neutral $y(\lambda x.x)$ as its second operand. A neutral cannot evaluate to a redex unless a suitable operand can be substituted for the head variable. For this, it is necessary for the neutral to occur within an abstraction that has the head variable for parameter. For example, in the neutral $xN$ the head variable is free and cannot be substituted. In $(\lambda x.xN)(yM)$, the abstraction body $xN$ is a neutral, but the substitution of $yM$ for $x$ delivers $yMN$ which is itself a neutral, not a redex. In contrast, in $(\lambda x.xN)(\lambda y.y)$ the contractum $(\lambda y.y)N$ is a redex.

An evaluation strategy is defined generically as a function subset of the reduction relation, e.g. [Bar84, p. 53] [TeR03, p. 130]. For instance, a one-step strategy $st$ is defined as a total function on terms such that either $M \equiv st(M)$ for all $M \in \mathbb{F}$ where $\mathbb{F}$ is a set of final forms, or $M \to st(M)$ for all $M \notin \mathbb{F}$. An iterative multiple-step definition is obtained by transitive closure: $M \to^+ st^n(M)$ for $n > 0$. For each input term the strategy determines a unique evaluation sequence up to, if finite, a final result in $\mathbb{F}$. The strategy converges (opposite, diverges) when the evaluation sequence is finite (opposite, infinite). The term is said to converge (opposite, diverge) under the strategy. The big-step notation, $st(M) = N$, can be translated in terms of one-step $st$ as follows: either $M \in \mathbb{F}$ and $st(M) \equiv M \equiv N$, or $M \notin \mathbb{F}$ and $M \to^+ st^n(M)$ and $st^n(M) \equiv N$ for $n > 0$ and $N \in \mathbb{F}$.

A generic definition of a strategy is uninformative because the particular redex contracted in the reduction is unspecified. We illustrate the evaluation sequence of a strategy by underlining the chosen redex: $(\lambda x.\lambda y(xy)(\lambda x.z)x \to (\lambda y.(\lambda x.z)y)x \to (\lambda x.z)x \to z)$. The second term in the sequence has another redex, $(\lambda y.(\lambda x.z)y)x$, which is not chosen by the strategy. In this example a final result is a normal form. Operational semantics styles [Plo81, Lan64, Kah87, FH92] define strategies precisely by stipulating how the chosen redex is located.

In the pure lambda calculus it is undecidable whether an arbitrary term can be evaluated to normal form. A strategy that aims at delivering normal forms is *full-reducing*. A strategy that delivers a normal form when the latter exists is *normalising*. A strategy that diverges
for terms for which a normal form exists is *not normalising*. The archetypal term without a normal form is $(\lambda x.xx)(\lambda x.xx)$ which is abbreviated as $\Omega$. The word *complete* (opposite, *incomplete*) is also used in the literature as a synonym of 'normalising'. We have not been able to trace the genesis of 'complete'. We think it comes from the idea that the strategy's evaluation sequence completes to (reaches) the final form, or perhaps from extending to the strategy the 'complete' property of the reduction relation which obtains when it is confluent and terminating [TeR03, p. 13]. A strategy determines a unique evaluation sequence so, if it converges in a final form, then it may be called complete by extension. We prefer 'complete' because of its generality: final forms need not be exclusively normal forms. Following an anonymous reviewer's suggestion, we say that a strategy is 'complete for' the particular set of terms.

## APPENDIX B. CALL-BY-VALUE IN THE LAMBDA-VALUE CALCULUS

The motivation for the lambda-value calculus of [Plo75] was to prove that the SECD abstract machine of the ISWIM language [Lan65] was correct with respect to a calculus with open and divergent terms and a reduction relation with blocking, and provide a standardisation theorem for a complete strategy with blocking that delivers values as results. The blocking of neutrals guarantees the confluence of the reduction relation.

The correctness of SECD is proven with respect to the big-step evaluator ‘eval<sub>V</sub>’ [Plo75, p. 130] and the small-step evaluator ‘$\rightarrow_V$’ [Plo75, p. 136] by (1) a standardisation theorem [Plo75, Thm. 3, p. 137] that proves that ‘$\rightarrow_V$’ is complete for values, (2) by the one-step equivalence between ‘eval<sub>V</sub>’ and ‘$\rightarrow_V$’ (proven on paper [Plo75, Thm. 4, p. 142], not by program transformation), and (3) by the one-step equivalence of ‘eval<sub>V</sub>’ and SECD (also proven on paper [Plo75, Thm. 1, p. 131], not by program transformation). The proofs of (2) and (3) assume *closed input terms*. Indeed, the evaluators do not correspond for open input terms because ‘eval<sub>V</sub>’ ignores neutrals whereas ‘$\rightarrow_V$’ evaluates the first operand of a neutral in its 4th clause. Stuck terms do not arise with closed input terms. Under this assumption, ‘eval<sub>V</sub>’ and ‘$\rightarrow_V$’ implement call-by-WNF (Section 3). With open terms, call-by-WNF differs from ‘$\rightarrow_V$’ and cannot even be compared to ‘eval<sub>V</sub>’ because the latter does not consider neutrals.

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]. Normal forms with stuck terms and a standardisation theorem for a full-reducing and complete strategy were not considered in [Plo75]. The issues have been addressed among others in [PR99, RP04, AP12, CG14, GPN16, KMR21, AG22]. A standardisation theorem for a full-reducing complete strategy that delivers lambda-value normal forms is given in [RP04, p. 70]. A standardisation theorem for a variant full-reducing strategy that evaluates blocks left-to-right is given in [GPN16, Sec. 7.1] along with a standard theory based on the operational relevance ('solvability') and sequentiality of some open neutrals and stuck normal forms. The relation between lambda-value and the sequentiality of the linear lambda calculus was first studied in [MOTW95]. For the most complete up-to-date work at the time of writing on lambda-value solvability see [AG22], and the references on standardisation there cited.
## APPENDIX C. OVERVIEW OF LWF

The LWF optimisation is outlined in [OS07, p. 144] using code written in the maths font we have used in this paper for lambda calculus terms. To avoid confusion, in this appendix we use the same code symbols as [OS07] but in typewriter font, which is appropriate because LWF is applied to code.

Fusion is a program-transformation optimisation that combines a composition $f \circ g$ into a single function $h$. LWF is a general fusion optimisation where $f$ and $g$ can be general recursive functions, of any algebraic type, and with any number of curried or uncurried parameters. LWF is lightweight because it consists of a few simple, terminating, and automatable steps that perform local syntactic transformations without the need for heuristics. Thus, LWF can be embedded in the inlining optimisation of a compiler.

Given two general recursive functions $f = \text{fix } f \cdot \lambda x \cdot E_f$ and $g = \text{fix } g \cdot \lambda x \cdot E_g$, the composition $f \circ g$ is fused by promoting $f$ through $g$'s fixed-point operator `fix` in the following steps.

(1) Inline $g$ in $f \circ g$ to obtain $f \circ (\lambda x \cdot E_g)$ and then beta-convert that to $\lambda x \cdot f \cdot E_g$.

(2) Transform the application $f E_g$ to $E_g'$ by distributing $f$ to tail position in $E_g$.

(3) Inline $f$ once in $E_g'$ and simplify to obtain $E_{f,g}$.

(4) Replace the occurrences of $f \circ g$ in $E_{f,g}$ by a new function name $h$ and generate a new binding $h = \text{fix } h \cdot \lambda x \cdot E_h$.

Because the first steps pull out $g$'s case expression, the transformation requires $f$ to be strict (to pattern-match) on its first argument.

The soundness of LWF is proven in [OS07, Sec. 3] assuming a 'standard call-by-name' denotational semantics for a small core functional programming language where $f$ and $g$ are least fixed points in the space of continuous functions. We believe that semantics is assumed for theoretical simplicity and reasons of space in a conference paper because LWF is used on code written in *both* lazy (non-strict, call-by-need, e.g. Haskell) and eager (strict, call-by-value, e.g. Standard ML) functional programming languages. Because a denotational soundness proof for the latter would depend on the particular call-by-value theory of choice (e.g. Appendix B), the authors left that proof as future work and suggested one possible choice in [OS07, Sec. 9].

An alternative would have been to prove the call-by-value operational (rather than denotational) soundness of the steps, but that would have also enlarged the paper. At any rate, such correctness is assumed by LWF's syntactic simplicity and by the empirical evidence provided by the correct results obtained in the 'expected typical cases' [OS07, p. 144], where the fused program $h$ is syntactically identical to a known existing correct solution $h'$. The code examples with correctly fused results in [OS07] are written in strict Standard ML which certainly has no call-by-name denotational semantics. Applications of LWF in strict Standard ML presented in subsequent work [Dan05, DM08, GPN14] confirm the soundness of the transformation by producing fused programs which are syntactically identical to the expected correct known ones.

The only caveat on soundness, discussed in [OS07, Sec. 6.3], occurs when there is an expression in between a binding $x = g e$ and the application $f x$. These two must be placed together to fuse them into $h e$, and this may require swapping the in-between expression, changing the evaluation order. For pure code, whether in lazy or eager functional programming languages, the swapping may affect divergence order and performance in particular cases [OS07, p. 152]. When the swapped expressions have side-effects, $f \circ g$ and $h$
would differ in side-effect order. It is for this reason that [OS07, p. 151, 154] state that LWF is unsound for *strict and impure languages*. However, the problem affects *impure code* in any language (the authors seem to consider only the pure subset of Haskell without impure features [OS07, p. 151]). When there are no in-between bindings or the impact of the change in evaluation order (divergence and side-effects) is factored in and taken into account, the LWF transformation is unproblematically applied in lazy and eager languages for strict and non-strict functions.

In our proof by LWF (Section 8.4) a change of evaluation order does occur in the swapping of bindings for neutral terms in Step (4). This change only affects the evaluation order of redexes in operands $N_i$ of neutrals $xN_1 \cdots N_n$. Such redexes are non-overlapping (commuting) and the change in evaluation order means the one-step equivalence is 'modulo commuting redexes' for some strategies. The use of impure IO in the Haskell code is consistent with this because the result term is printed as a side-effect, showing an equivalence modulo commuting those redexes.

The LWF transformation does not involve eta-conversion, $(\lambda x. f x) \rightarrow f$, nor eta-expansion, $f \rightarrow (\lambda x. f x)$, which is fortunate, as the first is sensitive to types [JG95] and the second introduces the equation $\perp = \lambda x.\perp$.

## APPENDIX D. HASKELL’S OPERATIONAL SEMANTICS

Haskell was deliberately conceived as a research language that should avoid ‘success’. This included avoiding standardisation and a formal semantics that would either tie up the language or would have to keep up with its fast evolution [HHPW07]. However, there is a Haskell 2010 standard, *The Haskell 2010 Language Report* (available online), that includes a static semantics and also an operational semantics, as we clarify below. The latest version of the language is known as ‘GHC Haskell’, namely, the latest version compiled by the Glorious Haskell Compiler which is the *de facto* compiler. The static and operational semantics of GHC Haskell are scattered in research papers, some of them listed on the Haskell website and wiki pages.

Haskell 2010 has a standard operational semantics. More precisely, any version of Haskell has an implementation-based operational semantics. Haskell has a stable small core language, System FC, which is a direct-style (in opposition to CPS-style) version of the well-known explicitly-typed System F with extra support for type casts and coercions [Eis20]. Haskell code is statically type-checked and desugared into System FC code on which GHC performs the optimisations and generates target code for the STG abstract machine [Pey92]. This code is, in turn, finally compiled to C or to native machine code.<fnref n="17" /> System FC has an operational semantics given by its compilation scheme and execution on the STG machine. Whatever the version of Haskell used, what needs to be explained is the static semantics and the translation to System FC. These are provided for Haskell 2010 by *The Haskell 2010 Language Report* and the GHC implementation of the 2010 standard. In this sense, Haskell 2010 has a well-defined operational semantics.

With the exception of the ‘arbitrary rank polymorphism’ (*RankNTypes*) extension, the Haskell code in this paper conforms to the Haskell 2010 standard. Type classes for ad-hoc polymorphism are supported by the standard, with the *Monad* type class and the *IO* instance shipped with the Haskell 2010 standard library. Type classes have a well-known

<footnote n="17">¹⁷See Chp. 10 of the GHC Users Guide (visited: July 2023).</footnote>
and simple dictionary semantics [HHPW96]. The *RankNTypes* extension enables GHC to type-check the type of our plain and generic evaluators which have a *forall* bounded on a monad type parameter. This extension has no run-time effect as it only allows the code to type-check. The Haskell 2010 standard uses a type-inference algorithm that cannot infer rank-polymorphic types whose inhabitants are representable in System FC. Such types are innocuous, type-checkable, and translatable to System FC. At any rate, in our case the extension is entirely optional and can be dropped if desired.

The use of strict monads for strict evaluation does require some elaboration. Haskell evaluates expressions to a weak head normal form. The 2010 standard provides features for strict evaluation to head normal form: `seq`, strict function application (`$!`), and strict value constructor application (or strict data-types), all of them discussed in Sections 4.2.1 and 6.2 of *The Haskell 2010 Language Report*. These features are partly reconcilable with parametricity theorems and the correctness of some fusion transformations [JV04]. GHC also offers extensions for evaluation to normal form (*deepseq* and fully evaluated data-types). However, we have used a non-strict data-type *Term* and the strict *IO* monad to fully evaluate Haskell expressions (evaluator calls) to print terms.

## APPENDIX E. COMPLETENESS OF LEFTMOST AND SPINE STRATEGIES

The completeness and 'completeness for' of the leftmost strategies is supported by the Standardisation Theorem [CF58] which states that a strategy that chooses the leftmost redex (the leftmost-outermost redex when considering the abstract syntax tree of the term) is complete. Strict strategies are thus incomplete because they evaluate the operand of a leftmost-outermost redex.

The Standardisation Theorem is relaxed by the Quasi-Leftmost-Reduction Theorem [HS08, p. 40] which states that a strategy that *eventually* chooses the leftmost-outermost redex is complete. Such strategies are called *quasi-leftmost*. They subsume the leftmost and spine strategies, whose completeness and completeness-for is supported by the theorem.

The Standardisation and Quasi-Leftmost-Reduction theorems are further relaxed by the 'needed reduction' theorem which states that a strategy that eventually chooses the 'needed' redexes is complete [BKKSS87, p. 208]. A needed redex is a redex that is reduced in every reduction sequence to normal form when the latter exists. Needed reduction eventually reduces all the needed redexes (or its residuals). Intuitively, the critical point is in applications *MN* where the reduction of *M* or *N* may diverge. The operator *M* should be reduced enough to deliver an abstraction. The operand *N* should not be reduced because it could be discarded. Only terms that eventually appear in operator position need be evaluated, and just enough (to head normal form) to contract the redex.

## REFERENCES

[ABDM03] M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard. A functional correspondence between evaluators and abstract machines. In *Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming*, pages 8–19. ACM Press, 2003. doi:10.1145/888251.888254.

[ABM14] B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. In *Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming*, pages 363–376. ACM Press, 2014. doi:10.1145/2628136.2628154.
[ABM15] B. Accattoli, P. Barenbaum, and D. Mazza. A strong distillery. In *Proceedings of the 13th Asian Symposium on Programming and Systems*, volume 9458 of LNCS, pages 231–250. Springer, 2015. doi:10.1007/978-3-319-26529-2_13.

[Abr90] S. Abramsky. The lazy lambda calculus. In *Research Topics in Functional Programming*, pages 65–116. Addison-Welsey, 1990.

[ACCL91] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. *Journal of Functional Programming*, 1(4):375–416, 1991. doi:10.1017/S0956796800000186.

[ACP<sup>+</sup>08] B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich. Engineering formal metatheory. In *Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 3–15. ACM Press, 2008. doi:10.1145/1328438.1328443.

[ADM05] M. S. Ager, O. Danvy, and J. Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. *Theoretical Computer Science*, 342(1):149–172, 2005. doi:10.1016/j.tcs.2005.06.008.

[AG98] A. Asperti and S. Guerrini. *The Optimal Implementation of Functional Programming Languages*, volume 45. Cambridge University Press, 1998.

[AG22] B. Accattoli and G. Guerrieri. The theory of call-by-value solvability. *Proceedings of the ACM on Programming Languages*, 6(ICFP):855–885, 2022. doi:10.1145/3547652.

[AL16] B. Accattoli and U. Dal Lago. (Leftmost-outermost) beta reduction is invariant, indeed. *Logical Methods in Computer Science*, 12(1), 2016. doi:10.2168/LMCS-12(1:4)2016.

[All78] J.R. Allen. *Anatomy of Lisp*. McGraw-Hill, 1978.

[ALV21] B. Accattoli, U. Dal Lago, and G. Vanoni. The (in) efficiency of interaction. *Proceedings of the ACM on Programming Languages*, 5(POPL):1–33, 2021. doi:10.1145/3434332.

[AP12] B. Accattoli and L. Paolini. Call-by-value solvability, revisited. In *Proceedings of the 11th International Symposium on Functional and Logic Programming*, volume 7294 of LNCS, pages 4–16, 2012. doi:10.1007/978-3-642-29822-6_4.

[ASS85] H. Abelson, G. J. Sussman, and J. Sussman. *Structure and Interpretation of Computer Programs*. MIT Press, 1st edition, 1985.

[Bar84] H. Barendregt. *The Lambda Calculus, Its Syntax and Semantics*. North Holland, 1984.

[Bar91] H. Barendregt. Introduction to generalized type systems. *Journal of Functional Programming*, 1(2):125–154, April 1991. doi:10.1017/S0956796800020025.

[BBCD20] M. Biernacka, D. Biernacki, W. Charatonik, and T. Drab. An abstract machine for strong call by value. In *Proceedings of the 18th Asian Symposium on Programming Languages and Systems*, volume 12470 of LNCS, pages 147–166. Springer, 2020. doi:10.1007/978-3-030-64437-6_8.

[BBD05] M. Biernacka, D. Biernacki, and O. Danvy. An operational foundation for delimited continuations in the CPS hierarchy. *Logical Methods in Computer Science*, 1(2), 2005. doi:10.2168/LMCS-1(2:5)2005.

[BC19] M. Biernacka and W. Charatonik. Deriving an abstract machine for strong call by need. In *Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction*, volume 131, pages 8:1–8:20. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.FSCD.2019.8.

[BCD21] M. Biernacka, W. Charatonik, and T. Drab. A derived reasonable abstract machine for strong call by value. In *Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming*, pages 1–14. ACM Press, 2021. doi:10.1145/3479394.3479401.

[BCD22] M. Biernacka, W. Charatonik, and T. Drab. The zoo of lambda-calculus reduction strategies, and Coq. In *Proceedings of the 13th International Conference on Interactive Theorem Proving*, pages 7:1–7:19, 2022. doi:10.4230/LIPIcs.ITP.2022.7.

[BCZ17] M. Biernacka, W. Charatonik, and K. Zielinska. Generalized refocusing: from hybrid strategies to abstract machines. In *Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction*, volume 84, pages 10:1–10:17. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.FSCD.2017.10.

[BD07] M. Biernacka and O. Danvy. A concrete framework for environment machines. *ACM Transactions on Computational Logic*, 9(1):6:1–6:30, December 2007. doi:10.1145/1297658.1297664.

[BGG<sup>+</sup>92] R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel. Experience with embedding hardware description languages in HOL. In *IFIP TC10/WG10.2 International*
Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129–156. North-Holland/Elsevier, 1992.

[BKKSS87] H. P. Barendregt, J. R. Kennaway, J. W. Klop, and M. R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information and Computation, 75:191–231, 1987. doi:10.1016/0890-5401(87)90001-0.

[BS91] U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, pages 203–211, 1991. doi:10.1109/LICS.1991.151645.

[Car97] L. Cardelli. Type systems. In The Computer Science and Engineering Handbook. CRC Press, Boca Raton, FL, 1997. Revised 2004.

[CCM84] G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture, volume 201 of LNCS, pages 50–64. Springer, 1984. doi:10.1007/3-540-15975-4_29.

[CF58] H. B. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, 1958.

[CG14] A. Carraro and G. Guerrieri. A semantical and operational account of call-by-value solvability. In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures, pages 103–118. Springer, 2014. doi:10.1007/978-3-642-54830-7_7.

[CH00] P.-L. Curien and H. Herbelin. The duality of computation. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming, volume 35(9) of ACM SIGPLAN Notices, pages 233–243. ACM Press, 2000. doi:10.1145/351240.351262.

[Cré07] P. Crégut. Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation, 20(3):209–230, September 2007. doi:10.1007/s10990-007-9015-z.

[Cur91] P.-L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82(2):389–402, May 1991. doi:10.1016/0304-3975(91)90230-Y.

[Dan05] O. Danvy. From reduction-based to reduction-free normalization. Electronic Notes on Theoretical Computer Science, 124(2):79–100, 2005. doi:10.1016/j.entcs.2005.01.007.

[DH92] O. Danvy and J. Hatcliff. Thunks (continued). In Proceedings of the Workshop on Static Analysis, pages 3–11, 1992.

[DHS00] S. Diehl, P. Hartel, and P. Sestoft. Abstract machines for programming language implementation. Future Generation Computer Systems, 16(7):739–751, 2000. doi:10.1016/S0167-739X(99)00088-6.

[Dij68] E. W. Dijkstra. Go To statement considered harmful. Communications of the ACM, 11:147–148, 1968. doi:10.1145/362929.362947.

[DJ04] N. A. Danielsson and P. Jansson. Chasing bottoms: a case study in program verification in the presence of partial and infinite values. In Proceedings of the 7th International Conference on Mathematics of Program Construction, volume 3125 of LNCS, pages 85–109. Springer, 2004. doi:10.1007/978-3-540-27764-4_6.

[DJ13] O. Danvy and J. Johannsen. From outermost reduction semantics to abstract machine. In Proceedings of the 23rd International Symposium in Logic-Based Program Synthesis and Transformation, volume 8901 of LNCS, pages 91–108. Springer, 2013. doi:10.1007/978-3-319-14125-1_6.

[DJZ11] O. Danvy, J. Johannsen, and I. Zerny. A walk in the semantic park. In Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pages 1–12, 2011. doi:10.1145/1929501.1929503.

[DM08] O. Danvy and K. Millikin. On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Information Processing Letters, 106(3):100–109, 2008. doi:10.1016/j.ipl.2007.10.010.

[DM09] O. Danvy and K. Millikin. Refunctionalization at work. Science of Computer Programming, 74(8):534–549, 2009. doi:10.1016/j.scico.2007.10.007.

[DMM13] O. Danvy, K. Milikin, and J. Munk. A correspondence between full normalization by reduction and full normalization by evaluation, 2013. A scientific meeting in honor of Pierre-Louis Curien. V. Danos and L. Regnier. Head linear reduction. Unpublished, 2004.

[EHR91] L. Egidi, F. Honsell, and S. Ronchi della Rocca. The lazy call-by-value lambda-calculus. In Proceedings of Mathematical Foundations of Computer Science, pages 161–169, 1991. doi: 10.1007/3-540-54345-7_59.
[EHR92] L. Egidi, F. Honsell, and S. Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. *Fundamenta Informaticae*, 16(1):149-169, 1992. doi:10.3233/FI-1992-16205.

[Eis20] R. A. Eisenberg. System FC, as implemented in GHC. Technical report, MS-CIS-15-09, University of Pennsylvania, 2020.

[Fel87] M. Felleisen. *The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages*. PhD thesis, Department of Computer Science, Indiana University, 1987.

[FF86] M. Felleisen and D. P. Friedman. Control operators, the SECD-machine, and the lambda-calculus. In *Formal Description of Programming Concepts III*, pages 193-217, 1986.

[FFF09] M. Felleisen, R. B. Findler, and M. Flatt. *Semantics Engineering with PLT Redex*. The MIT Press, 2009.

[FH88] A. J. Field and P. G. Harrison. *Functional Programming*. International Series in Computer Science. Addison-Wesley, 1988. Reprinted 1993.

[FH92] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. *Theoretical Computer Science*, 103(2):235-271, 1992. doi:10.1016/0304-3975(92)90014-7.

[GAL92] G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In *Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 15-26. ACM Press, 1992. doi:10.1145/143165.143172.

[Gar14] Á. García-Pérez. *Operational Aspects of Full Reduction in Lambda Calculi*. PhD thesis, ETSI Informáticos, Universidad Politécnica de Madrid, 2014. doi:10.20868/UPM.thesis.32851.

[GH11] J. Gibbons and R. Hinze. Just do it: simple monadic equational reasoning. In *Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming*, pages 2-14. ACM Press, 2011. doi:10.1145/2034773.2034777.

[GL02] B. Grégoire and X. Leroy. A compiled implementation of strong reduction. In *Proceedings of the 7th International ACM International Conference on Functional Programming*, volume 37(9), pages 235-246. ACM Press, 2002. doi:10.1145/581478.581501.

[GPN13] Á. García-Pérez and P. Nogueira. A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers. In *Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation*, pages 107-116. ACM Press, 2013. doi:10.1145/2426890.2426911.

[GPN14] Á. García-Pérez and P. Nogueira. On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines. *Science of Computer Programming*, 95 Part 2, 2014. doi:10.1016/j.scico.2014.05.011.

[GPN16] Á. García-Pérez and P. Nogueira. No solvable lambda-value term left behind. *Logical Methods in Computer Science*, 12(2):1-43, 2016. doi:10.2168/LMCS-12(2:12)2016.

[GPN19] Á. García-Pérez and P. Nogueira. The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus. *Journal of Functional Programming*, 29:e7, 2019. doi:10.1017/S0956796819000017.

[GPNG10] Á. García-Pérez, P. Nogueira, and E. J. Gallego Arias. The beta cube (extended abstract). In *Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming*, pages 3-7, 2010.

[GPNM13] Á. García-Pérez, P. Nogueira, and J. J. Moreno-Navarro. Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. In *Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming*, pages 85-96. ACM Press, 2013. doi:10.1145/2505879.2505887.

[GPNS14] Á. García-Pérez, P. Nogueira, and I. Sergey. Deriving interpretations of the gradually-typed lambda calculus. In *Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation*. ACM Press, 2014. doi:10.1145/2543728.2543742.

[HD94] J. Hatcliff and O. Danvy. A generic account of continuation-passing styles. In *Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 458-471, 1994. doi:10.1145/174675.178053.

[Hen87] M. C. Henson. *Elements of Functional Languages*. Blackwell Scientific, 1987.
[HHPW96] C. V. Hall, K. Hammond, S. Peyton Jones, and P. Wadler. Type classes in Haskell. *ACM Transactions on Programming Languages and Systems*, 18(2):109–138, 1996. doi:10.1145/227699.227700.

[HHPW07] P. Hudak, J. Hughes, S. Peyton Jones, and P. Wadler. A history of Haskell: being lazy with class. In *Proceedings of the 3rd ACM SIGPLAN Conference on History of Programming Languages*, pages 12–1–12–55. ACM Press, 2007. doi:10.1145/1238844.1238856.

[HS08] J. R. Hindley and J. P. Seldin. *Lambda-Calculus and Combinators: An Introduction*. Cambridge University Press, 2008.

[Ing61] P. Z. Ingerman. Thunks: a way of compiling procedure statements with some comments on procedure declarations. *Communications of the ACM*, 4(1):55–58, 1961. doi:10.1145/366062.366084.

[JG95] C. B. Jay and N. Ghani. The virtues of eta-expansion. *Journal of Functional Programming*, 5(2):135–154, 1995. doi:10.1017/S0956796800001301.

[JV04] P. Johann and J. Voigtländer. Free theorems in the presence of seq. In *Proceedings of 31st Symposium on Principles of Programming Languages*, pages 99–110, 2004. doi:10.1145/964001.964010.

[Kah87] G. Kahn. Natural semantics. In *Proceedings of Symposium on Theoretical Aspects of Computer Science*, volume 247 of LNCS, pages 22–39. Springer, 1987. doi:10.1007/BFb0039592.

[KMR21] A. Kerinec, G. Manzonetto, and S. Ronchi Della Rocca. Call-by-value, again! In *Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction*, 2021. doi:10.4230/LIPIcs.FSCD.2021.7.

[Kri07] J.-L. Krivine. A call-by-name lambda-calculus machine. *Higher-Order and Symbolic Computation*, 20(3):199–207, 2007. doi:10.1007/s10990-007-9018-9.

[Lam89] J. Lamping. An algorithm for optimal lambda calculus reduction. In *Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 16–30. ACM Press, 1989. doi:10.1145/96709.96711.

[Lan64] P. Landin. The mechanical evaluation of expressions. *Computer Journal*, 6(4):308–320, 1964. doi:10.1093/comjnl/6.4.308.

[Lan65] P. Landin. A correspondence between ALGOL 60 and Church’s lambda-notation. *Communications of the ACM*, 8(2–3):89–101, 158–165, 1965. doi:10.1145/363791.363804.

[Ler91] X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA, 1991.

[Lév78] J.-J. Lévy. Réductions correctes et optimales dans le λ-calcul. Thèse d'Etat, Université de Paris VII, 1978.

[Lév80] J.-J. Lévy. Optimal reductions in the lambda-calculus. In J. P. Seldin and J. R. Hindley, editors, *To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism*, pages 159–191. Academic Press, 1980.

[Mac90] B. J. MacLennan. *Functional Programming, Practice and Theory*. Addison-Wesley, 1990.

[McC60] J. McCarthy. Recursive functions of symbolic expressions and their computation by machine, Part I. *Communications of the ACM*, 3:184–195, 1960. doi:10.1145/367177.367199.

[McG70] C. L. McGowan. The correctness of a modified SECD machine. In *Proceedings of the 2nd ACM Symposium on Theory of Computing*, pages 149–157, 1970. doi:10.1145/800161.805160.

[Mog91] E. Moggi. Notions of computation and monads. *Information and Computation*, 93(1):55–92, 1991. doi:10.1016/0890-5401(91)90052-4.

[MOTW95] J. Maraist, M. Odersky, D. N. Turner, and P. Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. *Electronic Notes on Theoretical Computer Science*, 1:370–392, 1995. doi:10.1016/S1571-0661(04)00022-2.

[Mun08] J. Munk. A study of syntactic and semantic artifacts and its application to lambda definability, strong normalization, and weak normalization in the presence of state. Master’s thesis, BRICS, Aarhus University, Denmark, April 2008. doi:10.7146/brics.v15i3.21938.

[OS07] A. Ohori and I. Sasano. Lightweight fusion by fixed point promotion. In *Proceedings of 34th Symposium on Principles of Programming Languages*, pages 143–154, 2007. doi:10.1145/1190216.1190241.

[Pau96] L. C. Paulson. *ML for the Working Programmer*. Cambridge University Press, 2nd edition, 1996.
[Pey92] S. Peyton Jones. Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine. *Journal of Functional Programming*, 2(2):127-202, 1992. doi:10.1017/S0956796800000319.

[Pie02] B. C. Pierce. *Types and Programming Languages*. MIT Press, 2002.

[Plo75] G. Plotkin. Call-by-name, call-by-value and the lambda calculus. *Theoretical Computer Science*, 1:125-159, 1975. doi:10.1016/0304-3975(75)90017-1.

[Plo81] G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Department of Computer Science, Aarhus University, Denmark, 1981.

[PR99] L. Paolini and S. Ronchi Della Rocca. Call-by-value solvability. *Theoretical Informatics and Applications*, 33(6):507-534, 1999. doi:10.1051/ita:1999130.

[Rea89] C. Reade. *Elements of Functional Programming*. International Series in Computer Science. Addison-Wesley, 1989.

[Rey72] J. Reynolds. Definitional interpreters for higher-order programming languages. In *ACM Conference Proceedings*, pages 717-740. ACM Press, 1972. Reprinted in *Higher-Order and Symbolic Computation* 11(4), 1998. doi:10.1023/A:1010027404223.

[Ros50] P. C. Rosenbloom. *The Elements of Mathematical Logic*. Dover Publications, 1950.

[RP04] S. Ronchi Della Rocca and L. Paolini. *The Parametric Lambda Calculus*. Springer, 2004. doi:10.1007/978-3-662-10394-4.

[Ses02] P. Sestoft. Demonstrating lambda calculus reduction. In *The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones*, volume 2566 of LNCS, pages 420-435. Springer, 2002. doi:10.1007/3-540-36377-7_19.

[SPB23] F. Sieczkowski, M. Pyzik, and D. Biernacki. A general fine-grained reduction theory for effect handlers. *Proceedings of the ACM on Programming Languages*, 7(ICFP):511-540, 2023. doi:10.1145/3607848.

[SR15] G. Scherer and D. Rémy. Full reduction in the face of absurdity. In *Proceedings of Programming Languages and Systems, 24th European Symposium on Programming*, pages 685-709. Springer, 2015. doi:10.1007/978-3-662-46669-8_28.

[SS78] G. L. Steele, Jr. and G. J. Sussman. The art of the interpreter, or the modularity complex (parts zero, one, and two). AI Memo 453, MIT AI Laboratory, 1978.

[Sto77] J. E. Stoy. *Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory*. MIT Press, 1977.

[TeR03] TeReSe. *Term Rewriting Systems*, volume 55 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press, 2003.

[Wad76] C. Wadsworth. The relation between computational and denotational properties for Scott's $D_\infty$-models of the lambda calculus. *SIAM Journal of Computing*, 5(3):488-521, 1976. doi:10.1137/0205036.

[Wad92a] P. Wadler. Comprehending monads. *Mathematical Structures in Computer Science*, 2:461-493, 1992. doi:10.1017/S0960129500001560.

[Wad92b] P. Wadler. The essence of functional programming. In *Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 1-14. ACM Press, 1992. doi:10.1145/143165.143169.

[Wad03] P. Wadler. Call-by-value is dual to call-by-name. In *Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming*, pages 189-201. ACM Press, 2003. doi:10.1145/944705.944723.