IRIF, CNRS—Université de Paris Cité, F-75013 Paris, FrancePartly funded by the
ANR project PPS, ANR-19-CE48-0014. Huawei Research, Edinburgh Research Centre,
Edinburgh, United
Kingdomgiulio.guerrieri@huawei.comhttps://orcid.org/0000-0002-0469-4279
Claudia Faggian and Giulio Guerrieri [100]Theory of Computation Models of
computation [100]Theory of computation Equational logic and rewriting
[100]Theory of computation Lambda calculus Amy P. Felty 1 7th International
Conference on Formal Structures for Computation and Deduction (FSCD 2022) FSCD
2022 FSCD 2022 August 2–5, 2022 Haifa, Israel 228 8

# Strategies for Asymptotic Normalization

Claudia Faggian  Giulio Guerrieri

###### Abstract

We present an abstract technique to study normalizing strategies when
termination is asymptotic, that is, it appears as a limit. Asymptotic
termination occurs in several settings, such as effectful, and in particular
probabilistic computation—where the limits are distributions over the possible
outputs—or infinitary lambda-calculi—where the limits are infinitary terms
such as Böhm trees.

As a concrete application, we obtain a result which is of independent
interest: a normalization theorem for Call-by-Value (and—in a uniform way—for
Call-by-Name) probabilistic lambda-calculus.

###### keywords:

rewriting, strategies, normalization, lambda calculus, probabilistic rewriting

##  1 Introduction

Probabilistic computation is an example of computational paradigm where the
notion of termination is _asymptotic_ , that is, it appears as a _limit_ , as
opposed to reaching a normal form in a _finite_ number of steps. Streams,
infinitary $\lambda$-calculus, algebraic rewriting systems, effectful
computation, are other examples: the notion of asymptotic computation is
pervasive. Here, we investigate asymptotic normalization, and propose a
technique to prove that a strategy is guaranteed to produce a maximal
or—ideally—the best possible result. Our technique is abstract (in the sense
of Abstract Rewriting Systems) and so of general application.

Rewriting is a foundation for the operational theory of formal calculi and
programming languages—$\lambda$-calculus being the paradigmatic example where
rewriting is an abstract form of program execution. Even if a programming
language is usually defined by a specific _evaluation strategy_ , to have a
general rewriting theory allows for _program transformations, optimizations,
parallel/distributed implementations_ , and provides a base on which to reason
about program equivalence. The $\lambda$-calculus has a rich theory that
studies the properties of reductions. Asymptotic computation is much less
understood from a rewriting point of view, with the notable exception of
infinitary $\lambda$-calculus, whose rewriting theory, pioneered in [22, 9,
23], has been extensively studied.

The process of rewriting describes the _computation of a result_. Normal
forms, head normal forms, values, may or must termination, are all possible
notions of result. For concreteness, let us focus on normal forms.
Operationally, key questions about a system are the existence and uniqueness
of normal forms, but also _how_ the result is computed. In a _finitary
setting_ we would ask: may a computation produce a result (_Existence_ of
normal forms)? If so, is the result unique? Do different computations on the
same input lead to the same result (_Uniqueness_ of normal forms)? How to
compute a result? Is there a reduction strategy that is guaranteed to output a
result, if any exists (_Normalizing strategy_)? In the _asymptotic case_ ,
such questions are still relevant, but need to be opportunely formulated. To
answer, we then need suitable tools and techniques, because those for finitary
computation do not necessarily transfer (the key game-changer being that
asymptotic termination does not provide a well-founded order, see [13] for
examples in a probabilistic setting).

####  Abstract Asymptotic Rewriting.

Our approach is to study asymptotic reduction strategies and properties of
limits in an _abstract_ way (independent of the specific syntax of a calculus)
as the theory of Abstract Rewrite Systems (ARS) does for finitary computation,
so to isolate proof-techniques which are of general application. For example,
in infinitary lambda calculus, the limit is usually a (possibly infinite)
limit term, while in probabilistic lambda calculus, the limit is a
distribution over (finite) terms. The former is concerned with the depth of
the redexes, the latter with the probability of reaching a result. The
abstract notions of limit and normalization subsumes both, and so abstract
results apply to either setting. A further, conceptual advantage of an
abstract approach, is to display the essence of the arguments, an to neatly
discriminate between those properties which rely on specific structure of a
concrete setting, and those which belong to any asymptotic notion of
computation.

Specifically, we work in the setting of _Quantitative Abstract Rewrite System_
(QARS) [14], a framework to study asymptotic rewriting _abstractly_ which
refines Ariola and Blom’s ARSI [4].

#### From normal forms to limits.

Intuitively, a possibly infinite reduction sequence $\langle t_{n}\rangle_{n}$
from $t=t_{0}$ expresses a computation whose _result_ is the maximal amount of
information produced by that sequence. This is formalized as a limit. When the
reduction is deterministic, it is standard to interpret such a limit as the
meaning $\llbracket{t}\rrbracket$ of $t$. If however $t$ has _several possible
reduction sequences_ , each can produce a different outcome (a different
limit). It is then natural to define the meaning $\llbracket{t}\rrbracket$ of
a term $t$ as the _greatest_ element in the set of limits, if any.111One could
also define $\llbracket{t}\rrbracket$ as the lub of the set of limits, but
this opens the question if there is a strategy that asymptotically computes
$\llbracket{t}\rrbracket$, _internally_ to the calculus. Since our focus is
developing an _operational_ theory, we require that $\llbracket{t}\rrbracket$
is itself a limit – it is a result that can be (asymptotically) computed.
Intuitively, this means that the notion of “greatest amount of information
produced by any reduction sequence” is well defined. To adopt such a notion
demands care—for example, in the case of probabilistic and effectful
computation, non-deterministic evaluation brings out issues which do not
appear in pure lambda-calculus, not even when infinitary.

Given a term $t$ and a general reduction, the notion of result
$\llbracket{t}\rrbracket$ is not necessarily defined: the set of limits for
$t$ may contain different maximal elements, or it may not even have any
maximal element (think of $\mathbb{N}$ or $[0,1)$, which have no maximum).
Maximal limits play a role similar to normal forms, and the following
questions are then natural.

  1. 1.

Is there a strategy that produces a maximal amount of information (a maximal
limit)?

  2. 2.

Given a term $t$, is $\llbracket{t}\rrbracket$—the result of computing
$t$—well defined?

In Sect. 3 we provide tools to answer these questions, in this order, as we
discuss next.

#### On the workflow (and the limits of confluence).

The $\lambda$-calculus has two fundamental syntactical results: _confluence_ ,
which implies uniqueness of normal forms, and the _standardization theorem,_
which implies normalization, namely that a normal form can be reached by a
computable strategy, which is a standard reduction (typically, left-to-right).
Uniqueness guarantees that the notion of result is well defined, normalization
provides a method to actually compute it.

A common workflow when studying $\lambda$-calculi is to first prove uniqueness
of normal forms (via confluence), then normalization (via standardization).
However, in an asymptotic setting _confluence does not directly imply_ that
the set of limits has a greatest element, but only that it has a least upper
bound. So, even if confluence is established, one still needs to prove that
the lub is itself a limit, which may be a non-trivial task. For example, in
the probabilistic $\lambda$-calculus [13, 16, 14], such a proof relies on
(technical) properties of probability distributions.

In this paper, we _reverse the workflow_ , and focus on normalization. In the
finitary setting, if a rewriting relation $\rightarrow$ has a strategy
${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\subset{\rightarrow}$
which satisfies a suitable completeness hypothesis and uniqueness of normal
forms, so does $\rightarrow$ (see [11]). With opportune definitions, this
lifts well to the asymptotic setting. Forgoing confluence and focusing on
normalization yields an efficient and uniform method which is easy to apply
and which provides simultaneously (1.) existence and uniqueness of maximal
limits, and (2.) a strategy to compute it.

#### Content and contributions.

We start by illustrating asymptotic computation with examples (Sect. 1.1).
Instances of asymptotic computation are quite diverse, and the syntax of each
system may be rather complex. To study rewriting _abstractly_ , in the spirit
of of Abstract Rewriting Systems (ARS), makes possible to analyze asymptotic
properties in a way independent of specific syntax, and to develop _general_
proof techniques. In Sect. 2 we present the setting of Quantitative Abstract
Rewriting Systems (QARS) [14], which are ARS enriched with a notion of
observation. QARS are a natural refinement of ARSI [4].

11footnotetext: The difference between ARSI to QARS is moving from partial
orders to $\omega$-cpos as codomain of the observation function. QARS allows
us to deal uniformly with both finitary and asymptotic rewriting.

Our first original contribution, and the heart of this paper, is Sect. 3,
which proposes a proof technique to study asymptotic reduction strategies, and
properties of the limits. We first introduce _asymptotic normalization_ ,
which gives at the same time a tool to establish the existence of maximal
limits—or of a greatest one—and a way to compute it. It formalizes the
intuition that a normalizing strategy gradually computes (in a finite or
infinite number of steps) the/a maximal amount of information that an element
$t$ can produce. We then show (Sect. 3.1) that asymptotic normalization can be
established by proving that a strategy is asymptotically complete and has a
unique limit. Remarkably, such _infinitary properties_ reduce to a finitary
one, _factorization_ (a simple form of _standardization_) and to some _local,
elementary tests_ , yielding a practical and versatile proof-technique.

We then apply our method to some representative case studies based on
$\lambda$-calculus. In order to do so, we first revisit normalization for
$\lambda$-calculus—uniformly for CbV and CbN—so as to have _a (novel)
normalizing strategy_ which is well-suited to asymptotic normalization, and to
deal with probabilistic $\lambda$-calculi (Sect. 4.2). The application of our
method to _probabilistic $\lambda$-calculus_ yields a result of independent
interest, which was left as open question in [16] (Remark 27 there), namely a
theorem of asymptotic normalization for Call-by-Value probabilistic
$\lambda$-calculus. We develop the CbV case explicitly in Sect. 5.1—the same
results hold _in a uniform way_ for Call-by-Name. The same technique applies
to other monadic calculi such as calculi with output (as we sketch in Sect.
6), but also to the asymptotic computation of Böhm Trees, which can be
obtained as the limit of a normalizing strategy (we leave this case to
Appendix D.2).

###  1.1 Three examples of Asymptotic Computation

We illustrate three diverse examples of asymptotic computation, where the
result of the computation is the limit of an _infinitary_ process. All three
examples are built on $\lambda$-calculus.

#### Probabilistic computation.

A probabilistic program $P$ is a stochastic model generating a distribution
over all possible outputs of $P$. Even if the termination probability is $1$
(_almost sure termination_), that degree of certitude is typically not reached
in a finite number of steps, but _as a limit_. A standard example is a term
$M$ that reduces to either a normal form or $M$ itself, with equal probability
$1/2$. After $n$ steps, $M$ is in normal form with probability
$\frac{1}{2}+\frac{1}{2^{2}}+\dots+\frac{1}{2^{n}}$. _Only at the limit_ this
computation terminates with probability $1$. A direct way to model higher-
order probabilistic computation is to endow the untyped $\lambda$-calculus
with a binary operator $\oplus$ which models fair, binary probabilistic
choice: $M_{1}\oplus M_{2}$ reduces to either $M_{1}$ or $M_{2}$ with equal
probability $1/2$; we write this as $M_{1}\oplus
M_{2}\rightarrow[\frac{1}{2}M_{1},\frac{1}{2}M_{2}]$. Intuitively, _the
result_ of evaluating a probabilistic term is a _distribution_ on its possible
outputs.

######  Example 1.1.

Let $\Delta_{\oplus}=\lambda x.I\oplus(xx)$, where $I=\lambda x.x$. The term
$M:=\Delta_{\oplus}\Delta_{\oplus}$ has the behavior we have described above,
and evaluates to $I$ with probability $1$ only at the limit.

#### Computations with output.

Consider a program that can print an output. Following [17], we can represent
this with a pair ${\texttt{s}:M}$, where s is a string over an alphabet
$\mathbb{A}$, and $M$ is a term of the $\lambda$-calculus extended with a set
of operators $\mathtt{out}=\\{\mathtt{out}_{c}\mid c\in\mathbb{A}\\}$. The
term $\mathtt{out}_{c}(P)$ outputs $c$ , adding it to the string, and
continues as $P$. That is,
$\langle\texttt{s}:\mathtt{out}_{c}(P)\rangle\rightarrow\langle
c.\texttt{s}:P\rangle$.

######  Example 1.2.

Let $\mathbb{A}=\\{0,1\\}$, and $\Delta_{0}:=\lambda x.\mathtt{out}_{0}(xx)$.
The computation from $\langle\epsilon:\Delta_{0}\Delta_{0}\rangle$ (with
$\epsilon$ the empty string) produces a stream: a string of $0$’s whose length
tends to infinity.

#### Infinite Normal Forms.

Infinitary $\lambda$-calculi [22, 9, 23] model infinite structures in
$\lambda$-calculi. Terms and reduction sequences need not be finite. An
infinite reduction sequence is _strongly convergent_ if the depth of the
contracted redex tends to infinity. Based on different depth measures, in [23]
eight different infinitary $\lambda$-calculi are developed. If the calculus is
_confluent_ , the _infinite normal form of a term $N$ is unique_, and it is
the _meaning of $N$_. Infinite normal forms are well-known in
$\lambda$-calculus in the form of Böhm tres [7] or Lévy-Longo trees [29].

######  Example 1.3.

Let $\Delta_{z}:=\lambda x.z(xx)$. In the (infinite) reduction sequence
$\Delta_{z}\Delta_{z}\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}z(\Delta_{z}\Delta_{z})\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}z(z(\Delta_{z}\Delta_{z}))\allowbreak\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}z(z(z(\Delta_{z}\Delta_{z})))\dots$,
the depth of the redex $\Delta_{z}\Delta_{z}$ tends to infinity. It is
intuitively clear that $\Delta_{z}\Delta_{z}$ has an _infinite normal form_
$z(z(z\dots))$.

