1 Introduction

Since the introduction of the \(\pi \)-calculus, a lot of effort has been devoted to its comparison with the \(\lambda \)-calculus, beginning with Milner’s seminar work on functions as processes [14]. The attention has gone mostly to call-by-name and call-by-value \(\lambda \)-calculi [19], and the main results concern operational correspondence, validity of \(\beta \)-reduction, characterisation of the equivalence induced on \(\lambda \)-terms by the \(\pi \)-calculus encoding [6, 14, 21, 22, 27]. In particular, the call-by-name encoding, for its simplicity, is often presented as the \(\pi \)-calculus representation of functions.

In a call-by-name reduction, the redex contracted is the leftmost one; the reduction occurs regardless of whether the argument of the function is a value (as in call-by-value). As a consequence, if the argument is not a value and will be used several times, its evaluation will be repeated the same number of times. In implementation of programming languages following call-by-name, this repetition of evaluation is avoided: evaluation occurs only once, the first time the term is used, and the value so obtained is recorded for future uses. This implementation technique is referred to as call-by-need evaluation (or strategy) [28]. Thus call-by-need uses explicit environments and \(\beta \)-reduction does not require substituting a term for a variable, as in call-by-name (or call-by-value)—just substituting a reference to a term for a variable. In this sense call-by-need is closer to the \(\pi \)-calculus than call-by-name, as substitutions in the \(\pi \)-calculus only involve names. Again, the modifications that take us from call-by-name to call-by-need can be easily represented in a \(\pi \)-calculus encoding [24].

The \(\pi \)-calculus, having a rich and well-developed theory, as well as a remarkable expressiveness, has been advocated as a foundational model for reasoning about higher-order languages, including equivalence between programs and correctness of compilers and compiler optimisations [25, 26]. Indeed, the \(\pi \)-calculus and related languages have been used, via appropriate encodings, as a target language of compilers, for a number of experimental programming languages, beginning with Pict [18] and Join [7].

The above raises the question about how, and at which extent, the \(\pi \)-calculus and its current theory can be used to prove the correctness of call-by-need as an optimised implementation strategy for call-by-name. The only work on the correctness of the \(\pi \)-calculus representation of call-by-need is by Brock and Ostheimer [5]. The paper considers operational correspondence, between reduction in a call-by-need system and in the encoding \(\pi \)-calculus terms. However there are foundametal semantic issues that remain unexplored. A major one is the validity of \(\beta \)-reduction, namely the property that the processes encoding \(\beta \)-convertible \(\lambda \)-terms are behaviourally iundistinguishable. The property holds in call-by-name (and it is at the heart of its theory), as well as in the \(\pi \)-calculus encoding of call-by-name. One would therefore hope to find analoguos results for call-by-need. The correctness of the process representation of call-by-need is the topic of the present paper, focusing on the validity of \(\beta \)-reduction.

In a well-known and influential paper [17] Palamidessi has shown that the expressive power of the asynchronous \(\pi \)-calculus is strictly less than that of the full (synchronous) \(\pi \)-calculus. This gap in expressiveness has a correspondence, however, in sharper semantic properties for the former calculus, notably concerning algebraic laws. This paper may be seen as a demonstration of this, since most the proofs are carried out using algebraic laws that are only valid in the asynchronous \(\pi \)-calculus—precisely in the Asynchronous Local \(\pi \)-calculus, AL\(\pi \), [12], where only the output capability of names may be exported.

In Sect. 2 we present and some of its laws. In Sect. 3 we briefly recall the call-by-name and call-by-need \(\lambda \)-calculus. In Sect. 4 we consider two encodings of call-by-need. We show that limited forms of validity \(\beta \)-reduction hold, and that the general property fails. The questions that follow from this, discussed in Sect. 5, may contribute to open some interesting directions for future work, which may also shed further light on the theory of the \(\pi \)-calculus and similar name-passing calculi.

2 The Asynchronous Local \(\pi \)-calculus

2.1 Syntax

Small letters \(a,b, \ldots , x,y, \ldots \) range over the infinite set of names, and \(P,Q, R, \ldots \) over the set of all processes. A tilde represents a tuple. The i-th elements of a tuple \(\widetilde{E}\) is referred to as \({\widetilde{E}}_i\). Our notations are extended to tuples componentwise.

The Asynchronous Local \(\pi \)-calculus (AL\(\pi \)) [12] is built from the operators of inaction, input prefix, output, parallel composition, restriction, and replication:

