# Probabilistic Rewriting: on Normalization, Termination, and Unique Normal
Forms

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

###### Abstract

While a mature body of work supports the study of rewriting systems, abstract
tools for Probabilistic Rewriting are still limited. In this paper we study
the question of _uniqueness of the result_ (unique limit distribution), and
develop a set of proof techniques to analyze and compare _reduction
strategies_. The goal is to have tools to support the _operational_ analysis
of _probabilistic_ calculi (such as probabilistic lambda-calculi) whose
evaluation is also non-deterministic, in the sense that different reductions
are possible.

##  1 Introduction

_Rewriting Theory_ [41] is a foundational theory of computing. Its impact
extends to both the theoretical side of computer science, and the development
of programming languages. A clear example of both aspects is the paradigmatic
term rewriting system, $\lambda$-calculus, which is also the foundation of
functional programming. _Abstract Rewriting Systems (ARS)_ are the general
theory which captures the common substratum of rewriting theory, independently
of the particular structure of the objects. It studies properties of terms
transformations, such as normalization, termination, unique normal form, and
the relations among them. Such results are a powerful set of tools which can
be used when we study the computational and operational properties of any
calculus or programming language. Furthermore, the theory provides tools to
study and compare strategies, which become extremely important when a system
_may_ have reductions leading to a normal form, but _not necessarily_. Here we
need to know: is there a strategy which is guaranteed to lead to a normal
form, if any exists (_normalizing_ strategies)? Which strategies diverge if at
all possible (_perpetual_ strategies)?

_Probabilistic Computation_ models uncertainty. Probabilistic models such as
automata [36], Turing machines [39], and the $\lambda$-calculus [38] exist
since long. The pervasive role it is assuming in areas as diverse as robotics,
machine learning, natural language processing, has stimulated the research on
probabilistic programming languages, including functional languages [28, 37,
33] whose development is increasingly active. A typical programming language
supports at least discrete distributions by providing a probabilistic
construct which models sampling from a distribution. This is also the most
concrete way to endow the $\lambda$-calculus with probabilistic choice [14,
11, 17]. Within the vast research on models of probabilistic systems, we wish
to mention that probabilistic rewriting is the explicit base of PMaude [1], a
language for specifying probabilistic concurrent systems.

_Probabilistic Rewriting._ Somehow surprisingly, while a large and mature body
of work supports the study of rewriting systems – even infinitary ones [13,
25] – work on the abstract theory of _probabilistic_ rewriting systems is
still sparse. The notion of _Probabilistic_ Abstract Reduction Systems (PARS)
has been introduced by Bournez and Kirchner in [6], and then extended in [5]
to account for non-determinism. Recent work [8, 16, 26, 4] shows an increased
research interest. The key element in _probabilistic_ rewriting is that even
when the probability that a term leads to a normal form is $1$ (_almost sure
termination_), that degree of certitude is typically not reached in any finite
number of steps, but it appears as a limit. Think of a rewrite rule (as in
Fig. 3) which rewrites $c$ to either the value T or $c$, with equal
probability $1/2$. We write this
$c\rightarrow\\{c^{1/2},{\texttt{T}}^{1/2}\\}$. After $n$ steps, $c$ reduces
to T with probability $\frac{1}{2}+\frac{1}{2^{2}}+\dots+\frac{1}{2^{n}}$.
Only at the limit this computation terminates with probability $1$ .

The most well-developed literature on PARS is concerned with methods to prove
almost sure termination, see e.g. [5, 20, 4] (this interest matches the fact
that there is a growing body of methods to establish AST [2, 21, 23, 31]).
However, considering rewrite rules subject to probabilities opens numerous
other questions, which motivate our investigation.

We study a rewrite relation which describes the global evolution of a
probabilistic system, for example a probabilistic program $P$. The _result_ of
the computation is a probability distribution $\beta$ over all the possible
output of $P$. The intuition (see [28]) is that the program $P$ is executed,
and random choices are made by sampling. This process defines a distribution
$\beta$ over the various outputs that the program can produce. We write this
$P\xRightarrow{\infty}\beta$.

What happens if the _evaluation_ of a term $P$ is also _non-deterministic_?
Remember that non-determinism arises naturally in the $\lambda$-calculus,
because a term may have several redexes. This aspect has practical relevance
to programming. Together with the fact that the result of a terminating
computation is unique, (independently from the evaluation choices), it is key
to the inherent parallelism of functional programs (see _e.g._ [30]).

Assume program $P$ generates a distribution over booleans
$\\{{\texttt{T}}^{\frac{1}{16}},{\texttt{F}}^{\frac{15}{16}}\\}$; it is
desirable that the distribution which is computed is unique: it _only depends
on the ”input” (the problem)_ , not on the way the computational steps are
performed.

When assuming non-deterministic evaluation, several questions on PARS arise
naturally. For example: (1.) when –and in which sense– is the result unique?
(naively, if $P\xRightarrow{\infty}\alpha$ and $P\xRightarrow{\infty}\beta$,
is $\alpha=\beta$?) (2.) Do all rewrite sequences from the same term have the
same probability to reach a result? (3.) If not, does there exist a strategy
to find a result with greatest probability?

Such questions are relevant to the theory and to the practice of computing. We
believe that to study them, we can advantageously adapt techniques from
Rewrite Theory. However, we _cannot assume that standard properties of ARS
hold for PARS._ The game-changer is that termination appears as a _limit_. In
Sec. 4.2.3 we show that a well-known ARS property, Newman’s Lemma, does not
hold for PARS. This is not surprising; indeed, Newman’s Lemma is known not to
hold in general for infinitary rewriting [24, 27]. Still, our counter-example
points out that moving from ARS to PARS is non-trivial. There are two main
issues: we need to find the _right formulation_ and the _right proof
technique_. It seems then especially important to have a collection of proof
methods which apply well to PARS.

##### Content and contributions.

Probability is concerned with _asymptotic_ behaviour: what happens not after a
finite number $n$ of steps, but _when $n$ tends to infinity_. In this paper we
focus on the asymptotic behaviour of rewrite sequences _with respect to normal
forms_ – normal form being the most standard notion of result in rewriting. We
study computational properties such as (1.),(2.),(3.) above. We do so with the
point of view of ARS, aiming for properties which _hold independently_ of the
specific nature of the rewritten objects; the purpose is to have tools which
apply to any probabilistic rewriting system.

After motivating and introducing our formalism for PARS (Sec. 2 and 3), in
Sec. 4 we formalize the notion of limit distribution, and of well-defined
result. Since in a PARS each term has different possible reduction sequences
(each sequence leading to a possibly different limit distribution), to each
term is naturally associated _a set of limit distributions_. To study when a
PARS has a well-defined result is the main focus of the paper.

Recall a property which is crucial to the computational interpretation of a
system such as the $\lambda$-calculus: if a term has a normal form, it is
unique – meaning that the result of the computation is _well-defined_. With
this in mind, we investigate in the probabilistic setting an analogue of the
ARS notions of _Unique Normal Form ( UN)_, and the possibility or necessity to
reach a result: _Normalization ( WN), Termination (SN)_. We provide methods
and criteria to establish these properties, and we uncover relations between
them. Specific contributions are the following.

  * •

We propose an analogue of UN for PARS. The question was already studied in
[16] for PARS which are AST, but the solution there does not extend to the
general case.

  * •