#### Notation.

From now on, we use the following standard notations: $I=\lambda
x.x,\quad\Delta=\lambda x.xx$, together with: $\Delta_{\oplus}=\lambda
x.I\oplus(xx),\quad\Delta_{c}:=\lambda
x.\mathtt{out}_{c}(xx),\quad\Delta_{z}:=\lambda x.z(xx)$.

###  1.2 Motivations, and necessity, for non-deterministic evaluation.

In this paper we are concerned with evaluation towards a limit. We allow the
evaluation $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ (the normalizing
strategy) to be _non-deterministic_. Let us discuss the motivations.

A programming language which is built on a $\lambda$-calculus implements a
specific evaluation strategy $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ of the general
reduction $\rightarrow$. The evaluation strategy
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ may or may not be
deterministic, as long as _all choices eventually yield the same result_. Non-
deterministic evaluation (written NDE) is a useful feature, which for example
allows for parallel implementations, but in some cases is also a _necessity_
and a key _reasoning tool_ , as we discuss.

1. _NDE subsumes different evaluation policies_. A good illustration of this is in Plotkin’s Call-by-Value $\lambda$-calculus, whose general reduction is $\mathrel{\rightarrow_{\beta_{v}}}$. _Weak_ evaluation (which does not reduce in the body of a function) evaluates closed terms to values. There are three main weak schemes (see Sect. 4.1): reducing left-to-right, as defined by Plotkin [32], right-to-left, as in Leroy’s ZINC abstract machine [27], or in an arbitrary order. While left and right reduction are deterministic, weak reduction in arbitrary order is non-deterministic and _subsumes_ both.

2. NDE _supports parallel/distributed implementation_. Non-deterministic evaluation does not define an abstract machine, but is includes _all possible parallel implementations_.

3. _NDE allows for breadth-first scheduling._ Left-to-right evaluation is inherently depth-first. NDE allows for breadth-first evaluation (favoring redexes at minimal depth), which is a necessity when the reduction graph is infinitary. An example comes from CbN $\lambda$-calculus. Thinking of Example 1.3, the terms $z(\Delta\Delta)(Iz)\mbox{ and }z(\Delta\Delta)(\Delta_{z}\Delta_{z})$ do deliver more information than $z(\Delta\Delta)(\Delta\Delta)$. Their respective infinite normal forms are very different ($z\Omega z\mbox{ and }z\Omega(zz\dots)$, respectively). Still, for both left evaluation gets stuck at the leftmost redex, $\Delta\Delta$. Similar phenomena appear with effectful computation: in CbV $\lambda$-calculus with output of Example 1.2, the terms $(\Delta\Delta)(\mathtt{out}_{0}(I))\mbox{ and }(\Delta\Delta)(\Delta_{0}\Delta_{0})$ behave similarly to the previous terms. A breadth-first approach allows one to compute the “best” (in some sense) possible result across all settings, uniformly.

4\.  _NDE facilitates reasoning and proofs._ This point is highly relevant
when dealing with complex calculi, such as a probabilistic $\lambda$-calculus.
Two examples from the literature are [16] and [10]—in both cases moving from
the usual deterministic head reduction to its non-deterministic variant (given
in Sect. 4.1) is crucial to the results.

##  2 Quantitative Abstract Rewriting Systems

In this section we present Quantitative Abstract Rewriting Systems (QARS) [14,
4]. QARS are Abstract Rewriting Systems (ARS) enriched with a notion of
observation, where we can formalize both finitary and asymptotic rewriting. We
first recall some standard notions of rewriting (see [33] or [6]), in
particular that of ARS and of _normalizing strategy_.

###  2.1 Basics in (Finitary) Rewriting

An _abstract rewriting system (ARS)_ is a pair $(\mathcal{A},\rightarrow)$
consisting of a set $\mathcal{A}$ and a binary relation $\rightarrow$ on
$\mathcal{A}$ whose pairs are written $t\xrightarrow{}s$ and called _steps_.
We denote $\rightarrow^{*}$ (resp. $\rightarrow^{=}$, $\rightarrow^{+}$) the
transitive-reflexive (resp. reflexive, transitive) closure of $\rightarrow$.
We write $t\leftarrow u$ if $u\rightarrow t$. If
$\rightarrow_{1},\rightarrow_{2}$ are binary relations on $\mathcal{A}$ then
$\rightarrow_{1}\cdot\rightarrow_{2}$ denotes their composition (_i.e._
$t\rightarrow_{1}\cdot\rightarrow_{2}s$ if there exists $u\in\mathcal{A}$ such
that $t\rightarrow_{1}u\rightarrow_{2}s$). The relation $\rightarrow$ is
_confluent_ if ${\leftarrow}^{*}\cdot{\rightarrow}^{*}{\leavevmode\nobreak\
\subseteq\leavevmode\nobreak\ }{\rightarrow}^{*}\cdot\,{\leftarrow}^{*}$. An
element $u\in\mathcal{A}$ is $\rightarrow$-normal, or a $\rightarrow$-_normal
form_ (_nf_) if there is no $t$ such that $u\rightarrow t$ (we also write
$u\not\rightarrow$).

A $\rightarrow$-sequence (or reduction sequence) from $t$ is a possibly
infinite sequence $t=t_{0},\ t_{1},\ t_{2},\dots$ such that $t_{i}\rightarrow
t_{i+1}$. Notice that $t\rightarrow^{*}s$ holds exactly when there is a
_finite_ sequence from $t$ to $s$—we often write $t\rightarrow^{*}s$ to
indicate a finite $\rightarrow$-sequence. A $\rightarrow$-sequence from $t$ is
_maximal_ if it is either infinite or ends in a $\rightarrow$-_nf_. We write
$\langle t_{n}\rangle_{n}$ to indicate a maximal $\rightarrow$-sequence from
$t_{0}$; by convention, if $t_{i}=u\not\rightarrow$ then $t_{k}=u$ for all
$k\geq i$.

#### Normalization.

In general, $t\in\mathcal{A}$ may or may not reduce to a normal form. And if
it does, not all reduction sequences necessarily lead to normal form.
$(\mathcal{A},\rightarrow)$ is strongly (weakly, uniformly) normalizing if
every $t\in\mathcal{A}$ is, where the normalization notions are as follows.

  * •

$t$ is _strongly $\rightarrow$-normalizing_: every maximal
$\rightarrow$-sequence from $t$ ends in a normal form;

  * •

$t$ is _weakly $\rightarrow$-normalizing_: there is a $\rightarrow$-sequence
from $t$ which ends in a normal form;

  * •

$t$ is _uniformly $\rightarrow$-normalizing_: $t$ weakly
$\rightarrow$-normalizing implies $t$ strongly $\rightarrow$-normalizing.

Untyped $\lambda$-calculus is not strongly normalizing. How do we compute a
normal form, or _test_ if any exists? This problem is tackled by _normalizing
strategies_. By repeatedly performing _only specific steps
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$_, we are guaranteed
that a normal form, if any, will eventually be computed.

A reduction $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ is a _one-step_
(resp.  _multi-step_) _strategy for $\rightarrow$_ if
${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\subseteq{\rightarrow}$
(resp. ${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\subseteq{\rightarrow^{+}}$),
and it has the same normal forms as $\rightarrow$. It is a normalizing
strategy for $\rightarrow$ if, moreover, whenever $t$ has a
$\rightarrow$-normal form, then _every_ maximal
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$-sequence from $t$
ends in a $\rightarrow$-normal form. Note that $\rightarrow$ may not have the
property of unique normal forms.

######  Remark 2.1.

A familiar example of calculus where terms may not have a unique normal form
is Call-by-Name Weak $\lambda$-calculus (weak means no reduction under
$\lambda$), studied by Abramsky and Ong [1]. The term $M=(\lambda xy.x)(II)$
has two distinct normal forms, $N_{1}=\lambda y.II$ and $N_{2}=\lambda y.I$.
Weak head reduction is a normalizing strategy for it. However the strategy is
not complete, in the sense that it produces the normal form $N_{1}$, but it
cannot reach $N_{2}$.

A normalizing strategy $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ need not be
deterministic (a reduction $\rightarrow$ is deterministic if for all
$t\in\mathcal{A}$ there is at most one $s\in\mathcal{A}$ such that
$t\rightarrow s$). However, $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ is required to be
_uniformly normalizing_ on all elements $t$, _i.e._ , all reduction sequences
have the same behavior.

A property of $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ which guarantees
uniform normalization is Newman’s _Random Descent (RD)_ [31]: for each
$t\in\mathcal{A}$, all maximal sequences from $t$ have the same length and—if
it is finite—they all end in the same element. The following property suffices
to establish it.

######  Fact 1 (Newman).

If reduction $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ is RD-diamond, then
it has Random Descent, where

_RD-diamond_ : $(t_{1}\ \mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}}\leavevmode\nobreak\
\ t\ \mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}\ t_{2})\mbox{
implies }(t_{1}=t_{2}\mbox{ or }\exists u.\leavevmode\nobreak\ t_{1}\
\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}\ u\
\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}}\leavevmode\nobreak\
\ t_{2})$.

###  2.2 QARS

Ariola and Blom [4] have introduced the notion of Abstract Rewrite Systems
with Information content (ARSI); a rewrite system is associated with a partial
order that expresses the “information content” of the elements. ARSI however
are tailored to infinite normal forms in the sense of Böhm and Levy-Longo
trees: limits are there given by the ideal completion [3, Prop. 1.1.21] of the
partial order. QARS [14] move from partial orders to _$\omega$ -complete
partial orders_ ($\omega$-cpos)—this is enough to capture also effectful
computation, such as the probabilistic one. We illustrate the key notions with
several examples, including the calculi from Sect. 1.1.

Computation is a process that produces a result by gradually increasing the
amount of available information—the standard structure to express a result in
terms of partial information is that of an $\omega$-cpo. Recall that a
partially ordered set $\mathbb{S}=(\mathbb{S},\leq)$ is an $\omega$-complete
partial order ($\omega$-cpo) if every $\omega$-chain
$\boldsymbol{s}_{0}\leq\boldsymbol{s}_{1}\leq\dots$ has a supremum. We assume
that $\leq$ has a _least element_ $\bot$. The elements of $\mathbb{S}$ are
denoted by bold letters $\boldsymbol{s},\boldsymbol{p},\boldsymbol{q}$.

Let $(\mathcal{A},\rightarrow)$ be an ARS. With each $t\in\mathcal{A}$ is
associated a notion of (partial) information, called _observation_ , by means
of a function from $\mathcal{A}$ to an $\omega$-cpo. Def. 2.2 formalizes this
idea.

######  Definition 2.2 (QARS).

A _quantitative ARS_ (_QARS_) is an ARS $(\mathcal{A},\rightarrow)$ with a
function $\mathtt{obs}\colon\mathcal{A}\rightarrow\mathbb{S}$ (where
$\mathbb{S}$ is an $\omega$-cpo) such that for all $t,s\in\mathcal{A}$, if
$t\rightarrow s$ then $\mathtt{obs}(t)\leq\mathtt{obs}(s)$.

Intuitively, the function $\mathtt{obs}$ observes a specific property of
interest about $t\in\mathcal{A}$, and indicates how much stable information
$t$ delivers: the information content is monotonically increasing during
computation. Notice that $\mathtt{obs}$ may take numerical values, but needs
not.

######  Example 2.3.

  1. 1.

$\lambda$-calculus: let $\mathbb{S}=\\{0<1\\}$ and $\mathtt{obs}_{n}(t)=1$ if
$t$ is normal, $0$ otherwise.

  2. 2.

Probabilistic $\lambda$-calculus: take $\mathbb{S}=([0,1],\leq_{\mathbb{R}})$,
and for $\mathtt{obs}$ the probability to be in normal form (we will formalize
this in Sect. 5 , see $\mathtt{obs}_{{pn}}(\mathtt{m})$ in Fig. 4.)

  3. 3.

Infinitary $\lambda$-calculus: take
$\mathbb{S}=\mathbb{N}^{\infty}=\mathbb{N}\cup\\{\infty\\}$ with the usual
order, and for $\mathtt{obs}$ the function which associates with any term $t$
the minimal depth $k$ of any redex in $t$.

