Repetitive Reduction Patterns
in Lambda Calculus with letrec
(Work in Progress)∗
Jan Rochel

Clemens Grabmayer

Utrecht University
Utrecht, The Netherlands
Department of Information and Computing Sciences
Information and Software Systems
J.Rochel@cs.uu.nl

Utrecht University
Utrecht, The Netherlands
Department of Philosophy
Theoretical Philosophy
Clemens.Grabmayer@phil.uu.nl

For the λ -calculus with letrec we develop an optimisation, which is based on the contraction of a
certain class of ‘future’ (also: virtual) redexes.
In the implementation of functional programming languages it is common practice to perform
β -reductions at compile time whenever possible in order to produce code that requires fewer reductions at run-time. This is, however, in principle limited to redexes and created redexes that are
‘visible’ (in the sense that they can be contracted without the need for unsharing), and cannot generally be extended to redexes that are concealed by sharing constructs such as letrec. In the case of
recursion, concealed redexes become visible only after unwindings during evaluation, and then have
to be contracted time and again.
We observe that in some cases such redexes exhibit a certain form of repetitive behaviour at
run time. We describe an analysis for identifying binders that give rise to such repetitive reduction
patterns, and eliminate them by a sort of predictive contraction. Thereby these binders are lifted
out of recursive positions or eliminated altogether, as a result alleviating the amount of β -reductions
required for each recursive iteration.
Both our analysis and simplification are suitable to be integrated into existing compilers for
functional programming languages as an additional optimisation phase. With this work we hope to
contribute to increasing the efficiency of executing programs written in such languages.

In this extended abstract we report on work in progress carried out within the framework of the NWO
project Realising Optimal Sharing. Instead of discussing optimal reduction in the λ -calculus, however,
here we are concerned with a static analysis of λletrec -terms which aims at removing β -redexes that are
concealed by recursion constructs and cause cyclic migration of arguments during evaluation. We have
to stress that our research on this particular topic is still in an early phase.

1

Introduction

In this work we study terms in λletrec , i.e. in λ -calculus with an explicit letrec-construct for recursive
definitions, that exhibit a form of repetitive reduction pattern when evaluated. We try to identify a class of
such terms for which this behaviour can be avoided by a transformation into a term with, in some sense,
the same semantic denotation. Even though the presented optimisation can be described directly for
λletrec -terms, and hence is applicable in all functional languages of which λletrec is a meaningful abstraction, we will use Haskell to denote examples of such terms and their optimised equivalents. Additionally,
we depict terms as λ -graphs with explicit sharing-nodes (multiplexers) as used, for example, in [2].
∗

Funded by the NWO-project Realising Optimal Sharing

Rachid Echahed (Ed.): 6th International Workshop
on Computing with Terms and Graphs (TERMGRAPH 2011)
EPTCS 48, 2011, pp. 85–100, doi:10.4204/EPTCS.48.9

© Rochel, Grabmayer
This work is licensed under the
Creative Commons Attribution License.

86

Repetitive Reduction Patterns in Lambda Calculus with letrec

A function well-known to Haskell programmers is the repeat function that generates an infinite,
constant stream of the supplied argument. A definition is easily found, namely:

repeat x = x : repeat x
An experienced Haskell programmer, however, would spot a ‘space leak’, which refers to an O(n) memory consumption for generating n stream elements while O(1) is possible, due to lazy evaluation. Therefore in the Haskell standard libraries that function is defined as:

repeat x = let xs = x : xs in xs
The exact reasons for this difference in efficiency involve the characteristics of the deployed Haskell
compiler and run-time system. A more direct and theoretical explanation can be attempted within the
formal framework of λletrec : The improved variant of repeat does not require any β -reductions to produce
further stream elements. That becomes apparent by the λ -graphs and their infinite unfoldings (Fig. 1).
We use a rewriting relation arrow indexed by a triangle (→▽ ) to mark unfolding, regardless of whether
sharing is expressed by a multiplexer or a letrec-binding.

λx
:
x
↠
↠▽

λx
@

λx

x

↠
↠β

x

:

:
x
x

↞
↞▽

:

..
.

@
..
.

x

Figure 1: Term graph representation of the two repeat implementations and their unfoldings
From a software engineering perspective it is unsatisfactory that the programmer has to recognise
and mitigate such cases. One might even consider the unoptimised version superior with respect to
code clarity. Therefore we propose an analysis and transformation method to automate the optimisation,
which then can be integrated into the compiler pipeline of existing functional language implementations.
In the following sections we will work with simple examples to develop this method and successively
generalise it for wider applicability.

2

Preliminaries

The method we describe applies to the λletrec -calculus, which is a higher-order rewrite system. Still, in
this work-in-progress report we primarily intend to motivate our research and outline the approaches
developed so far. Hence, for the moment we give a largely informal description, and resort to first-order
formulations, λ -graphs, or Haskell, whichever seems more suited.

Rochel, Grabmayer

87