We investigate the classical ARS method to prove UN via _confluence_ ; we
uncover that subtle aspects appear when dealing with a notion of result as a
limit. We do prove an analogue of “confluence implies UN” for PARS – however
the proof is not simply an adaptation of the standard techniques, due to the
fact that the set of limit distributions is –in general– infinite, and it is
not guaranteed to have maximal elements (think of $[0,1[$ which has a sup, but
not a max). We need to exploit the structure of $\mathbb{R}$.

We then provide a set of proof techniques to support the analysis of PARS
_reduction strategies_. To do so, we extend to the probabilistic setting a
method which was introduced for ARS by Van Oostrom [42], which is based on
Newman’s property of Random Descent [32, 42, 43] (see Sec. 1.2). The Random
Descent method turns out to be well-suited to PARS, providing a useful _family
of tools_. In analogy to their counterpart in [42], we generalize in a
quantitative way the notions of Random Descent (which becomes
$\mathtt{obs}$-RD) and of being _better_ (which become
$\mathtt{obs}\mbox{-better}$); both properties are here parametric with
respect to a chosen event of interest.

  * •

$\mathtt{obs}$-RD entails that all rewrite sequences from a term lead to the
_same result_ , in the _same expected number of steps_ (the average of number
of steps, weighted w.r.t. probability).

  * •

$\mathtt{obs}\mbox{-better}$ offers a method to compare strategies (“strategy
$\mathcal{S}$ is always better than strategy $\mathcal{T}$”) w.r.t. the
_probability_ of reaching a result and the _expected time_ to reach a result.
It provides a sufficient criterion to establish that a strategy is
_normalizing_ (resp. _perpetual_) _i.e._ the strategy is guaranteed to lead to
a result with maximal (resp. minimal) probability.

A significant technical feature (inherited from [42]) is that both notions of
$\mathtt{obs}$-RD and $\mathtt{obs}\mbox{-better}$ come with a
characterization via a _local condition_ (in ARS, a typical example of a local
vs global condition is local confluence vs confluence).

We apply these methods to study a probabilistic $\lambda$-calculus, namely a
Weak Call-by-Value calculus. A larger example of application to probabilistic
$\lambda$-calculus is [19] – whose developments rely also on the abstract
results presented here; we illustrate this in Sec. 9.

######  Remark (On the term _Random_ Descent).

Please note that in [32], the term _Random_ refers to non-determinism (in the
choice of the redex), _not to randomized_ choice.

###  1.1 Probabilistic $\lambda$-calculus and (Non-)Unique Result

Rewrite theory provides numerous tools to study uniqueness of normal forms, as
well as techniques to study and compare strategies. This is not the case in
the probabilistic setting. Perhaps a reason is that when extending the
$\lambda$-calculus with a choice operator, confluence is lost, as was observed
early [12]; we illustrate it in Example 1 and 2, which is adapted from [12,
11]. The way to deal with this issue in probabilistic $\lambda$-calculi (e.g.
[14, 11, 17]) has been to _fix a deterministic reduction strategy_ , typically
“leftmost-outermost”. To fix a strategy is not satisfactory, neither for the
theory nor the practice of computing. To understand why this matters, recall
for example that confluence of the $\lambda$-calculus is what makes functional
programs inherently parallel: every sub-expression can be evaluated in
parallel, still, we can reason on a program using a deterministic sequential
model, because the result of the computation is independent of the evaluation
order (we refer to [30], and to Harper’s text “Parallelism is not Concurrency”
for discussion on _deterministic_ parallelism, and how it differs from
concurrency). Let us see what happens in the probabilistic case.

######  Example 1 (Confluence failure).

Let us consider the untyped $\lambda$-calculus extended with a binary operator
$\oplus$ which models probabilistic choice. Here $\oplus$ is just flipping a
fair coin: $M\oplus N$ reduces to either $M$ or $N$ with equal probability
$1/2$; we write this as $M\oplus
N\rightarrow\\{M^{\frac{1}{2}},N^{\frac{1}{2}}\\}$.

Consider the term $PQ$, where $P=(\lambda x.x)(\lambda
x.x\mathtt{~{}XOR~{}}x)$ and $Q=({\texttt{T}}\oplus{\texttt{F}})$; here
$\mathtt{~{}XOR~{}}$ is the standard constructs for the exclusive
$\mathtt{OR}$, T and F are terms which code the booleans.

  * •

If we evaluate $P$ and $Q$ independently, from $P$ we obtain $\lambda
x.(x\mathtt{~{}XOR~{}}x)$, while from $Q$ we have either T or F, with equal
probability $1/2$. By composing the partial results, we obtain
$\\{({\texttt{T}}\mathtt{~{}XOR~{}}{\texttt{T}})^{\frac{1}{2}},({\texttt{F}}\mathtt{~{}XOR~{}}{\texttt{F}})^{\frac{1}{2}}\\}$,
and therefore $\\{{\texttt{F}}^{1}\\}$.

  * •

If we evaluate $PQ$ sequentially, in a standard leftmost-outermost fashion,
$PQ$ reduces to $(\lambda x.x\mathtt{~{}XOR~{}}x)Q$ which reduces to
$({\texttt{T}}\oplus{\texttt{F}})\mathtt{~{}XOR~{}}({\texttt{T}}\oplus{\texttt{F}})$
and eventually to
$\\{{\texttt{T}}^{\frac{1}{2}},{\texttt{F}}^{\frac{1}{2}}\\}$.

######  Example 2.

The situation becomes even more complex if we examine also the possibility of
diverging; try the same experiment on the term $PR$, with $P$ as above, and
$R=({\texttt{T}}\oplus{\texttt{F}})\oplus\Delta\Delta$ (where $\Delta=\lambda
x.xx$). Proceeding as before, we now obtain either
$\\{{\texttt{F}}^{\frac{1}{2}}\\}$ or
$\\{{\texttt{T}}^{\frac{1}{8}},{\texttt{F}}^{\frac{1}{8}}\\}$.

We do not need to loose the features of $\lambda$-calculus in the
_probabilistic_ setting. In fact, while some care is needed, determinism of
the evaluation _can be relaxed_ without giving up uniqueness of the result:
the calculus we introduce in Sec. 7.2 is an example (we relax determinism to
RD); we fully develop this direction in further work [19]. To be able to do
so, we _need abstract tools and proof techniques_ to analyze _probabilistic_
rewriting. The same need for theoretical tools holds, more in general,
whenever we desire to have a probabilistic language which allows for
_deterministic parallel reduction_.

In this paper we focus on _uniqueness of the result_ , rather than confluence,
which is an important and sufficient, but not necessary property.

###  1.2 Other key notions

##### Local vs global conditions.

To work _locally_ means to reduce a test problem which is global, _i.e._ ,
quantified over _all rewrite sequences_ from a term, to local properties
(quantified only over _one-step reductions_ from the term), thus reducing the
space of search when testing.

The paradigmatic example of a global property is confluence (CR):
$b~{}{}^{*}\leftarrow a\rightarrow^{*}c$ $\Rightarrow$ $\exists d$ s.t.
$b\rightarrow^{*}d~{}{}^{*}\leftarrow c$. Its global nature makes it difficult
to establish. A standard way to factorize the problem is: (1.) prove
termination and (2.) prove _local_ confluence (WCR): $b\leftarrow a\rightarrow
c$ $\Rightarrow$ $\exists d$ s.t. $b\rightarrow^{*}d~{}{}^{*}\leftarrow c$).
This is exactly _Newman’s lemma: Termination + WCR $\Rightarrow$ CR._ The
beauty of Newman’s lemma is that a global property (CR) is guaranteed by a
local property (WCR).

Locality is also the strength and beauty of the Random Descent method. While
Newman’s lemma fails in a probabilistic setting, RD methods adapt well.

##### Random Descent.

Newman’s Random Descent (RD) [32] is an ARS property which guarantees that
normalization suffices to establish both termination and uniqueness of normal
forms. Precisely, if an ARS has random descent, paths to a normal form do not
need to be unique, but they have _unique length_. In its essence: _if a normal
form exists, all rewrite sequences lead to it, and all have the _same length_
111or, in Newman’s original terminology: the end-form is reached by _random
descent_ (whenever $x\rightarrow^{k}y$ and $x\rightarrow^{n}u$ with $u$ in
normal form, all maximal reductions from $y$ have length $n-k$ and end in
$u$)._. While only few systems directly verify it, RD is a powerful ARS tool;
a typical use in the literature is to prove that _a strategy_ has RD, to
conclude that it is _normalizing_. A well-known property which implies RD is a
form of
diamond:“$\leftarrow\cdot\rightarrow~{}\subseteq~{}(\rightarrow\cdot\leftarrow)~{}\cup~{}="$.

In [42] Von Oostrom defines a characterization of RD by means of a _local_
property and proposes RD as a uniform method to (locally) compare strategies
for normalization and minimality (resp. perpetuality and maximality). [43]
extends the method and abstracts the notion of length into a notion of
measure. In Sec. 7 and 8 we develop similar methods in a _probabilistic_
setting. The analogous of _length_ , is the _expected number of steps_ (Sec.
7.1).

##### Probabilistic Weak $\lambda$-calculus.

A notable example of system which satisfies RD is the pure untyped
$\lambda$-calculus endowed with call-by-value (CbV) weak evaluation. _Weak_
[22, 7] means that reduction does not evaluate function bodies (_i.e._ the
scope of $\lambda$-abstractions). We recall that weak CbV is the basis of the
ML/CAML family of functional languages (and of most probabilistic functional
languages). Because of RD, weak CbV $\lambda$-calculus has _striking
properties_ (see e.g. [9] for an account). First, if a term $M$ has a normal
form $N$, any rewrite sequence will find it; second, the number $n$ of steps
such that $M\rightarrow^{n}N$ is always the same.

In Sec. 7.2, we study a probabilistic extension of weak CbV,
$\Lambda_{\oplus}^{\texttt{weak}}$. We show that it has analogous properties
to its classical counterpart: all rewrite sequences converge to the same
result, in the same _expected_ number of steps.

###  1.3 Related work

First, let us observe that there is a vast literature on probabilistic
transition systems, however objectives and therefore questions and tools are
different than those of PARS. A similar distinction exist between abstract
rewrite systems (ARS) and transition systems. Here we discuss related work in
the context of PARS [5, 6].

We are not aware of any work which investigates _normalizing strategies_ (or
_normalization_ in general, rather than termination). Instead, _confluence_ in
probabilistic rewriting has already drawn interesting work. A notion of
confluence for a probabilistic rewrite system defined over a
$\lambda$-calculus is studied in [15, 10]; in both case, the probabilistic
behavior corresponds to measurement in a quantum system. The work more closely
related to our goals is [16]. It studies confluence of non-deterministic PARS
in the case of finitary termination (being finitary is the reason why a
Newman’s Lemma holds), and in the case of AST. As we observe in Sec. 4.2.2,
their notion of unique limit distribution (if $\alpha,\beta$ are limits, then
$\alpha=\beta$), while _simple_ , it is _not_ an analogue of UN for _general_
PARS. We extend the analysis beyond AST, to the general case, which arises
naturally when considering _untyped_ probabilistic $\lambda$-calculus. On
confluence, we also mention [26], whose results however do not cover _non-
deterministic PARS_ ; the probability of the limit distribution is
concentrated in a single element, in the spirit of Las Vegas Algorithms. [26]
revisits results from [6], while we are in the non-deterministic framework of
[5].

The way we define the _evolution of PARS_ , via the one-step relation
$\mathrel{\rightrightarrows}$, follows the approach in [8], which also
contains an embryo of the current work (a form of diamond property); the other
results and developments are novel. A technical difference with [8] is that
for the formalism to be general, a refinement is necessary (see Sec. 2.5); the
issue was first pointed out in [16]. Our refinement is a variant of the one
introduced (for the same reasons) in [4]; there normal forms are discarded –
because the authors are only interested in the probability of termination–
while we are interested in a more qualitative analysis of the result. [4]
demonstrates the equivalence with the approach in [5].

Finally, to better understand the asymptotic properties of PARS, and separate
the properties which really depend on probability from those which are
concerned with infinitary limits, we use the notion of QARS – which we have
recently developed (it does not appear in [18]). Quantitative Abstract Rewrite
Systems (QARS) refine Ariola and Blom’s notion of Abstract Rewrite Systems
with Information content (ARSI) [3]; there, to the ARS is associate a _partial
order_ which expresses a comparison between the ”information content” of the
elements. The completion is done “on the fly” –internally to the ARSI– via
ideal completion, an approach which would not suit probability distributions.
Indeed, ARSI are targeted to express partial normal forms in the sense of
Boehm trees. Let us give a concrete example that show the difference: a
confluent ARSI has unique infinite normal forms - the analogue result is (in
general) not true for QARS.

##  2 Probabilistic Abstract Rewriting System

We assume the reader familiar with the basic notions of rewrite theory (such
as Ch. 1 of [41]), and of _discrete_ probability theory. We review the basic
language of both. We then recall the definition of _probabilistic abstract
rewrite system_ from [6, 5] –here denoted pars– and explain on examples how a
system described by a pars evolves. This will motivate the formalism which we
present in Sec. 3.

###  2.1 Basics on ARS

An _abstract rewrite system (ARS)_ is a pair $\mathcal{C}=(C,\rightarrow)$
consisting of a set $C$ and a binary relation $\rightarrow$ on $C$ (called
reduction) whose pairs are written $t\to s$ and called _steps_ ;
$\rightarrow^{*}$ (resp. $\rightarrow^{=}$) denotes the transitive reflexive
(resp. reflexive) closure of $\rightarrow$. We write $c\not\rightarrow$ if
there is no $u$ such that $c\rightarrow u$; in this case, $c$ is a normal
form. $\scalebox{0.6}[1.0]{NF}_{\mathcal{C}}$ denotes the set of the normal
forms of $\mathcal{C}$. If $c\rightarrow^{*}u$ and
$u\in\scalebox{0.6}[1.0]{NF}_{\mathcal{C}}$, we say $c$ has a normal form $u$.

A relation $\rightarrow$ is _deterministic_ if for each $t\in C$ there is at
most one $s\in C$ such that $t\rightarrow s$.

##### Unique Normal Form

$\mathcal{C}$ has the property of unique normal form (_with respect to
reduction_) (UN) if $\forall c\in C,\forall
u,v\in\scalebox{0.6}[1.0]{NF}_{\mathcal{C}},\big{(}c\rightarrow^{*}u~{}\&~{}c\rightarrow^{*}v\Rightarrow
u=v\big{)}$. $\mathcal{C}$ has the normal form property (NFP) if $\forall
b,c\in C,\forall
u\in\scalebox{0.6}[1.0]{NF}_{\mathcal{C}},\big{(}b\rightarrow^{*}c~{}\&~{}b\rightarrow^{*}u\Rightarrow
c\rightarrow^{*}u\big{)}$. Clearly, NFP implies UN (and confluence implies
NFP).

##### Normalization and Termination

The fact that an ARS has unique normal forms implies neither that all terms
have a normal form, nor that if a term has a normal form, each rewrite
sequence converges to it. A term $c$ is terminating222Please observe that the
_terminology is community-dependent_. In logic: Strong Normalization, Weak
Normalization, Church-Rosser (hence the _standard abbreviations_ SN, WN, CR).
In computer science: Termination, Normalization, Confluence. (aka strongly
normalizing, SN), if it has no infinite sequence $c\rightarrow
c_{1}\rightarrow c_{2}...$; it is  normalizing (aka weakly normalizing, WN),
if it has a normal form. These are all important properties to establish about
an ARS, as it is important to have a rewrite strategy which finds a normal
form, if it exists.

###  2.2 Basics on Probabilities

The intuition is that random phenomena are observed by means of experiments
(running a probabilistic program is such an experiment); each experiment
results in an outcome. The collection of all possible outcomes is represented
by a set, called the sample space $\Omega$. When the sample space $\Omega$ is
_countable_ , the theory is simple. A _discrete probability space_ is given by
a pair $(\Omega,\mu)$, where $\Omega$ is a _countable_ set, and $\mu$ is a
discrete probability distribution on $\Omega$, _i.e._ a function
$\mu:\Omega\to[0,1]$ such that $\sum_{\omega\in\Omega}\mu(\omega)=1$. A
probability measure is assigned to any subset $A\subseteq\Omega$ as
$\mu(\mathcal{A})=\sum_{\omega\in A}\mu(\omega)$. In the language of
probabilists, a subset of $\Omega$ is called an _event_.

######  Example 3 (Die).

Consider tossing a die once. The space of possible outcomes is the set
$\Omega=\\{1,2,3,4,5,6\\}$. The probability $\mu$ of each outcome is $1/6$.
The event _“result is odd”_ is the subset $A=\\{1,3,5\\}$, whose probability
is $\mu(A)=1/2$.

Each _function_ $F:\Omega\to\Delta$, where $\Delta$ is another countable set,
induces a probability distribution $\mu^{F}$ on $\Delta$ by composition:
$\mu^{F}(d):=\mu(F^{-1}(d))$ _i.e._ $\mu\\{\omega\in\Omega:F(\omega)=d\\}$.
Thus $(\Delta,\mu^{F})$ is also a probability space. In the language of
probability theory, $F$ is called a _discrete random variable_ on
$(\Omega,\mu)$. The expected value (also called the expectation or mean) of a
random variable $F$ is the weighted (in proportion to probability) average of
the possible values of $F$. Assume $F:\Omega\to\Delta$ discrete and
$g:\Delta\to\mathbb{R}$ a non-negative function, then
$E(g(F))=\sum_{d\in\Delta}g(d)\mu_{F}(d)$.

###  2.3 (Sub)distributions: operations and notation

We need the notion of subdistribution to account for partial results, and for
unsuccessful computation. Given a countable set $\Omega$, and a function
$\mu:\Omega\to[0,1]$, we define $\|\mu\|:=\sum_{\omega\in\Omega}\mu(\omega)$.
The function $\mu$ is a probability subdistribution if $\|\mu\|\leq 1$. We
write $\mathsf{Dst}(\Omega)$ for the set of subdistributions on $\Omega$. The
_support_ of $\mu$ is the set
$\mathtt{Supp}(\mu)=\\{a\in\Omega\mid\mu(a)>0\\}$. $\mathsf{Dst^{F}}(\Omega)$
denotes the set of $\mu\in\mathsf{Dst}(\Omega)$ with _finite support_ , and
$\bm{0}$ indicates the subdistribution of empty support.

$\mathsf{Dst}(\Omega)$ is equipped with the pointwise order relation of
functions : $\mu\leq\rho$ if $\mu(a)\leq\rho(a)$ for each $a\in\Omega$.
Multiplication for a scalar ($p\cdot\mu$) and sum ($\mathtt{s}+\rho$) are
defined as usual, $(p\cdot\mu)(a)=p\cdot\mu(a)$,
$(\mathtt{s}+\rho)(a)=\mathtt{s}(a)+\rho(a)$, provided $p\in[0,1]$, and
$\|\mathtt{s}\|+\|\rho\|\leq 1$.

######  Notation 4 (Representation).

We represent a (sub)distribution by explicitly indicating the support, and (as
superscript) the probability assigned to each element by $\mu$. We write
$\mu=\\{a_{0}^{p_{0}},\dots,a_{n}^{p_{n}}\\}$ if
$\mu(a_{0})=p_{0},\dots,\mu(a_{n})=p_{n}$ and $\mu(a_{j})=0$ otherwise.

###  2.4 Probabilistic Abstract Rewrite Systems (pars)

$r_{0}:c\rightarrow\\{c^{1/2},{\texttt{T}}^{1/2}\\}$ L/.style= edge
label=node[left,blue,font=]#1 , for tree= grow=0,reversed, parent
anchor=east,child anchor=west, edge=line cap=round,outer sep=+1pt, l sep=8mm
[c, [c, L=1/2, [c, L=1/4,[…],[T]] [T, L=1/4]] [T, L=1/2] ]  Figure 1: Almost
Sure Termination P/.style= edge label=node[left,blue,font=]#1 , for tree=
grow=0,reversed, parent anchor=east,child anchor=west, edge=line
cap=round,outer sep=+1pt, l sep=8mm [2, [1,P=1/2[0,P=1/4],[2 $\cdots$,P=1/4]],
[3,P=1/2[2 $\cdots$,P=1/4],[4 $\cdots$,P=1/4]] ]  Figure 2: Deterministic pars
P/.style= edge label=node[left,blue,font=]#1 , for tree= grow=0,reversed,
parent anchor=east,child anchor=west, edge=line cap=round,outer sep=+1pt, l
sep=8mm [2, [1,P=1/2[0,P=1/4],[2,P=1/4,[1 $\cdots$,P=1/8],[3
$\cdots$,P=1/8]]], [3,P=1/2[2,P=1/4,[stop,P=1/4]],[4 $\cdots$,P=1/4]] ]
Figure 3: Non-deterministic
pars

A _probabilistic abstract rewrite system ( pars)_ is a pair $(A,\rightarrow)$
of a countable set $A$ and a relation
${\rightarrow}\subseteq{A\times\mathsf{Dst^{F}}(A)}$ such that for each
$(a,\beta)\in{\rightarrow}$, $\|\beta\|=1$. We write $a\rightarrow\beta$ for
$(a,\beta)\in{\rightarrow}$ and we call it a _rewrite step_ , or a
_reduction_. An element $a\in A$ is in _normal form_ if there is no $\beta$
with $a\rightarrow\beta$. We denote by $\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$
the set of the normal forms of $\mathcal{A}$ (or simply  NF when $\mathcal{A}$
is clear). A pars is deterministic if, for all $a$, there is at most one
$\beta$ with $a\rightarrow\beta$.

######  Remark.

The intuition behind $a\rightarrow\beta$ is that the rewrite step
$a\rightarrow b$ ($b\in A$) has probability $\beta(b)$. The total probability
given by the sum of all steps $a\rightarrow b$ is $1$.

##### Probabilistic vs Non-deterministic.

It is important to have clear the distinction between probabilistic choice
(which _globally happens with certitude_) and non-deterministic choice (which
leads to different distributions of outcomes.) Let us discuss some examples.

######  Example 5 (A deterministic pars).

Fig. 3 shows a simple random walk over $\mathbb{N}$, which describes a gambler
starting with $2$ points and playing a game where every time he either gains
$1$ point with probablity $1/2$ or looses $1$ point with probability $1/2$.
This system is encoded by the following pars on $\mathbb{N}$:
$n+1\rightarrow\\{n^{1/2},(n+2)^{1/2}\\}$. Such a pars is _deterministic_ ,
because for every element, at most one choice applies. Note that $0$ is a
normal form.

######  Example 6 (A non-deterministic pars).

Assume now (Fig. 3) that the gambler of Example 5 is also given the
possibility to stop at any time. The two choices are here encoded as follows:
$n+1\rightarrow\\{n^{1/2},(n+2)^{1/2}\\},\quad
n+1\rightarrow\\{\texttt{stop}^{1}\\}$.

###  2.5 Evolution of a system described by a pars.

We now need to explain how a system which is described by a pars evolves. An
option is to follow the stochastic evolution of a single run, _a sampling at a
time_ , as we have done in Fig. 3, 3, and 3. This is the approach in [5],
where non-determinism is solved by the use of policies. Here we follow a
different (though equivalent) way. We describe the possible states of the
system, at a certain time $t$, _globally_ , essentially as a distribution on
the space of all terms. The evolution of the system is then a sequence of such
states. Since all the probabilistic choices are taken together, a global step
happens with probability $1$; the only source of non-determinism in the
evolution of the system is choice. This global approach allows us to deal with
non-determinism by using techniques which have been developed in Rewrite
Theory. Before introducing the formal definitions, we informally examine some
examples, and point out why some care is needed.

$r_{0}:a\rightarrow\\{a^{1/2},{\texttt{T}}^{1/2}\\},~{}~{}r_{1}:a\rightarrow\\{a^{1/2},{\texttt{F}}^{1/2}\\}$
L/.style= edge label=node[midway,left, font=]#1 , for tree= grow=0,reversed,
parent anchor=east,child anchor=west, edge=-¿,outer sep=+1pt, l sep=6mm
[$\\{a^{1}\\}$, [$\boldsymbol{\\{a^{1/2},{\texttt{T}}^{1/2}\\}}$, blue,
L=$r_{0}$ [$\boldsymbol{\\{a^{1/4},{\texttt{T}}^{3/4}\\}}$ $\cdots$, blue,
L=$r_{0}$] [$\\{a^{1/4},{\texttt{T}}^{1/2},{\texttt{F}}^{1/4}\\}$, $\cdots$,
L=$r_{1}$, ]] [$\\{a^{1/2},{\texttt{F}}^{1/2}\\}$, L=$r_{1}$,
[$\\{a^{1/4},{\texttt{T}}^{1/4},{\texttt{F}}^{1/2}\\}$ $\cdots$, L=$r_{0}$ ]
[$\\{a^{1/4},{\texttt{F}}^{3/4}\\}$$\cdots$, L=$r_{1}$, ]] ]  Figure 4: Ex.8
(non-deterministic pars)
$r_{0}:a\rightarrow\\{a^{1/2},{\texttt{T}}^{1/2}\\},~{}~{}r_{2}:a\rightarrow\\{a^{1}\\}$
L/.style= edge label=node[midway,left, font=]#1 , for tree= grow=0,reversed,
parent anchor=east,child anchor=west, edge=-¿,outer sep=+1pt, l sep=6mm
[$\\{a^{1}\\}$, [$\boldsymbol{\\{a^{1/2},{\texttt{T}}^{1/2}\\}}$, blue,
L=$r_{0}$ [$\boldsymbol{\\{a^{1/4},{\texttt{T}}^{3/4}\\}}$ $\cdots$,blue,
L=$r_{0}$] [$\\{a^{1/2},{\texttt{T}}^{1/2}\\}$$\cdots$, L=$r_{2}$]]
[$\\{a^{1}\\}$, red, L=$r_{2}$ [$\\{a^{1/2},{\texttt{T}}^{1/2}\\}$ $\cdots$,
L=$r_{0}$ ] [$\\{a^{1}\\}$ $\cdots$, red, L=$r_{2}$]] ]  Figure 5: Ex.9 (non-
deterministic pars)

######  Example 7 (Fig.3 continued).

The pars described by the rule
$r_{0}:c\rightarrow\\{c^{1/2},{\texttt{T}}^{1/2}\\}$ (in Fig. 3) evolves as
follows:
$\\{c\\},\\{c^{1/2},{\texttt{T}}^{1/2}\\},\\{c^{1/4},{\texttt{T}}^{3/4}\\},\dots$.

######  Example 8 (Fig.5).

Fig. 5 illustrates the possible evolutions of a non-deterministic system which
has two rules: $r_{0}:a\rightarrow\\{a^{1/2},{\texttt{T}}^{1/2}\\}$ and
$r_{1}:a\rightarrow\\{a^{1/2},{\texttt{F}}^{1/2}\\}$. The arrows are annotated
with the chosen rule.

######  Example 9 (Fig.5).

Fig. 5 illustrates the possible evolutions of a system with rules
$r_{0}:a\rightarrow\\{a^{1/2},{\texttt{T}}^{1/2}\\}$ and
$r_{2}:a\rightarrow\\{a^{1}\\}$.

If we look at Fig. 3, we observe that after two steps, there are _two distinct
occurrences_ of the element 2, which live in _two different runs_ of the
program: the run 2.1.2, and the run 2.3.2. There are two possible transitions
from each $2$. The next transition only depends on the fact of having 2, not
on the run in which 2 occurs: its history is only a way to distinguish the
occurrence. For this reason, given a pars $(A,\rightarrow)$, we keep track of
_different occurrences_ of an element $a\in A$, but not necessarily of the
history. Next section formalizes these ideas.

##### Markov Decision Processes.

To understand our distinction between occurrences of $a\in A$ in different
paths, it is helpful to think how a system is described in the framework of
Markov Decision Processes (MDP) [35]. Indeed, in the same way as ARS
correspond to transition systems, pars correspond to probabilistic
transitions. Let us regard a pars step $r:a\rightarrow\beta$ as a
probabilistic transition ($r$ is here a name for the rule). Let assume
$a_{0}\in\mathcal{A}$ is an initial state. In the setting of MDP, a typical
element (called _sample path_) of the sample space $\Omega$ is a sequence
$\omega=(a_{0},r_{0},a_{1},r_{1}...)$ where $r_{0}:a_{0}\rightarrow\beta_{1}$
is a rule, $a_{1}\in\mathtt{Supp}(\beta_{1})$ an element,
$r_{1}:a_{1}\rightarrow\beta_{1}$, and so on. The index
$t=0,1,2,\dots,n,\dots$ is interpreted as _time_. On $\Omega$ various random
variables are defined; for example, $X_{t}=a_{t}$, which represents the state
at time $t$. The sequence $\langle X_{t}\rangle$ is called a stochastic
process.

##  3 A Formalism for Probabilistic Rewriting

This section presents a formalism to describe the global evolution of a system
described by a pars, which is a variant of that used in [4]. The equivalence
with the approach in [5] is demonstrated in [4].

###  3.1 PARS

Let $A$ be a countable set on which a pars $\mathcal{A}=(A,\rightarrow)$ is
given. We define a rewrite system $(\mathsf{m}A,\mathrel{\rightrightarrows})$,
where $\mathsf{m}A$ is the set of objects to be rewritten, and
$\mathrel{\rightrightarrows}$ a relation on $\mathsf{m}A$. We indicate as PARS
the resulting rewriting system.

##### The objects to be rewritten.

$\mathsf{m}A$ is the set of all _multidistributions_ on $A$, which are defined
as follows.

Let $\mathtt{m}$ be a multiset333A _multiset_ is a (finite) list of elements,
modulo reordering. of pairs of the form $pa$, with $p\in]0,1]$, $a\in A$; the
multiset $\mathtt{m}=[p_{i}a_{i}\mid i\in I]$ is a multidistribution on $A$ if
$\sum_{i\in I}p_{i}\leq 1$.

