Parameter-Passing and the Lambda Calculus

Erik Crank^{∗} Matthias Felleisen^{∗}

Department of Computer Science

Rice University Houston, TX 77251-1892

Abstract

The choice of a parameter-passing technique is an important decision in the design of a high-level programming language. To clarify some of the semantic aspects of the decision, we develop, analyze, and compare modifications of the λ-calculus for the most common parameter-passing techniques, i.e., call-by-value and call-by-name combined with pass-by-worth and passby-reference, respectively. More specifically, for each parameter-passing technique we provide

1. a program rewriting semantics for a language with side-effects and first-class procedures based on the respective parameter-passing technique;

2. an equational theory that is derived from the rewriting semantics in a uniform manner;

3. a formal analysis of the correspondence between the calculus and the semantics; and

4. a strong normalization theorem for the imperative fragment of the theory (when applicable).

A comparison of the various systems reveals that Algol’s call-by-name indeed satisfies the well-known β rule of the original λ-calculus, but at the cost of complicated axioms for the imperative part of the theory. The simplest and most appealing axiom system appears to be the one for a call-by-value/pass-by-worth language with reference cells as first-class values.

1 Parameter-Passing and Lambda Calculi

The choice of a parameter-passing technique is an important element in the design of a high-level programming language. The wide variety of techniques in modern languages, e.g., call-by-value, call-by-name, pass-by-reference, suggests a lack of consensus about the advantages and disadvantages of the various techniques. In this paper we analyze the most common techniques by studying and comparing equational theories for each of them.

Plotkin [20] was the first to consider equational theories for the analysis of parameter-passing techniques. Starting from the folklore that Church’s λ-calculus captures the essence of call-by-name in a functional language, he developed a variant of the calculus, the λ_{v}- calculus, to formalize the notion of call-by-value in a simple framework comparable to the λ-calculus. More importantly, he used these two examples, call-by-name and call-by-value, to analyze the formal relationship between programming languages and calculi. Both the λcalculus and the λ_{v}-calculus satisfy general correspondence conditions with respect to the appropriate semantics: (1) the calculi are sufficiently strong to evaluate a program to its answer and (2) they are sound in the sense that the equality of terms in the calculus implies their interchangeability in all program contexts.

Recently, Felleisen with Friedman [9] and Hieb [10] extended Plotkin’s work to call-by-value programming languages with imperative constructs like assignments and jumps. Their result shows that, like functional constructs, imperative constructs have a simple rewriting semantics, and that there are conservative extensions of the λ_{v}-calculus for reasoning about them, namely the λ_{v}-{C,S,CS}-calculi.

The extension of Plotkin’s work to imperative languages is important because it enables us to consider the whole spectrum of conventional parameter-passing techniques. Specifically, it is only through the addition of imperative constructs that the design options for alternative parameter-passing techniques become interesting. Whereas in a functional setting the only observable differences between call-by-value and call-by-name versions of a program is the termination behavior, the two versions of the same program can produce different results in imperative languages. Moreover, in the presence of assignments, it is also possible to distinguish parameter-passing techniques that bind parameters to values from those that bind parameters to references to values.

∗The authors are supported in part by NSF and DARPA. The Instituto de Computacion of the Universidad de la Republica Oriental del Uruguay generously provided facilities for preparing the final version of the paper.

Appeared in:

18th POPL January 19–22, 1991 Orlando, FL 0

Based on these observations, we classify parameterpassing techniques according to their respective evaluation and binding strategies. The evaluation strategy determines when to evaluate procedure arguments, while the binding strategy determines what part of the argument to bind to formal parameters.

The two prevailing evaluation strategies are eager evaluation (call-by-value), which evaluates the argument to a procedure call before binding the parameter, and delayed evaluation (call-by-name), which does not evaluate the argument until the value of the parameter is needed.^{1}

As for binding strategies, we consider pass-by-worth, which binds the parameter to the value, i.e., “worth,” of the argument, and pass-by-reference, which binds the parameter to a variable, i.e., a “reference” to a value. A third strategy, pass-by-value-result, has properties of both pass-by-worth and pass-by-reference.

In this paper, we analyze the parameter-passing techniques produced by the various combinations of evaluation and binding strategies. Also included is a discussion of the reference cell, a language construct that provides an alternative to the pass-by-reference binding technique. For each technique we develop a rewriting semantics and a calculus for a higher-order programming language that uses the technique. The calculi satisfy variants of Plotkin’s correspondence criteria. In addition, their imperative fragments satisfy strong normalization theorems and are therefore decidable.

The next section of this paper describes in more detail the steps of the analysis: the definition of an operational semantics, the derivation of an equational calculus, and the formal analysis of correspondence between the semantics and the calculus. Section 3 examines each of the parameter-passing techniques using the methods outlined in Section 2. We discuss related work and compare the different techniques in Sections 4 and 5.

2 From Operational Semantics to Calculi

In our analysis of parameter-passing, there are three main steps. First, we define an operational semantics for a language with a particular parameter-passing technique. Next, we derive an equational calculus directly from the semantics, and finally, we analyze the correspondence between the calculus and the semantics. This section describes each of these steps in more detail.

Definition of a Language and its Operational Semantics

The definition of a language consists of two parts: the specification of a syntax and an operational semantics. We provide one for each of the parameter-passing techniques. The core of our languages, Λ, consists of constants (c), variables (x), λ-abstractions and applications of the λ-calculus:

e ::= x | v | (ee)
v ::= c | λx.e

The languages extend Λ with constructs for side-effects, which we describe in later sections.

Following Barendregt’s [1] conventions, we assume that, in the following definitions and theorems, the bound variables are distinct from the free variables in expressions, and we identify expressions that differ only by a renaming of the bound variables. The expression e[x ← e′] denotes the expression resulting from the substitution of all free occurrences of the variable x in e with the expression e′. The set of free variables in an expression e is denoted by FV (e). An expression with no free variables is closed.

