Factorize Factorization

Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri

► To cite this version:

Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri. Factorize Factorization. CSL 2021 - 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. 10.4230/LIPIcs.CSL.2021.22 . hal-03044338

HAL Id: hal-03044338

https://hal.science/hal-03044338

Submitted on 7 Dec 2020

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Factorize Factorization

## Beniamino Accattoli

Inria & LIX, École Polytechnique, UMR 7161, Palaiseau, France

## Claudia Faggian

Université de Paris, IRIF, CNRS, F-75013 Paris, France

## Giulio Guerrieri

University of Bath, Department of Computer Science, Bath, UK

### Abstract

We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our technique is well adapted to deal with extensions of the call-by-name and call-by-value $\lambda$-calculi.

The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with $\beta$-reduction. We then closely analyze some common factorization schemas for the $\lambda$-calculus.

Concretely, we apply our technique to diverse extensions of the $\lambda$-calculus, among which de' Liguoro and Piperno's non-deterministic $\lambda$-calculus and—for call-by-value—Carraro and Guerrieri's shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.

**2012 ACM Subject Classification** Theory of computation $\rightarrow$ Rewrite systems; Theory of computation $\rightarrow$ Logic

**Keywords and phrases** Lambda Calculus, Rewriting, Reduction Strategies, Factorization

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2021.22

**Funding** This work is partially supported by ANR JCJC grant "COCA HOLA" (ANR-16-CE40-004-01), ANR PRC project PPS (ANR-19-CE48-0014), and EPSRC Project EP/R029121/1 *Typed lambda-calculi with sharing and unsharing*.

## 1 Introduction

The $\lambda$-calculus underlies functional programming languages and, more generally, the paradigm of higher-order computation. Through the years, more and more advanced features have enriched this paradigm, including control, non-determinism, states, probabilistic or quantum features. The well established way to proceed is to extend the $\lambda$-calculus with new operators. Every time, good operational properties, such as confluence, normalization, or termination, need to be proved. It is evident that the more complex and advanced is the calculus under study, the more the ability to *modularize the analyses* of its properties is crucial.

Techniques for modular proofs are available for termination and confluence, with a rich literature which examines under which conditions these properties lift from modules to the compound system—some representative papers are [54, 55, 55, 49, 38, 39, 40, 30, 10, 20, 18, 17, 5, 12], see Gramlich [22] for a survey. Termination and confluence concern the existence and the uniqueness of normal forms, which are the results of a computation. When the focus is on *how to compute* the result, that is, on identifying reduction strategies with good properties, then only few abstract techniques are currently available (we mention [21, 36, 37], [52](Ch.8), and [2])—this paper proposes a new one.

**Factorization.** The most basic property about how to compute is *factorization*, whose paradigmatic example is the head factorization theorem of the $\lambda$-calculus (theorem 11.4.6 in

<figure><img src="image_2.png" /></figure>

© Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri;

licensed under Creative Commons License CC-BY

29th EACSL Annual Conference on Computer Science Logic (CSL 2021).

Editors: Christel Baier and Jean Goubault-Larrecq; Article No. 22; pp. 22:1–22:25

Leibniz International Proceedings in Informatics

<figure><img src="image_3.png" /></figure>

LIPICS

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 22:2 Factorize Factorization

Barendregt's book [11]): every $\beta$-reduction sequence $t \to_{\beta}^* u$ can be re-organized/factorized so as to first reducing head redexes and then everything else—in symbols $t \underset{h}{\stackrel{*}{\to}} \underset{-h}{\stackrel{*}{\to}} u$.

The study of factorization in $\lambda$-calculus goes back to Rosser [48]. Here, we adopt Melliès terminology [37]; please be aware that factorization results are sometimes referred to as *semi-standardization* (Mitschke in [41]), or *postponement* ([52]), and often simply called *standardization*—standardization is however a more sophisticated property (sketched below) of which factorization is a basic instance.

According to Melliès [37], the meaning of factorization is that the *essential* part of a computation can always be separated from its junk. Let's abstract the role of head reduction, by assuming that computations consists of steps $\underset{e}{\to}$ which are in some sense *essential*, and steps $\underset{i}{\to}$ which are not. Factorization says that every rewrite sequence $t \to^* s$ can be factorized as $t \underset{e}{\stackrel{*}{\to}} u \underset{i}{\stackrel{*}{\to}} s$, i.e., as a sequence of essential steps followed by inessential ones.

Well known examples of essential reductions are head and leftmost-outermost reduction for the $\lambda$-calculus (see Barendregt [11]), or left and weak reduction for the call-by-value $\lambda$-calculus (see Plotkin [44] and Paolini and Ronchi Della Rocca [47]).

Very much as confluence, factorization is a non-trivial property of $\lambda$-calculi; proofs require techniques such as finite developments [15, 52], labeling [35, 29], or parallel reduction [51].

**Uses of Factorization.** Factorization is commonly used as a *building block* in proving more sophisticated properties of the *how-to-compute* kind. It is often the main ingredient in proofs of *normalization* theorems [11, 51, 27, 3], stating that a reduction strategy reaches a normal form whenever one exists. Leftmost-outermost normalization is a well known example.

Another property, *standardization*, generalizes factorization: reduction sequences can be organized with respect to an order on redexes, not just with respect to the distinction essential/inessential. It is an early result that factorization can be used to prove standardization: iterated head factorizations provides what is probably the simplest way to prove Curry and Feys' left-to-right standardization theorem, via Mitschke's argument [41].

Additionally, the independence of some computational tasks, such as garbage collection, is often modeled as a factorization theorem.

**Contributions of this Paper.** In this paper we propose a technique for proving in a *modular* way factorization theorems for *compound higher-order systems*, such as those obtained by extending the $\lambda$-calculus with advanced features. The approach can be seen as an analogous for factorization of the classical technique for confluence based on Hindley-Rosen lemma, which we discuss in the next paragraphs. Mimicking the use of Hindley-Rosen lemma is natural, yet to our knowledge such an approach has never been used before, at least not in the $\lambda$-calculus literature. Perhaps this is because a direct transposition of Hindley-Rosen technique does not work with $\beta$ reduction, as we discuss below and in Sect. 3.

After developing a sharper technique, we apply it to various known extensions of the $\lambda$-calculus which do not fit into easily manageable categories of rewriting systems. In all our case studies, our novel proofs are neat, concise, and simpler than the originals.

**Confluence via Hindley-Rosen.** Let's consider confluence. The simplest modular technique to establish it is based on Hindley-Rosen lemma, which states that the *union* of two confluent reductions $\to_1$ and $\to_2$ is confluent if $\to_1$ and $\to_2$ satisfy a commutation property. This is the technique used in Barendregt's book for proving confluence of $\to_{\beta\eta}$ (Thm. 3.3.9 in [11]), where it is also stressed that the proof is simpler than Curry and Feys' original one.
While the result is basic, Hindley-Rosen technique provides a powerful tool to prove confluence of compound systems. In the literature of λ-calculus, we mention for instance its use in the linear-algebraic λ-calculus [7], the probabilistic λ-calculus [19], the Λµ-calculus [50], the shuffling calculus [14], the λ-calculus extended with lists [46] or pattern-matching [13], or with a *let* construct [6]. It is worth to spell-out the gain. Confluence is often a non-trivial property to establish—when higher-order is involved, the proof of confluence requires sophisticated techniques. The difficulty *compounds* when extending the λ-calculus with new constructs. Still, the problem is often originated by *β* reduction itself, which encapsulates the higher-order features of the computation. By using Hindley-Rosen lemma, confluence of *β* is used as a *black box*: one *relies* on that—without having to prove it again—to show that the extended calculus is confluent.

**Hindley-Rosen and Sufficient Conditions.** There is a subtle distinction between Hindley-Rosen *lemma*, and what we refer to as Hindley-Rosen *technique*. Hindley-Rosen lemma reduces confluence of a compound system to commutation of the components—the modules. To establish commutation, however, is a non-trivial task, because it is a *global* property, that is, it quantifies over *all sequences* of steps. The success of the lemma in the λ-calculus literature stems from the existence of easy to check conditions which suffice to prove commutation. All the examples which we have mentioned above indeed satisfy Hindley’s *strong commutation* property [26] (Lemma 3.3.6 in [11]), where at most one reduction—but not both—may require multiple steps to close a diagram; commutation follows by a finitary tiling argument. Strong commutation turns Hindley-Rosen lemma into an effective, concrete proof technique.

**Modular Factorization, Abstractly.** Here, we present a modular approach to factorization inspired by the Hindley-Rosen *technique*. A formulation of Hindley-Rosen lemma for factorization is immediate, and is indeed folklore. But exactly as for confluence, this reduces factorization of a compound system to a property that is difficult to establish, without a real gain. The crucial point is finding suitable conditions that can be used in practice. The *issue* here is that the natural adaptation of strong commutation to factorization is—in general—not verified by extensions of the λ-calculi, as it does not interact well with *β* (see Ex. 3.2 in Sect. 3). We identify an alternative condition—called *linear swap*—which is satisfied by a large variety of interesting examples, turning the approach into an effective, concrete *technique*. Testing the linear swap condition is easy and combinatorial in nature, as it is a *local* property, in the sense that only single steps (rather than sequences of steps) need to be manipulated. This holds true even when the modules are not confluent, or non-terminating. The other key point in our approach is that we *assume* the modules to be factorizing, therefore we can use their factorization—that may require non-trivial proof techniques such as parallel reductions or finite developments—as a black box.

**Modular Factorization, Concretely.** We then focus on our target, how to establish factorization results for extensions of the λ-calculus. Concretely, we start from *β* reduction, or its call-by-value counterpart $\beta_v$, and allow the calculus to be enriched with extra rules. Here we discover a further striking gain: for common factorization schemas such as head or weak factorization, verifying the required linear swap conditions reduces to checking a *single case*, together with the fact that the new rule behaves well with respect to substitution. The test for modular factorization which we obtain is a ready-to-use and easy recipe that can be applied in a variety of cases.

We illustrate our technique by providing several examples, chosen to stress the independence of the technique from other rewriting properties. In particular, we give a *new* and
arguably *simpler* proof of two results from the literature. The first is head factorization for the non-deterministic $\lambda$-calculus by de' Liguoro and Piperno [16], that extends the $\lambda$-calculus with a choice operator $\oplus$. It is a *non confluent* calculus, and it is representative of the class of $\lambda$-calculi extended with a commutative effect, such as *probabilistic* choice; indeed, most features and all issues are already present there, see [32] for a thorough discussion.

The second is a new, simplified proof of factorization for the shuffling calculus—a refinement of the call-by-value $\lambda$-calculus due to Carraro and Guerrieri [14], whose left factorization is proved by Guerrieri, Paolini, and Ronchi della Rocca in [23]. In this case the $\lambda$-calculus is extended with extra rules but they are not associated to a new operator. The resulting calculus is subtle, as it has critical pairs.

In both cases, the new proof is neat, conceptually clear, and strikingly short. The reason why our proofs are only a few lines long, whereas the originals require several pages, is exactly that there is no need to "prove again" factorization of $\beta$ or $\beta_v$. We just show that $\beta$ (resp. $\beta_v$) interacts well with the new rules.

**Further Applications: Probabilistic $\lambda$-calculi.** The investigation in this paper was triggered by concrete needs, namely the study of strategies for probabilistic $\lambda$-calculi [19, 34]. The probabilistic structure adds complexity, and indeed makes the study of factorization painful—exposing the need for tools to make such an analysis more manageable. Our technique smoothly applies, providing new concise proofs that are significantly simpler than the originals—indeed surprisingly simple. These results are however only overviewed in this paper: we sketch the application to the call-by-value probabilistic calculus by Faggian and Ronchi della Rocca [19], leaving the technical details in Appendix B. The reason is that, while the application of our technique is simple, the *syntax* of probabilistic $\lambda$-calculi is not—because reduction is defined on (monadic) structures representing probability distributions over terms. Aiming at making the paper accessible within the space limits, we prefer to focus on examples in a syntax which is familiar to a wide audience. Indeed, once the technique is understood, its application to other settings is immediate, and in large part automatic.

**A Final Remark.** Like Hindley-Rosen for confluence, our technique is sufficient but not necessary to factorization. Still, its features and wide range of application make it a remarkable tool to tame the complexity which is often associated to the analysis of advanced compound calculi. By emphasizing the benefits of a modular approach to factorization, we hope to prompt the development of even more techniques.

**Related work.** To our knowledge, the only result in the literature about modular techniques for factorization is Accattoli's technique for calculi with explicit substitutions [2], which relies on termination hypotheses. Our *linear swap* condition (page 8) is technically the same as his *diagonal-swap* condition. One of the insights at the inception of this work is exactly that termination in [2] is used only to establish factorization of each single module, but not when combining them. Here we *assume* modules to be factorizing, therefore avoiding termination requirements, and obtaining a more widely applicable technique.

Van Oostrom's decreasing diagrams technique [57] is a powerful and *inherently modular* tool to establish confluence and commutation. Surprisingly, it has not yet been used for factorization, but steps in this direction have been presented recently [56].

A divide-and-conquer approach is well-studied for termination. The key point is finding conditions which guarantee that the union of terminating relations is terminating. Several have been studied [10, 20]; the weakest such condition, namely $\rightarrow_2 \cdot \rightarrow_1 \subseteq \rightarrow_1 \cup \rightarrow_2 \cdot (\rightarrow_1 \cup \rightarrow_2)^*$, is introduced by Doornbos and von Karger [18], and then studied by Dershowitz [17], under
the name of lazy commutation, and by van Oostrom and Zantema [59]. Interestingly, lazy commutation is similar to the linear swap condition.

Finally, a somehow orthogonal approach to study extensions of a rewriting system, which is isolating syntactical classes of term rewriting systems that always satisfy a property. While confluence is the most studied property (e.g., [52], Ch 10.4), factorization and standardization are also investigated, in particular for left-to-right standardization ([52], Ch. 8.5.7).

## 2 Preliminaries

In this section we start by recalling some standard definitions and notations in rewriting theory (see e.g. [52] or [9]); we provide an overview of commutation, confluence, and factorization. Both confluence and factorization are forms of commutation.

**Basics.** An abstract rewriting system (ARS) (see [52], Ch.1) is a pair $A = (A, \to)$ consisting of a set $A$ and a binary relation $\to$ on $A$ whose pairs are written $t \to s$ and called steps. We denote $\to^*$ (resp. $\to^=$) the transitive-reflexive (resp. reflexive) closure of $\to$; we denote $\leftarrow$ the reverse relation of $\to$, i.e. $u \leftarrow t$ if $t \to u$. If $\to_1, \to_2$ are binary relations on $A$ then $\to_1 \cdot \to_2$ denotes their composition, i.e. $t \to_1 \cdot \to_2 s$ iff there exists $u \in A$ such that $t \to_1 u \to_2 s$. We write $(A, \{\to_1, \to_2\})$ to denote the ARS $(A, \to)$ where $\to = \to_1 \cup \to_2$. We freely use the fact that the transitive-reflexive closure of a relation is a closure operator, i.e. satisfies

$$ \to \subseteq \to^*, \quad (\to^*)^* = \to^*, \quad \to_1 \subseteq \to_2 \text{ implies } \to_1^* \subseteq \to_2^* \qquad (\text{Closure}) $$

The following property is an immediate consequence:

$$ (\to_1 \cup \to_2)^* = (\to_1^* \cup \to_2^*)^* \qquad (\text{TR}) $$

**Local vs Global Properties.** An important distinction in rewriting theory is between local and global properties. A property of term $t$ is local if it is quantified over only one-step reductions from $t$; it is global if it is quantified over all rewrite sequences from $t$. Local properties are easier to test, because the analysis (usually) involves a finite number of cases.

**Commutation.** Two relations $\to_1$ and $\to_2$ on $A$ commute if $\leftarrow_1^* \cdot \to_2^* \subseteq \to_2^* \cdot \leftarrow_1^*$.

**Confluence.** A relation $\to$ on $A$ is confluent if it commutes with itself. A classic tool to modularize the proof of confluence is Hindley-Rosen lemma. Confluence of two relations $\to_1$ and $\to_2$ does not imply confluence of $\to_1 \cup \to_2$, however it does if they commute.

**Lemma (Hindley-Rosen).** Let $\to_1$ and $\to_2$ be relations on the set $A$. If $\to_1$ and $\to_2$ are confluent and commute with each other, then $\to_1 \cup \to_2$ is confluent.

**Easy-to-Check Conditions for Hindley Rosen.** Commutation is a global condition, which is difficult to test. What turns Hindley-Rosen lemma into an effective, usable technique, is the availability of local, easy-to-check sufficient conditions. One of the simplest but most useful such conditions is Hindley's strong commutation [26]:

$$ \leftarrow_1 \cdot \to_2 \subseteq \to_2^* \cdot \leftarrow_1 = \qquad (\text{Strong Commutation}) $$

**Lemma 2.1 (Local test for commutation [26]).** Strong commutation implies commutation.

All the extensions of $\lambda$-calculus we cited at page 2 (namely [11, 7, 19, 50, 14, 46, 13, 6]) prove confluence by using Hindley-Rosen lemma via strong commutation (possibly in its weaker diamond-like form $\leftarrow_1 \cdot \to_2 \subseteq \to_2^* \cdot \leftarrow_1^*$).
## 22:6 Factorize Factorization

**Factorization.** We now recall definitions and basic facts on the rewriting property at the center of this paper, factorization. Let $\mathcal{A} = (\mathcal{A}, \{\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}\})$ be an ARS.