######  Example 2.4 (Non-numerical $\mathtt{obs}$).

  1. 1.

$\lambda$-calculus: take for $\mathbb{S}$ the flat order on normal forms, and
define $\mathtt{obs}_{\mathcal{N}}(u)=u$ if $u$ is normal,
$\mathtt{obs}_{\mathcal{N}}(u)=\bot$ otherwise.

  2. 2.

Probabilistic $\lambda$-calculus: take for $\mathbb{S}$ the $\omega$-cpo of
the subdistributions on normal forms $\mathcal{D}(\mathcal{N})$ (we will
formalize this in Sect. 5, see Fig. 4).

  3. 3.

Infinitary $\lambda$-calculus: take the $\omega$-cpo of the partial normal
forms that are associated with $\lambda$-terms (see [3] page 52, and Sect.
D.2).

#### Limits as Results.

From now on, let $\mathcal{Q}=((\mathcal{A},\rightarrow),\mathtt{obs})$ be an
arbitrary but fixed QARS. By definition, given a $\rightarrow$-sequence
$\langle t_{n}\rangle_{n}$, its _limit_
$\sup_{n}\\{\mathtt{\mathtt{obs}}(t_{n})\\}$ with respect to $\mathtt{obs}$
always exists, because $\mathbb{S}$ is an $\omega$-cpo. If $\rightarrow$ is
deterministic—hence any $t$ has a unique maximal $\rightarrow$-sequence—it is
standard to interpret the limit as the _meaning_ of $t$. In a QARS, $t$ has
_several possible reduction sequences_ , and so can produce several outcomes
(limits). Following [13]:

######  Definition 2.5 ($\mathtt{obs}$-limits).

Let $t\in\mathcal{A}$. We write

  * •

$t\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\boldsymbol{p}$, if there exists a $\rightarrow$-sequence $\langle
t_{n}\rangle_{n}$ from $t$ whose limit
$\sup_{n}\\{\mathtt{\mathtt{obs}}(t_{n})\\}=\boldsymbol{p}$;

  * •

$\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$ is the set $\\{\boldsymbol{p}\mid
t\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\boldsymbol{p}\\}$ of limits from $t$;

  * •

${\llbracket{t}\rrbracket}$ denotes the greatest element of
$\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$, if it exists.

The notations omit the subscript $\mathtt{obs}$ when the function
$\mathtt{obs}$ is clear from the context.

Intuitively, $\llbracket{t}\rrbracket$ is well defined if different reduction
sequences from $t$ do not produce _essentially different_ results: if
$\boldsymbol{q}\not=\boldsymbol{p}$ then they both approximate a same result
$\boldsymbol{r}$ (_i.e._ , $\boldsymbol{q},\ \boldsymbol{p}\ \leq\
\boldsymbol{r}$).

Thinking of usual rewriting, consider $\mathtt{obs}_{\mathcal{N}}$ as in
Example 2.4, point 1: here to have a greatest limit exactly corresponds to
uniqueness of normal forms.

######  Example 2.6.

Let us revisit Example 2.3 pointwise, using the same notations.

  1. 1.

$\lambda$-calculus: consider $t=(\lambda x.z)(\Delta\Delta)$. This term has
infinite possible
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$-sequences. The set of
limits w.r.t. $\mathtt{obs}_{n}$ contains two elements:
$\mathtt{Lim}_{\mathtt{obs}_{n}}(t,\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}})=\\{0,1\\}$

  2. 2.

Probabilistic $\lambda$-calculus: consider the term $I\oplus\Delta\Delta$. It
has only one reduction sequence
$\mathtt{m}=[I\oplus\Delta\Delta]\Rightarrow[\frac{1}{2}I,\frac{1}{2}\Delta\Delta]\Rightarrow[\frac{1}{2}I,\frac{1}{2}\Delta\Delta]\Rightarrow\dots$.
Here
$\mathtt{Lim}_{\mathtt{obs}_{{pn}}}(\mathtt{m},\Rightarrow)=\\{\frac{1}{2}\\}$.

  3. 3.

Infinitary $\lambda$-calculus: consider the reduction sequence in Example 1.3.
The depth of the redex $(\Delta_{z}\Delta_{z})$ tends to $\infty$, which is
the limit.

Note that maximal elements of $\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$
need not be maximal elements of $\mathbb{S}$. For instance, in Example 2.6.2,
the term $I\oplus(\Delta\Delta)$ converges with probability $\frac{1}{2}$
(rather than $1$). As a consequence, _the set of limits may or may not have
maximal elements_. The fact that $\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$
may have a lub but not a maximum—similarly to $\mathbb{N}$ in
$\mathbb{N}^{\infty}$ or the real interval $[0,1)$— is also easy to realize.
We give an example in Some more examples., see Example .1.

Even if $\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$ has maximal elements, a
greatest limit does not necessarily exist: different reduction sequences may
lead to different limits. The probabilistic $\lambda$-calculus and the
$\lambda$-calculus with output provide several natural examples. Point 2 in
Example 2.7 below shows moreover that the set of limits is—in general—
_uncountable_.

######  Example 2.7 (Output $\lambda$-calculus).

Consider the calculus sketched in Example 1.2. Let
$\mathtt{Out}_{\mathbb{A}}=(\mathbb{A}^{*}\times\Lambda_{\mathtt{out}},\leavevmode\nobreak\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}})$, where
reduction is _CbV and weak_ , with the obvious definitions. Let $\mathbb{S}$
be the $\omega$-cpo of strings, and let
$\mathtt{obs}(\langle\texttt{s}:M\rangle)=\texttt{s}$. Clearly,
$(\mathtt{Out}_{\mathbb{A}},\mathtt{obs})$ is a QARS.

  1. 1.

Let
$\mathtt{m}=\langle\epsilon:\mathtt{out}_{0}(I)\mathtt{out}_{1}(I)\rangle$.
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m},{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}})$ contains
two limits, $10$ and $01$, both maximal, because
$\mathtt{m}{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\langle
0:I\mathtt{out}_{1}(I)\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\langle
10:II\rangle$, but also
$\mathtt{m}{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\langle
1:\mathtt{out}_{0}(I)I\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\langle
01:II\rangle$.

  2. 2.

Let $\mathtt{m}^{\prime}=\langle\epsilon:M^{\prime}\rangle$ for
${M^{\prime}=(\Delta_{0}\Delta_{0})(\Delta_{1}\Delta_{1})}$. This produces all
possible sequences on the alphabet $\\{0,1\\}$. So
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m}^{\prime},{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}})$ has
uncountable many elements, all maximal.

We are interested in the case when a greatest limit exists. The reason is that
if $\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$ has a sup
$\boldsymbol{s}\in\mathbb{S}$ which does not belong to
$\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$, no reduction sequence converges
to $\boldsymbol{s}$; that is, we cannot compute $\boldsymbol{s}$ internally to
the calculus.

##  3 Strategies and Asymptotic Normalization

The question of whether the result $\llbracket{t}\rrbracket$ of computing an
element $t$ is well defined is natural. Equally natural is to wonder if there
is a strategy that is guaranteed to compute $\llbracket{t}\rrbracket$. These
two questions are at the core of this section. The existence of unique normal
forms is independent of that of a normalizing strategy (see Remark 2.1).
However, the computationally interesting case is (often) when both hold, so we
will focus on this case.

We say that a reduction ${{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}}\subseteq\rightarrow$
is (asymptotically) normalizing if _each_
${{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}}$-sequence from a
given $t$ converges _maximally_. We decompose this property in two properties:
completeness and uniformity, which we discuss after the formal definition.

######  Definition 3.1 (Asymptotic properties).

Given a QARS $\big{(}(\mathcal{A},\rightarrow),\mathtt{obs}\big{)}$, a
subreduction ${{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}}\subseteq{\rightarrow}$
is asymptotically normalizing for $\rightarrow$ (or
$\mathtt{obs}$-normalizing) if it is both asymptotically complete and uniform,
where

  1. 1.

${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}$ is asymptotically
complete (or $\mathtt{obs}$-complete) if

$(\forall t\in\mathcal{A})$ :
$t\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\boldsymbol{q}$ implies $t{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\boldsymbol{p}$ for some $\boldsymbol{p}$ such that
$\boldsymbol{q}\leq\boldsymbol{p}$;

  2. 2.

$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ is asymptotically
uniform (or $\mathtt{obs}$-uniform) if

$(\forall t\in\mathcal{A})$ : all elements in
$\mathtt{Lim}_{\mathtt{obs}}(t,{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}})$ are maximal in
$\mathtt{Lim}_{\mathtt{obs}}(t,{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}})$.

All definitions adapt to $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ multistep
subreduction of $\rightarrow$.

Let us discuss all components, comparing with their ARS analog.

  * •

_Completeness_ guarantees that the strategy
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ is as good as
$\rightarrow$ in the amount of information it produces.

  * •

_Completeness is not enough:_ an asymptotically complete strategy is not
guaranteed to find a/the “best” result: in Sect. 5.1 we will study a reduction
$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ which is complete, but need not converge to the greatest limit
(Remark 5.3). Let us first see a classical example.

######  Example 3.2.

In the usual $\lambda$-calculus (as in Example 2.6.1), the term $M=(\lambda
x.I)(\Delta\Delta)$ has a
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$-sequence which reaches
$I$, and a diverging one. The leftmost-outermost strategy always produces $I$
(it is complete _and_ normalizing). Notice that
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$ is _trivially a
complete strategy_ for
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$, but it is not
normalizing, because $M$ has a diverging
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$-sequence. Indeed,
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$ is _complete, but not
uniform_.

  * •

_Asymptotic uniformity_ expresses that all
${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}$-sequences from a
term behave the same way. This corresponds to the ARS notion of _uniform
normalization_ : the reduction sequences from a term either all diverge, or
all terminate (not necessarily in the same normal form).

  * •

_Normalizing strategies._ If we consider usual ARS, and assume $\mathtt{obs}$
as in Example 2.3.1, expressing whether $t$ is or is not normal, then a
strategy for $\rightarrow$ that is $\mathtt{obs}$-normalizing is exactly a
normalizing strategy for $\rightarrow$ in the usual sense.

If ${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\subseteq\rightarrow$
is $\mathtt{obs}$-_complete_ , then
$\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$ has maximal elements (resp. a
greatest element) if and only if
$\mathtt{Lim}_{\mathtt{obs}}(t,{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}})$ does. So we can
reduce testing such properties for $\rightarrow$, to testing the same
properties for $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$, which is often
simpler to study. In particular, if we are able to find a reduction
${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\subseteq\rightarrow$
which is complete and moreover has a unique limit, then necessarily
$\rightarrow$ has a greatest limit. That is, we can simultaneously answer both
of our questions: whether $\llbracket{t}\rrbracket$ is well defined, and if
some strategy is guaranteed to compute it.

######  Proposition 2 (Main, abstractly).

If the following hold

  1. i.

${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}$ is asymptotically
complete for $\rightarrow$;

  2. ii.

$\mathtt{Lim}_{\mathtt{obs}}(t,{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}})$ contains a unique
element (_i.e._
$\mathtt{Lim}_{\mathtt{obs}}(t,{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}})=\\{\boldsymbol{p}\\}$,
for some $\boldsymbol{p}$).

Then: (1.) $\llbracket{t}\rrbracket$ is defined, and (2.)
$t{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\llbracket{t}\rrbracket$, for each
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$-sequence.

Notice that condition (ii.) means that _all_
${\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}$-sequences from the
term $t$ have the _same_ limit.

######  Remark 3.3 (Asymptotically normalizing strategies).

If a QARS is such that $\llbracket{t}\rrbracket$ is defined for each $t$, then
the two notions—to be an $\mathtt{obs}$-normalizing strategy and to satisfy
the conditions in Prop. 2—coincide. Indeed, any $\mathtt{obs}$-normalizing
strategy for $\rightarrow$, if it exists, is forced to have a _unique_ limit,
that is,
$\mathtt{Lim}_{\mathtt{obs}}(t,{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}})=\\{\llbracket{t}\rrbracket\\}$.

###  3.1 A proof technique for Asymptotic Normalization

The two conditions in Prop. 2 give a method to prove normalization. The
crucial step is to prove asymptotic completeness. Remarkably, as we show in
this section, this can be reduced to prove a _finitary_ property
(_factorization_) and an elementary one-step test (_neutrality_).

The other condition in Prop. 2, namely uniqueness of limits, is trivial if the
strategy is deterministic. Otherwise, random descent (opportunely formulated
[14]) is a property that guarantees it, and that can also be established via a
local test, as we recall below. While it is only a sufficient criterion, it
often suffices to deal with non-deterministic evaluation strategies in
$\lambda$-calculus, and in particular it suffices to deal with strategies in
probabilistic $\lambda$-calculus.

#### Asymptotic Completeness via Factorization.

The following theorem assumes a partition of the $\rightarrow$-steps into two
classes: essential steps $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ and internal steps
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}$. Point (i) states that every sequence $\rightarrow^{*}$ factorizes
into a $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$-sequence followed
by a $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}$-sequence. Point (ii) states that the internal steps
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}$ do not increase the information content.