Below we need the notion of a context for several definitions. A context, C , is a term with a “hole” ([ ]) in the place of a subexpression; C[e] is the expression produced by replacing the hole in a context C with the expression e.

The operational semantics of a language is a partial function, eval, from programs to answers. A program is a closed expression; an answer is some (yet-to-be-defined) syntactic class of expressions (and programs). The eval function is based on an abstract machine. The state space of the machine is the set of programs; an evaluation step in the machine corresponds to the rewriting of an entire program:

p > p′.

Thus, the transitive closure of the transformation function defines the semantics:^{2}

eval(p) = a iff p >^{∗} a,

1Two other delayed evaluation strategies, which we do not consider in this paper, are call-by-text and call-by-need. Call-by-text never evaluates procedure arguments, thus, delaying evaluation forever. Muller [17] recently analyzed some of the problems of deriving equational theories in the presence of call-by-text. Call-by-need is an optimization of call-by-name in a functional language, but produces different answers than call-by-name in the presence of side-effects. The extended version of this paper [4] contains a brief discussion of call-by-need.

2This characterization is too simple. For clarity, we omit the added complications that are described in the next section.

for program p and answer a.

Every evaluation step on the machine begins with partitioning the program into an evaluation context and a redex. The evaluation context is a special kind of context that specifies the evaluation order of subexpressions in a compound expression. Intuitively, the hole in an evaluation context points to the next subexpression to be evaluated. A redex is an expression that determines how the transformation function rewrites the program. For each redex there is a rewriting rule that specifies how to transform a program that contains the redex in the hole of an evaluation context into a new program. The union of these rewriting rules defines the machine transformation function.

Although we vary the evaluation and binding strategies for user defined procedures below, we assume that primitives have a fixed interpretation. Specifically, we assume that primitives are strict and that they only accept proper values. The set of values (Values) consists of constants and λ-abstractions. To avoid an overspecification of these constants (Consts), we only require the existence of a partial function, δ, from functional constants (FConsts) and closed values to closed values. We restrict δ so that functional constants cannot distinguish the intensional aspects of λ-abstractions. That is, if δ(f, v) is defined for some λ-abstraction v, then there exists a context C[ ] such that C[v] is a value and for all λ-abstractions v′, δ(f, v′) ≡ C[v′]. This restriction on functional constants is reasonable in the context of most programming languages. Essentially, it prohibits from the language only those primitive functions that can examine the text of procedure bodies. But, the restriction still permits functions that can distinguish constants from procedures (e.g., predicates such as int? and proc?) or that can build larger values composed of procedures (e.g., arrays or lists of procedures).

Observational Equality and Calculi

Since an implementation of a language generally provides the programmer with nothing but the evaluation function, the programmer can only observe the behavior of expressions when they are a part of the program. This fact induces a natural notion of equivalence for arbitrary phrases of a programming language. Intuitively, two terms are observationally equivalent if they are interchangeable in all programs without affecting the observable behavior of the programs.^{3} Two programs have the same observable behavior if either they both diverge or they both converge, and if one evaluates to a basic constant then the other evaluates to the same constant.

Definition 2.1. (Observational Equality) Two terms are observationally equivalent, e ≃ e′, if for all contexts C such that both C[e] and C[e′] are programs,

1. eval(C[e]) is defined iff eval(C[e′]) is defined, and

2. eval(C[e]) is a basic constant iff eval(C[e′]) is the same constant.

Proving the observational equivalence of two terms is a difficult task. A proof must show that for all program contexts, the two terms are interchangeable without affecting the program behavior. For this reason, programming language research attempts to construct theories for proving observational equivalences in an axiomatic fashion. Such theories are often referred to as calculi in analogy to the λ-calculus.

In the following sections, we will attempt to derive an equational theory from the operational semantics of each parameter-passing technique. The most straightforward attempt is to make the transformation steps for programs into equational axioms for arbitrary terms.

Definition 2.2. (Natural Calculus) The relation = is the least congruence relation generated by the transformation function >, extended to arbitrary expressions:

e_{1} > e_{2} ⇒ e_{1} = e_{2}  (Axioms)
e_{1} = e_{2} ⇒ C[e_{1}] = C[e_{2}]  (Compatible)
e_{1} = e_{1}  (Reflexive)
e_{1} = e_{2} ⇒ e_{2} = e_{1}  (Symmetric)
e_{1} = e_{2}, e_{2} = e_{3}
⇒ e_{1} = e_{3}  (Transitive)

For a specific theory th, we write th ⊢ e_{1} = e_{2} if e_{1} = e_{2} by the above axioms and rules. If e_{1} = e_{2} without use of the symmetry axiom, we also write e_{1} ⟶ e_{2} and refer to the relation as a reduction.

The Analysis of Calculi

Given a semantics, its observational equivalence relation and a calculus, it is natural to ask how the latter relates to the former. Plotkin [20] gave two criteria for correspondence between a calculus and a semantics. First, the calculus must be capable of evaluating programs. In particular, if the semantics defines the meaning of a program e to be a, then the two should be provably equivalent in the calculus. Similarly, if the calculus proves that a program is equivalent to an answer, then the meaning of the program must be defined by the semantics. Second, the calculus must be sound with respect to the observational equivalence relation: If two terms are equal in the calculus, they must be observationally equivalent with respect to eval.

Definition 2.3. (Correspondence) A theory th corresponds to a semantics eval:

th ⊧ Corr(eval),

if the following conditions hold:

3For historical reasons, some authors call this relation operational equivalence. To avoid confusion, we use the term observational because the relation is based upon observable characteristics, independent of an operational semantics.

1. th is adequate:

(a) if eval(e) = a, then th ⊢ e = a.

(b) if th ⊢ e = a, where a is an answer, then eval(e) is defined.

2. th is sound with respect to ≃:

th ⊢ e_{1} = e_{2} implies e_{1} ≃ e_{2}

A secondary question about a calculus is whether it is decidable. Although our calculi are not decidable, in most cases the imperative fragment of the languages has a decidable subtheory. For these cases we show that there is a strongly normalizing notion of reduction that corresponds to the subtheory. We write r ⊧ SN, if the notion of reduction r is strongly normalizing.

3 Equational Theories of Parameter-Passing Techniques

3.1 Call-by-value/Pass-by-worth

Many common programming languages, e.g., C, ML, Pascal and Scheme, employ the call-by-value/pass-by-worth parameter-passing technique. In these languages, a procedure application evaluates the argument expression before binding the formal parameter to the value of the argument. In this section, we present a call-by-value/pass-by-worth language with assignment, derive a calculus for reasoning about the language, and show that it corresponds to the semantics. Both the language and calculus are variations on the work by Felleisen and Hieb [10].

The call-by-value term language, Idealized Scheme or IS_{v}, extends Λ with two new expressions. First, there is an assignment statement, (set! x e), which assigns to the variable x the value of the expression e. The result of an assignment expression is the value that is assigned to the variable. Second, there is a ρ-expression, which is similar to a block in Algol and the letrec expression in Scheme. It contains a sequence of variable-value pairs and a sub-expression. The ρ-expression establishes mutually recursive bindings of the variables to their associated values and returns the value of the sub-expression. The term language IS_{v} is given in the first part of Figure 1.

There are two basic differences between this language and the language of Felleisen and Hieb [10]. First, we use the assignment statement set! instead of the sigma capability. Although the sigma capability is a powerful programming construct, most languages implement weaker constructs such as the set! expression. Second, like in Scheme, all variables are assignable, that is, they may occur in the variable position of a set! expression.

Therefore, unlike in the λ_{v}-calculus [20] and the λ_{v}-S-calculus [10], variables in our language are expressions, not values.^{4}

In addition to adopting Barendregt’s conventions for free and bound variables, we identify ρ-lists that differ only by the ordering of their pairs:

(x_{1}, v_{1}) … (x_{n}, v_{n}) ≡ (x_{i_{1}}, v_{i_{1}}) … (x_{i_{n}}, v_{i_{n}}),
for all permutations i_{1}, …, i_{n} of 1, …, n.

Put differently, we treat ρ-lists as sets of pairs and in some circumstances as finite functions. Accordingly, we refer to a ρ-list as a ρ-set and use standard set operations on these sets.

The set of assigned variables in an expression e, denoted AV (e), is the set of free variables in e that occur in the variable position of a set! expression.

Semantics

The semantics of the call-by-value/pass-by-worth language is the partial function, eval_{vw}, from programs to answers, where an answer is either a value, or a ρexpression whose body is a value. As discussed in the previous section, the program rewriting function first partitions a program into an evaluation context and a redex and then transforms it to a new program. A callby-value evaluation context specifies the eager evaluation strategy:

E_{v} ::= [ ] | (v E_{v}) | (E_{v} e) | (set! x E_{v})

The call-by-value/pass-by-worth language redexes are the following expressions: fv, (λx.e)v, x, (set! x v), and ρθ.e.

The machine rewrites the program until it produces an answer and then removes all unneeded ρ-bindings by applying “garbage collection” reductions to the answer. More technically, the garbage collection notion of reduction gc is the union of the following relations:

ρθ_{0} ∪ θ_{1}.e ⟶ ρθ_{1}.e
if θ_{0} ≠ and
FV (ρθ_{1}.e) ∩ Dom(θ_{0}) =
ρ .e ⟶ e

It is easy to verify that the notion of reduction gc is strongly normalizing and Church-Rosser. Therefore, all expressions in IS_{v} have a unique gc-normal form (gcnf). Furthermore, the gc-nf of an answer is also an answer.

4Although variables are values in the λ_{v}-calculus, the addition of an assignment statement to the language requires that assignable variables not be values. Felleisen et al [9, 10] conservatively extend the λ_{v}-calculus by enlarging the set of variables with a set of assignable variables. The original unassignable variables of the λ_{v}-calculus are values, whereas the additional assignable variables are not. Since this property is highly context-sensitive and possibly difficult to determine by a programmer, we abandon this distinction.

Syntax, IS_{v}:

x ∈ Vars
c ∈ Consts
f ∈ FConsts

e ::= v | x | (e e) | (set! x e) | ρθ.e
v ::= c | λx.e
θ ::= ϵ | θ(x, v), where (x, v′) ∉ θ
a ::= v | ρθ.v

(Expressions) (Values) (ρ-lists) (Answers)

Evaluation Contexts

E_{v} ::= [ ] | (v E_{v}) | (E_{v} e) | (set! x E_{v})

Transformation Function:

ρθ.E_{v}[fv] >_{vw} ρθ.E_{v}[δ(f, v)], if δ(f, v) defined.  (E.δ)
ρθ.E_{v}[(λx.e)v] >_{vw} ρθ.E_{v}[e[x ← v]], if x ∉ AV (e)  (E.β_{v})
ρθ.E_{v}[(λx.e)v] >_{vw} ρθ.E_{v}[ρ{(x, v)}.e], if x ∈ AV (e)  (E.β_{σ})
ρθ ∪ {(x, v)}.E_{v}[x] >_{vw} ρθ ∪ {(x, v)}.E_{v}[v]  (D_{v})
ρθ ∪ {(x, u)}.E_{v}[(set! x v)] >_{vw} ρθ ∪ {(x, v)}.E_{v}[v]  (σ_{v})
ρθ.E_{v}[ρθ′.e] >_{vw} ρθ ∪ θ′.E_{v}[e]  (ρ_{∪})

Semantics:

eval_{vw}(e) = a, if ρ .e >_{vw}^{∗} ρθ.v, and a is the gc-normal form of ρθ.v.

Fig. 1: Call-by-value/Pass-by-worth Language