- The relation $\rightarrow = \stackrel{\rightarrow}{e} \cup \stackrel{\leftarrow}{i}$ satisfies **e-factorization**, written $\text{Fact}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i})$, if

$$ \text{Fact}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}) : (\stackrel{\rightarrow}{e} \cup \stackrel{\leftarrow}{i})^* \subseteq \stackrel{\rightarrow}{e}^* \cdot \stackrel{\leftarrow}{i}^* \quad (\text{Factorization}) $$

- The relation $\rightarrow \stackrel{\rightarrow}{i}$ **postpones** after $\stackrel{\rightarrow}{e}$, written $\text{PP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i})$, if

$$ \text{PP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}) : \stackrel{\rightarrow}{i}^* \cdot \stackrel{\rightarrow}{e}^* \subseteq \stackrel{\rightarrow}{e}^* \cdot \stackrel{\leftarrow}{i}^* \quad (\text{Postponement}) $$

Postponement can be formulated in terms of commutation, and viceversa, since clearly $(\stackrel{\rightarrow}{i} \text{ postpones after } \stackrel{\rightarrow}{e})$ if and only if $(\stackrel{\leftarrow}{i} \text{ commutes with } \stackrel{\rightarrow}{e})$. Note that reversing $\stackrel{\rightarrow}{i}$ introduce an asymmetry between the two relations. It is an easy result that **e-factorization** is equivalent to postponement, which is a more convenient way to express it. The following equivalences—which we shall use freely—are all well known.

**Lemma 2.2.** For any two relations $\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}$ the following statements are equivalent:

1. Semi-local postponement: $\stackrel{\rightarrow}{i}^* \cdot \stackrel{\rightarrow}{e} \subseteq \stackrel{\rightarrow}{e}^* \cdot \stackrel{\leftarrow}{i}^*$ (and its dual $\stackrel{\leftarrow}{i} \cdot \stackrel{\rightarrow}{e}^* \subseteq \stackrel{\rightarrow}{e}^* \cdot \stackrel{\leftarrow}{i}^*$).

2. Postponement: $\text{PP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i})$.

3. Factorization: $\text{Fact}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i})$.

Another property that we shall use freely is the following, which is immediate by the definition of postponement and property TR (page 5).

**Property 2.3.** Given a relation $\stackrel{\rightarrow}{e}$ such that $\stackrel{\rightarrow}{i}^* = \stackrel{\rightarrow}{i}^*, \text{PP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i})$ if and only if $\text{PP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i})$.

A well-known use of the above is to instantiate $\stackrel{\rightarrow}{e}$ with a notion of parallel reduction ([51]).

**Easy-to-Check Sufficient Condition for Postponement.** Hindley first noted that a local property implies postponement, hence factorization [26]. It is immediate to recognize that the property below is exactly the postponement analog of strong commutation in Lemma 2.1; indeed it is the same expression, with $\stackrel{\rightarrow}{i} := \leftarrow_1$ and $\stackrel{\leftarrow}{e} := \rightarrow_2$.

We say that $\stackrel{\rightarrow}{i}$ **strongly postpones** after $\stackrel{\rightarrow}{e}$, if

$$ \text{SP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}) : \stackrel{\rightarrow}{i} \cdot \stackrel{\rightarrow}{e} \subseteq \stackrel{\rightarrow}{e}^* \cdot \stackrel{\leftarrow}{i} = \quad (\text{Strong Postponement}) $$

**Lemma 2.4 (Local test for postponement [26]).** Strong postponement implies postponement:

$$ \text{SP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}) \text{ implies } \text{PP}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}), \text{ and so } \text{Fact}(\stackrel{\rightarrow}{e}, \stackrel{\leftarrow}{i}). $$

Strong postponement is at the heart of several factorization proofs. However (similarly to the diamond property for confluence) it can rarely be used *directly*, because most interesting relations—e.g. $\beta$ reduction in $\lambda$ calculus—do not satisfy it. Still, its range of application hugely widens by using Lemma 2.3.

It is instructive to examine strong postponement with respect to $\beta$ reduction; this allows us also to recall why it is difficult to establish head factorization for the $\lambda$-calculus.

**Example 2.5 ($\lambda$-calculus and strong postponement).** In view of head factorization, the $\beta$ reduction is decomposed in head reduction $\stackrel{\rightarrow}{h} \stackrel{\rightarrow}{\beta}$ and its dual $\stackrel{\leftarrow}{h} \stackrel{\leftarrow}{\beta}$, that is $\rightarrow \beta = \stackrel{\rightarrow}{h} \stackrel{\rightarrow}{\beta} \cup \stackrel{\leftarrow}{h} \stackrel{\leftarrow}{\beta}$. To prove head factorization is non trivial precisely because $\text{SP}(\stackrel{\rightarrow}{h} \stackrel{\rightarrow}{\beta}, \stackrel{\leftarrow}{h} \stackrel{\leftarrow}{\beta})$ does not hold.

Consider the following example: $(\lambda x.xxx)(Iz) \stackrel{\rightarrow}{h} \stackrel{\rightarrow}{\beta} (\lambda x.xxx)z \stackrel{\rightarrow}{h} zzz$. The sequence $\stackrel{\rightarrow}{h} \stackrel{\rightarrow}{h}$ can only postpone to a reduction sequence of shape $\stackrel{\rightarrow}{h} \stackrel{\rightarrow}{h} \stackrel{\rightarrow}{h} \stackrel{\rightarrow}{h}$
$$ (\lambda x.xxx)(Iz) \underset{\bar{h}}{\to} \beta (Iz)(Iz)(Iz) \underset{\bar{h}}{\to} \beta z(Iz)(Iz) \underset{\bar{h}}{\to} \beta zz(Iz) \underset{\bar{h}}{\to} \beta zzz $$

A solution is to compress sequences of $\underset{\bar{h}}{\to}$ by introducing an intermediate relation $\underset{\bar{h}}{\to}^* \alpha$ (internal parallel reduction) such that $\underset{\bar{h}}{\to}^* = \underset{\bar{h}}{\to} \beta^*$ and which does verify strong postponement. This is indeed the core of Takahashi's technique [51]. All the work in [51] goes into defining parallel reductions, and proving $\text{SP}(\underset{\bar{h}}{\to} \beta, \underset{\bar{h}}{\to} \alpha)$. One indeed has $\underset{\bar{h}}{\to} \alpha \cdot \underset{\bar{h}}{\to} \beta \subseteq \underset{\bar{h}}{\to} \beta \cdot \underset{\bar{h}}{\to} \beta^* \cdot \underset{\bar{h}}{\to} \alpha$.

### 3 Modularizing Factorization

All along this section, we assume to have two relations $\to_\alpha, \to_\gamma$ on the same set A, such that

$$ \to_\alpha = \bar{e}^\alpha \cup \bar{e}^\gamma \text{ and } \to_\gamma = \bar{e}^\gamma \cup \bar{e}^\alpha. $$

We define $\bar{e}^\alpha := (\bar{e}^\alpha \cup \bar{e}^\gamma)$ and $\bar{e}^\gamma := (\bar{e}^\alpha \cup \bar{e}^\gamma)$. Clearly $\to_\alpha \cup \to_\gamma = \bar{e}^\alpha \cup \bar{e}^\gamma$. Our goal is obtaining a technique in the style of Hindley-Rosen's for confluence, to establish that if $\to_\alpha, \to_\gamma$ are e-factorizing then their union also is, that is, $\text{Fact}(\bar{e}^\alpha, \bar{e}^\gamma)$ holds.

**Issues.** In spite of the large and fruitful use in the $\lambda$-calculus literature of Hindley-Rosen technique to simplify the analysis of confluence, we are not aware of any similar technique in the analysis of factorization. In this section we explain why a transposition of the technique is not immediate when $\beta$ reduction is involved.

A direct equivalent of Hindley-Rosen lemma for commutation is folklore. An explicit proof is in [57]. Formulated in terms of postponement we obtain the following statement.

**► Lemma 3.1 (Hindley-Rosen transposed to factorization).** Assume $\to_\alpha$ and $\to_\gamma$ are e-factorizing relations. Their union $\to_\alpha \cup \to_\gamma$ satisfies $\text{Fact}(\bar{e}^\alpha, \bar{e}^\gamma)$ if