######  Theorem 3.4 (Asymptotic completeness criterion).

Given $((A,\rightarrow),\mathtt{obs})$ a QARS, and a subrelation
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}\subseteq\rightarrow$,
assume :

  1. i.

_$\mathsf{e}$ -factorization_: if $t\xrightarrow{}^{*}u$ then
$t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}\cdot\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}^{*}u$;

  2. ii.

_${\neg\mathsf{e}}$ -neutrality_:
$t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}s$ implies $\mathtt{\mathtt{obs}}(t)=\mathtt{\mathtt{obs}}(s)$.

Then: $t\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\boldsymbol{p}\mbox{ implies }t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}\leavevmode\nobreak\
\boldsymbol{p}.$

######  Proof 3.5.

Let $\langle t_{n}\rangle_{n}$ be a $\rightarrow$-sequence such that $t=t_{0}$
and $\sup_{n}\\{\mathtt{\mathtt{obs}}(t_{n})\\}=\boldsymbol{p}$. From $t$, we
inductively build a $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$-sequence $\langle
s_{n}\rangle_{n}$ with $s_{0}=t$ and such that, for every $k\in\mathbb{N}$,
there is an index $j(k)$ such that
$t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}s_{j(k)}$ and
$s_{j(k)}\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}^{*}t_{k}$. Case $k=0$ is trivial (set $s_{j(0)}:=t$).

Assume the claim holds for $k\geq 0$, so
$t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}s_{j(k)}$.
Observe that we have a sequence
$s_{j(k)}\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}^{*}t_{k}\rightarrow t_{k+1}$. By applying assumption (i.) to it, we
have $s_{j(k)}\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}u\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}^{*}t_{k+1}$. We concatenate
$t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}s_{j(k)}$ and
$s_{j(k)}\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}u$ to obtain
$t\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}s_{j(k)}\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}^{*}s_{j(k+1)}:=u$,
as desired. By assumption (ii.),
$s_{j(k)}\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{e}\leavevmode\nobreak\
$}\vss}}}^{*}t_{k}$ implies
$\mathtt{\mathtt{obs}}(t_{k})=\mathtt{\mathtt{obs}}(s_{j(k)})$. The claim
easily follows.

#### Uniqueness of the limit via Random Descent.

To establish that a strategy has a unique limit, Random Descent [31, 34, 35]
has already been shown to adapt well and naturally in a probabilistic and
asymptotic setting [13, 14].

The property $\mathtt{obs}$-RD below states that if $t$ has different
reduction sequences, they are all _indistinguishable_ if regarded through the
lenses of $\mathtt{obs}$. Namely, all reduction sequences $\langle
t_{n}\rangle_{n}$ starting from $t$ induce the same $\omega$-chain
$\langle\mathtt{obs}(t_{n})\rangle_{n}$. Thus, they all have the same
$\mathtt{obs}$-limit.

######  Definition 3.6 (Weighted Random Descent).

Let $((\mathcal{A},\rightarrow),\mathtt{obs})$ be a QARS. The relation
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}\subseteq\rightarrow$
satisfies the following properties if they hold for each $t\in\mathcal{A}$.

  1. 1.

$\mathtt{obs}$-RD: for each pair of
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$-sequences $\langle
r_{n}\rangle_{n}$, $\langle s_{n}\rangle_{n}$ from $t$,
$\mathtt{\mathtt{obs}}(r_{n})=\mathtt{\mathtt{obs}}(s_{n})$ for all $n$.

  2. 2.

$\mathtt{obs}$-diamond: $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}$ satisfies RD-
diamond, and if $t\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}}}\leavevmode\nobreak\
m\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}}s$ then
$\mathtt{\mathtt{obs}}(s)=\mathtt{\mathtt{obs}}(t)$.

######  Proposition 3 ([14]).

With the same notation as in Def. 3.6:
($\mathtt{obs}$-diamond) $\Rightarrow$ ($\mathtt{obs}$-RD) $\Rightarrow$
$\mathtt{Lim}_{\mathtt{obs}}(t,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{e}$}\vss}}})$ contains a unique
element.

######  Example 3.7 (CbV Weak reduction).

Let us consider Call-by-Value $\lambda$-calculus with weak reduction
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$, where weak
means no reduction in the scope of $\lambda$-abstractions. The following are
two different ${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$-sequences
from the term $(II)(Ix)$:
$(II)(Ix)\ {{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\ I(Ix)\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\ Ix\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\
x\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \mbox{ and
}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (II)(Ix)\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\ (II)x\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\ Ix\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\ x.$

The observations of interest are values. Let
$\mathtt{obs}_{v}:\Lambda\xrightarrow{}\\{0,1\\}$ be $1$ if the term is a
_value_ (i.e. a variable or an abstraction), $0$ otherwise. Through the lenses
of $\mathtt{obs}_{v}$, both sequences appear as $\langle
0,\leavevmode\nobreak\ 0,\leavevmode\nobreak\ 0,\leavevmode\nobreak\
1\rangle$.

##  4 Normalization in CbV and CbN $\lambda$-calculi

In the rest of the paper, we study asymptotic normalization in the setting of
$\lambda$-calculi—in particular we are interested in probabilistic
$\lambda$-calculus (Sect. 5).

In this section, after recalling the general syntax of $\lambda$-calculus, we
define a novel, flexible normalizing strategy, which is uniformly defined for
_Call-by-name_ (CbN) and _Call-by-Value_ (CbV) $\lambda$-calculi. Its
features—in particular the fact that it support breadth-first reduction—make
it suitable to then be extended to asymptotic normalization, in different
settings.

###  4.1 Call-by-Name and Call-by-Value (applied) $\lambda$-calculus

We recall the basics of $\lambda$-calculus. Our syntax admits _operator
symbols_ [20, 32], _i.e._  _constants_ with a fixed arity for their arguments.
_Terms_ and _values_ are defined by the grammars below.

$\begin{array}[]{rcllr}M&\Coloneqq&x\mid\lambda x.M\mid
MM\mid\mathbf{o}(M,\dots,M)&(\text{\emph{Terms,} }\Lambda_{\mathcal{O}})\\\
V&\Coloneqq&x\mid\lambda x.M&(\text{\emph{Values,} }\mathcal{V})\\\
\end{array}$

where $x$ ranges over a countable set of _variables_ , and $\mathbf{o}$ over a
disjoint (possibly empty) set $\mathcal{O}$ of operator symbols. If
$\mathcal{O}$ is empty, the calculus is _pure_ and we set
$\Lambda\coloneqq\Lambda_{\mathcal{O}}$. Terms are identified up to renaming
of bound variables, where $\lambda x$ is the only binder constructor.
$P\\{Q/x\\}$ is the capture-avoiding substitution of $Q$ for the free
occurrences of $x$ in $P$.

Contexts (with an hole $\llparenthesis\ \rrparenthesis$) are defined by the
grammar below. $\boldsymbol{\mathsf{C}}\llparenthesis N\rrparenthesis$ stands
for the term obtained from $\boldsymbol{\mathsf{C}}$ by replacing the hole
with $N$ (possibly capturing the free variables of $N$).

$\boldsymbol{\mathsf{C}}::=\llparenthesis\leavevmode\nobreak\
\rrparenthesis\mid
M\boldsymbol{\mathsf{C}}\mid\boldsymbol{\mathsf{C}}M\mid\lambda
x.\boldsymbol{\mathsf{C}}\mid\mathbf{o}(M,\dots,\boldsymbol{\mathsf{C}},\dots,M)\qquad(\textit{Contexts})$

#### Rules and Reductions.

A rule $\rho$ is a binary relation on $\Lambda_{\mathcal{O}}$, which we also
denote $\mapsto_{\rho}$, writing $R\mapsto_{\rho}R^{\prime}$. $R$ is called a
$\rho$-_redex_. The best known rule is $\beta$: $(\lambda
x.M)N\leavevmode\nobreak\ \mapsto_{\beta}\leavevmode\nobreak\ M\\{N/x\\}$.

A reduction step $\rightarrow_{\rho}$ is the closure under context
$\boldsymbol{\mathsf{C}}$ of $\rho$.

#### CbN and CbV Calculi.

The (pure) Call-by-Name calculus
$\Lambda^{\mathtt{cbn}}=(\Lambda,\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}})$
is the set of terms equipped with the contextual closure of the $\beta$-rule,
as described _e.g._ in [7]. The (pure) Call-by-Value calculus
$\Lambda^{\mathtt{cbv}}=(\Lambda,\mathrel{\rightarrow_{\beta_{v}}})$ is the
same set equipped with the contextual closure of the $\beta_{v}$-rule:
$(\lambda x.M)V\leavevmode\nobreak\ \mapsto_{\beta_{v}}\leavevmode\nobreak\
M\\{V/x\\}\leavevmode\nobreak\ \mbox{ where }V\in\mathcal{V}$, as introduced
by Plotkin [32].

CbN and CbV applied calculi are obtained by associating to operators (the
contextual closure of) a family of rules of the form
$\mathbf{o}(M_{1},\dots,M_{k})\mapsto_{\mathbf{o}}N$. This is a standard way
to enrich $\lambda$-calculus with new computational features, such as
probabilistic choice or output.

#### Weak reductions in CbV.

In CbV $\lambda$-calculus, various restrictions of
$\mathrel{\rightarrow_{\beta_{v}}}$ are studied. If the result of interest are
values, the reduction is _weak_ , that is, it does not reduce in the body of a
function. There are three main weak schemes: left, right and in arbitrary
order. _Left_ contexts $\boldsymbol{\mathsf{L}}$, _right_ contexts
$\boldsymbol{\mathsf{R}}$, and (arbitrary order) _weak_ contexts
$\boldsymbol{\mathsf{W}}$ are defined by

$\boldsymbol{\mathsf{L}}::=\llparenthesis\leavevmode\nobreak\
\rrparenthesis\mid\boldsymbol{\mathsf{L}}M\mid
V\boldsymbol{\mathsf{L}}\quad\quad\boldsymbol{\mathsf{R}}::=\llparenthesis\leavevmode\nobreak\
\rrparenthesis\mid
M\boldsymbol{\mathsf{R}}\mid\boldsymbol{\mathsf{R}}V\quad\quad\boldsymbol{\mathsf{W}}::=\llparenthesis\leavevmode\nobreak\
\rrparenthesis\mid\boldsymbol{\mathsf{W}}M\mid M\boldsymbol{\mathsf{W}}$

Given a rule $\mapsto$ on $\Lambda$, _weak reduction_
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}}}$ is the closure
of $\mapsto$ under context $\boldsymbol{\mathsf{W}}$. A step
$T\mathrel{\rightarrow}S$ is _non-weak_ , noted
$T{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\neg\mathsf{w}\leavevmode\nobreak\
}\,$}\vss}}}}}S$ if it is not weak. Similarly for left
(${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{l}\,$}\vss}}}}}$ and
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{l}\,$}\vss}}}}}$), and right
(${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{r}\,$}\vss}}}}}$ and
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{r}\,$}\vss}}}}}$). Left and
right reduction are _deterministic_. Reduction
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}$
_subsumes_ both. The choice of a redex is non-deterministic, but irrelevant
w.r.t. reaching a value and the number of steps to do so, because
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}$
is RD-diamond (1). We can fire any arbitrary redex in weak position—or _all of
them_ in parallel. A _parallel variant_ can easily be defined.

Weak factorization holds for the three reductions:
$\mathrel{\rightarrow_{\beta_{v}}}^{*}\ \subseteq\
\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}^{*}\cdot\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}^{*}$,
for $\mathsf{s}\in\\{\mathsf{w},\mathsf{l},{\mathsf{r}}\\}$.

##### Head reduction in CbN.

Head reduction [7] is the closure of $\beta$ under head context $\lambda
x_{1}\dots x_{n}.\llparenthesis\leavevmode\nobreak\ \rrparenthesis M_{1}\dots
M_{k}$. _Head normal forms_ (_hnf_), whose set is denoted by $\mathcal{H}$,
are its normal forms. The literature of linear logic often uses a variant of
head context which includes the standard one, and induces exactly the same set
$\mathcal{H}$ of normal forms. Given a rule ${\rho}$, we write
$\mathrel{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{h}$}\vss}}}{}_{\mkern-6.0mu\rho}}$
for its closure under context $\boldsymbol{\mathsf{H}}$.

$\boldsymbol{\mathsf{H}}::=\llparenthesis\leavevmode\nobreak\
\rrparenthesis\mid\lambda
x.\boldsymbol{\mathsf{H}}\mid\boldsymbol{\mathsf{H}}M\qquad(\emph{Head
contexts})$

Head factorization (see [7, Lemma 11.4.6]) and head normalization (see [7,
Thm. 8.3.11]) are classical results, which hold also when the calculus
includes constants, _i.e._ for
$(\Lambda_{\mathcal{O}},\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}})$.

###  4.2 A strategy for finitary normalization in CbV and CbN
$\lambda$-calculus