The program transformation function, >_{vw}, and the semantics, eval_{vw}, for the call-by-value/pass-by-worth language, are defined in the second part of Figure 1. The first two rules, E.δ and E.β_{v}, provide the call-by-value semantics for Λ; the others specify the effects of imperative constructs.

Calculus

We derive an equational theory, λ_{v}-W or the λ_{v}-W-calculus, for the call-by-value/pass-by-worth language by generating an equivalence relation, =_{vw}, based upon the compatible closure of the program transformation function and the notion of reduction gc. We write λ_{v}-W ⊢ e_{1} = e_{2} if e_{1} =_{vw} e_{2}. The λ_{v}-W-calculus corresponds to the semantics eval_{vw}.

Theorem 3.1 λ_{v}-W ⊧ Corr(eval_{vw}).

Proof. Adequacy follows from the fact that >_{vw} and gc are subsets of =_{vw}. For soundness, we derive a notion of reduction vw from >_{vw} and gc. The reduction satisfies Church-Rosser and Curry-Feys Standardization lemmas that imply the soundness of the calculus.

Otherwise, the proof is an adaptation of the proofs for the calculi of Plotkin [20] and Felleisen et al [9, 10]. For details, we refer the reader to the extended report [4].

Finally, we examine the question of whether there are decidable subsets of the calculus. In our case, the imperative subtheory ρ_{v}, that is, the theory based upon the transition relations that do not deal with procedure applications, is decidable. Specifically, the notion of reduction consisting of these relations is strongly normalizing. This is a new result, which does not hold for the imperative fragment of the λ_{v}-S-calculus. It is motivated by the completeness theorem for a non-recursive fragment of first-order Lisp by Mason and Talcott [16].

Theorem 3.2 Let δ_{c} be the modification of the relation E.δ as follows:

(f v) ⟶ δ(f, v), where δ(f, v) ∈ Consts  (δ_{c})

Let s = δ_{c} ∪ D_{v} ∪ σ_{v} ∪ ρ_{∪} ∪ gc. Then, s ⊧ SN.

Proof. The proof uses a size argument. We define a “potential” function, P : Expressions ⟶ × , such that P (e) ≻ P (e′), by lexicographical ordering, if e⟶_{s} e′. The naïve approaches to defining a size function fail, because certain reductions increase the size of the term and the number of redexes in the term. For example, the following reduction increases the size of the term and the number of redexes because the subexpression e is replicated:

ρ{(x, λx.e)}.E[x] ⟶_{s} ρ{(x, λx.e)}.E[λx.e]

Therefore, the function P not only counts the number of redexes in a term, but also takes into account potential redexes that may be introduced in reductions such as this. Again, the details can be found in the extended report [4].

3.2 Call-by-value/Pass-by-reference

Pascal, Fortran and other languages allow pass-by-reference procedure parameters in addition to pass-by-worth parameters. Generally, these languages require that the actual argument for a pass-by-reference parameter be a variable. A procedure application binds the parameter to the variable so that during the evaluation of the procedure body, references and assignments to the formal parameter are equivalent to references and assignments to the actual argument. Our semantics generalizes pass-by-reference and allows arbitrary expressions as arguments to procedures. If the argument is not a variable, the transformation function evaluates the argument until it becomes a variable before the procedure call. If the argument does not evaluate to a variable, then the meaning of the program is undefined.

Semantics

The term language for the pass-by-reference semantics is IS_{v}, except that we interpret λx.e as a pass-by-reference procedure. Two changes to the pass-by-worth program transformation function in Figure 1 are necessary to obtain the transformation function for the passby-reference semantics:

• When a variable occurs as an argument to a λabstraction, the transition function substitutes the argument variable for the bound variable within the body of a λ-abstraction:

ρθ.E_{v}[(λx.e)y] > ρθ.E_{v}[e[x ← y]]  (E.β_{r})

• The transition function does not dereference a variable when it occurs as an argument to a lambda abstraction:

ρθ.E_{v}[x] > ρθ.E_{v}[v]  (E.D′_{v})
if θ(x) = v, and
E_{v} ≠ E′_{v}[(λy.e)[ ]]

The pass-by-reference transformation function, >_{vr} is the union of the two new rules and previously defined rules in Figure 1:

>_{vr} = E.δ ∪ E.β_{r} ∪ E.D′_{v} ∪ σ_{v} ∪ ρ_{∪}

The semantic function eval_{vr} and observational equivalence relation ≃_{vr} are defined in the usual way.

Calculus

The first difference between the by-value and byreference parameter passing systems is that the natural derivation of the calculus from the semantics (as specified in Section 2) results in an unsound theory. Specifically, the variable dereference relation E.D′_{v} is an unsound axiom with respect to the observational equivalence relation. However, since this is only the case when the variable occurs in the empty context, adding a restriction solves the problem:

ρθ.E_{v}[x] = ρθ.E_{v}[v]  (D′_{v})
if θ(x) = v,
E_{v} ≠ E′_{v}[(λy.e)[ ]],
and E_{v} ≠ [ ]

With this axiom replacing E.D′_{v}, the derivation of the λ_{v}-R-calculus proceeds as usual by constructing the appropriate equivalence relation from the modified transformation function and the notion of reduction gc.

Because of the soundness problem encountered with the E.D′_{v} rule, the calculus does not exactly correspond to the semantics by Plotkin’s criteria. The condition on the D′_{v} reduction relation restricts the ability of the calculus to evaluate programs, i.e., the calculus can only evaluate the programs to an expression that is “one step away” from the answer by the program transformation function. Based on this observation, we prove the following weak correspondence theorem.^{5}

Theorem 3.3 The λ_{v}-R-calculus “weakly” corresponds to the call-by-value/pass-by-reference semantics of IS_{v}, λ_{v}-R ⊧ WCorr(eval_{vr}). In particular,