$$ \text{PP}(\bar{e}^\alpha, \bar{e}^\gamma) : \bar{e}^\alpha \cdot \bar{e}^\gamma \subseteq \bar{e}^\gamma \cdot \bar{e}^\alpha \quad \text{and} \quad \text{PP}(\bar{e}^\alpha, \bar{e}^\gamma) : \bar{e}^\gamma \cdot \bar{e}^\alpha \subseteq \bar{e}^\alpha \cdot \bar{e}^\gamma \quad (\#) $$

Exactly as Hindley-Rosen lemma, the modularization lemma above is of no practical use by itself, as the pair of conditions $(\#)$ one has to test are as global as the original problem. What we need is to have local conditions (akin to strong commutation) to turn the lemma into a usable technique. One obvious choice is strong postponement:

$$ \text{SP}(\bar{e}^\alpha, \bar{e}^\gamma) : \bar{e}^\alpha \cdot \bar{e}^\gamma \subseteq \bar{e}^\gamma \cdot \bar{e}^\alpha = \quad \text{and} \quad \text{SP}(\bar{e}^\alpha, \bar{e}^\gamma) : \bar{e}^\gamma \cdot \bar{e}^\alpha \subseteq \bar{e}^\alpha \cdot \bar{e}^\gamma = \quad (\#\#) $$

Clearly, $(\#\#)$ implies $(\#)$ (Lemma 2.4). We may hope to have all the elements for a postponement analog of Hindley-Rosen technique, but it is not the case. Unfortunately, conditions $(\#\#)$ usually do not hold in extensions of the $\lambda$-calculus. Let us illustrate the issue with an example, the non-deterministic $\lambda$-calculus, that we shall develop formally in Sect. 5.

**► Example 3.2 (Issues).** Consider the extension of the language of $\lambda$-terms with a construct $\oplus$ which models non-deterministic choice. The term $\oplus pq$ non-deterministically reduces to either $p$ or $q$, i.e. $\oplus pq \to_\oplus p$ or $\oplus pq \to_\oplus q$. The calculus $(\Lambda, \{\to_\beta, \to_\oplus\})$ has two reduction rules, $\to_\beta$ and $\to_\oplus$. For both, we define head and non-head steps as usual.

Consider the following sequence: $(\lambda x.xxx)(\oplus pq) \underset{\bar{h}}{\to} (\lambda x.xxx)p \underset{\bar{h}}{\to} \beta ppp$. This sequence $\underset{\bar{h}}{\to} \beta$ can only postpone to a reduction sequence of shape $\underset{\bar{h}}{\to} \beta \cdot \underset{\bar{h}}{\to} \beta \cdot \underset{\bar{h}}{\to} \beta \cdot \underset{\bar{h}}{\to} \beta$:

$$ (\lambda x.xxx)(\oplus pq) \underset{\bar{h}}{\to} \beta (\oplus pq)(\oplus pq)(\oplus pq) \underset{\bar{h}}{\to} p(\oplus pq)(\oplus pq) \underset{\bar{h}}{\to} ppp(\oplus pq) \underset{\bar{h}}{\to} ppp. $$

Since the $\beta$-step duplicates the redex $\oplus pq$, the condition $\text{SP}(\underset{\bar{h}}{\to} \beta, \underset{\bar{h}}{\to} \alpha) : \underset{\bar{h}}{\to} \beta \cdot \underset{\bar{h}}{\to} \alpha \subseteq \underset{\bar{h}}{\to} \beta^* \cdot \underset{\bar{h}}{\to} \alpha = \text{ does not hold.}$ The phenomenon is similar to Ex. 2.5, but now moving to parallel reduction is
## 22:8 Factorize Factorization

not a solution: the problem here is not just compressing steps, but the fact that by swapping $\xrightarrow{\rightarrow h \oplus}$ and $\xrightarrow{\rightarrow h \beta}$, a third relation $\xrightarrow{\rightarrow h \oplus}$ appears.

Note that the problem above is specific to factorization, and does not appear with confluence.

**A Robust Condition for Modular Factorization.** Inspired by Accattoli's study of factorization for $\lambda$-calculi with explicit substitutions [2], we consider an alternative sufficient condition for modular factorization, which holds in many examples, as the next sections shall show.

We say that $\xrightarrow{\rightarrow i \alpha}$ linearly swaps with $\xrightarrow{\rightarrow e \gamma}$ if

$$ \text{1Swap}(\xrightarrow{i}\alpha, \xrightarrow{e}\gamma) : \xrightarrow{i}\alpha \cdot \xrightarrow{e}\gamma \subseteq \xrightarrow{e}\gamma \cdot \xrightarrow{\alpha}^* \qquad (\text{Linear Swap}) $$

Note that, on the right-hand side, the relation is $\xrightarrow{\rightarrow \alpha}^*$, not $\xrightarrow{i} \alpha$. This small change will make a big difference, and overcome the issue we have seen in Ex. 3.2 (note that there $\xrightarrow{i} \beta \xrightarrow{\rightarrow h \oplus} \subseteq \xrightarrow{\rightarrow h} \beta \xrightarrow{\rightarrow h} \beta^*$ holds). Perhaps surprisingly, this easy-to-check condition, which is *local* and *linear* in $\xrightarrow{e} \gamma$, suffices, and holds in a large variety of cases. Moreover, it holds *directly* (even with $\beta$) that is, without the mediating role of parallel reductions (as it is the instead the case of Takahashi's technique, see Ex. 2.5).

We finally obtain a modular factorization technique, via the following easy property.

$$ \text{Lemma 3.3.} \quad \xrightarrow{\rightarrow a} \xrightarrow{\rightarrow b} \subseteq \xrightarrow{\rightarrow b} \cdot \xrightarrow{\rightarrow c}^* \text{ implies } \xrightarrow{\rightarrow a} \cdot \xrightarrow{\rightarrow b} \subseteq \xrightarrow{\rightarrow b} \cdot \xrightarrow{\rightarrow c}^*. $$

**Theorem 3.4 (Modular factorization).** Let $\xrightarrow{\rightarrow \alpha} = (\xrightarrow{e} \alpha \cup \xrightarrow{i} \alpha)$ and $\xrightarrow{\rightarrow \gamma} = (\xrightarrow{e} \gamma \cup \xrightarrow{i} \gamma)$ be e-factorizing relations. The union $\xrightarrow{\rightarrow \alpha} \cup \xrightarrow{\rightarrow \gamma}$ satisfies e-factorization Fact $(\xrightarrow{e}, \xrightarrow{i})$, for $\xrightarrow{e} := \xrightarrow{e} \alpha \cup \xrightarrow{e} \gamma$, and $\xrightarrow{i} := \xrightarrow{i} \alpha \cup \xrightarrow{i} \gamma$, if the following linear swaps hold:

$$ \text{1Swap}(\xrightarrow{i} \alpha, \xrightarrow{e} \gamma) : \xrightarrow{i} \alpha \cdot \xrightarrow{e} \gamma \subseteq \xrightarrow{e} \gamma \cdot \xrightarrow{\alpha}^* \quad \text{and} \quad \text{1Swap}(\xrightarrow{i} \gamma, \xrightarrow{e} \alpha) : \xrightarrow{i} \gamma \cdot \xrightarrow{e} \alpha \subseteq \xrightarrow{e} \alpha \cdot \xrightarrow{\gamma}^* $$

**Proof.** We prove that the assumptions imply $\text{SP}(\xrightarrow{e}, \xrightarrow{i} \alpha^* \cup \xrightarrow{i} \gamma^*)$, hence $\text{PP}(\xrightarrow{e}, \xrightarrow{i} \alpha^* \cup \xrightarrow{i} \gamma^*)$ (by Lemma 2.4). Therefore $\text{PP}(\xrightarrow{e}, \xrightarrow{i})$ by Lemma 2.3 (because $(\xrightarrow{i} \alpha \cup \xrightarrow{i} \gamma)^* = (\xrightarrow{i} \alpha^* \cup \xrightarrow{i} \gamma^*)^*$ by property TR), and so $\text{Fact}(\xrightarrow{e}, \xrightarrow{i})$ holds.

To verify $\text{SP}(\xrightarrow{e} \alpha \cup \xrightarrow{e} \gamma, \xrightarrow{i} \alpha^* \cup \xrightarrow{i} \gamma^*)$, we observe that the following holds:

$$ \xrightarrow{i} k^* \cdot \xrightarrow{e} j \subseteq (\xrightarrow{e} j \cup \xrightarrow{e} k)^* \cdot \xrightarrow{i} k^* \quad \text{for all } k, j \in \{\alpha, \gamma\} $$

- Case $j = k$. This is immediate by e-factorization of $\xrightarrow{\rightarrow \alpha}$ and $\xrightarrow{\rightarrow \gamma}$, and by Lemma 2.2.1.

- Case $j \neq k$. $\text{1Swap}(\xrightarrow{i} \alpha, \xrightarrow{e} \gamma)$ implies $(\xrightarrow{i} \alpha)^* \cdot \xrightarrow{e} \gamma \subseteq \xrightarrow{e} \gamma \cdot \xrightarrow{\alpha}^*$, by Lemma 3.3. Since $\xrightarrow{\rightarrow \alpha}$ e-factorizes, we obtain $(\xrightarrow{i} \alpha)^* \cdot \xrightarrow{e} \gamma \subseteq \xrightarrow{e} \gamma \cdot \xrightarrow{e} \alpha^* \cdot \xrightarrow{i} \alpha^*$. Similarly for $\text{1Swap}(\xrightarrow{i} \gamma, \xrightarrow{e} \alpha)$. $\quad \blacksquare$

Note that in the proof of Theorem 3.4, the assumption that $\xrightarrow{\rightarrow \alpha}$ and $\xrightarrow{\rightarrow \gamma}$ factorize is crucial. Using that, together with Lemma 3.3, we obtain $\text{SP}(\xrightarrow{e}, \xrightarrow{i} \alpha^*)$, that is, $\xrightarrow{i} \alpha^*$ postpones after both e-steps, (and similarly for $\xrightarrow{i} \gamma^*$). Note also that $\text{1Swap}(\xrightarrow{i} \alpha, \xrightarrow{e})$—taken alone—does not imply $\text{PP}(\xrightarrow{e}, \xrightarrow{i})$. For instance, let's consider again Ex. 2.5. It is clear that $\text{1Swap}(\xrightarrow{-h} \beta, \xrightarrow{h} \beta)$ holds and yet it does not imply $\text{Fact}(\xrightarrow{h} \beta, \xrightarrow{-h} \beta)$. Stronger tools, such as parallel reduction or finite development are needed here—there is no magic.

The next sections apply the modularization result to various $\lambda$-calculus extensions.
**Linear Postponement.** We collect here two easy properties which shall simplify the proof of factorization in several of the case studies (use Lemma 3.3).

► **Lemma 3.5 (Linear postponement).**

1. $(\vec{i} \cdot \vec{e} \subseteq \vec{e} \cdot \vec{i}^*) \Rightarrow \text{SP}(\vec{e}, \vec{i}^*) \Rightarrow \text{Fact}(\vec{e}, \vec{i})$.

2. $(\vec{i} \cdot \vec{e} \subseteq \vec{e} \cdot \vec{i}^*) \Rightarrow \text{SP}(\vec{e}, \vec{i}) \Rightarrow \text{Fact}(\vec{e}, \vec{i})$.

**Factorization vs. Confluence.** Factorization and confluence are *independent* properties. In Sect. 5 we apply our modular factorization technique to a non-confluent calculus. Conversely, $\beta\eta$, which is confluent, does not verify head nor leftmost factorization, even though both $\beta$ and $\eta$—separately—do.

# 4 Extensions of the Call-by-Name $\lambda$-Calculus: Head Factorization

We shall study factorization theorems for extensions of both of the call-by-name (shortened to CbN) and of the call-by-value (CbV) $\lambda$-calculus. The CbN $\lambda$-calculus—also simply known as $\lambda$-calculus—is the set of $\lambda$-terms $\Lambda$, equipped with the $\beta$-reduction, while the CbV $\lambda$-calculus is the set of $\lambda$-terms $\Lambda$, equipped with the $\beta_v$-reduction.

In this section, we first revise the language of the $\lambda$-calculus; we then consider the case when the calculus is *enriched with new operators*, such as a non-deterministic choice or a fix-point operator—so, together with $\beta$, we have other reduction rules. We study in this setting *head factorization*, which is by far the most important and common factorization scheme in $\lambda$-calculus. We show that here Theorem 3.4 further simplifies, providing an easy, *ready-to-use* test for head factorization of compound systems (Proposition 4.5). Indeed, verifying the two linear swap conditions of Theorem 3.4 now reduces to a single, simple test. Such a simplification only relies on $\beta$ and on the properties of contextual closure; it holds independently from the specific form of the extra rule.

## 4.1 The (Applied) $\lambda$-Calculus

Since in the next sections we shall extend the $\lambda$-calculus with new operators, such as a non-deterministic choice $\oplus$ or a fix-point $Y$, we allow in the syntax a set of constants, meant to represent such operators. So, for instance, in Sect. 5 we shall see $\oplus$ as a constant. This way factorization results with respect to $\beta$-reduction can be seen as holding also in the $\lambda$-calculus with extended syntax—this is absolutely harmless.

Note that despite the fact that the classic Barendregt's book [11] defines the $\lambda$-calculus without constants (the calculus is pure), other classic references such as Hindley and Seldin's book [25] or Plotkin [44] do include constants in the language of terms—thus there is nothing exotic in our approach. Following Hindley and Seldin, when the set of constants is empty, the calculus is called *pure*, otherwise *applied*.

**The Language.** The following grammars generate $\lambda$-terms and contexts.

$$ t, p, q, r ::= x \mid c \mid \lambda x.t \mid tt \quad (\text{terms } \Lambda) \qquad C ::= \langle \rangle \mid tC \mid Ct \mid \lambda x.C \quad (\text{contexts}) $$

where $x$ ranges over a countable set of *variables*, $c$ over a disjoint (finite, infinite or empty) set of constants. Variables and constants are *atoms*, terms of shape $pq$ are *applications*, and $\lambda x.p$ abstractions. If the constants are $c_1, \dots, c_n$, the set of terms is sometimes noted as $\Lambda_{c_1 \dots c_n}$.

The plugging $C\langle t \rangle$ of a term $t$ into a context is the operation replacing the only occurrence of a hole $\langle \rangle$ in $C$ with $t$, potentially capturing free variables of $C$.
## 22:10 Factorize Factorization

A reduction step $\rightarrow_{\gamma}$ is defined as the contextual closure of a root relation $\mapsto_{\gamma}$ on $\Lambda$, which is called a rule. Explicitly, if $r \mapsto_{\gamma} r'$, then $t \rightarrow_{\gamma} s$ holds if $t = C\langle r \rangle$ and $s = C\langle r' \rangle$, for some context $C$. The term $r$ is called a $\gamma$-redex. Given two rules $\mapsto_{\alpha}, \mapsto_{\gamma}$ on $\Lambda$, the relation $\rightarrow_{\alpha\gamma}$ is $\rightarrow_{\alpha} \cup \rightarrow_{\gamma}$, which can equivalently be defined as the contextual closure of $\mapsto_{\alpha} \cup \mapsto_{\gamma}$.

The (CbN) $\lambda$-calculus is $(\Lambda, \rightarrow_{\beta})$, the set of terms together with $\beta$-reduction $\rightarrow_{\beta}$, defined as the contextual closure of the $\beta$-rule: $(\lambda x.p)q \mapsto_{\beta} p\{x:=q\}$ where $p\{x:=q\}$ denotes capture-avoiding substitution. We silently work modulo $\alpha$-equivalence.

**Properties of the Contextual Closure.** Here we recall basic properties about contextual closures and substitution, preparing the ground for the simplifications studied next.

A relation $\mapsto$ on terms is substitutive if

$$r \mapsto r' \text{ implies } r\{x:=q\} \mapsto r'\{x:=q\}. \qquad (\text{substitutive})$$

An obvious induction on the shape of terms shows the following (see Barendregt [11], p. 54).

**► Property 4.1 (Substitutive).** Let $\rightarrow_{\gamma}$ be the contextual closure of $\mapsto_{\gamma}$.

1. If $\mapsto_{\gamma}$ is substitutive then $\rightarrow_{\gamma}$ is substitutive: $p \rightarrow_{\gamma} p'$ implies $p\{x:=q\} \rightarrow_{\gamma} p'\{x:=q\}$.

2. If $q \rightarrow_{\gamma} q'$ then $t\{x:=q\} \rightarrow_{\gamma} t\{x:=q'\}$.

We recall a basic but key property of contextual closures. If a step $\rightarrow_{\gamma}$ is obtained by closure under non-empty context of a rule $\mapsto_{\gamma}$, then it preserves the shape of the term:

**► Property 4.2 (Shape preservation).** Assume $t = C\langle r \rangle \rightarrow C\langle r' \rangle = t'$ and that context $C$ is non-empty. The term $t'$ is an application (resp. an abstraction) if and only if $t$ is.

Notice that since the closure under empty context of $\mapsto_{\gamma}$ is always an essential step (whatever head, left, or weak), Property 4.2 implies that non-essential steps always preserve the shape of terms—we spell this out in Property A.1 and A.2 in the Appendix. Please notice that we shall often write $\mapsto_{\gamma}$ to indicate the step $\rightarrow_{\gamma}$ which is obtained by empty contextual closure.

**Head Reduction.** Head contexts are defined as follows:

$$H ::= \lambda x_1 \dots \lambda x_n. \langle \rangle t_1 \dots t_n \qquad (\text{head contexts})$$

where $k \ge 0$ and $n \ge 0$. A non-head context is a context which is not head. A head step $\rightarrow_{\gamma}$ (resp. non-head step $\leftarrow_{\gamma}$) is defined as the closure under head contexts (resp. non-head contexts) of rule $\mapsto_{\gamma}$. Obviously, $\rightarrow_{\gamma} = \rightarrow_{\gamma} \cup \leftarrow_{\gamma}$.

Note that the empty context $\langle \rangle$ is a head context. Therefore $\mapsto_{\gamma} \subseteq \rightarrow_{\gamma}$ holds (a fact which we shall freely use) and Property 4.2 always applies to non-head steps.

## 4.2 Call-by-Name: Head Factorization, Modularly.

Head factorization is of great importance for the theory of the CbN $\lambda$-calculus, which is why head factorization for $\rightarrow_{\beta}$ is well studied. If we consider a calculus $(\Lambda, \rightarrow_{\beta} \cup \rightarrow_{\gamma})$, where $\rightarrow_{\gamma}$ is a new reduction added to $\beta$, our modular technique (Theorem 3.4) states that the compound system $\rightarrow_{\beta} \cup \rightarrow_{\gamma}$ satisfies head factorization if $\rightarrow_{\gamma}$ does, and both $\text{1Swap}(\leftarrow_{\gamma}, \rightarrow_{\beta}, \rightarrow_{\gamma})$ and $\text{1Swap}(\leftarrow_{\gamma}, \rightarrow_{\beta}, \rightarrow_{\gamma})$ hold. We show that in the head case our technique simplifies even more, reducing to the test in Proposition 4.5.

First, we observe that in this case, any linear swap condition can be tested by considering for the head step only the root relation $\mapsto$, that is, only the closure of $\mapsto$ under empty context, which is a head step by definition. This is expressed in the following lemma, where we include also a variant, that shall be useful later on.
**► Lemma 4.3 (Lifting root linear swaps).** Let $\mapsto_{\alpha}, \mapsto_{\gamma}$ be root relations on $\Lambda$.

1. $\underset{-h}{\to} \alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\to} \gamma \cdot \to_{\alpha}^{*}$ implies $\text{1Swap}(\underset{-h}{\to} \alpha, \underset{-h}{\to} \gamma)$.

2. Similarly, $\underset{-h}{\to} \alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\to} \gamma \cdot \to_{\alpha}^{\equiv}$ implies $\underset{-h}{\to} \alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\to} \gamma \cdot \to_{\alpha}^{\equiv}$.

Second, since we are studying $\to_{\beta} \cup \to_{\gamma}$, one of the linear swaps is $\text{1Swap}(\underset{-h}{\to} \gamma, \underset{h}{\to} \beta)$. We show that, whatever is $\to_{\gamma}$, it linearly swaps with $\underset{-h}{\to} \beta$ as soon as $\mapsto_{\gamma}$ is substitutive.

**► Lemma 4.4 (Swap with $\underset{-h}{\to} \beta$).** If $\mapsto_{\gamma}$ is substitutive then $\text{1Swap}(\underset{-h}{\to} \gamma, \underset{h}{\to} \beta)$ holds.

The proofs of these two lemmas are in Appendix A.1.

Summing up, since head factorization for $\beta$ is known, we obtain the following test to verify that the compound system $\to_{\beta} \cup \to_{\gamma}$ satisfies head factorization $\text{Fact}(\underset{h}{\to} \beta \cup \underset{h}{\to} \gamma, \underset{-h}{\to} \beta \cup \underset{-h}{\to} \gamma)$.

**► Proposition 4.5 (A test for modular head factorization).** Let $\to_{\beta}$ be $\beta$-reduction and $\to_{\gamma}$ be the contextual closure of a rule $\mapsto_{\gamma}$. Their union $\to_{\beta} \cup \to_{\gamma}$ satisfies head factorization if:

1. Head factorization of $\to_{\gamma}: \text{Fact}(\underset{h}{\to} \gamma, \underset{-h}{\to} \gamma)$.

2. Root linear swap: $\underset{-h}{\to} \beta \cdot \mapsto_{\gamma} \subseteq \underset{h}{\to} \gamma \cdot \to_{\beta}^{*}$.

3. Substitutivity: $\mapsto_{\gamma}$ is substitutive.

Note that none of the properties concerns $\to_{\beta}$ alone, as we already know that head factorization of $\to_{\beta}$ holds. In Sect. 5 we shall use our test (Proposition 4.5) to prove head factorization for the non-deterministic $\lambda$-calculus. The full proof is only a few lines long.

We conclude by observing that Lemma 4.3 gives either a proof that the swap conditions hold, or a counter-example. Let us give an example of this latter use.

**► Example 4.6 (Finding counter-examples).** The test of Proposition 4.5 can also be used to provide a counter-example to head factorization when it fails. Let's instantiate $\to_{\gamma}$ with $\to_{\eta}$, that is, the contextual closure of rule $\lambda x . tx \mapsto_{\eta} t$ if $x \notin fv(t)$. Now, consider the root linear swap: $t := \lambda x . (II)(Ix) \underset{-h}{\to} \beta \lambda x . (II)x \mapsto_{\eta} II :=: s$, where $I := \lambda z . z$. Note that $t$ has no $\underset{h}{\to} \eta$ step, and so the two steps cannot be swapped. The reduction sequence above is a *counter-example to both head and leftmost factorization for $\beta\eta$*. Start with the head (and leftmost) redex $II: \lambda x . (II)(Ix) \underset{h}{\to} \beta\eta \lambda x . I(Ix)$. From $\lambda x . I(Ix)$, there is no way to reach $s$. We recall that $\beta\eta$ still satisfies leftmost normalization—the proof is non-trivial [29, 51, 58, 28].

# 5 The Non-Deterministic $\lambda$-Calculus $\Lambda_{\oplus}$

De' Liguoro and Piperno's non-deterministic $\lambda$-calculus $\Lambda_{\oplus}$ is defined in [16] by extending the $\lambda$-calculus with a new operator $\oplus$ whose rule models *non-deterministic choice*. Intuitively, $t \oplus p$ non-deterministically rewrites to either $t$ or $p$. Notably, $\Lambda_{\oplus}$ is *not confluent*, hence it is a good example of the fact that confluence and factorization are independent properties.

We briefly recall $\Lambda_{\oplus}$ and its features, then use our technique to give a *novel and neat proof of de' Liguoro and Piperno's head factorization result* (Cor. 2.10 in [16]).

**Syntax.** We slightly depart from the presentation in [16], as we consider $\oplus$ as a constant, and write $\oplus tp$ rather than $t \oplus p$, working as usual for the $\lambda$-calculus with constants (see e.g.,
[25], or [11], Sec. 15.3)<fnref n="1" />. Terms and contexts are generated by:

$$ t, p, q, r ::= x | \oplus | \lambda x.t | tp \quad (\text{terms } \Lambda_{\oplus}) \quad C ::= \langle \rangle | tC | Ct | \lambda x.C \quad (\text{contexts}) $$

As before, $\to_\beta$ denotes $\beta$-reduction, while the rewrite step $\to_\oplus$ is the contextual closure of the following non-deterministic rule: $\oplus tp \mapsto_\oplus t$ and $\oplus tp \mapsto_\oplus p$.

**Subtleties.** The calculus $(\Lambda_\oplus, \to_\beta \cup \to_\oplus)$ is non trivial. Of course, $\to$ is not confluent. Moreover, the following examples from [16] show that permuting $\beta$ and $\oplus$ steps is delicate.

- $\to_\oplus$ creates $\beta$-redexes. For instance, $((\lambda x.x) \oplus y)z \to_\oplus (\lambda x.x)z \to_\beta z$, hence the $\to_\oplus$-step cannot be postponed after $\to_\beta$.

- **Choice duplication.** Postponing $\to_\beta$ after $\to_\oplus$ is also problematic, because $\beta$-steps may multiply choices, introducing new results: flipping a coin and duplicating the result is not equivalent to duplicating the coin and then flipping twice. For instance, let $t = (\lambda x.xx)(\oplus pq)$. Duplicating first one may have $t \to_\beta (\oplus pq)(\oplus pq) \to_\oplus q(\oplus pq) \to_\oplus qp$ while flipping first one has $t \to_\oplus (\lambda x.xx)p \to_\beta pp$ or $t \to_\oplus (\lambda x.xx)q \to_\beta qq$ but in both cases $qp$ cannot be reached.

These examples are significant as the same issues impact any calculus with choice effects.

**Head Factorization.** The head (resp. non-head)<fnref n="2" /> rewrite steps $\to_h^\beta$ and $\to_h^{\to_\oplus}$ (resp. $\to_{-h}^\beta$ and $\to_{-h}^{\to_\oplus}$) are defined as the closure by head (resp. non-head) contexts of rules $\mapsto_\beta$ and $\mapsto_\oplus$, respectively. We also set $\to_h := \to_h^\beta \cup \to_h^{\to_\oplus}$ and $\to_{-h} := \to_{-h}^\beta \cup \to_{-h}^{\to_\oplus}$.

De' Liguoro and Piperno prove that despite the failure of confluence, $\Lambda_\oplus$ satisfies head factorization. They prove this result via standardization, following Klop's technique [29].

**► Theorem 5.1 (Head factorization, Cor. 2.10 in [16].)** Fact($\to_h, \to_{-h}$) holds in the non-deterministic $\lambda$-calculus $\Lambda_\oplus$.

**A New Proof, Modularly.** We give a novel, strikingly simple proof of Fact($\to_h, \to_{-h}$), simply by proving that $\to_\beta$ and $\to_\oplus$ satisfy the hypotheses of the test for modular head factorization (Proposition 4.5). All the ingredients we need are given by the following easy lemma.

- **Lemma 5.2 (Root linear swaps).** 1. $t \to_{-h}^\beta p \mapsto_\oplus q$ implies $t \mapsto_\oplus \cdot \to_\beta q$.

2. $t \to_{-h}^\oplus p \mapsto_\oplus q$ implies $t \mapsto_\oplus \cdot \to_\beta q$.

**Proof.** 1. Let $p = \oplus p_1 p_2$ and assume $\oplus p_1 p_2 \mapsto_\oplus p_i = q$, with $i \in \{1, 2\}$. Since $t \to_\beta p$, by Property 4.2 (as spelled-out in Property A.1), $t$ has shape $\oplus t_1 t_2$, with $\oplus t_1 t_2 \to_{-h}^\beta \oplus p_1 p_2$. Therefore, either $t_1 \to_\beta p_1$ or $t_2 \to_\beta p_2$, from which $t = \oplus t_1 t_2 \mapsto_\oplus t_i \to_\beta q$.

2. The proof is the same as above, just replace $\beta$ with $\oplus$.

**► Theorem 5.3 (Testing head factorization).** We have Fact($\to_h, \to_{-h}$) because we have:

1. Head factorization of $\to_\oplus$: Fact($\to_h^\oplus, \to_{-h}^\oplus$).

2. Root linear swap: $\to_h^\beta \cdot \mapsto_\oplus \beta \subseteq \to_h^{\to_\oplus} \cdot \to_\beta$.

3. Substitutivity: $\mapsto_\oplus$ is substitutive.

<footnote n="1">¹ Note that there is no loss with respect to the syntax in [16], where $\oplus$ always comes with two arguments, because such a constraint defines a sub-system which is closed under reduction.</footnote>

<footnote n="2">² Non-head steps are called internal ($\to_\beta$) in [16].</footnote>
**Proof.** We prove the hypotheses of Proposition 4.5.

1. $\underset{\neg h}{\rightarrow} \oplus$ linearly postpones after $\underset{\neg h}{\rightarrow} \oplus$ because lifting the swap in Lemma 5.2.2 via Lemma 4.3.2 (with $\alpha = \gamma := \oplus$) gives $t \underset{\neg h}{\rightarrow} \oplus p \underset{\neg h}{\rightarrow} \oplus q \subseteq t \underset{\neg h}{\rightarrow} \oplus \rightarrow \underset{\neg h}{\oplus} q$. Lemma 3.5.2 gives Factorization.

2. This is exactly Lemma 5.2.1.

3. By definition of substitution $(\oplus p_1 p_2)\{x:=q\} = \oplus (p_1\{x:=q\})(p_2\{x:=q\}) \mapsto \oplus p_i\{x:=q\}$. ▼

# 6 Extensions of the CbV $\lambda$-Calculus: Left and Weak Factorization

Plotkin's call-by-value (CbV) $\lambda$-calculus [44] is the restriction of the $\lambda$-calculus where $\beta$-redexes can be fired only when the argument is a *value*, where values are defined by:

$$ v ::= x \mid a \mid \lambda x.t \quad (\text{values } \mathcal{V}) $$

The CbV $\lambda$-calculus is given by the pair $(\Lambda, \rightarrow_{\beta_v})$, where the reduction step $\rightarrow_{\beta_v}$ is the contextual closure of the following rule $\mapsto_{\beta_v}$: $(\lambda x.t)v \mapsto_{\beta_v} t\{x:=v\}$ where $v$ is a value.

**Left and Weak Reduction.** In the literature on the CbV $\lambda$-calculus, factorization is considered with respect to various essential reductions. Usually, the essential reduction is weak, i.e. it does not act under abstractions. There are three main weak schemes: reducing from left to right, as originally done by Plotkin [44], from right to left, as done for instance by Leroy's ZINC abstract machine [33], or in an unspecified non-deterministic order, used for example in [31].

Here we focus on the left(-to-right) and the (unspecified) weak schemes. Left contexts L and weak contexts W are respectively defined by

$$ L ::= \langle \rangle \mid Lt \mid vL \quad W ::= \langle \rangle \mid Wt \mid tW $$

Given a rule $\mapsto_{\gamma}$, a *left step* $\underset{L}{\rightarrow} \gamma$ (resp., a *weak step* $\underset{W}{\rightarrow} \gamma$) is its closure by left (resp. weak) context. A *non-left step* $\underset{W}{\rightarrow} \gamma$ (resp. *non-weak step* $\underset{L}{\rightarrow} \gamma$) is a step obtained as the closure by a context which is not left (resp. not weak).

**Left/Weak Factorization, Modularly.** For both left and weak reductions, we derive a test for modular factorization along the same lines as the test for head factorization (Proposition 4.5). Note that we already know that $(\Lambda, \rightarrow_{\beta_v})$ satisfies left and weak factorization; the former was proved by Plotkin [44], the latter is folklore—a proof can be found in our previous work [3].

**► Proposition 6.1 (A test for modular left/weak factorization).** Let $\rightarrow_{\beta_v}$ be $\beta_v$-reduction, $\rightarrow_{\gamma}$ the contextual closure of a rule $\mapsto_{\gamma}$, and $e \in \{\text{l}, \text{w}\}$. Their union $\rightarrow_{\beta_v} \cup \rightarrow_{\gamma}$ satisfies e-factorization if:

1. e-factorization of $\rightarrow_{\gamma}: \text{Fact}(\underset{e}{\rightarrow} \gamma, \underset{e}{\rightarrow} \gamma)$.

2. Root linear swap: $\underset{e}{\rightarrow} \beta_v \cdot \mapsto_{\gamma} \subseteq \underset{e}{\rightarrow} \gamma \cdot \rightarrow_{\beta_v}^*$.

3. Substitutivity: $\mapsto_{\gamma}$ is substitutive.

The easy proof is in Appendix A.2.

# 7 The Shuffling Calculus

Plotkin's CbV $\lambda$-calculus is usually considered on closed terms. When dealing with open terms, it is well known that a mismatch between the operational and the denotational
semantics arises, as first pointed out by Paolini and Ronchi della Rocca [43, 42, 47]. The literature contains several proposals of extensions of $\beta_v$ reduction to overcome this issue, see Accattoli and Guerrieri for discussions [4]. One such refinement is Carraro and Guerrieri's *shuffling calculus* [14], which extends Plotkin's $\lambda$-calculus with extra rules (without adding new operators). These rules are inspired by linear logic proof nets, and are the CbV analogous of Regnier's $\sigma$ rules [45]. Left factorization for the shuffling calculus is studied by Guerrieri, Paolini, and Ronchi della Rocca in [23], by adapting Takahashi's technique [51].

We recall the calculus, then use our technique to give a new proof of factorization, both left (as in [23]) and weak (new). Remarkably, our proofs are *very short*, whereas the original requires several pages (to define parallel reductions and prove their properties).

**The Syntax.** The shuffling calculus is simply Plotkin's calculus extended with $\sigma$-reduction
$\rightarrow_{\sigma}$, that is, the contextual closure of the root relation $\mapsto_{\sigma} = \mapsto_{\sigma_1} \cup \mapsto_{\sigma_3}$, where

$$ (\lambda x.t)us \mapsto_{\sigma_1} (\lambda x.ts)u \quad \text{if } x \notin \mathrm{fv}(s) \qquad v((\lambda x.t)u) \mapsto_{\sigma_3} (\lambda x.vt)u \quad \text{if } x \notin \mathrm{fv}(v) $$

We write $\rightarrow_{\sigma_i}$ for the contextual closure of $\mapsto_{\sigma_i}$ (so $\rightarrow_{\sigma} = \rightarrow_{\sigma_1} \cup \rightarrow_{\sigma_3}$), and $\rightarrow_{\mathrm{sh}} = \rightarrow_{\beta_v} \cup \rightarrow_{\sigma}$.

**Subtleties.** From a rewriting perspective, the shuffling calculus is an interesting extension of the $\lambda$-calculus because its intricate rules do not fit into easy to manage classes of rewriting systems. Orthogonal systems have only simple forms of overlaps of redexes. While the $\lambda$-calculus is an orthogonal system, the $\sigma$-rules introduce non-trivial overlaps such as the following ones. Setting $I := \lambda x.x$ and $\delta := \lambda x.xx$, the term $\delta I \delta$ is a $\sigma_1$-redex and contains the $\beta_v$-redex $\delta I$; the term $\delta(I\delta)(xI)$ is a $\sigma_1$-redex and contains the $\sigma_3$-redex $\delta(I\delta)$, which contains in turn the $\beta_v$-redex $I\delta$.

**Left and Weak Factorization.** Despite all these traits, the shuffling calculus has good properties, such as confluence [14], and left factorization [23]. Moreover, $\rightarrow_{\sigma}$ is terminating [14]. The tests developed in the previous section allow us to easily prove both left and weak factorization. We check the hypotheses of Proposition 6.1; all the ingredients we need are in Lemma 7.1 (the easy details are in Appendix A.3). Note that the empty context is both a left and a weak context, hence $t \mapsto_{\sigma_i} u$ implies both $t \underset{I}{\rightarrow} \sigma_i u$ and $t \underset{W}{\rightarrow} \sigma_i u$.

**► Lemma 7.1 (Root linear swaps).** Let $e \in \{l, w\}$ and $i \in \{1, 3\}$. Then:

1. $\neg \vec{e} \beta_v \cdot \mapsto_{\sigma_i} \subseteq \mapsto_{\sigma_i} \cdot \rightarrow_{\beta_v}$.

2. $\neg \vec{e} \sigma \cdot \mapsto_{\sigma_i} \subseteq \mapsto_{\sigma_i} \cdot \rightarrow_{\sigma}$.

**► Theorem 7.2 (Testing left (weak) factorization).** Let $e \in \{l, w\}$. Fact($\neg \vec{e} \mathrm{sh}$, $\neg \vec{e} \mathrm{sh}$) holds, as:

1. Left (resp. weak) factorization of $\rightarrow_{\sigma}: \mathrm{Fact}(\neg \vec{e} \sigma, \neg \vec{e} \sigma)$.

2. Root linear swap: $\neg \vec{e} \beta_v \cdot \mapsto_{\sigma} \subseteq \neg \vec{e} \sigma \cdot \rightarrow_{\beta_v}$.

3. Substitutivity: $\mapsto_{\sigma_i}$ is substitutive, for $i \in \{1, 3\}$.

**Proof.** We prove the hypotheses of Proposition 6.1:

1. Left (resp. weak) factorization of $\rightarrow_{\sigma}$ holds because $\neg \vec{e} \sigma$ linearly postpones after $\neg \vec{e} \sigma$: indeed, by Lemma 7.1.2 $\neg \vec{e} \sigma \cdot \mapsto_{\sigma} \subseteq \neg \vec{e} \sigma \cdot \rightarrow_{\sigma}$ and by contextual closure (Lemma A.3 with $\alpha = \gamma = \sigma$) we have that $\neg \vec{e} \sigma \cdot \neg \vec{e} \sigma \subseteq \neg \vec{e} \sigma \cdot \rightarrow_{\sigma}$. We conclude by Lemma 3.5.2.

2. This is Lemma 7.1.1.

3. By definition of substitution. The immediate proof is in Appendix A.3.

◄
## 8 Non-Terminating Relations

In this section we provide examples of the fact that our technique does not rest on termination hypotheses. We consider fixpoint operators in both CbN and CbV, which have non-terminating reductions. Obviously, when terms are not restricted by types, the operator is definable, so the example is slight artificial, but we hope clarifying.

There are also cases where the modules are terminating but the compound system is not; the technique, surprisingly, still works. Accattoli gives various examples based on λ-calculi with explicit substitutions in [2]. An insight of this paper—not evident in [2]—is that termination is not needed to lift factorization from the modules to the compound system.

**CbN Fixpoint, Head Factorization.** We first consider the calculus $\beta Y := (\Lambda, \rightarrow_{\beta} \cup \rightarrow_{Y})$ which is defined by Hindley [24]<fnref n="3" />. The reduction $\rightarrow_{Y}$ is the contextual closure of the root relation $Yp \mapsto_{Y} p(Yp)$. Points 1-3 below are all easily established—details in Appendix A.4.

**► Proposition 8.1 (Testing head factorization for $\beta Y$).** $\rightarrow_{\beta} \cup \rightarrow_{Y}$ satisfies head factorization:
1. Head factorization of $\rightarrow_{Y}: \text{Fact}(\underset{h}{\rightarrow} \gamma, \underset{h}{\rightarrow} \gamma)$.
2. Root linear swap: $\underset{h}{\rightarrow} \beta \cdot \mapsto_{Y} \subseteq \underset{h}{\rightarrow} Y \cdot \underset{h}{\rightarrow}^{*} \beta$.
3. Substitutivity: $\mapsto_{Y}$ is substitutive.

**CbV Fixpoint, Weak Factorization.** We now consider weak factorization and a CbV counterpart of the previous example. We follow Abramsky and McCusker [1], who study a call-by-value PCF with a fixpoint operator $Z$. Similarly, we extend the CbV $\lambda$-calculus with their reduction $\rightarrow_Z$, which is the contextual closure of rule $Zv \mapsto_Z \lambda x.v(Zv)x$ where $v$ is a value. The calculus $\beta_v Z$ is therefore $(\Lambda, \rightarrow_{\beta_v} \cup \rightarrow_Z)$. Points 1-3 below are all immediate—details in Appendix A.4.

**► Proposition 8.2 (Testing weak factorization for $\beta_v Z$).** $\rightarrow_{\beta} \cup \rightarrow_Z$ satisfies weak factorization:
1. Weak factorization of $\rightarrow_Z$: $\text{Fact}(\underset{w}{\rightarrow} Z, \underset{w}{\rightarrow} Z)$.
2. Root linear swap: $\underset{w}{\rightarrow} \beta_v \cdot \mapsto_Z \subseteq \underset{w}{\rightarrow} Z \cdot \underset{w}{\rightarrow}^{*} \beta_v$.
3. Substitutivity: $\mapsto_Z$ is substitutive.

## 9 Further Applications: Probabilistic Calculi

In this paper, we present our technique using examples which are within the familiar language of $\lambda$-calculus. However the core of the technique—Theorem 3.4—is independent from a specific syntax. It can be used in calculi whose objects are richer than $\lambda$-terms. The probabilistic $\lambda$-calculus is a prime example.

A recent line of research [19, 34] is developing probabilistic calculi where evaluation is not limited to a deterministic strategy. Faggian and Ronchi della Rocca [19] define two calculi—$\Lambda_{\oplus}^{cbv}$ and $\Lambda_{\oplus}^{cbn}$—which model respectively CbV and CbN probabilistic higher-order computation, while being conservative extensions of the CbV and CbN $\lambda$-calculus. For both calculi confluence and factorization (called *standardization* in [19]) hold. There is however a deep asymmetry between the two results. *Confluence* is neatly proved via Hindley-Rosen

<footnote n="3">³ Head factorization of $\beta Y$ is easily obtained by a high-level argument, as consequence of left-normality, see Terese [52], Ch. 8.5. The point that we want to stress here is that the validity of *linear swaps* is not limited to *terminating* reduction, and $\beta Y$ provides a simple, familiar example.</footnote>
technique, by relying on the fact the $\beta$ (resp. $\beta_v$) reduction is confluent. The proof of *factorization* is instead laborious: the authors define a notion of parallel reduction for the new calculus, and then adapt Takahashi's technique [51]. Leventis work [34] on call-by-name probabilistic $\lambda$-calculus suffers a similar problem; he proves factorization by relying on the finite developments method, but the proof is equally laborious.

Our technique allows for a *neat, concise proof of factorization*, which reduces to only testing a single linear swap, with no need of parallel reductions or finite developments. To prove factorization turns out to be in fact *easier* than proving confluence. The technical details—that is, the definition of the calculus and the proof—are in Appendix B.

**10 Conclusions and Discussions**

**Summary.** A well-established approach to model higher-order computation with advanced features, is starting from the call-by-name or call-by-value $\lambda$-calculus, and enrich it with new constructs. We propose a sharp technique to establish factorization of a compound system from factorization of its components. As we point out, the natural transposition of Hindley-Rosen technique for confluence does not work here, because the obtained conditions are—in general—not validated by extensions of the $\lambda$-calculus. The turning point is the identification of an alternative sufficient condition, called linear swap. Moreover, on common factorization schemes such as head or weak factorization, our technique reduces to a straightforward test. Concretely, we apply our technique to various examples, stressing its independence from common simplifying hypotheses such as confluence, orthogonality, and termination.

**Black Box and Elementary Commutations.** A key feature of our technique is to take factorization of the core relations—the modules—as *black boxes*. The focus is then on the analysis of the *interaction* between the modules. The benefit is both practical and conceptual: we disentangle the components—and the issues—under study. This is especially appealing when dealing with extensions of the $\lambda$-calculus, built on top of $\beta$ or $\beta_v$ reduction, because often most of the difficulties come from the higher-order component, that is, $\beta$ or $\beta_v$ itself—whose factorization is non-trivial to prove but known to hold—rather than from the added features.

Good illustrations of these points are our proofs of factorization. We stress that:

- the proof of factorization of the compound system is independent from the specific technique (finite developments, parallel reduction, etc.) used to prove factorization of the modules.

- to verify good interaction between the modules, it often suffices to check *elementary, local commutations*—the linear swaps.

These features provide a neat proof-technique *supporting the development and the analysis* of complex compound systems.

**Conclusions.** When one wants to model new computational features, the calculus is often not given, but it has to be designed, in such a way that it satisfies confluence and factorization. The process of *developing* the calculus and the process of *proving* its good properties, go hand in hand. If the latter is difficult and prone to errors, the former also is. The black-box approach makes our technique efficient and accessible also to working scientists who are not specialists in rewriting. And even for the $\lambda$-calculus expert who masters tools such as finite developments, labeling or parallel reduction, it still appears desirable to limit the amount of difficulties. The more advanced and complex are the computational systems we study, the more crucial it is to have reasoning tools as simple to use as possible.
References

1 Samson Abramsky and Guy McCusker. Call-by-value games. In *Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers*, pages 1-17, 1997. doi:10.1007/BFb0028004.

2 Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In *23rd International Conference on Rewriting Techniques and Applications, RTA 2012*, volume 15 of LIPIcs, pages 6-21, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.6.

3 Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorization and normalization, essentially. In Anthony Widjaja Lin, editor, *Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings*, volume 11893 of *Lecture Notes in Computer Science*, pages 159-180. Springer, 2019. doi:10.1007/978-3-030-34175-6\_9.

4 Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Atsushi Igarashi, editor, *Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings*, volume 10017 of *Lecture Notes in Computer Science*, pages 206-226, 2016. doi:10.1007/978-3-319-47958-3\_12.

5 Yohji Akama. On mints' reduction for ccc-calculus. In *Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings*, pages 1-12, 1993. doi:10.1007/BFb0037094.

6 Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In Ron K. Cytron and Peter Lee, editors, *Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995*, pages 233-246. ACM Press, 1995. doi:10.1145/199448.199507.

7 Pablo Arrighi and Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. *Log. Methods Comput. Sci.*, 13(1), 2017. doi:10.23638/LMCS-13(1:8)2017.

8 Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. In *Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings*, pages 132-148, 2018. doi:10.1007/978-3-319-90686-7\_9.

9 Franz Baader and Tobias Nipkow. *Term rewriting and all that*. Cambridge University Press, 1998.

10 Leo Bachmair and Nachum Dershowitz. Commutation, transformation, and termination. In *8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings*, pages 5-20, 1986. doi:10.1007/3-540-16780-3\_76.

11 Hendrik Pieter Barendregt. *The Lambda Calculus – Its Syntax and Semantics*, volume 103 of *Studies in logic and the foundations of mathematics*. North-Holland, 1984.

12 Frédéric Blanqui. Size-based termination of higher-order rewriting. *J. Funct. Program.*, 28:e11, 2018. doi:10.1017/S0956796818000072.

13 Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability = typability + inhabitation. *CoRR*, 2018. URL: http://arxiv.org/abs/1812.06009.

14 Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In *Foundations of Software Science and Computation Structures, 17th International Conference, FoSSaCS 2014*, volume 8412 of *Lecture Notes in Computer Science*, pages 103-118, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7\_7.

15 H.B. Curry and R. Feys. *Combinatory Logic*. Number v. 1 in Combinatory Logic. North-Holland Publishing Company, 1958.

16 Ugo de' Liguoro and Adolfo Piperno. Non deterministic extensions of untyped lambda-calculus. *Inf. Comput.*, 122(2):149-177, 1995. URL: https://doi.org/10.1006/inco.1995.1145.

17 Nachum Dershowitz. On lazy commutation. In *Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday*, pages 59-82, 2009. doi:10.1007/978-3-642-01748-3\_5.
18 Henk Doornbos and Burghard von Karger. On the union of well-founded relations. Logic Journal of the IGPL, 6(2):195-201, 1998. doi:10.1093/jigpal/6.2.195.

19 Claudia Faggian and Simona Ronchi Della Rocca. Lambda calculus and probabilistic computation. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13, 2019. doi:10.1109/LICS.2019.8785699.

20 Alfons Geser. Relative Termination. PhD thesis, University of Passau, Germany, 1990. URL: http://vts.uni-ulm.de/docs/2012/8146/vts_8146_11884.pdf.

21 Georges Gonthier, Jean-Jacques Lévy, and Paul-André Melliès. An abstract standardisation theorem. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22-25, 1992, pages 72-81, 1992. doi:10.1109/LICS.1992.185521.

22 Bernhard Gramlich. Modularity in term rewriting revisited. Theor. Comput. Sci., 464:3-19, 2012. doi:10.1016/j.tcs.2012.09.008.

23 Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods in Computer Science, 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:29)2017.