Definition 1 (First-order representation of λletrec ) Let V be a set of variables. Then a λletrec -term is
defined as follows:
(term)

∶∶=
∣
∣
∣
(definitions) Defs ∶∶=
T

λV.T
TT
V
letrec Defs in T
v1 = T ... vn = T
v1 ,...,vn ∈ V all distinct

(abstraction)
(application)
(variable)
(letrec)
(equations)

But ultimately only a higher-order formulation can be formally satisfactory, thus we propose the
following representation as a higher-order rewrite system (HRS) [13] for λletrec .
Definition 2 (Higher-order representation of λletrec ) Let Var be a set of variables, and BTypes a set of
base types that induce the set Types of simple types. The terms of λletrec are simply-typed higher-order
terms over the HRS-signature that for all n ∈ N, and all types τ0 ,τ1 ,...,τn ∈ Types contains a symbol
letn in of type:
letn in ∶ (τ1 × ... × τn → τ0 × τ1 ... × τn ) → τ0
Product types are only used for better readability. We will use the symbols t, s, u for terms in λletrec .
Based on this notion of terms, the λletrec -calculus consists of the rewrite relations: β -reduction,
η-reduction, and letrec-unfolding. Additionally, we use the concept of generalised β -reduction [11].
For example, letrec-unfolding on the informal λletrec -terms according to the grammar above could
be described by the following rewrite rules:
let f1 = s1 ( f⃗),..., fn = sn ( f⃗) in t →▽ t

(if f1 ,..., fn not free in t)

let f1 = s1 ( f⃗),..., fn = sn ( f⃗) in t( f⃗) →▽ t(let Defs in s1 ( f⃗),...,let Defs in sn ( f⃗))
´¹¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¸ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹¶
Defs

which, if translated into HRS-rules (using the signature defined in Def. 2), can take the following form:
letn in λ f1 ... fn .(Y,Z1 ( f⃗),...,Zn ( f⃗)) →▽ Y
letn in λ f1 ... fn .(Y ( f⃗),Z1 ( f⃗),...,Zn ( f⃗)) →▽
Y (letn in λ f1 ... fn .(Z1 ( f⃗),Z1 ( f⃗),...,Zn ( f⃗)))...
...(letn in λ f1 ... fn .(Zn ( f⃗),Z1 ( f⃗),...,Zn ( f⃗)))
Notation 3 (Rewrite relations in λletrec ) On λletrec -terms we consider the following rewrite relations:
β -reduction denoted by →β ; generalised β -reduction denoted by →gβ ; η-reduction denoted by →η ;
letrec-unfolding denoted by →▽ .
For each of these rewrite relations →, the many-step rewrite relation with respect to → will be written
as ↠, and the (strongly convergent) infinite rewrite relation as ↠
↠.
With the transformation from Section 1, which is further developed in the next sections, we aim
to convert a given term t with repetitive reduction patterns into a term t ′ that does not require these
reductions to be performed any more, but such that t and t ′ are ‘operationally equivalent’, in a sense that
guarantees that important properties observable during evaluation are preserved.

88

Repetitive Reduction Patterns in Lambda Calculus with letrec

One candidate for a precisely defined notion of operational equivalence is the extension to λletrec -terms
of ‘applicative bisimulation’ on λ -terms due to Abramsky [1]. Two λletrec -terms M and N are called applicative bisimilar (symbolically: M ∼B N) if M and N behave in the same way under all possible series
E0 ,E1 ,E2 ,... of ‘experiments’ of the following kind: on a starting term M0 the first experiment E0 consists in finding out whether or not M0 reduces to an abstraction (a weak head normal form); if the outcome
Mi of the previous experiment Ei is indeed an abstraction λ x.Ni , then for experiment Ei+1 an arbitrary
term Pi+1 is chosen, and it is determined whether or not the redex (λ x.Ni )Pi+1 reduces to an abstraction.
While applicative bisimulation has been frequently used to justify optimising transformations for
functional programming languages, there may be a host of other interesting notions of operational equivalence. Since, for the moment, we do not want to commit ourselves to a particular notion of operational
equivalence, we will use a syntactically defined notion of equivalence between terms instead. In fact,
we will define this syntactic notion as the convertibility relation with respect to rewrite relations that we
use for motivating and justifying the optimising transformation in, for example, Fig. 1 and Fig 2. There,
we use, in addition to infinite convertibility with respect to →▽ and →gβ , a restricted form of ‘vector
η-reduction’ that is defined by the following rewrite rule:
λ x1 ...xn .Mx1 ...xn → M

(if x1 ,...,xn distinct, and not free in M)