1. λ_{v}-R is “almost” adequate:

(a) if eval_{vr}(e) = a then either

• λ_{v}-R ⊢ e = a, or

• λ_{v}-R ⊢ e = ρθ ∪ {(x, v)}.x and λ_{v}-R ⊢ ρθ ∪ {(x, v)}.v = a.

(b) if λ_{v}-R ⊢ e = a, then eval_{vr}(e) is defined.

2. λ_{v}-R is sound with respect to ≃_{vr}:

λ_{v}-R ⊢ e_{1} = e_{2} implies e_{1} ≃_{vr} e_{2}

The imperative fragment of the pass-by-reference calculus, ρ′_{v}, as well as its procedure call reduction, β_{r}, are strongly normalizing for the full language.

Theorem 3.4 Let s′ = δ_{c} ∪ D′_{v} ∪ σ_{v} ∪ ρ_{∪} ∪ gc. Then, s′ ⊧ SN and β_{r} ⊧ SN.

3.3 Call-by-value-result

The programming languages Ada [23] and Algol W [24] specify a parameter-passing technique known as callby-value-result, or copy-in/copy-out.^{6} This parameterpassing technique uses the eager evaluation strategy and is similar to both the pass-by-worth and pass-by-reference binding techniques. Like pass-by-reference, arguments to procedures must be variables. Like pass-by-worth, the procedure applications bind the formal parameter to the value of the argument variable. However, after evaluation of the procedure body, the argument variable receives the value of the formal parameter.

5An alternative to formulating a weak correspondence relationship would be to redefine the semantics to correspond to the calculus. In particular, if we treat the expression ρθ.x as an answer in the semantics, then the calculus satisfies the correspondence criteria. However, existing programming languages do not use this notion of call-by-value/pass-by-reference semantics.

6Technically, the term “call-by-value/pass-by-value-result” is the name consistent with our terminology. We use the more popular name call-by-value-result for simplicity.

Semantics

The sequential nature of the call-by-value-result protocol requires the specification of a sequence statement for IS_{v}, ⟨e; e⟩, and an appropriate extension of evaluation contexts:

E_{v} ::= … | ⟨E_{v}; e⟩.

The  expression  ⟨e_{1}; e_{2}; … e_{n}⟩  abbre-

viates ⟨e_{1}; ⟨e_{2}; … e_{n}⟩⟩. The semantics of the sequence expression is straightforward; the left sub-expression is evaluated first, followed by the right:

ρθ.E_{v}[⟨v; e⟩] > ρθ.E_{v}[e]  (E.seq)

A procedure application requires four steps. First, the application binds the procedure parameter to the value of its argument. Second, evaluation continues with the procedure body. Third, the value bound to the parameter is “copied” back to the argument. Finally, the result of the application is the value obtained from evaluation of the procedure body. We use the sequence expression to specify this series of events:

ρθ.E_{v}[(λx.e)y] >  (E.β_{c})

ρθ.E_{v}[ρ{(x, λx.x), (r, λx.x)}. ⟨(set! x y); (set! r e); (set! y x); r⟩]

The variable r is a new variable that holds the return value of the procedure. The value λx.x is an arbitrary initial value. The complete rewriting function relies on these and previously defined rules:

>_{cc} = E.δ ∪ E.β_{c} ∪ E.D′_{v} ∪ σ_{v} ∪ ρ_{∪} ∪ E.seq

As usual, the transitive closure of >_{cc} and the notion of reduction gc determine eval_{cc}.

Calculus

The equational calculus for the call-by-value-result language closely resembles the λ_{v}-R-calculus for the callby-value/pass-by-reference language. The problems encountered with the dereference axiom in the previous section also occur with the call-by-value-result calculus. The same D′_{v} axiom solves the problem.

The call-by-value-result calculus only “weakly” corresponds to the semantics in the same way as the callby-value/pass-by-reference calculus.

Theorem 3.5 λ_{v}-VR ⊧ WCorr(eval_{cc})

The imperative fragment of this calculus extends the imperative fragment of the call-by-value/pass-by-ref-erence calculus with the seq reduction. With this addition, the Strong Normalization Theorem for the notion of reduction s′ also holds for s′ ∪ seq.

3.4 Call-by-name/Pass-by-reference

The Revised Report on Algol 60 [18] informally defined the semantics of call-by-name parameter-passing with the copy rule. The intention was to implement Church’s [3] β relation from the original λ-calculus as the parameter-passing technique of the new language. Copying an argument to every parameter occurrence was thought to be the computational equivalent to function evaluation in ordinary mathematics. A hidden motive may have been the desire to perceive Algol as an extension of the λ-calculus as a language as well as an equational theory.

The requirements of the copy rule imply a pass-by-reference semantics. If the formal parameter is assigned, then the procedure argument should evaluate to a variable. Assignments to the parameter become assignments to this variable argument, and these effects on the argument will be visible in the context of the procedure application.

Semantics

The term language for the call-by-name/pass-by-reference language, IS_{n}, differs from IS_{v} in two ways. First, to exploit the freedom of the delayed evaluation strategy, ρ-expressions can bind variables to arbitrary expressions:

θ ::= ϵ | θ(x, e) where (x, e′) ∉ θ

Second, since the copy rule substitutes expressions for free variables, the language must permit expressions to occur in any position where variables are allowed. In particular, we extend the syntax of IS_{n} to allow expressions in the variable position of set! expressions: (set! e e) replaces (set! x e) in the definition of the term language. The rest of IS_{n} is the same as IS_{v}, with λx.e representing a call-by-name/pass-by-reference procedure.

The call-by-name evaluation contexts specify the delayed evaluation strategy. Since the context (λx.e) E specifies the evaluation of procedure arguments prior to the procedure call, it cannot be an evaluation context for the delayed evaluation strategy. On the other hand, the application of functional constants remains strict. The definitions of the evaluation contexts and the program transformation function are given in Figure 2.