24 J. Roger Hindley. Reductions of residuals are finite. Transactions of the American Mathematical Society, 240:345-361, 1978.

25 J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, New York, NY, USA, 2 edition, 2008.

26 J.R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne, 1964.

27 Nao Hirokawa, Aart Middeldorp, and Georg Moser. Leftmost outermost revisited. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015, volume 36 of LIPIcs, pages 209-222, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.209.

28 Katsumasa Ishii. A proof of the leftmost reduction theorem for λβη-calculus. Theor. Comput. Sci., 747:26-32, 2018. URL: https://doi.org/10.1016/j.tcs.2018.06.003.

29 Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, Mathematisch Centrum, Amsterdam, 1980.

30 Masahito Kurihara and Ikuo Kaji. Modular term rewriting systems and the termination. Inf. Process. Lett., 34(1):1-4, 1990. doi:10.1016/0020-0190(90)90221-I.

31 Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008.

32 Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Informatics Appl., 46(3):413-450, 2012. doi:10.1051/ita/2012012.

33 Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. URL: http://gallium.inria.fr/~xleroy/publi/ZINC.pdf.

34 Thomas Leventis. A deterministic rewrite system for the probabilistic λ-calculus. Math. Struct. Comput. Sci., 29(10):1479-1512, 2019. doi:10.1017/S0960129519000045.

