Randomised Strategies in the λ-calculus
Gabriele Vanoni
Politecnico di Milano (on leave)

October 8, 2018

Joint work with Ugo Dal Lago

The usual untyped λ-calculus

Given a denumerable set of variables V,(terms) M, N ::= x ∈ V | MN | λx.M
(contexts) C , D ::=  | MC | CM | λx.C
(β-rule) (λx.M)N −→β M{N/x}β-reduction relation is the contextual closure of the β-rule:
M −→β N
C [M] −→β C [N]Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 20182 / 17Strategies in the λ-calculus

ExampleHow do we reduce M = (λx.x)N where N = (λx.x)y ?In M there
are two contexts in which we can apply the β-rule.
In fact β-reduction is a relation, not a function!
How do we pick the redex to reduce in a λ-term?
We need a reduction strategy, i.e. a computable (partial) functionthat given a reducible λ-term selects the redex to reduce.
ExampleLeftmost-outermost: M −→LO N −→LO y .
Rightmost-innermost: M −→RI (λx.x)y −→LO y .

Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 20183 / 17

Problems?
A few.
Not all strategies are normalizing.
Let ω = λx.xx and Ω = ωω. Note that Ω −→β Ω.
(λx.y )Ω −→LO y(λx.y )Ω −→RI (λx.y )Ω −→RI (λx.y )Ω −→RI · · ·Reductions of the same term to normal form can be ofdifferent length under different strategies.
Let I = λx.x.
(λx.xx)(II) −→LO (II)(II) −→LO I(II) −→LO II −→LO I(λx.xx)(II) −→RI (λx.xx)I −→RI II −→RI I
Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 20184 / 17

Minimal Strategies
Natural question
There exists a strategy that is minimal in the number of steps tonormal form?
Predictable answer [Barendregt ’84]
NO! (Of course such a function exists, but it is not computable inthe general case)
So what?
Restricting ourselves to some sub-λ-calculi the problem ofminimality becomes decidable.
TheoremIn λA, where copy is forbidden, LO is minimal.
In λI , where erasing is forbidden, RI is minimal.
Any insight about the general case?
Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 2018

5 / 17Randomised strategies
What if we choose the redex to reduce according to some probabilitydistribution?
ExampleWe can devise a randomised strategy U such that for each termM, every redex in M is reduced with the same probability i.e. |R1M | .
(λx.y )Ω
1212y(λx.y )Ω

In order to study properties of such a strategy we need to develop asuitable mathematical framework.
Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 20186 / 17

Fully Probabilistic Abstract Reduction SystemsDefinitionPρ ∈ PDist (S) if ρ : S → [0, 1] and |ρ| =ρ(s) ≤ 1.
ρ ∈ Dist (S) if ρ ∈ PDist (S) and |ρ| =s∈SPρ(s) = 1.

s∈SDefinition (Randomised Strategies)
Given an ARS (S, →), a randomised reduction strategy P for (S, →)is a partial function such that if s ∈ S is in normal form, thenP(s) = ⊥, otherwise P(s) = µ, and Supp(µ) ⊆ {t | s → t}.
(S, P) can be seen as a fully probabilistic abstract reduction system(FPARS), i.e. a purely probabilistic PARS, without any
nondeterminism. The configuration of an FPARS is ρ ∈ PDist (S),its evolution a function E : PDist (S) → PDist (S).
Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 20187 / 17

Termination
What does it mean that an FPARS (S, P) terminates?
In a probabilistic setting there are different possible answers.
Definition (AST)
A term is almost-surely terminating if it reaches normal form in a
finite number of steps almost-surely i.e. with probability 1.
StepsP (s) is the average number of steps of s to its normal form.
Definition (PAST)
A term s is positive almost-surely terminating if StepsP (s) < ∞.
PAST implies AST but the converse is not true! Think about thesimmetric random walk on Z.
/AST
Gabriele Vanoni (PoliMi)

PAST
Randomised Strategies

October 8, 20188 / 17

An example
Let us consider an abstract FPARS.
12

12ab