We write the multidistribution $[1a]$ simply as $[a]$. The disjoint sum of
multidistributions is denoted by $+$. The product $q\cdot\mathtt{m}$ of a
scalar $q$ and a multidistribution $\mathtt{m}$ is defined pointwise:
$q\cdot[p_{1}a_{1},...,p_{n}a_{n}]=[(qp_{1})a_{1},...,(qp_{n})a_{n}]$.

Intuitively, a multidistribution $\mathtt{m}\in\mathsf{m}A$ is a _syntactical
representation_ of a discrete probability space where at each element of the
space is associated a probability and a term of $A$. More precisely, _each
pair in $\mathtt{m}$ correspond to a trace of computation_, or –in the
language of Markov Decision Processes– to _a sample path_.

##### The rewriting relation.

The binary relation $\mathrel{\rightrightarrows}$ on $\mathsf{m}A$ is obtained
by lifting the relation $\rightarrow$ of the pars
$\mathcal{A}=(A,\rightarrow)$, as follows.

######  Definition 10 (Lifting).

Given a relation $\to\subseteq A\times\mathsf{Dst}(A)$, its lifting to a
relation $\mathrel{\rightrightarrows}\subseteq\mathsf{m}A\times\mathsf{m}A$ is
defined by the rules.

$[a]\mathrel{\rightrightarrows}[a]a\not\to\quad\quad[a]\mathrel{\rightrightarrows}[p_{k}a_{k}\mid
k\in K]a\to\\{a_{k}^{p_{k}}\mid k\in K\\}\quad\quad[p_{i}a_{i}\mid i\in
I]\mathrel{\rightrightarrows}\sum_{i\in
I}{p_{i}\cdot\mathtt{m}_{i}}\big{(}[a_{i}]\mathrel{\rightrightarrows}\mathtt{m}_{i}\big{)}_{i\in
I}$

For the lifting, several natural choices are possible. Here we force _all_
non-terminal elements to be reduced. This choice plays an important role for
the development of the paper, as it corresponds to the key notion of _one
step_ reduction in classical ARS (see discussion in Sec. 10). Note also that:

  * L1

$\mathrel{\rightrightarrows}$ is reflexive on normal forms.

  * L2

$[p_{k}a_{k}\mid k\in K]\in\mathsf{m}A$ is simply a representation of the
distribution $\\{a_{k}^{p_{k}}\mid k\in K\\}\in\mathsf{Dst}(A)$.

  * L3

To apply rule $(L3)$, we have to choose a reduction step from $a_{i}$ for
_each_ $i\in I$. The (disjoint) sum of all $\mathtt{m}_{i}$ ($i\in I$) is
weighted with the scalar $p_{i}$ associated to each $p_{i}a_{i}$.

######  Example 11.

Let us derive the reduction in Fig. 3. For readability, elements in
$\mathbb{N}$ are in bold.

$[\textbf{2}]\mathrel{\rightrightarrows}[\frac{1}{2}\textbf{1},\frac{1}{2}\textbf{3}]\textbf{2}\rightarrow\\{\textbf{1}^{\frac{1}{2}},\textbf{3}^{\frac{1}{2}}\\}$
$[\frac{1}{2}\textbf{1},\frac{1}{2}\textbf{3}]\mathrel{\rightrightarrows}[\frac{1}{4}\textbf{0},\frac{1}{4}\textbf{2},\frac{1}{4}\textbf{2},\frac{1}{4}\textbf{4}]\lx@proof@logical@and
1\rightarrow\\{\textbf{0}^{\frac{1}{2}},\textbf{2}^{\frac{1}{2}}\\}3\rightarrow\\{\textbf{2}^{\frac{1}{2}},\textbf{4}^{\frac{1}{2}}\\}$
$[\frac{1}{4}\textbf{0},\frac{1}{4}\textbf{2},\frac{1}{4}\textbf{2},\frac{1}{4}\textbf{4}]\mathrel{\rightrightarrows}[...,\frac{1}{4}\textbf{stop},\frac{1}{8}\textbf{1},\frac{1}{8}\textbf{3},...]\lx@proof@logical@and\dots\textbf{2}\rightarrow\\{stop^{1}\\}\textbf{2}\rightarrow\\{\frac{1}{2}\textbf{1},\frac{1}{2}\textbf{3}\\}\dots$

##### PARS.

We indicate as PARS the rewrite system $(mA,\mathrel{\rightrightarrows})$
which is induced by the pars $(A,\rightarrow)$.

##### Rewrite sequences.

We write $\mathtt{m}_{0}\mathrel{\rightrightarrows}^{*}\mathtt{m}_{n}$ to
indicate that there is a _finite sequence_
$\mathtt{m}_{0},\dots,\mathtt{m}_{n}$ such that
$\mathtt{m}_{i}\mathrel{\rightrightarrows}\mathtt{m}_{i+1}$ for all $0\leq
i<n$ (and $\mathtt{m}_{0}\mathrel{\rightrightarrows}^{k}\mathtt{m}_{k}$ to
specify its length $k$). We write
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ to indicate an _infinite
rewrite sequence_.

##### Figures conventions:

we depict _any_ rewrite relation simply as $\rightarrow$; as it is standard,
we use $\twoheadrightarrow$ for $\rightarrow^{*}$; solid arrows are
universally quantified, dashed arrows are existentially quantified.

###  3.2 Normal forms and observations

Intuitively, a multidistribution $\mathtt{m}\in\mathsf{m}A$ is a _syntactical
representation_ of a discrete probability space where at each element of the
space is associated a probability and a term of $A$. This space may contain
various information. We analyze this space by defining random variables that
_observe specific properties of interest_. Here we focus on a specific event
of interest: the set $\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$ of _normal forms_
of $\mathcal{A}$.

##### Distribution over the elements of $A$.

First of all, to each multidistribution $\mathtt{m}=[p_{i}a_{i}\mid i\in I]$
we can associate a (sub)distribution $\mu\in\mathsf{Dst}(A)$ as follows, where
the emtpy sum is $0$:

$\mu(c):=\sum_{i\in I}p_{i}\mbox{ s.t. }a_{i}=c$

Informally, for each $c\in A$, we sum the probability of all occurrence of $c$
in the multidistribution.

##### Distribution over the _normal forms_ of $A$.

Given $\mathtt{m}\in\mathsf{m}A$, the probability that the system is in normal
form is described by $\mu(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})$ (recall
Example 3); the probability that the system is in a specific normal form $t$
is described by $\mu(t)$.

It is convenient to have a direct definition of both, to which we will refer
in the rest of the paper.

  * •

The function $-^{\scriptscriptstyle{\textsf{NF}}}$

$-^{\scriptscriptstyle{\textsf{NF}}}:\mathsf{m}A\to\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})\quad\mathtt{m}\mapsto\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}$

is defined as follows, for $\mathtt{m}=[p_{i}a_{i}\mid i\in I]$, and
$u\in\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$

$\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}(u):=\sum_{i\in I}p_{i}\mbox{
s.t. }a_{i}=u$

Informally, this function extracts from $\mathtt{m}=[p_{i}a_{i}]_{i\in I}$ the
_subdistribution $\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}$ over normal
forms_.

  * •

The norm $\|-\|:\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})\to[0,1]$
(recall that
$\|\mu\|=\sum\limits_{u\in\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}}\mu(u)$)
induces the function

$\|-^{\scriptscriptstyle{\textsf{NF}}}\|:\mathsf{m}A\to[0,1]\quad\mathtt{m}\mapsto\|\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\|$

which observes the probability that $\mathtt{m}$ has reached a normal form.

######  Example 12.

Let
$\mathtt{m}=[\frac{1}{4}{\texttt{T}},\frac{1}{8}{\texttt{T}},\frac{1}{4}{\texttt{F}},\frac{3}{8}c]$
(where ${\texttt{T}},{\texttt{F}}$ are normal forms, and $c$ is not). Then
$\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}=\\{{\texttt{T}}^{\frac{3}{8}},{\texttt{F}}^{\frac{1}{4}}\\}$,
and $\|\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\|=\frac{5}{8}$.

Clearly, $\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}$ is the restriction of
$\mu$ to $\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$. Observe that
$\|\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\|=\mu(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})=\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})$.

The probability of reaching a normal form $u$ can only increase in a rewrite
sequence (because of (L1) in Def. 10). Therefore the following key lemma
holds.

######  Lemma 13.

If $\mathtt{m}_{1}\mathrel{\rightrightarrows}\mathtt{m}_{2}$ then
$\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}_{1}\leq\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}_{2}$
and
$\|\mathtt{m}_{1}^{\scriptscriptstyle{\textsf{NF}}}\|\leq\|\mathtt{m}_{2}^{\scriptscriptstyle{\textsf{NF}}}\|$

##### Equivalences and Order.

In this paper $\mathtt{m}\in MA$ is a multiset, for simplicity and uniformity
with [19], but we could have used lists rather than multisets – as we do in
[18]. We do not really care of equality of elements in $\mathsf{m}A$ – what we
are interested are instead equivalence and order relations w.r.t _the
observation of specific events_. For example, the following – recall that the
order on $\mathsf{Dst}(A)$ is the pointwise order (Sec. 2.3):

Let $\mathtt{m},\mathtt{r}\in\mathsf{m}A$.

  1. 1.

_Flat Equivalence_ : $\mathtt{m}=_{\texttt{flat}}\mathtt{r}$, if $\mu=\rho$.
Similarly, $\mathtt{m}\geq_{\texttt{flat}}\mathtt{r}$ if $\mu\geq\rho$.

  2. 2.

_Equivalence in Normal Form_ :
$\mathtt{m}=_{{\scriptscriptstyle{\textsf{NF}}}}\mathtt{r}$, if
$\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}=\mathtt{r}^{\scriptscriptstyle{\textsf{NF}}}$.
Similarly, $\mathtt{m}\geq_{{\scriptscriptstyle{\textsf{NF}}}}\mathtt{r}$, if
$\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\geq\mathtt{r}^{\scriptscriptstyle{\textsf{NF}}}$

  3. 3.

_Equivalence in the NF -norm_:
$\mathtt{m}=_{\scriptscriptstyle{\|\|}}\mathtt{r}$, if
$\|\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\|=\|\mathtt{r}^{\scriptscriptstyle{\textsf{NF}}}\|$,
and $\mathtt{m}\geq_{\scriptscriptstyle{\|\|}}\mathtt{r}$, if
$\|\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\|\geq\|\mathtt{r}^{\scriptscriptstyle{\textsf{NF}}}\|$

Note that (2.) and (3.) compare $\mathtt{m}$ and $\mathtt{r}$ abstracting from
any term which is not in normal form.

######  Example 14.

Assume T is a normal form and $a\not=c$ are not.

  1. 1.

Let
$\mathtt{m}=[\frac{1}{2}{\texttt{T}},\frac{1}{2}{\texttt{T}}],~{}\mathtt{r}=[{\texttt{T}}]$.
$\mathtt{m}=_{\texttt{flat}}\mathtt{r}$,
$\mathtt{m}=_{{\scriptscriptstyle{\textsf{NF}}}}\mathtt{r}$,
$\mathtt{m}=_{\scriptscriptstyle{\|\|}}\mathtt{r}$ all hold.

  2. 2.

Let $\mathtt{m}=[\frac{1}{2}a,\frac{1}{2}{\texttt{T}}]$,
$\mathtt{r}=[\frac{1}{2}c,\frac{1}{6}{\texttt{T}},\frac{2}{6}{\texttt{T}}]$.
$\mathtt{m}=_{{\scriptscriptstyle{\textsf{NF}}}}\mathtt{r}$,
$\mathtt{m}=_{\scriptscriptstyle{\|\|}}\mathtt{r}$ both _hold_ ,
$\mathtt{m}=_{\texttt{flat}}\mathtt{r}$ does _not_.

The above example illustrates also the following.

######  Fact 15.

$(\mathtt{m}=_{\texttt{flat}}\mathtt{r})~{}\Rightarrow~{}(\mathtt{m}=_{{\scriptscriptstyle{\textsf{NF}}}}\mathtt{r})~{}\Rightarrow~{}(\mathtt{m}=_{\scriptscriptstyle{\|\|}}\mathtt{r})$.
Similarly for the order relations.

##  4 Asymptotic Behaviour of PARS

We examine the asymptotic behaviour of rewrite sequences _with respect to
normal forms_ , which are the most common notion of result.

The intuition is that a rewrite sequence describes a computation; an element
$\mathtt{m}_{i}$ such that
$\mathtt{m}\mathrel{\rightrightarrows}^{i}\mathtt{m}_{i}$ represents a state
(precisely, the state at time $i$) in the evolution of the system with initial
state $\mathtt{m}$. The _result_ of the computation is a distribution over the
possible normal forms of the probabilistic program. We are interested in the
result when the number of steps tends to infinity, that is _at the limit_.
This is formalized by the (rather standard) notion of _limit distribution_
(Def. 18). What is new here, is that since each element $\mathtt{m}$ has
different possible reduction sequences (each sequence leading to a possibly
different limit distribution) to $\mathtt{m}$ is naturally associated a _set_
of limit distributions.

A fundamental property for a system such as the $\lambda$-calculus is that if
a term has a normal form, it is unique. This is crucial to the computational
interpretation fo the calculus, because it means that the result of the
computation is _well defined_. A question we need to address in the setting of
PARS, is what does it mean to have a well-defined result. With this in mind,
we investigate an analogue of the ARS notions of normalization, termination,
and unique normal form.

