A Lambda-Calculus with letrec, case,
constructors and non-determinism

arXiv:cs/0011008v1 [] 6 Nov 2000

Manfred Schmidt-Schauß and Michael Huber
Fachbereich Informatik
Johann Wolfgang Goethe-Universität
Postfach 11 19 32
D-60054 Frankfurt, Germany
E-mail: schauss@ki.informatik.uni-frankfurt.de

Abstract. A non-deterministic call-by-need lambda-calculus λndlr with
case, constructors, letrec and a (non-deterministic) erratic choice, based
on rewriting rules is investigated. A standard reduction is defined as
a variant of left-most outermost reduction. The semantics is defined by
contextual equivalence of expressions instead of using αβ(η)-equivalence.
It is shown that several program transformations are correct, for example
all (deterministic) rules of the calculus, and in addition the rules for
garbage collection, removing indirections and unique copy.
This shows that the combination of a context lemma and a metarewriting on reductions using complete sets of commuting (forking, resp.)
diagrams is a useful and successful method for providing a semantics of
a functional programming language and proving correctness of program
transformations.

1

Introduction

Functional programming languages are based on extended lambda calculi and
the corresponding rewrite semantics. There are several methods of giving these
languages a semantics and proving the correctness of program transformations:
– A denotational semantics uses a mathematical domain and a mapping from
expressions to their denotation. This defines an equivalence of expressions,
which can be used to define a notion of correctness of program transformations. This area is well-developed, but reaches its limits if non-deterministic
operations are possible in the language.
– An operational semantics defining the evaluation of expressions (the execution, resp.). Sometimes this is used with a kind of syntactic equality (e.g.
αβ(η)-equality in the lambda-calculus). It could also be complemented by a
behavioral equivalence, which can be used to define the a notion of correctness of program transformation.
– A contextual semantics is a kind of operational semantics as above enhanced
with an approximation relation based on a contextual preordering (see e.g.
[Smi92,MST96,Pit97]). An expression s has less information than an expression t, iff in all contexts C[], if C[s] gives some information (e.g. terminates),

then C[t] also gives some information (i.e. terminates). This notion is directly adapted to define a notion of correctness of program transformation.
Often it gives the intuitive correct notion of program equivalence, and hence
also of correct program transformations.
The advantage of the contextual semantics is that the number of equality relations is maximal and that the derived properties are independent of a specific
domain. The properties of the contextual preorder are comparable to the orderings in domains; for example it is possible to use fixed-point constructions
for recursion. The contextual semantics is superior to the more syntax-oriented
αβ(η)-equivalence, since contextual semantics permits considerably more program transformations.
An advantage of contextual semantics over the denotational approach becomes
obvious if non-determinism is on board and also sharing in the form of a (nonrecursive or recursive) let. It appears to be very hard to construct a useful domain for denotational semantics in the presence of non-determinism and higherorder functions, whereas it is possible to use the contextual equivalence for defining an intuitive correct semantics. This can then be used to prove correctness
of program transformations sometimes exploiting rewriting techniques. A slight
disadvantage of the contextual semantics (w.r.t. economy of proofs) is that it
depends on the available syntactic constructs, hence on the set of contexts, and
the defined standard reduction.
The prominent syntactic property of the lambda-calculus is confluence of reduction [Bar84]. In the framework of a contextual semantics for the lambda-calculus
(see e.g. [Abr90]), confluence is not thus important and is replaced by the correctness of program transformations. The really interesting propositions are:
– Every beta-reduction transforms a program P into an equivalent one P ′ ,
meaning that P and P ′ are contextually equivalent. This is the required
modification of confluence.
– (standardization) Whenever there is a reduction of an expression t to an
abstraction, then the standard reduction terminates, i.e. reduces t to an
abstraction.
These properties can be generalized to extended lambda-calculi, where confluence may be false (see e.g. [AK94]), but contextual equivalence can be easily
adapted.
Another approach is Rewriting Logic (see e.g. [Mes00]), which is a step in the
direction of providing a semantics for programming languages based on rewriting rules. This appears to work for deterministic languages based on rewriting
rules. However, the contextual semantics is our method of choice for the nondeterministic case.
In this paper we present the calculus λndlr that is rather close to a non-strict
functional core language. Reduction is like lazy call-by-need evaluation in functional programming languages. λndlr can be seen as a generalization of the calculus in [KSS98,Kut00] and thus of the calculi in [AFM+ 95,AF97,MOW98], which
2

