Yale University Department of Computer Science

The Unexpurgated Call by Name, Assignment, and the Lambda Calculus

Revised Report^{1}

Martin Odersky and Dan Rabin

Research Report YALEU/DCS/RR-930 May, 1993

This work was supported in part by DARPA grant number N00014-91-J-4043. The second author was supported by an IBM Graduate Fellowship during the preparation of this paper.

1A shorter version of this report appears in the proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 11–13, 1993, and is also available as Yale Research Report YALEU/DCS/RR-929.

The Unexpurgated Call by Name, Assignment, and the Lambda Calculus

Revised Report^{∗}

Martin Odersky and Dan Rabin

Abstract

We define an extension of the call-by-name lambda calculus with additional constructs and reduction rules that represent mutable variables and assignments. The extended calculus has neither a concept of an explicit store nor a concept of evaluation order; nevertheless, we show that programs in the calculus can be implemented using a single-threaded store. We also show that the new calculus has the Church-Rosser property and that it is a conservative extension of classical lambda calculus with respect to operational equivalence; that is, all algebraic laws of the functional subset are preserved.

1 Introduction

Are assignments harmful? Common wisdom in the functional programming community has it that they are: seemingly, they destroy referential transparency, they require a determinate evaluation order, and they weaken otherwise powerful type systems such as ML’s. Consequently, programming languages with a strong functional orientation often forbid or at least discourage the use of assignments.

On the other hand, assignments are useful. With them, one can implement mutable, implicit, distributed state—a powerful abstraction, even if it is easily misused. The traditional alternative offered by functional programming is to make state explicit. The resulting “plumbing” problems can be ameliorated by hiding the state parameter using monads [22, 29] or by using continuation-passing style [13]. Wadler, for example, uses the monad technique in [31] to present “pure” functional programming as an alternative to “impure” programming with assignments. Monads are indeed successful in eliminating explicit mention of state arguments, but they still require a centralized definition of state.

We show here that one need not choose between purity and convenience. We develop a framework that combines the worlds of functions and state in a way that can naturally express advanced imperative constructs without destroying the algebraic properties of the functional subset. The combinations are referentially transparent: names can be freely exchanged with their definitions. More generally, we show that every meaningful operational equivalence of the functional subset carries over to the augmented language.

Since we would like to abstract away from the issues of a particular programming language, we will concentrate in this paper on a calculus for reasoning about functions and assignments. The calculus is notable in that it has neither a concept of an explicit store nor a concept of evaluation order. Instead, expanding on an idea of Boehm [2], we represent “state” by the collection of assignment statements in a term. A Church-Rosser property guarantees that every reduction sequence to normal form yields the same result. Following Plotkin [23] and Felleisen [5], we derive from the reduction rules both a theory and an evaluator, and we study the relationship between them.

The main contributions of this paper are:

• We define (in Section 2) syntax and reduction rules of λ_{var}, a calculus for functions and state.

• We show (in Section 3) that λ_{var} is Church-Rosser and that it admits a deterministic evaluation function which acts as a semi-decision procedure for equations between terms and answers.

• Even though the syntax of λ_{var} is storeless, we show (in Section 4) that λ_{var}-programs can still be efficiently implemented using a single-threaded store.

• We show (in Section 6) a strong conservative extension theorem: every operational equivalence between terms in classical applied λ-calculus also holds in λ_{var} (provided the domain of basic constants and constructors is sufficiently rich). This is

This work was supported in part by DARPA grant number N00014-91-J-4043. The second author was supported by an IBM Graduate Fellowship during the preparation of this paper.

∗A shorter version of this report appears in the proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 11–13, 1993, and is also available as Yale Research Report YALEU/DCS/RR-929.

x ^{∈} V ars  immutable variables
v ^{∈} T ags  mutable variables (tags)
f ^{∈} F Consts  primitive functions
c^{n} ^{∈} Constrs  constructors of arity n (n ≥ 0)
M ^{∈} Λ_{var}  terms

M ::= f | c^{n} | x | x.M | M_{1} M_{2}
| v | pure M | P
P ::= var v.M | M? | M_{1} =: M_{2} | M_{1} ▷ x.M_{2} | return M

Figure 1: Syntax of λ_{var}

to our knowledge the first time such a result has been established for an imperative extension of the λ-calculus.

These properties make λ_{var} suitable as a basis for the design of wide-spectrum languages which combine functional and imperative elements. On the functional side, we generally assume call-by-name, but call-by-value can also be expressed, since strictness can be defined by a δ-rule. On the imperative side, first class variables and procedures can be used as building blocks for mutable objects. We do not impose any particular restrictions on either functions or side-effecting procedures, except for requiring that the difference between them be made explicit.

Building on λ_{var} is attractive because it gives us an equational semantics that makes reasoning about programs quite straightforward. In contrast, the traditional store-based denotational or operational semantics of imperative languages impose a much heavier burden on program derivations and proofs: at every step, one has to consider the global layout of the store, including a map from names to locations and a map from locations to values. Other semantic approaches, such as Hoare logic or weakest predicate transformers might accommodate simpler reasoning methods, but they are not easily extended to structure sharing or higher-order functions.

2 Term Syntax and Reduction Rules of λ_{var}

The term-forming productions of λ_{var} fall into three groups, as shown in Figure 1. The first group consists of clauses defining λ-calculus with primitive function symbols and data constructors. We refer to this basic calculus as the applied λ-calculus. To this kernel language the second group adds mutable variables v and a block construct pure M that encapsulates an imperative computation M. The third group adds the constructs for modeling imperative computations; these constructs form a separate syntactic category of procedures P.

Basic applied λ-terms. We denote functional abstraction (x.M) without the customary leading λ; this modification makes some of our reduction rules more legible. The presence of primitive function symbols f and fixed-arity constructors c^{n} shows the applied nature of the calculus. Basic constants are included as constructors of arity 0. We assume that every calculus we consider has at least the unit value () as basic constant.

Store tags and primitive procedures. The scope of a mutable variable v is delimited by the construct var v.M. Mutable variables, also called tags, are syntactically distinct from the immutable variables introduced by abstractions x.M. We denote tags by the letters u, v, w, and immutable variables by x, y, z.

Tag readers M? and assignments M_{1} =: M_{2} are the primitive procedures. If M computes a tag, M? is the procedure that produces the value associated with that tag without altering the store. Dually, if M_{2} computes a tag, M_{1} =: M_{2} is the procedure that sets that tag to M_{1} and produces an ignorable value.

Composition of procedures. Procedures are composed into sequences using the expression M_{1} ▷ x.M_{2}, which is a syntactic embodiment of the monadicsemantics operation that Wadler [31] calls ‘bind’. This

λ_{var}  Modula
v? ▷ x.M  [v/x]M  variable lookup (implicit in Modula)
N ▷ x.M  N(x) ; M  procedure call, x is result parameter
var v.M  V AR v : T ; M  variable definition
M =: v  v := M  assignment
N ; M  N ; M  sequential composition
return M  RET URN M  return statement
pure M  M  effect masking, implicit in Modula

Figure 2: Correspondence between λ_{var} and Modula

construct connects a procedure^{1} M_{1} with a functional abstraction x.M_{2}. It denotes the procedure that passes the value produced by M_{1} to x.M_{2} in the state resulting from the computation of M_{1}. We take (▷) to be rightassociative and often employ the following abbreviation:

N ; M =^{def} N ▷ x.M  (x ^{∉} fv M).

Coercion of procedures. The λ_{var}-expression return M allows a pure expression M to be used as a procedure; the expression pure M permits (under certain conditions) the coercion of a procedure to a pure expression.

Correspondence with programming languages. Figure 2 relates terms of Λ_{var} with constructs of traditional imperative programming languages. We use Modula as a representative of such a language.

The λ_{var}-calculus deviates from common imperative programming languages in its notation for assignments, which goes from left to right, and in its variable-readers, which are explicit procedures rather than expressions. These notational conventions make tag-matching in the reduction rules easier to follow. In particular, because of the re-orientation of assignments, information and computation in a procedure flows uniformly from left to right. In each case, the conventional notation can be obtained by syntactic sugaring, if desired. We would expect that such sugaring is introduced for any programming languages based on λ_{var}.

Notational conventions for reduction. We use bv M (fv M) to denote the bound (free) identifiers M. Likewise, bt M and ft M denote the bound and free tags in M. A term is closed if fv M = ft M = ∅.

Closed terms are also called programs. We use M ≡ N for syntactic equality of terms (modulo α-renaming) and reserve M = N for convertibility. If R is a notion of reduction, we use M ⟶_{R} N to express that M reduces in one R reduction step to N. M ⟶_{R} → N is used to express that M reduces in zero or more R-steps to N. The subscript is dropped if the notion of reduction is clear from the context. The letter Δ stands for a redex. A superscripted arrow M ⟶^{Δ} N expresses that M reduces to N by contracting redex Δ in M.

A value V is a λ-abstraction, a primitive function, or a (possibly applied) constructor. An observable value (or answer) A is an element of some nonempty subset of the basic constants^{2}.

\begin{aligned}V & ::= & x.M | f | c^{n} M_{1} ... M_{m} (0 ≤ m ≤ n) \\ A & ⊆ & c^{0} \end{aligned}

A context C is a term with a hole [ ] in it. (·) expresses context composition, i.e.

(C_{1} · C_{2}) M ≡ C_{1}[C_{2}[M]].

A pre-state prefix is a context R that has one of the forms

R ::= [ ] | var v.R | M =: v ; R.

The set of variables written in a pre-state prefix R, wr R, is the smallest set that satisfies

\begin{aligned}wr [ ] & = & ∅ \\ wr (var v.R) & = & wr R \\ wr (M =: v ; R) & = & \{v\} ∪ wr R. \end{aligned}

1Actually, any term. We expect that any term so used will reduce to a procedure.

2Other observations such as convergence to an arbitrary value can be encoded using suitable δ-rules.

A state prefix S is a pre-state prefix that satisfies the requirement that wr S ⊆ bt S.

We let letters L, M, N range over terms, while P, Q range over procedures, and V, W range over values.

Following Barendregt [1], we take terms that differ only in the names of bound variables to be equal. Hence all terms we write are representatives of equivalence classes of α-convertible terms. We follow the “hygiene” rule that bound and free variables in a representative are distinct, and we use the same conventions for tags. Thus, for example, M =: v ; var v.M is not a legal term since it contains a bound and a free variable, both with the same name. To satisfy the hygiene condition, we need to α-rename the bound variable v in this term.

Reduction rules. Figure 3 gives the reduction rules of λ_{var}. A reduction relation between terms is the defined in the usual way: we take → to be the smallest relation on Λ_{var} × Λ_{var} that contains the rules in Figure 3 and that, for any context C, is closed under the implication

M → N ⇒ C[M] → C[N].

Rule (β) is the usual β-rule of applied λ-calculus. Rule (δ) expresses rewriting of applied basic functions. To abstract from particular constants and their rewrite rules, we only require the existence of a partial function δ from primitive functions^{3} f and values to terms. We restrict δ not to “look inside” the structure of its argument term, except when the term is a fully applied constructor at top-level. That is, we postulate that for every primitive function f there exist terms N_{f} and N_{f,c^{n}} (c^{n} ^{∈} Constrs) such that for all values V for which δ(f, V) is defined:

δ(f, V) = \{ \begin{matrix}N_{c^{n}} M_{1} ... M_{n} & if V ≡ c^{n} M_{1} ... M_{n} \\ N V & otherwise. \end{matrix}

Procedures can be thought of as axiomatizing the laws of the Kleisli category associated with a monad [18, 31]. Two of the three laws of this monad are embodied in reduction rules: the rule (▷▷) states that (▷) is associative, and the rule (v▷) states return is a left unit. The third law, stating that return is also a right unit, is an operational equivalence (Proposition 5.4 (7)).

Rule (v▷) extends the scope of a tag over a (▷) to the right — this axiomatizes the intuition that allocation is of indefinite time-extent. Variable capture is prevented by the hygiene condition (bound and free variables are always different). Rule (=:▷) passes (), the result value of an assignment, to the term that follows the assignment.

Rules (f), (b_{1}), and (b_{2}) deal with assignments. The fusion rule (f) reduces a pair of an assignment and a dereference with the same tag. The bubble rules (b_{1}) and (b_{2}) allow variable-readers to “bubble” to the left past assignments and introductions involving other tags. Note that bubble and fusion reductions are defined only on tags v whereas the corresponding productions M_{v}? and M_{1} =: M_{v} in the context-free syntax (Figure 1) admit arbitrary terms in place of M_{v}. This is a consequence of tags being first class, for even if M_{v} is not a tag it might still be reducible to one.

The final three rules implement “effect masking”, by which local state manipulation can be isolated for use in a purely functional context. These three rules can be applied only if the argument to pure is of form S[return V] where V is a value and S is a state prefix. The context-condition (wr S ⊆ bt S) for state prefixes S ensures that evaluation of the argument to pure neither affects nor observes global storage. Effect masking “pushes state inwards”, and thus exposes the outermost structure of the result of the pure expression. In the special cases where the result is a basic constant or primitive function the state disappears altogether.^{4}

Example 2.1 (Counters) To illustrate the syntax and reduction semantics of λ_{var}, we construct a function to generate counter objects. The generated counters encapsulate an accumulator cnt. They export a function that takes an increment (inc) and yields the procedure that adds inc to the “current” value of cnt while returning cnt’s “old” value. This is expressed in λ_{var} as follows (with layout indicating grouping):

mkcounter =

initial . var cnt . initial =: cnt ; return inc . \begin{matrix}cnt? ▷ \\ c . \begin{matrix}c + inc =: cnt ; \\ return c \end{matrix} \end{matrix}

The sample reduction given in Figure 4 illustrates the use of mkcounter in a program that defines a counter ctr, increments it, and then inspects the final value. We use the abbreviation CT R ≡ inc . cnt? ▷ c . c +

3Primitive functions of more than one argument are obtained by currying.

4Initially, we studied a calculus that had only one effect masking rule: A context pure (S[return [ ]]) can be dropped if global storage is unaffected and none of the variables bound in S appear in the term in the hole. This approach looks simpler at first glance, but it is not clear how a standard evaluation function for the resulting calculus can be constructed.

β  (x.M) N  → [N/x] M
δ  f V  → δ(f, V)  (δ(f, V) defined)
▷▷ (M ▷ x.N) ▷ y.P  → M ▷ x.(N ▷ y.P)
r▷ (return M) ▷ x.P  → (x.P) M
v▷ (var v.M) ▷ x.P  → var v.(M ▷ x.P)
=:▷ (M =: N) ▷ x.P  → M =: N ; [()/x] P  (x ^{∈} fv P)
f  M =: v ; v? ▷ x.P  → M =: v ; (x.P) M
b_{1} M =: v ; w? ▷ x.P  → w? ▷ x . M =: v ; P  (v ≠ w)
b_{2} var v . w? ▷ x.P  → w? ▷ x . var v.P  (v ≠ w)
p_{c} pure (S[return c^{n} M_{1} ... M_{k}]) → c^{n} (pure (S[return M_{1}])) ... (pure (S[return M_{k}])) (k ≤ n)
p_{λ} pure (S[return x.M])  → x . pure (S[return M])
p_{f} pure (S[return f])  → f

Figure 3: Reduction rules for λ_{var}.

inc =: cnt ; return c. For each step in the reduction, the redex for the next reduction is underlined. Other reduction sequences are possible as well, but they all yield the same normal form, since λ_{var} is Church-Rosser (Theorem 3.10)

3 Fundamental Theorems

In this section, we establish that our calculus has the fundamental properties that make it suitable as a basis for reasoning about programs. Our main goals here are to prove that λ_{var} is Church-Rosser, which establishes that it is meaningful to regard terms as denoting answers, and to show that λ_{var} possesses a standard evaluation order, which makes it reasonable to regard the calculus as a programming language.

Our technical development here parallels the development in [1], Chapters 3 and 11. In Section 3.1 we prove a result combining the finiteness of developments for ⟶_{βδ} with strong normalization for ⟶_{!}. This result will be used to prove the Church-Rosser property in Section 3.2 and to establish the standard evaluation order in Section 3.4. In Section 3.3 we introduce the conversion theory for λ_{var}, the first of our formal theories of program equivalence.

In the sequel, let ⟶_{!} be the union of all reductions in Figure 3 except (β) and (δ).

3.1 Finite Developments

In this subsection, we prove that λ_{var} has the property of finite developments: if we mark some of a term’s β- and δ-redexes, and agree to reduce only marked redexes, all such reduction sequences (which may include !-reductions) terminate. We will use this technical result both in the proof that λ_{var} is Church-Rosser and in the proof that it possesses a standard evaluation order.

First we define the term languages incorporating marked terms and the associated notions of reduction. We define extensions Λ′_{var} and Λ_{var}^{∗} of Λ_{var} as follows:

The terms M in Λ′_{var} are given by extending the productions in Figure 1 with

M ::= ...
| ((x.M_{1}) M_{2})_{0}
| (f M)_{0}

The notion of reduction on Λ′_{var} is ! ∪ β_{0} ∪ δ_{0}, where

\begin{aligned}β_{0} & ((x.M) N)_{0} & → & [N/x] M \\ δ_{0} & (f V)_{0} & → & δ(f, V) \end{aligned}

We also define a language of weighted terms for use in the proof of finite developments. The terms of Λ_{var}^{∗} are those of Λ′_{var}, plus weighted variables x^{n} and weighted function constants f^{n}, where n ≥ 1. Reduction on Λ_{var}^{∗} is defined as on Λ′_{var}, with the additional rule that in

\underline{mkcounter 0} ▷ ctr . ctr 1 ; ctr 0  ⟶_{β}

(var cnt . 0 =: cnt ; return CT R) ▷ ctr . ctr 1 ; ctr 0 ⟶_{v▷}

var cnt . \underline{(0 =: cnt ; return CT R) ▷ ctr . ctr 1 ; ctr 0}  ⟶_{▷▷}
var cnt . 0 =: cnt ; \underline{return CT R ▷ ctr . ctr 1 ; ctr 0}  ⟶_{r▷}
var cnt . 0 =: cnt ; \underline{(ctr . ctr 1 ; ctr 0) CT R}  ⟶_{β}
var cnt . 0 =: cnt ; \underline{CT R 1 ; CT R 0}  ≡
var cnt . 0 =: cnt ; \underline{(inc . cnt? ▷ c . c + inc =: cnt ; return c) 1 ; CT R 0} ⟶_{β}
var cnt . \underline{0 =: cnt ; cnt? ▷ c . c + 1 =: cnt ; return c ; CT R 0}  ⟶_{f}
var cnt . 0 =: cnt ; \underline{(c . c + 1 =: cnt ; return c) 0 ; CT R 0}  ⟶_{β}
var cnt . 0 =: cnt ; 0 + 1 =: cnt ; \underline{return 0 ; CT R 0}  → →

var cnt . 0 =: cnt ; 0 + 1 =: cnt ; 0 + 1 + 0 =: cnt ; return 1

Figure 4: A sample reduction.

rule β_{0} substitution on weighted variables is defined by

[N/x] x^{n} ≡ N.

We now show that ⟶_{!β_{0}δ_{0}} is strongly normalizing on Λ′_{var}, that is, that all sequences of !β_{0}δ_{0}-reductions terminate. To this purpose, we define a norm on Λ_{var}^{∗} that is strictly decreasing under reduction: the norm of a term thus bounds the number of reductions in any sequence starting with that terms. The norm is defined in terms of another measure, the multiplier #M of a term M. Essentially, a multiplier is the number of terms connected in a chain by (▷) operators. It is defined as follows:

#(M ▷ x.N) = 1 + #x.M
#(x.M)  = #M
#(var v.M) = #M
#M  = 1  for all other terms M

The norm ∥ · ∥ is then defined as follows:

∥f∥  = 1
∥f^{n}∥  = n
∥c^{k}∥  = 1
∥x∥  = 1
∥x^{n}∥  = n
∥x.M∥  = 1 + ∥M∥, if x ∉ fv M
∥x.M∥  = 2 + ∥M∥, if x ^{∈} fv M
∥M N∥  = ∥M∥ + ∥N∥
∥v∥  = 1
∥var v.M∥ = 1 + ∥M∥ + #M
∥M?∥  = ∥M∥
∥M =: N∥ = ∥M∥ + ∥N∥
∥M ▷ x.N∥ = (1 + #N)∥M∥ + ∥x.N∥
∥return M∥ = ∥M∥
∥pure M∥ = (∥M∥ + 1)^{(∥M∥+1)}
= Eexp(∥M∥ + 1)

We use the notation Eexp(n) for n^{n}.

Definition. A term M has a decreasing weighting if

((x.M′) N)_{0} ⊆ M, x^{n} ⊆ M
implies n ≥ ∥N∥

and

(f^{n} V)_{0} ⊆ M, δ(f, V) defined
implies n + ∥V ∥ > ∥δ(f, V)∥

Definition. A term M ^{∈} Λ′_{var} is completed to a term in Λ_{var}^{∗} by superscripting some of the bound variables and function symbols in M.

Lemma 3.1 Every term in Λ′_{var} can be completed to a term with a decreasing weighting.

Proof: easy; just work outward.

Lemma 3.2 If M has a decreasing weighting, and

M ⟶_{!β_{0}δ_{0}} N then ∥M∥ > ∥N∥.

Proof: By a case analysis according to the form of reduction:

Case β_{0}

If x ∉ fv M we have [N/x] M ≡ M, so

∥((x.M) N)_{0}∥

= ∥x.M∥ + ∥N∥
= 1 + ∥M∥ + ∥N∥
> ∥M∥
= ∥[N/x] M∥

If x ^{∈} fv M, the fact that ((x.M) N)_{0} has a decreasing weighting gives us

∥((x.M) N)_{0}∥

= ∥x.M∥ + ∥N∥
> ∥[N/x] M∥

The last inequality holds because every instance of N replaces an instance of x having weight n. In fact, the definition of decreasing weighting was motivated by the need to make this case and the following case work out.

Case δ_{0}

In this case the redex is of the form f^{n} V, and we have:

∥f^{n} V ∥

= ∥f^{n}∥ + ∥V ∥
> ∥δ(f, V)∥

Case ▷ ▷

Note that ∥x.M∥ > ∥M∥ irrespective of whether x is free in M. Thus we have

∥(M ▷ x.N) ▷ y.P ∥
= (1 + #(y.P))∥M ▷ x.N∥ + ∥y.P ∥
= (1 + #P)((1 + #(x.N))∥M∥ + ∥x.N∥)
+ ∥y.P ∥
= (1 + #P + #N + #P #N)∥M∥
+ (1 + #P)∥x.N∥ + ∥y.P ∥
> (1 + 1 + #P)∥M∥ + (1 + #P)∥N∥
+∥y.P ∥
= (1 + #(x.N ▷ y.P))∥M∥
+ ∥N ▷ y.P ∥
= ∥M ▷ x.(N ▷ y.P)∥

Case r▷

∥(return M) ▷ x.P ∥
= ∥M∥ + ∥x.P ∥ + #(x.P)∥M∥
> ∥M∥ + ∥x.P ∥
= ∥(x.P) M∥

Case v▷

∥(var v.M) ▷ x.P ∥
= (1 + #P)∥var v.M∥ + ∥x.P ∥
= (1 + #P)(1 + ∥M∥ + #M) + ∥x.P ∥
= 1 + #P + (1 + #P)∥M∥ + (1 + #P)#M
+ ∥x.P ∥
> 1 + (1 + #P) + (1 + #P)∥M∥ + ∥x.P ∥
= 1 + #(M ▷ x.P) + ∥M ▷ x.P ∥
= ∥var v.(M ▷ x.P)∥

Case =:▷

Note that, since P has a decreasing weighting, ∥[()/x] P ∥ ≤ ∥P ∥. Thus we have:

∥M =: N ▷ x.P ∥, x ^{∈} fv P
= (1 + #(x.P))∥M =: N∥ + ∥x.P ∥
= (1 + #P)∥M =: N∥ + ∥P ∥ + 2
> (1 + #P)∥M =: N∥ + ∥[()/x] P ∥ + 1
= (1 + #P)∥M =: N∥ + ∥z.[()/x] P ∥,
where z ∉ fv P
= ∥(M =: N) ▷ z.[()/x] P ∥
= ∥M =: N ; [()/x] P ∥

Case f

Note that ∥M∥ < ∥M =: v∥, so 2∥M =: v∥ + ∥M∥ < 3∥M =: v∥. Thus we have:

∥M =: v ; v? ▷ x.P ∥

= ∥M =: v ▷ z.v? ▷ x.P ∥,

where z ∉ fv P

= (1 + #(z.v? ▷ x.P))∥M =: v∥

+ ∥z.v? ▷ x.P ∥

= (1 + 1 + #P)∥M =: v∥ + 1 + ∥v? ▷ x.P ∥
= (2 + #P)∥M =: v∥ + 1 + (1 + #P)∥v?∥

+ ∥x.P ∥

= (2 + #P)∥M =: v∥ + 1 + (1 + #P)

+ ∥x.P ∥

> 3∥M =: v∥ + 1 + ∥x.P ∥
> 2∥M =: v∥ + 1 + ∥x.P ∥ + ∥M∥
= (1 + #(z.(x.P) M))∥M =: v∥ + ∥z.(x.P) M∥,

where z ∉ fv P ∪ fv M

= ∥M =: v ; (x.P) M∥

Case b_{1}

∥M =: v ; w? ▷ x.P ∥

= ∥M =: v ▷ z.w? ▷ x.P ∥, where z ∉ fv P
= (1 + #(z.w? ▷ x.P))∥M =: v∥

+ ∥z.w? ▷ x.P ∥

= (1 + 1 + #P)∥M =: v∥ + 1

+ ∥w? ▷ x.P ∥

= (2 + #P)∥M =: v∥ + 1 + (1 + #(x.P))∥w?∥

+ ∥x.P ∥

= (2 + #P)∥M =: v∥ + 1 + (1 + #P) + ∥x.P ∥

⋯

We first continue with the (abnormal) case in which x ∉ fv P:

⋯

= (2 + #P)∥M =: v∥ + 1 + (1 + #P)
+ 1 + ∥P ∥
> (2 + #P) + 1 + (1 + #P)∥M =: v∥
+ 1 + ∥P ∥
= (2 + #P) + ∥x.M =: v ▷ z.P ∥,
where z ∉ fv P
= (1 + #(x.M =: v ▷ z.P))∥w?∥
+ ∥x.M =: v ▷ z.P ∥
= ∥w? ▷ x.M =: v ▷ z.P ∥
= ∥w? ▷ x.M =: v ; P ∥

We now complete the argument for the usual case in which x ^{∈} fv P:

⋯

= (2 + #P)∥M =: v∥ + 1 + (1 + #P)
+ 2 + ∥P ∥
> (2 + #P) + 2 + (1 + #P)∥M =: v∥
+ 1 + ∥P ∥
= (2 + #P) + 2 + (1 + #P)∥M =: v∥
+ ∥z.P ∥,
where z ∉ fv P
= (2 + #P) + 2 + ∥M =: v ▷ z.P ∥
= (1 + #(x.M =: v ▷ z.P))∥w?∥
+ ∥x.M =: v ▷ z.P ∥
= ∥w? ▷ x.M =: v ▷ z.P ∥
= ∥w? ▷ x.M =: v ; P ∥

Case b_{2}

∥var v . w? ▷ x.P ∥
= 1 + #(w? ▷ x.P) + ∥w? ▷ x.P ∥
= 1 + (1 + #P) + (1 + #P)∥w?∥ + ∥x.P ∥
= 3 + 2#P + ∥x.P ∥

⋯

We first continue with the case in which x ∉ fv P:

⋯

= 3 + 2#P + 1 + ∥P ∥
> 3 + 2#P + ∥P ∥
= 2 + #P + 1 + ∥P ∥ + #P
= (1 + #P) + 1 + ∥var v.P ∥
= (1 + #(x.var v.P))∥w?∥ + ∥x.var v.P ∥
= ∥w? ▷ x.var v.P ∥

We now complete the argument for the case in which x ^{∈} fv P:

⋯

= 3 + 2#P + 2 + ∥P ∥
> 3 + 2#P + 1 + ∥P ∥
= 3 + #P + 1 + #P + ∥P ∥
= (1 + #P) + 2 + ∥var v.P ∥
= (1 + #(x.var v.P))∥w?∥ + ∥x.var v.P ∥
= ∥w? ▷ x.var v.P ∥

In the analysis of the remaining cases, which involve reductions of pure terms, we make use of the following fact:

For every state prefix S, there are integer constants a_{S} ≥ 0, b_{S} ≥ 1 such that, for all terms M,

∥S[M]∥ = a_{S} + b_{S}∥M∥.

This can be shown by an easy induction over the structure of S. The remaining cases are then as follows:

Case p_{c}

∥pure(S[c^{n} M_{1} … M_{k}])∥

= Eexp(1 + a_{S} + b_{S}(1 + ∥M_{1}∥ + … + ∥M_{k}∥))
> 1 + Eexp(1 + a_{S} + b_{S}∥M_{1}∥) + …

+ Eexp(1 + a_{S} + b_{S}∥M_{k}∥)

= ∥c^{n} (pure (S[return M_{1}])) …

(pure (S[return M_{k}]))∥

Case p_{λ}

∥pure(S[x.M])∥

= Eexp(1 + a_{S} + b_{S}(1 + ∥M∥))
> 1 + Eexp(1 + a_{S} + b_{S}∥M∥)
= ∥pure (S[return M])∥

Case p_{f}

∥pure (S[return f^{n}])∥

= Eexp(1 + a_{S} + b_{S}n)
> n
= ∥f^{n}∥

By the same argument, taking n = 1, one gets ∥pure (S[return f^{n}])∥ > ∥f∥.

This concludes the case analysis and proves Lemma 3.2.

Lemma 3.3 If M ⟶_{!β_{0}δ_{0}} N, and M has a decreasing weighting, then M has a decreasing weighting.

Proof: If M ⟶_{β_{0}} N, the proposition is shown as in [1], Lemma 11.2.18(ii). The other cases are similar, but simpler.

Proposition 3.4 On Λ′_{var} the reduction ⟶_{!β_{0}δ_{0}} is strongly normalizing.

Proof: As in [1], Proposition 11.2.20.

Corollary 3.5 On Λ_{var} the reduction ⟶_{!} is strongly normalizing.

Proof: Every (!)-reduction sequence in Λ_{var} is also a (!∪β_{0}∪δ_{0})-sequence in Λ′_{var} and has (by Proposition 3.4) finite length.

3.2 Church-Rosser

We establish that → is Church-Rosser by combining several subsidiary results. We first establish that ⟶_{!} is Church-Rosser: this result is itself proved by using Newman’s lemma to decompose the problem into a proof of strong normalization plus a proof of the weak Church-Rosser property. We then use the Hindley-Rosen lemma to deduce Church-Rosser for → from the separate Church-Rosser results for ⟶_{!} and for ⟶_{βδ}: this requires that we show that ⟶_{!} → commutes with ⟶_{βδ} →. We now begin this series of proofs.

Lemma 3.6 Let S be a state prefix and let Δ be a redex fully contained in S. If S[M] ⟶^{Δ} S′[M] then S′ is a state prefix.

Proof: Since Δ is fully contained in S, there exists a term N, a tag v and pre-state prefixes R_{1} and R_{2} such that S ≡ R_{1}[N =: v ; R_{2}] and Δ ⊆ N. Assume N ⟶^{Δ} N′. Then S′ ≡ R_{1}[N′ =: v ; R_{2}] is a pre-state prefix. Moreover bt S′ = bt S and wr S′ = wr S. Since S is a state prefix, wr S′ = wr S ⊆ bt S = bt S′. Hence, S′ is a state prefix.

Lemma 3.7 ⟶_{!} is weakly Church-Rosser, that is, M_{0} ⟶_{!} M_{1} and M_{0} ⟶_{!} M_{2} imply that there exists M_{3} such that M_{1} ⟶_{!} → M_{3} and M_{2} ⟶_{!} → M_{3}. The following diagram shows the situation:

[figure: M_{0}; M_{1}; M_{2}; M_{3}; !; !; ^{.......}; !; . . . . . . .; !]

Proof: Assume M_{0} ⟶_{ρ_{1}}^{Δ_{1}} M_{1} and M ⟶_{ρ_{2}}^{Δ_{2}} M_{2}. We distinguish cases according to the relative positions of Δ_{1} and Δ_{2}. If Δ_{1} ≡ Δ_{2} then M_{1} ≡ M_{2} ≡ M_{3}, since the left-hand sides of the rules for (!) in Figure 3 are nonoverlapping. If Δ_{1} and Δ_{2} are disjoint, the proposition follows again from the fact that the left-hand sides of all rules in Figure 3 are non-overlapping. To show the proposition in case Δ_{2} ⊂ Δ_{1}, we distinguish according to the form of Δ_{1}.

Case 1 (f) Δ_{1} ≡ M =: v ; v? ▷ x.P

If M ⟶^{Δ_{2}} M′, the following diagram commutes:

[figure: M =: v ; v? ▷ x.P; M =: v ; (x.P) M; M′ =: v ; v? ▷ x.P; M′ =: v ; (x.P) M′; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2} (twice); Δ_{1}/ρ_{2}; ρ_{1}]

If, on the other hand, P ⟶^{Δ_{2}} P′, the following diagram commutes:

[figure: M =: v ; v? ▷ x.P; M =: v ; (x.P) M; M =: v ; v? ▷ x.P′; M =: v ; (x.P′) M; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 2 Δ_{1} is a b_{1}, b_{2}, ▷▷, r▷, v▷ or =:▷ redex

In these cases Δ_{1} has exactly one residual with respect to ρ_{2}. Hence:

[figure: M_{0}; M_{1}; M_{2}; M_{3}; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 3 (p_{c}) Δ_{1} ≡ pure (S[return c^{n} M_{1} … M_{k}]), k ≤ n

If Δ_{2} ⊆ M_{i} for some i, 0 ≤ i ≤ k, then we reason as in Case 2. If not, Δ_{2} must be fully contained in S. By Lemma 3.6, S/ρ_{2} is a state prefix. Hence the following diagram commutes. (We abbreviate pure (S[return [ ]]) by Π(S)).

[figure: Π(S) [c^{n} M_{1} … M_{k}]; c^{n} (Π(S) [M_{1}]) … (Π(S) [M_{k}]); Π(S/ρ_{1}) [c^{n} M_{1} … M_{k}]; c^{n} (Π(S/ρ_{2}) [M_{1}]) … (Π(S/ρ_{1}) [M_{k}]); Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2} (k times); Δ_{1}/ρ_{2}; ρ_{1}]

Case 4 (p_{λ}) Δ_{1} ≡ pure (S[return x.M])

If Δ_{1} ⊆ M then we reason as in Case 2. If not, Δ_{1} must be fully contained in S. By Lemma 3.6, S/ρ_{1} is a state prefix, and thus Δ_{2}/ρ_{1} is a redex. Furthermore, Δ_{1} has exactly one residual wrt ρ_{2}. From then on the proof is as in Case 2.

Case 5 (p_{f}) Δ_{1} ≡ pure (S[return f])

In this case Δ_{1} is fully contained in S By Lemma 3.6, S/ρ_{1} is a state prefix. Hence, the following diagram commutes:

[figure: pure (S[return f]); pure ((S/ρ_{2}) [return f]); f; Δ_{2}; ρ_{2}; Δ_{1}; ρ_{1}; Δ_{1}/ρ_{2}; ρ_{1}]

This concludes the case analysis for Δ_{2} ⊂ Δ_{1}. The case Δ_{1} ⊂ Δ_{2} is handled symmetrically.

Lemma 3.8 ⟶_{!} → commutes with ⟶_{βδ} →:

[figure: M_{0}; M_{1}; M_{2}; M_{3}; !; βδ; ^{.......}; βδ; . . . . . . .; !]

Proof: By Lemma 3.3.6 of [1], it suffices to show commutativity for the following diagram:

[figure: M_{0}; M_{1}; M_{2}; M_{3}; !; βδ; ^{.......}; βδ; . . . . . . .; !]

Assume then that M_{0} ⟶_{!}^{Δ_{!}} M_{1} and M_{0} ⟶_{βδ}^{Δ_{βδ}} M_{2}. We distinguish cases according to the relative positions of Δ_{!} and Δ_{βδ}. Since the left-hand sides of !-reduction rules do not overlap with those of βδ-reduction rules, Δ_{!} ≢ Δ_{βδ}. If Δ_{1} and Δ_{βδ} are disjoint, the proposition again follows from the fact that the left-hand sides of all rules in Figure 3 are non-overlapping. To show the proposition in the case where Δ_{!} ⊂ Δ_{βδ}, we distinguish cases according to the form of Δ_{βδ}.

Case 1 Δ_{βδ} ≡ (x.M) N

If M ⟶^{Δ_{!}} M′ then the following diagram commutes:

[figure: (x.M) N; (x.M′) N; [N/x] M; [N/x] M′; Δ_{!}; !; Δ_{βδ}; β; Δ_{βδ}/!; β; Δ_{!}/β; !]

If, on the other hand, N ⟶^{Δ_{!}} N′ then the following diagram commutes:

[figure: (x.M) N; (x.M) N′; [N/x] M; [N′/x] M; Δ_{!}; !; Δ_{βδ}; β; Δ_{βδ}/!; β; Δ_{!}/β; ! (for each x in M)]

Case 2 Δ_{βδ} ≡ f (c^{n} M_{1} … M_{n})

In this case we must have M_{i} ⟶^{Δ_{!}} M′_{i}, for some i, 0 ≤ i ≤ n. Because of the restrictions on δ,

f (c^{n} M_{1} … M_{n}) ⟶^{Δ_{βδ}} N_{f,c_{n}} M_{1} … M_{n}. Then

the following diagram commutes:

[figure: f (c^{n} M_{1} … M_{i} … M_{n}); f (c^{n} M_{1} … M′_{i} … M_{n}); N_{f,c^{n}} M_{1} … M_{i} … M_{n}; N_{f,c^{n}} M_{1} … M′_{i} … M_{n}; Δ_{!}; !; Δ_{βδ}; δ; Δ_{βδ}/!; δ; Δ_{!}/δ; !]

Case 3 Δ_{βδ} ≡ f (x.M)

Then M ⟶^{Δ_{!}} M′. Because of the restrictions on δ in Figure 3, we have f (x.M) ⟶^{Δ_{βδ}} N_{f} (x.M). Then the following diagram commutes:

[figure: f (x.M); f (x.M′); N_{f} (x.M); N_{f} (x.M′); Δ_{!}; !; Δ_{βδ}; δ; Δ_{βδ}/!; δ; Δ_{!}/δ; !]

This concludes the case analysis for Δ_{!} ⊂ Δ_{βδ}. The case Δ_{βδ} ⊂ Δ_{!} is handled as in the proof of Lemma 3.7.

Proposition 3.9 ⟶_{!} is Church-Rosser: if M_{0} ⟶_{!} → M_{1} and M_{0} ⟶_{!} → M_{2} then there exists M_{3} such that M_{1} ⟶_{!} →

M_{3} and M_{2} ⟶_{!} → M_{3}.

Proof: The relation ⟶_{!} is weakly Church-Rosser (Lemma 3.7) and strongly normalizing (Corollary 3.5). By Newman’s lemma ([1], Proposition 3.1.25), ⟶_{!} is Church-Rosser.

This allows us to conclude:

Theorem 3.10 → is Church-Rosser.

E ::= [ ]
| E M
| f E
| var v.E
| E?
| M =: E
| E ▷ x.M
| M ▷ x.E
| pure E
| pure S[return E]

Figure 5: Evaluation Contexts in λ_{var}

Proof: The purely functional reduction relation ⟶_{βδ} is easily shown to be Church-Rosser (using Mitschke’s theorem ([1], Theorem 15.3.3), for instance). By Proposition 3.9, ⟶_{!} is Church-Rosser. By Lemma 3.8, ⟶_{!} → commutes with ⟶_{βδ} →. Then, by the lemma of Hindley and Rosen ([1], Proposition 3.3.5), the combined notion of reduction → is Church-Rosser.

3.3 Equational Theory

Reduction gives rise in the standard way to an equational theory. As usual, we define equality (=) to be the smallest compatible equivalence relation that contains reduction.

Definition. The theory λ_{var} has as formulas equations M = N between terms M, N ^{∈} Λ_{var}. It is axiomatized as follows:

\begin{aligned}M → N & ⇒ & M = N \\ M & = & M \\ M = N & ⇒ & N = M \\ M = N, N = L & ⇒ & M = L \end{aligned}

Proposition 3.11 (Consistency of λ_{var}) There are closed terms M, N such that λ_{var} ⊬ M = N.

Proof: Pick two different closed terms in normal form. Because → is Church-Rosser, M and N are not convertible.

3.4 Evaluation

An evaluation function is just a partial function from programs to answers. We define evaluation functions via context machines. At every step, a context machine separates its argument term into a redex and an evaluation context and then performs a reduction on the redex. Evaluation stops once the argument is an answer. Given a notion of reduction → and a notion of “head redex”, we define eval by:

eval_{var} C[M] = eval_{var} C[N],

if M is head redex in C[M] and M → N

eval A  = A.

Definition. An evaluation context E is a context that is of one of the forms given in Figure 5.

Definition. A redex Δ is an evaluation redex of a term M if M ≡ E[Δ], for some evaluation context E. The leftmost outermost evaluation redex in M is called head redex. Every other redex in M is called an internal redex.

Proposition 3.12 eval_{var} is a recursive function.

Proof: Let M ^{∈} Λ_{var}. If M is an answer then eval_{var} M ≡ M. If M has a head-redex, say Δ_{h}, then there is a unique evaluation context E such that M ≡ E[Δ]. Since no two left-hand sides of rules in Figure 3 are unifiable, there is a unique term N such that E[Δ] ⟶^{Δ} E[N]. In that case, eval_{var} M ≡ eval_{var} E[N]. If M has no head-redex, eval_{var} M is undefined. Hence, eval_{var} is a recursive function.

Lemma 3.13 For any evaluation context E and redex Δ, E[Δ] has a unique head redex.

Proof: Direct from the definition of head redex.

What is the relation between λ_{var} and eval_{var}? We can show (by adapting a proof of the Curry-Feys standardization theorem in [1], Section 11.4) that eval_{var} is a semi-decision procedure for equations in λ_{var} of the form M = A where M is a program and A is an answer. First, we need some rather technical lemmas that show that head-redexes are in some sense preserved by internal reductions:

Lemma 3.14 For any term M, procedure P, if M ⟶^{Δ} P, and M ≢ Δ, then M is a procedure.

Proof: An easy case analysis according to the form of reduction in M → P.

Lemma 3.15 If M → N and N has a head redex, then so has M.

Proof: Assume that N has a head redex Δ_{h}, that M ⟶^{Δ} N, and that L is the result of reducing Δ. We distinguish cases according to the relative positions of L and Δ_{h}.

Case 1 L and Δ_{h} are disjoint.

In this case one can find evaluation contexts E, E′, context C, bound variable x, and tag v such that M is one of the following:

(1) E[(E′[Δ_{h}]) (C[Δ])]
(2) E[C[Δ] =: E′[Δ_{h}]]
(3) E[E′[Δ_{h}] ▷ x.C[Δ]]
(4) E[C[Δ] ▷ x.E′[Δ_{h}]]

where C is not an evaluation context

(5) E[pure (S[returnE′[Δ_{h}]])]

where Δ ⊆ S

In each of these cases, Δ_{h} is an evaluation redex of M. By Lemma 3.13, M must thus have a head redex.

Case 2 Δ_{h} ⊆ L

In this case there are contexts C_{1}, C_{2} such that M ≡

C_{1}[Δ] ⟶^{Δ} C_{1}[C_{2}[Δ_{h}]].

Since Δ_{h} is head redex, C_{1} ·C_{2} is an evaluation context. Since evaluation contexts are inductively defined, C_{1} is also an evaluation context. Lemma 3.13 then implies that M has a head redex.

Case 3 L ⊂ Δ_{h}

In this case M ≡ E[M̃] ⟶^{Δ} E[Δ_{h}], for some evaluation context E and term M̃ with Δ ⊂ M̃. Distinguishing cases according to the form of Δ_{h}, we now show that M̃ always has an evaluation redex. For each case, we list the possible forms of M̃ and the corresponding evaluation redex. In the following, C_{P} stands for some context different from [ ]. The cases that refer to C_{P} make use of the fact that if P is a procedure and C_{P} [Δ] ⟶^{Δ} P then C_{P} [Δ] is a procedure (Lemma 3.14).

Case 3.1 Δ_{h} ≡ (x.N_{1}) N_{2}

\underline{M̃ :}  \underline{eval. redex:}
Δ N_{2}  Δ
(x.C[Δ]) N_{2}  M̃
(x.N_{1}) (C[Δ])  M̃

Case 3.2 Δ_{h} ≡ f V

\underline{M̃ :}  \underline{eval. redex:}
Δ V  Δ
f Δ  Δ
f (c^{n} M_{1} … C[Δ] … M_{n})  M̃
f (x.C[Δ])  M̃

Case 3.3 Δ_{h} ≡ N =: v ; v? ▷ x.P

\underline{M̃ :}  \underline{eval. redex:}
Δ ; v? ▷ x.P  Δ
C[Δ] =: v ; v? ▷ x.P M̃
N =: Δ ; v? ▷ x.P  Δ
N =: v ; Δ  Δ
N =: v ; Δ ▷ x.P  Δ
N =: v ; Δ? ▷ x.P  Δ
N =: v ; v? ▷ x.Δ  Δ
N =: v ; v? ▷ x.C_{P} [Δ]  M̃

Case 3.4 Δ_{h} ≡ N =: v ; w? ▷ x.P, v ≠ w

\underline{M̃ :}  \underline{eval. redex:}
Δ ; w? ▷ x.P  Δ
C[Δ] =: v ; w? ▷ x.P M̃
N =: Δ ; w? ▷ x.P  Δ
N =: v ; Δ  Δ
N =: v ; Δ ▷ x.P  Δ
N =: v ; Δ? ▷ x.P  Δ
N =: v ; w? ▷ x.Δ  Δ
N =: v ; w? ▷ x.C_{P} [Δ]  M̃

Case 3.5 Δ_{h} ≡ var v.w? ▷ x.P, v ≠ w

\underline{M̃ :}  \underline{eval. redex:}
var v.Δ  Δ
var v.Δ ▷ x.P  Δ
var v.Δ? ▷ x.P  Δ
var v.w? ▷ x.Δ  Δ
var v.w? ▷ x.C_{P} [Δ]  M̃

Case 3.6 Δ_{h} ≡ (N_{1} ▷ x.N_{2}) ▷ y.P

\underline{M̃ :}  \underline{eval. redex:}
Δ ▷ y.P  Δ
(C[Δ] ▷ x.N_{2}) ▷ y.P M̃
(N_{1} ▷ Δ) ▷ y.P  Δ
(N_{1} ▷ x.C[Δ]) ▷ y.P M̃
(N_{1} ▷ x.N_{2}) ▷ y.Δ  Δ
(N_{1} ▷ x.N_{2}) ▷ y.C_{P} [Δ]  M̃

Case 3.7 Δ_{h} ≡ return N ▷ x.P

\underline{M̃ :}  \underline{eval. redex:}
Δ ▷ x.P  Δ
return C[Δ] ▷ x.P M̃
(return N) ▷ x.Δ  Δ
(return N) ▷ C_{P} [Δ]  M̃

Case 3.8 Δ_{h} ≡ (var v.N) ▷ x.P

\underline{M̃ :}  \underline{eval. redex:}
Δ ▷ x.P  Δ
(var v.C[Δ]) ▷ x.P M̃
(var v.N) ▷ x.Δ  Δ
(var v.N) ▷ x.C_{P} [Δ]  M̃

Case 3.9 Δ_{h} ≡ N_{1} =: N_{2} ▷ x.P, x ^{∈} fv P

\underline{M̃ :}  \underline{eval. redex:}
Δ ▷ x.P  Δ
C[Δ] =: N_{2} ▷ x.P  M̃
N_{1} =: C[Δ] ▷ x.P  M̃
N_{1} =: N_{2} ▷ x.Δ  Δ
N_{1} =: N_{2} ▷ x.C_{P} [Δ]  M̃

Case 3.10 Δ_{h} ≡ pure (S[return V])

An easy induction on the structure of state prefixes shows that, for any state prefix S, pure S[ ] and pure S[return [ ]] are evaluation contexts.

We distinguish further according to the relative positions of Δ and V.

Case 3.10.1 Δ and V disjoint

In this case M̃ ≡ pure (S′[C[Δ] ▷ C′[return V]]), for some state prefix S′ and contexts C, C′. Furthermore, one of the following cases applies:

Case 3.10.1.1 M̃≡ pure (S′[C[Δ]=:v; C′[returnV]])

Then, since S is a state prefix, and since

S′[C[Δ] =: v ; C′[return V]] ⟶^{Δ} S′[return V],

S′[C[Δ] =: v ; C′[ ]] must also be a state prefix. Therefore, M̃ is a redex (and hence an evaluation redex of itself).

Case 3.10.1.2 M̃ ≡ pure (S′[N =: Δ ; C′[return V]])

In this case, since pure S′ is an evaluation context, so is pure (S′[N =: [ ] ; C′[return V]]). Hence, Δ is an evaluation redex of M̃.

Case 3.10.1.3 M̃ ≡ pure (S′[Δ ▷ x.C′[return V]])

In this case pure (S′[[ ] ▷ x.C′[return V]]) is an evaluation context, and Δ is an evaluation redex of M̃.

Case 3.10.2 Δ ⊆ V

In this case, since pure (S[return [ ]]) is an evaluation context, one of the following applies:

\underline{M̃ :}  \underline{eval. redex:}
pure (S[return Δ])  Δ
pure (S[return c^{n} … C[Δ] …])  M̃
pure (S[return x.C[Δ]])  M̃

Case 3.10.3 V ⊂ Δ

In this case, since pure S′ is an evaluation context, M̃ must have the form pure (S′[Δ]), so Δ is an evaluation redex in M̃.

This concludes our case analysis. In every case, M̃ has an evaluation redex. Therefore,

M ≡ E[M̃] ≡ E[E′[Δ′]]

for some evaluation context E′ and redex Δ′. Since E and E′ are evaluation contexts, so is E · E′. Hence, by Lemma 3.13, M contains a head redex.

Lemma 3.16 Let Δ_{h} be head redex and Δ_{i} be an internal redex in M. If M ⟶_{ρ}^{Δ_{i}} N then Δ_{h}/ρ consists of one redex that is head redex in N.

Proof: We distinguish cases according to the relative positions of Δ_{h} and Δ_{i}.

Case 1 Δ_{i} and Δ_{h} are disjoint.

In this case the claim follows by a case analysis identical to the one in Lemma 3.15,Case 1.

Case 2 Δ_{h} ⊆ Δ_{i}

This case is not possible.

Case 3 Δ_{i} ⊂ Δ_{h}

In this case Δ_{h}/ρ is a redex, as is verified by inspecting the relevant clauses of the proof of Lemma 3.7. Furthermore, since M ≡ E[Δ_{h}] ⟶_{ρ} E[Δ_{h}/ρ] for some evaluation context E, Δ_{h}/ρ is an evaluation redex of N. It remains to shown that it is a head redex. Assume that it is not; Then Δ_{h}/ρ is either properly contained in another evaluation redex Δ, or there is another evaluation redex Δ disjoint from, and to the left of, Δ_{h}.

In the first case there are evaluation contexts E_{1}, E_{2}, with E_{2} ≢ [ ] such that

N ≡ E_{1}[Δ] ≡ E_{1}[E_{2}[Δ_{h}/ρ]].

Since Δ_{i} ⊂ Δ_{h}, there is a context C ≢ [ ] such that

M ≡ E_{1}[E_{2}[Δ_{h}]] ≡ E_{1}[E_{2}[C[Δ_{i}]]]

But then Lemma 3.17 implies that E_{2}[Δ_{h}] is a redex, contradicting the assumption that Δ_{h} is head redex in M.

In the second case, one can find evaluation contexts E, E′, E′′, bound variable x, tag v such that N is one of the following:

\begin{matrix}(1) & E[(E′[Δ]) (E′′[Δ_{h}/ρ])] \\ (2) & E[E′[Δ] =: E′′[Δ_{h}/ρ]] \\ (3) & E[E′[Δ] =: v ▷ x.E′′[Δ_{h}/ρ]] \end{matrix}

Hence, M is one of the following:

\begin{matrix}(1) & E[(E′[Δ]) (E′′[Δ_{h}])] \\ (2) & E[E′[Δ] =: E′′[Δ_{h}]] \\ (3) & E[E′[Δ] =: v ▷ x.E′′[Δ_{h}]] \end{matrix}

In each case, Δ an evaluation redex to the left of Δ_{h}. This contradicts the assumption that Δ_{h} is head redex.

Lemma 3.17 For any context C ≢ [ ], evaluation context E ≢ [ ], term M, and redex Δ, if E[C[M]] is a redex and C[Δ] is a redex then E[C[Δ]] is also a redex.

Proof: If, in the left-hand-side of the reduction rule according to which E[C[M] is a redex, M is contained in a meta-variable of [E[C[M]], then clearly E[C[N]] is a redex for any term N. A careful inspection of the reduction rules along with the definition of evaluation contexts E reveals that this is indeed the only way in which the hypotheses of the lemma can be satisfied.

Lemma 3.18 For any term M, internal redexes Δ_{i}, Δ′_{i} in M: If M ⟶_{ρ}^{Δ_{i}} N then all elements of Δ_{i}/ρ are internal redexes in N.

Proof: Assume the contrary. Then there is a redex Δ ^{∈} Δ_{i}/ρ that is head redex in N. By Lemma 3.15, M has a head redex, say Δ_{h}. By Lemma 3.16 and Lemma 3.13, Δ is the residual of Δ_{h}. This contradicts the assumption that Δ ^{∈} Δ_{i}/ρ.

Lemma 3.19 If M → → N, then there exist terms M_{k},

M′_{k} such that M ⟶^{Δ_{h,1}} M_{1} ⟶^{Δ_{h,2}} … ⟶^{Δ_{h,m}} M′_{0} ⟶^{Δ_{i,1}}

M′_{1} ⟶^{Δ_{i,2}} … ⟶^{Δ_{i,n}} N, where each Δ_{h,k} is head redex and each Δ_{i,k} is an internal redex.

Proof: Exactly as in [1], Lemma 11.4.4 – 11.4.6. One needs FD!, Lemma 3.15, Lemma 3.16, and Lemma 3.18.

We are now ready to prove the standardisation theorem:

Theorem 3.20 (Correspondence) For every closed term M and answer A,

λ_{var} ⊢ M = A ⇔ eval_{var} M ≡ A.

Proof: By Lemma 3.19 M → → M′ using only head reductions, and M′ → → A using only internal reductions. Since there is no internal reduction M → A, for any term M, we have M → → M′ using only head reductions. This implies eval_{var} M ≡ A.

4 Simulation by a Single-Threaded Store

We now show that assignments in λ_{var} can be implemented using a single sequentially-accessed store. In order to do this, we define a translation from λ_{var} into another calculus, λ_{σ}, that represents stores explicitly. This calculus has reduction rules that closely resemble the usual meanings of store-operations in imperative models of computation; furthermore, we can define an evaluation function on the language Λ_{σ} that evaluates sequences of such operations in the expected temporal order. We establish that the evaluation functions for λ_{σ} and λ_{var} agree on those terms that are present in both languages. This simulation result shows both that λ_{var} possesses a reasonable implementation as a programming language and also that λ_{var} indeed reasons about assignment as claimed.

To form the new term language Λ_{σ}, we make stores explicit by extending the defining grammar of Λ_{var} (Figure 1) with the additional production M ::= σ · M. Here, σ = {v_{1} : M_{1}, ..., v_{n} : M_{n}} is a state, represented by a set of pairs v : M of tags v and terms M. dom σ = {v_{1}, ..., v_{n}} is called the domain of σ. Tags in dom σ are considered to be bound by σ.

Reduction rules for states are derived from the reduction rules of λ_{var}, with the following modifications: We keep (β) and (δ) reduction as well as the flattening rules (▷▷), (r▷), (v▷), (=:▷). We replace the remaining bubble, fusion, and effect masking rules by rules that construct, access, update, and destroy states, as shown in Figure 6. The new basic constant undef is used to flag an unitialized variable. The rules in Figure 6 define a reduction relation λ_{σ} between terms in Λ_{σ}. This relation can be shown to be confluent.

Note that, even though a state σ can be duplicated in rule σ_{p_{c}}, the resulting states are all read-only. Therefore it suffices to copy a pointer to the state instead of the state itself: state in λ_{σ} is single-threaded [26].

4.1 Church-Rosser

We now embark on the proof that λ_{σ} is confluent. The proof follows the same outline as the corresponding proof for λ_{var} in Section 3, but differs in detail since we are dealing with a different calculus.

We first prove that the reduction ⟶_{β_{0}δ0!} is strongly normalizing for λ_{σ}. We define terms with marked βδredexes Λ′_{σ} and weighted terms Λ_{σ}^{∗} just as we did for Λ_{var}. The definition of the norm ∥ · ∥ is just as for Λ_{var} with the addition of the rules

∥σ · M∥ = Eexp(#M∥σ∥ + ∥M∥)
∥{}∥ = 0
∥σ ∪ {v : N}∥ = ∥σ∥ + ∥N∥

and the revised rule

∥pure M∥ = 1 + ∥M∥.

We note that every term in Λσ^{′} can be completed to a term in Λ_{σ}^{∗} with a decreasing weighting by working outward as before.

Lemma 4.1 For M, N ^{∈} Λ_{σ}^{∗}, if M has a decreasing weighting, and M ⟶_{!β_{0}δ_{0}} N then ∥M∥ > ∥N∥.

σ_{var}  σ · var v.P  → σ ∪ {v:undef} · P
σ_{=:}  σ ∪ {v:M′} · M =: v ; P → σ ∪ {v:M} · P
σ_{?}  σ ∪ {v:M} · v? ▷ x.P  → σ ∪ {v:M} · (x.P) M  (M ≢ undef).
σ_{pure}  pure M  → {} · M
σ_{p_{c}}  σ · return c^{n} M_{1} ... M_{k} → c^{n} (σ · return M_{1} ... (σ · return M_{k}) (k ≤ n)
σ_{p_{λ}}  σ · return x.M  → x . (σ · return M)
σ_{p_{f}}  σ · return [f]  → f

Figure 6: Modified reduction rules for λ_{σ}.

Proof: We proceed by case analysis on the form of single reduction steps.

Case β_{0}, δ_{0}, ▷▷, r▷, v▷, =:▷

In each of these cases, the corresponding case in the proof of Lemma 3.2 is independent of the presence of additional syntactic constructs in Λ_{σ}; hence each is a valid proof for the case in the present lemma.

Case σ_{var}

∥σ · var v.M∥

= Eexp((#var v.M)∥σ∥ + ∥var v.M∥)
= Eexp(#M∥σ∥ + 1 + #M + ∥M∥)
= Eexp(1 + #M(∥σ∥ + 1) + ∥M∥)
> Eexp(#M(∥σ∥ + 1) + ∥M∥)
= Eexp(#M∥σ ∪ {v : undef}∥ + ∥M∥)
= ∥σ ∪ {v : undef}∥

Case σ_{=:}

∥σ ∪ {v : N′} · N =: v ; M∥

= Eexp((#N =: v ; M)∥σ ∪ {v : N′}∥
+ ∥N =: v ; M∥)
= Eexp((1 + #M)(∥σ∥ + ∥N′∥)
+ (1 + #M)∥N =: v∥ + ∥M∥)
= Eexp(∥σ∥ + ∥N′∥ + #M∥σ∥ + #M∥N′∥
+ (1 + #M)(∥N∥ + 1) + ∥M∥)
> Eexp(#M∥σ∥ + #M∥N∥ + ∥M∥)
= ∥σ ∪ {v : N} · M∥

Case σ_{?}

∥σ ∪ {v : N} · v? ; x.M∥
= Eexp((#v? ; x.M)∥σ ∪ {v : N}∥
+ ∥v? ; x.M∥)
= Eexp((1 + #M)(∥σ∥ + ∥N∥)
+ (1 + #M)∥v?∥ + ∥x.M∥)
= Eexp((1 + #M)(∥σ∥ + ∥N∥)
+ 1 + #M + ∥x.M∥)
= Eexp(∥σ ∪ {v : N}∥ + #M∥σ∥
+ #M∥N∥ + 1 + #M + ∥x.M∥)
> Eexp(∥σ ∪ {v : N}∥ + 1 + ∥M∥ + ∥N∥)
= Eexp((#(x.M) N)∥σ ∪ {v : N}∥
+ ∥(x.M) N∥)
= ∥σ ∪ {v : N} · (x.M) N∥

Case σ_{pure}

\begin{aligned}& ∥pure M∥ \\ = & 1 + ∥M∥ \\ > & ∥M∥ \\ = & ∥∅ · M∥ \end{aligned}

Case σ_{p_{c}}

∥σ · return (c^{n} M_{1} … M_{k})∥

= Eexp(#return (c^{n} M_{1} … M_{k})∥σ∥
+ ∥return (c^{n} M_{1} … M_{k})∥)
= Eexp(∥σ∥ + ∥c^{n} M_{1} … M_{k}∥)
= Eexp(∥σ∥ + 1 + ∥M_{1}∥ … ∥M_{k}∥)
> 1 + Eexp(∥σ∥ + ∥M_{1}∥) + …

+ Eexp(∥σ∥ + ∥M_{k}∥)

= ∥c^{n}∥ + ∥σ · return M_{1}∥ + …

+ ∥σ · return M_{k}∥

= ∥c^{n}(σ · return M_{1}) … (σ · return M_{k})∥

Case σ_{p_{λ}}

∥σ · return x.M∥
= Eexp((#return x.M)∥σ∥ + ∥return x.M∥)
= Eexp(∥σ∥ + 1 + ∥M∥)
> 1 + Eexp(∥σ∥ + ∥M∥)
= ∥x.σ · return M∥

Case σ_{p_{f}}

∥σ · return f^{n}∥
= Eexp(∥σ∥ + ∥f^{n}∥)
= Eexp(∥σ∥ + n)
> n
= ∥f^{n}∥

Lemma 4.2 The reduction relation ⟶_{!}_{σ} is weakly Church-Rosser.

Proof: Assume M ⟶_{ρ_{1}}^{Δ_{1}} M_{1} and M ⟶_{ρ_{2}}^{Δ_{2}} M_{2}. We distinguish cases according to the relative positions of Δ_{1} and Δ_{2}. If Δ_{1} ≡ Δ_{2} then M_{1} ≡ M_{2} ≡ M_{3}, since the left-hand sides of the rules in Figure 6 do not overlap. If Δ_{1} and Δ_{2} are disjoint, then the desired property follows again from the lack of overlaps in the rules. We consider now the cases in which Δ_{2} ⊂ Δ_{1} by enumerating the possible forms of Δ_{1}. Wherever the redex Δ_{2} occurs in a store σ, we write the reduction as σ ⟶^{Δ_{2}} σ′ in the remainder of the proof.

Case 1 (σ_{var}) Δ_{1} ≡ σ · var v.M In this case, the pos-

sibilities for Δ_{2} are σ ⟶^{Δ_{2}} σ′ or M ⟶^{Δ_{2}} M′. The following two diagrams show how the weak Church-Rosser property can be established in this case:

[figure: σ · var v.M; σ ∪ {v : undef} · M; σ′ · var v.M; σ′ ∪ {v : undef} · M; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

[figure: σ · var v.M; σ ∪ {v : undef} · M; σ · var v.M′; σ ∪ {v : undef} · M′; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 2 (σ_{=:}) Δ_{1} ≡ σ ∪ {v : N′} · N =: v ; M In this

case Δ_{2} can occur in σ, N′, N, or M:

[figure: σ ∪ {v : N′} · N =: v ; M; σ ∪ {v : N} · M; σ′ ∪ {v : N′} · N =: v ; M; σ′ ∪ {v : N} · M; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

[figure: σ ∪ {v : N′} · N =: v ; M; σ ∪ {v : N} · M; σ ∪ {v : N′′} · N =: v ; M; σ ∪ {v : N} · M; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

[figure: σ ∪ {v : N′} · N =: v ; M; σ ∪ {v : N} · M; σ ∪ {v : N′} · N′′ =: v ; M; σ ∪ {v : N′′} · M; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

[figure: σ ∪ {v : N′} · N =: v ; M; σ ∪ {v : N} · M; σ ∪ {v : N′} · N =: v ; M′; σ ∪ {v : N} · M′; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 3 (σ_{?}) Δ_{1} ≡ σ ∪ {v : N} · v? ▷ x.M In this case,

Δ_{2} can be in σ, N, or M:

[figure: σ ∪ {v : N} · v? ▷ x.M; σ ∪ {v : N} · M N; σ′ ∪ {v : N} · v? ▷ x.M; σ′ ∪ {v : N} · M N; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

[figure: σ ∪ {v : N} · v? ▷ x.M; σ ∪ {v : N} · M N; σ ∪ {v : N′} · v? ▷ x.M; σ ∪ {v : N′} · M N′; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2} (twice); Δ_{1}/ρ_{2}; ρ_{1}]

[figure: σ ∪ {v : N} · v? ▷ x.M; σ ∪ {v : N} · M N; σ ∪ {v : N} · v? ▷ x.M′; σ ∪ {v : N} · M′ N; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 4 (σ_{pure}) Δ_{1} ≡ pure M

[figure: pure M; {} · M; pure M′; {} · M′; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 5 (σ_{p_{c}}) Δ_{1} ≡ σ · return (c^{n} M_{1} … M_{k})

[figure: σ · return (c^{n} M_{1} … M_{k}); c^{n} (σ · return M_{1}) …; σ′ · return (c^{n} M_{1} … M_{k}); c^{n} (σ′ · return M_{1}) …; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1} (k times)]

[figure: σ · return (c^{n} M_{1} … M_{k}); c^{n} (σ · return M_{1}) …; σ · return (c^{n} … M_{i}′ …); c^{n} … (σ′ · return M_{i}′) …; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 6 (σ_{p_{λ}}) Δ_{1} ≡ σ · return x.M

[figure: σ · return x.M; x.(σ · return M); σ · return x.M′; x.(σ · return M′); Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{2}/ρ_{1}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Case 7 (σ_{p_{f}}) Δ_{1} ≡ σ · return f

[figure: σ · return f; σ′ · return f; f; Δ_{1}; ρ_{1}; Δ_{2}; ρ_{2}; Δ_{1}/ρ_{2}; ρ_{1}]

Lemma 4.3 The reduction relations ⟶_{σ_{!}} → and ⟶_{βδ} → commute.

Proof: The proof is a case analysis directly analogous to that in the proof of Lemma 3.8.

Theorem 4.4 →_{σ} is Church-Rosser.

This follows from Lemma 4.2 and Lemma 4.3 by the reasoning used in the proof of Theorem 3.10.

4.2 Evaluation

We now proceed to prove that λ_{σ} possesses a standard order of evaluation. Our development here parallels the proof of Theorem 3.20.

The evaluation contexts for λ_{σ} are given by the following grammar:

E ::= [ ] | E M | f E
| E? | M =: E
| E ▷ x.M | M ▷ x.E
| σ · E | σ · return E

Based on this definition of evaluation context, we define the notion of head redex and the standard evaluation function eval_{σ} for programs in λ_{σ} as was done for λ_{var} in Section 3.4. eval_{σ} closely corresponds to the usual notion of store-based computations with store access and update as single reduction steps. eval_{σ} is a semi-decision procedure for equations between terms and answers in Λ_{σ}.

Lemma 4.5 If M →_{σ} N and N has a head redex, then so has M.

Proof: We proceed in the same manner as for Lemma 3.15.

Case 1 L andΔ_{h}are disjoint

In this case, M must have one of the following forms:

(1) E[(E′[Δ_{h}]) C[Δ]]
(2) E[C[Δ] =: E′[Δ_{h}]]
(3) E[E′[Δ_{h}] ▷ x.C[Δ]]
(4) E[C[Δ] ▷ x.E′[Δ_{h}]]

where C is not an evaluation context

(5) E[σ ∪ {v : C[Δ]} · E′[Δ_{h}]]
(6) E[σ ∪ {v : C[Δ]} · return E′[Δ_{h}]]

In every case, Δ_{h} is an evaluation redex of M, and therefore (by the observation in Lemma 3.13), M has a head redex.

Case 2 Δ_{h} ⊆ L

The reasoning for Lemma 3.15, Case 2, applies here without change.

Case 3 L ⊂ Δ_{h} In this case, M ≡ C̃[M̃] ⟶^{Δ} C̃[Δ_{h}], for some term M̃ with Δ ⊂ M̃. Distinguishing cases according to the form of Δ_{h}, we now show that M̃ always has an evaluation redex. For each case, we list the possible forms of M̃ and the corresponding left redex:

Case 3.1 Δ_{h} ≡ (x.M) N

The reasoning for Lemma 3.15, Case 3.1, applies here without change.

Case 3.2 Δ_{h} ≡ f V

The reasoning for Lemma 3.15, Case 3.2, applies here without change.

Case 3.3 Δ_{h} ≡ σ · var v.P

\underline{M̃ :}  \underline{eval. redex:}
σ′ ∪ {v′ : C[Δ]} · var v.P M̃
σ · Δ  Δ
σ · var v.C[Δ]  M̃

Case 3.4 Δ_{h} ≡ σ ∪ {v : N′} · N =: v ▷ x.P

\underline{M̃ :}  \underline{eval. redex:}

σ ∪ {v : N′, v′ : C[Δ]}

·N =: v ▷ x.P  M̃
σ ∪ {v : C[Δ]} · N =: v ▷ x.P  M̃
σ ∪ {v : N′} · Δ  Δ
σ ∪ {v : N′} · Δ ▷ x.P  Δ
σ ∪ {v : N′} · C[Δ] =: v ▷ x.P M̃
σ ∪ {v : N′} · N =: Δ ▷ x.P  Δ
σ ∪ {v : N′} · N =: v ▷ x.C[Δ]  M̃

Case 3.5 Δ_{h} ≡ σ ∪ {v : N} · v? ▷ x.P

\underline{M̃ :}  \underline{eval. redex:}
σ ∪ {v : N, v′ : C[Δ]} · v? ▷ x.P  M̃
σ ∪ {v : C[Δ]} · v? ▷ x.P  M̃
σ ∪ {v : N} · Δ  Δ
σ ∪ {v : N} · Δ ▷ x.P  Δ
σ ∪ {v : N} · Δ? ▷ x.P  Δ
σ ∪ {v : N} · v? ▷ x.C[Δ]  M̃

Case 3.6 Δ_{h} ≡ pure M

\underline{M̃ :}  \underline{eval. redex:}
pure C[Δ]  M̃

Case 3.7 Δ_{h} ≡ σ · return (c^{n}M_{1} … M_{k})

\underline{M̃ :}  \underline{eval. redex:}

σ ∪ {v : C[Δ]}

·return (c^{n}M_{1} … M_{k}) M̃
σ · Δ  Δ
σ · return Δ  Δ
σ · return (ΔM_{j} … M_{k})  &
(0 ≤ j ≤ k)  Δ
σ · return (c^{n} … C[Δ] …)  M̃

Case 3.8 Δ_{h} ≡ σ · return x.M

\underline{M̃ :}  \underline{eval. redex:}
σ ∪ {v : C[Δ]} · return x.M M̃
σ · Δ  Δ
σ · return Δ  Δ
σ · return x.C[Δ]  M̃

Case 3.9 Δ_{h} ≡ σ · return f

\underline{M̃ :}  \underline{eval. redex:}
σ ∪ {v : C[Δ]} · return f M̃
σ · Δ  Δ
σ · return Δ  Δ

Case 3.10 Δ_{h} ≡ (P ▷ x.Q) ▷ y.R

Case 3.11 Δ_{h} ≡ return P ▷ x.Q

Case 3.12 Δ_{h} ≡ (var v.P) ▷ x.Q

The reasoning for Lemma 3.15, Cases 3.6 to 3.8, applies here without change.

Lemma 4.6 Let Δ_{h} be the head redex and Δ_{i} be some interior redex in M. If M ⟶_{ρ}^{Δ_{i}} N then Δ_{h}/ρ consists of one redex that is head redex in N.

Proof: The proof is entirely analogous to the proof of Lemma 3.16.

Lemma 4.7 For any term M, internal redexes Δ_{i}, Δ′_{i} in M: If M ⟶_{ρ}^{Δ_{i}} N then all elements of Δ_{i}/ρ are internal redexes in N.

Proof: As for Lemma 3.18.

Theorem 4.8 (Correspondence) For every closed term M and answer A,

λ_{σ} ⊢ M = A ⇔ eval_{σ} M ≡ A.

Proof: As for Theorem 3.20.

4.3 Simulation of λ_{var}-evaluation by λ_{σ}- evaluation

Since every term in Λ_{var} is also a member of the language Λ_{σ}, it makes sense to apply λ_{σ}-standard reduction to λ_{var} terms. We now show that both reduction relations are equivalent if we consider only observable results. This equivalence can be interpreted as establishing that eval_{σ} is a correct implementation of eval_{var}. Combined with our informal understanding that eval_{σ} can be implemented by an abstract machine having a store, we will thus be reasonably convinced that λ_{var}- evaluation can also be implemented by such a machine.

We will first prove some auxiliary lemmas that establish that λ_{var}-reduction preserves certain features of state prefixes. We will then introduce a precise notion of correspondence between state prefixes in λ_{var} and explicit stores in λ_{σ}. After proving some properties of the correspondence relation we will prove this section’s main theorem that the two calculi simulate one another.

Define a bubble context to be one generated by the grammar B ::= [ ] | v? ▷ x.B.

Lemma 4.9 Assume λ_{var} ⊢ M → → M′.

(i) If M ≡ var v.N then there is a term N′ ^{∈} Λ_{var} and a bubble context B[ ] such that M′ ≡ B[var v.N′]. (ii) If M ≡ N =: v ; P then there are terms N′, P′ ^{∈} Λ_{var} and a bubble context B[ ] such that M′ ≡ B[N′ =: v ; P′]. (iii) If M ≡ return N then there is a term N′ ^{∈} Λ_{var} such that M′ ≡ return N′. (iv) If M ≡ v?▷x.P then there is a term P′ ^{∈} Λ_{var} such that M′ ≡ v? ▷ x.P′

Proof: By inspection of the reduction rules for λ_{var}, it is clear that only the pure-rules (p_{c}), (p_{λ}), and (p_{f}) can remove a var or =: from a term. Furthermore, there is no rule that can reduce a term with one of these constructs as a prefix to one that has them only within the context of a pure. The only remaining reduction rules involving terms of the forms dealt with in (i) and (ii) are the bubble rules (b_{1}) and (b_{2}), which clearly act to embed the former top-level construct within a bubble context. Similar reasoning establishes (iii) and (iv).

Lemma 4.10 Let M ^{∈} Λ_{var} and assume that M ≡ E[Δ_{h}] → → A, where Δ_{h} is a (f), (b_{1}), or (b_{2}) redex that is head redex in M. Then there is an evaluation context E′ and a pre-state prefix R′ such that M ≡ E′[pure (R′[Δ_{h}])].

Proof: Assume the contrary, that is, that M is not of the desired form. We then consider the remaining possible structures of M and show that none of them can reduce to an answer.

If E ≡ R′ for some pre-state prefix R′, then Lemma 4.9 applies to show that M ↛ → A, and we have a contradiction. Hence E ≡ E_{1} · E_{2} · R′, where E_{1} is an evaluation context, E_{2} is a non-empty evaluation context that is not a pre-state prefix, and R′ is a pre-state prefix. Without loss of generality assume that E_{1} ≡ [ ] and that E_{2} is minimal, that is, E_{2} can be obtained by exactly one of the productions in Figure 5. We distinguish cases according to the form of E_{2}:

Case E_{2} ≡ [ ] N

Assume R′[Δ_{h}] N → → A. By Theorem 4.8, we can choose the reduction to reduce Δ_{h} first. By Lemma 4.9, the reduction can only yield a term of the form B[R′′[N]]. Such a residual term can only interact with its context R′ by means of the bubble-rules (b_{1}) and (b_{2}); thus, there is no way to reduce R′[Δ_{h}] to an abstraction or primitive-function name, and hence no way to reduce the application to an answer. This is a contradiction.

Case E_{2} ≡ f [ ]

We argue similarly to the previous case, noting instead that R′[Δ_{h}] can reduce neither to an abstraction nor to a constructed value.

Case E_{2} ≡ [ ]?

Case E_{2} ≡ N =: [ ]

Case E_{2} ≡ pure (S[return [ ])]

These cases are all similar to the first two cases.

Case E_{2} ≡ [ ] ▷ x.N

In this case E_{2}[R′[Δ_{h}]] is a redex, contradicting the assumption that Δ_{h} is head redex.

Case E_{2} ≡ N ▷ x.[ ]

For this case to apply, N cannot have the form E′[Δ], else Δ_{h} could not be the head redex. Also, N ▷ x.Δ_{h} itself cannot be a redex. Thus N cannot have any of the forms N_{1} ▷ y.N_{2}, return N_{1}, var v.N_{1}, or N_{1} =: N_{2}. Now by Lemma 4.9, Δ_{h} → → B[R′′[N_{1}]], so a headreduction sequence will bubble the tag-lookups in B to the left, where they cannot interact with any of the remaining possible forms for N, hence the entire term cannot reduce to an answer.

Case E_{2} ≡ var v.[ ]

Case E_{2} ≡ N =: v ▷ x.[ ]

Case E_{2} ≡ return [ ]

These cases all contradict the assumption that E_{2} is not a pre-state prefix.

The only remaining case is E_{2} ≡ pure [ ], hence we must have

M ≡ E_{1}[E_{2}[R′[Δ_{h}]]] ≡ E_{1}[pure (R′[Δ_{h}])].

Lemma 4.11 Let M ^{∈} Λ_{var} with M → → A and M ≡ E[pure (R[Δ_{h}])], for some evaluation context E, prestate prefix R, and head redex Δ_{h}. Let Δ_{h} have one of the forms

\begin{matrix}Δ_{h} ≡ N =: v ; P \\ Δ_{h} ≡ v? ▷ x.P. \end{matrix}

Then v ^{∈} bt R.

Proof: We only spell out the proof for the case Δ_{h} ≡ N =: v ; P, the other case is shown by an analogous argument.

Assume the contrary, i.e. v ^{∉} bt R. Take any term M′ such that M → → M′. We show that M′ is not an answer.

Assume that M′ is an answer. By Theorem 3.20, M ⟶_{h} → A, using only head reductions ⟶_{h}. Assume that M ⟶_{h} M_{1} is the first step of this reduction sequence. We have M ≡ E[pure (R[N =: v ; P])]. By Lemma 4.9, M_{1} ≡ E[pure (R[B[N′ =: v ; P′]])], for some terms N′, P′ and bubble context B. If B is nonempty, beginning with v′? for some tag v′, then v′ ^{∈} bt R by the second part of the lemma. Otherwise, since by assumption v ^{∉} bt R, we have that R[N′ =: v ; [ ]] is not part of a state prefix, which implies that pure (R[N′ =: v ; P′]) is not a redex. Therefore, the head redex of M_{1}, if it exists, is contained in N′ =: v ; P′. By induction on the length of the head-reduction sequence we can thus show that M′ ≡ E[pure (R[N′′ =: v ; P′′])], for some terms N′′ and P′′, which contradicts the assumption that M′ is an answer.

Lemma 4.12 Let M ^{∈} Λ_{var} with M → → A and M ≡ E[pure (R[N])], for some evaluation context E, some term N and some pre-state prefix R. If M has a head redex then R is a state prefix.

Proof: Essentially the same as the proof of Lemma 4.11.

Definition. We define a correspondence relation ( ˆ= ) between terms and state-prefixes in Λ_{var} and terms and states in Λ_{σ} as follows:

(i) For any state prefix S, state σ, S ˆ= σ iff

dom σ = bt S,
S ≡ S′[N =: v ; R[ ]], v ^{∉} wr R ⇒
∃N′ . (v:N′) ^{∈} σ ∧ N ˆ= N′,
v ^{∈} bt S, v ^{∉} wr S ⇒ (v:undef) ^{∈} σ

(ii) On terms, ˆ= is axiomatized as follows:

M ≡ M′  ⇒ M ˆ= M′
S ˆ= σ, M ˆ= M′ ⇒ pure(S[M]) ˆ= σ · M′
M ˆ= M′, N ˆ= N′ ⇒ M N ˆ= M′ N′
M ˆ= M′  ⇒ x.M ˆ= x.M′
M ˆ= M′  ⇒ var v.M ˆ= var v.M′
M ˆ= M′  ⇒ M? ˆ= M′?
M ˆ= M′, N ˆ= N′ ⇒ M =: N ˆ= M′ =: N′
M ˆ= M′, N ˆ= N′ ⇒ M ▷ x.N ˆ= M′ ▷ x.N′
M ˆ= M′  ⇒ return M ˆ= return M′
M ˆ= M′  ⇒ pure M ˆ= pure M′

Lemma 4.13 For any term M ^{∈} Λ_{σ} there exists var(M) ^{∈} Λ_{var} such that var(M) ˆ= M. For any state σ ^{∈} Λ_{σ} there exists a state prefix S ≡ var(σ) in Λ_{var} such that S ˆ= σ.

Proof: An easy construction by structural induction. The base cases for terms are obvious. Define var({v_{1} : M_{1}, … v_{n} : M_{n}}) ≡ var v_{1}…. var v_{n}.var(M_{1}) =: v_{1} ; … var(M_{n}) =: v_{n} ; [ ].

Lemma 4.14 For any term M ^{∈} Λ_{var} and state prefix S, there is a state σ such that S ˆ= σ and

pure (S[M]) ⟶_{σ} σ · N.

Proof: Applying  a  σ_{pure}  reduction  one

gets pure (S[M]) → {} · M. Then, repeatedly applying σ_{var} and σ_{=:} reductions, one gets {} · M → → σ · M for some state σ with the required properties.

Lemma 4.15 Assume M ^{∈} Λ_{var}, M_{σ}, N_{σ} ^{∈} Λ_{σ} such that M ˆ= M_{σ} and M_{σ} ⟶_{σ} N_{σ}. Then there is a term N ^{∈} Λ_{var} such that the following diagram commutes:

[figure: M_{σ}; M; N; N_{σ}; ˆ=; σ; . . . . . . . . . . . . .; ˆ=; . . . . . . . . . . . . .; var]

Proof: We distinguish cases according to the reduction rule by which M_{σ} ⟶_{σ} N_{σ}. Since ( ˆ= ) distributes through all Λ_{σ} productions, we can assume without loss of generality that the redex in M_{σ} ⟶_{σ} N_{σ} is the whole term M_{σ}. If M_{σ} is a (b_{1}), (b_{2}), (▷▷), (r▷), (v▷), or (=:▷) redex, the result follows immediately, since these are also reductions in λ_{var}. The remaining cases are as follows (we use Lemma 4.13 freely without mention):

Case M_{σ} ≡ σ · var v.P_{σ}

In this case M ≡ pure (S[var v.P]) for some stateprefix S and term P such that S ˆ= σ and P ˆ= P_{σ}. The lemma then follows from the diagram:

[figure: M_{σ}; σ ∪ {v : undef} · P_{σ}; M; ˆ=; ˆ=]

Case M_{σ} ≡ σ ∪ {v : N′_{σ}} · N_{σ} =: v ; P_{σ}

In this case M ≡ pure (S[N =: v ; P]) for some stateprefix S and terms P, N such that S ˆ= σ ∪ {v : N′_{σ}}, P ˆ= P_{σ} and N ˆ= N_{σ}. The lemma then follows from the diagram:

[figure: M_{σ}; σ ∪ {v : N_{σ}} · P_{σ}; M; ˆ=; ˆ=]

Case M_{σ} ≡ σ ∪ {v : N_{σ}} · v? ▷ x.P_{σ}

In this case M ≡ pure (S[v? ▷ x.P]) for some stateprefix S and term P such that S ˆ= σ ∪ {v : N_{σ}} and P ˆ= P_{σ}. We have some choice in the ordering of the elements of S, so we choose to make the assignment to v be the innermost part of the state prefix. Since M_{σ} is a redex, N_{σ} ≢ undef. Since S ˆ= σ ∪ {v : N_{σ}}, there is an assignment N =: v in S such that N ˆ= N_{σ}. The lemma then follows from the diagram:

[figure: M_{σ}; σ ∪ {v : N_{σ}} · (x.P_{σ}) N_{σ}; M; pure (S[(x.P) N]); ˆ=; fb_{1}b_{2}; ˆ=]

Case M_{σ} ≡ pure N_{σ}

In this case M ≡ pure N, for some term N such that N ˆ= N_{σ}. The lemma then follows from the diagram:

[figure: M_{σ}; {} · N_{σ}; M; ˆ=; ˆ=]

Case M_{σ} ≡ σ · return c^{n} N_{σ,1} ... N_{σ,k}

In this case M ≡ pure (S[return c^{n} N_{1} ... N_{k}]) for some state-prefix S and term N_{i} such that S ˆ= σ and N_{i} ˆ= N_{σ,i} for 1 ≤ i ≤ k. The lemma then follows from the diagram:

[figure: M_{σ}; return c^{n} (σ · N_{σ,i}))_{i=1...k}; M; c^{n} (pure (S[return N_{i}]))_{i=1...k}; ˆ=; p_{c}; ˆ=]

The cases where M_{σ} is a p_{λ} or p_{f} redex are shown analogously to the last case.

Theorem 4.16 (Simulation) For every closed term M ^{∈} Λ_{var} and answer A,

λ_{var} ⊢ M = A ⇔ λ_{σ} ⊢ M = A.

Proof: We first prove “⇒”. Assume λ_{var} ⊢ M = A. By Theorem 3.20 M ⟶_{h} → A using only head reductions. We use an induction on the length of the head reduction sequence from M to A.

Base case. If M ≡ A, there is nothing to show.

Induction step. If M ≢ A, then we have (in λ_{var}):

M ≡ E[Δ] ⟶_{h} E[L] ≡ M′ ⟶_{h} → A

for some evaluation context E, head redex Δ, terms L, M′. We show that λ_{σ} ⊢ M = M′ by a case analysis on the form of Δ. If Δ is a β, δ, ▷▷, r▷ or v▷ redex the result follows immediately since these are also reductions in λ_{σ}. The remaining cases are:

Case Δ ≡ N =: v ; v? ▷ x.P

By Lemma 4.10 and Lemma 4.12 there is an evaluation context E and a state prefix S such that

M ≡ E[pure (S[N =: v ; v? ▷ x.P])].

By Lemma 4.14 M ⟶_{σ} → M_{σ}, where

M_{σ} ≡ E[σ_{S} · N =: v ; v? ▷ x.P]

and σ_{S} is as in Lemma 4.14. By Lemma 4.11, v ^{∈} bt S, hence v ^{∈} dom σ_{S}. Assume, without loss of generality, that σ_{S} ≡ σ′ ∪ {v : N′}. Then,

M_{σ} ≡ E[σ′ ∪ {v : N′} · N =: v ; v? ▷ x.P]
⟶_{σ_{=:}} E[σ′ ∪ {v : N} · v? ▷ x.P]
⟶_{σ_{?}} E[σ′ ∪ {v : N} · (x.P) N]
← − ←_{σ} E[pure (S[N =: v ; (x.P) N])]
≡ M′

Case Δ ≡ N =: v ; w? ▷ x.P , v ≠ w

As before,

M ≡ E[pure (S[N =: v ; w? ▷ x.P])] ⟶_{σ} → M_{σ}

where

M_{σ} ≡ E[σ_{S} · N =: v ; w? ▷ x.P]

By Lemma 4.11, both v and w are in bt S and hence in dom σ_{S}. Assume without loss of generality that σ_{S} ≡ σ′ ∪ {v : N′}. Then,

M_{σ} ≡ E[σ′ ∪ v : N′ · N =: v ; w? ▷ x.P]
→_{σ_{=:}} E[σ ∪ v : N · w? ▷ x.P]
→_{σ_{?}} E[σ ∪ v : N · (x.P) (σ w)]
→_{β} E[σ ∪ v : N · [(σ w)/x] P]
←_{σ_{=:}} E[σ ∪ v : N′ · N =: v ; [(σ w)/x] P],
(x ^{∉} fv N)
←_{β} E[σ ∪ v : N′ · (x. N =: v ; P) (σ w)]
←_{σ_{?}} E[σ ∪ v : N′ · w? ▷ N =: v ; x.P]
← ←_{σ} E[pure (S[w? ▷ x.N =: v ; P])]
≡ M′

Case Δ ≡ var v.w? ▷ x.P , v ≠ w

This case is proved similarly to the last case.

Case Δ ≡ pure (S[return x.M]) .

Again using Lemma 4.14:

M ≡ E[pure (S[return x.M])]
⟶_{σ} → E[σ_{S} · return x.M]
⟶_{σ_{pc}} → E[x.(σ · return M)]
← − ←_{σ} E[x.pure (S[return M])]

Case Δ ≡ pure (S[return c^{n}M_{1}...M_{n}]) .

Case Δ ≡ pure (S[return f]) .

These cases are similar to the previous case.

This concludes the proof in the direction “⇒”.

We now show “⇐”. Assume M ^{∈} Λ_{var} such that λ_{σ} ⊢ M = A. By the definition of ( ˆ= ), M ˆ= M. Also by the definitions of ˆ= , A ˆ= A′ ⇒ A ≡ A′. The proposition then follows by pasting together the diagrams provided by Lemma 4.15:

[figure: M; M; M′_{1}; M_{1}; A; A; ˆ=; ˆ=; ˆ=; σ; var; σ; var; ^{. . . . .}; . . . . .; ^{…}; …]

5 Operational equivalence

Operational equivalence is intended to reflect the notion of interchangeability of program fragments. It equates strictly more terms than does convertibility.

Definition. Let λ_{∗} be some extension of the λ-calculus. Two terms N and M are operationally equivalent in λ_{∗}, written λ_{∗} ⊧ N ≅ M, if for all contexts C in Λ_{∗} such that C[M] and C[N] are closed, and for all answers A,

λ_{∗} ⊢ C[M] = A ⇔ λ_{∗} ⊢ C[N] = A.

Lemma 5.1 λ_{∗} ⊢ M = N implies λ_{∗} ⊧ M ≅ N.

Proof: Assume λ_{∗} ⊢ M = N, and suppose λ_{∗} ⊢ C[M] = A. Since convertibility is closed under termformation, λ_{∗} ⊢ M = N implies λ_{∗} ⊢ C[M] = C[N], for any context C. The symmetry and transitivity of convertibility then imply that λ_{∗} ⊢ C[N] = A. The symmetric argument proves the converse implication, thus establishing λ_{∗} ⊢ C[M] = A ⇔ λ_{∗} ⊢ C[N] = A, which is the definition of λ_{∗} ⊧ M ≅ N.

Lemma 5.2 For any context C, λ_{∗} ⊧ M ≅ N implies λ_{∗} ⊧ C[M] ≅ C[N].

Proof: Assume that λ_{∗} ⊧ M ≅ N, and suppose that λ_{∗} ⊢ C′[C[M]] = A, for some context C′[ ] such that C′[C[M]] and C′[C[N]] are closed. Then the assumed operational equivalence implies that λ_{∗} ⊢ C′[C[N]] = A, and similar reasoning establishes the reverse implication. Thus λ_{∗} ⊧ C[M] ≅ C[N].

Lemma 5.3 For any variable x, λ_{∗} ⊧ M ≅ N ⇔ λ_{∗} ⊧ λx.M ≅ λx.N.

Proof: The left-to-right direction is a special case of Lemma 5.2.

To prove the converse, suppose that λ_{∗} ⊧ λx.M ≅ λx.N, and suppose that λ_{∗} ⊢ C[M] = A, where C[M] is closed. If x ^{∈} fv M, then λ_{∗} ⊢ (λx.M)x = M, and x ^{∈} bv(C[ ]). Let C′[ ] ≡ C[[ ]x]. Then λ_{∗} ⊢ C′[λx.M] = C[M] = A. Since λ_{∗} ⊧ λx.M ≅ λx.N it follows that λ_{∗} ⊢ C′[λx.N] = A, and therefore also λ_{∗} ⊢ C[N] = A. Since C was arbitrary, λ_{∗} ⊧ M ≅ N. If x ^{∉} fv M, choose C′[ ] = C[[ ]c] for any constant c.

Proposition 5.4 The following are operational equivalences in λ_{var}:

(1)  v? ▷ x . w? ▷ y . M ≅ w? ▷ y . v? ▷ x . M
(2) N =: v ; N′ =: w ; M ≅ N′ =: w ; N =: v ; M
(v ≠ w)
(3) var v . N =: w ; M ≅ N =: w ; var v . M
(v ≠ w, v ^{∉} ft N)
(4)  var v . var w . M ≅ var w . var v . M
(5) N =: v ; N′ =: v ; M ≅ N′ =: v ; M
(6)  S[P] ≅ P
(bt S ∩ ft (S[P]) = ∅)
(7)  P ▷ x.return x ≅ P

We will prove these operational equivalances soon, but first we describe what they mean in terms of informal programming concepts.

Equation (1) says that variable lookups commute. Equations (2), (3) and (4) say that assignments and variable introductions commute with themselves and with each other. Equation (5) says that if a variable is written twice in a row, the second assigned value is the one that counts.

Equation (6) implements “garbage collection”: it says that a state prefix S of an expression S[P] can be dropped if no variable written in S is used in P. Note that, using the “bubble” conversion laws and the commutative laws (2), (3) and (4), garbage can always be moved to a state prefix.

Proof: The definition of operational equivalence demands that we prove statements that are quantified over all λ_{var}-contexts; the statements themselves are quantified over all answer-producing reductions. We use a proof technique developed by Odersky [20] to reduce the burden of this proof.

The technique in question requires us only to prove certain properties of the interaction between the proposed operation equivalence and the reduction rules of the calculus.

For each proof, we construct a collection of symmetric rewrite rules that define a relation, similarity, intended to characterize the operational equivalence to be proved. In our present proposition, this collection will always consist of a single rule: the operational equivalence as stated. We then show that, in all cases in which the similarity rules have a critical overlap with the reduction rules of the calculus, there exists a parallel application of (already-established) operational equivalences to the similar term that yields a term similar to the result of the reduction. This aspect of the technique resembles the definition of the bisimulations used in concurrency theory [17]. The notion of critical overlap arises in the theory of term-rewriting systems [6].

The main proof requirements for each operational equivalence are explained in the following diagram, in which the given relations appear as solid lines and the relations to be established appear as dotted lines:

[figure: R; R′; R′_{1}; R′′; R′′_{1}; h; ^{. . . . . . . . . . . . .}; h; ∼_{1}; . . . . . . . . . . . . . . . . . . . . . . . . . . . . .; ≅; . . . . . . . . . . . . .; ∼_{1}]

where ∼_{1} is the parallel similarity derived from ∼; in our proofs it will suffice to think of this relation as being the union ∼ ∪ ≡.

For each proof below, we will give concrete meta-terms and reductions to instantiate this diagram.

Applying the proof technique requires in addition that we establish some minor technical conditions. First, we must verify that the evaluation contexts of λ_{var} are downward closed, that is, that E = C_{1} · C_{2} implies that C_{2} is itself an evaluation context. This is obvious from inspection of the definition of λ_{var}’s evaluation contexts in Figure 5. Second, we must establish, for each similarity relation we introduce, that the relation preserves evaluation contexts and is answer-preserving. Preservation of evaluation contexts means that the similarity rules do not overlap with the defining productions of evaluation contexts. An answer-preserving relation satisfies M ∼ A ⇒ M → → A; this is easily seen to be true for all our proposed similarity relations, so we will omit further mention of this issue.

We now proceed to prove each of the proposed operational equivalences. For most of the individual proofs, the operational equivalence required to construct the bottom edge of the above diagram is easily established by exhibiting a conversion; we only remark on the exceptions to this observation.

(1) We adopt the similarity relation implied by S = {v? ▷ x.w? ▷ y.M ∼ w? ▷ y.v? ▷ x.M}.

The rules in S do not overlap with any of the productions defining evaluation contexts in Figure 5. Hence, ∼ preserves evaluation contexts.

We now enumerate the various ways in which ∼ can intefere with →; for each case, we show how to instantiate the diagram so as to prove that the compatible equivalence closure of ∼ is an operational equivalence.

Case 1.1:

R ≡ N =: u ; v? ▷ x . w?y . M
(u ≢ v, u ≢ w, v ≢ w)
R′′ ≡ N =: u ; w? ▷ y . v? ▷ x . M
R′ ≡ v? ▷ x . N =: u ; w? ▷ y . M
R′_{1} ≡ v? ▷ x.w? ▷ y.N =: u ; M
R′′_{1} ≡ w? ▷ y.v? ▷ x.N =: u ; M
R ⟶_{b_{1}} R′
R′ ⟶_{b_{1}} R′_{1}
R′′ ⟶_{b_{1}} w? ▷ y.N =: u ; v? ▷ x.M
⟶_{b_{1}} R′′_{1}

Case 1.2:

R ≡ N =: w ; v? ▷ x.w? ▷ y.M
(u ≢ v, v ≢ w)
R′′ ≡ N =: w ; w? ▷ y.v? ▷ x.M
R′ ≡ v?x.N =: w ; w? ▷ y.M
R′_{1} ≡ R′′_{1} ≡ v? ▷ x.N =: w ; [N/y]M
R ⟶_{b_{1}} R′
R′ ⟶_{f} v? ▷ x.N =: w ; (y.M)N
⟶_{β} R′_{1}

R′′ ⟶_{f} N =: w ; (y.v? ▷ x.M)N
⟶_{β} N =: w ; v? ▷ x.[N/y]M
⟶_{b_{1}} R′′_{1}

Case 1.3:

R ≡ N =: v ; v? ▷ x.w? ▷ y.M
(v ≢ w)
R′′ ≡ N =: v ; w? ▷ y.v? ▷ x.M
R′ ≡ N =: v ; (x.w? ▷ y.M)N
R′_{1} ≡ R′′_{1} ≡ w? ▷ y.N =: v ; [N/x]M
R ⟶_{f} R′
R′′ ⟶_{b_{1}} w? ▷ y.N =: v ; v? ▷ x.M
⟶_{f,β} R′′_{1}
R′ ⟶_{β} N =: v ; w? ▷ y.[N/x]M
⟶_{b_{1}} R′_{1}

Case 1.4:

R ≡ N =: v ; v? ▷ x.v? ▷ y.M
(u ≢ v, u ≢ w)
R′ ≡ v? ▷ x.N =: u ; v? ▷ y.M
R′′ ≡ N =: u ; v? ▷ x.v? ▷ y.M
R′_{1} ≡ R′′_{1} ≡ R′
R ⟶_{b_{1}} R′
R′′ ⟶_{b_{1}} R′′_{1}

Case 1.5:

R ≡ N =: v ; v? ▷ x.v? ▷ y.M
R′ ≡ N =: v ; (x.v? ▷ y.M)N
R′′ ≡ R
R′_{1} ≡ N =: v ; v? ▷ y.[N/x]M
R′′_{1} ≡ R′_{1}
R ⟶_{f} R′
R′ ⟶_{β} R′_{1}
R′′ ⟶_{f,β} R′′_{1}

For the remaining operational equivalences, we give only the basic data needed to complete the diagram.

(2) S = {N =: v ; N′ =: w ; M ∼ N′ =: w ; N =: v ; M}, (v ≢ w).

Case 2.1:

R ≡ N =: v ; N′ =: w ; w? ▷ x.M′
(v ≢ w)
R′ ≡ N =: v ; N′ =: w ; (x.M)N′
R′_{1} ≡ R′
R′′ ≡ N′ =: w ; N =: v ; w? ▷ x.M′
R′′_{1} ≡ N′ =: w ; N =: v ; (x.M)N′
R ⟶_{f} R′
R′′ ⟶_{b_{1}} N′ =: w ; w? ▷ x.n =: v ; M′
note that x ^{∉} fv N
⟶_{f} N′ =: w ; (x.N =: v ; M′)N′
⟶_{β} N′ =: w ; N =: v ; [N′/x]M′
− ←_{β} R′′_{1}

Case 2.2:

R ≡ N =: v ; N′ =: w ; v? ▷ x.M
(v ≢ w)
R′ ≡ N =: v ; v? ▷ x.N′ =: w ; M′
(x ^{∉} fv N′)
R′′ ≡ N′ =: w ; N =: v ; v? ▷ x.M′
R′_{1} ≡ N =: v ; N′ =: w ; [N/x]M′
R′′_{1} ≡ N′ =: w ; N =: v ; [N/x]M′
R ⟶_{b_{1}} R′
R′ ⟶_{f} N =: v ; (x.N′ =: w ; M′)N
⟶_{β} R′_{1}
R′′ ⟶_{f} N′ =: w ; N =: v ; (x.M′)N
⟶_{β} R′′_{1}

Case 2.3:

R ≡ N =: v ; N′ =: w ; u? ▷ x.M′
(u ≢ w, u ≢ v)
R′ ≡ N =: v ; u? ▷ x.N′ =: w ; M′
R′′ ≡ N′ =: w ; N =: v ; u? ▷ x.M′
R′_{1} ≡ u? ▷ x.N =: v ; N′ =: w ; M′
R′′_{1} ≡ u? ▷ x.N′ =: w ; N =: v ; M′
R ⟶_{b_{1}} R′
R′ ⟶_{b_{1}} R′_{1}
R′′ ⟶_{b_{1}} R′′_{1}

(3) S = {var v.N =: w ; M ∼ N =: w ; var v.N | v ≢ w, v ^{∉} ft N}

Case 3.1:

R ≡ N =: w ; var v.u? ▷ x.M

(u ≢ w, u ≢ v)

R′ ≡ N =: w ; u? ▷ x.var v.M
R′′ ≡ var v.N =: w ; u? ▷ x.M
R′_{1} ≡ u? ▷ x.N =: w ; var v.M
R′′_{1} ≡ u? ▷ x.var v.N =: w ; M
R ⟶_{b_{2}} R′
R′ ⟶_{b_{1}} R′_{1}
R′′ − ←_{b_{1}} var v.u? ▷ x.N =: w ; M
⟶_{b_{2}} R′′_{1}

Case 3.2:

R ≡ N =: w ; var v.w? ▷ x.M

(u ≢ v)

R′ ≡ N =: w ; w? ▷ x.var v.M
R′′ ≡ var v.N =: w w? ▷ x.M
R′_{1} ≡ N =: w ; var v.[N/x]M
R′′_{1} ≡ var v.N =: w ; [N/x]M
R ⟶_{b_{2}} R′
R′ ⟶_{f} N =: w ; (x.var v.M)N
⟶_{β} R′_{1}
R′′ ⟶_{f} var v.N =: w ; (x.M)N
⟶_{β} R′′_{1}

Case 3.3:

R ≡ var v.N =: w ; u? ▷ x.P

(u ≢ w, u ≢ v)

R′ ≡ var v.u? ▷ x.N =: w ; P
R′′ ≡ N =: w ; var v.u? ▷ x.P
R′_{1} ≡ u? ▷ x.var v.N =: w ; P
R′′_{1} ≡ u? ▷ x.N =: w ; var v.P
R ⟶_{b_{1}} R′
R′ ⟶_{b_{2}} R′_{1}
R′′ ⟶_{b_{2}} N =: w ; u? ▷ x.var v.P
⟶_{b_{1}} R′′_{1}

Case 3.4:

R ≡ var v.N =: w ; w? ▷ x.P
R′ ≡ var v.N =: w ; (x.P)N
R′′ ≡ N =: w ; var v.w? ▷ x.P
R′_{1} ≡ var v.N =: w ; [N/x]P
R′′_{1} ≡ N =: w ; var v.[N/x]P
R ⟶_{f} R′
R′ ⟶_{β} R′_{1}
R′′ ⟶_{b_{2}} N =: w ; w? ▷ x.var v.P
⟶_{f} N =: w ; (x.var v.P)N
⟶_{β} R′′_{1}

Case 3.5:

R ≡ (var v.N =: w ; P) ▷ x.Q
R′ ≡ var v.N =: w ; P ▷ x.Q
R′′ ≡ (N =: w ; var v.P) ▷ x.Q
R′_{1} ≡ R′
R′′_{1} ≡ N =: w ; var v.P ▷ x.Q
R ⟶_{v▷} R′
R′′ ⟶_{▷▷} R′′_{1}

(4) S = {var v.var w.M ∼ var w.var v.M}

Some of the critical pairs we encounter in the course of proving this operational equivalence require more refined reasoning than we have yet encountered.

Case 4.1:

R ≡ (var v.var w.M) ▷ x.N
R′ ≡ var v.(var w.M) ▷ x.N
R′′ ≡ (var w.var v.M) ▷ x.N
R′_{1} ≡ var v.var w.(M ▷ x.N)
R′′_{1} ≡ var w.var v.(M ▷ x.N)
R ⟶_{v▷} R′
R′ ⟶_{v▷} R′_{1}
R′′ ⟶_{v▷} var w.(var v.M) ▷ x.N
⟶_{v▷} R′′_{1}

Case 4.2:

R ≡ var v.var w.u? ▷ x.M
(u ≢ v, u ≢ w)

R′ ≡ var v.u? ▷ x.var w.M
R′′ ≡ var w.var v.u? ▷ x.M
R′_{1} ≡ u? ▷ x.var v.var w.N
R′′_{1} ≡ u? ▷ x.var w.var v.N
R ⟶_{b_{2}} R′
R′ ⟶_{b_{2}} R′_{1}
R′′ ⟶_{b_{2}} var w.u? ▷ x.var v.M
⟶_{b_{2}} R′′_{1}

Case 4.3:

R ≡ var v.var w.v? ▷ x.M

(v ≢ w)

R′ ≡ var v.v? ▷ x.var w.M
R′′ ≡ var w.var v.v? ▷ x.M
R′_{1} ≡ R′
R′′_{1} ≡ R′_{1}
R ⟶_{b_{2}} R′
R′ ⟶_{b_{2}} R′_{1}
R′′  ≅ R′

by the following argument:

Informally, both R′′ and R′ are stuck terms: the only way a program containing either one as a subterm can reduce to an answer is to throw the term away, since no rule (including the δ-rule), can examine the substructure of terms constructed with var (or any other term except a value or a fully-applied constructor). Thus one would expect that putting both terms in the same context would yield a computation that either gets stuck or yields the same result regardless of the terms in question.

Formally, we apply the critical-pair method once again. We define an auxiliary similarity relation S′ = {var v.v? ▷ x.P ∼ var w.var v.v? ▷ x.P′ | v ≢ w}. This relation interferes with no reduction rules whatsoever.

(5) S = {N =: v ; N′ =: v ; M ∼ N′ =: v ; M}

Case 5.1:

R ≡ N′ =: v ; v? ▷ x.M
R′ ≡ N′ =: v ; (x.M)N′
R′′ ≡ N =: v ; N′ =: v ; v? ▷ x.M
R′_{1} ≡ R′
R′′_{1} ≡ N =: v ; N′ =: v ; (x.M)N′

R ⟶_{f} R′
R′′ ⟶_{f} R′′_{1}

Case 5.2:

R ≡ N′ =: v ; w? ▷ x.M
R′ ≡ w? ▷ x.N′ =: v ; M
R′′ ≡ N =: v ; N′ =: v ; w? ▷ x.M
R′_{1} ≡ R′
R′′_{1} ≡ w? ▷ x.N =: v ; N′ =: v ; M
R ⟶_{b_{1}} R′
R′′ ⟶_{b_{1}} N =: v ; w? ▷ x.N′ =: v ; M
⟶_{b_{1}} R′′_{1}

Case 5.3:

R ≡ N =: v ; N′ =: v ; v? ▷ x.M
R′ ≡ N =: v ; N′ =: v ; (x.M)N′
R′′ ≡ N′ =: v ; v? ▷ x.M
R′_{1} ≡ R′
R′′_{1} ≡ N =: v ; N′ =: v ; (x.M)N′
R ⟶_{f} R′
R′′ ⟶_{f} R′′_{1}

Case 5.4:

R ≡ N =: v ; N′ =: v ; u? ▷ x.M
(u ≢ v)
R′ ≡ N =: v ; u? ▷ x.N′ =: v ; M
R′′ ≡ N′ =: v ; u? ▷ x.M
R′_{1} ≡ u? ▷ x.N =: v ; N′ =: w ; M
R′′_{1} ≡ u? ▷ x.N′ =: v ; M
R ⟶_{b_{1}} R′
R′ ⟶_{b_{1}} R′_{1}
R′′ ⟶_{b_{1}} R′′_{1}

(6) S = {S[P] ∼ P | S a state context, bt S∩ft S′ = ∅} This similarity relation can interfere both with the purification rules and with the assignment rules. All the critical pairs having to do with the purification laws yield essentially the same diagram verification task, so we give only a single example:

R ≡ pure(S[return x.M])
R′ ≡ x.pure(S[return M])
R′′ ≡ pure(return x.M)
R′_{1} ≡ R′
R′′_{1} ≡ x.pure(return M)
R ⟶_{p_{λ}} R′
R′′ ⟶_{p_{λ}} R′′_{1}

The uses of ∼ in the converse direction are equally simple to verify.

The verification of the proof conditions in the cases of interference with assignment rules requires that we invoke our knowledge concerning the structure of S′. By the definition of a state prefix (Section 2), all assigments in S′ must be to tags defined in S′. Also, we have assumed that S′ is nonempty, so the immediate context of the metavariable M in the definition of S is either of the form var v.[ ] or the form N =: v ; [ ].

We work out one of the three simple cases of interference with an assignment rule:

R ≡ S[N =: v ; w? ▷ x.M]
R′ ≡ S[w? ▷ x.N =: v ; M]
R′′ ≡ N =: v ; w? ▷ x.M
R′_{1} ≡ R′
R′′_{1} ≡ w? ▷ x.N =: v ; M
R ⟶_{b_{1}} R′
R′′ ⟶_{b_{1}} R′′_{1}

(7) For this equivalence, we adopt the similarity relation defined by S = {P ▷ x.return x ∼ P }, where the metavariable P ranges over procedures only. This similarity relation only interferes with the rule (▷▷).

R ≡ (P ▷ x.return x) ▷ y.Q
R′ ≡ P ▷ x.(return x ▷ y.Q)
R′′ ≡ P ▷ y.Q
R′_{1} ≡ P ▷ x.(y.Q)x
R′′_{1} ≡ R′_{1}
R ⟶_{▷▷} R′

R′ ⟶_{r▷} R′_{1}
R′′  ≅ R′′_{1}

To establish the auxiliary operational equivalence R′′ ≅ R′′_{1}, we define a similarity relation by S′ = {y.M ∼ x.(y.M)x | x ^{∉} fvM}. This similarity only interferes with the β-rule:

R ≡ (x.(y.M)x)N
R′ ≡ (y.M)N
R′′ ≡ (y.M)N
R′_{1} ≡ R′
R′′_{1} ≡ R′′
R ⟶_{β} R′

6 Relationship between λ_{var} and classical λcalculus

Clearly, convertibility in λ implies convertibility in λ_{var}, since (β) and (δ) are reduction rules in λ_{var}. However, this goes only part of the way. For instance, the equation tail ∘ cons x ≅ id between list processing functions is not an equality in the sense of βδ-convertibility, but it is an operational equivalence. Other operational equivalences are those that identify some diverging terms or terms that involve fixed points. Since equivalences like these are routinely used when reasoning about programs, we would like them to be preserved in λ_{var}. We establish now the result that λ_{var} indeed preserves the operational equivalences of λ, and, furthermore, that λ_{var} does not introduce any new operational equivalences between Λ-terms^{5}. The only provision on this result is that the underlying set of constructors and basic function symbols needs to be “sufficiently rich”.

Definition. An (extension of) applied λ calculus λ_{∗} has a sufficiently rich set of constants if

(a) The constructor alphabet includes for every arity n an infinite number of constructors that do not form part of any of the terms N_{f,c^{n}}, N_{f} used to define the δ function. (That is, we can always find “fresh” constructors that are not used in the reduction of some given program).

5The latter property can be regarded as the preservation of distinctions or inequivalences between terms.

(b) For every constructor c^{n} one can define in λ_{∗} a projection function proj c^{n} such that

proj c^{n} (c^{n} M_{1} ... M_{n}) P Q = P M_{1} ... M_{n}
proj c^{n} V P Q  = Q V

for any other value V.

(That is, one can test for a constructor, and can take apart constructed terms).

(c) One can define in λ_{∗} a function projector proj f such that

proj f(c^{n} M_{1} ... M_{n}) P Q = Q (c^{n} M_{1} ... M_{n})

for any data value c^{n} M_{1} ... M_{n}

proj f V P Q  = P V

for any non-data value V (i.e. for any function).

(That is, one can test for a function).

Clearly, these projection functions can be defined by suitable δ-rules. The functions proj c^{n} represent a stripped down version of pattern matching on data types, as it is found in many functional programming languages. Function proj f can be thought to be a dynamic type test, similar to procedure? in Scheme [4].

In the following, we will assume that λ_{var} has a sufficiently rich set of constants that is shared by all other calculi in consideration (i.e. λ_{σ}, λν, and λ)

The rest of this section is devoted to the proof that λ_{var} is an operational extension of λ. This proof is based on finding an implementation of λ_{var} in λ. We will show below (in Theorem 6.15) that existence of an implementation implies operational extension, provided the implementation is sound and complete and maps closed λ terms to themselves. We call such an implementation a syntactic embedding.

Definition 6.1 (Extended Term) Given an inductively defined term language Λ_{∗}, an extended term is formed from the inductive definition of Λ_{∗} and [ ]. (Hence, both terms and contexts are extended terms).

Definition 6.2 A term M is λ-closed iff F V (M) = ∅.

Definition 6.3 (Syntactic Embedding) Let λ_{∗} and λ_{0} be extensions of λ with the same set of answers and suppose that Λ_{∗} ⊇ Λ_{0}. Let E be a syntactic mapping from extended λ_{∗}-terms to extended λ_{0}-terms. Then E is a syntactic embedding of λ_{∗} in λ_{0} if it satisfies the following two requirements.

1. E preserves λ-closed λ_{0}-subterms up to convertibility. For all λ_{∗}-contexts C, λ-closed λ_{0}-terms M,

λ_{0} ⊢ E[[C[M]]] = E[[C]] [M].

2. E preserves semantics. For all closed λ_{∗}-terms M, answers A,

λ_{∗} ⊢ M = A ⇔ λ_{0} ⊢ E[[M]] = A.

Syntactic embeddings generalize the syntactic (macro) expansions of [7]. They are useful for two reasons. First, a syntactic embedding E of λ_{∗} in λ_{0} allows us to extend models of λ_{0} to all of λ_{∗}, simply by composing the denotation function of λ_{0} with E. Second, and somewhat related to the first point, the existence of a syntactic embedding between two theories guarantees that all operational equivalences of the base theory are preserved in the extension. Indeed, we have:

Theorem 6.4 Let λ_{∗} and λ_{0} be two extensions of λ with the same set of answers and suppose that Λ_{∗} ⊇ Λ_{0}. If there is a syntactic embedding of λ_{∗} in λ_{0} then for any two terms M, N ^{∈} Λ_{0},

λ_{0} ⊧ M ≅ N ⇒ λ_{∗} ⊧ M ≅ N.

Proof: Assume that λ_{0} ⊧ M ≅ N Then, for all answers A and λ_{0}-contexts C_{0} such that C_{0}[M] and C_{0}[N] are closed,

λ_{0} ⊢ C_{0}[M] = A ⇔ λ_{0} ⊢ C_{0}[N] = A.

Assume first that both M and N are λ-closed. Let E be a syntactic embedding of λ_{∗} in λ_{0}. Let C be an arbitrary λ_{∗}-context such that C[M] and C[N] are closed, and let A be an answer such that C[M] = A. Then,

λ_{∗} ⊢ C[M] = A
⇔ (E preserves semantics)
λ_{0} ⊢ E[[C[M]]] = A
⇔ (E preserves λ-closed λ_{0} terms)
λ_{0} ⊢ E[[C]] [M] = A
⇔ (premise: λ_{0} ⊧ M ≅ N)
λ_{0} ⊢ E[[C]][N] = A
⇔ (reverse the argument)
λ_{∗} ⊢ C[N] = A.

Since A and C were arbitrary, λ_{∗} ⊧ M ≅ N. Now let M and N be arbitrary λ_{0} terms, with fv M ∪ fv N = {x_{1}, ..., x_{n}}. Then,

λ_{0} ⊢ M ≅ N
⇒ (Lemma 5.2)
λ_{0} ⊢ λx_{1}…. λx_{n}.M ≅ λx_{1}…. λx_{n}.N
⇒ (first part of proof)
λ_{∗} ⊢ λx_{1}…. λx_{n}.M ≅ λx_{1}…. λx_{n}.N
⇒ (Lemma 5.3)
λ_{∗} ⊢ M ≅ N.

Before we state and prove the operational extension theorem, let us quickly examine why finding a syntactic embedding of λ_{var} in λ is non-trivial. A natural implementation of λ_{var} in λ maps readers and assignments to read and write operations on a store. This suggests that we should work with a calculus with explicit stores. Because all operational equivalences of λ_{var} are preserved in λ_{σ} (Theorem 4.16), we can use just as well λ_{σ} instead of λ_{var} as the source language of the embedding. A store in λ_{σ} can be represented as a mapping from locations to terms. Variables in λ_{σ} are then mapped to locations. But what is a location? Conventionally, it is an element of some index type such as an integer. This is sufficient if there is only one global store, but the scheme breaks down for λ_{var}. The problem is that a λ_{var} term can contain multiple pure blocks. This makes it necessary to distinguish in the implementation between locations that are defined in a given pure block and locations defined in other blocks. The distinction is needed since only local variables may be read or written, and only global locations may be returned from a pure block.

Of course, local and global variables can be distinguished if they are represented by different locations (or, equivalently, if locations are tagged with a unique identifier associated with the block in which they are allocated). The problem then is how to ensure that all variable instances in a program (as opposed to those a single pure block) are mapped to unique locations. The obvious idea of passing a name supply to a pure block is not open to us, since then functions would need additional implicit arguments for the name-supply. This would violate the property that a syntactic embedding maps λ-closed terms in the base language to themselves.

Perhaps surprisingly, there is a way to ensure uniqueness of locations without passing a name supply to pureblocks. This is shown in [21], where a calculus λν is studied. λν is an extension of the λ-calculus with a binding construct for names. The term language of λν extends Λ by three new constructs:

M ::= ... | n | νn.M | M_{1} == M_{2}

Names form a new countable alphabet. A name n is bound in a construct νn.M. Like identifiers in λ (and variables in λ_{var}), names can be α-renamed. The only operation applicable to names is the equality test n_{1} == n_{2}. (==) is syntactic equality, its behavior is given by the reduction rules

\begin{aligned}n == n & → & true \\ n == m & → & false & if n ≠ m \end{aligned}

The other reductions that are particular to λν involve ν-terms:

νn.λx.M  → λx.νn.M
νn.c^{n} M_{1} ... M_{n} → c^{n} (νn.M_{1}) ... (νn.M_{n})
νn.m  → m  if n ≠ m

Standard reduction in λν is defined as in λ, with the added production

E ::= ... | νn.E

in the grammar for evaluation contexts.

For a more comprehensive discussion of λν, see [21]^{6}. Also in [21] it is shown that λν is an operational extension of λ. The proof of this theorem relies on a a syntactic embedding that maps names to level numbers. Similarly to a DeBruijn number, a level number indicates the number of intervening ν abstractions between the occurrence of a name and its definition.

Proposition 6.5 There exists a syntactic embedding E_{ν} of λν in λ.

Proof: See [21].

Since λ_{σ} preserves all operational equivalences of λ, it suffices for the proof of operational extension to give a syntactic embedding of λ_{σ} in λ. For technical reasons, we use a variant of λ_{σ}, in which states are represented as sequences of bindings v:M, rather than as sets of such bindings. The reduction rules in Figure 6 carry over, except that the first three rules are now defined on lists (with ⊣⊢ as the append operator) rather than sets:

σ · var v.M →

σ ⊣⊢[v:undef] · M

σ ⊣⊢[v:N′]⊣⊢σ′ · N =: v ; M →

σ ⊣⊢[v:N]⊣⊢σ′ · M

σ ⊣⊢[v:N]⊣⊢σ′ · v? ▷ x.M →

σ ⊣⊢[v:N]⊣⊢σ′ · (x.M) N  (N ≢ undef).

Clearly, Theorem 4.16 holds for the new just as for the original λ_{σ} calculus.

The embedding of this variant of λ_{σ} in λ, E_{σ} is given by

E_{σ}[[M]] = E_{ν}[[ F[[M]]⊥ ]]

where the mapping F is defined in Figure 7. F[[M]] takes as argument an environment ρ that maps identifiers and variables in λ_{σ} to identifiers and names in

6The calculus defined in [21] is a slight variation of the calculus described here, with unary constructors and pairs instead of the nary constructors described here. The difference does not influence the operational extension results.

F[[f]]ρ  = f
F[[c^{n}]]ρ  = c^{n}
F[[x]]ρ  = ρx
F[[v]]ρ  = ρv
F[[x.M]]ρ = λy.F[[M]]ρ[x ↦ y] (y ^{∉} range ρ)
F[[MN]]ρ  = (F[[M]]ρ) (F[[N]]ρ)
F[[var v.M]]ρ = νt.newref t (F[[M]]ρ[v ↦ t]) (t ^{∉} range ρ)
F[[M?]]ρ  = deref (F[[M]]ρ)
F[[M =: N]]ρ  = assign (F[[M]]ρ) (F[[N]]ρ)
F[[return M]]ρ  = return (F[[M]]ρ)
F[[M ▷ x.N]]ρ  = bind (F[[M]]ρ) (F[[x.N]]ρ)
F[[pure M]]ρ  = pure [[M]]ρ
F[[σ · M]]ρ  = νt_{1}. ... νt_{n}.block (F[[M]]ρ′) (F[[σ]]ρ′)
where \begin{matrix}\{v_{1}, ..., v_{n}\} = dom σ \\ ρ′ = ρ[v_{1} ↦ t_{1}] ... [v_{n} ↦ t_{n}] \\ t_{1}, ..., t_{n} ^{∉} range ρ \end{matrix}
F[[[v_{1} : M_{1}, ..., v_{n} : M_{n}]]]ρ = upd (Def F[[M_{n}]]ρ) (F[[v_{n}]]ρ) (...(upd (Def F[[M_{1}]]ρ) (F[[v_{1}]]ρ) ⊥)...)
block p s  = unwrap (p (λx.λs.(x, s)) s)
unwrap (a, s)  = case a of

Res (c^{n} M_{1} ... M_{n}) → c^{n} (unwrap (Res M_{1}, s)) ... (unwrap (Res M_{n}, s))

Res f → λx.unwrap (f x, s)  (f a function)
pure p  = block p ⊥
return a  k s = k (Res a) s
bind p q  k s = p (λx.q (strip x) k) s
where \begin{aligned}strip (Res x) & = & x \\ strip Unit & = & () \end{aligned}
newref t p k s = p k (upd Undef t s)
deref t  k s = case s t of Def a → k (Res a) s
assign a t k s = case s t of Undef, Def y → k Unit (upd (Def a) t s)
upd a t s  = λu.if t == u then a else s u

Figure 7: Environment mapping F λν. ⊥ denotes the totally undefined environment, and ρ[x ↦ y] denotes the environment ρ extended by the binding that sends x to y. To save parentheses, we adopt the convention that environment extension binds more strongly than function application, i.e. F[[M]]ρ[x ↦ y] parses as F[[M]](ρ[x ↦ y]).

Some other remarks on Figure 7:

• F maps an applicative term in λ_{σ} to itself (modulo α renaming). Procedures are mapped to functions that access and modify an explicit state.

• A state is a mapping from λν names to either Def M where M is a term, or Undef. Undef is returned if a variable is uninitialized. A store {v_{1} : M_{1}, ..., v_{n} : M_{n}} in λ_{σ} is translated to the state that maps each (image of) v_{i} to Undef, if M_{i} ≡ undef, and to Def (F[[M_{i}]]ρ) otherwise. The translated state is undefined on all other names. Such a function can be constructed from ⊥ (the totally undefined state) and upd. Note that the definition of upd relies on the equality test (==) on names. Note also that an uninitialized variable is different from a variable containing ⊥ (where ⊥ is any λ-term without weak head normal form). A procedure that reads from an uninitialized variable always gets stuck and hence never reduces to an answer. If it reads a variable whose value is ⊥ the procedure might still reduce to an answer, namely if the value of the variable is not demanded in the subsequent computation.

• A variable v in λ_{σ} is mapped to a λν name n.

• A procedure in λ_{σ} is mapped to a statetransformer. A state-transformer is a function from continuations and states to results. A continuation is a function from intermediate results and states to final results. Both intermediate and final results are wrapped in a constructor Res (or the result is Unit if it comes from an assignment; see below). It is assumed that Res and Unit are reserved, i.e. that they are not available for the reduction of pure λν terms. This can always be achieved since λ_{var} has by assumption a sufficiently rich set of constants that is shared by the other calculi in consideration.

Wrapping results in reserved constructors serves to keep state transformers apart from other λν functions. Without it, a term such as pure f, where f is a λν function that behaves like a statetransformer, would be translated to pure f, which might well reduce to a result. On the other hand, the original term pure f will always get stuck, since f is not a procedure. Hence, E_{σ} would fail to preserve semantics. Note that in a typed setting equivalent abstraction barriers could be provided by abstract data types.

• The definition of F makes use of the auxiliary functions given in the second half of Figure 7. To help readability, we give these functions in a sugared notation similar to Haskell [14] instead of in pure λν.

• Function block invokes its state-transformer argument p with its state argument s and the continuation λx.λs.(x, s). This continuation simply returns the intermediate result and the state passed to it. The result portion of this pair is then unwrapped using function unwrap. This is similar to the actions of productions σ_{p_{c}}, σ_{p_{λ}} and σ_{p_{f}}.

• The term νn_{1}. ... .νn_{m}.unwrap p k s corresponds to a λ_{σ} configuration with state s and procedure p ▷ k. The domain of s is {n_{1}, ..., n_{m}}.

• The state-transformer return x invokes its continuation in the current state with Res x as intermediate result.

• The state-transformer bind p q invokes the statetransformer p with q as a prefix of the continuation.

• A variable abstraction var v.M is mapped to the λν-term νn.newref n (F[[M]]ρ[v ↦ n]). Function newref n p invokes its state-transformer argument p in a state in which its name argument n is bound to Undef.

• The state-transformer deref n forces a read of n in the current state. This corresponds to the strict behavior of readers in λ_{var} where the read is performed even if its result is not demanded by the subsequent computation.

• The state-transformer assign x n also forces a read of n, but then performs the same action regardless of the value associated with n. This ensures that the name n has in fact been entered (via newref) in the current state and thus guards against nonlocal assignments. assign updates the state by the binding that sends n to Def x and invokes its continuation argument with Unit as intermediate result. If the assignment appears as first argument of a bind combinator, its Unit result will be translated (by function strip) to (). Otherwise, if the assignment occurs as last action in a state-transformer, reduction gets stuck, as it would in the λ_{σ} program.

We now proceed to prove that E_{σ} is a syntactic embedding.

Definition 6.6 Env(M), the set of admissible environments for a λ_{σ} term M, is the set of all injective mappings from identifiers to identifiers and variables to names that bind all free identifiers and variables in M.

Lemma 6.7 For all terms M, N, environments ρ ^{∈} Env((x.M) N),

F[[[N/x] M]]ρ ≡ [F[[N]]ρ/y] (F[[M]]ρ[x ↦ y]).

Proof: A routine induction on the structure of M.

Lemma 6.8 F is stable under reduction: For all terms M, N ^{∈} Λ_{σ}, environments ρ ^{∈} Env(M),

λ_{σ} ⊢ M → N ⇒ λν ⊧ F[[M]]ρ ≅ F[[N]]ρ.

Proof: We use a case analysis on the form of reduction in M → N. We only show three example cases; the other cases are similar. To simplify notation, we will place a tilde ˜ on identifiers in the target language and write M̃ for

F[[M]]ρ[x ↦ x̃]_{x^{∈}fv M\dom ρ}.

For instance, λx̃.M̃ is short for λx̃.F[[M]]ρ[x ↦ x̃]. Also, we will use infix notation liberally, with ‘f‘ in backquotes denoting the infix version of f.

Case ▷ ▷ In this case, the λ_{σ} reduction is

(M ▷ x.N) ▷ y.P → M ▷ x.(M ▷ y.P)

and we have in λν:

F[[(M ▷ x.N) ▷ y.P]]ρ
≡ (by definition of F)
(M̃ ‘bind‘ λx̃.Ñ) ‘bind‘ λỹ.P̃
= (by definition of bind, β)
λk.(M̃ ‘bind‘ λx̃.Ñ) (λỹ.P̃ (strip ỹ) k)
= (by definition of bind, β)

λk.(λk′.M̃ (λx̃.Ñ (strip x̃) k′)) (λỹ.P̃ (strip ỹ) k)

= (by β-reduction)
λk.M̃ (λx̃.Ñ (strip x̃) (λỹ.P̃ (strip ỹ) k))
= (by definition of bind, β)
M̃ ‘bind‘ (λx̃.Ñ ‘bind‘ λỹ.P̃)
≡ (by definition of F)
F[[M ▷ x.(N ▷ y.P)]]ρ

Case σ_{=:} In this case, the λ_{σ} reduction is

σ ⊣⊢[v:N′]⊣⊢σ′ · N =: v ; M → σ ⊣⊢[v:N]⊣⊢σ′ · M Let L = [n_{1}, ..., n_{m}] = [ρv | v ← dom σ], We abbreviate νn_{1}. ... νn_{m}.M by νL.M. Let k = λx.λs.(x, s). Let N^{∗} be Undef if N ≡ undef, and Def N otherwise. Then we have in λν:

F[[σ ⊣⊢[v:N′]⊣⊢σ′ · N =: v ; M]]ρ
≡ (by definition of F)
νL.block ((assign Ñ ṽ ‘bind‘ λ().M̃)
(F[[σ ⊣⊢[v:N′]⊣⊢σ′]]ρ))
≅ (by definition of block, upd)
νL.unwrap ((assign Ñ ṽ ‘bind‘ λ().M̃) k
(upd N^{∗} ṽ (F[[σ ⊣⊢σ′]]ρ)))
= (by definition of bind)
νL.unwrap (assign Ñ ṽ (λx.(λ().M̃) (strip x) k)
(upd N^{∗} ṽ (F[[σ ⊣⊢σ′]]ρ)))
= (by definition of assign)
νL.unwrap ((λx.(λ().M̃) (strip x) k) Unit
(upd (Def Ñ) ṽ (upd N^{∗} ṽ (F[[σ ⊣⊢σ′]]ρ))))
≅ (by β reduction (twice), definition of strip)
νL.unwrap (M̃ k
(upd (Def Ñ) ṽ (upd N^{∗} ṽ (F[[σ ⊣⊢σ′]]ρ))))
≅ (by β reduction, definition of upd)
νL.unwrap (M̃ k
(upd (Def Ñ) ṽ F[[σ ⊣⊢σ′]]ρ))
≅ (by definition of block, upd)
νL.block (M̃ k
(F[[σ ⊣⊢[v:N]⊣⊢σ′]]ρ))
≡ (by definition of F)
F[[σ ⊣⊢[v:N]⊣⊢σ′ · M]]ρ

Case σ_{p_{λ}} In this case the λ_{σ} reduction is

σ · return x.M → x.(σ · return M)

Define k, L and νL.M as above. Then we have in λν:

F[[σ · return x.M]]ρ

= (by definition of F, block)

νL.unwrap (return (λx̃.M̃) k σ̃)

= (by definition of return)

νL.unwrap (k (Res (λx̃.M̃)) σ̃)

= (by definition of k, β-reduction)

νL.unwrap (Res (λx̃.M̃), σ̃)

= (by definition of unwrap and β)

νL.λx̃.unwrap (Res M̃, σ̃)

= (by reduction in λν)

λx̃.νL.unwrap (Res M̃, σ̃)

= (by definition of unwrap, k, return, and β)

λx̃.νL.unwrap (return M̃ k σ̃)

= (by definition of F, block)

F[[x.(σ · return M)]]ρ

Lemma 6.8 shows that equal λ_{σ} terms get mapped to equal (wrt ≅) λν terms. We also have to show the converse, that different λ_{σ} terms get mapped to different λν terms. To this purpose, we define in Figure 8 a left inverse F^{−1} of F and show that F^{−1} is stable under standard reduction in λν.

To define F^{−1}, we will assume that all auxiliary functions in Figure 7 are primitive functions (in all their arguments). This is admissible since all these functions are strict. Hence, we invalidate no operational equivalences, nor do we create new ones. We assume that these primitive functions define the following δ reductions:

• block p s, unwrap (a, s), bind p q k s, and newref n p k s all reduce in one step to their right hand sides given in Figure 7.

• return a (λx.q) s reduces in one step to [Res a/x]q s.

• deref n (λx.q) s reduces in one step to [Res a/x]q s if s n is of the form Def a, and gets stuck otherwise.

• assign a n (λx.q) s reduces in one step to [Res a/x]q (upd (Def a) n s) if if s n is defined, and gets stuck otherwise.

• return a k s, deref n k s, and assign a n k s get stuck if k is not a λ-abstraction.

Definition 6.9 Let ρ^{−1} be the inverse of environment ρ. ρ^{−1} is a well-defined (partial) function since ρ is injective. Define Env^{−1}(M) = {ρ^{−1} | ρ ^{∈} Env(M)}.

The proofs of the following three lemmas are all easy inductions on the structure of M:

Lemma 6.10 F^{−1}[[ ]]ρ^{−1} is a left inverse of F[[ ]]ρ: For all M ^{∈} Λ_{σ}, ρ ^{∈} Env(M),

F^{−1}[[F^{−1}[[M]]ρ]]ρ^{−1} ≡ M.

Lemma 6.11 For all terms M ^{∈} Λν, environments ρ ^{∈} Env^{−1}(M), identifiers x ^{∉} fv M, y,

F^{−1}[[M]]ρ[x ↦ y] ≡ F^{−1}[[M]]ρ

provided either side is defined.

Lemma 6.12 For all terms M, N ^{∈} Λν, environments ρ ^{∈} Env^{−1}((λx.M) N),

F^{−1}[[[N/x] M]]ρ ≡ [F^{−1}[[N]]ρ/y] (F^{−1}[[M]]ρ[x ↦ y]).

provided either side is defined.

Lemma 6.13 F^{−1} is stable under standard reduction: For all terms M, N ^{∈} Λν, answers A, environments ρ ^{∈} Env(M), if

λν ⊢ M ⟶_{s} N ⟶_{s} → A

and F^{−1}[[M]]ρ is defined, then so is F^{−1}[[N]]ρ and

λ_{σ} ⊧ F^{−1}[[M]]ρ ≅ F^{−1}[[N]]ρ.

Proof: The proof is by a case analysis on the form of the redex Δ in M → N. We only show one case; the other cases are all similar, but tend to be simpler.

Case Δ = assign a n k s

Since the reduction appears in a standard reduction sequence to an answer, Δ must occur in a superterm of the form unwrap Δ, k must be a continuation of the form λx.q (strip x) k′ and s must be state, otherwise reduction would get stuck.

In λν the reduct R of Δ is

[()/x]q k′ (upd (Def x) n s),

and we have to show that, for any ρ ^{∈} Env^{−1}(Δ),

λ_{σ} ⊧ F^{−1}[[unwrap Δ]]ρ ≅ F^{−1}[[unwrap R]]ρ.

The left hand side of this operational equivalence expands to

S^{−1}[[s]]ρ · P^{−1}[[assign a n k]]ρ.  (1)

F^{−1}[[f]]ρ  = f
F^{−1}[[c^{n}]]ρ  = c^{n}
F^{−1}[[x]]ρ  = ρx
F^{−1}[[t]]ρ  = ρt
F^{−1}[[λx.M]]ρ = y.F^{−1}[[M]]ρ[x ↦ y] (y ^{∉} range ρ)
F^{−1}[[MN]]ρ  = (F^{−1}[[M]]ρ) (F^{−1}[[N]]ρ)
F^{−1}[[νt.M]]ρ = F^{−1}[[M]]ρ[t ↦ v] (v ^{∉} range ρ)
F^{−1}[[newref t M]]ρ  = var ρt.F^{−1}[[M]]ρ
F^{−1}[[deref M]]ρ  = (F^{−1}[[M]]ρ)?
F^{−1}[[assign M N]]ρ  = F^{−1}[[M]]ρ =: F^{−1}[[N]]ρ
F^{−1}[[return M]]ρ  = return (F^{−1}[[M]]ρ)
F^{−1}[[bind M N]]ρ  = F^{−1}[[M]]ρ ▷ F^{−1}[[N]]ρ
F^{−1}[[pure M]]ρ  = pure (F^{−1}[[M]]ρ)
F^{−1}[[unwrap (Res a, s)]]ρ = S^{−1}[[s]]ρ · return (F^{−1}[[a]]ρ)
F^{−1}[[unwrap (p s)]]  = S^{−1}[[s]]ρ · P^{−1}[[p]]ρ
S^{−1}[[⊥]]ρ  = ∅
S^{−1}[[upd Undef t s]]ρ  = UP D undef (ρt) (S^{−1}[[s]]ρ)
S^{−1}[[upd (Def a) t s]]ρ  = UP D (F^{−1}[[a]]ρ) (ρt) (S^{−1}[[s]]ρ)
where \begin{aligned}UP D a v [ ] & = & [v : a] \\ UP D a v ([v : b]⊣⊢σ) & = & [v : a]⊣⊢σ \\ UP D a v ([w : b]⊣⊢σ) & = & [w : b]⊣⊢UP D a v σ \end{aligned}  (v ≠ w)
P^{−1}[[p (λx.λs.(x, s)]]ρ  = F^{−1}[[p]]ρ
P^{−1}[[p (λx.q (strip x) k)]] = F^{−1}[[p]]ρ ▷ λy.P^{−1}[[q k]]ρ[x ↦ y]  (y ^{∉} range ρ)

Figure 8: Reverse mapping F^{−1} We first turn to the state portion of this term. By the definition of F, there are terms a_{1},...,a_{m} and names n_{1},...,n_{m} such that

s ≡ upd a_{m} n_{m} ( ... (upd a_{1} n_{1} ⊥) ... ).

Then by the definition of S^{−1},

S^{−1}[[s]]ρ ≡ [ρn_{1} : F^{−1}[[a_{1}]]ρ, ... , ρn_{m} : F^{−1}[[a_{m}]]ρ].

Since assign a n k is by assumption a redex, n is in the domain of s, hence is equal to at least one of n_{1}, ..., n_{m}. Therefore, there is a term M and states σ, σ′ such that

S^{−1}[[s]]ρ ≡ σ ⊣⊢[ρn : M]⊣⊢σ′.  (2)

We now turn to the procedure part of (1). Assume first that x occurs free in the prefix q of the continuation k = λx.q (strip x) k′ (an easy induction on the form of state-transformers shows that x cannot appear free in k′). Then we have in λ_{σ}:

S^{−1}[[s]]ρ · P^{−1}[[assign a n (λx.q (strip x) k′)]]ρ

≡ (by (2) and the definition of P^{−1})

σ ⊣⊢[ρn : M]⊣⊢σ′ ·

F^{−1}[[a]]ρ =: ρn ▷ λy.P^{−1}[[q k′]]ρ[x ↦ y]

= (by =:▷ and β reduction)

σ ⊣⊢[ρn : M]⊣⊢σ′ ·

F^{−1}[[a]]ρ =: ρn ; [()/y] (P^{−1}[[q k′]]ρ[x ↦ y])

≡ (by Lemma 6.12)

σ ⊣⊢[ρn : M]⊣⊢σ′ ·

F^{−1}[[a]]ρ =: ρn ; (P^{−1}[[[()/x](q k′)]]ρ[x ↦ y])

≡ (by Lemma 6.11)

σ ⊣⊢[ρn : M]⊣⊢σ′ ·

F^{−1}[[a]]ρ =: ρn ; (P^{−1}[[[()/x] (q k′)]]ρ)

= (by σ_{=:} reduction)

σ ⊣⊢[ρn : F^{−1}[[a]]ρ]⊣⊢σ′ ·

P^{−1}[[[()/x] (q k′)]]ρ

≡ (since x is not free in k′)

σ ⊣⊢[ρn : F^{−1}[[a]]ρ]⊣⊢σ′ ·

P^{−1}[[[()/x]q k′]]ρ

≡ ...

Here, k′ is a continuation, i.e. it is of one of the forms λy.q′ (strip y) k′′, λx.λs.(x, s). If k′ is of the form λy.q′ (strip y) k′′, this can be continued as follows:

...
≡ σ ⊣⊢[ρn : F^{−1}[[a]]ρ]⊣⊢σ′ ·
P^{−1}[[[()/x]q (λy.q′ (strip y) k′′)]]ρ
≡ (by definition of P^{−1})
σ ⊣⊢[ρn : F^{−1}[[a]]ρ]⊣⊢σ′ ·

F^{−1}[[[()/x]q]]ρ ▷ λz.P^{−1}[[q′ k′′]]ρ[y ↦ z]

≅ (by definition of UP D)
UP D (F^{−1}[[a]]ρ) n (S^{−1}sρ) ·

F^{−1}[[[()/x]q]]ρ ▷ λz.P^{−1}[[q′ k′′]]ρ[y ↦ z]

≡ (by definition of F^{−1}, S^{−1}, P^{−1})
F^{−1}[[unwrap ([()/x] q)

(λy.q′ (strip y) k′′) (upd (Def a) n s))]]ρ

≡ F^{−1}sqRρ

If, on the other hand, the continuation k′ is of the form λx.λy.(x, s), (...) can be continued as follows:

...
≡ σ ⊣⊢[ρn : F^{−1}[[a]]ρ]⊣⊢σ′ ·
P^{−1}[[[()/x]q (λx.λs.(x, s))]]ρ
≡ (by definition of P^{−1})
σ ⊣⊢[ρn : F^{−1}[[a]]ρ]⊣⊢σ′ ·
F^{−1}[[[()/x]q]]ρ
≡ (by definition of F^{−1}, S^{−1})
F^{−1}[[unwrap ([()/x]q)
(λx.λs.(x, s)) (upd (Def a) n s))]]ρ
≡ F^{−1}[[R]]ρ

This proves the case where x occurs free in q. The case where x does not occur free in q is identical, except that the =:▷ reduction step is left out.

Proposition 6.14 E_{σ} is a syntactic embedding of λ_{σ} in λ.

Proof: We first show that E_{σ} preserves λ-programs. Let M be a closed λ-term. Then by an easy induction on the structure of M, F[[M]]⊥ ≡ M. Since E_{ν} is a syntactic embedding, E_{ν}[[M]] ≡ M. Hence, E_{σ}[[M]] ≡ M.

We now show that E_{σ} preserves semantics. Since E_{ν} is a syntactic embedding this follows from

λ_{σ} ⊢ M = A ⇔ λν ⊢ F[[M]]⊥ = A  (3)

for all terms M ^{∈} Λ_{σ}, answers A.

We show each direction of “⇔” in (3) separately. “⇒”: Assume M = A. Then by an induction on the length of reduction from M to A, using Lemma 6.8 at each step, F[[M]]ρ ≅ F[[A]]ρ. But the latter term equals A.

“⇐”: Assume F[[M]]⊥ = A. Then by an induction on the length of standard reduction from F[[M]]⊥ to A, F^{−1}[[F[[M]]⊥]]⊥ ≅ F^{−1}[[A]]. The right-hand side of this equivalence equals A, whereas by Lemma 6.10 the left hand side equals M.

Theorem 6.15 λ_{σ} is a conservative operational extension of λ: For any two terms M, N ^{∈} Λ,

λ ⊧ M ≅ N ⇔ λ_{σ} ⊧ M ≅ N.

Proof: By Proposition 6.14, there is a syntactic embedding of λ_{σ} in λ. By Theorem 6.4, this implies that λ_{σ} is an operational extension of λ. It remains to show that the extension is conservative.

Assume λ_{σ} ⊧ M ≅ N. Then we have

λ_{σ} ⊢ C[M] = A ⇔ λ_{σ} ⊢ C[N] = A

for all contexts C in Λ_{σ} such that C[M] and C[N] are closed and therefore also for all such contexts C in Λ. Since terms M ^{∈} Λ have only β and δ redexes, and since Λ is closed under βδ reduction, this implies λ ⊧ M ≅ N.

Corollary 6.16 λ_{var} is a conservative operational extension of λ: For any two terms M, N ^{∈} Λ,

λ ⊧ M ≅ N ⇔ λ_{var} ⊧ M ≅ N.

Proof: Immediate from Theorem 6.15 and Theorem 4.16.

7 Related Work

Hoare et. al. [12] present a normalizing set of equations for an imperative language with assignment, conditional and nondeterministic choice. Functional abstraction is not considered. Field [10] extends the deterministic part of their theory with shared variables. Boehm [2] gives an equational semantics for a first-order Algol-like language. In his setting, expressions have both values and effects, which are defined by different fragments of his calculus.

Felleisen, Friedman, and Hieb [8, 9] have developed a succession of calculi for reasoning about Scheme programs. Since their target programming language is callby-value, they have based their work on the λ_{V} -calculus of Plotkin[23] instead of the pure λ-calculus. It is inherent in their goal of reasoning about Scheme that their theories are not a conservative extension with respect to operational equivalence of either the classical λ-calculus or of λ_{V}. Mason and Talcott [15, 16] have also developed equational calculi with motivations similar to those of Felleisen et. al. and with comparable results.

Our work was influenced in part by the Imperative Lambda Calculus (ILC) of Swarup, Reddy and Ireland [27]. Like λ_{var}, ILC assumes call-by-name and models assignment by rewriting variable uses to approach and merge with their definitions. Unlike λ_{var}, ILC is defined in terms of a three-level type system of values, references and observers. This somewhat restricts expressiveness on the imperative side: references to objects that encapsulate state cannot be expressed, and all procedures have to be formulated in continuation-passing style. Also, unlike λ_{var}, ILC is strongly normalizing, and, as a consequence, not Turing-equivalent (e.g. recursion is prohibited).

Recent work by Jon Riecke [25] also addresses the problem of conservative extension of the λ-calculus by a language with effects. His techniques are unlike ours based on the denotational semantics of a typed extension of PCF with parallel or. His method depends on a full abstraction result for the denotational semantics.

A programming language with motivation similar to that of λ_{var} is Forsythe [24]. The language distinguishes between mutable and immutable variables, and also between value expressions and commands; however, it does so by means of a refined type system that is based on intersection types. (a simpler type system is found in [32]). Forsythe essentially uses a two-phase semantics, in which a term is first expanded to some potentially infinite program which is then executed in a second phase. Some common programming idioms such as procedure variables do not fit in this framework and therefore cannot be expressed.

8 Conclusions and Future Work

We have extended the applied λ-calculus with assignment. We have shown that the resulting calculus is confluent, preserves all operational equivalences of the original calculus, and permits implementation by a conventional, sequentially updated, store. We hope that λ_{var} will prove useful as a framework for extending lazy functional programming languages with imperative constructs.

An important step to that goal is the study of type systems for λ_{var}. One possible appraoch make λ_{var} to add types to λ_{var} is outlined in a companion report [3]. The treatment in the present report was untyped in order that many of our results may be applied immediately to versions of λ_{var} with arbitrary descriptive type systems. Had we started out with a typed calculus instead, all our results would hold only for the particular type system used. This would result in a loss in generality, since there are many possible candidates for such a type system. In particular, there are several widely differing approaches to implementing the effect checking required by the pure rule (examples besides [3] are [11, 19, 27, 28, 30]). Left to future research is the investigation of variants of λ_{var}. A call-by-value variant promises to be a useful tool for reasoning about programs in existing imperative or impurely functional languages. A variant with control-operators could provide an equational theory for a language with call/cc or exceptions.

Acknowledgements

This work was supported in part by DARPA grant number N00014-91-J-4043. The second author was supported by an IBM Graduate Fellowship during the final preparation of this paper. We thank Manfred Broy, Kung Chen, Matthias Felleisen, John Field, Uday Reddy, Vipin Swarup and Philip Wadler for discussions and comments on earlier versions of this paper.

References

[1] H. P. Barendregt. The Lambda Calculus: its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984.

[2] Hans-Juergen Boehm. Side effects and aliasing can have simple axiomatic descriptions. ACM Transactions on Programming Languages and Systems, 7(4):637–655, October 1985.

[3] Kung Chen and Martin Odersky. A type system for a lambda calculus with assignment. Research Report YALEU/DCS/RR-963, Yale University, Department of Computer Science, May 1993.

[4] William Clinger and Jonathan Rees. Revised^{4} report on the algorithmic language Scheme. Distributed electronically, November 1991.

[5] Erik Crank and Matthias Felleisen. Parameter-passing and the lambda-calculus. In Proc. 18th ACM Symposium on Principles of Programming Languages, Orlando, Florida, pages 233–244, January 1991.

[6] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, chapter 6, pages 243–320. MIT Press, Cambridge, Massachusetts, 1990.

[7] Matthias Felleisen. On the expressive power of programming languages. Science of Computer Programming, 17:35–75, 1991.

[8] Matthias Felleisen and Daniel P. Friedman. A calculus for assignments in higher-order languages. In Proc. 14th ACM Symposium on Principles of Programming Languages, pages 314–325, January 1987.

[9] Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235–271, 1992.

[10] John Field. A simple rewriting semantics for realistic imperative programs and its application to program analysis. In PEPM’92: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 98–107, June 1992. Yale University Research Report YALEU/DCS/RR-909.

[11] Juan Guzmán and Paul Hudak. Single-threaded polymorphic lambda calculus. In IEEE Symposium on Logic in Computer Science, pages 333–343, June 1990.

[12] C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorensen, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672–686, August 1987.

[13] Paul Hudak and Dan Rabin. Mutable abstract datatypes – or – how to have your state and munge it too. Research Report YALEU/DCS/RR-914, Yale University, Department of Computer Science, July 1992.

[14] Paul Hudak and Philip Wadler. Report on the programming language Haskell: a non-strict, purely functional language, version 1.0. Technical Report YALEU/DCS/RR-777, Yale University Department of Computer Science, April 1990.

[15] Ian Mason and Carolyn Talcott. Programming, transforming, and proving with function abstractions and memories. In Automata, Languages, and Programming: 16th International Colloquium, volume 372 of Lecture Notes in Computer Science, pages 574–588. Springer-Verlag, 1989.

[16] Ian Mason and Carolyn Talcott. Equivalence in functional languages with side effects. Journal of Functional Programming, 1(3):287–327, July 1991.

[17] Robin Milner. Communication and Concurrency. Prentice-Hall International, 1989.

[18] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[19] Martin Odersky. Observers for linear types. In B. Krieg-Brückner, editor, ESOP ’92: 4th European Symposium on Programming, Rennes, France, Proceedings, pages 390–407. Springer-Verlag, February 1992. Lecture Notes in Computer Science 582.

[20] Martin Odersky. A syntactic method for proving observational equivalences. Research Report YALEU/DCS/RR-964, Department of Compter Science, Yale University, May 1993.

[21] Martin Odersky. A syntactic theory of local names. Research Report YALEU/DCS/RR-965, Department of Computer Science, Yale University, May 1993.

[22] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 71–84. ACM Press, January 1993.

[23] Gordon D. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, 1:125– 159, 1975.

[24] John C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.

[25] Jon G. Riecke. Delimiting the scope of effects. In Proc. Conf. on Functional Programming and Computer Architecture, pages 146–155, June 1993.

[26] David A. Schmidt. Detecting global variables in denotational specifications. ACM Transactions on Programming Languages and Systems, 7(2):299–310, 1985.

[27] Vipin Swarup, Uday S. Reddy, and Evan Ireland. Assignments for applicative languages. In John Hughes, editor, Functional Programming Languages and Computer Architecture, pages 192–214. Springer-Verlag, August 1991. Lecture Notes in Computer Science 523.

[28] J.-P. Talpin and P. Jouvelot. Type, effect and region reconstruction in polymorphic functional languages. In Workshop on Static Analysis of Equational, Functional, and Logic Programs, Bordeaux, Oct. 1991.

[29] Philip Wadler. Comprehending monads. In Proc. ACM Conf. on Lisp and Functional Programming, pages 61– 78, June 1990.

[30] Philip Wadler. Is there a use for linear logic? In Proc. Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 255–273, June 1991. SIG-PLAN Notices, Volume 26, Number 9.

[31] Philip Wadler. The essence of functional programming. In Proc.19th ACM Symposium on Principles of Programming Languages, pages 1–14, January 1992.

[32] Stephen Weeks and Matthias Felleisen. On the orthogonality of assignments and procedures in Algol. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 57–70. ACM Press, January 1993.