###  4.1 Limit Distributions

Before introducing limit distributions, we revisit some facts on sequences of
bounded functions.

##### Monotone Convergence.

We recall the following standard result.

######  Theorem 16 (Monotone Convergence for Sums).

Let $X$ be a countable set, $f_{n}:X\to[0,\infty]$ a non-decreasing sequence
of functions, such that $f(x):=\lim_{n\to\infty}f_{n}(x)=\sup_{n}f_{n}(x)$
exists for each $x\in X$. Then

$\lim_{n\to\infty}\sum_{x\in X}f_{n}(x)~{}=~{}\sum_{x\in\mathcal{X}}f(x)$

Let $\langle\alpha_{n}\rangle_{n\in\mathbb{N}}$ be a _non-decreasing sequence_
of (sub)distributions over a countable set $X$ (the order on subdistributions
is defined pointwise, Sec. 2.3). For each $t\in X,$ the sequence
$\langle{\alpha_{n}}(t)\rangle_{n\in\mathbb{N}}$ of real numbers is
_nondecreasing and bounded_ , therefore the sequence has a limit, which is the
supremum: $\lim_{n\to\infty}{\alpha_{n}}(t)=\sup_{n}\\{{\alpha_{n}}(t)\\}$.
Observe that if $\alpha<\alpha^{\prime}$ then
$\|\alpha\|<\|\alpha^{\prime}\|$, where we recall that $\|\alpha\|:=\sum_{x\in
X}\alpha(x)$.

######  Lemma 17.

Given $\langle\alpha_{n}\rangle_{n\in\mathbb{N}}$ as above, the following
properties hold. Define

$\beta(t)=\lim_{n\to\infty}{\alpha_{n}}(t),~{}\forall t\in X$

  1. 1.

$\lim_{n\to\infty}\|\alpha_{n}\|~{}=~{}\|\beta\|$

  2. 2.

$\lim_{n\to\infty}\|\alpha_{n}\|=\sup_{n}\\{\|\alpha_{n}\|\\}\leq 1$

  3. 3.

$\beta$ is a _subdistribution_ over $X$.

###### Proof.

(1.) follows from the fact that $\langle\alpha_{n}\rangle_{n\in\mathbb{N}}$ is
a nondecreasing sequence of functions, hence (by Monotone Convergence, see
Thm. 16 in Appendix) we have :

$\lim_{n\to\infty}\sum_{t\in X}{\alpha_{n}(t)}~{}=~{}\sum_{t\in
X}\lim_{n\to\infty}\alpha_{n}(t)$

(2.) is immediate, because the sequence
$\langle{\|\alpha_{n}\|}\rangle_{n\in\mathbb{N}}$ is nondecreasing and
bounded.
(3.) follows from (1.) and (2.). Since $\|\beta\|=\sup_{n}\|\alpha_{n}\|\leq
1$, then $\beta$ is a subdistribution. ∎

##### Limit distributions.

Let $\mathcal{A}=(mA,\mathrel{\rightrightarrows})$ be the rewrite system
induced by a pars $(A,\rightarrow)$.

Let $\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ be a rewrite sequence. If
$t\in\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$, then
$\langle\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}(t)\rangle_{n\in\mathbb{N}}$
is nondecreasing (by Lemma 13); so we can apply Fact 17, with
$\langle\alpha_{n}\rangle_{n\in\mathbb{N}}$ now being
$\langle\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}_{n}\rangle_{n\in\mathbb{N}}$.

######  Definition 18 (Limits).

Let $\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ be a rewrite sequence from
$\mathtt{m}\in\mathsf{m}A$. We say

  1. 1.

$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ converges with probability
$p=\sup_{n}\\{\|\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}\|\\}$.

  2. 2.

$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ converges to
${\beta}\in\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})$

$\beta(t)=\sup_{n}\\{\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}(t)\\}$

We call $\beta$ a limit distribution (on normal forms) of $\mathtt{m}$, and
$p$ a limit probability (to reach a normal form) of $\mathtt{m}$. We write
$\mathtt{m}\xRightarrow{\infty}\beta$ (resp.
$\mathtt{m}\xRightarrow{\infty}_{\scriptscriptstyle{\|\|}}p$) if $\mathtt{m}$
has a sequence which converges to $\beta$ (resp. converges with probability
$p$). We define
$\mathtt{Lim}(\mathtt{m}):=\\{\beta~{}\mid~{}\mathtt{m}\xRightarrow{\infty}\beta\\}$
the set of limit distributions, and
$\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m}):=\\{p~{}\mid~{}\mathtt{m}\xRightarrow{\infty}_{\scriptscriptstyle{\|\|}}p\\}$.

Note that $p$ is a scalar, while $\beta$ is a function, which describes a
distribution over the normal forms:

  1. 1.

is a quantitative version of a boolean (yes/no) property: to reach a normal
form.

  2. 2.

is a quantitative version of a qualitative property: which normal form is
reached.

Clearly

$\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})=\\{\|\beta\|~{}\mid~{}\beta\in\mathtt{Lim}(\mathtt{m})\\}$

because
$\sup_{n}\|\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}\|=\|\sup_{n}{\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}}\|$
(by Fact 17, point 1.).

A computationally natural question is if the result of computing an element
$\mathtt{m}$ is well defined. We analyze it in Sec. 5 –putting this question
in a more general, but also simpler, context.

In fact, most properties of the asymptotic behaviours of PARS are not specific
to probability, and are best understood when focusing only on the essentials,
abstracting from the details of the formalism.

Before doing so, we build an intuition by informally investigating the notions
of normalization, termination, and unique normal form in our concrete setting.

In the rest of the paper, we always intend a PARS to be equipped with the
notions of convergence and limit distribution which we have defined here.

###  4.2 PARS vs ARS: subtleties, questions, and issues

####  4.2.1 On Normalization and Termination

In the setting of ARS, a rewrite sequence from an element $c$ may or may not
reach a normal form. The notion of reaching a normal form comes in two
flavours (see Sec. 2.1): (1.) _there exists_ a rewrite sequence from $c$ which
leads to a normal form (_normalization_ , WN); (2.) _each_ rewrite sequence
from $c$ leads to a normal form (_termination_ , SN). If no rewrite sequence
leads to a normal form, then $c$ _diverges_.

It is interesting to analyze a similar $\exists/\forall$ distinction in a
quantitative setting. We distinguish two cases.

##### Convergence with _probability 1_.

If we restrict the notion of convergence to _probability 1_ , then it is
natural to say that an element $\mathtt{m}$ weakly normalize if it has a
reduction sequence which converges to $1$, and strongly normalizes (or, it is
AST) if all reduction sequences converges to $1$.

##### The general case.

Many natural examples –in particular when we consider untyped probabilistic
$\lambda$-calculus– are not limited to convergence with probability $1$, as
shows Example 2.

In the general case, extra subtleties emerge, due to the fact that _each
reduction sequence converges with some probability_ $p\in[0,1]$ (possibly 0).

A first important observation is that the set
$\\{q\mid\mathtt{m}\xRightarrow{\infty}_{\scriptscriptstyle{\|\|}}p\\}$ has a
supremum (say $p$), but _not necessarily a greatest element_. Think of
$[0,p[$, which has a sup, but not greatest element. If
$\mathtt{Lim}_{\scriptscriptstyle{\|\|}}$ has no greatest element , it means
that no reduction sequence converges to the supremum $p$.

A second remark is that we naturally speak of termination/normalization with
probability $0$. Not only it appears awkward to separate the case $0$ (as
distinct from $0.00001$), but divergence also –dually– should be quantitative.

We say that $\mathtt{m}$ (weakly) normalizes (with probability $p$) if
$\\{q\mid\mathtt{m}\xRightarrow{\infty}_{\scriptscriptstyle{\|\|}}q\\}$ has a
greatest element ($p$). This means that there _exists_ a reduction sequences
whose limit is $p$. Dually, we can say that $\mathtt{m}$ strongly normalizes
(or terminates)  (with probability $p$), if all reduction sequences converge
with the same probability $p\in[0,1]$.

Since in this case _all reduction sequences have have the same behavior_ , a
better term seems that $\mathtt{m}$ uniformly normalizes. And indeed, ”all
reduction sequences converge with the same probability” is the analogue of the
ARS notion of _uniform normalization_ , the property that all reduction
sequences form an element either all terminate, or all diverge (otherwise
stated: weak normalization implies strong normalization). Summing up, we use
the following terminology:

######  Definition 19 (Normalization and Termination).

A PARS is $\mathtt{WN^{\infty}}$, $\mathtt{SN^{\infty}}$, or AST, if each
$\mathtt{m}$ satisfies the corresponding property, where

  * •

$\mathtt{m}$ is $\mathtt{WN^{\infty}}$($\mathtt{m}$ normalizes) if there
_exists a sequence_ from $\mathtt{m}$ which converges with greatest
probability (say $p$). To specify, we say that $\mathtt{m}$ is
p-$\mathtt{WN^{\infty}}$.

  * •

$\mathtt{m}$ is $\mathtt{SN^{\infty}}$( $\mathtt{m}$ strongly –or uniformely–
normalizes) if _all sequences_ from $\mathtt{m}$ converge with the same
probability (say $p$). To specify, we say that $\mathtt{m}$ is
p-$\mathtt{SN^{\infty}}$.

  * •

$\mathtt{m}$ is Almost Sure Terminating (AST) if it strongly normalizes with
probability $1$.

######  Example 20.

The system in Fig. 5 is $1$-$\mathtt{WN^{\infty}}$, but not
$1$-$\mathtt{SN^{\infty}}$. The top rewrite sequence (in blue ) converges to
$1=\lim_{n\to\infty}\sum_{1}^{n}\frac{1}{2^{n}}$. The bottom rewrite sequence
(in red) converges to $0$. In between, we have all dyadic possibilities. In
contrast, the system in Fig. 5 is AST.

####  4.2.2 On Unique Normal Forms and Confluence

The main question on which we focus is when the notion of result
$[\\![\mathtt{m}]\\!]$ is well defined. It is also natural to wonder how do
different rewrite sequences from the same initial $\mathtt{m}$ compare. Given
a probabilistic program $M$, if $[M]\xRightarrow{\infty}\alpha$ and
$[M]\xRightarrow{\infty}\beta$, how $\beta$ and $\alpha$ relate?

Normalization and termination are _quantitative yes/no_ properties - we are
only interested in the number $\|\beta\|$, for $\beta$ limit distribution; for
example, if $\mathtt{m}\xRightarrow{\infty}\\{{\texttt{F}}^{1}\\}$ and
$\mathtt{m}\xRightarrow{\infty}\\{{\texttt{T}}^{1/2},{\texttt{F}}^{1/2}\\}$,
then $\mathtt{m}$ converges with probability $1$, but we make no distinction
between the two -very different- results. Similarly, consider again Fig. 5.
The system is AST, however the limit distributions are _not unique_ : they
span an infinity of distributions which have shape
$\\{{\texttt{T}}^{p},{\texttt{F}}^{1-p}\\}$. These observations motivate
attention to finer-grained properties.

In usual rewriting theory, the fact that the result is well defined is
expressed by the _unique normal form_ property (UN). Let us examine an
analogue of UN in a probabilistic setting. An intuitive candidate is the
following, which was first proposed in [16]:

ULD: if $\alpha,\beta\in\mathtt{Lim}(\mathtt{m})$, then $\alpha=\beta$

[16] shows that, in the case of AST, confluence implies ULD. However, ULD is
not a good analogue in general, because a PARS does not need to be AST (or
$\mathtt{SN^{\infty}}$); it may well be that
$\mathtt{m}\xRightarrow{\infty}\alpha$ and
$\mathtt{m}\xRightarrow{\infty}\beta$, with $\|\alpha\|\not=\|\beta\|$. We
have seen rewrite systems which are not AST in Fig. 5, and in Example 2.
Similar examples are natural in an _untyped_ probabilistic $\lambda$-calculus
(recall that the $\lambda$-calculus is not SN!).

In the general case, ULD is not implied by confluence: the system in Fig. 5 is
indeed confluent. We then would like to say that it satisfies UN.

We propose as probabilistic analogue of UN the following property

$\mathtt{UN^{\mathtt{\infty}}}$: $\mathtt{Lim}(\mathtt{m})$ has a _greatest_
element.

which we justify in section Sec. 5, where we show that PARS satisfy an
analogue of standard ARS results: “Confluence implies UN” (Thm. 38), and “the
Normal Form Property implies UN” (Prop. 31). There are however two important
observations to do.

##### Important observation!

While the statements are similar to the classical ones, the content is not. To
understand the difference, and what is non-trivial here, observe that in
general there is no reason to believe that $\mathtt{Lim}(\mathtt{m})$ has
maximal elements. Think again of the set $[0,1[$, which has no max, even if it
has a sup. Observe also that $\mathtt{Lim}(\mathtt{m})$ is –in general–
uncountable.

The proof that confluence implies uniqueness of maximal elements is a
refinement of the analogous ARS properties, similar to that in infinitary
rewriting. Instead, to prove the existence of maximal elements is non-trivial.

##### Which notion of Confluence?

To guarantee $\mathtt{UN^{\mathtt{\infty}}}$, it suffices a weaker form of
confluence than one would expect. Assume
$\mathtt{s}~{}{}^{*}\leftleftarrows\mathtt{m}\mathrel{\rightrightarrows}^{*}\mathtt{r}$;
with the standard notion of confluence in mind, we may require that
$\exists\mathtt{u}$ such that
$\mathtt{s}\mathrel{\rightrightarrows}^{*}\mathtt{u}$,
$\mathtt{r}\mathrel{\rightrightarrows}^{*}\mathtt{u}$ or that
$\exists\mathtt{u},\mathtt{u}^{\prime}$ such that
$\mathtt{s}\mathrel{\rightrightarrows}^{*}\mathtt{u}$,
$\mathtt{r}\mathrel{\rightrightarrows}^{*}\mathtt{u}^{\prime}$ and
$\mathtt{u}=_{\texttt{flat}}\mathtt{u}^{\prime}$. Both are fine, but in Sec.
5.2 we show that a weaker notion of equivalence (which was already discovered
in [3]) suffices– we only need to compare multidistributions w.r.t. their
information content on normal forms.

######  Remark 21.

In the case of AST(and $\mathtt{SN^{\infty}}$), all limits are maximal, hence
$\mathtt{UN^{\mathtt{\infty}}}$ becomes ULD.

####  4.2.3 Newman’s Lemma Failure, and Proof Techniques for PARS

The statement of Thm. 38 “Confluence implies $\mathtt{UN^{\mathtt{\infty}}}$”
has the _same flavour_ as the analogue one for ARS, but the _notions are not
the same_. The notion of limit (and therefore that of
$\mathtt{UN^{\mathtt{\infty}}}$, $\mathtt{SN^{\infty}}$, and
$\mathtt{WN^{\infty}}$) does not belong to ARS. For this reason, the rewrite
system $(mA,\mathrel{\rightrightarrows})$ which we are studying is not simply
an ARS, and one should not assume that standard ARS properties hold. An
illustration of this is Newman’s Lemma. Given a PARS, let us assume AST and
observe that in this case, confluence _at the limit_ can be identified with
$\mathtt{UN^{\mathtt{\infty}}}$. _A wrong attempt:_ AST \+
$\mathtt{WCR^{\mathtt{\infty}}}$ $\Rightarrow$
$\mathtt{UN^{\mathtt{\infty}}}$, where $\mathtt{WCR^{\mathtt{\infty}}}$: if
$\mathtt{m}\mathrel{\rightrightarrows}\mathtt{s}_{1}$ and
$\mathtt{m}\mathrel{\rightrightarrows}\mathtt{s}_{2}$, then
$\exists\mathtt{r}$, with $\mathtt{s}_{1}\xRightarrow{\infty}\mathtt{r}$,
$\mathtt{s}_{2}\xRightarrow{\infty}\mathtt{r}$. This does not hold. A
counterexample is the PARS in Fig. 5, which does satisfy
$\mathtt{WCR^{\mathtt{\infty}}}$. (More in the Appendix.)

What is at play here is that the notion of _termination_ is not the same in
ARS and in PARS. A fundamental fact of ARS (on which all proofs of Newman’s
Lemma rely) is: termination implies that the rewriting relation is well
founded. All terminating ARS allow well-founded induction as proof technique;
this is _not the case_ for probabilistic termination. To transfer properties
from ARS to PARS there are two issues: we need to find the _right formulation_
and the _right proof technique_.

Our counter-example still leaves open the question “Can a different
formulation uncover properties similar to Newman Lamma?” Or, better, “Are
there _local properties_ which guarantee $\mathtt{UN^{\mathtt{\infty}}}$?”

##  5 Quantitative Abstract Rewriting Systems

We observed that the notion of result as a limit does not belong to ARS. To be
able to formalize such a notion in an abstract framework, we enrich the
definition of ARS into that of Quantitative ARS (QARS). Working abstractly
allows us to study the asymptotic properties in a way that is independent from
the specific syntax, and to capture the essence of the arguments.

Ariola and Blom [3] have introduced the notion of Abstract Rewrite Systems
with Information content (ARSI); to the ARS is associate a partial order which
expresses a comparison between the ”information content” of the elements.
QARS, presented below, are a natural refinement of the ARSI in [3].

##### QARS.

We first give the intuition. Let $(C,\rightarrow)$ be an ARS, whose elements
we indicate with letters $\mathtt{t},\mathtt{s},\mathtt{r}\dots$. To each
element $\mathtt{t}$ in the set $C$ is associated a notion of (partial)
information. A reduction sequence gradually computes a result by converging
(in a finite or infinite number of steps) to the maximal amount of information
which it can produce. The standard structure to express a result in terms of
partial information is that of $\omega$-cpo. Def. 22 formalizes the intuition;
the information content of an element $\mathtt{t}\in C$ is modeled by a
function from $C$ to an $\omega$-cpo.

Recall that a partially ordered set $\mathbb{S}=(\mathbb{S},\leq)$ is an
$\omega$-complete partial order ($\omega$-cpo) if every chain
$\bm{s}_{0}\leq\bm{s}_{1}\leq...$ has a supremum. We assume the partial order
to have a least element $\bot$. We denote with bold letters
$\bm{s},\bm{p},\bm{q}$ elements of $\mathbb{S}$.

######  Definition 22 (QARS).

A Quantitative ARS (QARS) is an ARS $(C,\rightarrow)$ together with a function
$\mathtt{obs}:A\rightarrow\mathbb{S}$, where $\mathbb{S}$ is an $\omega$-cpo
and such that

$\mathtt{t}\rightarrow\mathtt{s}$ implies
$\mathtt{obs}(\mathtt{t})\leq\mathtt{obs}(\mathtt{s})$.

Intuitively, the function $\mathtt{obs}$ observes a specific property of
interest about $\mathtt{t}\in C$. The observation $\mathtt{obs}(\mathtt{t})$
indicates how much stable information $\mathtt{t}$ delivers: the information
content is monotone increasing during computation.

######  Example 23.

The following are all examples of QARS.

  1. 1.

ARS: take $\mathbb{S}=(\\{0,1\\},\leq)$ and the boolean function
$\mathtt{obs}(\mathtt{t})=1$ if $\mathtt{t}$ is a normal form,
$\mathtt{obs}(\mathtt{t})=0$ otherwise.

  2. 2.

PARS: take $\mathbb{S}=([0,1],\leq)$, and a function which corresponds to a
probability measure, for example the probability to be in normal form
$\mathtt{obs}(\mathtt{m})\mapsto\|\mathtt{m}^{\scriptscriptstyle{\textsf{NF}}}\|$
(as defined in Sec. 3.2).

The observation $\mathtt{obs}(\mathtt{t})$ does not need to take numerical
values. In the examples below, $\mathbb{S}$ is an $\omega$-cpo of _partial
results_.

######  Example 24.

  1. 1.

ARS: take for $\mathbb{S}$ the flat order on normal forms, and define the
function $\mathtt{obs}(\mathtt{u})=\mathtt{u}$ if $\mathtt{u}$ is normal,
$\mathtt{obs}(\mathtt{u})=\bot$ otherwise.

  2. 2.

PARS: take for $\mathbb{S}$ the $\omega$-cpo of subdistributions on normal
forms $\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})$, and for
$\mathtt{obs}$ the function $-^{\scriptscriptstyle{\textsf{NF}}}$, as defined
in Sec. 3.2.

##### Letters convention.

We use bold letters $\bm{s},\bm{p},\bm{q}$ to indicate elements of a generic
$\omega$-cpo $\mathbb{S}$. Letters $p,q$ indicate elements of
$[0,1]\subset\mathbb{R}$. Greek letters $\alpha,\beta,\gamma$ indicate
probability subdistributions.

##### Rewrite sequences.

A $\to$-sequence (or reduction sequence) from $\mathtt{t}$ is a (possibly
infinite) sequence $\mathtt{t}\to\mathtt{t}_{1}\to\dots$ such that
$\mathtt{t}_{i}\to\mathtt{t}_{i+1}$. We write
$\mathtt{t}\rightarrow^{*}\mathtt{s}$ to indicate that there is a _finite_
sequence from $\mathtt{t}$ to $\mathtt{s}$.

To indicate in a uniform way _maximal_ reduction sequences, whenever finite or
infinite, we write $\langle\mathtt{t}_{n}\rangle_{n\in\mathbb{N}}$ for an
_infinite_ sequence such that either
$\mathtt{t}_{i}\rightarrow\mathtt{t}_{i+1}$, or
$\mathtt{t}_{i}=\mathtt{t}_{i+1}\in\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$
(hence, $\langle\mathtt{t}_{n}\rangle_{n\in\mathbb{N}}$ is constant from an
index $k$ on if $\mathtt{t}\rightarrow^{*}\mathtt{t}_{k}\not\rightarrow$)

###  5.1 Limits and Results

In this section we assume fixed a QARS
$\mathbf{Q}=((C,\rightarrow),\mathtt{obs})$. Intuitively, the result computed
by a possibly infinite reduction sequence
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ is its _limit_.

By definition, given a $\rightarrow$-sequence
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$, its limit w.r.t.
$\mathtt{obs}$

$\sup_{n}\\{\mathtt{obs}(\mathtt{m}_{n})\\}$.

always exists, because $\mathbb{S}$ is an $\omega$-cpo. Intuitively, this is
the maximal amount of information produced by the sequence, the _result_ of
that computation. Note that, in general, an element $\mathtt{m}\in A$ has
several possible reduction sequences, and therefore can produce several
results/have several limits.

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

For $\mathtt{m}\in C$, we write

$\mathtt{m}\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}\bm{p}$

if there exists a sequence $\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$
from $\mathtt{m}$ such that
$\sup_{n}\\{\mathtt{obs}(\mathtt{m}_{n})\\}=\bm{p}$. Then

  * •

$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m}):=\\{\bm{p}\mid\mathtt{m}\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}\bm{p}\\}$

  * •