treat sharing in the lambda calculus. It also is a generalisation of [MSC99] insofar as the language of expressions is not restricted to have only variables
as arguments in applications. The calculus λndlr is related to the calculus in
[SS00], where a similar language is investigated, but with the emphasis on an
IO-interface.
Another method for treating sharing are explicit substitutions [ACCL91], which
optimize resource usage of reductions by exploiting sharing, however, it is i)
based on αβ(η)-equivalence and ii) the reduction rules are in general not compatible with non-determinism, i.e. not with λndlr nor with the calculus in [Kut00];
in particular, the let-over-lambda-rules are incompatible with non-determinism.
Specific ingredients of λndlr are
– sharing by using letrec, which moreover allows recursive definitions.
– a non-deterministic (erratic) choice, which allows to choose between two
expressions.
– a modified beta-reduction that prevents an unwanted duplication of nondeterministic expressions.
The motivation to investigate non-determinism is to model interfaces of lazy
functional languages to the outside world, i.e. to model input/output. This is
done by a simulation of an IO-action by a nested choice-expression that represents the set of possible input values of the IO.
The paper proposes to investigate extended lambda-calculi by using operational
methods and a contextual semantics. The contextual semantics includes a measure for the number of non-deterministic steps. As a method for proving program
transformation to be correct we propose to use complete sets of reduction diagrams in combination with an appropriate context lemma.
The results are that for λndlr a rather large set of basic program transformations
is proved to be correct. The paper also demonstrates the power of the method,
since the reduction rules of λndlr are numerous and complex.
As a check-program for complete sets, a program “Jonah“ was implemented to
automatically test the complete reduction diagrams using a generate-and-test
scheme; Jonah can also be used to compute proposals for complete sets.
As a remaining open problem the paper can be seen as a recommendation to
start an investigation into adapting the Knuth-Bendix method to automatically
computing the reduction diagrams. However, the reduction diagrams for (llet) for
example show that it would be necessary to integrate a kind of meta-description
like the Kleene-∗.
In this paper we do not present all proofs, but give enough hints and evidence
of how the claims can be verified and that they are valid.

2

The calculus λndlr

The syntax of the language is as follows:
There is a set of type-names. For every type there are constructors c coming with
an arity ar(c). This partitions the set of all constructors into the constructors
3

belonging to different types. For a type A, |A| is defined to be the number of
constructors belonging to A. The constructors belonging to type A are indexed,
and cA,i denotes the ith constructor of type A.
E ::= V | C | (choice s t) | (caseA E Alt1 . . . Alt|A| ) | (E1 E2 )
| (λV.E) | (letrec V1 = E1 , . . . Vn = En in E)
Alt ::= (P at → E)
P at ::= c V1 . . . Var(c)

where E, Ei are expressions, A is a type, V, Vi are variables, and C is a constructor. The variables in a pattern P at must be different, and also new ones.
Moreover, in a caseA -expression, there is exactly one alternative with a pattern of the form (cA,i y1 . . . yn ) for every constructor cA,i . The constants caseA
and choice can only occur in a special syntactic construction. Thus expressions
where choice or caseA is applied to a wrong number of arguments are not
allowed.
The structure letrec obeys the following conditions: The variables in the bindings are all distinct. We also assume that the bindings in letrec are commutative, i.e. can be commuted without syntactic change. letrec is recursive: I.e.
the scope of xi in (letrec xi = Ei in E) is Ei , E. This allows to define closed,
open expressions and α-renamings. For simplicity we use the disjoint variable
convention. I.e., all bound variables in expressions are assumed to be disjoint.
The reduction rules are such that the bound variables in the result are also
made distinct by α-renaming. We also use the convention to omit parenthesis in
denoting expression: (s1 . . . sn ) denotes (. . . (s1 s2 ) . . . sn ).
We say that an expression of the form (c t1 . . . tn ) is a constructor application,
if n ≤ ar(c). A constructor application of the form (c x1 . . . xn ) is called a pure
constructor application. An expression of the form (c t1 . . . tar(c) ) is called a
saturated constructor application.
Definition 2.1. Let R, R− , be context classes defined as follows:
R− ::= [] | R− E | (caseA R− alts)
R ::= R− | (letrec x1 = E1 , . . . , xn = En in R− )
| (letrec x1 = R1− [·], x2 = R2− [x1 ], . . . , xj = Rj− [xj−1 ], . . . in R− [xj ])
where Rj− is a context of class R−
R is called a reduction context and R− is called a weak reduction context. For a
term t with t = R− [t0 ], we say R− is maximal, iff there is no larger weak reduction context with this property. For a term t with t = R[t0 ], we say the reduction
context R is maximal, iff it is either a maximal weak reduction context, or of
the form (letrec x1 = R1− [·], x2 = R2− [x1 ], . . . , xj = Rj− [xj−1 ], . . . in R− [xj ]),
4

