The Correctness of Launchbury’s Natural
Semantics for Lazy Evaluation
Joachim Breitner
Programming Paradigms Group

arXiv:1405.3099v1 [cs.PL] 13 May 2014

Karlsruhe Institute of Technology, Germany
breitner@kit.edu

May 14, 2014
In his seminal paper „A Natural Semantics for Lazy Evaluation“, John
Launchbury proves his semantics correct with respect to a denotational semantics. We machine-checked the proof and found it to fail, and provide
two ways to fix it: One by taking a detour via a modified natural semantics
with an explicit stack, and one by adjusting the denotational semantics of
heaps.

Contents
1 Introduction
2 Launchbury’s semantics
2.1 Natural semantics . . . . . . . . . . . . . . . . . . .
2.2 Denotational semantics . . . . . . . . . . . . . . . .
2.3 The correctness theorem and the counter example
2.3.1 Failed attempts at fixing the proof . . . . .
2.3.2 A suitable alternative to ≤ . . . . . . . . . .

2
.
.
.
.
.

3
3
4
5
5
6

3 The stacked semantics
3.1 Equivalency with the natural semantics . . . . . . . . . . . . . . . . . . .
3.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7
7
8

4 The update-based semantics
4.1 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10
10

5 Related work

12

6 Discussion

13

7 Future work

14

A Appendix
A.1 Properties of the denotational semantics . . . . . . . . . . . . . . . . . . .
A.2 Properties of the update-based denotational semantics . . . . . . . . . .

15
15
19

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

1. Introduction
The Natural Semantics for Lazy Evaluation created by Launchbury [Lau93] has turned
out to be a popular and successful foundation for theoretical treatment of lazy evaluation, especially as the basis of semantic extensions [NH09, Nak10, SGHHOM10, EM04,
BKT00]. Therefore, its correctness and adequacy is important in this field of research.
The original paper defines a standard denotational semantics to prove the natural semantics correct against, and outlines the adequacy proof.
Unfortunately, the correctness proof is flawed: To show that a closed term evaluates to a value with the same denotation by induction on the derivation of the natural
semantics, Launchbury generalizes the correctness statement to non-empty semantic
environments. This is Theorem 2 in [Lau93], and a counter-example can be given (see
Section 2.3). Several later works based on Launchbury rely on this proof and hence also
contain the error.
Fortunately, the error only affects the proof and the correctness theorem still holds for
empty environments. One way to prove this is to add an explicit stack to the judgments
of the semantics, to capture more of the context of evaluation (Section 3). This way, we
need not generalize the statement to arbitrary environments for the inductive proof. As
both semantics are equivalent, this provides the correctness of Launchbury’s semantics.
Another way to fix the problem is to modify the meaning of the ⊔ operator in the
semantics of heap: If this is understood to be a right-sided update instead of a least
upper bound, the original proof by Launchbury goes through almost unmodified. We
reproduce this in Section 4.
All definitions, propositions and proofs were mechanically verified using the theorem prover Isabelle/HOL [NPW02] and can be found in the Archive of Formal Proofs
[Bre13]. Therefore, we take the liberty to concentrate on the important steps and tricky
calculations of the proofs here. In particular, we will not explicate the treatment of
names, we implicitly expect heaps to be distinctly named and we do not show that
partial operations like ⊔ are defined where used. For all gory details, we refer the interested reader to the Isabelle proof document, which not only contains the full proofs,
but also has the LaTeX code of the theorems automatically generated from the proved
statements.
Our contributions are:
• We exhibit an error in the original correctness proof of Launchbury’s semantics.
• We provide a variant of Launchbury’s semantics that allows for simpler proofs.
• We prove its correctness and, by equivalency, the correctness of the original semantics.
• We show that a modification to the original denotational semantics allows the
original correctness proof to go through.
• All these results are formally proven and machine-checked.

2

Γ : ńx. e ⇓ Γ : ńx. e

Γ : e ⇓ ∆ : ńy. e′

L AM

Γ:e⇓∆:v
Γ, x 7→ e : x ⇓ ∆, x 7→ v : v

∆ : e′ [ x/y] ⇓ Θ : v

Γ:ex⇓Θ:v
VAR

A PP

Γ, x1 7→ e1 , . . . , xn 7→ en : e ⇓ ∆ : v
Γ : let x1 = e1 , . . . , xn = en in e ⇓ ∆ : v

L ET

Figure 1: The original natural semantics

2. Launchbury’s semantics
Launchbury defines a semantics for a simple untyped lambda calculus consisting of
variables, lambda abstraction, applications and recursive let bindings:
x, y, z, w ∈ Var
e ∈ Exp ::= ńx. e | e x | x | let x1 = e1 , . . . , xn = en in e
It is worth noting that the term on the right hand side of an application has to be a
variable. A general lambda term of the form e1 e2 would have to be pre-processed to
let x = e2 in e1 x before it can be handled by this semantics.

2.1. Natural semantics
Launchbury gives this language meaning by a natural semantics, specified with the
rules in Figure 1, which obey the following naming convention for heaps and values:
Γ, ∆, Θ ∈ Heap = Var →
7 Exp
v ∈ Val ::= ńx. e
A heap is a partial function from variables to expressions. The domain of an heap Γ,
written dom Γ, is the set of variables bound in the heap.
A value is an expression in weak head normal form. A judgment of the form Γ : e ⇓
∆ : v means that the expression e with the heap Γ reduces to v, while modifying the
heap to ∆.
In this work we treat naming and binding naively, as these issues are not essential
for our results. For example, it is understood that the variables in the premise of the
rule L ET are actually fresh and distinct from the variables bound in the let expression.
Likewise the substitution e′ [ x/y] replaces all free occurrences of y in e′ with x and a
“fresh variable” is fresh with regard to the derivation tree and not just the elements of
the current judgment. To express the latter issue rigorously, we would have to add to
the judgment a set of variables to avoid, following Sestoft [Ses97].
We can take these shortcuts here with good conscience, as all proofs also exist in
machine-checked form and there, naming has been handled rigorously.

3