$[\\![\mathtt{t}]\\!]$ denotes the greatest element of
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, if any exists.

Informally, to $\mathtt{m}$ is associated a well-defined result, which we
denote $[\\![\mathtt{m}]\\!]$, if the maximal amount of information produced
by any reduction sequence is well defined. The intuition is that
$[\\![\mathtt{m}]\\!]$ is well defined if different reduction sequences from
$\mathtt{m}$ do not produce “essentially different” results: if
$\bm{s}\not=\bm{p}$ then they are both _approximants_ of a same result
$\bm{r}$ (_i.e._ , $\bm{s},\bm{p}\leq\bm{\mathtt{r}}$).

Thinking of usual rewriting, consider $\mathtt{obs}$ as defined in point 1,
Ex. 24. Then to have a greatest limit exactly corresponds to uniqueness of
normal forms.

######  Example 26.

Let us revisit Ex. 23.

  1. 1.

$\lambda$-calculus: consider $\mathtt{t}=(\lambda x.z)(\Delta\Delta)$. This
term has several possible reduction sequences. The set of limits w.r.t.
$\mathtt{obs}$ contains two elements: $\\{0,1\\}$.

  2. 2.

Probabilistic $\lambda$-calculus: consider
$\mathtt{m}:=[I\oplus\Delta\Delta]$, which has only one reduction, starting
with
$\mathtt{m}\mathrel{\rightrightarrows}[\frac{1}{2}I,\frac{1}{2}\Delta\Delta]\mathrel{\rightrightarrows}\dots$.
In this case
$\mathtt{m}\mathrel{\rightrightarrows}\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}\frac{1}{2}$
and $\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})=\\{\frac{1}{2}\\}$.

Point 2. in Ex. 26 shows well that the notion of result is _quantitative_ :
$\mathtt{m}$ reaches a normal form with probability $\frac{1}{2}$. This also
shows that maximal elements of $\mathtt{Lim}_{\mathtt{obs}}(t)$ do not need to
be maximal elements of $\mathbb{S}$; the reason for this choice is exactely
that terms like $I\oplus\Delta\Delta$ (which converges to $\frac{1}{2}$ rathen
than $1$) are natural in an untyped setting like $\lambda$-calculus. As a
consequence, in general, _the set of limits may or may not have maximal
elements_. We are interested in reductions which have this property444The
subtlety here is that if $\mathtt{Lim}_{\mathtt{obs}}(t)$ has a sup
$\bm{s}\in\mathbb{S}$ which does not belong to $\mathtt{Lim}_{\mathtt{obs}}$,
no reduction sequence converges to $\bm{s}$..

Note that, even if $\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ has maximal
elements, a greatest limit does not necessarily exist. The probabilistic
$\lambda$-term in Ex. 1 is a good example: different reduction sequences lead
to different limits. Another clear example is Ex. 8: $a$ has an infinity of
limits, all maximal.

Like for PARS, the natural question is if the result of computing an element
$\mathtt{m}$ is well defined. This is exactly the sense of the property
$\mathtt{UN^{\mathtt{\infty}}}$, which we can state in full generality for
QARS.

A QARS satisfies property $\mathtt{UN^{\mathtt{\infty}}}$ if
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ has a _greatest_ element.

Clearly, by definition:

$\mathtt{UN^{\mathtt{\infty}}}$ if and only if $[\\![\mathtt{m}]\\!]$ is
defined.

###  5.2 Confluence and $\mathtt{UN^{\mathtt{\infty}}}$

In our setting, maximal limits play the role that normal forms have for ARS.
We show that confluence (and variants of it) imply not only uniqueness of
maximal limits, but a stronger property: if a maximal limit exists, it is the
_greatest_ limit.

An important observation is in order. Note that the above _does not state_
that confluence imply $\mathtt{UN^{\mathtt{\infty}}}$; for general QARS, this
is not true, because we have no guarantee that
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ contains any maximal element.

Fortunatelly, in the case of PARS, confluence does imply
$\mathtt{UN^{\mathtt{\infty}}}$– however the proof relies on more properties
than the basic ones which we have assumed for QARS; it is non-trivial.

######  Definition 27 (Confluence).

A QARS $((C,\rightarrow),\mathtt{obs})$ satisfies

  * •

Confluence if: $\forall\mathtt{s},\mathtt{r}\in C$ with
$\mathtt{s}~{}{}^{*}\leftarrow\mathtt{m}\rightarrow^{*}\mathtt{r}$, exists
$\mathtt{t}^{\prime}$ such that
$\mathtt{s}\rightarrow^{*}\mathtt{t}^{\prime}$,
$\mathtt{r}\rightarrow^{*}\mathtt{t}^{\prime}$.

  * •

$\mathtt{obs}$-Confluence if: $\forall\mathtt{s},\mathtt{r}\in C$ with
$\mathtt{s}~{}{}^{*}\leftarrow\mathtt{m}\rightarrow^{*}\mathtt{r}$, exists
$\mathtt{s}^{\prime},\mathtt{r}^{\prime}$ such that
$\mathtt{s}\rightarrow^{*}{\mathtt{s}^{\prime}}$,
$\mathtt{r}\rightarrow^{*}\mathtt{r}^{\prime}$, and
$\mathtt{obs}(\mathtt{s})^{\prime}=\mathtt{obs}(\mathtt{r}^{\prime})$.

  * •

Skew-Confluence555In [18] we call this property Semi-Confluence. The same
property is studied in
citeAriolaBlom02 – here we adopt their terminology.
$\forall\mathtt{s},\mathtt{r}\in C$ with
$\mathtt{s}~{}{}^{*}\leftarrow\mathtt{m}\rightarrow^{*}\mathtt{r}$, exists
$\mathtt{s}^{\prime}$ such that
$\mathtt{s}\rightarrow^{*}\mathtt{s}^{\prime}$, and
$\mathtt{obs}(\mathtt{r})\leq\mathtt{obs}(\mathtt{s}^{\prime})$.

Clearly

######  Fact 28.

Confluence $\Rightarrow$ $\mathtt{obs}$-Confluence $\Rightarrow$ Skew-
Confluence.

In analogy to the normal form property of ARS (NFP, see Sec. 2.1), we define
the following

######  Definition 29 (Limit Property ($\mathtt{LIMP}$)).

A QARS $((C,\rightarrow),\mathtt{obs})$ satisfies the Limit Property
$\mathtt{LIMP}$ if ($\forall\mathtt{m},\mathtt{s}\in C$):

$\bm{p}\in\mathtt{Lim}(\mathtt{m})$ and $\mathtt{m}\rightarrow^{*}\mathtt{s}$
imply there exists $\bm{q}\in\mathtt{Lim}(\mathtt{m})$ such that
$\mathtt{s}\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}\bm{q}$ and
$\bm{p}\leq\bm{q}$.

Figure 6: Skew-Confluence implies $\mathtt{LIMP}$

######  Lemma 30 (Main Lemma).

Given a QARS, Skew-Confluence implies $\mathtt{LIMP}$.

###### Proof.

Let $\mathtt{r}_{0},\mathtt{s}\in C$,
${\bm{p}}\in\mathtt{Lim}(\mathtt{r}_{0})$,
$\mathtt{r}_{0}\rightarrow^{*}\mathtt{s}$. Let
$\langle\mathtt{r}_{n}\rangle_{n\in\mathbb{N}}$ be a sequence with limit
${\bm{p}}$. As illustrated in Fig. 6, starting from $\mathtt{s}$, we build a
sequence
$\mathtt{s}=\mathtt{s}_{\mathtt{r}_{0}}\rightarrow^{*}\mathtt{s}_{\mathtt{r}_{1}}\rightarrow^{*}\mathtt{s}_{\mathtt{r}_{2}}\dots$,
where $\mathtt{s}_{\mathtt{r}_{i}}$, $i\geq 1$ is given by Skew Confluence:
from $\mathtt{r}_{0}\rightarrow^{*}\mathtt{r}_{i}$ and
$\mathtt{r}_{0}\rightarrow^{*}\mathtt{s}_{\mathtt{r}_{i-1}}$ we obtain
$\mathtt{s}_{\mathtt{r}_{i-1}}\rightarrow^{*}\mathtt{s}_{\mathtt{r}_{i}}$ with
$\mathtt{obs}(\mathtt{r}_{i})\leq\mathtt{obs}(\mathtt{s}_{\mathtt{r}_{i}})$.
Let ${\bm{q}}$ be the limit of the sequence so obtained; observe that
${\bm{q}}\in\mathtt{Lim}(\mathtt{r}_{0})$. By construction, $\forall i$,
$\mathtt{obs}(\mathtt{r}_{i})\leq\mathtt{obs}(\mathtt{s}_{\mathtt{r}_{i}})\leq{\bm{q}}$.
From ${\bm{p}}=\sup{\langle{\mathtt{obs}(\mathtt{r}_{n})}\rangle}$ it follows
that ${\bm{p}}\leq{\bm{q}}$. ∎

$\mathtt{LIMP}$ implies that if a maximal limit exists, it is the _greatest_
limit.

######  Proposition 31 (Greatest limit).

Given a QARS $((C,\rightarrow),\mathtt{obs})$, and $\mathtt{m}\in C$,
$\mathtt{LIMP}$ implies that if $\mathtt{Lim}(\mathtt{m})$ has a maximal
element, then it is the greatest element.

###### Proof.

Let ${\bm{p}}\in\mathtt{Lim}(\mathtt{m})$ be maximal. For each
${\bm{u}}\in\mathtt{Lim}(\mathtt{m})$, there is a sequence
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{m}$ such that
${\bm{u}}=\sup_{n}\mathtt{obs}(\mathtt{m}_{n})$. $\mathtt{LIMP}$ implies that
$\forall n$,
$\mathtt{m}_{n}\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}{\bm{q}}_{n}\geq{\bm{p}}$.
By maximality of ${\bm{p}}$, ${\bm{q}}_{n}={\bm{p}}$ and therefore
$\mathtt{obs}(\mathtt{m}_{n})\leq{\bm{p}}$. From
${\bm{u}}=\sup_{n}\mathtt{obs}(\mathtt{m}_{n})$ we conclude that
${\bm{u}}\leq{\bm{p}}$, that is, ${\bm{p}}$ is _the greatest element_ of
$\mathtt{Lim}(\mathtt{m})$. ∎

Given a confluent QARS, to guarantee that $\mathtt{UN^{\mathtt{\infty}}}$
holds and therefore for each $\mathtt{m}\in C$, $[\\![\mathtt{m}]\\!]$ is
defined, it suffices to establish that $\mathtt{Lim}(\mathtt{m})$ has a
maximal element.

In Sec. 5.4 we prove that in the case of PARS, confluence implies the
existence of a maximal element and therefore of a greatest element. To do
that, we use more structure, namely the fact that the $\omega$-cpo
$\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})$ is equipped with an
order-preserving norm
$\|\|:\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})\to[0,1]$.