35 Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda calcul. PhD thesis, University of Paris 7, 1978.

36 Paul-André Melliès. Typed lambda-calculi with explicit substitutions may not terminate. In Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin, editors, Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings, volume 902 of Lecture Notes in Computer Science, pages 328-334. Springer, 1995. doi:10.1007/BFb0014062.

37 Paul-André Melliès. A factorisation theorem in rewriting theory. In Category Theory and Computer Science, 7th International Conference, CTCS '97, volume 1290 of Lecture Notes in Computer Science, pages 49-68, 1997. URL: https://doi.org/10.1007/BFb0026981.

38 Aart Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Rewriting Techniques and Applications, 3rd International Conference, RTA-89,
Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings, pages 263-277, 1989. doi: 10.1007/3-540-51081-8\_113.

39 Aart Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 396-401, 1989. doi:10.1109/LICS.1989.39194.

40 Aart Middeldorp. Confluence of the disjoint union of conditional term rewriting systems. In Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, pages 295-306, 1990. doi:10.1007/3-540-54317-1\_99.

41 Gerd Mitschke. The standardization theorem for λ-calculus. Mathematical Logic Quarterly, 25(1-2):29-31, 1979. URL: https://doi.org/10.1002/malq.19790250104.

42 Luca Paolini. Call-by-value separability and computability. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, Torino, Italy, October 4-6, 2001, Proceedings, volume 2202 of Lecture Notes in Computer Science, pages 74-89. Springer, 2001. doi:10.1007/3-540-45446-2\_5.