The computation is a stochastic process:(10ab(ρ01212
ρ1(ab1414ρ2ab(···12k12kρkab···Termination resultslim |ρn | = limn→+∞StepsP (a) =Gabriele Vanoni (PoliMi)

1n−1n→+∞ 2∞
Pn=1|ρn | == 0 ⇒ AST.
∞
Pn=1

1= 2 ⇒ PAST
2n−1

Randomised Strategies

October 8, 2018

9 / 17

The uniform strategy is not PASTLet ∆2 = λx.(xx)(xx), ∆4 = ∆2 ∆2 and M = (λx.λy .y )∆4 .
Since ∆4 −→β ∆4 ∆4 , reducing under U leads to the following tree:(λx.λy .y )∆41212(λx.λy .y )(∆4 ∆4 )λy .y
1
3λy .yStepsU (M) =∞P
i=1Gabriele Vanoni (PoliMi)|ρi | =1313(λx.λy .y )((∆4 ∆4 )∆4 )(λx.λy .y )(∆4 (∆4 ∆4 ))

···

···

∞
P
1i=1

i= +∞ ⇒ (ΛWN , U) is not PAST.

Randomised Strategies

October 8, 201810 / 17

Why U is not PAST?
Because there is no lower bound on the probability of picking theLO-redex, the one that assures normalisation.
Consider again the term M0 = (λx.λy .y )∆4 and a reduction
sequence of length n.
M0 −→β M1 −→β · · ·−→β Mn
1n+2121
3λy .y

λy .y

λy .y

As n → +∞, the probability of picking the LO-redex goes to zero.
Is the uniform strategy AST? Open problem.

Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 201811 / 17

A proof method for PASTFor ε > 0 we write x >ε y if and only if x ≥ y + ε.
Definition
Given an FPARS (S, P), we define a function V : S → R as
Lyapunov if:
1There exists b ∈ R such that V (s) ≥ b for each s ∈ S.

2There exists ε > 0 such that for every s ∈ S if P (s) = µ, thenV (s) >ε V (µ), where V is extended to partial distributions asfollows:
XV (µ) =V (t) · µ (t) .
t∈STheorem ([Foster ’53])
If we can define for an FPARS P = (S, P) a Lyapunov function V ,then P is PAST and StepsP (s) is bounded by V ε(s) .
Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 201812 / 17

(ΛWN , Pε ) is PASTCan we exploit Foster criterion to prove that a strategy is PAST?
Theorem
Each FPARS (ΛWN , Rε ) is PAST if Rε reduces the LO-redex withprobability ε > 0.
Proof.
StepsLO is a Lyapunov function for (ΛWN , Rε )That means that reducing a term with a strategy Rε brings tonormal form in a finite number of steps, in average. Thus
efficiency of any strategy Rε should be compared to the one of LO.
We consider now a very simple strategy which reduces withprobability 1 − ε the RI-redex. We call it Pε .

Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 201813 / 17Pε is non trivial.75

Can Pε be more efficient, in average, than LO?
Let us consider a family of terms Mn = NLn where:
N = λx. ((λy .z)Ω) x

Ln = Cn ((λx.x)y )||{z}

ExpLenM9 (ε)

P{zS

Cn = λx. xx· · · x}
| {z}n times15

105-0.50-0.25

Gabriele Vanoni (PoliMi)

00.25

0.50

Randomised Strategies

0.75

1.00
εOctober 8, 201814 / 17

Experimental work

We have tried to find out which terms benefit fromrandomisation.We adopted an experimental approach, developing
a tool that ouputs ExpLenM (ε) for a given M.
E.g. let Nn,m = ((λy .z)Im )(Cn (Iy )). Where is worth randomising?
m\n1
2
3451costLO
LOLO
LO

2RIPε
PεPε
Pε

3RIPεPεPε
Pε

4RIPεPεPεPε

5RIPεPεPε
Pε

In all non-trivial cases it is worth randomising!

Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 201815 / 17

Analysis of ExpLen(ε)
We would want to analyze the shape of ExpLen(ε). In particular weare interested in its minima.If M −→LO N and M −→RI L thenExpLenM (ε) = ε · ExpLenN (ε) + (1 − ε) · ExpLenL (ε) + 1.
Differentiating with respect to ε we have
ExpLen0M (ε) = ExpLenN (ε) − ExpLenL (ε)++ ε · ExpLen0N (ε) + (1 − ε) · ExpLen0L (ε).
By induction we are able to prove monotonicity for sub-λ-calculi
λA and λI , looking only at the sign of ExpLenN (ε) − ExpLenL (ε).
TheoremIn λA ExpLen(ε) is monotonically decreasing.
In λI ExpLen(ε) is monotonically increasing.
Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 201816 / 17

Future works

This was the first study on randomised strategies. Many
questions remain open.
Are there better randomised strategies?
How to tune ε?
What about the real world?

Gabriele Vanoni (PoliMi)Randomised Strategies

October 8, 201817 / 17