with the syntactic constraint that in processes \({ a({\widetilde{b}}).P }\) and \(! { a({\widetilde{b}}).P }\) names \({\widetilde{b}}\) may not occur free in P in input position.

When the tilde is empty, the surrounding brackets () and \(\langle \rangle \) will be omitted. \({\varvec{0}}\) is the inactive process. An input-prefixed process \(a ({\widetilde{b}}) .P\), where \({\widetilde{b}}\) has pairwise distinct components, waits for a tuple of names \( \widetilde{c} \) to be sent along a and then behaves like , where is the simultaneous substitution of names \({\widetilde{b}}\) with names \( \widetilde{c} \). An output particle emits names \({\widetilde{b}}\) at a. Parallel composition is to run two processes in parallel. The restriction \({\varvec{\nu }} a\, P\) makes name a local, or private, to P. A replication \( ! P\) stands for a countable infinite number of copies of P in parallel. We assign parallel composition the lowest precedence among the operators.

2.2 Terminologies and Notations

We write \(\overline{a}(b) . b( \widetilde{c} ).Q\) as an abbreviation for \({\varvec{\nu }} b\, (\overline{a} b \,\,|\,\,b( \widetilde{c} ).Q)\), and similarly for \(\overline{a}(b) .! b( \widetilde{c} ).Q\). The prefix ‘\(\overline{a}(b) \)’ is called a bound output. In prefixes \( a ({\widetilde{b}})\) and , we call a the subject and \({\widetilde{b}}\) the object. We use \(\alpha \) to range over prefixes. We often abbreviate \(\alpha . {\varvec{0}}\) as \(\alpha \), and \({\varvec{\nu }} a\, {\varvec{\nu }} b\, P\) as \(({\varvec{\nu }} a,b)\, P\). An input prefix \(a ({\widetilde{b}}) .P\) and a restriction \({\varvec{\nu }} b\, P\) are binders for names \({\widetilde{b}}\) and b, respectively, and give rise in the expected way to the definition of free names (fn), bound names (bn) and names (n) of a term or a prefix, and alpha conversion. We identify processes or actions that only differ on the choice of the bound names. The symbol \(=\) will mean “syntactic identity modulo alpha conversion”. Sometimes, we use \({\mathop {=}\limits ^{\text{ def }}}\) as abbreviation mechanism, to assign a name to an expression to which we want to refer later. In a statement, a name declared fresh is supposed to be different from any other name appearing in the objects of the statement, like processes or substitutions. Substitutions are of the form , and are finite assignments of names to names. A context is a process expression with a hole \( [ \cdot ] \) in it. We use \( C \) to range over contexts; then \( C [P] \) is the process obtained from \( C \) by filling its hole with P.

2.3 Sorting

Following Milner [13], we only admit well-sorted agents, that is agents obeying a predefined sorting discipline in their manipulation of names. The sorting prevents arity mismatching in communications, like in \(\overline{a} \langle b, c \rangle \,\,|\,\,a(x) . Q\). A sorting is an assignment of sorts to names, which specifies the arity of each name and, recursively, of the names carried by that name. We do not present the formal system of sorting because it is not essential in the exposition of the topics in the present paper.

We will however allow sorting to identify linear names, that is, names that are supposed to be used only once. Linearity will be used a few times to replace input-replicated prefixes with ordinary input prefixes. Again, we omit the details of linearity in type systems (sorting is a form of type system), as they are by now standard [9, 24].

Fig. 1.
figure 1

The transition system for

Full size image

2.4 Relations

A process has three possible forms of action. A silent action represents an interaction, i.e. an internal activity in P. Input and output actions are, respectively, of the form and In both cases, the action occurs at a—the subject of the action. In the output action, \({\widetilde{b}}\) is the tuple of names which are emitted, and \( \widetilde{d} \subseteq {\widetilde{b}}\) are private names which are carried out from their current scope. We use \(\mu \) to represent the label of a generic action (not to be confused with \(\alpha \), which represents prefixes). In an input action \( a ( \widetilde{d} )\) and in an output action \( ({\varvec{\nu }} \, \widetilde{d} ) \,\overline{a}\langle {\widetilde{b}} \rangle \), names \( \widetilde{d} \) are bound, the remaining ones free. Bound and free names of an action \(\mu \), respectively written \({\mathrm{\mathsf {bn}}}(\mu )\) and \({\mathrm{\mathsf {fn}}}(\mu )\), are defined accordingly. The names of \(\mu \), briefly \( {\mathrm{\mathsf {n}}}(\mu )\), are \({\mathrm{\mathsf {bn}}}(\mu )\cup {\mathrm{\mathsf {fn}}}(\mu )\). The transition system of the calculus is presented in Fig. 1. We have omitted the symmetric versions of rules par and com. Alpha convertible processes have deemed to have the same transitions. We often abbreviate with \(P \longrightarrow Q\). The ‘weak’ arrow \(\Longrightarrow \) is the reflexive and transitive closure of \(\longrightarrow \).