43 Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO Theor. Informatics Appl., 33(6):507-534, 1999. doi:10.1051/ita:1999130.

44 Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. doi:10.1016/0304-3975(75)90017-1.

45 Laurent Regnier. Une équivalence sur les lambda-termes. Theor. Comput. Sci., 126(2):281-292, 1994. doi:10.1016/0304-3975(94)90012-4.

46 György E. Révész. A list-oriented extension of the lambda-calculus satisfying the church-rosser theorem. Theor. Comput. Sci., 93(1):75-89, 1992. doi:10.1016/0304-3975(92)90212-X.

47 Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-10394-4.

48 J. B. Rosser. A mathematical logic without variables. Duke Math. J., 1(3):328-355, 09 1935. doi:10.1215/S0012-7094-35-00123-5.

49 Michaël Rusinowitch. On termination of the direct sum of term-rewriting systems. Inf. Process. Lett., 26(2):65-70, 1987. doi:10.1016/0020-0190(87)90039-1.

50 Alexis Saurin. On the relations between the syntactic theories of lambda-mu-calculi. In Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, pages 154-168, 2008. doi:10.1007/978-3-540-87531-4\_13.

51 Masako Takahashi. Parallel reductions in lambda-calculus. Inf. Comput., 118(1):120-127, 1995. doi:10.1006/inco.1995.1057.

52 Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

53 Yoshihito Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett., 25(3):141-143, 1987. doi:10.1016/0020-0190(87)90122-0.

54 Yoshihito Toyama. On the church-rosser property for the direct sum of term rewriting systems. J. ACM, 34(1):128-143, 1987. doi:10.1145/7531.7534.