We revisit normalization for $\lambda$-calculus—uniformly for CbV and CbN —and
define a strategy which is well-suited to be extended to probabilistic
$\lambda$-calculi, and to asymptotic normalization. It supports non-
deterministic head and weak reduction (as needed in the probabilistic case)
and breadth-first evaluation of redexes (as needed to deal with infinitary
reduction graphs).

We call _surface reduction_ weak reduction in CbV and head reduction in CbN,
because they only fire redexes at _depth 0_ , where in CbV the depth of a
redex $R$ is the number of _abstractions_ in which $R$ is nested, and in CbN
is the number of arguments. Normal forms for $\beta$ and $\beta_{v}$ can be
computed by iterating surface reduction in a suitable way, as we show below.

#### Normalizing strategies.

In $\Lambda^{\mathtt{cbn}}$, a paradigmatic normalizing strategy is leftmost-
outermost reduction. It can be described as: first apply head reduction
$\mathrel{\mathrel{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{h}$}\vss}}}{}_{\mkern-6.0mu\beta}}}$
until _hnf_ , and then iterate the process, in left-to-right order.
Normalization in $\Lambda^{\mathtt{cbv}}$ is less established: one can iterate
$\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{l}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}$
left to right (as in Plotkin’s standard reduction [32]), but also iterate
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{r}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}$
right to left, as in Grégoire and Leroy’s implementation [19]. In all cases,
once a head or weak normal form is reached (think of $xM_{1}\dots M_{k}$ in
CbN) no interaction is possible among the subterms $M_{i},\dots,M_{k}$, so in
fact the process can be iterated in any _arbitrary order_.

We define a rather liberal normalizing strategy, _uniformly_ for CbN and CbV,
and _parametrically_ in the choice of surface reduction. Unlike leftmost-
outermost reduction, which is sequential and _inherently depth-first_ , the
_unbiased_ reduction
$\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}$ is non-
deterministic in the choice of the outermost redex, and can support a breadth-
first reduction policy. It persistently performs surface steps, as long as it
is possible, and then iterates the process in the subterms, in arbitrary
order.

######  Definition 4.1 (Unbiased iteration of surface reduction).

Given $(\Lambda_{\mathcal{O}},\rightarrow)$, where $\rightarrow$ is the
contextual closure of a rule $\mathtt{b}\in\\{\beta,\beta_{v}\\}$, let
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\subseteq\,\rightarrow$
be as follows:

${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\,=\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{h}$}\vss}}}\mbox{ if
}\mathtt{b}=\beta\text{ (CbN)
}\quad\quad{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\in\\{{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}},\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{l}$}\vss}}},{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{r}\,$}\vss}}}}}\\}\mbox{ if
}\mathtt{b}=\beta_{v}\mbox{ (CbV) }.$

The relation $\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}\,\subseteq\,\rightarrow$
is inductively defined as follows:

  * •

if $M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}M^{\prime}$ then
$M\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}M^{\prime}$;

  * •

if $M\not\\!{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}$ then
$M\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}M^{\prime}$ is
defined according the rules below.

$(\lambda x.P)\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}(\lambda
x.P^{\prime})P\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P^{\prime}\quad
PQ\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P^{\prime}QP\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P^{\prime}\quad
PQ\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}PQ^{\prime}Q\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}Q^{\prime}\quad\mathbf{o}(P_{1},\dots,P_{i},\dots,P_{k})\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}\mathbf{o}(P_{1},\dots,P^{\prime}_{i},\dots,P_{k})P_{i}\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P^{\prime}_{i}$

The same definition of
$\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}\,\subseteq\,\rightarrow$
still applies if $\rightarrow$ is the contextual closure of
$\mapsto_{\mathtt{b}}\cup\mapsto_{\rho}$, i.e. of the rule
$\mapsto_{\mathtt{b}}$ extended with some other rule $\mapsto_{\rho}$ on
$\Lambda_{\mathcal{O}}$.

We study ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$.
It is RD-diamond (see 1) and is a normalizing strategy for both CbN and CbV
$\lambda$-calculi. Note that in CbN,
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\beta}}}}$
_subsumes_ usual _leftmost-outermost reduction_.

######  Proposition 4.2 (u-Factorization).

Let $\mathtt{b}\in\\{\beta,\beta_{v}\\}$.

$M\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}^{*}N\mbox{
implies }M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}^{*}\cdot{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}^{*}N$ (u-Factorization )

######  Proposition 4.3.

With the same assumptions as in Def. 4.1, let
$\mathtt{b}\in\\{\beta,\beta_{v}\\}$. Then:

  1. 1.

${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$
is RD-diamond.

  2. 2.

${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$
has the same normal forms as
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}$.

  3. 3.

Let $N$ be $\mathtt{b}$-normal.
$M\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}{}^{\mkern-6.0mu*}N$
implies $M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}{}^{\mkern-6.0mu*}N$.

Normalization for both CbN and CbV follows from the points above.

######  Theorem 4.4 (Normalization).

For $\mathtt{b}\in\\{\beta,\beta_{v}\\}$,
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$
is a normalizing strategy for
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}$.

#### Depth-first vs Breadth-first.

Leftmost-outermost reduction fires redexes in a depth-first way. Instead,
$\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}$ evaluates in a
breadth-first style, which is more suitable to deal with possibly infinitary
reductions. For example, in CbN think of
$z(\Delta\Delta)(\Delta_{z}\Delta_{z})$. Leftmost-outermost reduction never
leaves the redex $\Delta\Delta$, while
$\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}$ can also fire
$(\Delta_{z}\Delta_{z})$ yielding $z(z(z\dots))$.

#### A parallel variant.

Once a term is ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}$-normal, the
process can be iterated in any arbitrary order, or in _parallel_. Parallel
(multi-step) reduction
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{//u}\leavevmode\nobreak\
\,$}\vss}}}}}$ is easily defined (Sect. B.1).

##  5 Probabilistic $\lambda$-calculi and Asymptotic Normalization

A standard way to model _probabilistic choice_ (a fair coin) is by means of a
binary operator $\oplus$. We write $M\oplus N$ for $\oplus(M,N)$. Intuitively,
$M\oplus N$ reduces to either $M$ or $N$, _with equal probability_
$\frac{1}{2}$. Reduction is then defined not simply on terms but on (monadic)
structures representing probability distributions over terms. Here we follow
[16], which defines both a CbV and a CbN calculus
$\Lambda_{\oplus}^{\mathtt{cbv}}$ and $\Lambda_{\oplus}^{\mathtt{cbn}}$, where
$\beta$ or $\beta_{v}$ reduction are “as usual”, so if a term contains no
probabilistic operator, it behaves the same as in the usual $\lambda$-calculus
(_i.e._ the extension is _conservative_). Probabilistic reduction instead
needs to be constrained in order to have good properties such as confluence
(see [16], and [12, 26] for a discussion of the issues).

##### Discrete Probability Distributions.

Given a countable set $\Omega$, a function
$\mu\colon\Omega\xrightarrow{}[0,1]$ is a probability _subdistribution_ if
$\|\mu\|:=\sum_{\omega\in\Omega}\mu(\omega)\leq 1$ (a _distribution_ if
$\|\mu\|=1$). Subdistributions allow us to deal with partial results. We write
$\mathcal{D}(\Omega)$ for the set of subdistributions on $\Omega$, equipped
with the pointwise order on functions: $\mu\leq\rho$ if
$\mu(\omega)\leq\rho(\omega)$ for all $\omega\in\Omega$. $\mathcal{D}(\Omega)$
has a bottom element (the subdistribution $\mathbf{0}$) and maximal elements
(all distributions).

##### Multi-distributions.

We use multi-distributions [5] to syntactically represent distributions, A
_multi-distribution_ $\mathtt{m}=[p_{i}M_{i}]_{i\in I}$ on the set of terms
$\Lambda_{\mathcal{O}}$ is a finite multiset of pairs of the form $pM$, with
$p\in]0,1]$, $M\in\Lambda_{\mathcal{O}}$, and $\sum_{i}p_{i}\leq 1$. The set
of all multi-distributions on $\Lambda_{\mathcal{O}}$ is
$\mathcal{M}(\Lambda_{\mathcal{O}})$. The sum of multi-distributions is noted
$+$. The product $q\cdot\mathtt{m}$ of a scalar $q$ and a multi-distribution
$\mathtt{m}$ is defined pointwise $q[p_{i}M_{i}]_{{i\in
I}}:=[(qp_{i})M_{i}]_{{i\in I}}$. We write $[M]$ for $[1M]$.

#### Syntax.

_Terms ( $\Lambda_{\oplus}$)_ and _values_ are as in Sect. 4.1, with the
operator $\mathbf{o}$ being here $\oplus$.

##### Call-by-Value.

The _calculus_ $\Lambda_{\oplus}^{\mathtt{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. 3 and Fig. 3. First, 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, 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:

  1. 1.

The reductions
$\mathrel{\rightarrow_{\beta_{v}}},\rightarrow_{\oplus}\subseteq\Lambda_{\oplus}\times\mathcal{M}(\Lambda_{\oplus})$
are defined in Fig. 3. _Contexts $\boldsymbol{\mathsf{C}}$ and
$\boldsymbol{\mathsf{W}}$_ are as in Sect. 4.1. Note that $\beta_{v}$ is
closed under arbitrary context, while the $\oplus$ rule—probabilistic
choice—is closed under weak contexts $\boldsymbol{\mathsf{W}}$ (no reduction
in the scope of $\lambda$ or $\oplus$). We write
$\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}$
for the closure of $\beta_{v}$ under context $\boldsymbol{\mathsf{W}}$. The
relation $\rightarrow$ is
$\mathrel{\rightarrow_{\beta_{v}}}\cup\rightarrow_{\oplus}$. _Surface
reduction_ is ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\,=\,\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}\cup\rightarrow_{\oplus}$.
A $\rightarrow$-step which is not surface is noted
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}}}$.

  2. 2.

The lifting of a relation
$\rightarrow_{r}\subseteq\Lambda_{\oplus}\times\mathcal{M}(\Lambda_{\oplus})$
to a reduction on multi-distributions is defined in Fig. 3. In particular,
$\rightarrow,\mathrel{\rightarrow_{\beta_{v}}},\rightarrow_{\oplus},{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}},{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}}}$ lift to
$\Rightarrow,\Rightarrow_{\beta_{v}},\Rightarrow_{\oplus},\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\leavevmode\nobreak\
$}\vss}}},\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\leavevmode\nobreak\
$}\vss}}}$.

A term $M$ is $\rightarrow$-normal if there is no $\mathtt{m}$ such that
$M\rightarrow\mathtt{m}$. We also write $M\not\rightarrow$. We denote by
$\mathcal{N}_{v}$ the set of the normal forms of
$\rightarrow\,=\,(\mathrel{\rightarrow_{\beta_{v}}}\cup\rightarrow_{\oplus})$.