2.2. Denotational semantics
In order to show that the natural semantics behaves as expected, Launchbury defines a
standard denotational semantics for expressions and heaps, following Abramsky [Abr90].
The semantic domain Value is the initial solution to the domain equation
Value = (Value → Value )⊥ ,
which allows to distinguish ⊥ from λx.⊥. Lifting between Value → Value and Value is
performed using the injection Fn (_) and projection _ ↓Fn . Values are partially ordered
by ⊑.
A semantic environment maps variables to values
ρ ∈ Env = Var → Value
and the initial environment ρ⊥ maps all variables to ⊥.
The domain of an environment ρ, written dom ρ, is the set of variables that are
not mapped to ⊥. The environment ρ|S , where S is a set of variables, is the domainrestriction of ρ to S:
(
ρ x, if x ∈ S
( ρ|S ) x =
⊥
if x 6∈ S.
The environment ρ \ S is defined as the the domain-restriction of ρ to the complement
of S, i.e. ρ \ S := ρ|Var \S .
The semantics of expressions and heaps are mutually recursive. The meaning of a
expression e ∈ Exp in an environment ρ ∈ Env is written as JeKρ ∈ Value and is defined
as
Jńx. eKρ := Fn (λv.JeKρ⊔{ x 7→v} )
Je xKρ := JeKρ ↓Fn JxKρ
JxKρ := ρ x
Jlet x1 = e1 , . . . , xn = en in eKρ := JeK{ x1 =e1 ,...,xn =en } ρ.
The meaning of a heap Γ ∈ Heap in an environment ρ is { Γ} ρ ∈ Env, defined as

{ x1 7→ e1 , . . . , xn 7→ en } ρ = µρ′ .ρ ⊔ ( x1 7→ Je1 Kρ′ , . . . , xn 7→ Jen Kρ′ )
where ⊔ is the least upper bound and µ is the least-fixed-point operator. This definition
only makes sense when all occurring least upper bounds actually exist. This is the case
here, as shown in the machine-checked proofs.
We sometimes write { Γ} instead of { Γ} ρ⊥ , and we write Jx1 7→ e1 , . . . , xn 7→ en Kρ
for ( x1 7→ Je1 Kρ , . . . , xn 7→ Jen Kρ ) as it occurs in the definition of { _} _. In an expression
{ Γ} ({{∆} ρ) we omit the parentheses and write { Γ} { ∆} ρ.
The relation ⊑ on environments is ⊑ on Value, lifted pointwise.
Launchbury additionally introduces the partial order ≤ on environments, where ρ ≤
ρ′ is defined as ∀ x.ρ x 6= ⊥ =⇒ ρ x = ρ′ x. While this captures, as intended, the

4

concept of ρ′ adding bindings to ρ, the use of this definition in the proofs is problematic,
as discussed in the following section.
The notation { Γ} ρ  { ∆} ρ′ is an abbreviation for the expression dom Γ ⊆ dom ∆ ∧
∀ x ∈ dom Γ.({{Γ} ρ) x = ({{∆} ρ′ ) x, and  is transitive.

2.3. The correctness theorem and the counter example
The main correctness theorem for the natural semantics is
Theorem 1 If Γ : e ⇓ ∆ : v, then JeK{ Γ} = JvK{ ∆} .
Launchbury generalizes this to arbitrary environments, supposedly to obtain a stronger
result, and to enable a proof by induction:
‘Theorem’ 2 If Γ : e ⇓ ∆ : v holds, then for all environments ρ ∈ Env, JeK{ Γ} ρ = JvK{ ∆} ρ
and { Γ} ρ ≤ { ∆} ρ.
Counter example 3 ‘Theorem’ 2 does not hold for e = x, v = ńa. let b = b in b, Γ = ∆ =
( x 7→ v) and ρ = ( x 7→ Fn (λ_.Fn (λx.x))).
Proof.
Note that the denotation of v is Fn (λ_.⊥) in every environment. We have Γ : e ⇓ ∆ : v,
so according to the theorem, JeK{ Γ} ρ = JvK{ ∆} ρ should hold, but

JeK{ Γ} ρ = { Γ} ρ x

= ρ x ⊔ JvK{ Γ} ρ

= Fn (λ_.Fn (λx.x)) ⊔ Fn (λ_.⊥)
= Fn (λ_.Fn (λx.x) ⊔ ⊥)
= Fn (λ_.Fn (λx.x))
6= Fn (λ_.⊥)
= JvK{ ∆} ρ.



Tracing the counter example through the original proof we find that in the case for
VAR , the equation ({{∆, x 7→ z} ρ ) x = JzK{ ∆,x 7→z} ρ is used, while in fact ({{∆, x 7→ z} ρ ) x =
ρ x ⊔ JzK{ ∆,x 7→z} ρ holds. So the problem occurs when ρ contains bindings that are, in
some way, incompatible with the semantics of Γ.
2.3.1. Failed attempts at fixing the proof
The main Theorem 1 is not affected by the flaw, as such “bad” environments do not
occur during the evaluation of closed expressions. So it seems that ‘Theorem’ 2 can be
fixed by restricting ρ to a certain subset of all environments that somehow comprises
of all environments occurring in the inductive proof. Such a property will relate ρ with
the semantics of Γ, has to hold for ρ⊥ and needs to be strong enough to hold for the

5

inductive cases. In particular, it needs to be preserved by evaluation. Unfortunately,
the required property does not appear to have a simple definition. As negative results
can be very educating as well, we briefly discuss some apparent definitions and why
they fail.
As we have to relate ρ with the semantics of Γ, a first attempt is to restrict ‘Theorem’
2 to environments for which ∀ x 7→ e ∈ Γ. ρ x ⊑ JeKρ holds. But this property is not
preserved by evaluation: Evaluating x in the heap Γ = ( x 7→ let y = z in ń_. y) yields the
updated heap ∆ = ( x 7→ ń_. y, y 7→ z). An environment with ρ x = Fn (λ_.Fn (λ_.⊥)),
ρ y = ⊥ and ρz = Fn (λ_.⊥) fulfills the property with respect to Γ, but not ∆.
Obviously it is not sufficient to relate ρ with the entries of the heap individually.
Therefore, the next attempt is to consider environments for which ∀ x 7→ e ∈ Γ. ρ x ⊑
JeK{ Γ} ρ or, equivalently ∀ x 7→ e ∈ Γ. ({{Γ} ρ) x ⊑ JeK{ Γ} ρ holds. Here, our counter example is evaluating x in Γ = ( x 7→ ńz. z, y 7→ x). In the inductive case of rule VAR, the
heap becomes (y 7→ x), so an environment ρ with ρ x = ⊥ and ρ y = Fn (λz.z) fulfills
the condition with regard to Γ, but not with regard to (y 7→ x), so the condition is too
weak to allow for an inductive proof.
A different approach would be to demand that the domain of ρ is distinct from the
set of variables bound in Γ and ∆. But in the case for VAR in Launchbury’s proof the
induction hypothesis is invoked for a ρ′ bound by the least-fixed-point operator in the
term (µρ′ .{ Γ} ρ′ ⊔ ( x 7→ JeK{ Γ} ρ′ ) ⊔ ρ) and clearly the domain of ρ′ will include the
variables bound by Γ, so again this requirement is too strong.
As there seems to be no easy characterization of the environments ρ for which we
need the result of ‘Theorem’ 2, we had to find a different proof, which is provided in
Section 3.
2.3.2. A suitable alternative to ≤
A second pitfall is the use of the partial order ≤ to capture that the denotation of the
heap is not modified where defined, but only extended with new bindings. Again in
the proof of case VAR Launchbury first shows that { Γ, x 7→ e} ρ ≤ { ∆, x 7→ z} ρ and
from that concludes ({{Γ, x 7→ e} ρ) x = ({{∆, x 7→ z} ρ) x in order to show the first part
of the correctness statement. But for that conclusion one would first have to show that
({{Γ, x 7→ e} ρ) x 6= ⊥, which is not true in general.
One approach to fix this would be to model environments as partial maps from Var
to Value. Then we could differentiate between variables not bound in ρ and variables
bound to ⊥ and have ≤ state that bound variables have to be equal, whether they are
⊥ or not. This is the approach taken in [Bre13], where it also helps with other technical
issues of the machine formalization, but it adds notational complexity that is unwanted
for this presentation.
Similarly, one could define a relation ρ =S ρ′ which is defined as ∀ x ∈ S.ρ x = ρ′ x,
and always state the set of variables to be compared. But again the notational overhead
is considerable.
Therefore, in this work, we simply use { Γ} ρ  { ∆} ρ′ to express that dom Γ ⊆ dom ∆
and ∀ x ∈ dom Γ.({{Γ} ρ) x = ({{∆} ρ′ ) x.

6

3. The stacked semantics

⇚

⇚

⇚

In order to prove Theorem 1, we take a detour via a different semantics that allows to
perform the induction without the problematic generalization. The judgments of this
semantics are of the form Γ : Γ′ ∆ : ∆′ and have new fields (storing a list of variableexpression pairs) that not only contain the expression currently under evaluation, but
also the expressions whose evaluation has caused the current evaluation, together with
their respective names. Such expressions are always either variables or applications,
so the resulting data structures strongly resembles an evaluation stack, consisting of
update frames and function parameters. We re-use the syntax of heaps (which are unordered) here, but keep in mind that Γ′ and ∆′ are ordered, so that we can talk about
the topmost expression.
The rules are given in Figure 2. When compared to Figure 1 one will find that Γ : e ⇓
∆ : z 7→ v, ∆′ , i.e. the expression under evaluation
∆ : v has become Γ : z 7→ e, Γ′
is the topmost expression in the stack. The variables bound in the heap and stack on
either side of the rule are always distinct – another detail that is not further discussed
here, but handled in the formal development.
The rules L AM and L ET correspond directly to their counterpart in the original semantics.
The rule A PP takes the application e x apart. First, the expression e is bound to a new
name w and put on top of the stack, where e x is replaced by w x, in order to evaluate
e. This evaluation provides a lambda abstraction ńy. e′ The body thereof is then, with x
substituted for y, continued to be evaluated.
The rule VAR just shuffles between the heap and the stack: In order to evaluate a variable, its binding is removed from the heap and put on top of the stack. After evaluation,
the binding is updated with the value and moved back to the heap.
∆ : w 7→ v, ∆′ ,
Note that it follows from the rules that if we have Γ : z 7→ e, Γ′
′
′
then w = z and ∆ = Γ , i.e. during one step of evaluation, only the topmost expression
on the stack can change. We deliberately keep this redundancy in the semantics for a
more natural presentation of, for example, the correctness statement and to allow for
later extensions that might want to modify the stack, such as garbage collection.

3.1. Equivalency with the natural semantics
The stacked semantics is equivalent to the original semantics in the following sense:

(∃ z ∆′ . Γ : z 7→ e, Γ′

⇚

Theorem 4 For all Γ, Γ′ , ∆, e, v we have
∆ : z 7→ v, ∆′ ) ⇐⇒ Γ : e ⇓ ∆ : v.

Proof.
Both directions are proved by induction.



7

Γ, x 7→ e : z 7→ x, Γ′

∆ : z 7→ e′ [ x/y], ∆′

Θ : Θ′

Θ : Θ′

∆ : x 7→ v, z 7→ x, ∆′
∆, x 7→ v : z 7→ v, ∆′

Γ, x1 7→ e1 , . . . , xn 7→ en : z 7→ e, Γ′

⇚

Γ : x 7→ e, z 7→ x, Γ′

⇚ ⇚

Γ : z 7→ e x, Γ′

L AM

⇚

∆ : w 7→ ńy. e′ , z 7→ w x, ∆′

Γ : z 7→ let x1 = e1 , . . . , xn = en in e, Γ′

A PP

VAR

∆ : ∆′

⇚

⇚

Γ : z 7→ ńx. e, Γ′

⇚

Γ : w 7→ e, z 7→ w x, Γ′

⇚

Γ : z 7→ ńx. e, Γ′

∆ : ∆′

L ET

Figure 2: The stacked semantics

3.2. Correctness
For the stacked semantics, we prove correctness with respect to the denotational semantics, in the sense that reduction of a heap and stack preserves their denotation:

Γ : Γ′

⇚

Theorem 5 For all Γ, Γ′ , ∆, ∆′ we have
∆ : ∆′ =⇒ { Γ, Γ′ }  { ∆, ∆′ } .

Proof.
by induction on the derivation of Γ : Γ′

⇚

As this proof is one of the main contributions of this paper, we spell it out in greater
detail, and use the technical lemmas found in appendix A.1.
∆ : ∆′ .

Case: L AM
We need to show { Γ, Γ′ }  { Γ, Γ′ } , which holds trivially.

∆ : w 7→ ńy. e′ , z 7→ w x, ∆′ and ∆ : z 7→ e′ [ x/y], ∆′

so by the induction hypothesis,

{ Γ, w 7→ e, z 7→ w x, Γ′ }  { ∆, w 7→ ńy. e′ , z 7→ w x, ∆′ }
and

{ ∆, z 7→ e′ [ x/y], ∆′ }  { Θ, Θ′ } .

8

⇚

Γ : w 7→ e, z 7→ w x, Γ′

⇚

Case: A PP
We have
Θ : Θ′ ,

We need to show { Γ, z 7→ e x, Γ′ }  { Θ, Θ′ } :

{ Γ, z 7→ e x, Γ′ } = { Γ, w 7→ e, z 7→ e x, Γ′ } \ {w}
{ adding a fresh variable, Lemma 11 }
= { Γ, w 7→ e, z 7→ w x, Γ′ } \ {w}
{ substituting the indirection, Lemma 8 }
 { ∆, w 7→ ńy. e′ , z 7→ w x, ∆′ } \ {w}
{ by the induction hypothesis }
= { ∆, w 7→ ńy. e′ , z 7→ ( ńy. e′ ) x, ∆′ } \ {w}
{ substituting the indirection again, Lemma 8 }
= { ∆, z 7→ ( ńy. e′ ) x, ∆′ }
{ removing the fresh variable again, Lemma 11 }
= { ∆, z 7→ e′ [ x/y], ∆′ }
{ semantics of application }
 { Θ, Θ′ }
{ by the induction hypothesis. }
Case: VAR
We have

{ Γ, x 7→ e, z 7→ x, Γ′ }  { ∆, x 7→ v, z 7→ x, Γ′ }

by the induction hypothesis. Using Lemma 8 on the right hand side, we obtain

{ Γ, x 7→ e, z 7→ x, Γ′ }  { ∆, x 7→ v, z 7→ v, Γ′ } .
Case: L ET
We have

{ Γ, z 7→ let x1 = e1 , . . . , xn = en in e, Γ′ }
 { Γ, x1 7→ e1 , . . . , xn 7→ en , z 7→ e, Γ′ }
{ by unfolding the let-expression, Lemma 13 }
 { ∆, ∆′ }
{ by the induction hypothesis }



From the correctness of the stacked semantics we can easily obtain the correctness of
the original semantics:

⇚

Proof (of Theorem 1).
∆ : z 7→ v for a fresh z by Theorem 4. By
From Γ : e ⇓ ∆ : v, we have Γ : z 7→ e
the theorem just shown, we have { Γ, z 7→ e}  { ∆, z 7→ v} . This implies JeK{ Γ,z7→e} =
JvK{ ∆,z7→v} by Lemma 2. As z is fresh, by Lemma 10 we have JeK{ Γ} = JvK{ ∆} .


9

4. The update-based semantics
We have found another way to fix Launchbury’s correctness proof: We modify the denotational semantics of heaps to be

{ Γ} u ρ = µρ′ .ρ + JΓKuρ′ ,
where

(ρ

+ JΓKuρ′ ) x

=

(

(JΓKuρ′ ) x, if x ∈ dom Γ
ρx

otherwise,

i.e. we replace the least upper bound operator by a right-sided update, and otherwise
let J_Ku_ be defined by the same equations as J_K_ .
Interestingly, the denotational semantics of expressions are the same under both definitions:
Lemma 1 For all e and ρ, JeKρ = JeKuρ .
Proof.
by induction on e. The interesting case is L ET , where we use that { Γ} ρ = { Γ} u ρ if the
domains of Γ and ρ are distinct, which is the case as the variables introduced on the
heap in rule L ET are fresh.

In the following we will only mention J_K_ .

4.1. Correctness
Using the modified denotational semantics we can state ‘Theorem’ 2 as a theorem and
prove it:
Theorem 6 If Γ : e ⇓ ∆ : v holds, then for all environments ρ ∈ Env, JeK{ Γ} uρ = JvK{ ∆} uρ
and { Γ} u ρ  { ∆} u ρ.
Our proof follows Launchbury’s steps quite closely, the only differences are the use
of  instead of ≤ and the slightly different iterative fixed-point expression in case VAR .
Nevertheless we reproduce it here for completeness and clarifying details. The required
technical lemmas about the denotational semantics are compiled in appendix A.2.
Proof.
This is essentially the proof in [Lau93], which proceeds by induction on the derivation
of Γ : e ⇓ ∆ : v.
Case: L AM
This case is trivial.
Case: A PP
By the induction hypothesis we know JeK{ Γ} uρ = Jńy. e′ K{ ∆} uρ and { Γ} u ρ  { ∆} u ρ as
well as Je′ [ x/y]K{ ∆} u ρ = JvK{ Θ} uρ and { ∆} u ρ  { Θ} u ρ.

10

While the second part follows from the transitivity of , the first part is a simple
calculation:
Je xK{ Γ} uρ = JeK{ Γ} uρ ↓Fn JxK{ Γ} uρ

{ by the denotation of application }
= Jńy. e′ K{ ∆} uρ ↓Fn JxK{ Γ} uρ
{ by the induction hypothesis }
= Jńy. e′ K{ ∆} uρ ↓Fn JxK{ ∆} uρ
{ by the induction hypothesis and the definition of  }
= Je′ K({{∆} uρ)(y7→JxK{ ∆} uρ )
{ by the denotation of lambda abstraction }
= Je′ [ x/y]K{ ∆} u ρ
{ by substitution Lemma 17 }
= JvK{ Θ} uρ
{ by the induction hypothesis }
Case: VAR
We know that JeK{ Γ} ρ′ = JvK{ ∆} ρ′ and { Γ} ρ′  { ∆} ρ′ for all ρ′ ∈ Env.
We begin with the second part:

{ x 7→ e, Γ} u ρ = µρ′ . ρ + ({{Γ} u ρ′ )|dom Γ + ( x 7→ JeK{ Γ} uρ′ )
{ by Lemma 16 }
= µρ′ . ρ + ({{Γ} u ρ′ )|dom Γ + ( x 7→ JvK{ ∆} uρ′ )


by the induction hypothesis. Note that
we invoke it for ρ′ with ρ′ 6= ρ!

 µρ′ . ρ + ({{∆} u ρ′ )|dom ∆ + ( x 7→ JvK{ ∆} uρ′ )

{ by induction and the monotonicity of µ with regard to  }
= { x 7→ v, ∆} u ρ
{ by Lemma 16 }
The first part now follows from the second part:
JxK{ x 7→e,Γ} uρ = ({{ x 7→ e, Γ} u ρ) x
u

= ({{ x 7→ v, ∆} ρ) x
= JxK{ x7→v,∆} uρ

{ by the denotation of variables }
{ by the first part and x ∈ dom ( x 7→ e, Γ) }
{ by the denotation of variables }

= JvK{ x7→v,∆} uρ .
Case: L ET
We know that JeK{ Γ,x1 7→e1,...,xn 7→en } ρ = JvK{ ∆} ρ and { Γ, x1 7→ e1 , . . . , xn 7→ en } ρ  { ∆} ρ.

11

For the first part we have
Jlet x1 = e1 , . . . , xn = en in eK{ Γ} ρ

= JeK{ x1 7→e1 ,...,xn 7→en } { Γ} ρ

{ by the denotation of let-expressions }

= JeK{ Γ,x17→e1 ,...,xn 7→en } ρ

{ by Lemma 18 }

= JvK{ ∆} ρ

{ by the induction hypothesis }

and for the second part we have

{ Γ } ρ  { x1 7 → e1 , . . . , x n 7 → e n } { Γ } ρ
 { Γ, x1 7→ e1 , . . . , xn 7→ en } ρ
 { ∆} ρ.

{ because the x1 , . . . , xn are fresh }
{ by Lemma 18 }
{ by the induction hypothesis }



5. Related work
A large number of developments on formal semantics of functional programming languages in the last two decades build on Launchbury’s work. Many of them implicitly
or explicitly rely on the correctness proof as spelled out by Launchbury:
Van Eekelen & de Mol [EM04] add strictness annotations to the syntax and semantics
of Launchbury’s work. They state the correctness as in ‘Theorem’ 2, without spotting
the issue.
Nakata & Hasegawa [NH09] define a small-step semantics for call-by-need and relate
it to a Launchbury-derived big-step semantics. They state the correctness with respect
to the denotational semantics and reproduce the ‘Theorem’ 2 in the flawed form, in
their extended version.
Sánchez-Gil et al. [SGHHOM10] extend Launchbury’s semantics with distributed
evaluation. In their modified natural semantics the heap retains the expression under
evaluation with a special flag, marking them as blocked. Furthermore, the expression
under evaluation has a name. Thus the non-distributed subset of their semantics is
very similar to our stacked semantics and their correctness statement corresponds to
Theorem 6.
An interesting case is the work by Baker-Finch et al. on parallel call-by-need: While
an earlier report [BFKHT99] uses Launchbury’s definitions unmodified and states the
flawed ‘Theorem’ 2, the following publication at ICFP [BKT00] uses an update-based
denotational semantics, unfortunately without motivating that change.
Similarly, Nakata [Nak10], who modifies the denotational semantics to distinguish
direct cycles from looping recursion, uses update-based semantics without further explanation.
This list is just a small collection of many more Launchbury-like semantics. Often
the relation to a denotational semantics is not stated, but nevertheless they are standing
on the foundations laid by Launchbury. Therefore it is not surprising that others have
worked on formally fortifying these foundations as well:

12

Sánchez-Gil et al. identified a step in his adequacy proof relating the standard and the
resourced denotational semantics that is not as trivial as it seemed at first and worked
out a detailed pen-and-paper proof [SGHHOM11]. They also plan to prove the equivalency between Launchbury’s natural semantics and a variant thereof, which was used
by Launchbury in his adequacy proof, in the theorem prover Coq.
As one step in that direction, they address the naming issues and suggest a mixed
representation, using de Bruijn indices for locally bound variables and names for free
variables [SGHHOM12]. This corresponds to our treatment of names in the formal
development, using the Nominal logic machinery [UK12] locally but not for names
bound in heaps.
They also proved that the natural semantics with a modified A PP that uses an indirection on the heap instead of substitution, can be proven equivalent to the original
semantics [SGHHOM14]. This is one step towards showing Launchbury’s alternative
natural semantics equivalent to the original.

6. Discussion
Although we have found a flaw in the proof and the formulation of the correctness
theorem in Launchbury’s semantics, the essential correctness result (as formulated in
Theorem 1) stills holds. In that sense our work, especially with the computer-verified
proofs in [Bre13], actually strengthens the foundations of formal work in that field.
We have provided two ways to fix the problem: One by adding a stack to the operational semantics, and one by changing the denotation of heaps. Both variants have
precursors in the literature: The extended heaps of [SGHHOM10] resemble the heapstack-pairs of our semantics, while Baker-Finch et al. [BKT00] and Nakata [Nak10] use
right-sided updates in their denotational heap semantics.
Adding the stack to the judgments of the natural semantics, although it does not
affect the evaluation of expressions at all, seems to make the semantics more suitable
for formal proofs than the original semantics:
• Launchbury’s global notion of “fresh variable” is hard to work with, as noted
and fixed before by adding to the judgments an explicit list of variable names to
avoid [Ses97]. As the stack in our semantics already contains these names, this
additional step is not required.
• While proving Theorem 5, the environment ρ does not have to be all-quantified
in the inductive step. This simplified the proof a bit and avoids the pitfall that the
original proof fell into.
The similarity with the extended heaps in [SGHHOM10] further supports the usefulness of the stacked semantics.
We had to spend slightly more pages on the properties of the original denotational semantics (Appendix A.1) than of the update-based denotational semantics (Appendix A.2).
This is partly due to more details in the proofs in the former section, partly because +
behaves nicer than ⊔ (e.g. it is defined everywhere). This is orthogonal to the usefulness
of the stack-based natural semantics, which could be proven correct with regard to the

13

updates-based denotational semantics as well.
Unless one has to stick with ⊔, e.g. to stay compatible with previous work using this
definition, little stands in the way of using the update-based denotational semantics to
model the denotation of heaps.

7. Future work
Proving correctness is of course only half the battle: The adequacy of Launchbury’s semantics is not yet formally proven. The original paper itself outlines the steps of a proof,
and some of these steps have since then been spelled out in greater detail [SGHHOM11],
and the same authors are currently working on the equivalency of Launchbury’s original and modified natural semantics [SGHHOM14].
We however found that the adequacy is shown easier and more elegantly by taking
care of indirections and blackholing on the denotational side, and have a complete and
machine-checked proof (yet to be published) of that.
We hope that by proving the correctness and adequacy in a theorem prover, we not
“just” reinforce our theoretical foundations but also create a practical (for a theoretician’s understanding of practical) tool that can be used to experiment with the many
various ways that this semantics can be extended and modified.

Acknowledgments
I would like to thank Andreas Lochbihler and Denis Lohner for careful proof-reading
and very constructive comments. Furthermore I’d like to thank the anonymous referees
at the Journal of Functional Programming for further typo spotting. This work was
supported by the Deutsche Telekom Stiftung.

References
[Abr90]

Samson Abramsky, Research topics in functional programming, ch. The
lazy lambda calculus, pp. 65–116, 1990.

[BFKHT99]

Clem Baker-Finch, David King, Jon Hall, and Phil Trinder, An operational
semantics for parallel call-by-need, Tech. Report 99/1, Faculty of Mathematics and Computing, The Open University, 1999.

[BKT00]

Clem Baker-Finch, David J. King, and Phil W. Trinder, An operational
semantics for parallel lazy evaluation, ACM SIGPLAN International Conference on Functional Programming, 2000.

[Bre13]

Joachim Breitner, The correctness of Launchbury’s natural semantics for lazy evaluation, Archive of Formal Proofs (2013),
http://afp.sf.net/entries/Launchbury, Formal proof development.

14

[EM04]

Marko van Eekelen and Maarten de Mol, Mixed lazy/strict graph semantics, Tech. Report NIII-R0402, Radboud University Nijmegen, January
2004.

[Lau93]

John Launchbury, A natural semantics for lazy evaluation, Principles of
Programming Languages, 1993, pp. 144–154.

[Nak10]

Keiko Nakata, Denotational semantics for lazy initialization of letrec: black
holes as exceptions rather than divergence, 7th Workshop on Fixed Points
in Computer Science, 2010.

[NH09]

Keiko Nakata and Masahito Hasegawa, Small-step and big-step semantics
for call-by-need, Journal of Functional Programming 19 (2009), no. 6, 699–
722.

[NPW02]

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel, Isabelle/HOL
- a proof assistant for higher-order logic, vol. 2283, 2002.

[Ses97]

Peter Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming 7 (1997), 231–264.

[SGHHOM10] Lidia Sánchez-Gil, Mercedes Hidalgo-Herrero, and Yolanda OrtegaMallén, An operational semantics for distributed lazy evaluation, Trends in
Functional Programming, vol. 10, Intellect Books, 2010, pp. 65–80.
[SGHHOM11]

, Relating function spaces to resourced function spaces, ACM Symposium on Applied Computing, 2011, pp. 1301–1308.

[SGHHOM12]

, A locally nameless representation for a natural semantics for lazy evaluation, International Colloquium on Theoretical Aspects of Computing,
2012, pp. 105–119.

[SGHHOM14]

, The role of indirections in lazy natural semantics, PSI, 2014.

[UK12]

Christian Urban and Cezary Kaliszyk, General bindings and alphaequivalence in nominal Isabelle, Logical Methods in Computer Science 8
(2012), no. 2.

A. Appendix
A.1. Properties of the denotational semantics
This section collects the various technical lemmas about the denotational semantics that
we need in the proof for the correctness of the stacked semantics (Theorem 5).
The following two lemmas give the result of looking up a variable x in the denotation
of a heap { Γ} ρ, depending on whether x is bound in the heap or not.
Lemma 2 If x 7→ e ∈ Γ, then ({{Γ} ρ) x = ρ x ⊔ JeK{ Γ} ρ. In particular, ({{Γ} ) x = JeK{ Γ} .

15

Proof.
by unfolding the fixed point once.



Lemma 3 If x ∈
/ dom Γ, then ({{Γ} ρ) x = ρ x. In particular, if dom Γ ∩ dom ρ = ∅, then
({{Γ} ρ) \ dom Γ = ρ.
Proof.
by unfolding the fixed point once.



The denotation of a heap { Γ} ρ is a refinement of the environment ρ, as shown by the
next lemma.
Lemma 4 ρ ⊑ { Γ} ρ.
Proof.
This follows from the fixed-point equation { Γ} ρ = ρ ⊔ JΓK{ Γ} ρ.



We often need to show that the denotation of a heap is less defined than an environment, and usually do this using the following lemma.
Lemma 5 If ρ ⊑ ρ∗ and JΓKρ∗ ⊑ ρ∗ , then { Γ} ρ ⊑ ρ∗ .
Proof.
By definition, { Γ} ρ is the least fixed point of the functorial λρ′ .ρ ⊔ JΓKρ′ , and hence the
least pre-fixed point. By assumption, ρ∗ is a pre-fixed point, so { Γ} ρ ⊑ ρ∗ holds.

The following two lemmas provide a way to replace a binding in a heap.
Lemma 6 If Je1 K{ x1 7→e2,Γ} ρ ⊑ Je2 K{ x 7→e2,Γ} ρ then { x1 7→ e1 , Γ} ρ ⊑ { x1 7→ e2 , Γ} ρ.
Proof.
By Lemma 5, it suffices to show ρ ⊑ { x 7→ e2 , Γ} ρ, which follows from Lemma 4, and

( x 7→ Je1 K{ x7→e2,Γ} ρ, JΓK{ x7→e2,Γ} ρ ) ⊑ { x 7→ e2 , Γ} ρ.
This follows from Lemma 2 for Variables from dom Γ, and for x via the assumption,
Lemma 2 and transitivity of ⊑.

Lemma 7 If Je1 K{ x 7→e2,Γ} ρ ⊑ Je2 K{ x 7→e2,Γ} ρ and Je2 K{ x 7→e1,Γ} ρ ⊑ Je1 K{ x 7→e1,Γ} ρ holds then
{ x 7→ e1 , Γ} ρ = { x 7→ e2 , Γ} ρ.
Proof.
By Lemma 6 and antisymmetry of ⊑.



The next lemmas allows to replace a subexpression e of an expression e′ [e] by a variable bound to that subexpression:
Lemma 8 Let z ∈
/ dom ρ. Then { y 7→ e′ [e], z 7→ e, Γ} ρ = { y 7→ e′ [z], z 7→ e, Γ} ρ.

16

Proof.
We have JzK{ y7→e′[e],z7→e,Γ} ρ = JeK{ y7→e′[e],z7→e,Γ} ρ by Lemma 2, so by the compositionality
of the denotational semantics, Je′ [z]K{ y7→e′ [e],z7→e,Γ} ρ = Je′ [e]K{ y7→e′ [e],z7→e,Γ} ρ holds.
Analogously, Je′ [e]K{ y7→e′ [z],z7→e,Γ} ρ = Je′ [z]K{ y7→e′ [z],z7→e,Γ} ρ, so by Lemma 7 the proof is
finished.

Removing bindings from the denotation of a heap and adding them again does not
modify the heap.
Lemma 9 { Γ} ({{Γ, ∆} \ dom Γ) = { Γ, ∆}
Proof.
We use the antisymmetry of ⊑. Note that we use the first inequality in the proof of the
second inequality.
⊑: By Lemma 5, it suffices to show

({{Γ, ∆} \ dom Γ) ⊔ JΓK{ Γ,∆} ⊑ { Γ, ∆} .
which follows immediately from Lemma 2.
⊒: Again by Lemma 5, it suffices to show
JΓ, ∆K{ Γ} ({{Γ,∆} \dom Γ) ⊑ { Γ} ({{Γ, ∆} \ dom Γ),
which we verify pointwise. For x 7→ e ∈ Γ, we even have equality:
JeK{ Γ} ({{Γ,∆} \dom Γ) = ({{Γ, ∆} \ dom Γ) x ⊔ JeK{ Γ} ({{Γ,∆} \dom Γ)

{ because x ∈ dom Γ }
= ({{Γ} ({{Γ, ∆} \ dom Γ)) x
{ by Lemma 2. }

For x 7→ e ∈ ∆, we have
JeK{ Γ} ({{Γ,∆} \dom Γ) ⊑ JeK{ Γ,∆}

{ by case ⊑ and the monotonicity of JeK_ . }
= ({{Γ, ∆} ) x.
{ by Lemma 2 }
= ({{Γ, ∆} \ dom Γ) x.
/ dom Γ. }
{ because x ∈
= ({{Γ} ({{Γ, ∆} \ dom Γ)) x
/ dom Γ. }
{ by Lemma 3, as x ∈



Fresh variables do not affect the denotation of expressions, as shown in the next tree
lemmas.

17

Lemma 10 If all variables in S are fresh with regard to e, then JeKρ = JeKρ\S .
Proof.
by induction on e.



Lemma 11 Let x be fresh. Then { Γ} ρ = ({{ x 7→ e, Γ} ρ) \ { x}.
Proof.
If x is fresh with regard to Γ, then a binding of x in ρ does not affect JΓKρ , as shown by
induction on the expressions bound in Γ.

Lemma 12 If dom Γ is fresh with regard to ∆ and ρ, then { Γ} { ∆} ρ = { Γ, ∆} ρ.
Proof.
We show this by using antisymmetry.
⊑: By invoking Lemma 5 twice, it suffices to show
– ρ ⊑ { Γ, ∆} ρ, which follows from Lemma 4, as well as
– J∆K{ Γ,∆} ρ ⊑ { Γ, ∆} ρ and
– JΓK{ Γ,∆} ρ ⊑ { Γ, ∆} ρ, which follows from Lemma 2.
⊒: By Lemma 10, it suffices to show ρ ⊑ { Γ} { ∆} ρ, for which we invoke Lemma 4
twice, and JΓ, ∆K{ Γ} { ∆} ρ ⊑ { Γ} { ∆} ρ. For the latter we consider two cases:
1. For x 7→ e ∈ dom Γ, this follows from Lemma 2.
2. For x 7→ e ∈ dom ∆, we have that dom Γ is fresh with regard to e, so
JeK{ Γ} { ∆} ρ = JeK{ ∆} ρ

{ by Lemma 10 }

= ({{∆} ρ) x
= ({{Γ} { ∆} ρ ) x

{ by Lemma 2 }
/ dom Γ. }
{ by Lemma 3 and x ∈



The last lemma of this section states that unpacking a let-expression on the heap
preserves the denotation of the existing bindings.
Lemma 13 { z 7→ let x1 = e1 , . . . , xn = en in e, Γ}  { x1 7→ e1 , . . . , xn 7→ en , z 7→ e, Γ} .
Proof.
Let Γ′ ::= ( x1 7→ e1 , . . . , xn 7→ en , z 7→ e, Γ) and e′ ::= let x1 = e1 , . . . , xn = en in e.
The lemma follows from { z 7→ e′ , Γ} = { Γ′ } \ { x1 , . . . , xn }, which we show using
antisymmetry.
⊑: The left hand side is a least fixed point, so it suffices to show Jz 7→ e′ , ΓKΓ′ \{ x1 ,...,xn } =
Γ′ \ { x1 , . . . , xn }. For variables in the domain of Γ, this follows from Lemma 2. For
z, we have
Je′ KΓ′ \{ x1 ,...,xn } = JeK{ x1 7→e1,...,xn 7→en } ({{Γ′} \{ x1,...,xn })

{ by the denotation of let-expressions }
= JeK{ Γ′ }
{ by Lemma 9 }
⊑ Γ′ z.
{ by Lemma 2. }

18

⊒: First note that
{ Γ ′ } ⊑ { x1 7 → e1 , . . . , x n 7 → e n } { z 7 → e ′ , Γ }

(∗)

for which it suffices to show
JΓ′ K{ x1 7→e1 ,...,xn 7→en } { z7→e′,Γ} ⊑ { x1 7→ e1 , . . . , xn 7→ en } { z 7→ e′ , Γ} ,
which falls into two cases:
1. For z, we have
JeK{ x1 7→e1 ,...,xn 7→en } { z7→e′,Γ} = Je′ K{ z7→e′,Γ}

{ by the denotation of let-expressions }
= ({{z 7→ e′ , Γ} ) z
{ by Lemma 2 }
= ({{ x1 7→ e1 , . . . , xn 7→ en } { z 7→ e′ , Γ} ) z
{ by Lemma 3 }
2. For x 7→ e∗ ∈ ( x1 7→ e1 , . . . , xn 7→ en , Γ), we have
Je∗ K{ x1 7→e1 ,...,xn 7→en ,z7→e′ ,Γ} = ({{ x1 7→ e1 , . . . , xn 7→ en , z 7→ e′ , Γ} ) x
by Lemma 2. Using Lemma 12 this concludes case 2, as the x1 , . . . , xn are fresh
with regard to (z 7→ e′ , Γ).
Now we can show

{ Γ ′ } \ { x1 , . . . , x n } ⊑ { x1 7 → e1 , . . . , x n 7 → e n } { z 7 → e ′ , Γ } \ { x1 , . . . , x n }
{ by (∗) }
= { z 7→ e′ , Γ }
{ by Lemma 3. }



A.2. Properties of the update-based denotational semantics
To reproduce Launchbury’s correctness proof (Theorem 6) with regard to the updatebased semantics we first show some lemmas about the denotational semantics.
The lemma that justifies the introduction of the update-based semantics is the following, which is the equality that was used in the original proof but does not hold for the
standard denotational semantics (see Section 2.3).
Lemma 14 For ( x 7→ e) ∈ Γ we have ({{Γ} u ρ) x = JeK{ Γ} uρ .
Proof.
by unrolling the fixed point once.



19

The other case when looking up a variable in the denotation of a heap is
Lemma 15 For x ∈
/ dom Γ we have ({{Γ} u ρ) x = ρ x.
Proof.
by unrolling the fixed point once.



We show an alternative, iterative definition of the heap semantics.

Lemma 16 { x 7→ e, Γ} u ρ = µρ′ . ρ + ({{Γ} u ρ′ )|dom Γ + ( x 7→ JeK{ Γ} uρ′ ) .

A corresponding lemma can be found in Launchbury [Lau93], but without proof. As
the proof involves some delicate fixed-point-juggling, we include it here in detail:
Proof.
Let L = (λρ′ . ρ + Jx 7→ e, ΓKρ′ ) be the functorial of the fixed point on the left hand side,
R be the functorial on the right hand side.
By Lemmas 14 and 15, we have
(1) (µL) y = Je′ KµL for y 7→ e′ ∈ dom Γ,
(2) (µL) x = JeKµL ,
(3) (µL) y = ρ y for y ∈
/ { x} ∪ dom Γ.
Similarly, by unrolling the fixed points, we have
(4) (µR) y = Je′ K{ Γ} u(µR) for y 7→ e′ ∈ dom Γ,
(4) (µR) x = JeK{ Γ} u(µR) ,
(4) (µR) y = ρ y for y ∈
/ { x} ∪ dom Γ,
′
and also for ρ ∈ Env (in particular for ρ′ = (µL), (µR)), again using Lemmas 14 and
15,
(7) ({{Γ} u ρ′ ) y = JeK{ Γ} uρ′ for y 7→ e′ ∈ dom Γ,
(8) ({{Γ} u ρ′ ) y = ρ′ y for y ∈
/ dom Γ.
We obtain
(9) { Γ} u (µR) = (µR)
from comparing (4)–(6) with (7) and (8). We can also show
(10) { Γ} u (µL) = (µL),
by antisymmetry and use that least fixed points are least pre-fixed points:
⊑: We need to show that (µL) + JΓK(µL) ⊑ (µL), which follows from (1).
⊒: We need to show that { Γ} u (µL) + Jx 7→ e, ΓK{ Γ} u(µL) ⊑ { Γ} u (µL). For dom Γ, this
follows from (7), so we show JeK{ Γ} u(µL) ⊑ (µL) x = JeK(µL) , which follows from the
monotonicity of JeK_ and case ⊑.
To show the lemma, (µL) = (µR), we use the antisymmetry of ⊑ and the leastness
of least fixed points:
⊑: We need to show that L (µR) = µR, i.e.
– ρ y = (µR) y for y ∈
/ { x} ∪ dom Γ, which follows from (6),
′
– Je KµR = (µR) y for y 7→ e′ ∈ Γ, which follows from (4) and (9) and
– JeKµR = (µR) x, which follows from (5) and (9).
⊒: Now we have to show that R (µL) = (µL), i.e.

20

– ρ y = (µL) y for y ∈
/ { x} ∪ dom Γ, which follows from (3),
′
– Je K{ Γ} u(µL) = (µL) y for y 7→ e′ ∈ Γ, which follows from (1) and (10), and
– JeK{ Γ} u(µL) = (µL) x, which follows from (2) and (10).



Next we prove that substitutions in terms are equivalent to indirections on the heap.
This lemma will also be useful when proving adequacy: Instead of bringing the operational semantics closer to the denotational semantics by replacing the substiution in
the operational semantics with an indirection via the heap, as proposed in [Lau93] and
carried out in [SGHHOM14], this lemma performs the step on the denotational side.
Lemma 17 If y is fresh with regard to ρ, then
JeKρ(y7→JxKρ ) = Je[ x/y]Kρ .
Proof.
By induction on e. All cases are trivial but case L ET , which requires some shuffling of
fixed points. We need to show that
Jlet x1 = e1 , . . . , xn = en in eKρ(y7→JxKρ ) = J(let x1 = e1 , . . . , xn = en in e)[ x/y]Kρ .
using JeKρ′ (y7→JxKρ′ ) = Je[ x/y]Kρ′ and Jei Kρ′ (y7→JxKρ′ ) = Jei [ x/y]Kρ′ for i = 1, . . . , n.
Let Γ = ( x1 7→ e1 , . . . , xn 7→ en ). The variables x1 , . . . , xn are fresh. In particular, none
of them are x or y.
We first show that

{ Γ} u (ρ(y 7→ JxKρ )) = ({{Γ[ x/y]}}u ρ)(y 7→ JxK{ Γ[x/y]}}uρ )

(∗)

using the antisymmetry of ⊑. Let ρ L and ρR denote the left- and right-hand-side of the
equation.
⊑: By the leastness of the fixed point, it suffices to show that ρ(y 7→ JxKρ ) + JΓKρR = ρR ,
which we verify pointwise.
– For y, because the xi are fresh, we have ρ x on both sides.
– For the xi , we have to show Jei Kρ R = Jei [ x/y]K{ Γ[ x/y]}}u ρ , which is our induction
hypothesis (with ρ′ = ρR ).
– For any other variable x′ , we have ρ x′ on both sides.
⊒: Clearly JxK{ Γ[x/y]}}uρ = ρ x = ρ L y, so it remains to show that { Γ[ x/y]}}u ρ ⊑ ρ L \
{y}. We again use the leastness of the fixed point and verify the inequality ρ +
JΓ[ x/y]Kρ L \{y} ⊑ ρ L \ {y} pointwise:
– For y, as y is fresh with regard to ρ, we have ⊥ on both sides.
– For the xi , we have to show Jei [ x/y]Kρ L \{y} = Jei Kρ L , which follows from our
induction hypothesis (with ρ′ = ρ L \ {y}) and (ρ L \ {y})(y 7→ JxKρ L \{y} ) = ρ L .
– For any other variable x′ , we have ρ x′ on both sides.

21

Finally, we calculate
Jlet x1 = e1 , . . . , xn = en in eKρ(y7→JxKρ )

= JeKρL
= JeKρR
= Je[ x/y]K{ Γ[x/y]}}uρ

{ by the denotation of let expressions }
{ by (∗) }
{ by the induction hypothesis }

= J(let x1 = e1 , . . . , xn = en in e)[ x/y]Kρ

{ by the denotation of let expressions. }

The final lemma required for the correctness proof of shows that the denotation of a
heap with only fresh variables can be merged with the heap it was defined over:
Lemma 18 If dom Γ is fresh with regard to ∆ and ρ, then

{ Γ} { ∆} ρ = { Γ, ∆} ρ.
Proof.
First note that

{ ∆} ρ  { Γ} { ∆} ρ,

(∗)

as the variables bound in Γ are fresh and existing bindings in { ∆} ρ keep their semantics.
We use the antisymmetry of ⊑, and the leastness of least fixed points.
⊑: We need to show that { ∆} ρ + JΓK{ ∆,Γ} ρ = { ∆, Γ} ρ. This follows from (∗) and from
unrolling the fixed point on the right hand side once.
⊒: We need to show that ρ + JΓ, ∆K{ Γ} { ∆} ρ = { Γ} { ∆} ρ, which we verify pointwise.
– For x ∈ dom Γ, this follows from unrolling the fixed point on the right hand
side once.
– For x 7→ e ∈ dom ∆ (and hence x ∈
/ dom Γ), we have

(ρ + JΓ, ∆K{ Γ} { ∆} ρ) x = JeK{ Γ} { ∆} ρ
= JeK{ ∆} ρ
{ because dom Γ is fresh with regard to e }
= ({{∆} ρ) x
{ by unrolling the fixed point }
= (JΓK{ ∆} ρ) x
/ dom Γ }
{ because x ∈
– For x ∈
/ dom Γ ∪ dom ∆, we have ρ x on both sides.

22



