CallbyNeed, Neededness and All That
Abstract
We show that callbyneed is observationally equivalent to weakhead needed reduction. The proof of this result uses a semantical argument based on a (nonidempotent) intersection type system called \(\mathcal {V}\). Interestingly, system \(\mathcal {V}\) also allows to syntactically identify all the weakhead needed redexes of a term.
1 Introduction
One of the fundamental notions underlying this paper is the one of needed reduction in \(\lambda \)calculus, which is to be used here to understand (lazy) evaluation of functional programs. Key notions are those of reducible and nonreducible programs: the former are programs (represented by \(\lambda \)terms) containing nonevaluated subprograms, called reducible expressions (redexes), whereas the latter can be seen as definitive results of computations, called normal forms. It turns out that every reducible program contains a special kind of redex known as needed or, in other words, every \(\lambda \)term not in normal form contains a needed redex. A redex \(\mathsf {r}\) is said to be needed in a \(\lambda \)term t if \(\mathsf {r}\) has to be contracted (i.e. evaluated) sooner or later when reducing t to normal form, or, informally said, if there is no way of avoiding \(\mathsf {r}\) to reach a normal form.
The needed strategy, which always contracts a needed redex, is normalising [8], i.e. if a term can be reduced (in any way) to a normal form, then contraction of needed redexes necessarily terminates. This is an excellent starting point to design an evaluation strategy, but unfortunately, neededness of a redex is not decidable [8]. As a consequence, real implementations of functional languages cannot be directly based on this notion.
Our goal is, however, to establish a clear connection between the semantical notion of neededness and different implementations of lazy functional languages (e.g. Miranda or Haskell). Such implementations are based on callbyneed calculi, pioneered by Wadsworth [20], and extensively studied e.g. in [3]. Indeed, callbyneed calculi fill the gap between the wellknown operational semantics of the callbyname \(\lambda \)calculus and the actual implementations of lazy functional languages. While callbyname reevaluates an argument each time it is used –an operation which is quite expensive– callbyneed can be seen as a memoized version of callbyname, where the value of an argument is stored the first time it is evaluated for subsequent uses. For example, if Open image in new window , where Open image in new window and Open image in new window , then callbyname duplicates the argument Open image in new window , while lazy languages first reduce Open image in new window to the value I so that further uses of this argument do not need to evaluate it again.
While the notion of needed reduction is defined with respect to (full strong) normal forms, callbyneed calculi evaluate programs to special values called weakhead normal forms, which are either abstractions or arbitrary applications headed by a variable (i.e. terms of the form Open image in new window where \(t_1 \ldots t_n\) are arbitrary terms). To overcome this shortfall, we first adapt the notion of needed redex to terms that are not going to be fully reduced to normal forms but only to weakhead normal forms. Thus, informally, a redex \(\mathsf {r}\) is weakhead needed in a term t if \(\mathsf {r}\) has to be contracted sooner or later when reducing t to a weakhead normal form. The derived notion of strategy is called a weakhead needed strategy, which always contracts a weakhead needed redex.
This paper introduces two independent results about weakhead neededness, both obtained by means of (nonidempotent) intersection types [12, 13] (a survey can be found in [9]). We consider, in particular, typing system \(\mathcal {V}\) [14] and show that it allows to identify all the weakhead needed redexes of a weakhead normalising term. This is done by adapting the classical notion of principal type [17] and proving that a redex in a weakhead normalising term t is weakhead needed iff it is typed in a principally typed derivation for t in \(\mathcal {V}\).
Our second goal is to show observational equivalence between callbyneed and weakhead needed reduction. Two terms are observationally equivalent when all the empirically testable computations on them are identical. This means that a term t can be evaluated to a weakhead normal form using the callbyneed machinery if and only if the weakhead needed reduction normalises t.
This leads to the observational equivalence between callbyneed, callbyname and weakhead needed reduction.
Structure of the paper: Sect. 2 introduces preliminary concepts while Sect. 3 defines different notions of needed reduction. The type system \(\mathcal {V}\) is studied in Sect. 4. Section 5 extends \(\beta \)reduction to derivation trees. We show in Sect. 6 how system \(\mathcal {V}\) identifies weakhead needed redexes, while Sect. 7 gives a characterisation of normalisation for the weakhead needed reduction. Sect. 8 is devoted to define callbyneed. Finally, Sect. 9 presents the observational equivalence result.
2 Preliminaries
This section introduces some standard definitions and notions concerning the reduction strategies studied in this paper, that is, callbyname, head and weakhead reduction, and neededness, this later notion being based on the theory of residuals [7].
2.1 The CallbyName LambdaCalculus
The set of \(\lambda \)terms is denoted by \(\mathcal {T}_{\mathtt {a}}\). We use I, K and \(\varOmega \) to denote the terms \(\lambda {x}.{x}\), \(\lambda {x}.{\lambda {y}.{x}}\) and Open image in new window respectively. We use \({\mathtt {C}}\langle {t}\rangle \) (resp. \({\mathtt {E}}\langle {t}\rangle \)) for the term obtained by replacing the hole \(\Box \) of \(\mathtt {C}\) (resp. \(\mathtt {E}\)) by t. The sets of free and bound variables of a term t, written respectively \(\mathtt {fv}({t})\) and \(\mathtt {bv}({t})\), are defined as usual [7]. We work with the standard notion of \(\alpha \)conversion, i.e. renaming of bound variables for abstractions; thus for example Open image in new window .
A term of the form Open image in new window is called a \(\beta \)redex (or just redex when \(\beta \) is clear from the context) and \(\lambda x\) is called the anchor of the redex. The onestep reduction relation \(\mathrel {\rightarrow _{\beta }}\) (resp. \(\mathrel {\rightarrow _{\mathtt {name}}}\)) is given by the closure by contexts \(\mathtt {C}\) (resp. \(\mathtt {E}\)) of the rewriting rule Open image in new window , where Open image in new window denotes the capturefree standard higherorder substitution. Thus, callbyname forbids reduction inside arguments and \(\lambda \)abstractions, e.g. Open image in new window and Open image in new window but neither Open image in new window nor Open image in new window holds. We write \(\mathrel {\twoheadrightarrow _{\beta }}\) (resp. \(\mathrel {\twoheadrightarrow _{\mathtt {name}}}\)) for the reflexivetransitive closure of \(\mathrel {\rightarrow _{\beta }}\) (resp. \(\mathrel {\rightarrow _{\mathtt {name}}}\)).
2.2 Head, WeakHead and Leftmost Reductions
In order to introduce different notions of reduction, we start by formalising the general mechanism of reduction which consists in contracting a redex at some specific occurrence. Occurrences are finite words over the alphabet \(\{{\mathsf {0}, \mathsf {1}}\}\). We use \(\epsilon \) to denote the empty word and notation \(\mathsf {a^n}\) for \(\mathsf {n} \in \mathbb {N}\) concatenations of some letter \(\mathsf {a}\) of the alphabet. The set of occurrences of a given term is defined by induction as follows: Open image in new window ; Open image in new window ; Open image in new window .
Given two occurrences \(\mathsf {p}\) and \(\mathsf {q}\), we use the notation \(\mathsf {p} \le \mathsf {q}\) to mean that \(\mathsf {p}\) is a prefix of \(\mathsf {q}\), i.e. there is \(\mathsf {p'}\) such that \(\mathsf {p} \mathsf {p'} = \mathsf {q}\). We denote by \({t}_{\mathsf {p}}\) the subterm of t at occurrence \(\mathsf {p}\), defined as expected [4], thus for example Open image in new window . The set of redex occurrences of t is defined by Open image in new window . We use the notation \({\mathsf {r}}:{t}\mathrel {\rightarrow _{\beta }}{t'}\) to mean that \(\mathsf {r} \in \mathtt {r}\mathtt {oc}({t})\) and t reduces to \(t'\) by contracting the redex at occurrence \(\mathsf {r}\), e.g. Open image in new window . This notion is extended to reduction sequences as expected, and noted \({\rho }:{t}\mathrel {\twoheadrightarrow _{\beta }}{t'}\), where \(\rho \) is the list of all the redex occurrences contracted along the reduction sequence. We use \( nil \) to denote the empty reduction sequence, so that \({ nil }:{t}\mathrel {\twoheadrightarrow _{\beta }}{t}\) holds for every term t.
Any term t has exactly one of the following forms: Open image in new window or Open image in new window with \(n, m \ge 0\). In the latter case we say that Open image in new window is the head redex of t, while in the former case there is no head redex. Moreover, if \(n = 0\), we say that Open image in new window is the weakhead redex of t. In terms of occurrences, the head redex of t is the minimal redex occurrence of the form \(\mathsf {0^n}\) with \(\mathsf {n} \ge 0\). In particular, if it satisfies that \({t}_{\mathsf {0^k}}\) is not an abstraction for every \(\mathsf {k} \le \mathsf {n}\), it is the weakhead redex of t. A reduction sequence contracting at each step the head redex (resp. weakhead redex) of the corresponding term is called the head reduction (resp. weakhead reduction).
Given two redex occurrences \(\mathsf {r}, \mathsf {r'} \in \mathtt {r}\mathtt {oc}({t})\), we say that \(\mathsf {r}\) is totheleft of \( \mathsf {r'}\) if the anchor of \(\mathsf {r}\) is to the left of the anchor of \(\mathsf {r'}\). Thus for example, the redex occurrence \(\mathsf {0}\) is totheleft of \(\mathsf {1}\) in the term Open image in new window , and \(\mathsf {\epsilon }\) is totheleft of \(\mathsf {00}\) in Open image in new window . Alternatively, the relation totheleft can be understood as a dictionary order between redex occurrences, i.e. \(\mathsf {r}\) is totheleft of \(\mathsf {r'}\) if either \(\mathsf {r' = rq}\) with \(\mathsf {q} \ne \epsilon \) (i.e. \(\mathsf {r}\) is a proper prefix of \(\mathsf {r'}\)); or \(\mathsf {r} = \mathsf {p0q}\) and \(\mathsf {r'} = \mathsf {p1q'}\) (i.e. they share a common prefix and \(\mathsf {r}\) is on the lefthand side of an application while \(\mathsf {r'}\) is on the righthand side). Notice that in any case this implies \(\mathsf {r'} \not \le \mathsf {r}\). Since this notion defines a total order on redexes, every term not in normal form has a unique leftmost redex. The term t leftmost reduces to \(t'\) if t reduces to \(t'\) and the reduction step contracts the leftmost redex of t. For example, Open image in new window leftmost reduces to Open image in new window and Open image in new window leftmost reduces to Open image in new window . This notion extends to reduction sequences as expected.
3 Towards Neededness
Needed reduction is based on two fundamental notions: that of residual, which describes how a given redex is traced all along a reduction sequence, and that of normal form, which gives the form of the expected result of the reduction sequence. This section extends the standard notion of needed reduction [8] to those of head and weakhead needed reductions.
3.1 Residuals
Notice that \({\mathsf {p}}/{\mathsf {r}} \subseteq \mathtt {oc}({t'})\) where \({\mathsf {r}}:{t}\mathrel {\rightarrow _{\beta }}{t'}\). Furthermore, if \(\mathsf {p}\) is the occurrence of a redex in t (i.e. \(\mathsf {p} \in \mathtt {r}\mathtt {oc}({t})\)), then \({\mathsf {p}}/{\mathsf {r}} \subseteq \mathtt {r}\mathtt {oc}({t'})\), and each position in \({\mathsf {p}}/{\mathsf {r}}\) is called a residual of \(\mathsf {p}\) after reducing \(\mathsf {r}\). This notion is extended to sets of redex occurrences, indeed, the residuals of \(\mathcal {P}\) after \(\mathsf {r}\) in t are Open image in new window . In particular \({\varnothing }/{\mathsf {r}} = \varnothing \). Given \({\rho }:{t}\mathrel {\twoheadrightarrow _{\beta }}{t'}\) and \(\mathcal {P} \subseteq \mathtt {r}\mathtt {oc}({t})\), the residuals of \(\mathcal {P}\) after the sequence \(\rho \) are: Open image in new window and Open image in new window
Stability of the totheleft relation makes use of the notion of residual:
Lemma 1
Given a term t, let \(\mathsf {l}, \mathsf {r}, \mathsf {s} \in \mathtt {r}\mathtt {oc}({t})\) such that \(\mathsf {l}\) is totheleft of \(\mathsf {r}\), \(\mathsf {s} \nleq \mathsf {l}\) and \({\mathsf {s}}:{t}\mathrel {\rightarrow _{\beta }}{t'}\). Then, \(\mathsf {l} \in \mathtt {r}\mathtt {oc}({t'})\) and \(\mathsf {l}\) is totheleft of \(\mathsf {r'}\) for every \(\mathsf {r'} \in {\mathsf {r}}/{\mathsf {s}}\).
Proof
By case analysis using the definition of totheleft [15]. \(\square \)
Notice that this result does not only implies that the leftmost redex is preserved by reduction of other redexes, but also that the residual of the leftmost redex occurs in exactly the same occurrence as the original one.
Corollary 1
Given a term t, and \(\mathsf {l} \in \mathtt {r}\mathtt {oc}({t})\) the leftmost redex of t, if the reduction \({\rho }:{t}\mathrel {\twoheadrightarrow _{\beta }}{t'}\) contracts neither \(\mathsf {l}\) nor any of its residuals, then \(\mathsf {l} \in \mathtt {r}\mathtt {oc}({t'})\) is the leftmost redex of \(t'\).
Proof
By induction on the length of \(\rho \) using Lemma 1. \(\square \)
3.2 Notions of Normal Form
The expected result of evaluating a program is specified by means of some appropriate notion of normal form. Given any relation \(\mathrel {\rightarrow _{\mathcal {R}}}\), a term t is said to be in \(\mathcal {R}\)normal form (\(\mathcal {N\!F}_{\mathcal {R}}\)) iff there is no \(t'\) such that \(t \mathrel {\rightarrow _{\mathcal {R}}} t'\). A term t is \(\mathcal {R}\)normalising (\(\mathcal {W\!N}_{\mathcal {R}}\)) iff there exists \(u \in \mathcal {N\!F}_{\mathcal {R}}\) such that \(t \mathrel {\twoheadrightarrow _{\mathcal {R}}} u\). Thus, given an \(\mathcal {R}\)normalising term t, we can define the set of \(\mathcal {R}\)normal forms of t as Open image in new window .
In particular, it turns out that a term in weakhead \(\beta \)normal form (\(\mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\)) is of the form Open image in new window (\(n \ge 0\)) or \(\lambda {x}.{t}\), where \(t, t_1, \ldots , t_n\) are arbitrary terms, i.e. it has no weakhead redex. The set of weakhead \(\beta \)normal forms of t is Open image in new window
Similarly, a term in head \(\beta \)normal form (\(\mathcal {H}\mathcal {N\!F}_{\beta }\)) turns out to be of the form Open image in new window (\(n,m \ge 0\)), i.e. it has no head redex. The set of head \(\beta \)normal forms of t is given by Open image in new window .
Last, any term in \(\beta \)normal form (\(\mathcal {N\!F}_{\beta }\)) has the form Open image in new window (\(n, m \ge 0\)) where \(t_1, \ldots , t_m\) are themselves in \(\beta \)normal form. It is wellknown that the set \(\mathtt {nf}_{\beta }({t})\) is a singleton, so we may use it either as a set or as its unique element.
It is worth noticing that \(\mathcal {N\!F}_{\beta } \subset \mathcal {H}\mathcal {N\!F}_{\beta } \subset \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\). Indeed, the inclusions are strict, for instance Open image in new window is in weakhead but not in head \(\beta \)normal form, while Open image in new window is in head but not in \(\beta \)normal form.
3.3 Notions of Needed Reduction
 1.
\(\mathsf {r}\) is needed in t if every reduction sequence from t to \(\beta \)normal form uses \(\mathsf {r}\);
 2.
\(\mathsf {r}\) is head needed in t if every reduction sequence from t to head \(\beta \)normal form uses \(\mathsf {r}\);
 3.
\(\mathsf {r}\) is weakhead needed in t if every reduction sequence of t to weakhead \(\beta \)normal form uses \(\mathsf {r}\).
Notice in particular that \(\mathtt {nf}_{\beta }({t}) = \varnothing \) (resp. \(\mathtt {hnf}_{\beta }({t}) = \varnothing \) or \(\mathtt {whnf}_{\beta }({t}) = \varnothing \)) implies every redex in t is needed (resp. head needed or weakhead needed).
A onestep reduction \(\mathrel {\rightarrow _{\beta }}\) is needed (resp. head or weakhead needed), noted \(\mathrel {\rightarrow _{\mathtt {nd}}}\) (resp. \(\mathrel {\rightarrow _{\mathtt {hnd}}}\) or \(\mathrel {\rightarrow _{\mathtt {whnd}}}\)), if the contracted redex is needed (resp. head or weakhead needed). A reduction sequence \(\mathrel {\twoheadrightarrow _{\beta }}\) is needed (resp. head or weakhead needed), noted \(\mathrel {\twoheadrightarrow _{\mathtt {nd}}}\) (resp. \(\mathrel {\twoheadrightarrow _{\mathtt {hnd}}}\) or \(\mathrel {\twoheadrightarrow _{\mathtt {whnd}}}\)), if every reduction step in the sequence is needed (resp. head or weakhead needed).
Leftmost redexes and reduction sequences are indeed needed:
Lemma 2
The leftmost redex in any term not in normal form (resp. head or weakhead normal form) is needed (resp. head or weakhead needed).
Proof
By contradiction using the definition of needed [15]. \(\square \)
Theorem 1
Let \(\mathsf {r} \in \mathtt {r}\mathtt {oc}({t})\) and \({\rho }:{t}\mathrel {\twoheadrightarrow _{\beta }}{t'}\) be the leftmost reduction (resp. head reduction or weakhead reduction) starting with t such that \(t' = \mathtt {nf}_{\beta }({t})\) (resp. \(t' \in \mathtt {hnf}_{\beta }({t})\) or \(t' \in \mathtt {whnf}_{\beta }({t})\)). Then, \(\mathsf {r}\) is needed (resp. head or weakhead needed) in t iff \(\mathsf {r}\) is used in \(\rho \).
4 The Type System \(\mathcal {V}\)
In this section we recall the (nonidempotent) intersection type system \(\mathcal {V}\) [14] –an extension of those in [12, 13]– used here to characterise normalising terms w.r.t. the weakhead strategy. More precisely, we show that t is typable in system \(\mathcal {V}\) if and only if t is normalising when only weakhead needed redexes are contracted. This characterisation is used in Sect. 9 to conclude that the weakhead needed strategy is observationally equivalent to the callbyneed calculus (to be introduced in Sect. 8).
The empty multiset is denoted by \(\{\!\!\{{}\}\!\!\}_{}\). We remark that types are strict [18], i.e. the righthand sides of functional types are never multisets. Thus, the general form of a type is \({\mathcal {M}_1}\rightarrow {{\ldots }\rightarrow {{\mathcal {M}_n}\rightarrow {\tau }}}\) with \(\tau \) being the constant type or a base type variable.
Typing contexts (or just contexts), written \(\varGamma , \varDelta \), are functions from variables to multiset types, assigning the empty multiset to all but a finite set of variables. The domain of \(\varGamma \) is given by Open image in new window . The union of contexts, written \({\varGamma }\mathrel {+_{}}{\varDelta }\), is defined by Open image in new window , where \(\sqcup \) denotes multiset union. An example is \((x:\{\!\!\{{\sigma }\}\!\!\}_{}, y:\{\!\!\{{\tau }\}\!\!\}_{}) + (x:\{\!\!\{{\sigma }\}\!\!\}_{}, z:\{\!\!\{{\tau }\}\!\!\}_{}) = (x:\{\!\!\{{\sigma , \sigma }\}\!\!\}_{}, y:\{\!\!\{{\tau }\}\!\!\}_{}, z:\{\!\!\{{\tau }\}\!\!\}_{})\). This notion is extended to several contexts as expected, so that \(+_{i \in I} \varGamma _i\) denotes a finite union of contexts (when \(I = \varnothing \) the notation is to be understood as the empty context). We write \({\varGamma }\mathrel {\setminus \!\!\setminus _{}}{x}\) for the context \(({\varGamma }\mathrel {\setminus \!\!\setminus _{}}{x})(x) = \{\!\!\{{}\}\!\!\}_{}\) and \(({\varGamma }\mathrel {\setminus \!\!\setminus _{}}{x})(y) = \varGamma (y)\) if \(y \ne x\).
The constant type \(\mathtt {a}\) in rule \(\mathtt {({val})}\) is used to type values. The axiom \(\mathtt {({ax})}\) is relevant (there is no weakening) and the rule \(\mathtt {({{\!}\rightarrow {\!}e})}\) is multiplicative. Note that the argument of an application is typed \(\#(I)\) times by the premises of rule \(\mathtt {({{\!}\rightarrow {\!}e})}\). A particular case is when \(I = \varnothing \): the subterm u occurring in the typed term Open image in new window turns out to be untyped.
Intersection type systems can usually be seen as models [11], i.e. typing is stable by convertibility: if t is typable and \(t =_{\beta } t'\), then \(t'\) is typable too. This property splits in two different statements known as subject reduction and subject expansion respectively, the first one giving stability of typing by reduction, the second one by expansion. In the particular case of nonidempotent types, subject reduction refines to weighted subjectreduction, stating that not only typability is stable by reduction, but also that the size of type derivations is decreasing. Moreover, this decrease is strict when reduction is performed on special occurrences of redexes, called typed occurrences. We now introduce all these concepts.
Given a type derivation \(\varPhi \), the set \(\mathtt {TOC}({\varPhi })\) of typed occurrences of \(\varPhi \), which is a subset of \(\mathtt {oc}({\mathtt {SUBJ}({\varPhi })})\), is defined by induction on the last rule of \(\varPhi \).

If \(\mathtt {RULE}({\varPhi }) \in \{{\mathtt {({ax})}, \mathtt {({val})}}\}\), then Open image in new window .

If \(\mathtt {RULE}({\varPhi }) = \mathtt {({{\!}\rightarrow {\!}i})}\) with \(\mathtt {SUBJ}({\varPhi }) = \lambda {x}.{t}\) and \(\mathtt {PREM}({\varPhi }) = \{\!\!\{{\varPhi _{t}}\}\!\!\}\), then Open image in new window .

If Open image in new window and \(\mathtt {PREM}({\varPhi }) = \{\!\!\{{\varPhi _{t}}\}\!\!\} \sqcup \{\!\!\{{\varPhi _{u}^{i} \mid i \in I}\}\!\!\}\), then Open image in new window .
Then, \(\mathtt {TOC}({\varPhi _{KI\varOmega }}) = \{{\epsilon , \mathsf {0}, \mathsf {00}, \mathsf {01}, \mathsf {000},\mathsf {0000}}\} \subseteq \mathtt {oc}({KI\varOmega })\).
Remark 1
The weakhead redex of a typed term is always a typed occurrence.
Given \(\varPhi \) and \(\mathsf {p} \in \mathtt {TOC}({\varPhi })\), we define \({\varPhi }_{\mathsf {p}}\) as the multiset of all the subderivations of \(\varPhi \) at occurrence \(\mathsf {p}\) (a formal definition can be found in [15]). Note that \({\varPhi }_{\mathsf {p}}\) is a multiset since the subterm of \(\mathtt {SUBJ}({\varPhi })\) at position \(\mathsf {p}\) may be typed several times in \(\varPhi \), due to rule \(\mathtt {({{\!}\rightarrow {\!}e})}\).
We can now state the two main properties of system \(\mathcal {V}\), whose proofs can be found in Sect. 7 of [9].
Theorem 2
 1.
If \(\mathsf {r} \in \mathtt {TOC}({\varPhi })\), then \(\mathtt {sz}({\varPhi }) > \mathtt {sz}({\varPhi '})\).
 2.
If \(\mathsf {r} \notin \mathtt {TOC}({\varPhi })\), then \(\mathtt {sz}({\varPhi }) = \mathtt {sz}({\varPhi '})\).
Theorem 3
(Subject Expansion). Let \({\varPhi '}\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t'}:{\tau }}}\). If \(t \mathrel {\rightarrow _{\beta }} t'\), then there exists \(\varPhi \) s.t. \({\varPhi }\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\).
Note that weighted subject reduction implies that reduction of typed redex occurrences turns out to be normalising.
5 Substitution and Reduction on Derivations
The following lemma relates the typed occurrences of the trees composing a substitution and those of the substituted tree itself:
Lemma 3
 1.
\(\mathsf {p} \in \mathtt {TOC}({\varPhi _{t}})\) iff Open image in new window .
 2.
\(\mathsf {q} \in \mathtt {TOC}({\varPhi _{u}^{k}})\) for some \(k \in I\) iff there exists \(\mathsf {p} \in \mathtt {TOC}({\varPhi _{t}})\) such that \({t}_{\mathsf {p}} = x\) and Open image in new window .
Proof
By induction on \(\varPhi _{t}\). \(\square \)
Based on the previous notion of substitutions on derivations, we are now able to introduce (nondeterministic) reduction on derivation trees. The reduction relation \(\mathrel {\rightarrow _{\beta }}\) on derivation trees is then defined by first considering the following basic rewriting rules.
 1.For typed \(\beta \)redexes:
 2.For \(\beta \)redexes in untyped occurrences, with \(u \mathrel {\rightarrow _{\beta }} u'\):
As in the case of the \(\lambda \)calculus, where reduction is closed under usual term contexts, we need to close the previous relation under derivation tree contexts. However, a onestep reduction on a given subterm causes many onestep reductions in the corresponding derivation tree (recall \({\varPhi }_{\mathsf {p}}\) is defined to be a multiset). Then, informally, given a redex occurrence \(\mathsf {r}\) of t, a type derivation \(\varPhi \) of t, and the multiset of minimal subderivations of \(\varPhi \) containing \(\mathsf {r}\), written \(\mathscr {M}\), we apply the reduction rules \(\mathrel {\mapsto _{\beta ,\nu ,\xi }}\) to all the elements of \(\mathscr {M}\), thus obtaining a multiset \(\mathscr {M'}\), and we recompose the type derivation of the reduct of t (see [15] for a formal definition). This gives the reduction relation \(\mathrel {\rightarrow _{\beta }}\) on trees. A reduction sequence on derivation trees contracting only redexes in typed positions is dubbed a typed reduction sequence.
Note that typed reductions are normalising by Theorem 2, yielding a special kind of derivation. Indeed, given a type derivation \({\varPhi }\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\), we say that \(\varPhi \) is normal iff \(\mathtt {TOC}({\varPhi }) \cap \mathtt {r}\mathtt {oc}({t}) = \varnothing \). Reduction on trees induces reduction on terms: when \({\rho }:{\varPhi }\mathrel {\twoheadrightarrow _{\beta }}{\varPhi '}\), then \(\mathtt {SUBJ}({\varPhi }) \mathrel {\twoheadrightarrow _{\beta }} \mathtt {SUBJ}({\varPhi '})\). By abuse of notation we may denote both sequences with the same letter \(\rho \).
6 WeakHead Neededness and Typed Occurrences
This section presents one of our main results. It establishes a connection between weakhead needed redexes and typed redex occurrences. More precisely, we first show in Sect. 6.1 that every weakhead needed redex occurrence turns out to be a typed occurrence, whatever its type derivation is. The converse does not however hold. But, we show in Sect. 6.2 that any typed occurrence in a special kind of typed derivation (that we call principal) corresponds to a weakhead needed redex occurrence. We start with a technical lemma.
Lemma 4
Let \({\mathsf {r}}:{\varPhi _{t}}\mathrel {\rightarrow _{\beta }}{\varPhi _{t'}}\) and \(\mathsf {p} \in \mathtt {oc}({t})\) such that \(\mathsf {p} \ne \mathsf {r}\) and \(\mathsf {p} \ne \mathsf {r0}\). Then, \(\mathsf {p} \in \mathtt {TOC}({\varPhi _{t}})\) iff there exists \(\mathsf {p'} \in {\mathsf {p}}/{\mathsf {r}}\) such that \(\mathsf {p'} \in \mathtt {TOC}({\varPhi _{t'}})\).
Proof
By induction on \(\mathsf {r}\) using Lemma 3. \(\square \)
6.1 WeakHead Needed Redexes Are Typed
In order to show that every weakhead needed redex occurrence corresponds to a typed occurrence in some type derivation we start by proving that typed occurrences do not come from untyped ones.
Lemma 5
Let \({\rho }:{\varPhi _{t}}\mathrel {\twoheadrightarrow _{\beta }}{\varPhi _{t'}}\) and \(\mathsf {p} \in \mathtt {oc}({t})\). If there exists \(\mathsf {p'} \in {\mathsf {p}}/{\rho }\) such that \(\mathsf {p'} \in \mathtt {TOC}({\varPhi _{t'}})\), then \(\mathsf {p} \in \mathtt {TOC}({\varPhi _{t}})\).
Proof
Straightforward induction on \(\rho \) using Lemma 4. \(\square \)
Theorem 4
Let \(\mathsf {r}\) be a weakhead needed redex in t. Let \(\varPhi \) be a type derivation of t. Then, \(\mathsf {r} \in \mathtt {TOC}({\varPhi })\).
Proof
By Theorem 1, \(\mathsf {r}\) is used in the weakhead reduction from t to \(t' \in \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\). By Remark 1, the weakhead reduction contracts only typed redexes. Thus, \(\mathsf {r}\) or some of its residuals is a typed occurrence in its corresponding derivation tree. Finally, we conclude by Lemma 5, \(\mathsf {r} \in \mathtt {TOC}({\varPhi })\). \(\square \)
6.2 Principally Typed Redexes Are WeakHead Needed

Open image in new window , and \(\varGamma = \{{{x}:{\{\!\!\{{{\overbrace{{{\{\!\!\{{}\}\!\!\}_{}}\rightarrow {\ldots }}\rightarrow {\{\!\!\{{}\}\!\!\}_{}}}^{\text {n times}}}\rightarrow {\tau }}\}\!\!\}_{}}}\}\) and \(\tau \) is a type variable \(\alpha \) (i.e. none of the \(t_i\) are typed), or

\(t = \lambda {x}.{t'}\), and \(\varGamma = \varnothing \) and \(\tau = \mathtt {a}\).
Given a weakhead normalising term t such that \({\varPhi _t}\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\), we say that \(\varPhi _{t}\) is principally typed if \(\varPhi _{t} \mathrel {\twoheadrightarrow _{\beta }} \varPhi _{t'}\) for some \(t' \in \mathtt {whnf}_{\beta }({t})\) implies \(\varPhi _{t'}\) is normal principally typed.
Note in particular that the previous definition does not depend on the chosen weakhead normal form \(t'\): suppose \(t'' \in \mathtt {whnf}_{\beta }({t})\) is another weakhead normal form of t, then \(t'\) and \(t''\) are convertible terms by the ChurchRosser property [7] so that \(t'\) can be normal principally typed iff \(t''\) can, by Theorems 2 and 3.
Lemma 6
Let \(\varPhi _{t}\) be a type derivation with subject t and \(\mathsf {r} \in \mathtt {r}\mathtt {oc}({t}) \cap \mathtt {TOC}({\varPhi _{t}})\). Let \({\rho }:{\varPhi _{t}}\mathrel {\twoheadrightarrow _{\beta }}{\varPhi _{t'}}\) such that \(\varPhi _{t'}\) is normal. Then, \(\mathsf {r}\) is used in \(\rho \).
Proof
Straightforward induction on \(\rho \) using Lemma 4. \(\square \)
The notions of leftmost and weakhead needed reductions on (untyped) terms naturally extends to typed reductions on tree derivations. We thus have:
Lemma 7
Let t be a weakhead normalising term and \(\varPhi _{t}\) be principally typed. Then, a leftmost typed reduction sequence starting at \(\varPhi _{t}\) is weakhead needed.
Proof
By induction on the leftmost typed sequence (called \(\rho \)). If \(\rho \) is empty the result is immediate. If not, we show that t has a typed weakhead needed redex (which is leftmost by definition) and conclude by inductive hypothesis. Indeed, assume \(t \in \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\). By definition \(\varPhi _{t}\) is normal principally typed and thus it has no typed redexes. This contradicts \(\rho \) being nonempty. Hence, t has a weakhead redex \(\mathsf {r}\) (i.e. \(t \notin \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\)). Moreover, \(\mathsf {r}\) is both typed (by Remark 1) and weakhead needed (by Lemma 2). Thus, we conclude. \(\square \)
Theorem 5
Let t be a weakhead normalising term, \(\varPhi _{t}\) be principally typed and \(\mathsf {r} \in \mathtt {r}\mathtt {oc}({t}) \cap \mathtt {TOC}({\varPhi _{t}})\). Then, \(\mathsf {r}\) is a weakhead needed redex in t.
Proof
Let \({\rho }:{\varPhi _{t}}\mathrel {\twoheadrightarrow _{\beta }}{\varPhi _{t'}}\) be the leftmost typed reduction sequence where \(\varPhi _{t'}\) is normal. Note that \(\varPhi _{t'}\) exists by definition of principally typed. By Lemma 7, \(\rho \) is a weakhead needed reduction sequence. Moreover, by Lemma 6, \(\mathsf {r}\) is used in \(\rho \). Hence, \(\mathsf {r}\) is a weakhead needed redex in t. \(\square \)
As a direct consequence of Theorems 4 and 5, given a weakhead normalising term t, the typed redex occurrences in its principally typed derivation (which always exists) correspond to its weakhead needed redexes. Hence, system \(\mathcal {V}\) allows to identify all the weakhead needed redexes of a weakhead normalising term.
7 Characterising WeakHead Needed Normalisation
This section presents one of the main pieces contributing to our observational equivalence result. Indeed, we relate typing with weakhead neededness by showing that any typable term in system \(\mathcal {V}\) is normalising for weakhead needed reduction. This characterisation highlights the power of intersection types. We start by a technical lemma.
Lemma 8
Let \({\varPhi }\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\). Then, \(\varPhi \) normal implies \(t \in \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\).
Proof
By induction on \(\varPhi \) analysing the last rule applied. \(\square \)
Let \({\rho }:{t_1}\mathrel {\twoheadrightarrow _{\beta }}{t_n}\). We say that \(\rho \) is a lefttoright reduction sequence iff for every \(i < n\) if \({\mathsf {r_i}}:{t_i}\mathrel {\rightarrow _{\beta }}{t_{i+1}}\) and \(\mathsf {l_i}\) is to the left of \(\mathsf {r_i}\) then, for every \(j > i\) such that \({\mathsf {r_j}}:{t_j}\mathrel {\rightarrow _{\beta }}{t_{j+1}}\) we have that \(\mathsf {r_j} \notin {\{{\mathsf {l_i}}\}}/{\rho _{ij}}\) where \({\rho _{ij}}:{t_i}\mathrel {\twoheadrightarrow _{\beta }}{t_j}\) is the corresponding subsequence of \(\rho \). In other words, for every j and every \(i < j\), \(\mathsf {r_j}\) is not a residual of a redex to the left of \(\mathsf {r_i}\) (relative to the given reduction subsequence from \(t_i\) to \(t_j\)) [7].
Lefttoright reductions define in particular standard strategies, which give canonical ways to construct reduction sequences from one term to another:
Theorem 6
([7]). If \(t \mathrel {\twoheadrightarrow _{\beta }} t'\), there exists a lefttoright reduction from t to \(t'\).
Theorem 7
Let \(t \in \mathcal {T}_{\mathtt {a}}\). Then, \({\varPhi }\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\) iff \(t \in \mathcal {W\!N}_{\mathtt {whnd}}\).
Proof
We claim that all reduction steps in \(t_1 \mathrel {\twoheadrightarrow _{\beta }} t_n\) are leftmost. Assume towards a contradiction that there exists \(k < n\) such that \({\mathsf {r}}:{t_k}\mathrel {\rightarrow _{\beta }}{t_{k+1}}\) and \(\mathsf {r}\) is not the leftmost redex of \(t_k\) (written \(\mathsf {l_{k}}\)). Since \(\rho \) is a lefttoright reduction, no residual of \(\mathsf {l_{k}}\) is contracted after the kth step. Thus, there is a reduction sequence from \(t_k \notin \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\) to \(t_n \in \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta }\) such that \(\mathsf {l_{k}}\) is not used in it. This leads to a contradiction with \(\mathsf {l_{k}}\) being weakhead needed in \(t_k\) by Lemma 2.
As a consequence, there is a leftmost reduction sequence \(t \mathrel {\twoheadrightarrow _{\beta }} t_n\). Moreover, by Lem. 2, \(t \mathrel {\twoheadrightarrow _{\mathtt {whnd}}} t_n \in \mathcal {W}\mathcal {H}\mathcal {N\!F}_{\beta } = \mathcal {N\!F}_{\mathtt {whnd}}\). Thus, \(t \in \mathcal {W\!N}_{\mathtt {whnd}}\).
\(\Leftarrow \)) Consider the reduction \({\rho }:{t}\mathrel {\twoheadrightarrow _{\mathtt {whnd}}}{t'}\) with \(t' \in \mathtt {whnf}_{\beta }({t})\). Let \({\varPhi '}\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t'}:{\tau }}}\) be the normal principally typed derivation for \(t'\) as defined in Sect. 6.2. Finally, we conclude by induction in \(\rho \) using Theorem 3, \({\varPhi }\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\). \(\square \)
8 The CallbyNeed LambdaCalculus
This section describes the syntax and the operational semantics of the callbyneed lambdacalculus introduced in [1]. It is more concise than previous specifications of callbyneed [2, 3, 10, 16], but it is operationally equivalent to them [6], so that our results could also be presented by using alternative specifications.
We denote the set of terms by \(\mathcal {T}_{\mathtt {e}}\). Terms of the form \({t}[{x}\backslash {u}]\) are closures, and \([{x}\backslash {u}]\) is called an explicit substitution (ES). The set of \(\mathcal {T}_{\mathtt {e}}\)terms without ES is the set of terms of the \(\lambda \)calculus, i.e. \(\mathcal {T}_{\mathtt {a}}\). The notions of free and bound variables are defined as expected, in particular, Open image in new window , Open image in new window , Open image in new window and Open image in new window . We extend the standard notion of \(\alpha \)conversion to ES, as expected.
We use the special notation \({\mathtt {N}}\langle \langle {u}\rangle \rangle \) or \({\mathtt {L}}\langle \langle {u}\rangle \rangle \) when the free variables of u are not captured by the context, i.e. there are no abstractions or explicit substitutions in the context that binds the free variables of u. Thus for example, given Open image in new window , we have Open image in new window , but Open image in new window cannot be written as \({\mathtt {N}}\langle \langle {x}\rangle \rangle \). Notice the use of this special notation in the last case of needed contexts, an example of such case being Open image in new window
9 Observational Equivalence
The results in Sect. 7 are used here to prove soundness and completeness of callbyneed w.r.t weakhead neededness, our second main result. More precisely, a callbyneed interpreter stops in a value if and only if the weakhead needed reduction stops in a value. This means that callbyneed and callbyname are observationally equivalent.
Formally, given a reduction relation \(\mathcal {R}\) on a term language \(\mathcal {T}\), and an associated notion of context for \(\mathcal {T}\), we define t to be observationally equivalent to u, written \(t \cong _{\mathcal {R}} u\), iff \({\mathtt {C}}\langle {t}\rangle \in \mathcal {W\!N}_{\mathcal {R}} \Leftrightarrow {\mathtt {C}}\langle {u}\rangle \in \mathcal {W\!N}_{\mathcal {R}}\) for every context \(\mathtt {C}\). In order to show our final result we resort to the following theorem:
Theorem 8
 1.
Let \(t \in \mathcal {T}_{\mathtt {a}}\). Then, \({\varPhi }\rhd _{\mathcal {V}}{{\varGamma }\vdash {{t}:{\tau }}}\) iff \(t \in \mathcal {W\!N}_{\mathtt {name}}\).
 2.
For all terms t and u in \(\mathcal {T}_{\mathtt {a}}\), \(t \cong _{\mathtt {name}} u\) iff \(t \cong _{\mathtt {need}} u\).
These observations allows us to conclude:
Theorem 9
For all terms t and u in \(\mathcal {T}_{\mathtt {a}}\), \(t \cong _{\mathtt {whnd}} u\) iff \(t \cong _{\mathtt {need}} u\).
10 Conclusion
We establish a clear connection between the semantical standard notion of neededness and the syntactical concept of callbyneed. The use of nonidempotent types –a powerful technique being able to characterise different operational properties– provides a simple and natural tool to show observational equivalence between these two notions. We refer the reader to [5] for other proof techniques (not based on intersection types) used to connect semantical notions of neededness with syntactical notions of lazy evaluation.
An interesting (and not difficult) extension of our result in Sect. 6 is that callbyneed reduction (defined on \(\lambda \)terms with explicit substitutions) contracts only \(\mathtt {dB}\) weakhead needed redexes, for an appropriate (and very natural) notion of weakhead needed redex for \(\lambda \)terms with explicit substitutions. A technical tool to obtain such a result would be the type system \(\mathcal {A}\) [14], a straightforward adaptation of system \(\mathcal {V}\) to callbyneed syntax.
Given the recent formulation of strong callbyneed [6] describing a deterministic callbyneed strategy to normal form (instead of weakhead normal form), it would be natural to extend our technique to obtain an observational equivalence result between the standard notion of needed reduction (to full normal forms) and the strong callbyneed strategy. This remains as future work.
References
 1.Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1–3 September 2014, pp. 363–376. ACM (2014)Google Scholar
 2.Ariola, Z.M., Felleisen, M.: The callbyneed lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)MathSciNetCrossRefGoogle Scholar
 3.Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: The callbyneed lambda calculus. In: Cytron, R.K., Lee, P. (eds.) Conference Record of POPL 1995: 22nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, 23–25 January 1995, pp. 233–246. ACM Press (1995)Google Scholar
 4.Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, New York (1998)CrossRefGoogle Scholar
 5.Balabonski, T.: La pleine paresse, une certaine optimalité. Ph.D. Thesis, Université ParisDiderot (2012)Google Scholar
 6.Balabonski, T., Barenbaum, P., Bonelli, E., Kesner, D.: Foundations of strong call by need. PACMPL 1(ICFP), 20:1–20:29 (2017)Google Scholar
 7.Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics, vol. 103, revised edition, North Holland (1984)Google Scholar
 8.Barendregt, H.P., Kennaway, J.R., Klop, J.W., Sleep, M.R.: Needed reduction and spine strategies for the lambda calculus. Inf. Comput. 75(3), 191–231 (1987)MathSciNetCrossRefGoogle Scholar
 9.Bucciarelli, A., Kesner, D., Ventura, D.: Nonidempotent intersection types for the lambdacalculus. Logic J. IGPL 25(4), 431–464 (2017)MathSciNetGoogle Scholar
 10.Chang, S., Felleisen, M.: The callbyneed lambda calculus, revisited. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 128–147. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642288692_7CrossRefGoogle Scholar
 11.Coppo, M., DezaniCiancaglini, M.: An extension of the basic functionality theory for the \(\lambda \)calculus. Notre Dame J. Formal Log. 21(4), 685–693 (1980)MathSciNetCrossRefGoogle Scholar
 12.de Carvalho, D.: Sémantiques de la logique linéaire et temps de calcul. Ph.D. thesis, Université AixMarseille II (2007)Google Scholar
 13.Gardner, P.: Discovering needed reductions using type theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 555–574. Springer, Heidelberg (1994). https://doi.org/10.1007/3540578870_115CrossRefGoogle Scholar
 14.Kesner, D.: Reasoning about callbyneed by means of types. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 424–441. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662496305_25CrossRefzbMATHGoogle Scholar
 15.Kesner, D., Ríos, A., Viso, A.: Callbyneed, neededness and all that. Extended report (2017). https://arxiv.org/abs/1801.10519
 16.Maraist, J., Odersky, M., Wadler, P.: The callbyneed lambda calculus. J. Funct. Program. 8(3), 275–317 (1998)MathSciNetCrossRefGoogle Scholar
 17.Rocca, S.R.D.: Principal type scheme and unification for intersection type discipline. Theor. Comput. Sci. 59, 181–209 (1988)MathSciNetCrossRefGoogle Scholar
 18.van Bakel, S.: Complete restrictions of the intersection type discipline. Theor. Comput. Sci. 102(1), 135–163 (1992)MathSciNetCrossRefGoogle Scholar
 19.Vial, P.: Nonidempotent intersection types, beyond lambdacalculus. Ph.D. thesis, Université ParisDiderot (2017)Google Scholar
 20.Wadsworth, C.P.: Semantics and pragmatics of the lambda calculus. Ph.D. thesis, Oxford University (1971)Google Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.