The induced rewrite relation →η⃗ extends η-reduction, but can be mimicked with η-steps, and therefore
has the same many-step relation. However, neither for η-reduction nor for vector η-reduction it holds in
generality that the source and the target of a step are applicative bisimilar: for example, in the η-reduction
step λ x.yx →η y the source is an abstraction, but the target is not.
Since we want to obtain a syntactically defined notion of operational equivalence that is stronger
than applicative bisimilarity, we define a restriction →η⃗0 of →η⃗ , and a variant →η⃗ per of →η⃗0 , both of
0
which serve our purposes and, importantly, only allow steps between applicative bisimilar terms. The
converse rewrite relation ←η⃗0 of →η⃗0 performs a copying operation for λ -abstraction prefixes in terms;
and the converse rewrite relation ←η⃗ per of →η⃗ per both copies a λ -abstraction prefix and carries out a
0
0
permutation in it.
Definition 4 (Restriction and variant of →η⃗ ) The restricted version →η⃗0 of the rewrite relation →η⃗ on
λletrec -terms is defined by the rule:
λ x1 ...xn .(λ x1 ...xn .M)x1 ...xn → λ x1 ...xn .M

(if x1 ,...,xn distinct, and not free in M)

And the extension →η⃗ per of →η⃗0 with respect to permuting variable names in abstraction prefixes is
0
defined by the rewrite rule:
λ x1 ...xn .(λ xπ(1) ...xπ(n) .M)xπ(1) ...xπ(n) → λ x1 ...xn .M
(if x1 ,...,xn distinct, and not free in M,
and π is a permutation on {1,...,n})
It is easy to verify that left- and right-hand sides of these rules are applicative bisimilar.
Now we define the syntactic notion of equivalence on which we base our transformation.
Definition 5 (Equivalence relation =∞
▽,gβ ) Infinite convertibility with respect to →▽ and →gβ , extended
by finitely many →η⃗ per -reduction steps, is the following relation on λletrec -terms:
0