$\displaystyle\boldsymbol{\mathsf{C}}\llparenthesis(\lambda
x.M)V\rrparenthesis$
$\displaystyle\mathrel{\rightarrow_{\beta_{v}}}[\boldsymbol{\mathsf{C}}\llparenthesis
M\\{V/x\\}\rrparenthesis]$ $\displaystyle\boldsymbol{\mathsf{W}}\llparenthesis
M\oplus N\rrparenthesis$
$\displaystyle\rightarrow_{\oplus}[\frac{1}{2}\boldsymbol{\mathsf{W}}\llparenthesis
M\rrparenthesis,\frac{1}{2}\boldsymbol{\mathsf{W}}\llparenthesis
N\rrparenthesis]$
$\displaystyle\rightarrow\,:=\,\mathrel{\rightarrow_{\beta_{v}}}\\!\cup$
$\displaystyle\rightarrow_{\oplus}\quad{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\\!:=\\!{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}\\!\cup\rightarrow_{\oplus}$
Figure 1: $\rightarrow$-steps for the calculus
$\Lambda_{\oplus}^{\mathtt{cbv}}$
$\dfrac{}{[M]\Rightarrow[M]}\quad\dfrac{M\rightarrow\mathtt{m}}{[M]\Rightarrow\mathtt{m}}\quad\dfrac{([M_{i}]\Rightarrow\mathtt{m}_{i})_{{i\in
I}}}{[p_{i}M_{i}\mid i\in I]\Rightarrow\sum_{{i\in
I}}{p_{i}\\!\cdot\mathtt{m}_{i}}}$
$\dfrac{M\not\rightarrow}{[M]\rightrightarrows[M]}\quad\dfrac{M\rightarrow\mathtt{m}}{[M]\rightrightarrows\mathtt{m}}\quad\dfrac{([M_{i}]\rightrightarrows\mathtt{m}_{i})_{{i\in
I}}}{[p_{i}M_{i}\mid i\in I]\rightrightarrows\sum_{{i\in
I}}{p_{i}\\!\cdot\mathtt{m}_{i}}}$ Figure 2: Lifting of $\rightarrow$ Figure
3: Full lifting of $\rightarrow$

##### Call-by-Name.

The calculus $\Lambda_{\oplus}^{\mathtt{cbn}}$ is defined in a similar way, by
replacing $\beta_{v}$ with $\beta$ and weak contexts with head contexts
$\boldsymbol{\mathsf{H}}$ (as defined in Sect. 4.1).

##### Observations on multi-distributions.

In CbV, events of interest are the set $\mathcal{V}$ of values and the set
$\mathcal{N}_{v}$ of $\rightarrow$-normal forms (for
$\rightarrow\,=\,\mathrel{\rightarrow_{\beta_{v}}}\cup\rightarrow_{\oplus}$).
Focusing on $\mathcal{N}_{v}$, we can define:

$\mathtt{obs}_{\mathcal{N}}\colon$
$\mathcal{M}(\Lambda_{\oplus})\xrightarrow{}\mathcal{D}(\mathcal{N}_{v})$
$[p_{i}M_{i}]_{i\in I}\mapsto\mu$ where $\forall N\in{\mathcal{N}_{v}},\
\mu(N)=\sum_{{i\in I}}p_{i}\mbox{ s.t. }M_{i}=N$ $\mathtt{obs}_{{pn}}\colon$
$\mathcal{M}(\Lambda_{\oplus})\xrightarrow{}[0,1]$ $[p_{i}M_{i}]_{i\in
I}\mapsto\|\mu\|$

Figure 4: CbV observations on multi-distributions

  * •

$\mathtt{obs}_{\mathcal{N}}$ extracts from $\mathtt{m}=[p_{i}M_{i}]_{{i\in
I}}$ a _subdistribution $\mu$ over normal forms_. For example, if
$\mathtt{m}=[\frac{1}{4}\mathtt{T},\frac{1}{8}\mathtt{T},\frac{1}{4}\mathtt{F},\frac{1}{4}II]$,
$\mathtt{obs}_{\mathcal{N}}(\mathtt{m})$ is the subdistribution
$\\{\mathtt{T}^{\frac{3}{8}},\mathtt{F}^{\frac{1}{4}}\\}$, _i.e._
$\mu(\mathtt{T})=\frac{3}{8}$, $\mu(\mathtt{F})=\frac{1}{4}$.

  * •

$\mathtt{obs}_{{pn}}$ observes the probability that $\mathtt{m}$ has reached a
normal form. For example, with $\mathtt{m}$ as above,
$\mathtt{obs}_{{pn}}(\mathtt{m})=\frac{5}{8}$.

In CbN, events of interest are the set of normal forms (w.r.t.
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}\cup\rightarrow_{\oplus}$),
and the set $\mathcal{H}$ of head normal forms. The corresponding observations
are defined in the obvious way.

###  5.1 Asymptotic Normalization for Probabilistic $\lambda$-Calculi

We can now revisit the probabilistic calculi $\Lambda_{\oplus}^{\mathtt{cbv}}$
and $\Lambda_{\oplus}^{\mathtt{cbn}}$ as QARS, and define for them an
asymptotically normalizing strategy. We develop explicitly only the CbV case,
but similar definitions and results hold for CbN, taking into account that
$\mathrel{\rightarrow_{\beta_{v}}}$ is replaced by
$\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\beta}}}$ and surface reduction
is $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{h}$}\vss}}}$. Method and proofs
are exactly the same.

The QARS framework allows us to express and analyze the asymptotic behaviour
of the calculus
$\Lambda_{\oplus}^{\mathtt{cbv}}=(\mathcal{M}(\Lambda_{\oplus}),\Rightarrow)$.
Here we are interested in
$\mathtt{obs}_{\mathcal{N}}:\mathcal{M}(\Lambda_{\oplus})\xrightarrow{}\mathcal{D}(\mathcal{N})$
as defined in Fig. 4. It is immediate that
$\mathtt{m}\rightarrow\mathtt{m}^{\prime}$ implies
$\mathtt{obs}_{\mathcal{N}}(\mathtt{m})\leq\mathtt{obs}_{\mathcal{N}}(\mathtt{m}^{\prime})$.
So, $\big{(}\Lambda_{\oplus}^{\mathtt{cbv}},\mathtt{obs}_{\mathcal{N}}\big{)}$
is a QARS. We prove (Thm. 5.7) that $\Lambda_{\oplus}^{\mathtt{cbv}}$
satisfies the following properties: (1) the result
$\llbracket{\mathtt{m}}\rrbracket$ of computing $\mathtt{m}$ is well defined;
(2) there exists a strategy that is guaranteed to produce
$\llbracket{\mathtt{m}}\rrbracket$.

##### Beyond the surface.

We define a reduction $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\subseteq\Lambda_{\oplus}\times\mathcal{M}(\Lambda_{\oplus})$ which
performs surface steps
(${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}=\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}\cup\rightarrow_{\oplus}$,
see Sect. 5) as much as possible, and then iterates the process on the
subterms. There are two subtleties here. First:
$M\not{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}$ if and only if
($M\not\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}$
and $M\not\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\oplus}}}}}$).
Second: an occurrence of $\oplus$-redex can only be fired when it is a surface
redex. By keeping this into account, Def. 4.1 updates as follows. We denote by
$\mathcal{S}$ the set of
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}$-normal forms.

######  Definition 5.1 (Unbiased evaluation
$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$, $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ ).

  * •

The relation $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\subseteq\Lambda_{\oplus}\times\mathcal{M}(\Lambda_{\oplus})$ is
defined by the following rules, depending if $M\not\in\mathcal{S}$ or
$M\in\mathcal{S}$. The relation
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}$
is as in Def. 4.1.

$M\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\ \mathtt{m}M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\
\mathtt{m}\quad\quad M\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}[M^{\prime}]\lx@proof@logical@and
M\not{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}M^{\prime}$

  * •

$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}},\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\
$}\vss}}}\subseteq\mathcal{M}(\Lambda_{\oplus})\times\mathcal{M}(\Lambda_{\oplus})$
are respectively the lifting and full lifting of
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ (Figs. 3 and 3).

Clearly, $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\subseteq\rightarrow$, and moreover $\rightarrow$ and
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ have the _same normal forms_.

######  Remark 5.2.

Notice that $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\ \not=\ {\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}\cup\rightarrow_{\oplus}$,
which is not diamond, check $(\Delta\oplus\Delta\Delta)(x(Iz))$.

######  Remark 5.3.

$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ is $\mathtt{obs}_{\mathcal{N}}$-complete, but not
$\mathtt{obs}_{\mathcal{N}}$-normalizing for $\Rightarrow$. Indeed, the
sequence
$\mathtt{m}=[II\oplus\Delta\Delta]\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}[\frac{1}{2}II,\frac{1}{2}\Delta\Delta]\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}[\frac{1}{2}II,\frac{1}{2}\Delta\Delta]\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\dots$ never fires $II$. The solution is to move to
$\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$, which forces all non-normal terms to reduce.
Note that $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ does not factorize $\Rightarrow$.

We show that $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ is an $\mathtt{obs}_{\mathcal{N}}$-normalizing
strategy for $\Rightarrow$. The pillars of our construction are
e-factorization and weighted Random Descent. The former holds for
$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$, the latter for $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$.

######  Proposition 4 (Factorization and
$\mathtt{obs}_{\mathcal{N}}$-neutrality).

  1. 1.

_e -factorization:_ $\mathtt{m}\Rightarrow^{*}\mathtt{n}$ implies
$\mathtt{m}\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}^{*}\cdot\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{e}\leavevmode\nobreak\
$}\vss}}}^{*}\mathtt{n}$.

  2. 2.

_$\mathtt{obs}_{\mathcal{N}}$ -neutrality:_
$\mathtt{m}\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{e}\leavevmode\nobreak\
$}\vss}}}\mathtt{n}$ implies
$\mathtt{obs}_{\mathcal{N}}(\mathtt{m})=\mathtt{obs}_{\mathcal{N}}(\mathtt{n})$.

######  Proposition 5 (Diamond).

$\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ is $\mathtt{obs}_{\mathcal{N}}$-diamond.

We are now ready to prove that, in
$\big{(}\Lambda_{\oplus}^{\mathtt{cbv}},\mathtt{obs}_{\mathcal{N}}\big{)}$,
the reduction $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\subseteq\Rightarrow$ (_i.e._ , the full lifting
of $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$) is guaranteed to compute the best possible result from each
$\mathtt{m}\in\mathcal{M}(\Lambda_{\oplus})$.

##### Asymptotic Completeness.

We have that $\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ is asymptotically complete for $\Rightarrow$, because it satisfies
the conditions of Thm. 3.4 (by Prop. 4).

######  Lemma 5.4.

If $\mathtt{m}\Rightarrow\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{\mathtt{r}}$ then
$\mathtt{m}\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\ \boldsymbol{\mathtt{r}}$.

In turn, $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ is asymptotically complete for
$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ (immediate). So via Lemma 5.4 we have:

######  Theorem 5.5.

$\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ is asymptotically complete for $\Rightarrow$:
if $\mathtt{m}\Rightarrow\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{\mathtt{r}}$ then
$\mathtt{m}\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{\mathtt{s}}$ and
$\boldsymbol{\mathtt{r}}\leq\boldsymbol{\mathtt{s}}$.

##### Unique Result.

All $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$-sequences from $\mathtt{m}$ converge to the
same limit, by Prop. 5 and 3.

######  Theorem 5.6.

$\mathtt{Lim}_{\mathtt{obs}_{\mathcal{N}}}(\mathtt{m},\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}})$ contains a unique element.

##### Asymptotic Normalization.

By Prop. 2, the main result follows from Thm. 5.5 and 5.6.

######  Theorem 5.7 (Main, probabilistic CbV).

For each $\mathtt{m}\in\mathcal{M}(\Lambda_{\oplus})$:

  1. 1.

$\llbracket{\mathtt{m}}\rrbracket$ is defined;

  2. 2.

$\mathtt{m}\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{\mathtt{r}}$ if and only if
$\boldsymbol{\mathtt{r}}=\llbracket{\mathtt{m}}\rrbracket$.

Hence $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$ is an _$\mathtt{obs}_{\mathcal{N}}$
-normalizing strategy_ for $\Rightarrow$ (see Remark 3.3).

Some simple examples will help to see how the normalizing strategy works, and
how it differs from surface reduction.

######  Example 5.8.

Recall that $\beta_{v}$-reduction is unrestricted, so for example $M=\lambda
z.(Iz)\mathrel{\rightarrow_{\beta_{v}}}\lambda z.z$. Instead, $\lambda
z.(Iz)\not{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}$, because
surface reduction cannot fire under abstraction. So _surface reduction is not
a complete strategy_ w.r.t. $\beta_{v}$-normal forms.

A direct consequence is that surface reduction is not informative about
normalization, as it produces “false positive”. For example, $N=\lambda
z.\Delta\Delta$ is diverging w.r.t. $\beta_{v}$-reduction, but it is a surface
normal form. Let us now incept probability (with the terms $M$ and $N$ as
above).

  1. 1.

Let $R=(\lambda x.M\oplus xx)(\lambda x.M\oplus xx)$. Then
$[R]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}[M\oplus
R]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\
$}\vss}}}[\frac{1}{2}M,\frac{1}{2}R]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}[\frac{1}{2}I,\frac{1}{2}M\oplus
R]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\
$}\vss}}}[\frac{1}{2}I,\frac{1}{4}M,\frac{1}{4}R]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\cdots$. At the limit, $R$ converges with
probability $1$ to $I$, as wanted.

  2. 2.

The term $S=(\lambda x.N\oplus xx)(\lambda x.N\oplus xx)$ converges to normal
form with probability $0$. One can easily check that
$[S]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\mathbf{0}$.

  3. 3.

The term $S^{\prime}=(\lambda x.(N\oplus I)\oplus xx)(\lambda x.(N\oplus
I)\oplus xx)$ converges with probability $\frac{1}{2}$ to the normal form $I$.
One can easily check that
$[S^{\prime}]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\\{I^{\frac{1}{2}}\\}$.

  4. 4.

Notice that from $S^{\prime}$, the reduction
$\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}$ (instead of $\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}$) would admit also reduction sequences which
produces no normal form, for example
$S^{\prime}\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}^{*}[\frac{1}{4}N,\frac{1}{2}I,S^{\prime}]\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}[\frac{1}{4}N,\frac{1}{4}I,\frac{1}{2}S^{\prime}]\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}[\frac{1}{4}N,\frac{1}{4}I,\frac{1}{2}S^{\prime}]\cdots$. By
persistently reducing only $N$, we have
$[S^{\prime}]\mathrel{\mathop{\Rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
$}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\ \mathbf{0}$.

######  Example 5.9.

One can easily build probabilistic terms with a more interesting behaviour
than those in Example 5.8. First, observe that for $F=\lambda x.I$ (encoding
the boolean _false_), we have that $(\lambda
z.FF)\mathrel{\rightarrow_{\beta_{v}}}F$. Now let $U=\lambda xy.\big{(}y\oplus
xx(\lambda z.yy)\big{)}$ and consider the term $UUF$, which converges with
probability $1$ to $F$. Indeed
$[UUF]\mathrel{\mathop{\rightrightarrows}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{e}\leavevmode\nobreak\
\leavevmode\nobreak\ $}\vss}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\\{F^{1}\\}$. In contrast, surface reduction converges to a distribution over
_countably many different surface normal forms_ , since each iteration
produces a new snf: $\frac{1}{2}F,\frac{1}{4}\lambda z.FF,\frac{1}{8}\lambda
z.(\lambda z.FF)(\lambda z.FF),...$.