###  5.3 Boolean QARS: Confluence implies $\mathtt{UN^{\mathtt{\infty}}}$

Let us consider the case of QARS where the associated $\omega$-cpo is the
bounded interval $[0,1]\subset\mathbb{R}^{\geq 0}$, equipped with the standard
order. We call boolean a QARS $\mathbf{Q}=((C,\rightarrow),\mathtt{obs})$ such
that $\mathtt{obs}:C\to[0,1]\subset\mathbb{R}$.

We show that property $\mathtt{LIMP}$ implies that
$p=\sup\,\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ _belongs_ to
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, where
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})=\\{q~{}\mid~{}\mathtt{m}\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}q\\}$.
Therefore, $\mathtt{UN^{\mathtt{\infty}}}$ holds.

We need a technical lemma

######  Lemma 32.

Let $\mathbf{Q}$ and $\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ and $p$ be as
above. For each $\epsilon>0$, property $\mathtt{LIMP}$ implies the following:
if $q\in\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, $|p-q|\leq\epsilon$, and
$\mathtt{m}\rightarrow^{*}\mathtt{s}$, then there exists $\mathtt{t}$, such
that $\mathtt{s}\rightarrow^{*}\mathtt{t}$ and
$|p-\mathtt{obs}(\mathtt{t})|\leq 2\epsilon$.

###### Proof.

The assumption $\mathtt{m}\rightarrow^{*}\mathtt{s}$ and $\mathtt{LIMP}$ imply
that there exists a rewrite sequence
$\langle\mathtt{s}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{s}$ which
converges to $q^{\prime}\geq q$; clearly $|p-q^{\prime}|\leq\epsilon$.

By definition of limit of a sequence, there is an index $k_{\epsilon}$ such
that $|q^{\prime}-\mathtt{obs}(\mathtt{s}_{k_{\epsilon}})|\leq\epsilon$, hence
$|p-\mathtt{obs}(\mathtt{s}_{k_{\epsilon}})|\leq 2\epsilon$. Since
$\mathtt{s}\rightarrow^{*}\mathtt{s}_{k_{\epsilon}}$,
$\mathtt{t}=\mathtt{s}_{k_{\epsilon}}$ satisfies the claim. ∎

######  Proposition 33 (Greatest limit).

Given a boolean QARS, property $\mathtt{LIMP}$ implies that
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ has a greatest element.

###### Proof.

(1. ) Let $p=\sup~{}\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$. We show that
$p\in\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, by building a rewrite sequence
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{m}$ such that
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}\xRightarrow{\infty}p$.

Observe that if $p\not\in\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, then for
each $\epsilon>0$, there exists $q\in\mathtt{Lim}_{\mathtt{obs}}$ such that
$|p-q|\leq\epsilon$. For each $k\in\mathbb{N}$, we define
$\epsilon_{k}=\frac{p}{2^{k}}$. Let $\mathtt{s}_{0}=\mathtt{m}$. From here, we
build a sequence of reductions
$\mathtt{m}\rightarrow^{*}\mathtt{s}_{1}\rightarrow^{*}\mathtt{s}_{2}\rightarrow^{*}\dots$
whose limit is $p$, as follows.

For each $k>0$:

  * •

there exists $q_{k}\in\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ such that
$|p-q_{k}|\leq\frac{1}{2}\frac{p}{2^{k}}$.

  * •

From $\mathtt{m}\rightarrow^{*}\mathtt{s}_{k-1}$, we use Lemma 32 to establish
that there exists $\mathtt{s}_{k}$ such that
$\mathtt{s}_{k-1}\rightarrow^{*}\mathtt{s}_{k}$ and
$|p-\mathtt{obs}({\mathtt{s}_{k}})|\leq\frac{p}{2^{k}}$
($p,~{}q_{k},~{}\mathtt{s}_{k-1},~{}\mathtt{s}_{k}$ resp. instantiate
$p,q,~{}\mathtt{s},~{}\mathtt{t}$ of Lemma 32).

Let $\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ be the concatenation of
all the finite sequences $\mathtt{s}_{k-1}\rightarrow^{*}\mathtt{s}_{k}$. By
construction, $\lim_{n\to\infty}\langle\mathtt{obs}(\mathtt{m}_{n})\rangle=p$.
We conclude that $p\in\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$.

∎

###  5.4 PARS: Confluence implies $\mathtt{UN^{\mathtt{\infty}}}$

We show that in the case of PARS, confluence (in all its variants) implies
$\mathtt{UN^{\mathtt{\infty}}}$ (Thm. 38) and therefore for each $\mathtt{m}$,
$[\\![\mathtt{m}]\\!]$ is defined.

In this section, we fix a PARS $(\mathsf{m}A,\mathrel{\rightrightarrows})$,
and define
$\mathbf{P}=((\mathsf{m}A,\mathrel{\rightrightarrows}),-^{\scriptscriptstyle{\textsf{NF}}})$
and
$\mathbf{P}_{\scriptscriptstyle{\|\|}}=((\mathsf{m}A,\mathrel{\rightrightarrows}),\|-^{\scriptscriptstyle{\textsf{NF}}}\|)$,
where $-^{\scriptscriptstyle{\textsf{NF}}}$ and
$\|-^{\scriptscriptstyle{\textsf{NF}}}\|$ are as defined in Sec. 5.1.

It is immediate to check that

######  Fact 34.

$\mathbf{P}=((\mathsf{m}A,\mathrel{\rightrightarrows}),-^{\scriptscriptstyle{\textsf{NF}}})$
and
$\mathbf{P}_{\scriptscriptstyle{\|\|}}=((\mathsf{m}A,\mathrel{\rightrightarrows}),\|-^{\scriptscriptstyle{\textsf{NF}}}\|)$
are QARS.

Recall that $\|-^{\scriptscriptstyle{\textsf{NF}}}\|$ is induced by composing
$-^{\scriptscriptstyle{\textsf{NF}}}$ with the norm
$\|~{}\|:\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})\to[0,1]$, and
that letters $\alpha,\beta,\gamma$ denote elements in
$\mathsf{Dst}(\scalebox{0.6}[1.0]{NF}_{\mathcal{A}})$.

First, we observe that

######  Fact 35.

$\mathbf{P}_{\scriptscriptstyle{\|\|}}$ is a boolean QARS.

By Prop. 33, if $\mathbf{P}_{\scriptscriptstyle{\|\|}}$ satisfies confluence
(and therefore $\mathtt{LIMP}$), then
$\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})$ has a greatest element.

We now lift the result to $\mathbf{P}$. Precisely, we prove that for
$\mathbf{P}$, property $\mathtt{LIMP}$ (Def. 29) implies _existence of a
maximal element_ $\alpha$ of $\mathtt{Lim}(\mathtt{m})$. By Prop. 31, $\alpha$
is the greatest element of of $\mathtt{Lim}(\mathtt{m})$. To do so we rely on
the following properties, which we already established in Sec. 4.1.

  * •

$\alpha<\beta$ implies $\|\alpha\|<\|\beta\|$,

  * •

$\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})=\\{\|\beta\|~{}\mid~{}\beta\in\mathtt{Lim}(\mathtt{m})\\}$

######  Lemma 36.

If $\mathbf{P}$ satisfies $\mathtt{LIMP}$, then
$\mathbf{P}_{\scriptscriptstyle{\|\|}}$ also does. Similarly for all variants
of confluence in Def. 27.

######  Proposition 37 (Maximal elements).

If $\mathbf{P}$ satisfies $\mathtt{LIMP}$, then $\mathtt{Lim}(\mathtt{m})$ has
maximal elements.

###### Proof.

By Prop. 31 $\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ has a greatest element.
We observe that if $\alpha\in\mathtt{Lim}(\mathtt{m})$ and $\|\alpha\|$ is
maximal in $\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, then $\alpha$ is maximal
in $\mathtt{Lim}(\mathtt{m})$ (because if $\gamma\in\mathtt{Lim}(\mathtt{m})$
and $\gamma>\alpha$, then $\|\gamma\|>\|\alpha\|$). ∎

######  Theorem 38 (Confluence implies $\mathtt{UN^{\mathtt{\infty}}}$).

Given a PARS, any variant of confluence in Def. 27 implies
$\mathtt{UN^{\mathtt{\infty}}}$.

###### Proof.

The claim follows from Fact 28, Lemma 30, and Propositions 31 and 37. ∎

##  6 Tools for the analysis of QARS

We closed Sec. 4.2.3 with the question:

“Are there _local properties_ which guarantee
$\mathtt{UN^{\mathtt{\infty}}}$?”

This section develops criteria of this kind.

If the result $[\\![\mathtt{m}]\\!]$ of computing $\mathtt{m}$ is well
defined, the next natural question is how to compute it: does it exist a
strategy
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}\
\subseteq\ \rightarrow$ whose limit is guaranteed to be
$[\\![\mathtt{m}]\\!]$? More generally: does it exists a strategy
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}\
\subseteq\ \rightarrow$ whose limit is guaranteed to be a maximal element of
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$, if it exist?

We introduce some tools to help in this analysis. Our focus is on properties
which can be expressed by _local conditions_.

##### The beauty of local.

By local conditions we mean the following: to show that a property $X$ holds
globally (_i.e._  _for each_ two rewrite sequences, $X$ holds), we can show
that $P$ holds locally (_i.e._ for each pair of one-step reductions, _there
exist_ two rewrite sequences such that $X$ holds). This reduces the space of
search for testing the property, a fact that we exploit for instance in the
proofs of Sec. 7.2.

###  6.1 Weighted Random Descent

We present a method to establish –with a _local_ test– that for each element
$\mathtt{m}$ of a QARS, $\mathtt{Lim}(\mathtt{m})$ contains a _unique element_
by generalizing the ARS property of Random Descent. Random Descent is not only
an elegant technique in rewriting, developed in [42, 43], but adapts well and
naturally to limits and to the probabilistic setting (Sec. 6.1).

##### Random Descent.

A reduction $\rightarrow$ has _random descent_ (RD) [32] if whenever a term
$t$ has normal form, then all rewrite sequences from $t$ lead to it, and all
have the same length. The best-known property which implies RD, as first
observed by Newman [32], is the following

_RD-diamond_ : if $s_{1}\leftarrow t\rightarrow s_{2}$ then either
$s_{1}=s_{2}$, or $s_{1}\rightarrow u\leftarrow s_{2}$ for some $u$.

This is only a sufficient condition. Quite surprisingly, Random Descent can be
characterized by a local (one-step) property [42].

##### Weighted Random Descent

We generalize Random Descent to observations. The property $\mathtt{obs}$-RD
states that even though an element $\mathtt{m}$ may have different reduction
sequences, they are all _indistinguishable_ if regarded through the lenses of
$\mathtt{obs}$. That is, if we consider all reduction sequences
$\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ starting from the same
$\mathtt{m}$, they all induce the same $\omega$-chain
$\langle\mathtt{obs}(\mathtt{m}_{n})\rangle$. Obviously, if all
$\omega$-chains from $\mathtt{m}$ are equal, they all have the same limit
$\sup_{n}\\{\mathtt{obs}(\mathtt{m}_{n})\\}$.

The main technical result of the section is a _local characterization_ of the
property (Thm 43), similarly to [42].

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

The QARS $((C,\rightarrow),\mathtt{obs})$ satisfies the following properties
if they hold for each $\mathtt{m}\in C$.

  1. 1.

$\mathtt{obs}$-RD: for each pair of $\rightarrow$-sequences
$\langle\mathtt{r}_{n}\rangle_{n\in\mathbb{N}}$,
$\langle\mathtt{s}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{t}$,
$\mathtt{obs}(\mathtt{t}_{n})=\mathtt{obs}(\mathtt{s}_{n}),~{}\forall n$.

  2. 2.

local $\mathtt{obs}$-RD: if
$\mathtt{r}\leftarrow\mathtt{m}\rightarrow\mathtt{s}$, then there exists a
pair of sequences $\langle\mathtt{r}_{n}\rangle_{n\in\mathbb{N}}$ from
$\mathtt{r}$ and $\langle\mathtt{s}_{n}\rangle_{n\in\mathbb{N}}$ from
$\mathtt{s}$ such that
$\mathtt{obs}(\mathtt{s}_{n})=\mathtt{obs}(\mathtt{r}_{n})$, $\forall n$.

######  Example 40.

Let us consider Call-by-Value $\lambda$-calculus with weak reduction, _i.e._
no reduction is allowed in the scope of $\lambda$. Let $I=\lambda z.z$; the
following are reduction sequences from $(II)(Ix)$.

  1. 1.

$(II)(Ix)\rightarrow_{\beta_{v}}I(Ix)\rightarrow_{\beta_{v}}Ix\rightarrow_{\beta_{v}}x$

  2. 2.

$(II)(Ix)\rightarrow_{\beta_{v}}II(x)\rightarrow_{\beta_{v}}Ix\rightarrow_{\beta_{v}}x$

Let $\mathtt{obs}:\Lambda\to\\{0,1\\}$ be $1$ if the term is a value (_i.e._ ,
a variable or an abstraction), $0$ otherwise. Seen through the lenses of
$\mathtt{obs}$, both sequences appear as $\langle 0,~{}0,~{}0,~{}1\rangle$.

######  Example 41.

In Fig. 5 $\mathtt{obs}$-RD holds for
$\mathtt{obs}=\|-^{\scriptscriptstyle{\textsf{NF}}}\|$, and not for
$\mathtt{obs}=-^{\scriptscriptstyle{\textsf{NF}}}$.

Figure 7: Random Descent Figure 8: Diamond Figure 9: Proof of 43

It is immediate that

######  Proposition 42.

If a QARS $((C,\mathrel{\rightrightarrows}),\mathtt{obs})$ satisfies
$\mathtt{obs}$-RD, then for each $\mathtt{m}\in C$,
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ has a unique element,

While expressive, $\mathtt{obs}$-RD is of little practical use, as it is a
property which is _universally quantified_ on the sequences from $\mathtt{m}$.
The property $\mathtt{obs}$-LRD is instead _local_. Remarkably, _the local
property characterizes_ $\mathtt{obs}$-RD.

######  Theorem 43 (Characterization).

The following properties are equivalent:

  1. 1.

$\mathtt{obs}$-LRD;

  2. 2.

$\forall k,\forall\mathtt{m},\mathtt{u},\mathtt{r}\in C$ if
$\mathtt{m}\rightarrow^{k}\mathtt{u}$ and
$\mathtt{m}\rightarrow^{k}\mathtt{r}$, then
$\mathtt{obs}(\mathtt{u})=\mathtt{obs}(\mathtt{r})$;

  3. 3.

$\mathtt{obs}$-RD.

###### Proof.

The proof is illustrated in Fig. 9.

$\bm{(1\Rightarrow 2)}$. We prove that (2) holds by induction on $k$. If
$k=0$, the claim is trivial. If $k>0$, let $\mathtt{m}\rightarrow\mathtt{s}$
be the first step from $\mathtt{m}$ to $\mathtt{u}$ and
$\mathtt{m}\rightarrow\mathtt{t}$ the first step from $\mathtt{m}$ to
$\mathtt{r}$. By $\mathtt{obs}$-LRD, there exists $\mathtt{s}_{k-1}$ such that
$\mathtt{s}{\rightarrow^{k-1}}\mathtt{s}_{k-1}$ and $\mathtt{t}_{k-1}$ such
that $\mathtt{t}\rightarrow^{k-1}\mathtt{t}_{k-1}$, with
$\mathtt{obs}(\mathtt{s}_{k-1})=\mathtt{obs}(\mathtt{t}_{k-1})$. Since
$\mathtt{s}\rightarrow^{k-1}\mathtt{u}$, we can apply the inductive
hypothesis, and conclude that
$\mathtt{obs}(\mathtt{s}_{k-1})=\mathtt{obs}(\mathtt{u})$. By using the
induction hypothesis on $\mathtt{t}$, we have that
$\mathtt{obs}(\mathtt{t}_{k-1})=\mathtt{obs}(\mathtt{r})$ and conclude that
$\mathtt{obs}(\mathtt{r})=\mathtt{obs}(\mathtt{u})$.

$\bm{(2\Rightarrow 3)}$. Immediate.

$\bm{(3\Rightarrow 1)}$. Assume
$\mathtt{t}\leftleftarrows\mathtt{m}\rightarrow\mathtt{s}$. Take a sequence
$\langle\mathtt{t}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{t}$ and a
sequence $\langle\mathtt{s}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{s}$. By
(3), $\mathtt{obs}(\mathtt{t}_{k})=\mathtt{obs}(\mathtt{s}_{k})$ $\forall k$.
∎

##### A diamond.