where t = (letrec x1 = t1 , . . . in R− [xj ]), R1− [·] is maximal for t1 , and the
number j is maximal.
For example the maximal reduction context of (letrec x2 = λx.x, x1 =
x2 x1 in x1 ) is (letrec x2 = [], x1 = x2 x1 in x1 ), in contrast to the nonmaximal reduction context (letrec x2 = λx.x, x1 = x2 x1 in []).
The (call-by-need) reduction rules defined in 2.2 follow the principle of minimizing copying at the cost of perhaps following several indirections. This holds for
the copy rule (cpn) as well as (case). The technical reason is that this principle
assures well-behaved reduction diagrams.
Definition 2.2. The reduction rules are defined below in figure 2. If the context
is important, then we denote it as a label of the reduction or state it explicitly.
Note that for (case), the typical example is written down, where the position
of the case is left open. There are two variants, one where the caseis in the
in-expression, and one where the case-expression is in the right hand side of
a binding. An exceptional case, where perhaps a letrec-expression has to be
omitted, is the case of a constructor with zero arguments like (case N il . . .).
The union of ndl, ndr is called (nd). Reductions are denoted using an arrow with
llet

super and/or subscripts: e.g. −−→. Transitive closure is denoted by a +, reflexive
∗
transitive closure by a ∗. E.g. −→ is the reflexive, transitive closure of →.
As a short comment of the reduction rules:
– (lbeta) is a sharing version of beta-reduction
– (cpn) is a lazy version of the replacement done by usual beta-reduction,
where the copy may jump over several indirections.
– (case) is the generalized if for case analysis of values. To find the value to
be analyzed, it has to be virtually assembled by following the bindings.
– (llet), (lapp), (lcase) are used to adjust the let-environments
– (nd) is the non-deterministic (erratic) choice.
The next definition is intended to formalize the standard reduction. The idea is
to find the reduction that is outermost, in a reduction context and also necessary
for making progress in the evaluation.
Definition 2.3. Let t be an expression. Let R be the maximal reduction context such that t ≡ R[t′ ] for some t′ . The standard redex and the corresponding
st

standard reduction −−→ is defined by one of the following cases:
– t′ is a choice-expression: then use (ndr) or (ndl).
– R = (letrec x1 = t1 , . . . xn = tn in []), and t′ is a letrec-expression. Then
apply (llet) to R[t′ ].
– R = R0 [(· t′′ )] where R0 is a reduction context. If t′ is a letrec-expression,
then use (lapp) in context R0 ; If t′ is an abstraction, then use (lbeta) in
context R0 .
5

– R = R0 [caseA · alts].
If t′ is a letrec-expression, then use (lcase) in context R0 ;
If t′ is a saturated constructor application, then use (case) in context R0 , if
it is applicable.
– R = (letrec x1 = [], x2 = x1 , . . . , xj = xj−1 , . . . in R1− [xj ])] where R1− is a
weak reduction context.
If t′ is an abstraction, then use (cpn) as follows: (letrec x1 = t′ , x2 =
x1 , . . . , xj = xj−1 , . . . in R1− [xj ])] → (letrec x1 = t′ , x2 = x1 , . . . , xj =
xj−1 , . . . in R1− [t′ ])].
If t′ is a letrec-expression, then use (llet),(lcase), or (lapp) to flatten the
letrec-expression t′ into its superexpression.
If t′ is a constructor application, and (case) is applicable to a case-expression
in a reduction context, then apply this (case)-reduction.
– R = (letrec x1 = [], x2 = x1 , . . . , xj = xj−1 , xj+1 =
−
−
−
Rj+1
[xj ], . . . in R∞
[xk ])] where Ri− , R∞
are weak reduction contexts.
′
If t is an abstraction, then use (cpn) such that the result is: R =
−
−
(letrec x1 = t′ , x2 = x1 , . . . , xj = xj−1 , xj+1 = Rj+1
[t′ ], . . . in R∞
[xk ])].
′
If t is a letrec-expression, then use (llet),(lcase), or (lapp) to flatten the
letrec-expression t′ into its superexpression.
If t′ is a constructor application, and (case) is applicable to a case-expression
in a reduction context, then apply this (case)-reduction.

Lemma 2.4. For every term t: if t has a standard redex, then this redex is
unique. If the standard reduction is not an (nd), then the standard reduction is
also unique.
st

st

st

Definition 2.5. A standard reduction s −−→ s1 −−→ s2 . . . sn −−→ t has ndcount D, iff D is the number of (nd)-reductions in it.
Note that we use the notion standard reduction also for non-maximal reductions.
Definition 2.6. For a term t and an nd-count D, t⇓D holds if there is some
standard-reduction starting with t, and the reduction has nd-count D.
Note that a standard reduction for an nd-count D is in general not unique. Note
also that there may be expressions without a standard redex.
Definition 2.7.
define:

(contextual preorder and equivalence) Let s, t be terms. We

s ≤c t iff ∀C[].∀D : C[s]⇓D ⇒ (∃B.D ≤ B ∧ C[t]⇓B )
s ∼c t iff s ≤c t ∧ t ≤c s
Note that we permit contexts such that C[s] is an open term.
6