##  6 Asymptotic Normalization: More Case Studies

Our method applies—uniformly—to the other examples in Sect. 1.1. In this
section we consider a CbV $\lambda$-calculus extended with an output operator.
For the sake of a compact presentation, we take as output not a string, but
simply an integer (think of it as a string on a single character). Albeit
simple, this case study allows us to illustrate the subtleties related to
limits with output calculi, and the use of our method. In a similar way, one
can revisit Böhm Trees as the limit of a specific asymptotic strategy—we leave
this to Appendix D.2.

####  $\lambda$-calculus with output: the payoff calculus.

$\langle
n:\boldsymbol{\mathsf{W}}\llparenthesis\mathtt{tick}.P\rrparenthesis\rangle\leavevmode\nobreak\
{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}}\leavevmode\nobreak\
\langle n+1:\boldsymbol{\mathsf{W}}\llparenthesis P\rrparenthesis\rangle$
$\langle n:M\rangle{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}\langle
n:M^{\prime}\rangle M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}M^{\prime}$
$\langle n:M\rangle\mathrel{\rightarrow_{\beta_{v}}}\langle
n:M^{\prime}\rangle M\mathrel{\rightarrow_{\beta_{v}}}M^{\prime}$

Figure 5: Payoff reductions
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}},{\mathrel{\rightarrow_{\beta_{v}}}},{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}}\subseteq(\mathbb{N}\times\Lambda_{\mathtt{tick}})$

$\displaystyle\langle
0:M\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\\!\langle 0:M^{\prime}\rangle M\mapsto_{\beta_{v}}M^{\prime}\qquad\langle
0:M\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\\!\langle 1:M^{\prime}\rangle
M\mapsto_{\mathtt{tick}}M^{\prime}\qquad\langle
0:V\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\\!\langle 0:V\rangle$ $\displaystyle\langle
0:P_{1}P_{2}\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\\!\langle k_{1}+k_{2}:P_{1}P_{2}\rangle\lx@proof@logical@and\langle
0:P_{1}\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\langle k_{1}:P_{1}\rangle\langle
0:P_{2}\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\langle k_{2}:P_{2}\rangle\qquad\langle
n:M\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\\!\langle n+k:M^{\prime}\rangle\lx@proof@logical@and n>0\langle
0:M\rangle{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\
}\langle k:M^{\prime}\rangle$

Figure 6: Parallel weak reduction in the payoff calculus

The payoff $\lambda$-calculus (called cost $\lambda$-calculus in [24, 18])
extends the $\lambda$-calculus with a ticking operation. Its intrinsic purpose
is to facilitate an intensional analysis of programs, endowing terms with
constructs to perform cost analysis.

Let $\Lambda_{\mathtt{tick}}$ denote the set of $\lambda$-terms extended with
a unary operator $\mathtt{tick}$. The elements of the payoff calculus are
pairs $\mathtt{m}=\langle n:M\rangle$ of a counter $n\in\mathbb{N}$ and a
closed term $M\in\Lambda_{\mathtt{tick}}$. Intuitively, the term
$\mathtt{tick}(P)$ increments the counter by $1$, and continues as $P$.
Following [18], in $(\mathbb{N}\times\Lambda_{\mathtt{tick}})$ we define the
full reduction $\rightarrow$ and the weak reduction
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$ as follows:

$\rightarrow\;\coloneqq\;\mathrel{\rightarrow_{\beta_{v}}}\cup\;{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}}$
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\;\coloneqq\;{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}\cup\;{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}}$

where ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}}$,$\mathrel{\rightarrow_{\beta_{v}}}$,
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}\subseteq(\mathbb{N}\times\Lambda_{\mathtt{tick}})$
are given in Fig. 6. Note that weak effectful reduction
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}}$
is the closure under weak context $\boldsymbol{\mathsf{W}}$ of the rule
$(\mathtt{tick}.P)\mapsto_{\mathtt{tick}}P$ (effects are only allowed under
weak context). Left and right reductions
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{l}$}\vss}}}$ and
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{r}\,$}\vss}}}}}$ can be defined
similarly.

The pair $\big{(}(\Lambda_{\mathtt{tick}},\rightarrow),\mathtt{obs}\big{)}$ is
a QARS where we observe the payoff, _i.e._ $\mathtt{obs}\langle n:M\rangle=n$.
We now prove (using Thm. 3.4) that
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}={\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}\cup\;{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{tick}}}}}$
is asymptotically complete for $\rightarrow$.

######  Lemma 6.1.

For every pair $\mathtt{m}=\langle n:M\rangle$, $\mathtt{m}\
\rightarrow\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\ \boldsymbol{n}$ implies
$\mathtt{m}\ {{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{n}$, because

  * •

$\mathsf{w}$-factorization of $\rightarrow$: if $\mathtt{m}\ \rightarrow^{*}\
\mathtt{n}$ then $\mathtt{m}\
{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}^{*}\cdot{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{w}\,\,$}\vss}}}}}^{*}\
\mathtt{n}$;

  * •

$\mathtt{obs}$-neutrality : if $\mathtt{m}\
{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{w}\,\,$}\vss}}}}}\
\mathtt{m}^{\prime}$ then
$\mathtt{obs}{(\mathtt{m})}=\mathtt{obs}{(\mathtt{m}^{\prime})}$.

Weak reduction ${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$ however does
_not_ have a unique limit, as Example 6.2 below illustrates. An unsatisfactory
solution would be to fix a deterministic evaluation order (left or right, as
in point 1. below), making the limit easy to predict but also rather
_arbitrary_.

######  Example 6.2.

Consider $M=(\Delta\Delta)(\Delta_{{\surd}}\Delta_{{\surd}})$, where
$\Delta_{{\surd}}=\lambda x.\mathtt{tick}(xx)$, and let $\mathtt{m}=\langle
0:M\rangle$.

  1. 1.

By fixing left (resp. right) evaluation,
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m},\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{l}$}\vss}}})=\\{0\\}$ (resp.
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m},{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{r}\,$}\vss}}}}})=\\{\infty\\}$).

  2. 2.

By choosing a redex in unspecified order, we have an uncountable number of
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$-sequences,
leading to
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m},{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}})=\\{0,1,\dots\,\infty\\}=\mathbb{N}^{\infty}$.

A way out is to proceed somehow similarly to Sect. 5.1. If we examine more
closely the set of limits associated with
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$, we realize
that
$\mathtt{Lim}_{\mathtt{obs}}{(\mathtt{m},{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}})}$ does have
a greatest element. Thus $\llbracket{\mathtt{m}}\rrbracket$ can naturally be
defined as the best possible payoff from $\mathtt{m}$. We prove that parallel
reduction ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}$
(given in Fig. 6) is a (_multistep_) strategy which is guaranteed to compute
$\mathtt{m}$. Indeed, it is easy to verify that
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}$ is
asymptotically complete for
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$. By
composing with Lemma 6.1 we have that
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}$ is
asymptotically complete for $\rightarrow$ (point 1. below).

######  Lemma 6.3.

  1. 1.

_Asymptotic Completeness._ If $\langle
k:M\rangle\;{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{n}$ then $\langle
k:M\rangle{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\boldsymbol{n}^{\prime}$ and $\boldsymbol{n}\leq\boldsymbol{n}^{\prime}$. That
is, ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}$ is
asymptotically complete for
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$ and (by
Lemma 6.1) for $\rightarrow$.

  2. 2.

_Unique Limit._ The reduction
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}$ is
deterministic.

Since (by points 1. and 2. in Lemma 6.3) both conditions of Prop. 2 are
verified, we have:

######  Theorem 6.4 (Main, payoff).

