In this work we study randomised reduction strategies- a notion already known in the context of abstract reduction systems-for the -calculus. We develop a simple framework that allows us to prove a randomised strategy to be positive almost-surely normalising. Then we propose a simple example of randomised strategy for the -calculus that has such a property and we show why it is non-trivial with respect to classical deterministic strategies such as leftmost-outermost or rightmostinnermost. We conclude studying this strategy for the affine -calculus, where duplication is syntactically forbidden.
There are different possible strategies you can follow to evaluate expressions.
Some are better than others, and bring you to the result in a lower number of
steps. Since programs in pure functional languages are essentially expressions, the
problem of defining good strategies is particularly interesting. Finding minimal
strategies, i.e. strategies that minimise the number of steps to normal form, seems
even more interesting. However, the problem of picking the redex leading to
the reduction sequence of minimal length has been proven undecidable for the
-calculus [3, Section 13.5], the paradigmatic pure functional language. In the
last decades several reduction strategies have been developed. Their importance
is crucial in the study of evaluation orders in functional programming languages,
which is one of their main characteristics and defines an important part of their
semantics. The reader can think about the differences between Haskell
(call-byneed ) and Caml (call-by-value). The -calculus is a good abstraction to study
reduction mechanisms because of its very simple structure. In fact, although
Turing-complete, it can be seen as a rewriting system [
Inria/JSPS EA Crecogi. An Extended Version with more details is available [
Example 1. Let ! = x:xx and = !!. We now consider the reduction of the term ( x:y) according to two different reduction strategies, namely leftmostoutermost (LO) and rightmost-innermost (RI). The term is a looping combinator i.e. it reduces to itself. However, in ( x:y) the argument is discarded since the function returns the constant y. Thus leftmost-outermost (akin to call-by-name in functional programming languages) yields a normal form in one step. Conversely, rightmost-innermost (akin to callby-value) continues to evaluate the argument ( x:y) , though it is useless, and rewrites always the same term, yielding to a non-terminating process. Example 2. Let I = x:x. We now consider the reduction of the term ( x:xx)(II), according to LO and RI strategies, as above.
( x:xx)(II) ( x:xx)(II) !LO (II)(II) !RI ( x:xx)I !LO I(II) !LO II
!LO I !RI II !RI I Here the argument II is duplicated and thus it is much more convenient to reduce it before it is copied, as in rightmost-innermost. Leftmost-outermost does, indeed, some useless work.
In general, innermost strategies are considered more efficient, because programs
often need to copy their arguments (as in Example 2). However, as seen in
Example 1, rightmost-innermost is not normalising: there exist terms which have
a normal form which, however, can be missed by innermost strategies. Instead, a
classical result by Curry and Feys [
In this work we consider a simple randomised reduction strategy P", where
the LO-redex is reduced with probability " and the RI-redex is reduced with
probability 1 ". This is not necessarily the most interesting example, but
certainly a good starting point in our investigation. The uniform randomised
strategy which picks one between all the redexes in the term uniformly at
random looks more natural, although much more difficult to analyse: there is
no fixed lower bound on the probability of picking the standard redex, i.e. the
leftmost-outermost one. The following are our main results:
For every, 0 < " 1, the strategy P" is positive almost-surely normalising on
weakly normalising terms. That means that if a term M is weakly normalising,
then the expected number of reduction steps from M to its normal form with
strategy P" is finite. This is in contrast to the rightmost-innermost strategy,
as can be seen from Example 1. Rightmost-innermost, in other words, is the
only non normalising strategy in the family fP"g0 " 1, namely P0.
The family of strategies fP"g0<"<1 is shown to be non-trivial. In other words,
there exists a class of terms and 0 < < 1 for which P outperforms, on
average, both LO and RI. This shows that randomisation can indeed be
useful in this context. This is not surprising: in computer science there are
a lot of examples where adding a random factor improves performances,
e.g. in randomised algorithms, which are often faster (in average) than their
deterministic counterparts [
The expected number of reduction steps to normal form with strategy P", seen as a function on ", has minimum in 1 for terms in the affine -calculus
A.
The rest of this paper is structured as follows. In Section 2 basic definitions and results for the untyped -calculus are given. In Section 3 we present our model of fully probabilistic abstract reduction system and we give a sufficient condition to prove positive almost-sure termination. In Section 4 we apply this model to the -calculus, defining a randomised reduction strategy and collecting some results. Section 5 contains the conclusions with some ideas for further investigations on the subject.
Our interest in randomised strategies comes from some interesting and insightful discussions the first author had with Prakash Panangaden. 2
The following definitions are standard and are adapted from [
the language of terms defined by the following grammar:
M; N ::= x 2 V j M N j x:M We denote by the set of all -terms. As usual, -terms are taken modulo equivalence, which allows to appropriately define the capture-avoiding substitution of all the free occurrences of x for N in M , denoted M fN=xg.
Reduction will be defined based on the notion of a context, which needs to be given a formal status. Definition 2. We define (one-hole) contexts by the following grammar: C; D ::= j CM j M C j x:C We denote with
the set of all contexts.
Intuitively, contexts are -terms with a hole that can be filled with another -term. We indicate with C[M ] the term obtained by replacing with M in C. Those -terms in the form R = ( x:M )N are called -reducible expressions or -redexes and M fN=xg is said to be the contractum of R. This is justified by the following definition.
, is defined as ! = f(C[( x:M )N ]; C[M fN=xg]) j M; N 2 ; C 2 g: The relation of ANF- -reduction, , is defined by ! ANF ! = f(C[( x:M )N ]; C[M fN=xg]) j M; N 2 ANF ; N is in normal form; C 2 g:
We can see the -calculus defined above as an abstract reduction system
(ARS) [
Two Subcalculi of There are interesting subsets of the -calculus. In particular we focus our attention on two subsystems where terms satisfy a predicate on the number of occurrences of free variables. These systems are meaningful because they are stable w.r.t.
-reduction i.e. if M 2 S and M ! N then N 2 S. A comprehensive treatment
is in [
The I-calculus. The I-calculus was the original calculus studied by Alonzo
Church in the ’30 [
I-terms, weak normalisation implies strong normalisation: in other words, all strategies are qualitatively equivalent. This does not mean, however, that they are quantitatively equivalent.
The A-calculus. The A-calculus is the dual of I-calculus and it is sometimes called affine -calculus in the literature. It is a very weak calculus in which variables bound by abstractions occur at most once free in the abstraction’s body, thus forbidding duplication. The A-calculus is strongly normalising, in a very strong sense: every reduction sequence from a term M has length bounded by the size of M .
Reduction Strategies ARSs are sets endowed with a relation, and are thus inherently nondeterministic. The notion of reduction strategy allows us to fix one redex among the available ones, thus turning reduction into a deterministic process.
Definition 4 (Deterministic Strategies). Given an ARS (A; !), a deterministic reduction strategy for A is a partial function S : A * A such that S(a) is defined iff a is not in normal form and a ! S(a) whenever S(a) is defined. If : a0 ! a1 ! ! an is a reduction sequence with strategy S and an is in normal form, we write StepsS(a0) = n = j j. If : a0 ! a1 ! is infinite, we say that StepsS(a0) = +1. We define two reduction strategies for the -calculus that will be useful in the following sections.
Definition 5. Leftmost-outermost (LO) is a deterministic reduction strategy in which LO(M ) = N if and only if M ! N and the redex contracted in M is the leftmost among the ones in M (measuring the position of a redex by its beginning). If LO(M ) = N , we write M !LO N .
Definition 6. Rightmost-innermost (RI) is a deterministic reduction strategy in which RI(M ) = N if and only if M ! N and the redex contracted in M is the rightmost among the ones in M (measuring the position of a redex by its beginning). Again, if RI(M ) = N , we write N !RI N .
!
N , then StepsLO(N ) StepsLO(M ). 3
We introduce now a framework suitable to define randomised strategies. In particular, we shift the notion of ARS to the fully probabilistic case. With respect to standard Markov chain theory, our construction is simpler and allows to reason better in an infinite state context. The first preliminary concept we need is that of a distribution.
Definition 7 (Distribution). A partial probability distribution over a
countable set A is a mapping : A ! [0; 1] such that j j 1 where j j = P (a). We
a2A
denote the set of partial probability distributions over A by PDist (A). The support
of a partial distribution 2 PDist (A) is the set Supp ( ) = fa 2 A j (a) > 0g. A
probability distribution over a countable set A is a partial probability distribution
such that j j = 1. Dist (A) denotes the set of probability distributions over A.
Strategies as from Definition 4 are inherently deterministic: the process of picking
a reduct among the many possible ones can only have one outcome. But what if
this process becomes probabilistic? This is captured by the following notion:
Definition 8 (Randomised Strategies). Given an ARS (S; !), a randomised
reduction strategy P for (S; !) is a partial function such that if s 2 S is in normal
form, then P(s) = ?, otherwise P(s) = 2 Dist (S), and Supp ( ) ft j s ! tg.
Please notice that if (S; !) is an ARS and P is a randomised reduction strategy
for it, then (S; P) can be seen as a fully probabilistic abstract reduction system
(FPARS), namely a probabilistic abstract reduction system [
The dynamics of an FPARS can be handled by way of an appropriate notion of a configuration, on which an evolution function can be defined: Definition 9 (Configurations, Computations). Let (S; P) be an FPARS and s; t 2 S be two states. We define the probability P (s ! t) of a transition from s to t:
P (s ! t) = ( (t) if P (s) = ;
0 if P (s) = ?:
PDist (S). The evolution of an FPARS (S; P) from a configuration is a function
E ( ) = where (s) = X
(t) P (t ! s) for every s 2 S: t2S If E ( ) =
we write i i+1.
. A computation is any sequence ( i)i2N, such that Remark 1. Those computations ( i)i2N where 0 is Dirac (i.e. there exists s 2 S such that 0(s) = 1) are particularly interesting: they model the evolution of an FPARS starting from one state. We write in this case 0 = Dirac(s). Example 3. Consider an ARS (S; !), where S = fa; bg and ! = f(a; a); (a; b)g. We define a randomised strategy P on top of (S; !). P(a) = such that (a) = (b) = 12 , while P(b) = ? since b is in normal form. A computation ( i)i2N starting from 0 = Dirac(a) has the following form. Definition 10. Let (S; P) be an FPARS and 0 = Dirac(s), where s 2 S. Given 1 the computation ( i)i2N, StepsP(s) = P j ij.
i=1
Observe that the definition above collapses to the one given for the deterministic
case when P is deterministic. That it is the expected value of a random variable
capturing the number of reduction steps to normal form from s can be proved
by standard arguments from the theory of Markov Chains, see [
Example 4. Consider the same setting of Example 3. It is easy to see that (S; P) is AST since n !lim+1 j nj = n !lim+1 2n1 1 = 0. Moreover (S; P) is PAST since StepsP(a) = P1 j nj = nP1=1 2n1 1 = 2 and StepsP(b) = 0.
n=1 It is well-known from Markov chain literature that AST does not imply PAST e.g. in the symmetric random walk on Z. We recall a standard result in Markov chain theory that gives a sufficient condition for PAST and a bound on the average number of steps to normal form.
Notation 1. For " > 0 we write x >" y if and only if x well-founded on real numbers with a lower bound. y + ". This order is
Lyapunov if:
There exists " > 0 such that for every s 2 S if P (s) = , then V (s) >" V ( ), where V is extended to partial distributions as follows:
V ( ) = X V (t)
(t) : t2S Remark 2. Without loss of generality, given a Lyapunov function V we can always consider a new Lyapunov function W (s) 0 for each s 2 S simply adding a constant to V .
Theorem 1 (Foster [
We define here a randomised strategy P" for the ARS ( ; ! ). Given a reducible term M , P"(M ) = such that for each N 2 :
>8" (N ) = <1 >:0
if M ! N and the LO-redex is reduced, " if M ! N and the RI-redex is reduced,
otherwise: In this way we have defined an FPARS ( ; P"). y "
Notation 2. For the FPARS ( ; P") we define the function ExpLenM : [0; 1] ! R where ExpLenM (") = StepsP" (M ).
Example 5. Let us consider the term M = ( x:y) where = !! with ! = x:xx. There are two possible representations of the development of the strategy P" for this term, one as an infinite tree (Figure 1a) and another one as a cyclic graph (Figure 1b). According to the different representations, we can compute in different ways the probability of reaching normal form and the average derivation length. The results coincide yielding in both cases probability of termination equal to 1 and average derivation length equal to 1" .
Theorem 2. The FPARS ( WN; P") is PAST whenever " > 0.
Proof. We use Foster’s Theorem to prove the claim. Thus, we have to find a suitable Lyapunov function V . We consider V = StepsLO. Certainly condition (1) is verified since StepsLO (M ) 0 for each M 2 WN. We have to verify (2). Suppose P"(M ) = . If M !LO N and M !RI L, by Lemma 1 we can write: StepsLO ( ) = StepsLO(N ) " + StepsLO(L) (1 ") (StepsLO (M ) 1) " + StepsLO(M ) (1 = " StepsLO (M ) " + StepsLO (M ) (1 ") ") = StepsLO (M ) ": Since 0 " 1, StepsLO (M ) >" StepsLO ( ) for each normalising term M . Then, if " > 0, ( WN; P") is PAST and the average number of steps to normal form of a term M reduced with strategy P" is bounded by StepsL"O(M) . tu The bound we obtain on ExpLenM (") from the above proof is very loose and thus it does not give us any information on the actual nature of the function ExpLenM ("). We show, by means of an example, that the strategy P" is non-trivial i.e. there exists a term M and 0 < " < 1, such that ExpLenM (") < ExpLenM (1) = StepsLO(M ) < ExpLenM (0) = StepsRI(M ). -0.75 -0.50 -0.25 After quite simple computations one can derive ExpLenMn (") = (n 3)"3 +4"2 + 2" . Clearly for " = 0 the expression diverges. If n 2 there is a minimum for 0 < " < 1, and thus ExpLenMn (") < ExpLenMn (1) = StepsLO(Mn) < ExpLenMn (0) = StepsRI(Mn) = +1. ExpLenM9 (") is plotted in Figure 2.
Studying the behaviour of ExpLenM (") for an arbitrary term M is a difficult task, which goes outside the scope of this paper.
As a first step in the direction of a full understanding of the nature of ExpLenM ("), we study it in the case M is a term of the subcalculus A we have previously introduced. In particular we show in the next section that ExpLenM (") has minimum in " = 1. 4.1
The Case of the
The following lemma is an easy consequence of Xi’s combinatorial analysis of the
Standardisation Theorem [
where is standard, we can construct a standard reduction sequence : M L such that j j 1 + j j.
It is then easy to get the optimality of the leftmost-outermost strategy for
A-terms: Theorem 3. Given a reduction sequence : M in normal form, then the reduction sequence : M Proof. By induction on j j. The case j j = 0 is trivial. So now let us suppose that the theorem holds for j j k. Let us prove it for j j = k + 1. We can assume that: : M L !R N . By induction hypothesis we can construct a LO reduction sequence : M L such that j j j j. Then, since LO reduction sequences are standard, by Lemma 2 we can build a standard reduction sequence : M N such that j j 1 + j j 1 + j j = j j. The claim follows from the fact that standard reduction sequences to normal form are leftmost. tu Theorem 3 is a Theorem about a deterministic strategy, while our purpose here is to show the optimality of a randomised strategy. Some preliminary lemmas are necessary in order to appropriately lift it.
The following two lemmas tell us that the existence of a strictly partial probability distribution along a computation witnesses the existence of a deterministic computation leading to normal form: Lemma 3. Let (S; P) an FPARS and ( i)i2N a computation, where 0 = Dirac(s0).
Proof. We argue by induction on k. If k = 0, then the reduction sequence is trivially s0 s. If k = h, h(s) = P h 1 (t) P (t ! s). Since h(s) > 0, there t2S exists t 2 S such that h 1 (t) P (t ! s) =6 0, i.e. h 1(t) > 0 and P (t ! s) > 0. Thus, by induction hypothesis there exists a sequence s0 ! s1 ! ! sh 2 ! t, and t ! s. Hence there exists a reduction sequence s0 ! s1 ! ! sh 2 ! t ! s. tu Lemma 4. Let (S; P) an FPARS and ( i)i2N a computation, where 0 = Dirac(s0).
Proof. We argue by induction on k. If k = 1, since j 0j is Dirac(s0) then P(s0) = ? (otherwise j 1j = 1). Hence s0 is in normal form. If k = h and j h 1j < 1 by induction hypothesis we are done. So let us consider the case in which j h 1j = 1 and j hj < 1. We claim that there exists t 2 NF(S) such that h 1(t) > 0.
j hj = X X
s2S t2S = X X = t2S s2S
X t62NF(S) h 1(t) P (t ! s) h 1(t) P (t ! s) = X t2S
! h 1(t)XP (t ! s) + s2S h 1(t)XP (t ! s) s2S
!
X t2NF(S)
! h 1(t)XP (t ! s) : s2S If there was not t 2 NF(S) such that h 1(t) > 0, then the second term in the sum would vanish and j hj = P h 1(t) = 1. But j hj < 1 by hypothesis. t62NF(S) Hence there exists t 2 NF(S) such that h 1(t) > 0 and thus by Lemma 3 there exist a sequence s0 ! s1 ! ! sh 2 ! t. tu We are almost done: the following lemma tells us that all configurations along a computation starting from a A-term M are proper until the n-th configuration, where n = StepsLO(M ).
Lemma 5. Given the FPARS ( A; P"), and a computation ( i)i2N, where 0 = Dirac(M0), for each k StepsLO(M0), then j kj = 1.
Proof. Let n = StepsLO(M0). By contradiction if there was k n such that j kj < 1, then by Lemma 4 would exist a sequence M0 ! M1 ! ! Mj such that j k 1 and Mj is normal form. But this is impossible from Theorem 3.
Corollary 1. For each term M in
A, ExpLenM (") has minimum in " = 1.
Proof. Let n = StepsLO(M ) = ExpLenM (1).
1 ExpLenM (") = X
i=1
= n +
n
X
i=1
j ij =
j ij +
In terms of the I-calculus all redexes are needed to compute normal forms and
redexes can be duplicated. One might thus guess that the rightmost-innermost
strategy could be optimal there. However, innermost strategies, which do not
reduce a redex unless its argument is in normal form, are not optimal [
In this work we have initiated the study of randomised reduction strategies for the -calculus. We have defined a family of examples of such strategies, and we have shown that all of them, except one, are positive almost-surely normalising. Then we have studied those strategies for A, the affine -calculus, proving optimality results.
Further work could consist in analysing the behaviour of the proposed strategies in the scope of the full -calculus. In particular one could try to characterize classes of -terms for which our strategies work strictly better than deterministic ones, and to develop some methods to tune the parameter " in order to get good performances.
( x:xI)( y:!(yz)) ( y:!(yz))I
( x:xI)( y:(yz)(yz)) !(Iz)