A useful case of $\mathtt{obs}$-LRD is the $\mathtt{obs}$-diamond property
(Fig. 9): $\forall\mathtt{m},\mathtt{s},\mathtt{t}$, if
$\mathtt{t}\leftarrow\mathtt{m}\rightarrow\mathtt{s}$, then
$\mathtt{obs}(\mathtt{s})=\mathtt{obs}(\mathtt{t})$, and either
$\mathtt{s}=\mathtt{t}$, or $\exists\mathtt{u}$ s.t.
($\mathtt{t}\rightarrow\mathtt{u}\leftarrow\mathtt{s}$ ) It is easy to check
that $\mathtt{obs}$-diamond $\Rightarrow$ $\mathtt{obs}$-LRD.

######  Proposition 44.

($\mathtt{obs}$-diamond) $\Rightarrow$ ($\mathtt{obs}$-LRD) $\Rightarrow$
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{t})$ contains a unique element.

Note that while $\mathtt{obs}$-LRD  _characterizes_ $\mathtt{obs}$-RD,
$\mathtt{obs}$-diamond is only a _sufficient condition_.

###  6.2  Strategies and Completeness

_Strategies_ are a way to control the non-determinism which arises from
different possible choices of reduction.

##### ARS Strategies.

If $(C,\rightarrow)$ is an ARS, the relation
$\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{s}~{}$}\vss}}}\subseteq\rightarrow$
is a _strategy_ for $\rightarrow$ if it has the same normal forms as
$\rightarrow$.

##### QARS Strategies.

Given a QARS $\mathbf{Q}=(C,\rightarrow,\mathtt{obs})$ we call rewrite
strategy for $\rightarrow$ a relation
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}\subseteq\rightarrow$.
We indicate strategies for $\rightarrow$ by colored arrows
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}$.

Note that the ARS condition “have the same normal forms” is replaced by the
fact that we (tacitly) consider the QARS
$\big{(}(C,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}),\mathtt{obs}\big{)}$,
where the function $\mathtt{obs}$ is the _same_ as for $\mathbf{Q}$.

##### Completeness.

We formulate an asymptotic notion of completeness.

######  Definition 45 (Completeness).

A reduction
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}\subseteq\rightarrow$
is $\mathtt{obs}$-complete (or asymptotically compelte) for $\rightarrow$ if
$\mathtt{t}\rightarrow\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}\bm{\mathtt{q}}$
implies
($\mathtt{t}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}\mkern-2.0mu{}^{\infty}_{\mathtt{obs}}~{}\bm{\mathtt{p}}\geq\bm{\mathtt{q}}$)

Note that a strategy
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}$
which is asymptotically complete is not guaranteed to find the “best” result,
as one can immediately see by noticing that $\rightarrow$ is trivially a
complete strategy for $\rightarrow$ itself. However, it does if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}$
is deterministic, or “essentially” deterministic w.r.t. $\mathtt{obs}$. This
is what the method in section Sec. 6.1 provides.

###  6.3 Comparing Strategies

In this section we refine the results given the previous section into a method
to compare strategies. _When strategy
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}$
is _better_ than strategy
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}$?_.
We adapt to QARS the ARS notion of ” _better_ ” introduced in [42]. Again, we
obtain a local characterization (Th. 47) of the property, similarly to [42].

In Sec. 8 we will analyze these notions in the setting of PARS. What we obtain
are sufficient criteria to establish that a strategy is normalizing or
perpetual (Cor. 62), and to compare the _expected number of steps_ of rewrite
sequences.

The method also provides another sufficient condition to establish
$\mathtt{UN^{\mathtt{\infty}}}$.

Figure 10: $\mathtt{obs}$-better

######  Definition 46 ($\mathtt{obs}$-better).

We define the following properties, which are illustrated in Fig. 10.

  * •

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
is $\mathtt{obs}$-better than
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}}$
($\mathtt{obs}\mbox{-better}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}})$):
for each $\mathtt{m}$ and for each pair of a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$-sequence
$\langle\mathtt{r}_{n}\rangle_{n\in\mathbb{N}}$ and a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}}$-sequence
$\langle\mathtt{u}_{n}\rangle_{n\in\mathbb{N}}$ from $\mathtt{m}$,
$\mathtt{obs}(\mathtt{r}_{k})\geq\mathtt{obs}(\mathtt{u}_{k})$ holds ($\forall
k$).

  * •

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
is locally $\mathtt{obs}$-better than
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}}$
(written
$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}})$):
if
$\mathtt{t}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{~{}{}_{\clubsuit}\leftleftarrows}}\mathtt{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}}\mathtt{s}$,
then for each $k\geq 0$, $\exists\mathtt{s}_{k},\mathtt{t}_{k}$, such that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{s}\rightarrow_{\clubsuit}^{k}\mathtt{s}_{k}}}$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathtt{t}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}^{k}~{}\mathtt{t}_{k}}}$,
and $\mathtt{obs}(\mathtt{t}_{k})\geq\mathtt{obs}(\mathtt{s}_{k})$

It is immediate that
$\mathtt{obs}\mbox{-better}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},\rightarrow)$
implies that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
is $\mathtt{obs}$-complete for $\rightarrow$ (Def. 45). The notion of
$\mathtt{obs}\mbox{-better}$ is another condition which is expressive, but
_quantified over all reduction sequences_ from $\mathtt{m}$. We now prove that
the local property $\mathtt{obs}\mbox{-LB}$ is sufficient to establish
$\mathtt{obs}$-better, and even necessary when comparing with $\rightarrow$.

######  Theorem 47.

$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}})$
implies
$\mathtt{obs}\mbox{-better}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}})$.
The reverse also holds if either
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
or
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}}$
is $\rightarrow$.

###### Proof.

$\boldsymbol{\Rightarrow}.$ The proof is illustrated in Fig. 10. We prove by
induction on $k$ the following:

_$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}})$
implies
$\big{(}\forall k,\forall\mathtt{m},\mathtt{r},\mathtt{u}\in C$, if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{m}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}^{k}\mathtt{r}}}$
and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathtt{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}^{k}\mathtt{u}}}$,
then $\mathtt{obs}(\mathtt{r})\geq\mathtt{obs}(\mathtt{u})\big{)}$ _.

If $k=0$, the claim is trivial. If $k\geq 1$, let
$\mathtt{m}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}\mathtt{s}$
be the first step from $\mathtt{m}$ to $\mathtt{u}$, and
$\mathtt{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}\mathtt{t}$
the first step from $\mathtt{m}$ to $\mathtt{r}$, as in Fig. 10.
$\mathtt{obs}\mbox{-LB}$ implies that exist $\mathtt{s}_{k-1}$ and
$\mathtt{t}_{k-1}$ such that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{s}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}^{k-1}\mathtt{s}_{k-1}}}$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathtt{t}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}^{k-1}~{}\mathtt{t}_{k-1}}}$,
with $\mathtt{obs}(\mathtt{t}_{k-1})\geq\mathtt{obs}(\mathtt{s}_{k-1})$. Since
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathtt{s}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}^{k-1}~{}\mathtt{u}}}$
we can apply the inductive hypothesis, and obtain that
$\mathtt{obs}(\mathtt{s}_{k-1})\geq\mathtt{obs}(\mathtt{u})$. Again by
inductive hypothesis, from
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{t}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}^{k-1}\mathtt{r}}}$
we obtain $\mathtt{obs}(\mathtt{r})\geq\mathtt{obs}(\mathtt{t}_{k-1})$. By
transitivity, it holds that
$\mathtt{obs}(\mathtt{r})\geq\mathtt{obs}(\mathtt{u})$.

$\boldsymbol{\Leftarrow}.$ Assume
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow_{\heartsuit}}}}}=\rightarrow$,
and
$\mathtt{t}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{~{}{}_{\clubsuit}\leftleftarrows}}\mathtt{m}\rightarrow\mathtt{s}$.
Let $\langle\mathtt{t}_{n}\rangle_{n\in\mathbb{N}}$ and
$\langle\mathtt{s}_{n}\rangle_{n\in\mathbb{N}}$ be obtained by extending
$\mathtt{t}$ and $\mathtt{s}$ with a maximal
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
sequence. The claim follows from the hypothesis that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
dominates $\rightarrow$, by viewing the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
steps in $\langle\mathtt{s}_{n}\rangle_{n\in\mathbb{N}}$ as $\rightarrow$
steps. ∎

##### Greatest Element.

Finally, we mention that $\mathtt{obs}\mbox{-LB}$ provides another method to
establish $\mathtt{UN^{\mathtt{\infty}}}$, and therefore the fact that for
each $\mathtt{m}$, $[\\![\mathtt{m}]\\!]$ is defined.

######  Proposition 48 (Greatest Element).

Given $\mathbf{Q}=\\{(C,\rightarrow),\mathtt{obs}\\}$, if there is a strategy
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}}$
such that
$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},\rightarrow)$
then $\mathbf{Q}$ satisfies $\mathtt{UN^{\mathtt{\infty}}}$.

###### Proof.

First, observe that the assumption implies in particular
$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}})$,
and therefore the QARS $((C,\rightarrow),\mathtt{obs})$ satisfies
$\mathtt{obs}$-RD. It follows that, given $\mathtt{m}\in C$, all
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}$-sequences
from $\mathtt{m}$ have the same limit $\bm{p}$.

From
$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rightarrow_{\clubsuit}}}}},\rightarrow)$,
it follows that $\bm{p}$ is the greatest limit of
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$. ∎

######  Remark 49.

Note that $\mathtt{obs}$-RD (resp. $\mathtt{obs}$-LRD) is a special case of
$\mathtt{obs}\mbox{-better}$ (resp. $\mathtt{obs}\mbox{-LB}$). We have
preferred to treat $\mathtt{obs}$-RD independently, for the sake of
presentation.

##  7 PARS: Weighted Random Descent

When applied to PARS, $\mathtt{obs}$-RD is able to guarantee some remarkable
properties : $\mathtt{UN^{\mathtt{\infty}}}$, _$p$ -$\mathtt{SN^{\infty}}$_ as
soon as _there exists a sequence_ which converges to $p$, and also the fact
that all rewrite sequences from a term have the same _expected_ number of
steps.

Take $\mathtt{obs}$ to be either $-^{\scriptscriptstyle{\textsf{NF}}}$ or
$\|-^{\scriptscriptstyle{\textsf{NF}}}\|$, $\mathtt{obs}$-RD implies that all
rewrite sequences from $\mathtt{m}$:

  * •

have the same probability of reaching a normal form after $k$ steps (for each
$k\in\mathbb{N}$);

  * •

converge to the same limit;

  * •

have the same expected number of steps.

######  Proposition 50.

  1. 1.

$\|-^{\scriptscriptstyle{\textsf{NF}}}\|$-RD implies
$\mathtt{SN^{\infty}}$_(_uniform normalization_)_; moreover, for each
$\mathtt{m}\in\mathsf{m}A$ all elements in
$\mathtt{Lim}_{\mathtt{obs}}(\mathtt{m})$ are maximal.

  2. 2.

$-^{\scriptscriptstyle{\textsf{NF}}}$-RD implies $\mathtt{SN^{\infty}}$and
$\mathtt{UN^{\mathtt{\infty}}}$.

##### Point-wise formulation.

In section 7.2, we exploit the fact that not only $\mathtt{obs}$-RD admits a
local characterization, but also that the properties $\mathtt{obs}$-LRD and
$\mathtt{obs}$-diamond can be expressed point-wise, making the condition even
easier to verify.

  1. 1.

pointed $\mathtt{obs}$-LRD: $\forall a\in A,$ if
$\mathtt{t}\leftleftarrows[a^{1}]\mathrel{\rightrightarrows}\mathtt{s}$, then
$\forall k,\exists\mathtt{s}_{k},\mathtt{t}_{k}$ with
$\mathtt{s}\mathrel{\rightrightarrows}^{k}\mathtt{s}_{k}$,
$\mathtt{t}\mathrel{\rightrightarrows}^{k}\mathtt{t}_{k}$, and
$\mathtt{obs}(\mathtt{s}_{k})=\mathtt{obs}(\mathtt{t}_{k})$.

  2. 2.

pointed $\mathtt{obs}$-diamond: $\forall a\in A,$ if
$\mathtt{t}\leftleftarrows[a^{1}]\mathrel{\rightrightarrows}\mathtt{s}$, then
it holds that $\mathtt{obs}(\mathtt{t})=\mathtt{obs}(\mathtt{s})$, and
$\exists\mathtt{r}$ such that
$\mathtt{t}\mathrel{\rightrightarrows}\mathtt{r}\leftleftarrows\mathtt{s}$.

######  Proposition 51 (point-wise $\mathtt{obs}$-LRD).

The following hold

  * •

$\mathtt{obs}$-LRD iff pointed $\mathtt{obs}$-LRD;

  * •

$\mathtt{obs}$-diamond iff pointed $\mathtt{obs}$-diamond.

###### Proof.

Immediate, by the definition of $\mathrel{\rightrightarrows}$. Given
$\mathtt{m}=[p_{i}a_{i}]_{i\in I}$, we establish the result for each $a_{i}$,
and put all the resulting multidistributions together. ∎

###  7.1 Expected Termination Time

For ARS, Random Descent captures the property (Length) “ _all maximal rewrite
sequences from a term have the same length_.”

$\mathtt{obs}$-RD also implies a property similar to (Length) for PARS, where
we consider not the number of steps of the rewrite sequences, but its
probabilistic analogue, the expected number of steps.

In an ARS, if a maximal rewrite sequence terminates, the number of steps is
finite; we interpret this number as _time to termination_. In the case of
PARS, a system may have infinite runs even if it is AST; the number of rewrite
steps $\rightarrow$ from an initial state is (in general) infinite. However,
what interests us is its _expected value_ , _i.e._ the weighted average w.r.t.
probability (see Sec. 2.2) which we write
ETime($\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$). This expected value
can be finite; in this case, not only the system is AST, but is said PAST
_(Positively AST)_ (see [5]).

######  Example 52.

An example of probabilistic system with finite expected time to termination is
the one in Fig. 3. The reduction from $c$ has ETime $2$. We can see this
informally, recalling Sec. 2.2. Let the sample space $\Omega$ be the set of
paths ending in a normal form, and let $\mu$ be the probability distribution
on $\Omega$. What is the expected value of the random variable
$\texttt{length}:\Omega\to\mathbb{N}$? We have
$E(\texttt{length})=\sum_{\omega}\texttt{length}(\omega)\cdot\mu(\omega)=$
$\sum_{n\in\mathbb{N}}n\cdot\mu\\{\omega\mid\texttt{length}(\omega)=n\\}=$
$\sum n\cdot\frac{1}{2^{n}}=2$.

[4] makes a nice observation: the expected number of steps of a rewrite
sequence $\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$ admits a very simple
formulation, as follows:

ETime($\langle\mathtt{m}_{n}\rangle_{n\in\mathbb{N}}$)=
$\sum_{n\in\mathbb{N}}(1-\|\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}\|)$

Intuitively, each tick in time (_i.e._ each $\mathrel{\rightrightarrows}$
step) is weighted with its probability to take place, which is
$\mu_{i}\\{c\mid
c\not\in\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}\\}=1-\|\mathtt{m}_{i}^{\scriptscriptstyle{\textsf{NF}}}\|$
(where $\mu_{i}$ is the distribution over $A$ associated to $\mathtt{m}_{i}$).
We refer to [4] for the details.

######  Example 53.

It is immediate to check that in Example 7, the (only) rewrite sequence
$\mathfrak{s}$ from $[a^{1}]$ has
$\texttt{ETime}(\mathfrak{s})=\sum_{n\in\mathbb{N}}\frac{1}{2^{n}}=2$.

Using this formulation, the following result is immediate.

######  Corollary 54.

Let $\mathtt{m}\in\mathsf{m}A$. $\|-^{\scriptscriptstyle{\textsf{NF}}}\|$-RD
implies that all maximal rewrite sequences from $\mathtt{m}$ have the _same
ETime_.

The well-known consequence is that
$\sum_{n}(1-\|\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}\|)<\infty$
implies
$\lim_{n\to\infty}(1-\|\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}\|)=0$,
hence
$\lim_{n\to\infty}\|\mathtt{m}_{n}^{\scriptscriptstyle{\textsf{NF}}}\|=1$.
Cor. 54 means that if there exists _one_ sequence from $\mathtt{m}$ with
_finite_ ETime, all do, hence $\mathtt{m}$ is AST and PAST.

###  7.2 Analysis of probabilistic reduction: _weak_ CbV $\lambda$-calculus

We define $\Lambda_{\oplus}^{\texttt{weak}}$, a probabilistic analogue of
call-by-value $\lambda$-calculus (see Sec. 1.2). Evaluation is non-
deterministic, because in the case of an application there is no fixed order
in the evaluation of the left and right subterms (see Example 55). We show
that $\Lambda_{\oplus}^{\texttt{weak}}$ satisfies
$-^{\scriptscriptstyle{\textsf{NF}}}$-RD. Therefore it has remarkable
properties (Cor. 60), analogous to those of its classical counter-part: the
choice of the redex is irrelevant with respect to the _final result_ , to its
_approximants_ , and to the _expected number of steps_.

####  7.2.1 The syntax