=∞
↞▽ ∪ ↞
↞gβ ∪ ↠
↠gβ ∪ ↠
↠▽ ∪ ↠η⃗ per )∗
⃗ per ∪ ↞
▽,gβ ∶= (↞η
0

0

Rochel, Grabmayer

89

Since source and targets of each of the rewrite relations →▽ , →gβ , and →η⃗ per are applicative bisimilar,
0
and since applicative bisimilarity is a contextual congruence [1], the following proposition can be proved,
which states that the syntactical equivalence from Definition 5 is at least as strong as, i.e. is contained in,
applicative bisimulation.
B
Proposition 6 For all λletrec -terms M,N it holds: M =∞
▽,gβ N ⇒ M ∼ N.

3

Further Examples

The repeat function shows that for some cases it is possible to lift parameters out of recursive positions
and thereby improve run-time efficiency. That raises the question of when this is possible. What is the
pattern that allows for such an optimisation?
What strikes the eye are the occurrences of the syntactic element repeat x on both the left-hand and
the right-hand sides of the function definition. That suggests a sort of common subexpression elimination
that takes into account both sides of the equation. This formulation, however, cannot cover the following
example, which differs from repeat essentially only by an additional parameter n on the left-hand side,
and the argument n − 1 on the right.

replicate 0 x = [ ]
replicate n x = x : replicate (n − 1) x
As it was the case for repeat, again it is possible to lift the parameter x out of the recursion.

replicate n x = let rec 0 = [ ]
rec n = x : rec (n − 1)
in rec n
Again we regard both variants and their infinite unfolding (Fig. 2) to understand the transformation. For
reasons of clarity, however, we completely leave out the scrutinisation of parameter n and the subsequent
case discrimination and concentrate on the recursive pattern.
In comparison with the previous example we observe two differences. First, note the ‘header’
λ n.λ x. [ ] n x attached on top of the second graph, which we obtain by two η-expansions. This allows us to produce an optimised term that does not comprise a duplicated function body. Furthermore,
instead of relying on ordinary β -reduction we have to add generalised beta-reductions (gβ -reduction)
[11] to our arsenal.
The key pattern shared by the two presented examples that permits optimisation is a parameter p
that is being passed through unchanged in the recursive application. Consequently, once the function is
called from the outside with some argument a in p’s position, while recursively evaluating that call, p
can never again be bound to another value than a or a descendant of a. In that sense one might call p a
‘constant parameter’. It suggests itself, that components that are ‘constant’ to a recursive construct can
be lifted out of the recursion.

4

A rewrite rule for simple recursive patterns

The examples in Section 1 and Section 3 suggest that there are many similar situations in which optimisations of the kind as described can be carried out. A first attempt to obtain general formulations of such
simplification steps would be to use schemata, and in effect, rewrite rules on λletrec -terms.

90

Repetitive Reduction Patterns in Lambda Calculus with letrec

λn

λn

λx

λx

@
@
@
λn

←η⃗0

x

λx

↠
↠▽

λn

n

n

↠
↠gβ

:
x

:

λn

x

−

@
:
@
−
n

n

1

x
x

λn
λx
..
.

↞
↞▽

@

1

@
λn
..
.

−
n

1

Figure 2: Operational equivalence of the two replicate variants depicted in graph notation

Rochel, Grabmayer

91

As an example, let us consider the recursive definition of a function f in which the (n+1)th parameter
y is passed on to all recursive calls of f as the (n + 1)th argument. In this case the transformation that
eliminates the recurrent parameter y can be described by the following first-order rewrite rule on λletrec

let f = λx1 . ... λxn .λy.C [f t1 ... tn y ] in f
→

λx1 . ... λxn .λy.let f 0 = λx1 . ... λxn .C [f 0 t1 ... tn ] in f 0 x1 ... xn
where C is a λletrec -context with possibly more than one occurrence of the context-hole [], f and f ′
do not occur in C, and y does not get bound during hole-filling. Here the recurrent parameter y in the
recursive definition of f is lifted out of the recursion, and the number of arguments in the recursive call
of the function in the let-construct has decreased by one after the transformation. Note, that context C
might start off with initial lambdas, and therefore also covers the case in which y is followed by further
parameters.
To cover situations with multiple recursive calls to f with (possibly) varying arguments, we can
generalise the rewrite rule as follows, as long as the argument in question, y, is the same.

let f = λx1 . ... λxn .λy.C [f t11 ... tn1 y, ..., f t1m ... tnm y ] in f
→

λx1 . ... λxn .λy.let f 0 = λx1 . ... λxn .C [f 0 t11 ... tn1 , ..., f 0 t1m ... tnm ] in f 0 x1 ... xn
C is a context with m sort of holes []1 , . . . , []m , in which holes of each sort may occur more than once,
where f and f ′ do not occur in C, and the parameter y does not get bound during hole-filling.
In order to enhance its application to a bigger class of λletrec -terms, the second rule can be further generalised to cover situations in which f is only one amongst many functions defined in a letrec-construct,
or there are also other recursive calls to f that are not of the ‘good’ form. Namely, if a definition like:

f = λx1 . ... λxn .λy.C [f t11 ... tn1 y, ..., f t1m ... tnm y ]
occurs somewhere in a let-binding, then it can be substituted by:

f = λx1 . ... λxn .λy.let f 0 = λx1 . ... λxn .C [f 0 t11 ... tn1 y, ..., f 0 t1m ... tnm y ] in f 0 x1 ... xn
There might be calls of f in C that are of ‘bad’ shape. These remain unchanged. On λletrec -terms, this
more general transformation can be expressed by the rewrite rule:

let E [f = λx1 . ... λxn .λy.C [f t11 ... tn1 y, ..., f t1m ... tnm y ]] in M
→

let f = λx1 . ... λxn .λy.
let E [f 0 = λx1 . ... λxn .C [f 0 t11 ... tn1 y, ..., f 0 t1m ... tnm y ]] in f 0 x1 ... xn
in M
where E is a context of the form D1 ,...,Di−1 ,[],Di ,...,Dl consisting of definitions D1 , . . . , Di−1 , Di+1 ,
. . . , Dl and a single hole [].

92

4.1

Repetitive Reduction Patterns in Lambda Calculus with letrec

Rewriting the Haskell Prelude

To demonstrate the above rewriting rule, we apply it to straightforward implementations of some wellknown functions from the Haskell Prelude.

map [ ]
= []
map f (x : xs) = f x : map f xs
until p f x = if p x then x else until p f (f x )
(++) [ ]
ys = ys
(++) (x : xs) ys = x : xs ++ ys
For the optimised counterparts the amount of β -reduction steps saved per recursive call amounts to
one for map and (++), and to two for until.

map f = let rec [ ]
= []
rec (x : xs) = f x : rec xs
in rec
until p f x = let rec x = if p x then x else rec (f x )
in rec x
(++) xs ys = let rec [ ]
= ys
rec (x : xs) = x : rec xs
in rec xs
In practise, however, the amount of β -reductions is only one of many factors for the run time that is
necessary to evaluate a piece of code. Therefore it is to be expected that when executed with a system
like the Glasgow Haskell Compiler (GHC) the obtained functions would not necessarily lead to better
performance. Depending on the compiler version and the flags provided in the invocation of GHC, simple
benchmarks yield mixed results, but never resulting in severe degradation (more than an increase of 5%
in run time) and with one of the functions (until) consistently reaching a speed-up of over 200%.
Let us conclude that before integrating the transformation into a compiler for practical purposes an
analysis on how it interacts with other optimisations remains yet to be done.

4.2

Limitations of the Rewrite Rules

While the most general rewrite rule above has proven to be applicable in a number of situations that
occur in practice, it also has some severe limitations: First and foremost it applies only to patterns with
immediate recursion, thus it fails to capture the repetitive reduction pattern in the evaluation of the term
in Fig. 3. If f and g are not used at further positions, once in the recursion initiated by f a both x and
y will never be bound to a different value than a. The property leading to this behaviour is the relation
between the parameters of f and g. In f , if g is called, then x is passed as an argument and thereby bound
to y. Conversely, y is bound to x in the call of f in g. Thus, we observe a relation between parameters that
is cyclic. Also for all of the previous example such a parameter cycle exists, however comprising only a
single parameter. In the following section we shall elaborate further on the idea of parameter cycles.

Rochel, Grabmayer

93

let f x = ... g x ...
g y = ... f y ...
in ... f a ...
Figure 3: Schematic term involving mutual recursion

5

Binding Analysis

In this section we shall develop an analysis that statically recognises repetitive reduction patterns indicated by parameter cycles, and show how this allows us to eliminate those binders that are part of such
a cycle. Parameter cycles describe the possibility of a parameter being passed on from function to function unchanged, finally arriving at its original position. To detect such cycles we need to analyse which
subterm might be bound to which variable during the evaluation of a term.

5.1

Binding Graph

To this end we introduce a binding relation b ⊆ V × T on variables V and subterms T of a term. It is
a conservative approximation of which bindings might occur during the evaluation of the term and does
not distinguish between different descendants of its components.
Since we need to take a global vantage point, i.e. to uniquely identify the term’s syntactic elements
we assume globally unique variable naming. To this end we could also use positional information, but
only along with additional technicalities. Therefore, without loss of generality we henceforth assume that
each abstraction binds a distinct variable (variables in the term are ‘distinctly bound’), and no variable
name has both a free and a bound occurrence (the term observes ‘Barendregt’s Variable Convention’ [3,
2.1.13, p.26]). That allows us to unmistakably address a specific binding λ x by the variable x it binds.1
For example for some context C in the reduction of term t = C[(λ x.e1 ) e2 ] the β -redex (λ x.e1 ) e2
might be contracted and by consequence a descendant of e2 be bound to an instance of x. Therefore t
implies x b e2 . This principle carries over to gβ -reduction, and more importantly, to sharing.
In order to obtain the binding relation for a term t one has to identify all terms in argument position
that might ever match up with λ x in its reduction. (More precisely: terms whose descendants might ever
match up with descendants of λ x.) This could be naively accomplished by a search that starts at each
abstraction λ x and from there travels upwards the spine segment of λ x. When an applicator with a as
an argument is encountered that matches λ x according to the semantics of gβ -reduction x b a is noted
down. When a multiplexer is encountered the search is pursued for each of the incoming edges.
The use of higher-order functions makes it impossible to enumerate the binding relation completely.
Thus, if during the search the end of the spine is reached one cannot make a safe assumptions on ‘future’
arguments for that branch. Therefore we employ an additional ‘artificial’ blackhole node ● that represents
an unknown term on the right hand side of the binding relation. According to this, the occurrence of
e1 (λ x.e2 ) implies x b ●. Note, that the blackhole node is not needed to identify parameter cycles, but
is however required for the domination property introduced later on.
Let us revisit the examples presented so far and enlist their binding relation. In the λ -graph of repeat
(Fig. 1) the search starting from the only abstraction λ x branches at the multiplexer above. The left
1

Even if that forbids distinguishing between different occurrences of the term x, it turns out not to be necessary for our
needs.

94

Repetitive Reduction Patterns in Lambda Calculus with letrec

branch yields a matching application with x in argument position, so we obtain x b x. At right branch
the spine immediately ends yielding x b ●. The directed graph that is induced by this relation features
a single-node parameter cycle.

•

•

•
a

x

x

n
x

y

n−1
Figure 4: Binding graphs of repeat, replicate, and the term from Fig. 3
The binding-graph of replicate is very similar featuring the same kind of parameter cycle, only does it
involve an additional parameter. Also we have to apply the idea of gβ -reduction when searching upwards
from λ x. First we encounter another abstraction λ n, which according to the notion of gβ -reduction
requires us to leave out the next application node. In the left branch of the multiplexer this is the one
with n − 1 in argument position. Therefore we end up with x as the argument of the matching application
node, by which we obtain x b x. Parameter cycles of greater length would occur for scenarios involving
mutual recursion such as the term in Fig. 3.

5.2

Inference Rules

To properly define the binding relation we formulate it using inference rules. Since it follows the structure
of typing rules, we first give rules for a simply-typed λletrec -calculus (Fig. 5) and then decorate these
typing rules to also yield a term’s binding graph, by which we hope to provide an easier access for those
who are already familiar with typing rules for the λ -calculus. Type variables are denoted by Greek letters.
VAR

A BS

Γ⇒x∶τ

Γ ⇒ λ x.e ∶ τ → σ

x∶τ ∈Γ

L ETREC

Γ ∪ {x ∶ τ} ⇒ e ∶ σ

A PP

∀i ∈ {0,...,n} ∶ Γ ∪ { f1 ∶ τ1 ,..., fn ∶ τn } ⇒ ei ∶ τi
Γ ⇒ letrec f1 = e1 ... fn = en in e0 ∶ τ0

Γ ⇒ e1 ∶ τ → σ

Γ ⇒ e2 ∶ ρ

τ =ρ

Γ ⇒ e1 e2 ∶ σ
Figure 5: Typing rules for the simply-typed λletrec -calculus
In order to infer the binding relation (Fig. 6), at any application e1 e2 one has to determine to which
variable e2 might be bound to in e1 . That we accomplish by annotating the types of terms with the names
of the variables that are bound by their abstractions. The annotations are in superscript position, so for
some annotated types x ∶ τ, y ∶ σ , e3 ∶ ρ, the annotated type of e1 = λ x.λ y.e3 is e1 ∶ (τ → (σ → ρ)y )x . We
use ε as an annotation to indicate that we cannot determine the associated variable (due to the use of
higher-order functions).

Rochel, Grabmayer

95

The binding relation is denoted on the left-hand side of the turnstile symbol. Both upper-case and
lower-case Greek letters denote annotated type variables, but the latter do not include the outermost
annotation (which are then added explicitly).
VAR

A BS

∅⊢Γ⇒x∶T

B ⊢ Γ ⇒ λ x.e ∶ (τ ε → Σ)x

x∶T ∈Γ

B ⊢ Γ ∪ {x ∶ τ ε } ⇒ e ∶ Σ

L ETREC

∀i ∈ {0,...,n} ∶ Bi ⊢ Γ ∪ { f1 ∶ T1 ,..., fn ∶ Tn } ⇒ ei ∶ Ti

B0 ∪ ... ∪ Bn ⊢ Γ ⇒ letrec f1 = e1 ... fn = en in e0 ∶ T0
A PP

B1 ⊢ Γ ⇒ e1 ∶ (T → Σ)x

B2 ⊢ Γ ⇒ e2 ∶ R

bare(T ) = bare(R)

B1 ∪ B2 ∪ bind(x,e2 ) ∪ blackholes(R) ⊢ Γ ⇒ e1 e2 ∶ Σ
⎧
blackholes(R) ∪ {x b
⎪
⎪
⎪
⎪
blackholes(T ) = ⎨blackholes(R)
⎪
⎪
⎪
⎪
⎩∅
⎧
⎪
⎪∅
bind(x,e2 ) = ⎨
b
⎪
⎪
⎩{x

e2 }

●} if T = (Σ → R)x
if T = (Σ → R)ε
otherwise
if x = ε
otherwise

Figure 6: Inductive definition of the binding relation based on annotated types
In the A BS rule the abstraction puts a new variable x, which is annotated by an ε because we do not
make assumptions on the variables exposed by higher-order functions. The type of λ x.e is annotated by
x, which is exposed. To compare types A PP employs a function bare ∶ A → T , which maps annotated
types A to bare types T by removing all annotations. Two further functions, bind and blackholes, are
used to enumerate the elements to be added to the binding relation. In case the argument e2 is a higherorder function the expressions cannot be determined that are bound to the variables it exposes, therefore
blackholes binds a blackhole to each of them.
Proposition 7 Every derivation D in the type system in Fig. 5 with conclusion ∅ ⇒ M ∶ τ, which justifies
the assignment of type τ to the λletrec -term M, can be decorated effectively with as result a derivation
D̃ in the proof system in Fig. 6 with conclusion B ⊢ ∅ ⇒ M ∶ τ̃, by which the binding graph B for M is
obtained and justified.
The proof of this proposition consists in describing an effective algorithm that, given a derivation D
in the type system in Fig. 5, proceeds as follows: First it constructs, in a step by step manner, variable
decorations for the types in D (by concentrating on ‘spine loops’ of M that correspond to cyclic threads
in D, and starting with the decorations at formulas on such threads where the types have minimal length)
in such a way that the rule instances are correct for the system in Fig. 6 when the leading binding
graph annotations of the form B ⊢ are neglected. Second, after the first step is concluded, the algorithm
constructs the binding graph annotations according to the rules in Fig. 6 in a top-down manner.

96

Repetitive Reduction Patterns in Lambda Calculus with letrec

6

Transformation

Using the binding graph we will now develop a more general version of the optimisation previously
formulated as rewriting rules restricted to directly recursive functions.
An edge x b e in the binding graph of a term t indicates a (possibly infinite) class of gβ -redexes
on the infinite unfolding T of t. While all these redexes could be at once contracted on T this does not
automatically carry over to its finite representation t.2 Let us for the present restrict our attention to cases
where x has no further incoming edges.
Proposition 8 Let t be a λletrec -term with infinite unfolding T and a binding graph featuring a node x
with a single incoming edge x b e. If we label the transition that contracts all gβ -redexes with involving
a λ x-abstraction red, and the substitution of all occurrences of t by e and the subsequent elimination of
all vacuous λ x-abstractions trans, then the following diagram commutes.
t ↠
↠▽ T
trans ↓
↓ red
t′ ↠
↠▽ T ′
This follows from the following considerations. Since we assume unique variable naming, the infinitely
unfolding t without any renaming is semantics preserving. [8]3 Every occurrence of λ v in t gives rise to
one ore more gβ -redexes in T each having λ v with p as an argument. This follows from x b e being
the sole incoming edge of x. By both paths from t to T ′ one finds T ′ to have the same shape: There are
no occurrences of neither λ x nor x. Evidently this not a very strong argument and we hope to improve
on it by means of higher-order reasoning.
The restriction above to only consider nodes with a single predecessor prevents us from dealing with
any of the examples shown so far since they involve cyclic binding graphs. Fortunately, it can be relaxed
to a much less restrictive property.
Definition 9 (Domination, and strong domination) Let a G = ⟨V, ↣⟩ be a directed graph, and u and v
be vertices of G. We say that v dominates w (v is a dominator for w, symbolically: domG (v,w)) if either
v = w or v ≠ w and for every path π in G that leads to w but does not contain v it holds that the start vertex
of π is reachable from v; more formally, if:4
v = w ∨ (v ≠ w ∧ ∀u0 ,...,un ∈ V ∖ {v}[u0 ↣ u1 ↣ ... ↣ un = w Ô⇒ v ↣∗ u0 ])

(1)

Note that v ↣∗ w holds if v dominates w.
And we say that v strongly dominates w (v is a strong dominator for w, symbolically: sdomG (v,w))
if v ≠ w and for every path π in G that leads to w but does not contain v it holds that the start vertex u0 of
π is reachable from v, but does not reside on a common cycle with v, more formally, if:
v ≠ w ∧ ∀u0 ,...,un ∈ V ∖ {v}[u0 ↣ u1 ↣ ... ↣ un = w Ô⇒ v ↣∗ u0 ∧ u0 ↣
/ ∗ v]
2

(2)

In fact, the reduct of an unfolded λletrec -term does not have to be expressible as a finite term in λletrec in general.
Even if this has only been proven for µ-unfolding but it is assumed that it also holds for λletrec . The unfolding does not
preserve unique naming.
4
The condition 1 could be simplified by taking it to be just the subformula starting with the universal quantification (that
subformula is true if v = w); the longer condition is used here to increase readability.
3

Rochel, Grabmayer

97

Remark 10 The standard definition of a ‘v dominates w’ for control-flow graphs (see e.g. [9]) requires
that each path from the start node to w has to pass through v. The definition above is a generalisation
to directed graphs that does not depend on the existence of a designated start node. Our definition of
‘v strongly dominates w’ excludes self-domination (i.e. makes the relation irreflexive), and adds the
restriction that for all paths from v to w that do not repeatedly pass through v it holds no vertex except
the starting vertex v resides on a common cycle with v.
The following proposition suggests an alternative, co-recursive definition of strong domination between vertices, which proceeds stepwisely by examining predecessors of the strongly dominated vertex.
Proposition 11 Let G = ⟨V, ↣⟩ be a directed graph. Then for all v,w ∈ V it holds:
sdomG (v,w) ⇐⇒ v ≠ w ∧ v ↣+ w ∧ w ↣
/ + v ∧ ∀u ∈ V (u ↣ w ∧ u ≠ v ⇒ sdomG (v,u))
For the definition of the optimising transformation, we choose a formulation different from the one
using rewrite rules described in Section 4, one that is particularly easy to express. Such as β -reduction
can be decomposed into substitution of individual occurrences of variables (local β -reduction) and the
elimination of vacuous bindings (AT-removal) as described in [4], for the transformation we have the
possibility of expressing the transformation with an arbitrary level of granularity. The following rule
encompasses the substitution of all occurrences of one dominated variable. It could have been formulated more fine-grained by substituting only individual occurrences, or less fine-grained by including the
elimination of the bindings that have become vacuous.
Proposition 12 (Main proposition) In a λletrec -term t occurrences of a variable that is dominated by an
expression d in t’s binding graph can be substituted by d.
B⊢∅⇒t ∶Σ
t

7

=∞
▽,gβ

B ⇒ domB (d,x)
t⟨x ∶= d⟩

Advanced Examples

There are interesting examples to which the presented transformation cannot be directly applied or does
not lead to satisfactory results. Only in combination with a number well-directed unfoldings the desired
effect can be obtained. Let us consider two schematic examples:

λy. ... let rec = λx .C [rec x ] in ... rec ...
let f = λx .λy.D [f x b, f a y ] in ... f ...
The first one exhibits dominated parameters only after a single let-unfolding (Fig. 7). Also it features
repetitive reduction pattern, without having a parameter cycle. This because the argument in question is
bound outside of the recursion. Still, after the unfolding the presented optimisation does cure the term.
The second of the two term is particularly intricate since it can be unfolded and then transformed
in many different ways with considerable differences in the amount of concealed gβ -redexes. Most
solutions involve more than one recursive call with more than two arguments. The ideal transformation
with respect to the number of concealed redexes of both terms is depicted in Fig. 8.

98

Repetitive Reduction Patterns in Lambda Calculus with letrec

•

•

•

•

y

x1

→▽

x

y

x2

Figure 7: A term, which after one unfolding exhibits a dominated parameter

8

Status quo

Presently this work consists mostly of an extended problem description, which is to a some extent rather
informal. Ideas for resolution have been presented, but yet lack both precision and genericity. Therefore,
outstanding issues to continue the investigation suggest themselves. Currently we are working on the
following problems:
• Properly formalising the concepts introduced in this report. This involves putting grammars and
rewrite rules into the higher-order setting of HRSs.
• Investigate whether there are other interesting notions of ‘operational equivalence’, apart from
applicative bisimulation, with respect to which we could show correctness of our optimising transformation. (We think of notions that are in line with the semantics of functional programming
languages, but nevertheless are language independent, and also of theoretical interest.)
• Expressing the presented transformation as a higher-order rewrite system and proving its correctness with respect to that equivalence relation.
Once these fundamental issues are resolved, we intend to tackle the following questions:
• We have seen that unfolding a λletrec -term in order to facilitate the optimisation can be effected in

Rochel, Grabmayer

=∞
▽,gβ

99

=∞
▽,gβ

@
b

Figure 8: Optimisation of two terms that are not covered by the presented rewriting rules
different ways, leading to terms of different quality. To obtain the most efficient terms one has to
provide a procedure to select the most suitable unfolding for each situation.
• This requires an adequate measure for efficiency.
• We would like to learn more about the rewrite properties of the transformation: is it possible to
find a formulation that guarantees confluence and normalisation?
• In some of the easy examples we studied, our transformation seemed to be closely connected
with the concept of ‘lambda-dropping’ [7, 5], and hence also with its converse, ‘lambda-lifting’
[10, 12, 6]. We want to understand that relationship in detail.
• Once the analysis has been optimised in terms of genericity, i.e. that it recognises as many cases
as possible for which the transformation is correct, it would be interesting to assess the frequency
in which these cases occur in existing systems, such as functional programming libraries or intermediate code generated by compilers.

100

Repetitive Reduction Patterns in Lambda Calculus with letrec
• The remaining question is, how the optimisation actually affects the run-time efficiency of realworld systems like Haskell programs.

Acknowledgment. The incentive to investigate the presented optimisation was provided by Doaitse
Swierstra. We thank him and Vincent van Oostrom for many insightful discussions and hints.

References
[1] Samson Abramsky (1990): The Lazy Lambda Calculus. In: Research Topics in Functional Programming. Addison-Wesley, pp. 65–116. Updated version (2006) available at http://web.comlab.ox.ac.
uk/people/Samson.Abramsky/lazy.pdf.
[2] Andrea Asperti & Stefano Guerrini (1998): The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science 45, Cambridge University Press.
[3] H.P. Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics, 2nd edition. SLFM 103, Elsevier.
[4] N.G. de Bruijn (1987): Generalizing Automath by Means of a Lambda-Typed Lambda Calculus. Technical Report AUT092 (AUTOMATH archive http://www.win.tue.nl/automath/), Technische Universiteit Eindhoven, Eindhoven, the Netherlands. Available at http://alexandria.tue.nl/repository/
freearticles/597608.pdf.
[5] Olivier Danvy (1999): An Extensional Characterization of Lambda-Lifting and Lambda-Dropping. In Aart
Middeldorp & Taisuke Sato, editors: Functional and Logic Programming. LNCS 1722, Springer Berlin /
Heidelberg, pp. 241–250, doi:10.1007/10705424 16.
[6] Olivier Danvy & Ulrik Schultz (2002): Lambda-Lifting in Quadratic Time. In Zhenjiang Hu & Mario
Rodrı́guez-Artalejo, editors: Functional and Logic Programming. LNCS 2441, Springer Berlin / Heidelberg,
pp. 134–151, doi:10.1007/3-540-45788-7 8.
[7] Olivier Danvy & Ulrik P. Schultz (1997): Lambda-dropping: transforming recursive equations into programs with block structure. In: Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. PEPM ’97, ACM, New York, NY, USA, pp. 90–106,
doi:10.1145/258993.259007.
[8] Jörg Endrullis, Clemens Grabmayer, Jan Willem Klop & Vincent van Oostrom (2010): On Equal µ-Terms.
Submitted, currently under review, to be published in 2011.
[9] M. S. Hecht & J. D. Ullman (1974): Characterizations of Reducible Flow Graphs. JACM 21, pp. 367–375,
doi:10.1145/321832.321835.
[10] Thomas Johnsson (1985): Lambda lifting: Transforming programs to recursive equations. In Jean-Pierre
Jouannaud, editor: Functional Programming Languages and Computer Architecture. LNCS 201, Springer
Berlin / Heidelberg, pp. 190–203, doi:10.1007/3-540-15975-4 37.
[11] Fairouz Kamareddine & Rob Nederpelt (1995): Refining reduction in the lambda calculus. Journal of Functional Programming 5(4), pp. 637–651, doi:10.1017/S0956796800001507.
[12] Simon L. Peyton Jones (1987): The Implementation of Functional Programming Languages (Prentice-Hall
International Series in Computer Science). Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
[13] Terese (2003): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55, Cambridge
University Press.