55 Yoshihito Toyama, Jan Willem Klop, and Hendrik Pieter Barendregt. Termination for the direct sum of left-linear term rewriting systems -preliminary draft-. In Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings, pages 477-491, 1989. doi:10.1007/3-540-51081-8\_127.

56 Vincent Van Oostrom. Some symmetries of commutation diamonds. Talk at the International Workshop on Confluence, 30 June 2020.

57 Vincent van Oostrom. Confluence by decreasing diagrams. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg,
Austria, July 15-17, 2008, *Proceedings*, volume 5117 of *Lecture Notes in Computer Science*, pages 306-320. Springer, 2008. doi:10.1007/978-3-540-70590-1\_21.

58 Vincent van Oostrom and Yoshihito Toyama. Normalisation by random descent. In Delia Kesner and Brigitte Pientka, editors, *1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal*, volume 52 of LIPIcs, pages 32:1-32:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. doi: 10.4230/LIPIcs.FSCD.2016.32.

59 Vincent van Oostrom and Hans Zantema. Triangulation in rewriting. In *23rd International Conference on Rewriting Techniques and Applications (RTA'12)*, RTA 2012, May 28 - June 2, 2012, *Nagoya, Japan*, pages 240-255, 2012. doi:10.4230/LIPIcs.RTA.2012.240.
# APPENDIX

Appendix A collects omitted details of proofs. In Appendix B we illustrate a more advanced *example* of application of our technique, namely to the *probabilistic λ-calculus*.

## A Appendix: Omitted Proofs

### A.1 Head Factorization (Sect. 4)

**Consequences of Property 4.2.** Note that the empty context `()` is a head context. Hence for non-head steps if $C\langle r \rangle \underset{-h}{\rightarrow} C\langle r' \rangle$ necessarily $C \neq \langle \rangle$, and Property 4.2 always applies. The following key property holds.

**► Property A.1 (Shape Preservation).** By Property 4.2, $\underset{-h}{\rightarrow}\gamma$ preserves the shapes of terms:

1. Atoms: there is no $t$ such that $t \underset{-h}{\rightarrow}\gamma a$, for any variable or constant $a$.

2. $t \underset{-h}{\rightarrow}\gamma \lambda x.u_1$ implies $t = \lambda x.t_1$ and $t_1 \underset{-h}{\rightarrow}\gamma u_1$.

3. $t \underset{-h}{\rightarrow}\gamma u_1 u_2$ implies $t = t_1 t_2$, with $t_1 \underset{-h}{\rightarrow}\gamma u_1$ (and $t_2 = u_2$), or $t_2 \rightarrow\gamma u_2$ (and $t_1 = u_1$).

4. Redex: if $t \underset{-h}{\rightarrow}\gamma u$, and $u$ is a $\beta$-redex, then $t$ is a $\beta$-redex.

Similarly, if $t \underset{-h}{\rightarrow}\gamma u$ and $u$ has shape $Kt_1...t_k$ ($K$ a constant), $t$ has the same shape.

Point 4. follows from points 1. to 3. Note that, in particular, if $u$ is a $\oplus$-redex, so is $t$.

**Head Factorization, Modularly.**

**► Lemma (4.3, Lifting root linear swaps).** Let $\mapsto_{\alpha}, \mapsto_{\gamma}$ be root relations on $\Lambda$.

1. $\underset{-h}{\rightarrow}\alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\rightarrow}\gamma \cdot \rightarrow_{\alpha}^{*}$ implies $\text{1Swap}(\underset{-h}{\rightarrow}\alpha, \underset{-h}{\rightarrow}\gamma)$.

2. Similarly, $\underset{-h}{\rightarrow}\alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\rightarrow}\gamma \cdot \rightarrow_{\alpha}^{=}$ implies $\underset{-h}{\rightarrow}\alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\rightarrow}\gamma \cdot \rightarrow_{\alpha}^{=}$.

**Proof.** (1). We prove that $\underset{-h}{\rightarrow}\alpha \cdot \mapsto_{\gamma} \subseteq \underset{-h}{\rightarrow}\gamma \cdot \rightarrow_{\alpha}^{*}$ implies $t \underset{-h}{\rightarrow}\alpha u \underset{-h}{\rightarrow}\gamma s \subseteq t \underset{-h}{\rightarrow}\gamma \cdot \rightarrow_{\alpha}^{*} s$, by induction on the head context $H = \lambda x_1 \dots \lambda x_k \langle \rangle t_1 \dots t_n$ of the reduction $u \underset{-h}{\rightarrow}\gamma s$.

A. $u$ is the $\gamma$-redex (i.e. $H = \langle \rangle$, $k = 0$, $n = 0$). The claim holds by assumption.

B. $u = \lambda x.u_1$ (i.e., $k > 0$). Immediate by shape preservation (Property A.1.2) and the i.h.,

C. $u = u_1 u_2$ (i.e., $k = 0$, $n > 0$). Then $u_1 \underset{-h}{\rightarrow}\gamma u_1'$ and $u_1 u_2 \underset{-h}{\rightarrow}\gamma u_1' u_2 = s$. By shape preservation (Property A.1.3), there are two cases.

Case (i): $t := t_1 u_2$. By i.h., $t_1 \underset{-h}{\rightarrow}\gamma t_1'$ and $t_1' \rightarrow_{\alpha}^{*} u_1'$. Hence, $t_1 u_2 \underset{-h}{\rightarrow}\gamma t_1' u_2 \rightarrow_{\alpha}^{*} u_1' u_2 = s$.

Case (ii): $t := u_1 t_2$. Immediate, because $t = u_1 t_2 \underset{-h}{\rightarrow}\gamma u_1' t_2 \rightarrow_{\alpha} u_1' u_2$.

(2). The proof is similar. The only minimal difference is case (ii) in point (C). ◀

**► Lemma (4.4, Swap with $\underset{-h}{\rightarrow}\beta$).** If $\mapsto_{\gamma}$ is substitutive then $\text{1Swap}(\underset{-h}{\rightarrow}\gamma, \underset{-h}{\rightarrow}\beta)$ holds.

**Proof.** First, note that by Property 4.1, we have that $\rightarrow_{\gamma}$ is substitutive. We prove $(t \underset{-h}{\rightarrow}\gamma u \underset{-h}{\rightarrow}\beta s)$ implies $t \underset{-h}{\rightarrow}\beta \cdot \rightarrow_{\gamma}^{*} s)$ by using Lemma 4.3.

Let $u = (\lambda x.u_1)u_2 \mapsto_{\beta} u_1\{x:=u_2\}$. By Property A.1, either (i) $t = (\lambda x.p)u_2$ and $p \underset{-h}{\rightarrow}\gamma u_1$ or (ii) $t = (\lambda x.u_1)q$ and $q \rightarrow_{\gamma} u_2$. Case (i): $(\lambda x.p)u_2 \underset{-h}{\rightarrow}\beta p\{x:=u_2\}$. By Property 4.1 (point 1) $p\{x:=u_2\} \rightarrow_{\gamma} u_1\{x:=u_2\}$. Case (ii): $(\lambda x.u_1)q \underset{-h}{\rightarrow}\beta u_1\{x:=q\}$. By using Property 4.1(point 2), $u_1\{x:=q\} \rightarrow_{\gamma}^{*} u_1\{x:=u_2\}$. ◀
## A.2 Call-by-Value λ-Calculus (Sect. 6)

**Consequences of Property 4.2.** The empty context `()` is both a left and a weak context. Hence Property 4.2 always applies to non-left and non-weak steps. Consequently:

**► Property A.2 (Shape Preservation).** Fixed $e \in \{\mathbf{l}, \mathbf{w}\}$, $\overleftarrow{\mathbf{e}} \gamma$ preserves the shape of terms:

1. Atoms: there is no $t$ such that $t \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} a$, for any variable or constant $a$;

2. Abstraction: $t \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} \lambda x.u_1$ implies $t = \lambda x.t_1$ and $t_1 \to_{\gamma} u_1$;

3. Application: $t \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} u_1 u_2$ implies $t = t_1 t_2$, with either (i) $t_1 \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} u_1$ and $t_2 = u_2$, or (ii) $t_2 \to_{\gamma} u_2$ and $t_1 = u_1$. Moreover, in case (ii): if $vt_2 \to_{\mathbf{l}} vu_2$ (v a value), then $t_2 \to_{\mathbf{l}} u_2$; if $t_1 t_2 \to_{\mathbf{w}} u_1 u_2$, then $t_2 \to_{\mathbf{w}} u_2$ (always).

4. Redex: if $t \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} u$, and $u$ is a $\beta_v$-redex, then $t$ also is (as a consequence of points 1. to 3.)

**Left and Weak Factorization, Modularly.** To prove Proposition 6.1 we proceed similarly to Sect. 4.2.

**► Lemma A.3 (Root linear swaps).** Let $\mapsto_{\alpha}, \mapsto_{\gamma}$ be root relations on $\Lambda$.

i. If $t \xrightarrow{\overleftarrow{\mathbf{l}} \alpha} u \mapsto_{\gamma} s \subseteq t \xrightarrow{\mathbf{l}} \gamma \cdot \to_{\alpha}^{*} s$ then $\text{1Swap}(\xrightarrow{\overleftarrow{\mathbf{l}} \alpha}, \xrightarrow{\mathbf{l}} \gamma)$.

ii. If $t \xrightarrow{\overleftarrow{\mathbf{w}} \alpha} u \mapsto_{\gamma} s \subseteq t \xrightarrow{\mathbf{w}} \gamma \cdot \to_{\alpha}^{*} s$ then $\text{1Swap}(\xrightarrow{\overleftarrow{\mathbf{w}} \alpha}, \xrightarrow{\mathbf{l}} \gamma)$.

Similarly $\xrightarrow{\overleftarrow{\mathbf{e}} \alpha} \mapsto_{\gamma} \subseteq \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} \to_{\alpha}^{\equiv}$ implies $\xrightarrow{\overleftarrow{\mathbf{e}} \alpha} \to_{\gamma} \subseteq \xrightarrow{\overleftarrow{\mathbf{e}} \gamma} \to_{\alpha}^{\equiv}$, with $e \in \{\mathbf{l}, \mathbf{w}\}$

**Proof.** (i.) We prove that $t \xrightarrow{\overleftarrow{\mathbf{l}} \alpha} u \xrightarrow{\mathbf{l}} \gamma \subseteq t \xrightarrow{\mathbf{l}} \gamma \cdot \to_{\alpha}^{*} s$, by induction on the context $\mathbf{L}$ of $u$.

1. $\mathbf{L} = \langle\rangle$, i.e. $u \mapsto_{\gamma} s$. The claim holds by hypothesis.

2. $\mathbf{L} = \mathbf{Lu}_2$, i.e. $u = u_1 u_2 \xrightarrow{\mathbf{l}} \gamma s_1 u_2 = s$ with $u_1 \xrightarrow{\mathbf{l}} \gamma s_1$. By Property A.2.3 $t = t_1 t_2$ and

a. either $t_1 \xrightarrow{\overleftarrow{\mathbf{l}} \alpha} u_1$ (and $t_2 = u_2$); then, by i.h., $t_1 \xrightarrow{\mathbf{l}} \gamma \cdot \to_{\alpha}^{*} s_1$, so $t = t_1 u_2 \xrightarrow{\mathbf{l}} \gamma \cdot \to_{\alpha}^{*} s_1 u_2$;

b. or $t_2 \xrightarrow{\alpha} u_2$ (and $t_1 = u_1$), so $t = u_1 t_2 \xrightarrow{\mathbf{l}} \gamma s_1 t_2 \to_{\alpha} s_1 u_2$.

3. $\mathbf{L} = \mathbf{vL}$, i.e. $u = v u_2 \xrightarrow{\mathbf{l}} \gamma v s_2 = s$ with $u_2 \xrightarrow{\mathbf{l}} \gamma s_2$. Then $t = t_1 t_2$ and by Property A.2.3

a. either $t_1 \xrightarrow{\overleftarrow{\mathbf{l}} \alpha} v$ (and $t_2 = u_2$). Since $v$ is a value, by Property A.2.1-2, $t_1$ is also a value and so $t = t_1 u_2 \xrightarrow{\mathbf{l}} \gamma t_1 s_2 \to_{\alpha} v s_2$.

b. or $t_2 \xrightarrow{\overleftarrow{\mathbf{l}} \alpha} u_2$ ($t_1 = v$). By i.h., $t_2 \xrightarrow{\mathbf{l}} \gamma \cdot \to_{\alpha}^{*} s_2$, so $vt_2 \xrightarrow{\mathbf{l}} \gamma \cdot \to_{\alpha}^{*} v s_2$;

(ii.) The proof of (ii.) is similar, but simpler. Case $\mathbf{W} = \langle\rangle$ is the same. Case $\mathbf{Wu}_2$ is exactly like $\mathbf{Lu}_2$, and case $u_1 \mathbf{W}$ is symmetric to case (2).

The proof of the last claim is similar.

**► Lemma A.4 (Swap with $\xrightarrow{\overleftarrow{\mathbf{e}} \beta_v}$).** If $\mapsto_{\gamma}$ is substitutive then $\text{1Swap}(\xrightarrow{\overleftarrow{\mathbf{e}} \gamma}, \xrightarrow{\overleftarrow{\mathbf{e}} \beta_v})$, for $e \in \{\mathbf{l}, \mathbf{w}\}$.