Proposition 2.8. ≤c is a preordering and ∼c is an equivalence relation.
s ≤c t implies that C[s] ≤c C[t] for all contexts C[.]. I.e., ≤c is a precongruence
on the set of expressions.
s ∼c t implies that C[s] ∼c C[t] for all contexts C[.]. I.e., ∼c is a congruence on
the set of expressions.
Note that there are terms t without a standard redex, i.e. the standard reduction
stops. The reasons could be classified as i) type-error like (caseA (λx.x) . . .), ii)
a kind of non-termination like (letrec x = x in x), iii) as a value or a kind of
normal form like (Cons True Nil) or λx.x.
The following lemma shows that it is sufficient to use reductions contexts for
checking contextual approximation.
Lemma 2.9. (Context Lemma) Let s, t be terms. If for all reduction contexts
R and all nd-counts D: R[s]⇓D ⇒ (∃B.D ≤ B ∧ R[t]⇓B ), then s ≤c t.
Proof. We prove the more general claim:
if for all i: si , ti satisfy the conditions of the lemma for reduction contexts,
then for all multicontexts C[·1 , . . . , ·m ]: C[s1 , . . . , sn ]⇓D ⇒ (∃B.D ≤
B ∧ C[t1 , . . . , tn ]⇓B .
Assume this is false. Then there is a multicontext C, an nd-count D, such that
C[s1 , . . . , sn ]⇓D , and for all B with D ≤ B: C[t1 , . . . , tn ]6⇓B .
We select a multicontext, C, terms si , ti , and an nd-count D, and a corresponding
reduction, such that the counterexample is minimal w.r.t. the following lexicographic ordering: i) the number of reduction steps of C[s1 , . . . , sn ], ii) the number
of holes of C[. . .].
The search for a standard redex is performed top-down. There are two cases:
1. The search for the reduction context inspects the term in a hole. Then we
can assume wlog that the first hole is inspected first. Hence C[·, t2 , . . . , tn ]
is a reduction context. Let C ′ := C[s1 , ·2 , . . . , ·n ]. Since C ′ [s2 , . . . , sn ] ≡
C[s1 , . . . , sn ], we can select the the same standard reduction for nd-count D.
Since the number of holes of C ′ is smaller than the number of holes in C, we
obtain some B ≥ D with C ′ [t2 , . . . , tn ]⇓B , which means C[s1 , t2 , . . . , tn ]⇓B .
Since C[·, t2 , . . . , tn ] is a reduction context, the preconditions of the lemma
imply that there is some B ′ ≥ B with C[t1 , t2 , . . . , tn ]⇓B ′ , a contradiction.
2. The search for the reduction context does not inspect any hole of C. Then
C[s1 , . . . , sn ] as well as C[t1 , . . . , tn ] can be reduced using the same standard
reduction, since the search for a standard redex takes place only in the outer
context C[. . .]. There are two cases for a reduction:
st

If the reduction C[s1 , . . . , sn ] −−→ s′ is not (nd), then this may result in
C ′ [...] with more holes, and the holes are filled with copies of si , ti . Then we
get a smaller counterexample since the number of reductions steps is smaller,
and since non-(nd) standard reductions are unique.
7

st

If the reduction C[s1 , . . . , sn ] −−→ s′ is an (ndl) (or (ndr), respectively), then
the reduction of s′ has nd-count D′ = D − 1. We make the corresponding
st,ndl

reduction: C[t1 , . . . , tn ] −−→ t′ . This is a smaller counterexample; hence we
get a contradiction also in this case.
Definition 2.10. A program transformation is a relation T between programs
(expressions). A program transformation T is called correct, iff for all expressions P, P ′ : P T P ′ implies P ∼c P ′ .
The reductions rules in definition 2.2 define corresponding program transformations if they are allowed in arbitrary contexts.
Definition 2.11. Let an internal reduction be a non-standard reduction that
takes place within a reduction context. Usually, this is denoted by the label i on
the reduction arrow.
We define complete sets of commuting and forking diagrams adapted from
[Kut99,Kut00]. In the following definition we use a notation for rewrite rules
(i,llet)

(st,a)

(st,a)

(i,llet)

on reduction sequences. For example −→ · −→ ❀ −→ · −→ , where a
is a reduction type. The · on the left hand side is like a joker, and the · on the
right hand side can be seen as an existentially quantified term.
Definition 2.12. Assume given a reduction type (red) and a set of (complementary) reduction types T , where the base calculus reduction types are contained in
T , as well as (red).
A complete set of commuting diagrams for a reduction (red) is a set of rewrite
rules on reduction sequences of the form
i,red

st,a1

st,ak

−−→ . −−→ . . . −−→

st,b1

❀

st,bm

i,ch

i,c1

−−→ . . . −−→ . −−→ . . . . . −−→,
i,red

st,∗

where ci ∈ T , such that for every reduction sequence s −−→ . −−→ t: Either
it can be transformed using one of the meta-reductions into another reduction
i,red

st,∗

sequence from s to t, such that at least −−→ can be replaced. Or . −−→ t can be
st,∗