Remark. Although some of the relations in Figure 2 have the same names as relations introduced for the callby-value language, there are differences due to change in the definition of evaluation contexts. Relations with the same name share reduction schema. The textual context will disambiguate all uses of these names. End.

The transformation function uses only the E.β rule for defining the behavior of all procedure applications.

E_{n} ::= [ ] | (f E_{n}) | (E_{n} e) | (set! x E_{n}) | (set! E_{n} e)

ρθ.E_{n}[fv] >_{nr} ρθ.E_{n}[δ(f, v)]  (E.δ)
ρθ.E_{n}[(λx.e)e′] >_{nr} ρθ.E_{n}[e[x ← e′]]  (E.β)
ρθ ∪ {(x, e)}.E_{n}[x] >_{nr} ρθ ∪ {(x, e)}.E_{n}[e], if E_{n} ≠ E′_{n}[(set! [ ] e′)]  (E.D_{n})
ρθ ∪ {(x, e)}.E_{n}[(set! x v)] >_{nr} ρθ ∪ {(x, v)}.E_{n}[v]  (σ_{n})
ρθ.E_{n}[ρθ′.e] >_{nr} ρθ ∪ θ′.E_{n}[e]  (ρ_{∪})

Fig. 2: Call-by-name/Pass-by-reference Semantics

The restriction on the E.D_{n} rule is necessary to disallow dereference of a variable when it occurs in the variable position of an assignment. The semantics eval_{nr} is determined by the transitive closure of >_{nr} and gc as in previous sections.

Calculus

The derivation of a calculus from the semantics follows the same course as the call-by-value/pass-by-reference language, but the natural approach results in an unsound system. Again, the dereferencing rule causes the problem. Adding an appropriate condition to the dereference rule solves the problem:

ρθ.E_{n}[x] ⟶ ρθ.E_{n}[e]  (D_{n})
if θ(x) = e,
E_{n} ≠ E′_{n}[(set! [ ] e′)],
and E_{n} ≠ [ ]

We then derive the calculus by constructing the appropriate equivalence relation from a modified transformation function in which D_{n} replaces E.D_{n}.

The call-by-name/pass-by-reference and call-by-value/pass-by-reference languages have several similarities. Both require a modified dereference rule to prohibit variable dereference in certain positions. Similarly, the direct derivation of a calculus from the semantics results in an unsound system. Not surprisingly, as with the λ_{v}-R-calculus, the λ_{n}-R-calculus only “weakly” corresponds to the semantics. However, this weak correspondence is even weaker than for the call-by-value language. The reason is that while neither calculus can perform a variable dereference in an empty context, this kind of dereference in the call-by-value language would return a value and thus an answer, whereas in the callby-name language it does not. As a result, the λ_{v}- R-calculus can evaluate programs to expressions that are just one transformation step from an answer, but the λ_{n}-R-calculus requires an arbitrary number of these transformation steps throughout the derivation.^{7} Theorem 3.6 The λ_{n}-R-calculus only very weakly corresponds to the call-by-name/pass-by-reference semantics of IS_{n}, eval_{nr}. In particular,

1. λ_{n}-R is weakly adequate:

(a) if eval_{nr}(e) = a then either λ_{n}-R ⊢ e = a, or there exists an m such that for all n between 0 and m:

λ_{n}-R ⊢ e = ρθ_{1} ∪ {(x_{1}, e′_{1})}.x_{1}
λ_{n}-R ⊢ ρθ_{n} ∪ {(x_{n}, e′_{n})}.e′_{n} =
ρθ_{n+1} ∪ {(x_{n+1}, e′_{n+1})}.x_{n+1}
λ_{n}-R ⊢ ρθ_{m} ∪ {(x_{m}, e′_{m})}.e′_{m} = a

(b) if λ_{n}-R ⊢ e = a, then eval_{nr}(e) is defined; and

2. λ_{n}-R is sound with respect to ≃_{nr}:

λ_{n}-R ⊢ e_{1} = e_{2} implies e_{1} ≃_{nr} e_{2}.

Because ρ-sets may have recursive references, the imperative subtheory, ρ_{n}, is not decidable on the full language IS_{n}. For example, there are infinite reduction sequences in ρ_{n} for the diverging IS_{n} program ρ{(x, x)}.x. On the other hand, ρ_{n} is strongly normalizing over the subset of IS_{n} in which the ranges of all ρ-sets are in Values.

Theorem 3.7 The notion of reduction s_{n} = δ_{c} ∪ D′_{n} ∪ σ_{n} ∪ ρ_{∪} ∪ gc is strongly normalizing over the subset of IS_{n} in which the ranges of ρ-sets are restricted to values.

Finally, as intended by the designers of Algol, the λ_{n}- R-calculus is indeed a conservative extension of the λcalculus.

Theorem 3.8 λ = λ_{n}-R|Λ

Proof. Clearly, any proof in λ is also a proof in λ_{n}-R. On the other hand, a proof in λ_{n}-R may use axioms that are not in λ. In this case, the Church-Rosser property ensures that two equivalent expressions reduce to a third expression. These reductions must only use the β and δ axioms of the λ-calculus since the expressions are in Λ.

7As above, changing the semantics would fix the problem, too:

this time thunks would have to be valid answers. But again, existing languages are strict at the top level.

Syntax, IS_{b}:

b ∈ Boxes

e ::= v | (e e) | ρθ.e
v ::= c | b | x | λx.e | box | setbox! | unbox | (setbox! b)
θ ::= ϵ | θ(b, v), where (b, v′) ∉ θ

(Expressions) (Values) (ρ-lists)

Semantics:

E ::= [ ] | (v E) | (E e)
ρθ.E[fv] >_{bx} ρθ.E[δ(f, v)] if δ(f, v) defined.  (E.δ)
ρθ.E[(λx.e)v] >_{bx} ρθ.E[e[x ← v]]  (E.β_{v})
ρθ.E[box v] >_{bx} ρθ.E[ρ{(b, v)}.b]  (E.box)
ρθ ∪ {(b, v)}.E[unbox b] >_{bx} ρθ ∪ {(b, v)}.E[v]  (D_{b})
ρθ ∪ {(b, u)}.E[(setbox! b)v] >_{bx} ρθ ∪ {(b, v)}.E[v]  (σ_{b})
ρθ.E[ρθ′.e] >_{bx} ρθ ∪ θ′.E[e]  (ρ_{∪})

Fig. 3: Reference Cell Language

3.5 Call-by-value/Pass-by-worth: Reference Cells as Values

The motivation for the pass-by-reference parameterpassing technique is the need to affect argument variables. To accomplish this, the pass-by-reference passing technique binds the formal parameter to the argument variable so that assignments to the parameter become assignments to the argument. Languages such as C, ML and Scheme do not use pass-by-reference, but instead have a new class of values, namely, pointers, reference cells or boxes that can achieve a similar result. A reference cell is a language object that refers to a value. A dereference expression returns the value to which a cell refers; an assignment expression changes this value. When a cell occurs as the argument to a procedure, the application binds the formal parameter to the cell because a cell is a value. In this way, an assignment to the formal parameter becomes visible in the context of the procedure application, as in pass-by-reference. Although the reference cell concept is not a proper parameter-passing technique, we consider it here because of its relation to both pass-by-worth and passby-reference parameter-passing.

Semantics

We abandon the assignment of IS_{v} in favor of the reference cell assignment expression. Since variables are no longer assignable, we treat them as values. The term language IS_{b} extends the language of the λ_{v}-calculus with the ρ-expression, a set of reference cells and expressions for creating, assigning and dereferencing cells. Adopting Chez Scheme terminology [7], we use the primitives box, setbox!, and unbox to perform these operations in IS_{b}. The first part of Figure 3 contains the specification of the term language IS_{b}. As usual, both λ-abstractions and ρ-expressions are binding expressions, but while λ binds variables, ρ binds reference cells. There is also a notion of free cells analogous to free variables.

The evaluation contexts and the transformation function are also defined in Figure 3. As usual, the transitive closure of the transformation function and the garbage collection reductions define the semantics, eval_{bx}. The notion of reduction gc is slightly different in this setting because it uses the notion of free cells instead of free variables to determine the unneeded items in ρ-sets.

Calculus

We derive the λ_{v}-B-calculus for reasoning with reference cells directly from the semantics by generating an equivalence relation from the transformation function and the garbage collection reduction as in previous sections. The resulting theory, λ_{v}-B, corresponds to the semantics, eval_{bx}:

Theorem 3.9 λ_{v}-B ⊧ Corr(eval_{bx})

Furthermore, the imperative fragment of this calculus, ρ_{b}, is decidable:

Theorem 3.10 Let s_{b} = δ_{c} ∪ D_{b} ∪ σ_{b} ∪ ρ_{∪} ∪ gc. Then, s_{b} ⊧ SN.

Finally, the λ_{v}-B-calculus is a conservative extension of the λ_{v}-calculus. Thus, the equivalence proofs from the λ_{v}-calculus also hold in the λ_{v}-B-calculus.

Theorem 3.11 λ_{v} = λ_{v}-B|Λ

The reference cell is interesting because of its relation to both pass-by-worth and pass-by-reference languages. The connection to the pass-by-worth language is apparent: the reference cell language employs callby-value/pass-by-worth parameter passing, and box assignments in IS_{b} are similar to variable assignments in IS_{v}. In fact, it is possible to show that IS_{b} and IS_{v} are equivalent in the formal sense of programming language expressiveness [8]. For the pass-by-reference language, the connection is not as clear, and we have no formal expressibility results. However, reference cells in the pass-by-worth language provide the ability to abstract over assignments to formal arguments (cells in this case), which was the original motivation for passby-reference. The reason is that cells are values and can be passed as arguments, whereas variables in IS_{v} are not values and are dereferenced when they occur as arguments in the pass-by-worth semantics. The passby-reference semantics provides an alternative: it passes only variables and does not allow dereferencing variables when they occur as arguments. Reference cells in a callby-value/pass-by-worth language provide both options within the same, simple language.

4 Related Work

Our equational systems were motivated by the work of Plotkin [20], who studied equational reasoning systems for call-by-name and call-by-value in functional languages, and Felleisen et al [9, 10] who developed calculi for call-by-value imperative languages. Demers and Donahue [5] give an equational logic for reasoning about a higher-order language that uses call-by-value parameter-passing and has memory objects similar to reference cells. The equational theory contains several dozen axioms for which they present no formal results. Mason and Talcott [16] present a conditional deduction system for observational equivalences of Lisp expressions with side-effects, a language similar to the imperative fragment of our reference cell language. Their logic is complete for the recursion-free, first-order fragment of Lisp with side-effects.

In the area of denotational semantics, several authors [11, 22] have given denotational descriptions of the different parameter-passing techniques. Such descriptions specify precise set-theoretic interpretations of parameter-passing but do not provide an intuitive and simple set of equations nor other axiomatic theories.

Finally, a number of researchers have studied parameter-passing in the context of Hoare-like axiomatic semantics [14, 12, 6]. These systems are generally for first-order subsets of Pascal and have a number of restrictions on procedure calls, such as aliasing. Cartwright and Oppen [2] overcome the aliasing restriction, but still do not allow procedures as arguments. Olderog [19] eliminates the restrictions on procedures, but his Hoare-like calculi explicitly require operational specifications of procedure calls using the copy rule.

5 Conclusions