We use the symbol \(\equiv \) to denote structural congruence, a relation used to rearrange the structure of processes [13]. We shall also use it to represent garbage-collection of restrictions and of inert terms.

Definition 1

(Structural congruence).Structural congruence, \(\equiv \), is the smallest congruence relation satisfying the axioms below:

  • \(P\,\,|\,\,{\varvec{0}}\equiv P\), \(\; P{\,\,|\,\,}Q \equiv Q{\,\,|\,\,}P\), \(\; P\,\,|\,\,(Q{\,\,|\,\,}R) \equiv (P{\,\,|\,\,}Q){\,\,|\,\,}R\)

  • \(!{a(x).P} \equiv {a(x).P}\,\,|\,\,!{a(x).P}\);

  • \({{\varvec{\nu }} a\,} {\varvec{0}}\equiv {\varvec{0}}\), \(\; {{\varvec{\nu }} a\,}{{\varvec{\nu }} b\,}P \equiv {{\varvec{\nu }} b\,}{{\varvec{\nu }} a\,}P\), \(\; {{\varvec{\nu }} a\,}(P{\,\,|\,\,}Q) \equiv P\,\,|\,\,{{\varvec{\nu }} a\,}Q \,\) if \(a \not \in {\mathrm{\mathsf {fn}}}(P)\);

  • \({\varvec{\nu }} a\, ( P \,\,|\,\, ! a({\widetilde{b}}).Q) \equiv P\) and \({\varvec{\nu }} a\, ( P \,\,|\,\,a({\widetilde{b}}).Q ) \equiv P\), if \(a\not \in {\mathrm{\mathsf {fn}}}(P)\).