st,+

prolonged into a longer standard reduction sequence . . . −−→ t −−→ t′ , such that
it can be replaced as above.
A complete set of forking diagrams for a reduction (red) is a set of rewrite rules
on reduction sequences of the form
st,a1

st,ak

i,red

←−− . . . ←−− . −−→

i,c1

❀

i,ch

st,b1

st,bm

−−→ . . . . . −−→ . ←−− . . . ←−−,
st,∗

i,red

where ci ∈ T , such that: Either every reduction sequence s ←−− . −−→ t can
be transformed into another reduction sequence between s and t, such that at
i,red

st,∗

least −−→ is replaced. Or s ←−− . can be prolonged into a reduction sequence
st,+

st,∗

s′ ←−− s ←−− . , such that it can be replaced as above.
We also use reductions not in the base calculus as internal reductions.
8

It is intended that the corresponding meta-rewriting on reduction sequences
terminates, which has to be proved for every such complete set. The complete
sets of commuting (forking) diagrams are not unique.
Note that in many cases, the forking diagrams can be derived from the commuting diagrams.
Lemma 2.13. For every reduction that is not a (llet) or (cp)-reduction, i.e.,
a ∈ {(nd), (lbeta), (lapp), (lcase), (case)}, there are no internal reductions. This
means, every internal a-reduction with a ∈ {(nd), (lbeta), (lapp), (lcase), (case)}
is a standard reduction.
Proof. By inspecting all the finitely many cases.
a

Proposition 2.14. If s −−→ t, where a ∈ {(lbeta), (lapp), (lcase), (case)}, then
s ∼c t.
I.e., all the program transformations defined by one of the reductions
{(lbeta),(lapp),(lcase),(case)} are correct.
a,[]

Proof. Let s′ −−→ t′ by a (a)-reduction on the surface with a ∈
{(lbeta), (lapp), (lcase), (case)}.
We show s′ ≤c t′ exploiting the context lemma. Let R be a reduction context.
i,a
st,a
Then R[s′ ] −→ R[t′ ] is not possible by Lemma 2.13. Then R[s′ ] −→ R[t′ ] by a
unique standard reduction, hence if there a reduction for R[s′ ] with nd-count D,
there is also one for R′ [t′ ] with nd-count D. The context lemma now shows that
s ′ ≤ c t′ .
To show t′ ≤c s′ using the context lemma is similar: If there a standard reduction
for R[t′ ] with nd-count D, there is also one for R[s′ ] with nd-count D. The context
lemma now shows that t′ ≤c s′ .
Hence we have shown s′ ∼c t′ . Since ∼c is a congruence, we have also that
C[s′ ] ∼c C[t′ ] for an arbitrary context C. Hence the proposition holds.

3

Correctness of the reduction (llet)

The union of the reductions (llet),(lapp),(lcase) is denoted as (lll). The reduction
lll+ means a reduction sequence consisting only of (lll)-reductions of length at
least 1. Accordingly lll∗ is defined as any number of (lll)-reductions. (i, llet)0∨1
means no reduction or 1 reduction (i, llet). In the following two lemmas, a stands
a

for an arbitrary reduction −−→.
Lemma 3.1. A complete set of commuting diagrams for (llet) is:
(i,llet)

(st,a)

(st,a)

(i,llet)

(i,llet)

(st,a)

(st,a)

(st,llet)

(i,llet)

(st,lll+ )

– −−→ · −−→ ❀ −−→ · −−→

– −−→ · −−→ ❀ −−→ · −−→
– −−→ · −−→

(st,lll+ )

❀

(i,llet)0∨1

−−→ · −−−→

9

Lemma 3.2. A complete set of forking diagrams for (llet) is:
(st,a)

(i,llet)

– ←−− · −−→
(st,llet)

(st,a)

(i,llet)

(i,llet)

(st,a)

– ←−− · ←−− · −−→
(st,lll+ )

(i,llet)

– ←−−−− · −→
(st,lll+ )

(i,llet)

– ←−−−− · −→

(st,a)

❀ −−→ · ←−−
❀