For several common parameter-passing techniques we presented a program rewriting semantics and derived a corresponding calculus. The calculi of pass-by-value languages are simply the equational theories over the rewriting semantics but the calculi for pass-by-reference languages are weaker. In the latter cases, the rewriting rule for dereferencing variables is not sound with respect to observational equivalence. As a result, the correspondence between the calculi and the semantics is weaker for pass-by-reference languages than for pass-by-value languages. All of the calculi are sound but the calculi for pass-by-reference are too weak to serve as a substitute for an evaluator. The underlying reduction systems of the calculi are always Church-Rosser and have the standard reduction property. Finally, the imperative fragments of most calculi are strongly normalizing and therefore decidable.

Table 1 summarizes our results. The Correspondence column refers to how closely a calculus corresponds to the semantics. The necessary modifications to the familiar β axiom are shown under the Beta Axiom heading. The Param and Arg columns show the restrictions on the formal parameter and on the argument in procedure applications. The entry “non-assign” indicates that the rule only applies to applications in which the formal parameter is not assigned in the procedure body. The last column indicates which fragments are strongly normalizing.

A comparison of the calculi reveals some aspects of the relative semantic complexity of the parameterpassing techniques. Although this study verifies the folklore that Algol’s call-by-name/pass-by-reference parameter-passing technique satisfies the full β axiom, it also reveals that this comes at the expense of a weak correspondence relationship and of strange restrictions on the axioms for the imperative fragment of the language. Indeed, call-by-value/pass-by-reference as well as copyin-copy-out share these problems. Of the two remaining combinations, call-by-value/pass-by-worth with boxes has the better characteristics:

1. the calculus is the equational closure of a reduction semantics;

2. because of (1), there is a strong correspondence between the semantics and the calculus;

3. the axioms are simple, without complicated restrictions;

4. and the calculus is a conservative extension of the functional core language.

Because of the above properties, using call-by-value with boxes and reasoning about programs in such language seems the most attractive choice.

Evaluation  Binding  Corres-  Beta Axiom  Decidable
Strategy  Strategy  pondence  Param  Arg  Fragment
call-by-value worth  exact  β_{v} non-assign value ρ_{v}
reference  weak  β_{r}  any  variable ρ′_{v}; β_{r}
value-result  weak  β_{c}  –  –  ρ′_{v} ∪ seq
call-by-name reference  very weak β  any  any  restricted ρ_{n}
call-by-value & reference cells  exact  β_{v}  any  value ρ_{b}

Table 1: Summary

Acknowledgement. We thank Amr Sabry and Rebecca Selke for comments on an early draft.

References

1. Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics. Revised Edition. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, 1984.

2. Cartwright, R. and D. Oppen. The logic of aliasing. Acta Inf. 15, 1981, 365–384.

3. Church, A. The Calculi of Lambda-Conversion. Princeton University Press, Princeton, 1941.

4. Crank, E. Parameter-passing and the lambdacalculus. Master’s Thesis, Rice University, August 1990.

5. Demers, A. and J. Donahue. Making variables abstract: an equational theory for Russell. In Proc. 10th ACM Symposium on Principles of Programming Languages, 1983, 59–72.

6. Donahue, J.E. Complementary Definitions of Programming Language Semantics. Lecture Notes in Computer Science 42, Springer-Verlag, Heidelberg, 1980.

7. Dybvig, R. K. The Scheme Programming Language, Prentice-Hall, Englewood Cliffs, New Jersey, 1987.

8. Felleisen, M. On the expressive power of programming languages. In Proc. 1990 European Symposium on Programming. Neil Jones, Ed. Lecture Notes in Computer Science, 432. Springer Verlag, Berlin, 1990, 134–151.

9. Felleisen, M. and D.P. Friedman. A syntactic theory of sequential state. Theor. Comput. Sci. 69(3), 1989, 243–287. Preliminary version in: Proc. 14th ACM Symposium on Principles of Programming Languages, 1987, 314-325.

10. Felleisen, M. and R. Hieb. The revised report on the syntactic theories of sequential control and state. Technical Report 100, Rice University, June 1989.

11. Gordon, M.J. The Denotational Description of Programming Languages, Springer-Verlag, New York, 1979.

12. Gries, D. and G. Levin. Assignment and Procedure Call Proof Rules. ACM Trans. Program. Lang. Syst. 2(4), 1980, 564–579.

13. Hoare, C. A. R. An axiomatic basis for computer programming. Commun. ACM 12, 1969, 576–580.

14. Hoare, C.A.R. Procedures and parameters: An axiomatic approach. In Symposium on Semantics of Algorithmic Languages, E. Engeler (Ed.). Lecture Notes in Mathematics 188. Springer-Verlag, Berlin, 1971, 102–116.

15. Landin, P.J. The next 700 programming languages. Commun. ACM 9(3), 1966, 157–166.

16. Mason, I.A. and C. Talcott. A sound and complete axiomatization of operational equivalence between programs with memory. In Proc. Symposium on Logic in Computer Science, 1989, 284–293. An extended version will appear in Theor. Comput. Sci.

17. Muller, R. The operational semantics and equational logic of eval and fexprs. Unpublished manuscript. Harvard University, 1990.

18. Naur, P. (Ed.). Revised report on the algorithmic language ALGOL 60. Comm. ACM 6(1), 1963, 1– 17.

19. Olderog, E. Sound and complete Hoare-like calculi based on copy rules. Acta Inf. 16, 1981, 161– 197.

20. Plotkin, G.D. Call-by-name, call-by-value, and the λ-calculus. Theor. Comput. Sci. 1, 1975, 125– 159.

21. Rees, J. and W. Clinger (Eds.). The revised^{3} report on the algorithmic language Scheme. SIG-PLAN Notices 21(12), 1986, 37–79.

22. Schmidt, D.A. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Newton, Mass., 1986.

23. US Department of Defense. The Programming Language Ada—Reference Manual, Lecture Notes in Computer Science 106, Springer-Verlag, 1981.

24. Wirth N. and C.A.R. Hoare. A contribution to the development of ALGOL. Commun. ACM 9(6), 1966, 413–432.