(A derivable law is \({\varvec{\nu }} a\, P \equiv P\), for a not free in P.) A standard behavioural equivalence for the \(\pi \)-calculus is barbed congruence. Barbed congruence can be defined in any calculus possessing: (i) an interaction relation (the \(\tau \)-steps in the \(\pi \)-calculus), modelling the evolution of the system; and (ii) an observability predicate \(\downarrow _{a}\) for each name a, which detects the possibility of a process of accepting a communication with the environment at a. More precisely, we write \(P \downarrow _{a}\;\) if P can make an output action whose subject is a, that is, if there are \(P'\) and an output action \(\mu \) with subject a such that . We write \(P \Downarrow _{a}\) if \(P \Longrightarrow P'\) and \(P' \downarrow _{a}\). Unlike synchronous \(\pi \)-calculus, in asynchronous calculi it is natural to restrict the observation to output actions [1]. The reason is that in asynchronous calculi the observer has no direct way of knowing when a message emitted is received.

Definition 2

(Barbed congruence). A symmetric relation \(\mathcal{S}\) on \(\pi \)-calculus processes is a barbed bisimulation if implies:

  1. 1.

    If then there exists \( Q'\) such that \(Q \Longrightarrow Q'\) and .

  2. 2.

    If \(P \downarrow _{ a}\) then \(Q \Downarrow _{a}\).

Two \(\pi \)-calculus processes P and Q are barbed bisimilar if for some barbed bisimulation \(\mathcal{S}\). We say that P and Q are barbed congruent, written \(P \approx Q\), if for each \(\pi \)-calculus context C, processes C[P] and C[Q] are barbed bisimilar.

Strong barbed congruence, written \(\sim \), is defined analogously but replacing the weak arrows \(\Longrightarrow \) and \(\Downarrow _a\) with the strong arrows \(\longrightarrow \) and \(\downarrow _a\). As expected, we have \({\equiv } \subseteq {\sim } \subseteq {\approx }\); each containment is strict.

2.5 Further Algebraic Laws

Most of the proofs in the paper are carried out using algebraic reasoning. We report here some important laws. First some simple laws that are valid in the full (synchronous) \(\pi \)-calculus (Lemma 1). Then laws that are specific to .

Lemma 1

  1. 1.

    and ;

  2. 2.

    \({\varvec{\nu }} a\, (\alpha . Q{\,\,|\,\,}! a( \widetilde{x} ).P ) \sim \alpha . {\varvec{\nu }} a\, (Q\,\,|\,\,! a( \widetilde{x} ).P ) \), if \({\mathrm{\mathsf {bn}}}(\alpha )\cap {\mathrm{\mathsf {fn}}}(a(\widetilde{x}).P ) = \emptyset \) and \(a\not \in {\mathrm{\mathsf {n}}}(\alpha )\) (a similar law holds without the replication);

  3. 3.

    \( a( \widetilde{x} ). ( P\,\,|\,\,! a( \widetilde{x} ).P ) \sim ! a( \widetilde{x} ).P \).

Important laws of are the following ones. Their validity hinges on the asynchronous and output-capability properties of . For simplicity we present them on monadic prefixes.

Lemma 2

We have \( \overline{a} b \approx {\varvec{\nu }} c\, (\overline{a} c\,\,|\,\,! c(x).\overline{b} x)\). Moreover, if b is linear, then the replication can be removed thus: \( \overline{a} b \approx {\varvec{\nu }} c\, (\overline{a} c\,\,|\,\,c(x).\overline{b} x).\)

Next, we report some distributivity laws for private replications, i.e., for systems of the form

$$\begin{aligned} {\varvec{\nu }} y\, (P \,\,|\,\, ! y(\widetilde{q}).Q) \end{aligned}$$

in which y may occur free in P and Q only in output position. One should think of Q as a private resource of P, for P is the only process who can access Q; indeed P can activate as many copies of Q as needed. One such law has already been given as Lemma 1(2). (The laws can be generalised to the full \(\pi \)-calculus, but need stronger assumptions.)

Lemma 3

Suppose a occurs free in P, R, Q only in output position. Then:

  1. 1.

    \({\varvec{\nu }} a\, (P \,\,|\,\,R \,\,|\,\, ! a({\widetilde{b}}).Q) \sim {\varvec{\nu }} a\, (P \,\,|\,\, ! a({\widetilde{b}}).Q) \,\,|\,\,{\varvec{\nu }} a\, (R \,\,|\,\, ! a({\widetilde{b}}).Q) \);

  2. 2.

    \({\varvec{\nu }} a\, ( ( ! P ) \,\,|\,\, ! a({\widetilde{b}}).Q) \sim ! {\varvec{\nu }} a\, (P \,\,|\,\, ! a({\widetilde{b}}).Q)\);

  3. 3.

    \({\varvec{\nu }} a\, ( \alpha .P \,\,|\,\, ! a({\widetilde{b}}).Q) \sim \alpha .{\varvec{\nu }} a\, (P \,\,|\,\, ! a({\widetilde{b}}).Q)\), if \({\mathrm{\mathsf {bn}}}(\alpha )\cap {\mathrm{\mathsf {fn}}}(a(\widetilde{b}).Q ) = \emptyset \) and \(a\not \in {\mathrm{\mathsf {n}}}(\alpha )\);

  4. 4.

    \({\varvec{\nu }} a\, ( ({\varvec{\nu }} c\,P ) \,\,|\,\, ! a({\widetilde{b}}).Q) \sim {\varvec{\nu }} c\,{\varvec{\nu }} a\, (P \,\,|\,\, ! a({\widetilde{b}}).Q)\) if \(c\not \in {\mathrm{\mathsf {fn}}}(a(\widetilde{b}).Q)\).

has also sharper properties concerning labelled characterisation of bisimilarity and associated congruence properties [3, 12].

3 The \(\lambda \)-calculus

We use M, N to range over the set \(\varLambda \) of \(\lambda \)-terms, and x, y, z to range over variables. The set \(\varLambda \) of \(\lambda \)-terms is given by the grammar:

A redex is a term of the form \((\lambda x. M) N\), and then its contractum is . In call-by-name evaluation [19], the redex is always at the extreme left of a term. We omit the standard evaluation rules.

Call-by-need [2, 28] optimises call-by-name as follows, so to guarantee that in the contractum the evaluation of N is not performed more than once. Roughly, N is placed in an environment, and the evaluation continues on M. When x is needed (i.e., x reaches the leftmost position), then N is evaluated and, if a value (i.e., an abstraction) is obtained, say V, then V replaces x (value V can replace all occurrences of x or, more commonly, only the leftmost occurrence, and then other occurrences of x when they reach the outermost position). Call-by-need is best presented in a graph; or in a system with a \(\mathtt{let}\) construct to represent sharing. We refer to Ariola et al. [2] for details, as they are not essential for understanding the remainder of the paper; see also the references in Sect. 5.

We sometimes omit \( \lambda \) in nested abstractions, thus for example, \(\lambda x_1 x_2. M\) stands for \( \lambda x_1. \lambda x_2. M\). We assume the standard concepts of free and bound variables and substitutions, and identify \(\alpha \)-convertible terms. Thus, throughout the paper ‘\(=\)’ is syntactic equality modulo \(\alpha \)-conversion.

Following the call-by-value terminology, the set of abstractions and variables are the values. (Indeed, call-by-need may also be thought of as a modified form of call-by-value, in which the evaluation of the argument of a function \(\lambda x. M\) is made only when x is used for the first time, rather than before performing the reduction.)

4 The Encoding and Its Properties

4.1 Background Material

Figure 2 presents the call-by-name and call-by-need encodings [16, 24]. The call-by-name one is a variant of the original encoding by Milner [14], with the advantage that it can be written in and can be easily modified to follow call-by-need.

We explain the encodings. The important part is the treatment of application. Both in call-by-name and in call-by-need, a function located at q (its ‘location’) is a process that signals to be a function on q, and then receives a pointer x to the argument N together with the location p for the next interaction. Now the evaluation of M continues. The difference between call-by-name and call-by-need arises when the argument N is needed. This is signaled by an output at x that also provides the location for the evaluation of a copy of N. In call-by-name, every output at x triggers the evaluation of a new copy of N. In call-by-need, in contrast, the evaluation is made only the first time. Precisely, in call-by-need N is evaluated at the first request and, when it becomes a value, a pointer to this value is returned (instantiating w, in the table). This pointer is returned to the process that requested N. When further requests for N are made, the pointer is returned immediately. Thus, for instance, in the call-by-name encoding of \((\lambda . xx) (II)\) term II is evaluated twice, whereas in the call-by-need encoding only once. In all encodings, the location names (in the table, the names ranged over by p, q, r) are linear.

Fig. 2.
figure 2

The encoding of call-by-name and call-by-need

Full size image

Correcteness of call-by-name has been studied in depth. In particular, it has been shown that \(\beta \)-reduction is validated by the encoding, that the encoding gives rise to a term model for the \(\lambda \)-calculus, and that the equivalence on \(\lambda \)-terms induced by the encoding corresponds to the best tree-structures of the \(\lambda \)-calculus—which are also at the heart of its denotational semantics—namely Böhm Trees and Lévy-Longo Trees [14, 23] Correctness of the call-by-need encoding has been studied only by Brock and Ostheimer [5], and only for operational correspondence with respect to Ariola et al.’s system [2]. (The encoding in Fig. 2 is actually a minor improvement over that in [5]—avoiding one reduction step during a \(\beta \)-reducition—and maintains the results of operational correspondence in [5] recalled below.) Following Ariola et al.’s system [2] we write \(M \Downarrow \) if the call-by-need computation of M terminates, and \(M \Uparrow \) it the computation does not terminate.

Theorem 1

(Brock and Ostheimer [5]). We have, for M closed:

  1. 1.

    \(M \Downarrow \) iff \( \mathcal{{N}} [\! [ M ] \! ] {p} \Downarrow _p\);

  2. 2.

    \(M \Uparrow \) iff \( \mathcal{{N}} [\! [ M ] \! ] {p} \Uparrow \).

The proof in [5] considers an extended version of the call-by-need system in [2], one that yields a closer (nearly one-to-one) correspondence between reductions in the call-by-need system and reductions on the encoding \(\pi \)-calculus processes.

Note that, since M is closed, the only free name of \( \mathcal{{N}} [\! [ M ] \! ] {p} \) is p; and since p is used in \( \mathcal{{N}} [\! [ M ] \! ] {p} \) in output, the first visible action of \( \mathcal{{N}} [\! [ M ] \! ] {p} \) (if there is one) is an output at p.

However, operational correspondence alone is not fully satisfactory as a criterium for correctness. It does not ensure foundamental semantic properties of the source language terms. In the following sections we focus on the validity of \(\beta \)-reduction.

4.2 \(\beta \)-validity

We consider in this section a few cases of validity of \(\beta \)-reduction; that is, the property that a \(\beta \)-redex \((\lambda x. M) N \) and its contractum are barbed congruent when represented as processes.

A form of \(\beta \)-reduction that is straightforward to handle is one in which the argument is never used.

Theorem 2

If then .

A more interesting form deals with \(\beta \)-reduction between closed values.

Theorem 3

.

Proof

Using algebraic reasoning, we first derive:

figure i

where the two occurrences of \(\approx \) represent applications of law (1) of Lemma 1, and the two occurrences of \(\sim \) are due to laws (2) and (3) of the same lemma, respectively.

Now we proceed by induction on the structure of M. If M is variable different from x then the two replications at v and x can be garbage-collected and we are done. If \(M = x\), then

where \(\approx \) is obtained from law (1) of Lemma 1, and \(\equiv \) from the garbage-collection laws of Definition 1.

When M is an abstraction or an application, we proceed by induction and exploit the distributivity properties of private replications in Lemma 3.

Finally we consider the case when the argument of the function is divergent—a form of \(\beta \)-reduction that is not valid in call-by-value.

Theorem 4

Suppose \((\lambda x. M ) N\) is closed. If \(N \Uparrow \) then we have .

Proof

Using Theorem 1 we have \( \mathcal{{N}} [\! [ N ] \! ] {q} \Uparrow \), for any q, hence \( \mathcal{{N}} [\! [ N ] \! ] {q} \approx {\varvec{0}}\). As a consequence, using algebraic reasoning similar to that in the proof of Theorem 3, we obtain

$$ \begin{array}{rcl} \mathcal{{N}} [\! [ (\lambda x. M) N ] \! ] {p}\approx & {} {\varvec{\nu }} x\, ( \mathcal{{N}} [\! [ M ] \! ] {p} \,\,|\,\,x(r).{\varvec{0}}) \end{array} $$

Now, since x occurs in \( \mathcal{{N}} [\! [ M ] \! ] {p} \) only in output subject position, each output at x, say \(\overline{x} r\), can be removed, or replaced by \( \mathcal{{N}} [\! [ N ] \! ] {r} \) (because in the relation \(\approx \) with \({\varvec{0}}\)), up-to \(\approx \). This yields .

4.3 Failure of General \(\beta \)-validity

However, in call-by-name and call-by-need \(\beta \)-reduction is not confined to values. We show that, in the call-by-need encoding, the general \(\beta \)-reduction fails. Notably \(\beta \)-reduction fails when the argument of the function is a variable. For this we show that

$$\begin{aligned} \mathcal{{N}} [\! [ y y ] \! ] {p} \not \approx \mathcal{{N}} [\! [ (\lambda z. zz) y ] \! ] {p} \end{aligned}$$
(1)

While for simplicity this counterexample is shown for open terms, a similar one can be given for closed terms, by closing the two terms with an abstraction, i.e.,

$$ \mathcal{{N}} [\! [ \lambda y . (y y) ] \! ] {p} \not \approx \mathcal{{N}} [\! [ \lambda y . ((\lambda z. zz) y) ] \! ] {p} $$

The remainder of the section is devoted to the proof of (1). We first unroll the initial traces of the two processes (the only traces that they can perform) We have:

figure j

Since the above is the only possible trace of the term, we have

$$\begin{aligned} \mathcal{{N}} [\! [ y y ] \! ] {p} \sim \overline{y}(q) . q(v).{\varvec{\nu }} x\, \overline{v}\langle x,p \rangle . x(r).\overline{y}(q') . q'(w).( \overline{r}{w}\,\,|\,\,! x(r'). \overline{r'}{w} ) \end{aligned}$$
(2)

We now consider the analogous trace for \( \mathcal{{N}} [\! [ (\lambda z. zz ) y ] \! ] {p} \). Below, the uses of \(\equiv \) are due to some garbage-collection of restrictions and private inputs (possibly replicated), and some rearrangements of the scopes of some restrictions; the use of \(\sim \) is due to (2).

figure k

Again, the above is the only possible trace for the term. Up-to some renaming, the final derivative is the same as the final derivative of the trace emanating from \( \mathcal{{N}} [\! [ yy ] \! ] {p} \) examined earlier. However, the two traces are different—the first is longer. As a consequence, the two terms can be distinguished, for instance in the context

$$ C {\mathop {=}\limits ^{\text{ def }}}{\varvec{\nu }} y\, ( [ \cdot ] \,\,|\,\,y(q).\overline{q}(v) . v(x,p).{\varvec{\nu }} r\, ( \overline{x} r\,\,|\,\,y(q').\overline{h} )) $$

The observable output at h becomes visible only when the context is filled with the first term, \( \mathcal{{N}} [\! [ yy ] \! ] {p} \) (the one that produces the longer trace).

In contrast, in the call-by-name encoding the validity of the full \(\beta \)-reduction holds [23]. Therefore the above counterexample not only shows that the call-by-need encoding is observably different from the call-by-name one; it also tells us that the properties that the two encoding satisfy are quite different.

4.4 A Refined Encoding

In this section we experiment with a refinement \(\mathcal{{R}}{}\) of the encoding so to improve on the problems described in Sect. 4.3.

Such encoding is shown in Fig. 3. In the definition of application for call-by-need, the argument of a function is interrogated only once, the first time the argument is used. Future uses of the argument will directly use the answer so received, without repeating the interrogation—this is indeed the essence of the call-by-need optimisation over call-by-name. To mirror this policy we modify the encoding of an abstraction \(\lambda x. M\), so that the body M will interrogate the parameter x only once. As a consequence, in this refined encoding when the head ‘\(\lambda x\)’ of the function is consumed a local entry is left that takes care of the dialogue with x; in particular the local entry makes sure that x is consulted only once. The refined encoding, while it exhibits more interactions than the original one, in a distributed setting may be thought of as an optimisation of the latter, as the interactions with the new local entry replace interactions with the possibly remote actual parameter for x. We write \(\mathtt{{LE}}(x,y) \) for a local entry in which the internal resource is x and the external one is y; it will be convenient to break its definition into two parts, using the auxiliary local entry \( \mathtt{{LE'}}(s,r,x)\); see Fig. 3.

The local entry is unnecessary if the internal resource is used only once.

Fig. 3.
figure 3

The refined call-by-need encoding

Full size image

Lemma 4

Suppose \(z'\) appears only once in M. Then

Proof

By induction on the structure of M. The most interesting case is when \(M = z'\), in which case we exploit the (linear) law of in Lemma 2. When M is an application we exploit the hypothesis (\(z'\) occurring only once), and simple algebraic manipulation, so to be able to carry out the induction.

The next lemma shows that local entries compose.

Lemma 5

\({\varvec{\nu }} x\, {( \mathtt{{LE}}(z,x) \,\,|\,\,\mathtt{{LE}}(x,y) )} \approx \mathtt{{LE}}(z,y)\).

Proof

We use laws (2) and (1) of Lemma 1, and the garbage-collection laws of structural congruence.

We revisite the counterexample of Sect. 4.3, that involves terms yy and \((\lambda z .zz)y\), under the refined encoding \(\mathcal{{R}}{}\). All free variables should be protected under a local entry, except for the variables that occur only once (by Lemma 4). We begin by examining \({\varvec{\nu }} y'\, (\mathcal{{R}} [\! [ y'y' ] \! ] {q} \,\,|\,\,\, \mathtt{{LE}}(y',y) )\). We have:

figure m

where the occurrence of \(\sim \) is justified by (2) (the two encodings coincide on terms that do not contain abstractions) and definition of \(\mathtt{{LE}}(y',y)\), and the occurrence of \(\approx \) comes from law (1) of Lemma 1.

We now consider the second term, \( { (\lambda z. zz ) y }\), under the refined encoding. First we note that, if the argument of a function L is a variable, then the refined encoding can be simplified thus:

figure n

Using this property, we have:

figure o

where \(\approx \) is obtained by composition of local entries (Lemma 5).

The above reasoning shows that the behaviour of the initial and refined encodings are the same on the term \({ (\lambda z. zz ) y }\):

$$ \mathcal{{R}} [\! [ (\lambda z. zz ) y ] \! ] {p} \approx \mathcal{{N}} [\! [ (\lambda z. zz ) y ] \! ] {p} $$

And it is also the same as that of the refined encoding on the \(\beta \)-contractum yy, when the free variables y are protected under the appropriate local entry, i.e.,

$$ \mathcal{{R}} [\! [ (\lambda zz) y ] \! ] {p} \approx {\varvec{\nu }} y'\, ( \mathcal{{R}} [\! [ y' y' ] \! ] {p} \,\,|\,\,\mathtt{{LE}}(y',y )) $$

The result also holds by closing up the terms:

$$ \mathcal{{R}} [\! [ \lambda y . (yy) ] \! ] {p} \approx \mathcal{{R}} [\! [ \lambda y . ((\lambda z. zz) y) ] \! ] {p} $$

In the refined encoding \(\mathcal{{R}}{}\), the local entry (necessary for confining the behaviour of yy) is produced by the encoding of the abstraction.

More generally, proceeding as above one can show that, on the encoding \(\mathcal{{R}}{}\), \(\beta \)-reduction is valid when the argument of a function is a variable. Moreover, \(\beta \)-reduction is also valid when the argument is itself a function, reasoning as in Theorem 3. We may therefore conclude that \(\beta \)-reduction is valid when the argument is a value (as it is the case for the encoding of the call-by-value strategy [24]).

We write \(\mathtt{{LE}}( \widetilde{x} , \widetilde{y} )\) for \(\mathtt{{LE}}(x_1,y_1)\,\,|\,\,\ldots \,\,|\,\,\mathtt{{LE}}(x_n,y_n)\) where n is the length of the tuples \( \widetilde{x} \) and \( \widetilde{y} \). We use V to range over values.

Theorem 5

Suppose \({\mathrm{\mathsf {fv}}}((\lambda z. M V)) \subseteq \widetilde{x} \). Then, for any y and fresh \(\widetilde{y}\), we have

Similarly to what done earlier, a local entry \(\mathtt{{LE}}(x_i,y_i)\) may be removed when the variable \(x_i\) appears at most once.

However, even in the encoding \(\mathcal{{R}}{}\), the full \(\beta \)-reduction is unvalid. As a counterexample we can use the terms (xz)(xz) and \( (\lambda y. yy )(xz)\). Indeed we have:

$$ {\varvec{\nu }} xz\,( \mathcal{{R}} [\! [ (xz)(xz) ] \! ] {p} \,\,|\,\,\mathtt{{LE}}(x,x')\,\,|\,\,\mathtt{{LE}}(z,z') \not \approx \mathcal{{R}} [\! [ (\lambda y. yy )(xz) ] \! ] {p} $$

We omit the calculations, which are rather involved. Intuitively, the difference appears because the full trace of the process computing the application xz is visible twice in the first process, whereas, in the second process, the second time, part of the trace is concealed.

5 Conclusions

Call-by-need was proposed by Wadsworth [28] as an implementation technique. Formalizations of call-by-need on a \(\lambda \)-calculus with a let construct or with environments include Ariola et al. [2], Launchbury [11], Purushothaman and Seaman [20], and Yoshida [29]. The uniform encoding in Sect. 4 is from [16]. A study of the correctness of the call-by-need encoding in Fig. 2 is in [5]. Encodings of graph reductions, related to call-by-need, into \(\pi \)-calculus were given in [4, 8] but their correctness was not studied. Niehren [15] used encodings of call-by-name, call-by-value and call-by-need \(\lambda \)-calculi into \(\pi \)-calculus to compare the time complexity of the strategies.

In the paper we have used the theory of the Asynchronous Local \(\pi \)-calculus ( ) [12] to reason about the encoding of the call-by-need \(\lambda \)-calculus strategy as processes. We have mainly focused on the validity of \(\beta \)-reduction. We have showed that various instances of the property on closed terms hold, though the general property fails. We have also considered a refined encoding in which \(\beta \)-reduction on arbitrary values (though not on arbitrary terms) holds. All this leaves us with some challenging questions, that we leave for future work:

  1. 1.

    In the refined encoding, we use special processes called local entries to protect the formal parameter of the function, thus improving the results about \(\beta \)-validity. Is it possible to further protect variables (or terms) so to recover the full \(\beta \)-validity?

  2. 2.

    Is there a different form of behavioural equivalence under which the full \(\beta \)-validity holds, in the initial or in the refined encoding?

  3. 3.

    What is an appropriate process preorder under which call-by-need can indeed be proved to be an optimisation of call-by-name?

  4. 4.

    What is the equivalence on \(\lambda \)-terms induced by the call-by-need encoding? Following the results for call-by-name and call-by-value, one expects to recover some kind of tree structure (Böhm Trees and Lévy-Longo Tree for call-by-name, Lassen’s trees [10] for call-by-value). We are not aware of similar tree structures for call-by-need. Hence investigating this question may also shed light on what should the appropriate forms of trees for call-by-need be.

In questions (2) and (3), ‘easy’ answers may be obtained by confining the testing contexts to be encodings of \(\lambda \)-calculus contexts. The challenge is to find more general and useful answers, with applications outside the realm of pure \(\lambda \)-calculi. One may consider forms of behavioural types.

In questions (1) and (2), perhaps requiring the validity of the full \(\beta \)-reduction, in the same way as for call-by-name, is too demanding. Indeed in this way probably the tree structure referred to in question (4) is likely to be the same as that for call-by-name. One may find it acceptable to limit \(\beta \)-validity to reductions between closed terms.