❀ ←−−
(i,llet

(st,lll+ )

−→ · ←−−−−

(st,lll+ )

❀ ←−−−−
(i,llet)

Proposition 3.3. If s −−→ t, then s ∼c t.
I.e. (llet) is a correct program transformation in any context.
Proof. First we assume that the reduction is on top level.
To use the context lemma, we have to show what happens in a reduction context.
I.e. assume that s ≡ R[s′ ] and s′ is the llet-redex.
Using the forking diagrams, it is possible to construct from a standard reduction
of s a standard reduction of t with the same nd-count. The context lemma then
shows that s ≤c t.
Using the commuting diagrams, it is possible to construct from a standard reduction of t a standard reduction of s with the same nd-count by shifting the
(i,llet)

−−→ to the right. The context lemma then shows that t ≤c s.
Together, this means s ∼c t.
Finally, the congruence property of ∼c implies that a (llet) can be applied everywhere in a term. ✷

4

Garbage Collection: ldel

Garbage collection in the calculus has two forms, a non-cyclic one, and the other
one that also collects cyclic references:
The noncyclic reduction (ldel) is defined as :
(ldel) (letrec x = s in t) → t if x does not occur in t
(ldel) (letrec x = s, E in t) → (letrec E in t) if x does not occur in t, E
The cyclic reduction (ldelcyc) consisting of (ldelcyc1), (ldelcyc2) is defined as :
(ldelcyc1) (letrec x1 = s1 , . . . , xm = sm in t) → (letrec xj = sj , . . . , xm = sm in t)
if xi for 1 ≤ i ≤ j − 1 does not occur in sj , . . . , sm , t and m > 1
(ldelcyc2) (letrec x1 = s1 , . . . , xm = sm in t) → t
if xi for 1 ≤ i ≤ m does not occur in t
Here we show the correctness of (ldel).
Lemma 4.1. A complete set of commuting diagrams for (ldel) is:
(ldel)

(st,a)

(st,a)

(ldel)

– −−→ · −−→ ❀ −−→ · −−→
10

(ldel)

– −−→ ❀

(st,lll+ )

(st,lll+ )

(ldel)

ldel

−−→ · −−→

– −−→ · −−→

(st,lll∗ )

❀

(ldel)

−−→ · −−→

As an example for computing commuting diagrams, we show one case: We write
\ instead of λ.
Example 4.2. We compute the overlap of an (ldel)-redex and a standard (lapp)redex. If the overlap is trivial, then it is not hard to see that the reductions
commute, including the property “standard“.
In the case of a proper overlap, the redex and the corresponding reduction is as
follows:
ldel
((letrec x = c in \y.y) d) −−→ (\y.y d)
On the other hand, if first the (lapp) rule is applied, then:
st,lapp

((letrec x = c in \y.y) d) −−→ (letrec x = c in (\y.y
ldel

−−→ (\y.y

d))

d)
(ldel)

This is covered by the rule −−→ ❀

(st,lll+ )

ldel

−−→ · −−→.

Lemma 4.3. A complete set of forking diagrams for (ldel) is:
(st,a)

(ldel)

– ←−− · −→
+

(st,lll )

❀

(ldel)

– ←−−−− · −→
(st,lll+ )

(ldel)

– ←−−−− · −→

(ldel)

❀
❀

(st,a)

−→ · ←−−
(ldel)

−→

(ldel)

(st,lll∗ )

−→ · ←−−

Lemma 4.4. There are no infinite lll-reductions
Proof. This can be shown by a natural-number valuation of expressions similar
as in [Kut00], which is strictly decreasing in every reduction step. ✷
(ldel)

Proposition 4.5. If s −−→ t, then s ∼c t.
Proof. (sketch)
Follows by induction on the length of reductions from the context lemma, and
since there are no infinite (lll)-reduction sequences. ✷

5

Copying variables

This section contains the reduction (lcv) which is like compressing references
used in letrecs. It can also be described as removing indirections.
(lcv) (letrec x = y, E in C[x]) → (letrec x = y, E in C[y])
(lcv) (letrec x1 = y, x2 = C[x1 ], E in t)
→ (letrec x1 = y, x2 = C[y], E in t)

11

Lemma 5.1. A complete set of commuting diagrams for (lcv) is:
(lcv)

(st,a)

(st,a)

(lcv)

– −→ · −→ ❀ −→ · −→
(lcv) (st,cpn)
(st,cpn) (lcv) (lcv)
– −→ · −→
❀
−→ · −→ · −→.
(lcv) (st,a)
(st,a)
– −→ · −→ ❀ −→ , where a ∈ {case, cpn, ndr, ndl}.
Lemma 5.2. A complete set of forking diagrams for (lcv) is:
(st,a)

(lcv)

(lcv)

(st,a)

– ←−− · −−→ ❀ −−→ · ←−−
(st,cpn)

(lcv)

(lcv)

(lcv)

(st,cpn)

– ←−− · −−→ ❀ −−→ · −−→ · ←−−
(st,a)

(lcv)

(st,a)

– ←−− · −−→ ❀ ←−− for a ∈ {cp, case, ndl, ndr}.
(lcv)

Proposition 5.3. If s −−→ t, then s ∼c t.
I.e., (lcv) is a correct program transformation in any context.
The proof uses the context lemma, and the complete set of commuting and
forking diagrams to meta-reduce reduction sequences.

6

Contextual equivalence of copy reductions

The required diagrams and the proof of correctness of non-standard copy reductions are complex. Only the complete set of commuting diagrams are presented.
For this rule we require a special class of contexts: surface contexts: Surface
contexts define expressions with holes not in the body of an abstraction.
Definition 6.1.
S ::= [] | (S E) | (E S) | (caseA S alts) | (caseA E . . . (p → S) . . .)
| (choice E S) | (choice S E)
| ((letrec . . . in S) | ((letrec . . . , xi = S, . . . in E)
where E stands for an expression. S is called surface context.
We consider the following atomic copy reductions:
(cp) (letrec x1 = s1 , . . . , xn = sn in C[x1 ])
→ (letrec x1 = s1 , . . . , xn = sn in C[s1 ])
where s1 is an abstraction
(cp) (letrec x1 = s1 , . . . , xn = sn in s)
→ (letrec x1 = s1 , . . . , xj = C[s1 ], . . . , xn = sn in s)
where s1 is an abstraction
and where sj ≡ C[x1 ]
We distinguish the (cp)-reduction into two subreductions: If the target occurrence of the variable is in a surface context, then (cpt), otherwise it is a (cpd).
Equivalently, it is a (cpd) iff the target variable is within an abstraction.
Thus ((letrec x = s, E in D[λz.C[x]])) → ((letrec x = s, E in D[λz.C[s]]))
is a reduction of type (cpd).
12

Lemma 6.2. A complete set of commuting diagrams for (cpt), (cpd) is:
(i,cpt)

(st,a)

(i,cpd)

(st,a)

(i,cpd)

(st,lbeta)

– −→ · −→ ❀
(i,cpt) (st,a)
– −→ · −→ ❀

(st,a)

({i,st},cpt)

(st,a)

(i,cpd)

−→ · −−→
(st,a)
−→ , where a ∈ {case, ndr, ndl}.

– −→ · −→ ❀ −→ · −→
(i,cpd) (st,cpn)
(st,cpn) (i,cpd) (i,cpd)
– −→ · −→
❀
−→ · −→ · −→
(i,cpd) (st,a)
(st,a)
– −→ · −→ ❀ −→ , where a ∈ {case, ndr, ndl}.
– −→ ·

−→

❀

(st,lbeta)

−→

·

({i,st},cpt)

−−→ .

This is sufficient to show that the (cp)-reductions retain contextual equivalence
by a meta-reduction on reduction sequences.
(cp)

Proposition 6.3. If s −−→ t, then s ∼c t.
I.e., (cp) is a correct program transformation in any context.
In summary, we can prove:
Theorem 6.4. All the reductions of the base calculus with the exception of
(ndr), (ndl) are correct program transformations
It is obvious that (ndr), (ndl) are not correct as program transformations,
since (choice T rue F alse) may reduce to T rue, but T rue is not equivalent
to (choice T rue F alse).

7

Unique Copy: Inlining

If a letrec-bound variable occurs only once, then it is possible to replace this
variable by the bound expression and to remove the binding:
(ucp) (letrec x = s, E in C[x]) → (letrec E in C[s]), where C[] is a surface
context, s arbitrary, x has exactly one occurrence in C[x] and no
occurrence in E nor in s.
(ucp) (letrec x = s in C[x]) → C[s], where C[] is a surface context, s arbitrary,
and x has exactly one occurrence in C[x] and no occurrence in s.
(ucp) (letrec x = s, y = C[x], E in t) → (letrec y = C[s], E in t), where C[]
is a surface context, s arbitrary, x has exactly one occurrence in C[x]
and no occurrence in E,s and t.
Note that if s is an abstraction, then the rule is a combination of (cp) and (ldel).
Lemma 7.1. A complete set of commuting diagrams for (ucp) is:
(ucp)

(st,a)

– −→ · −→ ❀
(ucp) (st,a)
– −→ · −→ ❀
(ucp)

(st,a)

– −→ · −→

❀

(st,a)

(ucp)

−→ · −→
(ldel)
−→ · −→ for a ∈ {case, ndr, ndl, cpn}

(st,a)
(st,a)

−→ for a ∈ {case, ndr, ndl}
13

(ucp)

(st,lll∗ )

(st,lll∗ )

(ucp)

– −→ · −→ ❀ −→ · −→
(ucp)
where the extreme case −→ ❀
(ucp)
(st,cpn) (ldel)
– −→ ❀
−→ · −→

(ucp)

−→ is excluded.

(ucp)

Proposition 7.2. If s −−→ t, then s ∼c t.
I.e., (ucp) is a correct program transformation in any context.

8

Conclusion

The rewriting based method of computing complete sets of commuting (resp.
forking) diagrams to prove program transformations to be correct is demonstrated to be successful. We are able to show that all deterministic reduction
rules in the rather complex lambda calculus λndlr and also some other rules are
correct. A general automatic method to compute diagrams by checking all nontrivial overlaps would be a valuable tool and deserves further research efforts.

References
Abr90.

Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research
Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.
ACCL91. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J Lévy. Explicit substitutions.
J. functional programming, 4(1):375–416, 1991.
AF97.
Z.M. Ariola and M Felleisen. The call-by-need lambda calculus. J. functional
programming, 7(3):265–301, 1997.
AFM+ 95. Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A callby-need lambda calculus. In Principles of programming languages, pages
233–246, San Francisco, California, 1995. ACM Press.
AK94.
Z.M. Ariola and Jan Willem Klop. Cyclic lambda graph rewriting. In LICS
94, pages 416–425. IEEE Press, 1994.
Bar84.
H.P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. NorthHolland, Amsterdam, New York, 1984.
KSS98.
Arne Kutzner and Manfred Schmidt-Schauß. A nondeterministic call-byneed lambda calculus. In International Conference on Functional Programming 1998, pages 324–335. ACM Press, 1998.
Kut99.
Arne Kutzner. A non-deterministic call-by-need lambda-calculus with erratic choice: operational semantics, program transformations and applications. draft of thesis, 1999.
Kut00.
Arne Kutzner. Ein nichtdeterministischer call-by-need Lambda-Kalkül mit
erratic choice: Operationale Semantik, Programmtransformationen und Anwendungen. Dissertation, J.W.Goethe-Universität Frankfurt, 2000. in german.
Mes00.
José Meseguer. Rewriting Logic and Maude: concepts and applications. In
Leo Bachmair, editor, Proceedings RTA’2000, pages 1–26. Springer-Verlag,
2000.
MOW98. John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda
calculus. J. of Functional programming, 8:275–317, 1998.

14

MSC99.

MST96.
Pit97.
Smi92.
SS00.

A.K.D. Moran, D. Sands, and M. Carlsson. Erratic fudgets: A semantic
theory for an embedded coordination language. In Coordination ’99, volume
1594 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
Ian Mason, Scott F. Smith, and Carolyn L. Talcott. From operational semantics to domain theory. Information and Computation, 128:26–47, 1996.
Andrew D. Pitts. Operationally-based theories of program equivalence. In
Semantics and Logics of Computation. Cambridge University Press, 1997.
S.F. Smith. From operational to denotational semantics. In 7th International Conference MFPS, LNCS 598, pages 54–76. Springer-Verlag, 1992.
M. Schmidt-Schauß. FUNDIO: A lambda-calculus with a recursive let, case,
constructors, and an IO-interface, 2000. draft.

15

(lbeta) ((λx.s) t) → (letrec x = t in s)
(cpn) (letrec x1 = s1 , x2 = x1 , . . . , xj = xj−1 , xj+1 = sj+1 . . . in C[xj ])
→ (letrec x1 = s1 , x2 = x1 , . . . , xj = xj−1 , xj+1 = sj+1 . . . in C[s1 ])
where s1 is an abstraction
(cpn) (letrec x1 = s1 , x2 = x1 , . . . , xj = xj−1 , xj+1 = C[xj ], . . . in s)
→ (letrec x1 = s1 , x2 = x1 , . . . , xj = xj−1 , xj+1 = C[s1 ], . . . in s)
where s1 is an abstraction
(llet) (letrec x1 = s1 , . . . , xn = sn in (letrec y1 = t1 , . . . , ym = sm in r))
→ (letrec x1 = s1 , . . . , xn = sn , y1 = t1 , . . . , ym = sm in r)
(llet) (letrec x1 = s1 , . . . , xi =
(letrec y1 = t1 , . . . , ym = tm in si ), . . . , xn = sn in r)
→ (letrec x1 = s1 , . . . , xn = sn , y1 = t1 , . . . , ym = sm in r)
(lapp) ((letrec xi = ti in t) s) → (letrec xi = ti in (t s))
(lcase) (caseA (letrec E in t) alts) → (letrec E in caseA t alts)
(case) (caseA (cA,i t1 . . . tn ) . . . ((cA,i y1 . . . yn ) → t) . . .)
→ (letrec y1 = t1 . . . yn = tn in t)
letrec x1 = (cA,i t1 . . . tj1 ),
x2 = x1 tj1 +1 . . . tj2 ,
...
(case)
xm = xm−1 tjm−1 +1 . . . tjm ,
...
C[caseA (xm tjm +1 . . . tjm+1 ) . . . ((cA,i z1 . . . zn ) → t)])
−→
letrec x1 = (cA,i y1 . . . yj1 ), y1 = t1 , . . . yj1 = tj1 ,
x2 = x1 yj1 +1 . . . yj2 , yj1 +1 = tj1 +1 , . . . , yj2 = tj2 ,
...
xm = xm−1 yjm−1 +1 . . . yjm , yjm−1 +1 = tjm−1 +1 , . . . , yjm = tjm ,
...
C[(letrec yjm +1 = tjm +1 , . . . , yjm+1 = tjm+1 , z1 = y1 , . . . , zn = yn in t)]
where n = jm and the case-expression may be in a bound or in the in-expression
and where yi are fresh variables
(ndl)
(ndr)

(choice s t) → s
(choice s t) → t

Fig. 1. Reduction rules of λndlr

16