**Proof.** We prove $\text{1Swap}(\xrightarrow{\overleftarrow{\mathbf{l}} \gamma}, \xrightarrow{\mathbf{l}} \beta_v)$, the other swap is similar. By Lemma A.3, it is enough to prove that $t \xrightarrow{\overleftarrow{\mathbf{l}} \gamma} u \mapsto_{\beta_v} s$ implies $t \xrightarrow{\mathbf{l}} \beta_v \cdot \to_{\gamma}^{*} s$. We use Property 4.1 (substitutivity). Let $u = (\lambda x.u_1)v \mapsto_{\beta_v} u_1\{x:=v\} = s$. By Property A.2 (3. and 4.) we have:

1. either $t = (\lambda x.t_1)v$ and $t_1 \to_{\gamma} u_1$; thus, $t = (\lambda x.t_1)v \xrightarrow{\mathbf{l}} \beta_v$ $t_1\{x:=v\} \to_{\gamma} u_1\{x:=v\} = s$, where the $\to_{\gamma}$ step takes place by Property 4.1.1 since $\to_{\gamma}$ is substitutive.

2. or $t = (\lambda x.u_1)w$ where $w \to_{\gamma} v$ and $w$ is a value; hence, $t = (\lambda x.u_1)w \xrightarrow{\mathbf{l}} \beta_v$ $u_1\{x:=w\} \to_{\gamma}^{*} u_1\{x:=v\}$, where the $\to_{\gamma}$ steps take place by Property 4.1.2. ◀
1. Weak factorization of $\rightarrow_Z$: $\text{Fact}(\underset{\rightarrow}{w}z, \underset{\leftarrow}{w}z)$.

2. Root linear swap: $\underset{\rightarrow}{w}\beta_v \cdot \mapsto Z \subseteq \underset{\rightarrow}{w}Z \cdot \underset{\leftarrow}{w}^*\beta_v$.

3. Substitutivity: $\mapsto_Z$ is substitutive.

**Proof.** We prove the hypotheses of Proposition 4.5:

1. It is easy to verify that $\underset{\rightarrow}{w}Z \cdot \underset{\leftarrow}{w}Z \subseteq \underset{\rightarrow}{w}Z \cdot \underset{\leftarrow}{w}^*Z$. Then apply Lemma 3.5.1.

2. Assume $t \underset{\rightarrow}{w}\beta_v Zv \mapsto_Z \lambda x.v(Zv)x$. By Property 4.2 (as spelled-out in Property A.2), if $t \underset{\rightarrow}{w}\beta_v Zv$ then $t = Zw$ and $w \rightarrow \beta_v v$. So, $t = Zw \underset{\rightarrow}{w}Z \lambda x.v(Zw)x \rightarrow_{\beta_v}^* \lambda x.v(Zv)x$.

3. Simply $(Zv)\{x:=q\} = Z(v\{x:=q\}) \mapsto_Z \lambda y.v\{x:=q\}(Z(v\{x:=q\})y = (\lambda y.v(Zv)y)\{x:=q\})$.

<figure><img src="image_4.png" /></figure>

## B Appendix: Factorizing Factorization in Probabilistic $\lambda$-calculus

Faggian and Ronchi della Rocca [19] define two calculi—$\Lambda_{\oplus}^{\text{cbn}}$ and $\Lambda_{\oplus}^{\text{cbv}}$—which model respectively CbV and CbN probabilistic higher-order computation, and are conservative extensions of the CbN and CbV $\lambda$-calculi. Here we focus on CbV, which is the most relevant paradigm for calculi with effects, but the same approach applies to CbN.

We first recall the syntax of $\Lambda_{\oplus}^{\text{cbv}}$ (we refer to [19] for background and details), and then give a new proof of weak factorization, using our technique and obtaining a neat, compact proof of factorization, which only requires a few lines.

**Terms.** $\Lambda_{\oplus}^{\text{cbv}}$ is a rewrite system where the objects to be rewritten are not terms, but monadic structures on terms, namely multi-distributions [8]. Intuitively, a multi-distribution represents a probability distribution on the possible reductions from a term. Terms and contexts are the same as for the non-deterministic $\lambda$-calculus, but here we write the $\oplus$ infix, to facilitate reference to [19]. *Terms and values* are generated by the grammars

$$M ::= x \mid \lambda x.M \mid MM \mid M \oplus M \qquad (\text{Terms } \Lambda_{\oplus})$$

$$V ::= x \mid \lambda x.M \qquad (\text{Values } V)$$

where $x$ ranges over a countable set of variables. *Contexts* and *weak contexts* are given by:

$$C ::= \langle \rangle \mid CM \mid MC \mid \lambda x.C \mid C \oplus M \mid M \oplus C \qquad (\text{Contexts})$$

$$W ::= \langle \rangle \mid WM \mid MW \qquad (\text{Weak Contexts})$$

where $\langle \rangle$ denotes the hole of the context.

The intended behaviour of $M \oplus N$ is to reduce to either $M$ or $N$, with equal probability $\frac{1}{2}$. This is formalized by means of *multi-distributions*.

**Multi-distributions.** A *multi-distribution* $\mathfrak{m} = [p_i M_i \mid i \in I]$ is a multiset of pairs of the form $pM$, with $p \in \{0, 1\}$, $M \in \Lambda_{\oplus}$, and $\sum p_i \le 1$. We denote by $\mathcal{M}(\Lambda_{\oplus})$ the set of all multi-distributions. The sum of multi-distributions is denoted by $+$. The product $q \cdot \mathfrak{m}$ of a scalar $q$ and a multi-distribution $\mathfrak{m}$ is defined pointwise $q[p_i M_i]_{i \in I} := [(qp_i)M_i]_{i \in I}$.

**The calculus ($\mathcal{M}(\Lambda_{\oplus}), \Rightarrow$).** The calculus $\Lambda_{\oplus}^{\text{cbv}}$ is the rewrite system ($\mathcal{M}(\Lambda_{\oplus}), \Rightarrow$) where $\mathcal{M}(\Lambda_{\oplus})$ is the set of multi-distributions on $\Lambda_{\oplus}$ and the relation $\Rightarrow \subseteq \mathcal{M}(\Lambda_{\oplus}) \times \mathcal{M}(\Lambda_{\oplus})$ is defined in Fig. 1 and Fig. 2. First, we define one-step reductions from terms to multi-distributions—so for example, $M \oplus N \rightarrow [\frac{1}{2}M, \frac{1}{2}N]$. Then, we lift the definition of reduction to a binary relation on $\mathcal{M}(\Lambda_{\oplus})$, in the natural way—for instance $[\frac{1}{2}(\lambda x.x)z, \frac{1}{2}(M \oplus N)] \Rightarrow [\frac{1}{2}z, \frac{1}{4}M, \frac{1}{4}N]$. Precisely:
$$ C(\langle \lambda x.M \rangle V) \to_{\beta_v} [C(M\{x:=V\})] \quad W\langle M \oplus N \rangle \to_{\oplus} [\frac{1}{2}W(M), \frac{1}{2}W(N)] \quad \begin{aligned} & \to := \to_{\beta_v} \cup \to_{\oplus} \\ & \xrightarrow{\overline{\omega}} := \xrightarrow{\overline{\omega}} \beta_v \cup \to_{\oplus} \end{aligned} $$

Figure 1 Reduction Steps

$$ \begin{array}{ccc} \overline{[M] \Rightarrow_r [M]} & \overline{M \to_r m} & ([M_i] \Rightarrow_r m_i)_{i \in I} \\ [M] \Rightarrow_r m & [M] \Rightarrow_r m & [p_i M_i \mid i \in I] \Rightarrow_r +_{i \in I} p_i \cdot m_i \end{array} $$

Figure 2 Lifting $\to_r$ to $\Rightarrow_r$

1. The reductions $\to_{\beta_v}, \to_{\oplus} \subseteq \Lambda_{\oplus} \times \mathcal{M}(\Lambda_{\oplus})$ are defined in Fig. 1. Observe that the $\oplus$ rule—probabilistic choice—is closed only under weak contexts (no reduction in the body of a function nor in the scope of an operator $\oplus$). Instead, the $\beta_v$ rule is closed under general contexts. Its restriction to closure under weak context is denoted $\xrightarrow{\overline{\omega}} \beta$. The relation $\to$ is the union $\to_{\beta} \cup \to_{\oplus}$, while weak$^4$ reduction $\xrightarrow{\overline{\omega}}$ is the union of the weak reductions $\xrightarrow{\overline{\omega}} \beta_v \cup \to_{\oplus}$. A $\to$-step which is not weak is noted $\xrightarrow{\overline{\omega}}$.

2. The lifting of a relation $\to_r \Lambda_{\oplus} \times \mathcal{M}(\Lambda_{\oplus})$ to a reduction on multi-distribution is defined in Fig. 2. In particular, $\to, \to_{\beta_v}, \to_{\oplus}, \xrightarrow{\overline{\omega}}, \xrightarrow{\overline{\omega}}$ lift to $\Rightarrow, \Rightarrow_{\beta_v}, \Rightarrow_{\oplus}, \xrightarrow{\overline{\omega}}, \xrightarrow{\overline{\omega}}$.

The restriction of $\to_{\oplus}$ to weak contexts is necessary to have confluence, see [19] for a discussion. The fact that reduction $\to_{\beta_v}$ is unrestricted guarantees that the new calculus is a conservative extension of CbV $\lambda$-calculus.

**Factorization, Modularly.** Faggian and Ronchi della Rocca prove—by defining suitable notions of parallel reduction and internal parallel reduction with respect to $\Rightarrow_{\beta_v} \cup \Rightarrow_{\oplus}$—that $\Lambda_{\oplus}^{\text{cbv}}$ satisfies Fact($\xrightarrow{\overline{\omega}}$, $\xrightarrow{\overline{\omega}}$), that is $m \Rightarrow^* n$ implies $m \xrightarrow{\overline{\omega}}^* \cdot \xrightarrow{\overline{\omega}}^* n$.

This result—there called *finitary surface standardization*—is central in [19] because it is the base of the asymptotic constructions which are the core of that paper.

We now give a novel, strikingly short proof of the same result, by using Theorem 3.4. It turns out that we only need to verify the following swap, which is immediate to check.

► **Lemma B.1.** $M \xrightarrow{\overline{\omega}} \beta_v \cdot \to_{\oplus} n$ implies $M \to_{\oplus} \cdot \Rightarrow_{\beta_v} n$.

► **Theorem B.2 (Factorization of $\Rightarrow$).** Let $\xrightarrow{\overline{\omega}} := (\xrightarrow{\overline{\omega}} \beta_v \cup \Rightarrow_{\oplus})$ and $\xrightarrow{\overline{\omega}} := (\xrightarrow{\overline{\omega}} \beta_v)$. Then $(\mathcal{M}(\Lambda_{\oplus}), \{\Rightarrow_{\beta_v}, \Rightarrow_{\oplus}\})$ satisfies w-factorization Fact($\xrightarrow{\overline{\omega}}, \xrightarrow{\overline{\omega}}$).

**Proof.** We verify that the conditions of Theorem 3.4 hold. Note that $\oplus$ has no internal steps, therefore, it suffices to verify only two conditions:

1. weak factorization of $\Rightarrow_{\beta_v}: \text{Fact}(\xrightarrow{\overline{\omega}} \beta_v, \xrightarrow{\overline{\omega}} \beta_v)$.

2. $\xrightarrow{\overline{\omega}} \beta_v$ linearly swaps with $\Rightarrow_{\oplus}: \xrightarrow{\overline{\omega}} \beta_v \cdot \Rightarrow_{\oplus} \subseteq \Rightarrow_{\oplus} \Rightarrow_{\beta_v}^*$.

The other two conditions of Theorem 3.4 hold vacuously, because $\xrightarrow{\overline{\omega}} \oplus = \emptyset$ (and $\xrightarrow{\overline{\omega}} \oplus = \Rightarrow_{\oplus}$).

1. $\text{Fact}(\xrightarrow{\overline{\omega}} \beta_v, \xrightarrow{\overline{\omega}} \beta_v)$ follows from weak factorization of the CbV $\lambda$-calculus $\text{Fact}(\xrightarrow{\overline{\omega}} \beta_v, \xrightarrow{\overline{\omega}} \beta_v)$ (see Sect. 6) because clearly $([1M] \Rightarrow_{\beta_v} [1N]$ if and only if $M \to_{\beta_v} N$), $([1M] \Rightarrow_{\overline{\omega}} \beta_v [1N]$ if and only if $M \xrightarrow{\overline{\omega}} \beta_v N)$, and similarly $([1M] \xrightarrow{\overline{\omega}} \beta_v [1N]$ if and only if $M \xrightarrow{\overline{\omega}} \beta_v N)$.

2. Lemma B.1 implies $m \xrightarrow{\overline{\omega}} \beta_v \cdot \Rightarrow_{\oplus} n \subseteq m \Rightarrow_{\oplus} \Rightarrow_{\beta_v} n$, by the definition of lifting. ◀

<footnote n="4">⁴ In [19], a weak reduction (resp. weak context) is called surface, and hence noted $\xrightarrow{\overline{s}}$.</footnote>