The set $\Lambda_{\oplus}$ of terms ($M,N,P,Q$) and the set $\mathcal{V}$ of
values ($V,W$) are defined as follows:

$\begin{array}[]{lllc lll}M&{:}{:}{=}&x\mid\lambda x.M\mid MM\mid M\oplus
M&&V&{:}{:}{=}&x\mid\lambda x.M\end{array}$

Free variables are defined as usual. A term $M$ is closed if it has no free
variable. The substitution of $V$ for the free occurrences of $x$ in $M$ is
denoted $M[x:=V]$.

#####  pars.

The pars $(\Lambda_{\oplus},\rightarrow)$ is given by the set of terms
together with the relation
$\rightarrow\subseteq\Lambda_{\oplus}\times\mathsf{Dst^{F}}(\Lambda_{\oplus})$
which is inductively defined by the rules below.

$\begin{array}[]{l }(\lambda x.M)V\rightarrow\\{M[x:=V]^{1}\\}\\\ P\oplus
Q\rightarrow\\{P^{1/2}\\}+\\{Q^{1/2}\\}\\\ \end{array}$ $\begin{array}[]{l
}MN\rightarrow\\{(MN_{i})^{p_{i}}\mid i\in
I\\}N\rightarrow\\{N_{i}^{p_{i}}\mid i\in I\\}\quad
MN\rightarrow\\{(M_{i}N)^{p_{i}}\mid i\in I\\}M\rightarrow\\{M_{i}^{p_{i}}\mid
i\in I\\}\end{array}$

##### PARS $\Lambda_{\oplus}^{\texttt{weak}}$.

The calculus $\Lambda_{\oplus}^{\texttt{weak}}$ is the PARS
$(\mathsf{m}\Lambda_{\oplus},\mathrel{\rightrightarrows})$, where
$\mathsf{m}\Lambda_{\oplus}$ is the set of multidistributions on
$\Lambda_{\oplus}$, and
$\mathrel{\rightrightarrows}\subseteq\mathsf{m}\Lambda_{\oplus}\times\mathsf{m}\Lambda_{\oplus}$
is the lifting (as defined in ) of $\rightarrow$.

####  7.2.2 Examples

######  Example 55 (Non-deterministic evaluation).

A term may have several reductions. The two reductions here join in one step:
$\big{[}P[x:=Q](A\oplus B)\big{]}\leftleftarrows[((\lambda x.P)Q)(A\oplus
B)]\rightrightarrows[\frac{1}{2}(\lambda x.P)QA,\frac{1}{2}(\lambda x.P)QB]$.

######  Example 56 (Infinitary reduction).

Let $R=(\lambda x.xx\oplus{\texttt{T}})(\lambda x.xx\oplus{\texttt{T}})$. We
have $[R^{1}]\xRightarrow{\infty}\\{{\texttt{T}}^{1}\\}$. This term models the
behaviour we discussed in Fig.3.

######  Example 57 (Fix-Points).

$\Lambda_{\oplus}^{\texttt{weak}}$ is expressive enough to allow fix-point
combinators. A simple one is Turing combinator $\Theta=AA$ where $A=\lambda
xf.f(xxf)$. For each value $F$, $\\{\Theta
F\\}\mathrel{\rightrightarrows}^{*}\\{F(\Theta F)\\}$.

######  Example 58.

The term $PR$ in Example 2 has (among others) the following reduction. $[PR]$
$\mathrel{\rightrightarrows}[\frac{1}{2}P({\texttt{T}}\oplus{\texttt{F}}),\frac{1}{2}P(\Delta\Delta)]$
$\mathrel{\rightrightarrows}$
$[\frac{1}{4}P({\texttt{T}}),\frac{1}{4}P({\texttt{F}}),\frac{1}{2}P(\Delta\Delta)]$
$\mathrel{\rightrightarrows}^{*}$
$[\frac{1}{4}({\texttt{T}}\mathtt{~{}XOR~{}}{\texttt{T}}),\frac{1}{4}({\texttt{F}}\mathtt{~{}XOR~{}}{\texttt{F}}),\frac{1}{4}\Delta\Delta]$
$\mathrel{\rightrightarrows}$
$[\frac{1}{4}{\texttt{F}},\frac{1}{4}{\texttt{F}},\frac{1}{2}\Delta\Delta]\dots$
We conclude that $PR\xRightarrow{\infty}\\{{\texttt{F}}^{1/2}\\}$.

####  7.2.3 Properties

######  Theorem 59.

$\Lambda_{\oplus}^{\texttt{weak}}$ satisfies $\mathtt{obs}$-RD, with
$\mathtt{obs}=-^{\scriptscriptstyle{\textsf{NF}}}$

###### Proof.

We prove the $\mathtt{obs}$-diamond property, using the definition of lifting
and induction on the structure of the terms (see Appendix). ∎

Therefore, by Sec. 7, each $\mathtt{m}$ satisfies the following properties:

######  Corollary 60.

  * •

_All_ rewrite sequences from $\mathtt{m}$ converge to the same limit
distribution.

  * •

_All_ rewrite sequences from $\mathtt{m}$ have the same _expected_ termination
time ETime.

  * •

If $\mathtt{m}\mathrel{\rightrightarrows}^{k}\mathtt{s}$ and
$\mathtt{m}\mathrel{\rightrightarrows}^{k}\mathtt{t}$, then
$\mathtt{s}^{\scriptscriptstyle{\textsf{NF}}}=\mathtt{t}^{\scriptscriptstyle{\textsf{NF}}}$,
$\forall\mathtt{s},\mathtt{t},k$.

##### More diamonds.

Call-by-Name $\lambda$-calculus also has a variant of head reduction which is
non-deterministic, but satisfy Random Descent; a most well-known calculus with
similar properties is surface reduction in Simpson’s linear $\lambda$-calculus
[40]. [19] uses a probabilistic extension of both these calculi – they satisfy
similar properties as those of $\Lambda_{\oplus}^{\texttt{weak}}$.

Another calculus which satisfy Random Descent is Lafont’s interaction nets
[29] – we expect that its extension with a probabilistic choice would also
satisfy Weighted Random Descent.

##  8 PARS: Comparing Strategies

In this section, we briefly examine the notion of $\mathtt{obs}\mbox{-better}$
in the setting of PARS. We focus on the following question:

“is there a strategy which is guaranteed to reach a normal form

with greatest probability”?

##### ARS Normalizing Strategies.

The strategy $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{s}~{}$}\vss}}}\subseteq\rightarrow$
is a _normalizing strategy_ for $\rightarrow$ if whenever $c\in A$ has a
normal form, then _every_ maximal $\mathrel{\mathop{\rightarrow}\limits_{\vbox
to0.0pt{\kern-6.0pt\hbox{$\scriptstyle\textsc{s}~{}$}\vss}}}$-sequence from
$c$ ends in a normal form.

##### PARS Normalizing Strategies

Let $(\mathsf{m}A,\mathrel{\rightrightarrows})$ be a PARS. We recall that
$\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})=\\{p\mid\mathtt{m}\xRightarrow{\infty}_{\scriptscriptstyle{\|\|}}p\\}$.
We write $q\geq\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})$ if $q\geq
p,\forall p\in\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})$; similarly
for $\leq$.

######  Definition 61.

Given a PARS $(\mathsf{m}A,\mathrel{\rightrightarrows})$, a strategy
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}$
for $\mathrel{\rightrightarrows}$ is (asymptotically) normalizing if for each
$\mathtt{m}$, _each_
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}$-sequence
starting from $\mathtt{m}$ converges with the same probability
$p_{\max}(\mathtt{m})\geq\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})$.
A strategy
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrel{\rightrightarrows}_{\heartsuit}}}}$for
$\mathrel{\rightrightarrows}$ is (asymptotically) perpetual if for each
$\mathtt{m}$, each
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrel{\rightrightarrows}_{\heartsuit}}}}$
sequence from $\mathtt{m}$ converges with the same probability
$p_{\min}(\mathtt{m})\geq\mathtt{Lim}_{\scriptscriptstyle{\|\|}}(\mathtt{m})$.

It is immediate that
$\mathtt{obs}\mbox{-better}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}},\mathrel{\rightrightarrows})$
with $\mathtt{obs}=\|-^{\scriptscriptstyle{\textsf{NF}}}\|$ implies that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}}$
is normalizing. By using the results in Sec. 6.3, we have a method to prove
that a strategy is normalizing or perpetual by means of a local condition.

######  Corollary 62 (Normalizing criterion).

Let $\mathtt{obs}$ be $\|-^{\scriptscriptstyle{\textsf{NF}}}\|$. It holds
that:

  1. 1.

$\mathtt{obs}\mbox{-LB}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}},{\mathrel{\rightrightarrows}})$
implies that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}}$
is _asymptotically normalizing_.

  2. 2.

$\mathtt{obs}\mbox{-LB}(\mathrel{\rightrightarrows},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrel{\rightrightarrows}_{\heartsuit}}}}})$
implies that
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrel{\rightrightarrows}_{\heartsuit}}}}}$
is _asymptotically perpetual_.

##### Expected Number of Steps.

Let $\mathtt{obs}=\|-^{\scriptscriptstyle{\textsf{NF}}}\|$. It is easy to
check that
if,$\mathtt{obs}$-better$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}},\mathrel{\rightrightarrows})$
holds, and $\mathfrak{s}$ is a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrel{\rightrightarrows}_{\clubsuit}}}}}$-sequence,
then ETime($\mathfrak{s}$) $\leq$ETime($\mathfrak{t}$), for each
$\mathfrak{t}$ $\mathrel{\rightrightarrows}$-sequence. Therefore, with a
similar argument as in Sec.7.1, we have a criterion to establish not only that
a strategy is normalizing (resp. perpetual), but also minimality (resp.
maximality) of the _expected termination time_.

##  9 Further work. A larger example of application

It is illustrate an example of application of the tools which we have
developed. We do so by summarizing further work [19] where for each of the
following, Plotkin’s Call-by-Value [34], Call-by-Name, and Simpson’s linear
$\lambda$-calculus [40], a fully fledged probabilistic extension is developed.
Each probabilistic calculus satisfies confluence, and a form of
standardization (surface standardization). To obtain confluence, only the
probabilistic reduction is constrained, while $\beta$ reduction is
unrestricted. In the three calculi, the role of asymptotically standard
strategy is played by a reduction which is non-deterministic but satisfy
Random Descent – this is necessary for technical reasons, because with the
(usual) deterministic strategy, a standardization result for finite sequences
fails.

Let us see some details.

The notion of result which is studied in [19] are, respectively, values in
CbV, head normal forms in CbN, and surface normal forms in the linear
calculus. Once confluence is established, [19] relies on the abstract results
given in Sec. 5.4 to conclude that –in each calculus– the evaluation of a
program $\mathtt{m}$ leads to a unique maximal result $[\\![\mathtt{m}]\\!]$ –
the greatest limit distribution.

[19] then studies the question _“is there a strategy which is guaranteed to
reach the unique result (_asymptotic standardization_)?”_. Again, key elements
rely on the abstract tools developed here; let us sketch the construction.

We focus on the CbV calculus, namely
$\Lambda_{\oplus}^{\mathtt{cbv}}=(\mathsf{m}\Lambda_{\oplus},\Rightarrow)$,
where $\mathsf{m}\Lambda_{\oplus}$ is as in Sec. 7.2, and $\Rightarrow$ is the
(more general) reduction which is defined in [19]. The role of standard
strategy is played by a relation $\Rightarrow_{s}\subseteq\Rightarrow$ which
is a (more relaxed) lifting of the weak reduction $\rightarrow$ defined in
Sec. 7.2. The construction then goes as follows.

  1. 1.

First, it is proved that $\Rightarrow_{s}$ is asymptotically complete for
$\Rightarrow$. Note however that $\Rightarrow_{s}$ is not guaranteed to
compute $[\\![\mathtt{m}]\\!]$.

  2. 2.

It is observed that the relation $\mathrel{\rightrightarrows}$ as defined in
Sec. 7.2 is asymptotically complete for $\Rightarrow_{s}$, and therefore for
$\Rightarrow$.

  3. 3.

The properties of $\mathrel{\rightrightarrows}$ which are proved in Sec. 7.2
guarantee that, from $\mathtt{m}$, the limit of _any_
$\mathrel{\rightrightarrows}$-sequence is _the same_ , and it is exactly
$[\\![\mathtt{m}]\\!]$.

A similar reasoning apply to Call-by-Name.

Point 3. has another implication: for both CbN and CbV, the leftmost strategy
reaches the best possible limit distribution (respectively over value and over
head normal forms). This is remarkable for two reasons. First –as we already
observed in Sec. 1.1– the leftmost strategy is the deterministic strategy
which has been adopted in the literature of probabilistic $\lambda$-calculus,
in either its CbV ([28, 10]) or its CbN version ([14, 17]), but without any
completeness result with respect to _probabilistic_ computation. [19] offers
an “a-posteriori” justification for its use. Second, the result is non-
trivial, because in the probabilistic case, a standardization result for
finite sequences using the leftmost strategy fails for both CbV and CbN. To
use the tools in Sec. 7 allow for an elegant solution.

##  10 Conclusions

The motivation behind this work is the need for theoretical tools to support
the study of operational properties in probabilistic computation, similarly to
the role that ARS have for classical computation.

We have investigated several abstract properties of probabilistic rewriting,
and how the behavior of different rewrite sequences starting from the same
element compare w.r.t. normal forms. To guarantee that the result of a
computation is well defined, we have introduced and studied the property
$\mathtt{UN^{\mathtt{\infty}}}$, a robust probabilistic analogue of the notion
of unique normal form. In particular, we have analyzed its relation with
(various notions of) confluence. We also investigated relations with
normalization ($\mathtt{WN^{\infty}}$) and termination
($\mathtt{SN^{\infty}}$), and between these notions. We have developed the
notions of $\mathtt{obs}$-RD and $\mathtt{obs}\mbox{-better}$ as tools to
analyze and compare PARS strategies. $\mathtt{obs}$-RD is an alternative to
strict determinism, analogous to Random Descent for ARS (non-determinism is
irrelevant w.r.t. a chosen event of interest). The notion of
$\mathtt{obs}\mbox{-better}$ provides a sufficient criterion to establish that
a strategy is _normalizing_ (resp. _perpetual_) _i.e._ the strategy is
guaranteed to lead to a result with maximal (resp. minimal) probability.

We have illustrated our techniques by studying a probabilistic extension of
weak call-by-value $\lambda$-calculus; it has analogous properties to its
classical counterpart: all rewrite sequences converge to the _same result_ ,
in the same _expected number of steps_.

##### One-Step Reduction and Expectations.

In this paper, we focus on _normal forms_ and properties related to the event
$\scalebox{0.6}[1.0]{NF}_{\mathcal{A}}$. However, we believe that the methods
would allow us to compare strategies w.r.t. other properties and random
variables of the system. The formalism seems especially well suited to express
the _expected value_ of random variables. A key feature of the binary relation
$\mathrel{\rightrightarrows}$ is to exactly capture the ARS notion of _one-
step reduction_ (in contrast to _one or no step_), with a gain which is two-
folded.

  1. 1.

_Probability Theory_. Because all terms in the distribution are forced to
reduce at the same pace, a rewrite sequence faithfully represents the
evolution in time of the system (_i.e._ if
$\mathtt{m}\mathrel{\rightrightarrows}^{i}\mathtt{m}_{i}$, then
$\mathtt{m}_{i}$ captures the state at time $i$ of all possible paths
$a_{0}\rightarrow\dots\rightarrow a_{i}$). This makes the formalism well
suited to express the expected value of stochastic processes.

  2. 2.

_Rewrite Theory_. The results in Sections 6.1, 6.3, 7.2, crucially rely on
_exactly_ one-step reduction. The reason why this is crucial, is similar to
the classical fact that termination follows from normalization by the diamond
property [Newman 1942], but not by the very similar property $b\leftarrow
a\rightarrow c\Rightarrow\exists d~{}(b\rightarrow^{=}d~{}{}^{=}\leftarrow c$)
(see [Terese], 1.3.18).

##### Finite Approximants.

$\mathtt{obs}$-RD characterizes the case when (not only at the limit, but also
at the level of the approximants) the non-deterministic choices are
irrelevant. The notion of approximant which we have studied here is “stop
after a number $k$ of steps” ($k\in\mathbb{N}$ ). We can consider different
notion of approximants. For example, we could also wish to stop the evolution
of the system when it reaches a normal form with probability $p$. Our method
can easily be adapted to analyze this case. We believe it is also possible to
extend to the probabilistic setting the results in [43], which would go
further in this direction.

##### Further and future work.

In this paper, we have studied existence and uniqueness of the result of
asymptotic computation. The next goal is to study how to compute such a
result, _i.e._ the study of reduction strategies – this is the object of
current investigation.

[42] makes a convincing case of the power of the RD methods for ARS, by using
a large range of examples from the literature, to elegantly and uniformly
revisit normalization results of various $\lambda$-calculi. We cannot here,