Given the QARS
$\big{(}(\mathbb{N}\times\Lambda_{\mathtt{tick}},\rightarrow),\mathtt{obs}\big{)}$,
for each pair $\mathtt{m}=\langle k:M\rangle$,
$\llbracket{\mathtt{m}}\rrbracket$ is defined, and
$\mathtt{m}{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}\mkern-2.0mu{}^{\infty}\leavevmode\nobreak\
\llbracket{\mathtt{m}}\rrbracket$. Hence, multistep reduction
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\textsc{//}}\mathsf{w}\,$}\vss}}}}}$ is
asymptotically normalizing for
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$ and for
$\rightarrow$ (Remark 3.3).

####  $\lambda$-calculus with outputs.

The calculus in Example 1.2 can be formalized in a similar way to the payoff
calculus. We can define $\mathtt{obs}(\langle s:M\rangle)\,=\,s$. As already
noted, ${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$ is not
confluent, and given a pair $\mathtt{m}$, the set of limits may contain
uncountably many different elements. Still, the reduction has interesting
properties, which appear when looking not directly at the string $s$ itself,
but at its length $|s|$. This way, one can transfer the results from the
payoff calculus.

##  7 Conclusions

We propose a method to study completeness and normalization when the result of
computation is _asymptotic_. Our techniques abstract from details specific to
the calculus under study—they are therefore of _general_ application. The
robustness of the method is witnessed by its ability to deal with different
settings and _different notions of asymptotic computation_.

The application to probabilistic $\lambda$-calculus yields a result of
independent interest: a theorem of _asymptotic normalization_ , both for CbV
and CbN probabilistic $\lambda$-calculi. Remarkably, the same definitions and
proof techniques apply _uniformly_ to both. In the paper we prefer to give the
details for the CbV calculus, which is arguably a more natural one in presence
of effects.

#### Related work.

QARS, proposed in [14] in the setting of probabilistic rewriting, refine
Ariola and Blom’s ARSI [4]. The techniques in Sect. 3 are an original
contribution of this paper. Our Thm. 3.4 generalizes an ARS technique for
finitary normalization (studied in [2, 35, 21]) to asymptotic computation,
refining it for arbitrary observations.

The study of reduction strategies in a probabilistic $\lambda$-calculus where
the notion of reduction is general—rather than simply fixing a deterministic
reduction—started in [16] (CbV and CbN) and [28] (CbN). Asymptotic
completeness is there established only for _surface_ normal forms (values in
closed CbV, hnf’s in CbN). Strategies that are complete for _full normal
forms_ (which we treat and solve here) are more difficult to study than head
or weak reduction, especially in the CbV setting. The question of defining
such a strategy was left open in [16, Remark 27]. We stress that our technique
would also yield a simpler proof of the results in [16, 28], where confluence
is used to establish that a greatest limit exists. The (non-trivial) proofs
there use properties that are _specific_ to probability distributions. The
method we propose here avoids technical issues, it is much simpler, and it is
general, in that it can be applied to other settings.

Finally, we mention that forgoing confluence and studying uniqueness of normal
forms via a complete subreduction is a route already employed in the context
of infinitary $\lambda$-calculi [9, 8].

## References

  * [1] Samson Abramsky and C.-H. Luke Ong.  Full Abstraction in the Lazy Lambda Calculus.  Inf. Comput., 105(2):159–267, 1993.  doi:10.1006/inco.1993.1044.
  * [2] Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri.  Factorization and Normalization, Essentially.  In Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, volume 11893 of Lecture Notes in Computer Science, pages 159–180. Springer, 2019.  doi:10.1007/978-3-030-34175-6_9.
  * [3] Roberto M. Amadio and Pierre-Louis Curien.  Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 1998.  URL: https://dblp.org/rec/bib/books/daglib/0093287, doi:10.1017/CBO9780511983504.
  * [4] Zena M. Ariola and Stefan Blom.  Skew confluence and the lambda calculus with letrec.  Annals of Pure and Applied Logic, 117(1):95–168, 2002.  doi:10.1016/S0168-0072(01)00104-X.
  * [5] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada.  On probabilistic term rewriting.  Sci. Comput. Program., 185, 2020.  doi:10.1016/j.scico.2019.102338.
  * [6] Franz Baader and Tobias Nipkow.  Term Rewriting and All That. Cambridge University Press, 1998.  doi:10.1017/CBO9781139172752.
  * [7] Hendrik Pieter Barendregt.  The Lambda Calculus – Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics.  North-Holland, 1984.
  * [8] Henk Barendregt and Jan Willem Klop.  Applications of infinitary lambda calculus.  Inf. Comput., 207(5):559–582, 2009.  doi:10.1016/j.ic.2008.09.003.
  * [9] Alessandro Berarducci and Benedetto Intrigila.  Church-Rosser $\lambda$-theories, infinite $\lambda$-calculus and consistency problems.  In W. Hodges, M. Hyland, and et. al., editors, Logic: From Foundations to Applications (European Logic Colloquium), pages 33–58. Oxford Sci. Publ., 1996.
  * [10] Gianluca Curzi and Michele Pagani.  The Benefit of Being Non-Lazy in Probabilistic $\lambda$-calculus: Applicative Bisimulation is Fully Abstract for Non-Lazy Probabilistic Call-by-Name.  In LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 327–340. ACM, 2020.  doi:10.1145/3373718.3394806.
  * [11] Roel C. de Vrijer.  Conditional linearization.  Indagationes Mathematicae, 10(1):145–159, 1999.  doi:10.1016/S0019-3577(99)80012-3.
  * [12] Ugo de’Liguoro and Adolfo Piperno.  Non Deterministic Extensions of Untyped Lambda-Calculus.  Inf. Comput., 122(2):149–177, 1995.  doi:10.1006/inco.1995.1145.
  * [13] Claudia Faggian.  Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms.  In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, volume 131 of LIPIcs, pages 19:1–19:25. Schloss Dagstuhl, 2019.  doi:10.4230/LIPIcs.FSCD.2019.19.
  * [14] Claudia Faggian.  Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms.  Log. Methods Comput. Sci., vol. 18, issue 2, 2022.
  * [15] Claudia Faggian and Giulio Guerrieri.  Strategies for Asymptotic Normalization (long version).  CoRR, 2022.  URL: http://arxiv.org/abs/2204.08772, arXiv:2204.08772.
  * [16] 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, pages 1–13. IEEE, 2019.  doi:10.1109/LICS.2019.8785699.
  * [17] Francesco Gavazzo.  Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects.  PhD thesis, Università di Bologna, Italy, 2019.  URL: https://tel.archives-ouvertes.fr/tel-02386201.
  * [18] Francesco Gavazzo and Claudia Faggian.  A Relational Theory of Monadic Rewriting Systems, Part I.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1–14. IEEE, 2021.  doi:10.1109/LICS52264.2021.9470633.
  * [19] Benjamin Grégoire and Xavier Leroy.  A compiled implementation of strong reduction.  In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), pages 235–246. ACM, 2002.  doi:10.1145/581478.581501.
  * [20] J. Roger Hindley and Jonathan P. Seldin.  Introduction to Combinators and Lambda-Calculus.  Cambridge University Press, 1986.
  * [21] 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. Schloss Dagstuhl, 2015.  doi:10.4230/LIPIcs.RTA.2015.209.
  * [22] J. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries.  Transfinite Reductions in Orthogonal Term Rewriting Systems.  Inf. Comput., 119(1):18–38, 1995.  doi:10.1006/inco.1995.1075.
  * [23] J. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries.  Infinitary lambda calculus.  Theoretical Computer Science, 175(1):93–125, 1997.  doi:10.1016/S0304-3975(96)00171-5.
  * [24] Ugo Dal Lago and Francesco Gavazzo.  Effectful Normal Form Bisimulation.  In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 263–292. Springer, 2019\.  doi:10.1007/978-3-030-17184-1_10.
  * [25] Ugo Dal Lago and Simone Martini.  The weak lambda calculus as a reasonable machine.  Theor. Comput. Sci., 398(1-3):32–50, 2008.
  * [26] 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.
  * [27] 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.
  * [28] Thomas Leventis.  A deterministic rewrite system for the probabilistic $\lambda$-calculus.  Mathematical Structures in Computer Science, 29(10):1479–1512, 2019\.  doi:10.1017/S0960129519000045.
  * [29] Jean-Jacques Lévy.  Réductions correctes et optimales dans le lambda calcul.  PhD thesis, Université Paris 7, 1978.  URL: http://pauillac.inria.fr/~levy/pubs/74phd-cycle3.pdf.
  * [30] Gerd Mitschke.  The Standardization Theorem for $\lambda$-Calculus.  Mathematical Logic Quarterly, 25(1-2):29–31, 1979.
  * [31] Maxwell H. A. Newman.  On Theories with a Combinatorial Definition of Equivalence.  Annals of Mathematics, 43(2), 1942.
  * [32] 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.
  * [33] Terese.  Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2003.
  * [34] Vincent van Oostrom.  Random Descent.  In Term Rewriting and Applications, 18th International Conference, RTA 2007, volume 4533 of Lecture Notes in Computer Science, pages 314–328. Springer, 2007.  doi:10.1007/978-3-540-73449-9_24.
  * [35] Vincent van Oostrom and Yoshihito Toyama.  Normalisation by Random Descent.  In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, volume 52 of LIPIcs, pages 32:1–32:18. Schloss Dagstuhl, 2016.  doi:10.4230/LIPIcs.FSCD.2016.32.

## APPENDIX

We include some proofs and details that have been omitted in the article.

#### Some more examples.

$\mathtt{Lim}_{\mathtt{obs}}(t,\rightarrow)$ may have a lub but not a
maximum—similarly to $\mathbb{N}$.

######  Example .1 (Sect. 2, QARS).

We revisit Example 2.7, now allowing full reduction
$\mathrel{\rightarrow_{\beta_{v}}}$. Let $\mathtt{obs}_{p}(\langle
s:M\rangle)=s$ if $M\in\mathcal{V}$, $\bot$ otherwise. The pair
$\mathtt{m}\,=\,\langle\epsilon:(\lambda z.I)(\lambda
z.\Delta_{0}\Delta_{0})\rangle$ has countably many limits, but not a greatest
one, because all strings in
$\mathtt{Lim}_{\mathtt{obs}_{p}}(\mathtt{m},\mathrel{\rightarrow_{\beta_{v}}})$
are finite.

######  Example .2 (Sect. 3.1, Weighted Random Descent, strings).

By fine tuning the notion of observation, one can establish non trivial
properties of the calculus $\mathtt{Out}_{\mathbb{A}}$ in Example 2.7 (here
reduction is CbV and weak), such as the following, which is also an example of
weighted RD. If $\mathtt{m}=\langle s:M\rangle$ has a terminating computation
$\mathtt{m}\ {{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}^{*}\ \langle
s^{\prime}:V\rangle$ for some value $V$, then _all maximal
${{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{w}\,\,$}\vss}}}}}}$-sequences
from $\mathtt{m}$ terminate_ (in the same number of steps) and all end exactly
with _the same value $V$ and a string of the same length as $s^{\prime}$_.

#### Surface reduction.

Everywhere in the appendix, we fix surface reduction to be as follows.

  * •

CbN ($\mathtt{b}=\beta$): $\mathsf{s}=\mathsf{h}$ (the contextual closure of
$\boldsymbol{\mathsf{H}}$).

  * •

CbV ($\mathtt{b}=\beta_{v}$): $\mathsf{s}=\mathsf{w}$ (the contextual closure
of $\boldsymbol{\mathsf{W}}$).

##  Appendix A Properties of surface normal forms

We will use extensively the following easy fact.

######  Lemma A.1 (Surface normal forms).

$M$ is $\mathsf{w}$-normal (resp. $\mathsf{h}$-normal) if there is no redex
$R$ such that $M=\boldsymbol{\mathsf{W}}\llparenthesis R\rrparenthesis$ (resp.
$M=\boldsymbol{\mathsf{H}}\llparenthesis R\rrparenthesis$).

  1. 1.

CbV. Assume $M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle{\neg\mathsf{w}\leavevmode\nobreak\
}\,$}\vss}}}{}_{\mkern-6.0mu{\beta_{v}}}}}M^{\prime}$. $M$ is
$\mathsf{w}$-normal $\Leftrightarrow$ $M^{\prime}$ is $\mathsf{w}$-normal.

  2. 2.

CbN. Assume $M\mathrel{\mathrel{\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{h}\leavevmode\nobreak\
$}\vss}}}{}_{\mkern-6.0mu\beta}}}M^{\prime}$. $M$ is $\mathsf{h}$-normal
$\Leftrightarrow$ $M^{\prime}$ is $\mathsf{h}$-normal.

##  Appendix B  Sect. 4.2: properties of unbiased reduction

With the same assumptions as in Def. 4.1, let
$(\mathtt{b},\mathsf{s})\in\\{(\beta,\mathsf{h}),(\beta_{v},\mathsf{w})\\}$.
The relation ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$
is as in Def. 4.1. The relation
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$ is the complement of
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$,
_i.e._ ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}\ =\
\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}\smallsetminus{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$.

We start with a basic remark.

######  Remark B.1.

Fixed
$(\mathtt{b},\mathsf{s})\in\\{(\beta,\mathsf{h}),(\beta_{v},\mathsf{w})\\}$,
we have ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\subseteq{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$.
Hence, ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}\subseteq{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}}}$.

#### Diamonds.

######  Lemma B.2 (RD-diamond).

With the same assumptions as in Def. 4.1, let
$(\mathtt{b},\mathsf{s})\in\\{(\beta,\mathsf{h}),(\beta_{v},\mathsf{w})\\}$.
${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}$
has the RD-diamond property of 1.

######  Proof B.3.

We already know that ${\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}$
($\mathsf{s}\in\\{\mathsf{h},\mathsf{w}\\}$) has the $RD$-diamond property. If
$M$ has $\mathsf{s}$-redexes, then
$M_{1}\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}$}\vss}}}}}M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}M_{2}$, and the
claim holds. Otherwise, if $M$ has no $\mathsf{s}$-redexes, then $M$, $M_{1}$
and $M_{2}$ have the same shape. We have either $M=\lambda x.P$ or $M=PQ$.

  * •

Case $M=\lambda x.P$. Then $M_{1}=\lambda x.P_{1}$, $M_{2}=\lambda x.P_{2}$,
and $P_{1}\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}P\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P_{2}$, and we
conclude by _i.h._.

  * •

Case $M=PQ$. Three cases are possible:

    * –

$P_{1}Q\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}PQ\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P_{2}Q$, and we
conclude by _i.h._.

    * –

$PQ_{1}\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}PQ\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}PQ_{2}$, and we
conclude by _i.h._.

    * –

$P^{\prime}Q\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}PQ\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}PQ^{\prime}$,
where $P\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}P^{\prime}$ and
$Q\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}Q^{\prime}$.
Then we conclude
$P^{\prime}Q{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}PQ^{\prime}\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}PQ^{\prime}$.

  * •

Case $M=\mathbf{o}(P_{1}\dots P_{k})$.

    * –

If $\mathbf{o}(\dots
P_{i}^{\prime}\dots)\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}\mathbf{o}(\dots
P_{i}\dots)\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}\mathbf{o}(\dots
P_{i}^{\prime\prime}\dots)$, we conclude by _i.h._.

    * –

If $\mathbf{o}(\dots P_{i}^{\prime}\dots
P_{j}\dots)\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}\mathbf{o}(\dots
P_{i}\dots
P_{j}\dots)\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}}}}\mathbf{o}(\dots
P_{i}\dots P_{j}^{\prime}\dots)$, then
$\mathbf{o}(\dots P_{i}^{\prime}\dots
P_{j}\dots){\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}}}\mathbf{o}(\dots
P_{i}^{\prime}\dots
P_{j}^{\prime}\dots)\mathrel{{\mathrel{\mathop{\leftarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}$}\vss}}}}}\mathbf{o}(\dots
P_{i}\dots P_{j}^{\prime}\dots)$

#### Factorization.

We only sketch the proof of u-factorization, which is straightforward to
establish from $\mathsf{s}$-Factorization, using Mitschke argument [30].

######  Theorem B.4 (u-Factorization).

With the same assumptions as in Def. 4.1, let
$(\mathtt{b},\mathsf{s})\in\\{(\beta,\mathsf{h}),(\beta_{v},\mathsf{w})\\}$.
Then:

$M\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}^{*}N\mbox{
implies }M{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{u}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}^{*}\cdot{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}^{*}N$ (u-Factorization )

######  Proof B.5.

By induction on the term $N$. From
$M\mathrel{\mathrel{\rightarrow{}_{\mkern-6.0mu\mathtt{b}}}}^{*}N$, by
$\mathsf{s}$-Factorization, we have that

$M\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}}^{*}U\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}}^{*}N.$

Since $\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}}$-steps
preserve the shape of terms, all terms in the sequence
$U\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}}^{*}N$
have the same shape.

  * •

If $U$ contains any $\mathsf{s}$-redex, so does every term in the sequence
$U\mathrel{{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\mathsf{s}\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}}^{*}N$
by Lemma A.1, and so $U{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}^{*}N$. Hence the claim.

  * •

Assume $U$ contains no $\mathsf{s}$-redex. We examine the possible shape of
$N$, and conclude by _i.h._.

#### Normalization.

######  Lemma B.6 (Normal forms).

If $U{\mathrel{\,\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\neg\textsc{u}\leavevmode\nobreak\
\,$}\vss}}}{}_{\mkern-6.0mu{\mathtt{b}}}}}N$, then $N$ is not
$\mathtt{b}$-normal.

######  Proof B.7.

By induction on the shape of $U$, observing that $N$ and $U$ have the same
shape.

  * •

Assume $U$ is not $\mathsf{s}$-normal. Then (by Lemma A.1) $N$ is not
$\mathsf{s}$-normal, and a fortiori not $\mathtt{b}$-normal.

  * •

Assume $U$ is $\mathsf{s}$-normal. We examine its shape.

    * –

Case $U=U_{1}U_{2}$ and $N=N_{1}N_{2}$. Then either (i)